1 /*  Boolector: Satisfiability Modulo Theories (SMT) solver.
2  *
3  *  Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
4  *
5  *  This file is part of Boolector.
6  *  See COPYING for more information on using this software.
7  */
8 
9 #ifndef BTORSAT_H_INCLUDED
10 #define BTORSAT_H_INCLUDED
11 
12 #include <stdbool.h>
13 #include <stdio.h>
14 
15 #include "btortypes.h"
16 #include "utils/btormem.h"
17 #include "utils/btorstack.h"
18 
19 /*------------------------------------------------------------------------*/
20 
21 typedef struct BtorSATMgr BtorSATMgr;
22 
23 struct BtorSATMgr
24 {
25   /* Note: direct solver reference for PicoSAT, wrapper object for for
26    *	   Lingeling (BtorLGL) and MiniSAT (BtorMiniSAT). */
27   void *solver;
28   Btor *btor;
29 
30   const char *name; /* solver name */
31 
32   /* Note: do not change order! (btor_sat_mgr_clone relies on inc_required
33    * to come first of all fields following below.) */
34   bool inc_required;
35 #ifdef BTOR_USE_LINGELING
36   bool fork;
37 #endif
38   FILE *output;
39 
40   bool initialized;
41   int32_t satcalls;
42   int32_t clauses;
43   int32_t true_lit;
44   int32_t maxvar;
45 
46   double sat_time;
47 
48   struct
49   {
50     int32_t (*fun) (void *); /* termination callback */
51     void *state;
52   } term;
53 
54   bool have_restore;
55   struct
56   {
57     void (*add) (BtorSATMgr *, int32_t); /* required */
58     void (*assume) (BtorSATMgr *, int32_t);
59     int32_t (*deref) (BtorSATMgr *, int32_t); /* required */
60     void (*enable_verbosity) (BtorSATMgr *, int32_t);
61     int32_t (*failed) (BtorSATMgr *, int32_t);
62     int32_t (*fixed) (BtorSATMgr *, int32_t);
63     int32_t (*inc_max_var) (BtorSATMgr *);
64     void *(*init) (BtorSATMgr *); /* required */
65     void (*melt) (BtorSATMgr *, int32_t);
66     int32_t (*repr) (BtorSATMgr *, int32_t);
67     void (*reset) (BtorSATMgr *);           /* required */
68     int32_t (*sat) (BtorSATMgr *, int32_t); /* required */
69     void (*set_output) (BtorSATMgr *, FILE *);
70     void (*set_prefix) (BtorSATMgr *, const char *);
71     void (*stats) (BtorSATMgr *);
72     void *(*clone) (Btor *btor, BtorSATMgr *);
73     void (*setterm) (BtorSATMgr *);
74   } api;
75 };
76 
77 /*------------------------------------------------------------------------*/
78 
79 struct BtorCnfPrinter
80 {
81   FILE *out;
82   BtorIntStack clauses;
83   BtorIntStack assumptions;
84   BtorSATMgr *smgr; /* SAT manager wrapped by DIMACS printer. */
85 };
86 
87 typedef struct BtorCnfPrinter BtorCnfPrinter;
88 
89 /*------------------------------------------------------------------------*/
90 
91 /* Creates new SAT manager.
92  * A SAT manager is used by nearly all functions of the SAT layer.
93  */
94 BtorSATMgr *btor_sat_mgr_new (Btor *btor);
95 
96 bool btor_sat_mgr_has_clone_support (const BtorSATMgr *smgr);
97 
98 bool btor_sat_mgr_has_incremental_support (const BtorSATMgr *smgr);
99 
100 void btor_sat_mgr_set_term (BtorSATMgr *smgr,
101                             int32_t (*fun) (void *),
102                             void *state);
103 
104 /* Clones existing SAT manager (and underlying SAT solver). */
105 BtorSATMgr *btor_sat_mgr_clone (Btor *btor, BtorSATMgr *smgr);
106 
107 /* Deletes SAT manager from memory. */
108 void btor_sat_mgr_delete (BtorSATMgr *smgr);
109 
110 /* Generates fresh CNF indices.
111  * Indices are generated in consecutive order. */
112 int32_t btor_sat_mgr_next_cnf_id (BtorSATMgr *smgr);
113 
114 /* Mark old CNF index as not used anymore. */
115 void btor_sat_mgr_release_cnf_id (BtorSATMgr *smgr, int32_t);
116 
117 #if 0
118 /* Returns the last CNF index that has been generated. */
119 int32_t btor_get_last_cnf_id_sat_mgr (BtorSATMgr * smgr);
120 #endif
121 
122 void btor_sat_enable_solver (BtorSATMgr *smgr);
123 
124 /* Inits the SAT solver. */
125 void btor_sat_init (BtorSATMgr *smgr);
126 
127 /* Returns if the SAT solver has already been initialized */
128 bool btor_sat_is_initialized (BtorSATMgr *smgr);
129 
130 /* Sets the output file of the SAT solver. */
131 void btor_sat_set_output (BtorSATMgr *smgr, FILE *output);
132 
133 /* Prints statistics of SAT solver. */
134 void btor_sat_print_stats (BtorSATMgr *smgr);
135 
136 /* Adds literal to the current clause of the SAT solver.
137  * 0 terminates the current clause.
138  */
139 void btor_sat_add (BtorSATMgr *smgr, int32_t lit);
140 
141 /* Adds assumption to SAT solver.
142  * Requires that SAT solver supports this.
143  */
144 void btor_sat_assume (BtorSATMgr *smgr, int32_t lit);
145 
146 /* Checks whether an assumption failed during
147  * the last SAT solver call 'btor_sat_check_sat'.
148  */
149 int32_t btor_sat_failed (BtorSATMgr *smgr, int32_t lit);
150 
151 /* Solves the SAT instance.
152  * limit < 0 -> no limit.
153  */
154 BtorSolverResult btor_sat_check_sat (BtorSATMgr *smgr, int32_t limit);
155 
156 /* Gets assignment of a literal (in the SAT case).
157  * Do not call before calling btor_sat_check_sat.
158  */
159 int32_t btor_sat_deref (BtorSATMgr *smgr, int32_t lit);
160 
161 /* Gets equivalence class represenative of a literal
162  * or the literal itself if it is in a singleton
163  * equivalence, fixed or eliminated.
164  * Do not call before calling btor_sat_check_sat.
165  */
166 int32_t btor_sat_repr (BtorSATMgr *smgr, int32_t lit);
167 
168 /* Gets assignment of a literal (in the SAT case)
169  * similar to 'deref', but only consider top level.
170  * Do not call before calling btor_sat_check_sat.
171  */
172 int32_t btor_sat_fixed (BtorSATMgr *smgr, int32_t lit);
173 
174 /* Resets the status of the SAT solver. */
175 void btor_sat_reset (BtorSATMgr *smgr);
176 
177 #endif
178