1 /*-------------------------------------------------------------------------*/
2 /* Copyright 2010-2014 Armin Biere Johannes Kepler University Linz Austria */
3 /*-------------------------------------------------------------------------*/
5 #ifndef lglib_h_INCLUDED
6 #define lglib_h_INCLUDED
8 #include <stdio.h> // for 'FILE'
9 #include <stdlib.h> // for 'int64_t'
11 //--------------------------------------------------------------------------
14 #define LGL_SATISFIABLE 10
15 #define LGL_UNSATISFIABLE 20
17 //--------------------------------------------------------------------------
19 typedef struct LGL LGL;
21 //--------------------------------------------------------------------------
23 LGL * lglinit (void); // constructor
24 void lglrelease (LGL *); // destructor
26 // externally provided memory manager ...
28 typedef void * (*lglalloc) (void*mem, size_t);
29 typedef void (*lgldealloc) (void*mem, void*, size_t);
30 typedef void * (*lglrealloc) (void*mem, void *ptr, size_t old, size_t);
32 LGL * lglminit (void *mem, lglalloc, lglrealloc, lgldealloc);
34 // 'Cloning' produces identicaly behaving solvers.
36 LGL * lglclone (LGL *);
37 LGL * lglmclone (LGL *, void *mem, lglalloc, lglrealloc, lgldealloc);
39 int lglunclone (LGL * dst, LGL * src); // does not release 'src'
41 // 'Forking' copies only irredundant clauses and also uses internal variable
42 // indices of the parent as external variable indices. Thus 'parent' and
43 // the forked off 'child' do neither exactly work the same way, nor do they
44 // use from the API point of view the same set of variables. They are
45 // satisfiability equivalent. If the child becomes unsatisfiable the parent
46 // can be assumed to be unsatisfiable too and thus 'lgljoin' would just add
47 // the empty clause to the parent. If the child produces a satisfying
48 // assignment, this assignment is turned into an assignment of the parent by
49 // 'lgljoin'. Parents can be forked multiple times. A child has exactly
50 // one parent. Parents and children can be released independently. Between
51 // 'lglfork' and 'lgljoin' no other operations but further 'lglfork' are
52 // allowed. The effect ot multiple 'lgljoin' with the same parent is
53 // unclear at this point. The same memory manager is use for the child and
54 // the parent. Options, prefix, output file and the callbacks for 'getime'
55 // and 'onabort' are copied too (if set).
57 LGL * lglfork (LGL * parent);
58 int lgljoin (LGL * parent, LGL * child); // does not release 'child'
60 // Both 'Cloning' and 'Forking' can be used to implement 'Push & Pop', but
61 // the asymmetric forking is more similar to the classical way of
62 // implementing it, needs less resources since for instance eliminated
63 // variables do not occupy any memory in the children, but requires lifting
64 // back satisfying assignments explicitly (through the whole parent chain).
65 // If these full satisfying assignments are really needed actually cloning
66 // could be more space efficient too. Assume you want to split the solver
67 // into two instances, one with a literal set to false, the other one to
68 // true. Then cloning allows you to produce two independent branches, while
69 // for forking you need three, since the root / top solver still has to be
70 // kept for lifting back a potential assignment.
72 //--------------------------------------------------------------------------
74 const char * lglversion ();
76 void lglbnr (const char * name,
78 FILE * file); // ... banner
80 void lglusage (LGL *); // print usage "-h"
81 void lglopts (LGL *, const char * prefix, int); // ... defaults "-d" | "-e"
82 void lglrgopts (LGL *); // ... option ranges "-r"
83 void lglpcs (LGL *, int mixed); // ... PCS file
84 void lglsizes (LGL *); // ... data structure sizes
86 //--------------------------------------------------------------------------
87 // setters and getters for options
89 void lglsetout (LGL *, FILE*); // output file for report
90 void lglsetprefix (LGL *, const char*); // prefix for messages
92 FILE * lglgetout (LGL *);
93 const char * lglgetprefix (LGL *);
95 void lglsetopt (LGL *, const char *, int); // set option value
96 int lglreadopts (LGL *, FILE *); // read and set options
97 int lglgetopt (LGL *, const char *); // get option value
98 int lglhasopt (LGL *, const char *); // exists option?
100 int lglgetoptminmax (LGL *, const char *, int * minptr, int * maxptr);
102 void * lglfirstopt (LGL *); // option iterator: first
104 void * lglnextopt (LGL *, // option iterator: next
106 const char ** nameptr,
107 int *valptr, int *minptr, int *maxptr);
109 // individual ids for logging and statistics:
111 void lglsetid (LGL *, int tid, int tids);
113 // Set default phase of a literal. Any decision on this literal will always
114 // try this phase. Note, that this function does not have any effect on
115 // eliminated variables. Further equivalent variables share the same forced
116 // phase and thus if they are set to different default phases, only the last
117 // set operation will be kept.
119 void lglsetphase (LGL *, int lit);
120 void lglresetphase (LGL *, int lit); // Stop forcing phase in decisions.
122 // Assume the solver is in the SATISFIABLE state (after 'lglsat' or
123 // 'lglsimp'), then calling 'lglsetphases' will copy the current assignment
124 // as default phases.
126 void lglsetphases (LGL *);
128 //--------------------------------------------------------------------------
129 // call back for abort
131 void lglonabort (LGL *, void * state, void (*callback)(void* state));
133 //--------------------------------------------------------------------------
134 // write and read API trace
136 void lglwtrapi (LGL *, FILE *);
137 void lglrtrapi (LGL *, FILE *);
139 //--------------------------------------------------------------------------
140 // traverse units, equivalences, remaining clauses, or all clauses:
142 void lglutrav (LGL *, void * state, void (*trav)(void *, int unit));
143 void lgletrav (LGL *, void * state, void (*trav)(void *, int lit, int repr));
144 void lglctrav (LGL *, void * state, void (*trav)(void *, int lit));
145 void lgltravall (LGL *, void * state, void (*trav)(void *state, int lit));
147 //--------------------------------------------------------------------------
149 void lglprint (LGL *, FILE *); // remaining in DIMACS format
150 void lglprintall (LGL *, FILE *); // including units & equivs
152 //--------------------------------------------------------------------------
153 // main interface as in PicoSAT (see 'picosat.h' for more information)
155 int lglmaxvar (LGL *);
156 int lglincvar (LGL *);
158 void lgladd (LGL *, int lit);
159 void lglassume (LGL *, int lit); // assume single units
161 void lglcassume (LGL *, int lit); // assume clause
164 void lglfixate (LGL *); // add assumptions as units
167 int lglsimp (LGL *, int iterations);
169 int lglderef (LGL *, int lit); // neg=false, pos=true
170 int lglfixed (LGL *, int lit); // ditto but toplevel
172 int lglfailed (LGL *, int lit); // ditto for assumptions
173 int lglinconsistent (LGL *); // contains empty clause?
174 int lglchanged (LGL *); // model changed
176 void lglreducecache (LGL *); // reset cache size
177 void lglflushcache (LGL *); // flush all learned clauses
179 /*------------------------------------------------------------------------*/
181 /* Return representative from equivalence class if literal is not top-level
182 * assigned nor eliminated.
184 int lglrepr (LGL *, int lit);
186 /* Set 'startptr' and 'toptr' to the 'start' and 'top' of the reconstruction
187 * stack, which is used in BCE, BVE and CCE for reconstructing a solution
188 * after eliminating variables or clauses. These pointers are only valid
189 * until the next 'lglsat/lglsimp' call.
191 void lglreconstk (LGL * lgl, int ** startptr, int ** toptr);
193 //--------------------------------------------------------------------------
194 // Multiple-Objective SAT tries to solve multiple objectives at the same
195 // time. If a target can be satisfied or falsified the user is notified via
196 // a callback function of type 'lglnotify'. The argument is an abstract
197 // state (of the user), the target literal and as last argument the value
198 // (-1 = unsatisfiable, 1 = satisfiable). If the notification callback
199 // returns 1 the 'lglmosat' procedure continues, otherwise it stops. It
200 // returns a non zero value iff only all targets have been either proved to
201 // be satisfiable or unsatisfiable. Even if 'val' given to the notification
202 // function is '1', it can not assume that the current assignment is
203 // complete, e.g. satisfies the formula.
205 typedef int (*lglnotify)(void *state, int target, int val);
207 int lglmosat (LGL *, void * state, lglnotify, int * targets);
209 //--------------------------------------------------------------------------
210 // Incremental interface provides reference counting for indices, i.e.
211 // unfrozen indices become invalid after next 'lglsat' (or 'lglsimp').
212 // This is actually a reference counter for variable indices still in use
213 // after the next 'lglsat' or 'lglsimp' call. It is actually variable based
214 // and only applies to literals in new clauses or used as assumptions,
215 // e.g. in calls to 'lgladd' and 'lglassume'.
217 // The following example is actually compilable and used for explaining
218 // all the details of this rather complicated incremental API contract:
220 /***** start of incremental example ***************************************
231 LGL * lgl = lglinit ();
233 lgladd (lgl, -14); lgladd (lgl, 2); lgladd (lgl, 0); // binary clause
234 lgladd (lgl, 14); lgladd (lgl, -1); lgladd (lgl, 0); // binary clause
235 lglassume (lgl, 1); // assume '1'
236 lglfreeze (lgl, 1); // will use '1' below
237 lglfreeze (lgl, 14); // will use '14 too
238 assert (lglfrozen (lgl, 1));
239 assert (lglfrozen (lgl, 14));
242 (void) lglderef (lgl, 1); // fine
243 (void) lglderef (lgl, 2); // fine
244 (void) lglderef (lgl, 3); // fine !
245 (void) lglderef (lgl, 14); // fine
246 assert (!lglusable (lgl, 2));
247 // lgladd (lgl, 2); // ILLEGAL
248 // lglassume (lgl, 2); // ILLEGAL
249 assert (lglusable (lgl, 15)); // '15' not used yet!
250 lgladd (lgl, -14); lgladd (lgl, 1); lgladd (lgl, 0); // binary clause
251 lgladd (lgl, 15); lgladd (lgl, 0); // fine!
252 lglmelt (lgl, 14); // '1' discarded
255 assert (lglfrozen (lgl, 1));
256 (void) lglderef (lgl, 1); // fine
257 (void) lglderef (lgl, 2); // fine
258 (void) lglderef (lgl, 3); // fine
259 (void) lglderef (lgl, 14); // fine
260 (void) lglderef (lgl, 15); // fine
261 assert (!lglusable (lgl, 2));
262 assert (!lglusable (lgl, 14));
263 // lglassume (lgl, 2); // ILLEGAL
264 // lglassume (lgl, 14); // ILLEGAL
265 lgladd (lgl, 1); // still frozen
270 assert (!lglusable (lgl, 1));
271 // lgladd(lgl, 1); // ILLEGAL
272 lglsetopt (lgl, "plain", 1); // disable BCE ...
273 lgladd (lgl, 8); lgladd (lgl, -9); lgladd (lgl, 0);
276 assert (!lglusable (lgl, 8));
277 assert (!lglusable (lgl, -9));
278 assert (lglreusable (lgl, 8));
279 assert (lglreusable (lgl, -9));
281 lgladd (lgl, -8); lgladd (lgl, 0);
282 lglsetopt (lgl, "plain", 0); // enable BCE ...
288 ****** end of incremental example ****************************************/
290 void lglfreeze (LGL *, int lit);
291 int lglfrozen (LGL *, int lit);
293 void lglmelt (LGL *, int lit);
294 void lglmeltall (LGL *); // melt all literals
296 // If a literal was not frozen at the last call to 'lglsat' (or 'lglsimp')
297 // it becomes 'unusable' after the next call even though it might not
298 // have been used as blocking literal etc. This
300 int lglusable (LGL *, int lit);
301 int lglreusable (LGL *, int lit);
302 void lglreuse (LGL *, int lit);
304 //--------------------------------------------------------------------------
305 // Returns a good look ahead literal or zero if all potential literals have
306 // been eliminated or have been used as blocking literals in blocked clause
307 // elimination. Zero is also returned if the formula is already
308 // inconsistent. The lookahead literal is made usable again, for instance
309 // if it was not frozen during a previous SAT call and thus implicitly
310 // became melted. Therefore it can be added in a unit clause.
312 int lglookahead (LGL *);
314 //--------------------------------------------------------------------------
317 void lglflushtimers (LGL *lgl); // after interrupt etc.
319 void lglstats (LGL *);
320 int64_t lglgetconfs (LGL *);
321 int64_t lglgetdecs (LGL *);
322 int64_t lglgetprops (LGL *);
323 size_t lglbytes (LGL *);
324 int lglnvars (LGL *);
325 int lglnclauses (LGL *);
326 double lglmb (LGL *);
327 double lglmaxmb (LGL *);
328 double lglsec (LGL *);
329 double lglprocesstime (void);
331 //--------------------------------------------------------------------------
332 // low-level parallel support through call backs
334 void lglseterm (LGL *, int (*term)(void*), void*);
336 void lglsetproduceunit (LGL *, void (*produce)(void*, int), void*);
337 void lglsetconsumeunits (LGL *, void (*consume)(void*,int**,int**), void*);
338 void lglsetconsumedunits (LGL *, void (*consumed)(void*,int), void*);
340 void lglsetproducecls (LGL*, void(*produce)(void*,int*,int glue),void*);
341 void lglsetconsumecls (LGL*,void(*consume)(void*,int**,int *glueptr),void*);
342 void lglsetconsumedcls (LGL *, void (*consumed)(void*,int), void*);
344 void lglsetlockeq (LGL *, int * (*lock)(void*), void *);
345 void lglsetunlockeq (LGL *, void (*unlock)(void*,int cons,int prod), void *);
347 void lglsetmsglock (LGL *, void (*lock)(void*), void (*unlock)(void*), void*);
348 void lglsetime (LGL *, double (*time)(void));