1 /****************************************************************************
2 Copyright (c) 2006 - 2015, Armin Biere, Johannes Kepler University.
3
4 Permission is hereby granted, free of charge, to any person obtaining a copy
5 of this software and associated documentation files (the "Software"), to
6 deal in the Software without restriction, including without limitation the
7 rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
8 sell copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
10
11 The above copyright notice and this permission notice shall be included in
12 all copies or substantial portions of the Software.
13
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
19 FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
20 IN THE SOFTWARE.
21 ****************************************************************************/
22
23 #include <stdlib.h>
24 #include <stdio.h>
25 #include <string.h>
26 #include <assert.h>
27 #include <limits.h>
28 #include <ctype.h>
29 #include <stdarg.h>
30 #include <stdint.h>
31
32 #include "picosat.h"
33
34 /* By default code for 'all different constraints' is disabled, since 'NADC'
35 * is defined.
36 */
37 #define NADC
38
39 /* By default we enable failed literals, since 'NFL' is undefined.
40 *
41 #define NFL
42 */
43
44 /* By default we 'detach satisfied (large) clauses', e.g. NDSC undefined.
45 *
46 #define NDSC
47 */
48
49 /* Do not use luby restart schedule instead of inner/outer.
next(void)50 *
51 #define NLUBY
52 */
53
54 /* Enabling this define, will use gnuplot to visualize how the scores evolve.
55 *
56 #define VISCORES
57 */
58 #ifdef VISCORES
59 // #define WRITEGIF /* ... to generate a video */
60 #endif
61
62 #ifdef VISCORES
63 #ifndef WRITEGIF
64 #include <unistd.h> /* for 'usleep' */
65 #endif
66 #endif
67
68 #ifdef RCODE
69 #include <R.h>
70 #endif
71
72 #define MINRESTART 100 /* minimum restart interval */
73 #define MAXRESTART 1000000 /* maximum restart interval */
74 #define RDECIDE 1000 /* interval of random decisions */
75 #define FRESTART 110 /* restart increase factor in percent */
76 #define FREDUCE 110 /* reduce increase factor in percent */
77 #define FREDADJ 121 /* reduce increase adjustment factor */
78 #define MAXCILS 10 /* maximal number of unrecycled internals */
79 #define FFLIPPED 10000 /* flipped reduce factor */
80 #define FFLIPPEDPREC 10000000/* flipped reduce factor precision */
81 #define INTERRUPTLIM 1024 /* check interrupt after that many decisions */
82
83 #ifndef TRACE
84 #define NO_BINARY_CLAUSES /* store binary clauses more compactly */
85 #endif
86
87 /* For debugging purposes you may want to define 'LOGGING', which actually
88 * can be enforced by using './configure.sh --log'.
89 */
90 #ifdef LOGGING
91 #define LOG(code) do { code; } while (0)
92 #else
93 #define LOG(code) do { } while (0)
94 #endif
95 #define NOLOG(code) do { } while (0) /* log exception */
96 #define ONLYLOG(code) do { code; } while (0) /* force logging */
97
98 #define FALSE ((Val)-1)
99 #define UNDEF ((Val)0)
100 #define TRUE ((Val)1)
101
102 #define COMPACT_TRACECHECK_TRACE_FMT 0
103 #define EXTENDED_TRACECHECK_TRACE_FMT 1
104 #define RUP_TRACE_FMT 2
105
106 #define NEWN(p,n) do { (p) = new (ps, sizeof (*(p)) * (n)); } while (0)
107 #define CLRN(p,n) do { memset ((p), 0, sizeof (*(p)) * (n)); } while (0)
108 #define CLR(p) CLRN(p,1)
109 #define DELETEN(p,n) \
110 do { delete (ps, p, sizeof (*(p)) * (n)); (p) = 0; } while (0)
111
112 #define RESIZEN(p,old_num,new_num) \
113 do { \
114 size_t old_size = sizeof (*(p)) * (old_num); \
115 size_t new_size = sizeof (*(p)) * (new_num); \
116 (p) = resize (ps, (p), old_size, new_size) ; \
117 } while (0)
118
119 #define ENLARGE(start,head,end) \
120 do { \
121 unsigned old_num = (ptrdiff_t)((end) - (start)); \
122 size_t new_num = old_num ? (2 * old_num) : 1; \
123 unsigned count = (head) - (start); \
124 assert ((start) <= (end)); \
125 RESIZEN((start),old_num,new_num); \
126 (head) = (start) + count; \
127 (end) = (start) + new_num; \
128 } while (0)
129
130 #define NOTLIT(l) (ps->lits + (1 ^ ((l) - ps->lits)))
131
132 #define LIT2IDX(l) ((ptrdiff_t)((l) - ps->lits) / 2)
133 #define LIT2IMPLS(l) (ps->impls + (ptrdiff_t)((l) - ps->lits))
134 #define LIT2INT(l) ((int)(LIT2SGN(l) * LIT2IDX(l)))
135 #define LIT2SGN(l) (((ptrdiff_t)((l) - ps->lits) & 1) ? -1 : 1)
136 #define LIT2VAR(l) (ps->vars + LIT2IDX(l))
die(const char * fmt,...)137 #define LIT2HTPS(l) (ps->htps + (ptrdiff_t)((l) - ps->lits))
138 #define LIT2JWH(l) (ps->jwh + ((l) - ps->lits))
139
140 #ifndef NDSC
141 #define LIT2DHTPS(l) (ps->dhtps + (ptrdiff_t)((l) - ps->lits))
142 #endif
143
144 #ifdef NO_BINARY_CLAUSES
145 typedef uintptr_t Wrd;
146 #define ISLITREASON(C) (1&(Wrd)C)
147 #define LIT2REASON(L) \
percent(double a,double b)148 (assert (L->val==TRUE), ((Cls*)(1 + (2*(L - ps->lits)))))
149 #define REASON2LIT(C) ((Lit*)(ps->lits + ((Wrd)C)/2))
150 #endif
151
152 #define ENDOFCLS(c) ((void*)((Lit**)(c)->lits + (c)->size))
153
154 #define SOC ((ps->oclauses == ps->ohead) ? ps->lclauses : ps->oclauses)
155 #define EOC (ps->lhead)
156 #define NXC(p) (((p) + 1 == ps->ohead) ? ps->lclauses : (p) + 1)
157
158 #define OIDX2IDX(idx) (2 * ((idx) + 1))
159 #define LIDX2IDX(idx) (2 * (idx) + 1)
160
161 #define ISLIDX(idx) ((idx)&1)
162
163 #define IDX2OIDX(idx) (assert(!ISLIDX(idx)), (idx)/2 - 1)
164 #define IDX2LIDX(idx) (assert(ISLIDX(idx)), (idx)/2)
165
166 #define EXPORTIDX(idx) \
167 ((ISLIDX(idx) ? (IDX2LIDX (idx) + (ps->ohead - ps->oclauses)) : IDX2OIDX(idx)) + 1)
168
169 #define IDX2CLS(i) \
170 (assert(i), (ISLIDX(i) ? ps->lclauses : ps->oclauses)[(i)/2 - !ISLIDX(i)])
171
172 #define IDX2ZHN(i) (assert(i), (ISLIDX(i) ? ps->zhains[(i)/2] : 0))
173
174 #define CLS2TRD(c) (((Trd*)(c)) - 1)
175 #define CLS2IDX(c) ((((Trd*)(c)) - 1)->idx)
176
177 #define CLS2ACT(c) \
178 ((Act*)((assert((c)->learned)),assert((c)->size>2),ENDOFCLS(c)))
179
180 #define VAR2LIT(v) (ps->lits + 2 * ((v) - ps->vars))
181 #define VAR2RNK(v) (ps->rnks + ((v) - ps->vars))
182
183 #define RNK2LIT(r) (ps->lits + 2 * ((r) - ps->rnks))
184 #define RNK2VAR(r) (ps->vars + ((r) - ps->rnks))
185
186 #define BLK_FILL_BYTES 8
187 #define SIZE_OF_BLK (sizeof (Blk) - BLK_FILL_BYTES)
188
189 #define PTR2BLK(void_ptr) \
190 ((void_ptr) ? (Blk*)(((char*)(void_ptr)) - SIZE_OF_BLK) : 0)
191
192 #define AVERAGE(a,b) ((b) ? (((double)a) / (double)(b)) : 0.0)
193 #define PERCENT(a,b) (100.0 * AVERAGE(a,b))
194
195 #ifndef RCODE
196 #define ABORT(msg) \
197 do { \
198 fputs ("*** picosat: " msg "\n", stderr); \
199 abort (); \
200 } while (0)
201 #else
202 #define ABORT(msg) \
203 do { \
204 Rf_error (msg); \
205 } while (0)
main(int argc,char ** argv)206 #endif
207
208 #define ABORTIF(cond,msg) \
209 do { \
210 if (!(cond)) break; \
211 ABORT (msg); \
212 } while (0)
213
214 #define ZEROFLT (0x00000000u)
215 #define EPSFLT (0x00000001u)
216 #define INFFLT (0xffffffffu)
217
218 #define FLTCARRY (1u << 25)
219 #define FLTMSB (1u << 24)
220 #define FLTMAXMANTISSA (FLTMSB - 1)
221
222 #define FLTMANTISSA(d) ((d) & FLTMAXMANTISSA)
223 #define FLTEXPONENT(d) ((int)((d) >> 24) - 128)
224
225 #define FLTMINEXPONENT (-128)
226 #define FLTMAXEXPONENT (127)
227
228 #define CMPSWAPFLT(a,b) \
229 do { \
230 Flt tmp; \
231 if (((a) < (b))) \
232 { \
233 tmp = (a); \
234 (a) = (b); \
235 (b) = tmp; \
236 } \
237 } while (0)
238
239 #define UNPACKFLT(u,m,e) \
240 do { \
241 (m) = FLTMANTISSA(u); \
242 (e) = FLTEXPONENT(u); \
243 (m) |= FLTMSB; \
244 } while (0)
245
246 #define INSERTION_SORT_LIMIT 10
247
248 #define SORTING_SWAP(T,p,q) \
249 do { \
250 T tmp = *(q); \
251 *(q) = *(p); \
252 *(p) = tmp; \
253 } while (0)
254
255 #define SORTING_CMP_SWAP(T,cmp,p,q) \
256 do { \
257 if ((cmp) (ps, *(p), *(q)) > 0) \
258 SORTING_SWAP (T, p, q); \
259 } while(0)
260
261 #define QUICKSORT_PARTITION(T,cmp,a,l,r) \
262 do { \
263 T pivot; \
264 int j; \
265 i = (l) - 1; /* result in 'i' */ \
266 j = (r); \
267 pivot = (a)[j]; \
268 for (;;) \
269 { \
270 while ((cmp) (ps, (a)[++i], pivot) < 0) \
271 ; \
272 while ((cmp) (ps, pivot, (a)[--j]) < 0) \
273 if (j == (l)) \
274 break; \
275 if (i >= j) \
276 break; \
277 SORTING_SWAP (T, (a) + i, (a) + j); \
278 } \
279 SORTING_SWAP (T, (a) + i, (a) + (r)); \
280 } while(0)
281
282 #define QUICKSORT(T,cmp,a,n) \
283 do { \
284 int l = 0, r = (n) - 1, m, ll, rr, i; \
285 assert (ps->ihead == ps->indices); \
286 if (r - l <= INSERTION_SORT_LIMIT) \
287 break; \
288 for (;;) \
289 { \
290 m = (l + r) / 2; \
291 SORTING_SWAP (T, (a) + m, (a) + r - 1); \
292 SORTING_CMP_SWAP (T, cmp, (a) + l, (a) + r - 1); \
293 SORTING_CMP_SWAP (T, cmp, (a) + l, (a) + r); \
294 SORTING_CMP_SWAP (T, cmp, (a) + r - 1, (a) + r); \
295 QUICKSORT_PARTITION (T, cmp, (a), l + 1, r - 1); \
296 if (i - l < r - i) \
297 { \
298 ll = i + 1; \
299 rr = r; \
300 r = i - 1; \
301 } \
302 else \
303 { \
304 ll = l; \
305 rr = i - 1; \
306 l = i + 1; \
307 } \
308 if (r - l > INSERTION_SORT_LIMIT) \
309 { \
310 assert (rr - ll > INSERTION_SORT_LIMIT); \
311 if (ps->ihead == ps->eoi) \
312 ENLARGE (ps->indices, ps->ihead, ps->eoi); \
313 *ps->ihead++ = ll; \
314 if (ps->ihead == ps->eoi) \
315 ENLARGE (ps->indices, ps->ihead, ps->eoi); \
316 *ps->ihead++ = rr; \
317 } \
318 else if (rr - ll > INSERTION_SORT_LIMIT) \
319 { \
320 l = ll; \
321 r = rr; \
322 } \
323 else if (ps->ihead > ps->indices) \
324 { \
325 r = *--ps->ihead; \
326 l = *--ps->ihead; \
327 } \
328 else \
329 break; \
330 } \
331 } while (0)
332
333 #define INSERTION_SORT(T,cmp,a,n) \
334 do { \
335 T pivot; \
336 int l = 0, r = (n) - 1, i, j; \
337 for (i = r; i > l; i--) \
338 SORTING_CMP_SWAP (T, cmp, (a) + i - 1, (a) + i); \
339 for (i = l + 2; i <= r; i++) \
340 { \
341 j = i; \
342 pivot = (a)[i]; \
343 while ((cmp) (ps, pivot, (a)[j - 1]) < 0) \
344 { \
345 (a)[j] = (a)[j - 1]; \
346 j--; \
347 } \
348 (a)[j] = pivot; \
349 } \
350 } while (0)
351
352 #ifdef NDEBUG
353 #define CHECK_SORTED(cmp,a,n) do { } while(0)
354 #else
355 #define CHECK_SORTED(cmp,a,n) \
356 do { \
357 int i; \
358 for (i = 0; i < (n) - 1; i++) \
359 assert ((cmp) (ps, (a)[i], (a)[i + 1]) <= 0); \
360 } while(0)
361 #endif
362
363 #define SORT(T,cmp,a,n) \
364 do { \
365 T * aa = (a); \
366 int nn = (n); \
367 QUICKSORT (T, cmp, aa, nn); \
368 INSERTION_SORT (T, cmp, aa, nn); \
369 assert (ps->ihead == ps->indices); \
370 CHECK_SORTED (cmp, aa, nn); \
371 } while (0)
372
373 #define WRDSZ (sizeof (long) * 8)
374
375 #ifdef RCODE
376 #define fprintf(...) do { } while (0)
377 #define vfprintf(...) do { } while (0)
378 #define fputs(...) do { } while (0)
379 #define fputc(...) do { } while (0)
380 #endif
381
382 typedef unsigned Flt; /* 32 bit deterministic soft float */
383 typedef Flt Act; /* clause and variable activity */
384 typedef struct Blk Blk; /* allocated memory block */
385 typedef struct Cls Cls; /* clause */
386 typedef struct Lit Lit; /* literal */
387 typedef struct Rnk Rnk; /* variable to score mapping */
388 typedef signed char Val; /* TRUE, UNDEF, FALSE */
389 typedef struct Var Var; /* variable */
390 #ifdef TRACE
391 typedef struct Trd Trd; /* trace data for clauses */
392 typedef struct Zhn Zhn; /* compressed chain (=zain) data */
393 typedef unsigned char Znt; /* compressed antecedent data */
394 #endif
395
396 #ifdef NO_BINARY_CLAUSES
397 typedef struct Ltk Ltk;
398
399 struct Ltk
400 {
401 Lit ** start;
402 unsigned count : WRDSZ == 32 ? 27 : 32;
403 unsigned ldsize : WRDSZ == 32 ? 5 : 32;
404 };
405 #endif
406
407 struct Lit
408 {
409 Val val;
410 };
411
412 struct Var
413 {
414 unsigned mark : 1; /*bit 1*/
415 unsigned resolved : 1; /*bit 2*/
416 unsigned phase : 1; /*bit 3*/
417 unsigned assigned : 1; /*bit 4*/
418 unsigned used : 1; /*bit 5*/
419 unsigned failed : 1; /*bit 6*/
420 unsigned internal : 1; /*bit 7*/
421 unsigned usedefphase : 1; /*bit 8*/
422 unsigned defphase : 1; /*bit 9*/
423 unsigned msspos : 1; /*bit 10*/
424 unsigned mssneg : 1; /*bit 11*/
425 unsigned humuspos : 1; /*bit 12*/
426 unsigned humusneg : 1; /*bit 13*/
427 unsigned partial : 1; /*bit 14*/
428 #ifdef TRACE
429 unsigned core : 1; /*bit 15*/
430 #endif
431 unsigned level;
432 Cls *reason;
433 #ifndef NADC
434 Lit ** inado;
435 Lit ** ado;
436 Lit *** adotabpos;
437 #endif
438 };
439
440 struct Rnk
441 {
442 Act score;
443 unsigned pos : 30; /* 0 iff not on heap */
444 unsigned moreimportant : 1;
445 unsigned lessimportant : 1;
446 };
447
448 struct Cls
449 {
450 unsigned size;
451
452 unsigned collect:1; /* bit 1 */
453 unsigned learned:1; /* bit 2 */
454 unsigned locked:1; /* bit 3 */
455 unsigned used:1; /* bit 4 */
456 #ifndef NDEBUG
457 unsigned connected:1; /* bit 5 */
458 #endif
459 #ifdef TRACE
460 unsigned collected:1; /* bit 6 */
461 unsigned core:1; /* bit 7 */
462 #endif
463
464 #define LDMAXGLUE 25 /* 32 - 7 */
465 #define MAXGLUE ((1<<LDMAXGLUE)-1)
466
467 unsigned glue:LDMAXGLUE;
468
469 Cls *next[2];
470 Lit *lits[2];
471 };
472
473 #ifdef TRACE
474 struct Zhn
475 {
476 unsigned ref:31;
477 unsigned core:1;
478 Znt * liz;
479 Znt znt[0];
480 };
481
482 struct Trd
483 {
484 unsigned idx;
485 Cls cls[0];
486 };
487 #endif
488
489 struct Blk
490 {
491 #ifndef NDEBUG
492 union
493 {
494 size_t size; /* this is what we really use */
495 void *as_two_ptrs[2]; /* 2 * sizeof (void*) alignment of data */
496 }
497 header;
498 #endif
499 char data[BLK_FILL_BYTES];
500 };
501
502 enum State
503 {
504 RESET = 0,
505 READY = 1,
506 SAT = 2,
507 UNSAT = 3,
508 UNKNOWN = 4,
509 };
510
511 enum Phase
512 {
513 POSPHASE,
514 NEGPHASE,
515 JWLPHASE,
516 RNDPHASE,
517 };
518
519 struct PicoSAT
520 {
521 enum State state;
522 enum Phase defaultphase;
523 int last_sat_call_result;
524
525 FILE *out;
526 char * prefix;
527 int verbosity;
528 int plain;
529 unsigned LEVEL;
530 unsigned max_var;
531 unsigned size_vars;
532
533 Lit *lits;
534 Var *vars;
535 Rnk *rnks;
536 Flt *jwh;
537 Cls **htps;
538 #ifndef NDSC
539 Cls **dhtps;
540 #endif
541 #ifdef NO_BINARY_CLAUSES
542 Ltk *impls;
543 Cls impl, cimpl;
544 int implvalid, cimplvalid;
545 #else
546 Cls **impls;
547 #endif
548 Lit **trail, **thead, **eot, **ttail, ** ttail2;
549 #ifndef NADC
550 Lit **ttailado;
551 #endif
552 unsigned adecidelevel;
553 Lit **als, **alshead, **alstail, **eoals;
554 Lit **CLS, **clshead, **eocls;
555 int *rils, *rilshead, *eorils;
556 int *cils, *cilshead, *eocils;
557 int *fals, *falshead, *eofals;
558 int *mass, szmass;
559 int *mssass, szmssass;
560 int *mcsass, nmcsass, szmcsass;
561 int *humus, szhumus;
562 Lit *failed_assumption;
563 int extracted_all_failed_assumptions;
564 Rnk **heap, **hhead, **eoh;
565 Cls **oclauses, **ohead, **eoo; /* original clauses */
566 Cls **lclauses, **lhead, ** EOL; /* learned clauses */
567 int * soclauses, * sohead, * eoso; /* saved original clauses */
568 int saveorig;
569 int partial;
570 #ifdef TRACE
571 int trace;
572 Zhn **zhains, **zhead, **eoz;
573 int ocore;
574 #endif
575 FILE * rup;
576 int rupstarted;
577 int rupvariables;
578 int rupclauses;
579 Cls *mtcls;
580 Cls *conflict;
581 Lit **added, **ahead, **eoa;
582 Var **marked, **mhead, **eom;
583 Var **dfs, **dhead, **eod;
584 Cls **resolved, **rhead, **eor;
585 unsigned char *levels, *levelshead, *eolevels;
586 unsigned *dused, *dusedhead, *eodused;
587 unsigned char *buffer, *bhead, *eob;
588 Act vinc, lscore, ilvinc, ifvinc;
589 #ifdef VISCORES
590 Act fvinc, nvinc;
591 #endif
592 Act cinc, lcinc, ilcinc, fcinc;
593 unsigned srng;
594 size_t current_bytes;
595 size_t max_bytes;
596 size_t recycled;
597 double seconds, flseconds;
598 double entered;
599 unsigned nentered;
600 int measurealltimeinlib;
601 char *rline[2];
602 int szrline, RCOUNT;
603 double levelsum;
604 unsigned iterations;
605 int reports;
606 int lastrheader;
607 unsigned calls;
608 unsigned decisions;
609 unsigned restarts;
610 unsigned simps;
611 unsigned fsimplify;
612 unsigned isimplify;
613 unsigned reductions;
614 unsigned lreduce;
615 unsigned lreduceadjustcnt;
616 unsigned lreduceadjustinc;
617 unsigned lastreduceconflicts;
618 unsigned llocked; /* locked large learned clauses */
619 unsigned lrestart;
620 #ifdef NLUBY
621 unsigned drestart;
622 unsigned ddrestart;
623 #else
624 unsigned lubycnt;
625 unsigned lubymaxdelta;
626 int waslubymaxdelta;
627 #endif
628 unsigned long long lsimplify;
629 unsigned long long propagations;
630 unsigned long long lpropagations;
631 unsigned fixed; /* top level assignments */
632 #ifndef NFL
633 unsigned failedlits;
634 unsigned ifailedlits;
635 unsigned efailedlits;
636 unsigned flcalls;
637 #ifdef STATS
638 unsigned flrounds;
639 unsigned long long flprops;
640 unsigned long long floopsed, fltried, flskipped;
641 #endif
642 unsigned long long fllimit;
643 int simplifying;
644 Lit ** saved;
645 unsigned saved_size;
646 #endif
647 unsigned conflicts;
648 unsigned contexts;
649 unsigned internals;
650 unsigned noclauses; /* current number large original clauses */
651 unsigned nlclauses; /* current number large learned clauses */
652 unsigned olits; /* current literals in large original clauses */
653 unsigned llits; /* current literals in large learned clauses */
654 unsigned oadded; /* added original clauses */
655 unsigned ladded; /* added learned clauses */
656 unsigned loadded; /* added original large clauses */
657 unsigned lladded; /* added learned large clauses */
658 unsigned addedclauses; /* oadded + ladded */
659 unsigned vused; /* used variables */
660 unsigned llitsadded; /* added learned literals */
661 unsigned long long visits;
662 #ifdef STATS
663 unsigned loused; /* used large original clauses */
664 unsigned llused; /* used large learned clauses */
665 unsigned long long bvisits;
666 unsigned long long tvisits;
667 unsigned long long lvisits;
668 unsigned long long othertrue;
669 unsigned long long othertrue2;
670 unsigned long long othertruel;
671 unsigned long long othertrue2u;
672 unsigned long long othertruelu;
673 unsigned long long ltraversals;
674 unsigned long long traversals;
675 #ifdef TRACE
676 unsigned long long antecedents;
677 #endif
678 unsigned uips;
679 unsigned znts;
680 unsigned assumptions;
681 unsigned rdecisions;
682 unsigned sdecisions;
683 size_t srecycled;
684 size_t rrecycled;
685 unsigned long long derefs;
686 #endif
687 unsigned minimizedllits;
688 unsigned nonminimizedllits;
689 #ifndef NADC
690 Lit *** ados, *** hados, *** eados;
691 Lit *** adotab;
692 unsigned nadotab;
693 unsigned szadotab;
694 Cls * adoconflict;
695 unsigned adoconflicts;
696 unsigned adoconflictlimit;
697 int addingtoado;
698 int adodisabled;
699 #endif
700 unsigned long long flips;
701 #ifdef STATS
702 unsigned long long FORCED;
703 unsigned long long assignments;
704 unsigned inclreduces;
705 unsigned staticphasedecisions;
706 unsigned skippedrestarts;
707 #endif
708 int * indices, * ihead, *eoi;
709 unsigned sdflips;
710
711 unsigned long long saved_flips;
712 unsigned saved_max_var;
713 unsigned min_flipped;
714
715 void * emgr;
716 picosat_malloc enew;
717 picosat_realloc eresize;
718 picosat_free edelete;
719
720 struct {
721 void * state;
722 int (*function) (void *);
723 } interrupt;
724
725 #ifdef VISCORES
726 FILE * fviscores;
727 #endif
728 };
729
730 typedef PicoSAT PS;
731
732 static Flt
733 packflt (unsigned m, int e)
734 {
735 Flt res;
736 assert (m < FLTMSB);
737 assert (FLTMINEXPONENT <= e);
738 assert (e <= FLTMAXEXPONENT);
739 res = m | ((unsigned)(e + 128) << 24);
740 return res;
741 }
742
743 static Flt
744 base2flt (unsigned m, int e)
745 {
746 if (!m)
747 return ZEROFLT;
748
749 if (m < FLTMSB)
750 {
751 do
752 {
753 if (e <= FLTMINEXPONENT)
754 return EPSFLT;
755
756 e--;
757 m <<= 1;
758
759 }
760 while (m < FLTMSB);
761 }
762 else
763 {
764 while (m >= FLTCARRY)
765 {
766 if (e >= FLTMAXEXPONENT)
767 return INFFLT;
768
769 e++;
770 m >>= 1;
771 }
772 }
773
774 m &= ~FLTMSB;
775 return packflt (m, e);
776 }
777
778 static Flt
779 addflt (Flt a, Flt b)
780 {
781 unsigned ma, mb, delta;
782 int ea, eb;
783
784 CMPSWAPFLT (a, b);
785 if (!b)
786 return a;
787
788 UNPACKFLT (a, ma, ea);
789 UNPACKFLT (b, mb, eb);
790
791 assert (ea >= eb);
792 delta = ea - eb;
793 if (delta < 32) mb >>= delta; else mb = 0;
794 if (!mb)
795 return a;
796
797 ma += mb;
798 if (ma & FLTCARRY)
799 {
800 if (ea == FLTMAXEXPONENT)
801 return INFFLT;
802
803 ea++;
804 ma >>= 1;
805 }
806
807 assert (ma < FLTCARRY);
808 ma &= FLTMAXMANTISSA;
809
810 return packflt (ma, ea);
811 }
812
813 static Flt
814 mulflt (Flt a, Flt b)
815 {
816 unsigned ma, mb;
817 unsigned long long accu;
818 int ea, eb;
819
820 CMPSWAPFLT (a, b);
821 if (!b)
822 return ZEROFLT;
823
824 UNPACKFLT (a, ma, ea);
825 UNPACKFLT (b, mb, eb);
826
827 ea += eb;
828 ea += 24;
829 if (ea > FLTMAXEXPONENT)
830 return INFFLT;
831
832 if (ea < FLTMINEXPONENT)
833 return EPSFLT;
834
835 accu = ma;
836 accu *= mb;
837 accu >>= 24;
838
839 if (accu >= FLTCARRY)
840 {
841 if (ea == FLTMAXEXPONENT)
842 return INFFLT;
843
844 ea++;
845 accu >>= 1;
846
847 if (accu >= FLTCARRY)
848 return INFFLT;
849 }
850
851 assert (accu < FLTCARRY);
852 assert (accu & FLTMSB);
853
854 ma = accu;
855 ma &= ~FLTMSB;
856
857 return packflt (ma, ea);
858 }
859
860 static Flt
861 ascii2flt (const char *str)
862 {
863 Flt ten = base2flt (10, 0);
864 Flt onetenth = base2flt (26843546, -28);
865 Flt res = ZEROFLT, tmp, base;
866 const char *p = str;
867 int ch;
868
869 ch = *p++;
870
871 if (ch != '.')
872 {
873 if (!isdigit (ch))
874 return INFFLT; /* better abort ? */
875
876 res = base2flt (ch - '0', 0);
877
878 while ((ch = *p++))
879 {
880 if (ch == '.')
881 break;
882
883 if (!isdigit (ch))
884 return INFFLT; /* better abort? */
885
886 res = mulflt (res, ten);
887 tmp = base2flt (ch - '0', 0);
888 res = addflt (res, tmp);
889 }
890 }
891
892 if (ch == '.')
893 {
894 ch = *p++;
895 if (!isdigit (ch))
896 return INFFLT; /* better abort ? */
897
898 base = onetenth;
899 tmp = mulflt (base2flt (ch - '0', 0), base);
900 res = addflt (res, tmp);
901
902 while ((ch = *p++))
903 {
904 if (!isdigit (ch))
905 return INFFLT; /* better abort? */
906
907 base = mulflt (base, onetenth);
908 tmp = mulflt (base2flt (ch - '0', 0), base);
909 res = addflt (res, tmp);
910 }
911 }
912
913 return res;
914 }
915
916 #if defined(VISCORES)
917
918 static double
919 flt2double (Flt f)
920 {
921 double res;
922 unsigned m;
923 int e, i;
924
925 UNPACKFLT (f, m, e);
926 res = m;
927
928 if (e < 0)
929 {
930 for (i = e; i < 0; i++)
931 res *= 0.5;
932 }
933 else
934 {
935 for (i = 0; i < e; i++)
936 res *= 2.0;
937 }
938
939 return res;
940 }
941
942 #endif
943
944 static int
945 log2flt (Flt a)
946 {
947 return FLTEXPONENT (a) + 24;
948 }
949
950 static int
951 cmpflt (Flt a, Flt b)
952 {
953 if (a < b)
954 return -1;
955
956 if (a > b)
957 return 1;
958
959 return 0;
960 }
961
962 static void *
963 new (PS * ps, size_t size)
964 {
965 size_t bytes;
966 Blk *b;
967
968 if (!size)
969 return 0;
970
971 bytes = size + SIZE_OF_BLK;
972
973 if (ps->enew)
974 b = ps->enew (ps->emgr, bytes);
975 else
976 b = malloc (bytes);
977
978 ABORTIF (!b, "out of memory in 'new'");
979 #ifndef NDEBUG
980 b->header.size = size;
981 #endif
982 ps->current_bytes += size;
983 if (ps->current_bytes > ps->max_bytes)
984 ps->max_bytes = ps->current_bytes;
985 return b->data;
986 }
987
988 static void
989 delete (PS * ps, void *void_ptr, size_t size)
990 {
991 size_t bytes;
992 Blk *b;
993
994 if (!void_ptr)
995 {
996 assert (!size);
997 return;
998 }
999
1000 assert (size);
1001 b = PTR2BLK (void_ptr);
1002
1003 assert (size <= ps->current_bytes);
1004 ps->current_bytes -= size;
1005
1006 assert (b->header.size == size);
1007
1008 bytes = size + SIZE_OF_BLK;
1009 if (ps->edelete)
1010 ps->edelete (ps->emgr, b, bytes);
1011 else
1012 free (b);
1013 }
1014
1015 static void *
1016 resize (PS * ps, void *void_ptr, size_t old_size, size_t new_size)
1017 {
1018 size_t old_bytes, new_bytes;
1019 Blk *b;
1020
1021 b = PTR2BLK (void_ptr);
1022
1023 assert (old_size <= ps->current_bytes);
1024 ps->current_bytes -= old_size;
1025
1026 if ((old_bytes = old_size))
1027 {
1028 assert (old_size && b && b->header.size == old_size);
1029 old_bytes += SIZE_OF_BLK;
1030 }
1031 else
1032 assert (!b);
1033
1034 if ((new_bytes = new_size))
1035 new_bytes += SIZE_OF_BLK;
1036
1037 if (ps->eresize)
1038 b = ps->eresize (ps->emgr, b, old_bytes, new_bytes);
1039 else
1040 b = realloc (b, new_bytes);
1041
1042 if (!new_size)
1043 {
1044 assert (!b);
1045 return 0;
1046 }
1047
1048 ABORTIF (!b, "out of memory in 'resize'");
1049 #ifndef NDEBUG
1050 b->header.size = new_size;
1051 #endif
1052
1053 ps->current_bytes += new_size;
1054 if (ps->current_bytes > ps->max_bytes)
1055 ps->max_bytes = ps->current_bytes;
1056
1057 return b->data;
1058 }
1059
1060 static unsigned
1061 int2unsigned (int l)
1062 {
1063 return (l < 0) ? 1 + 2 * -l : 2 * l;
1064 }
1065
1066 static Lit *
1067 int2lit (PS * ps, int l)
1068 {
1069 return ps->lits + int2unsigned (l);
1070 }
1071
1072 static Lit **
1073 end_of_lits (Cls * c)
1074 {
1075 return (Lit**)c->lits + c->size;
1076 }
1077
1078 #if !defined(NDEBUG) || defined(LOGGING)
1079
1080 static void
1081 dumplits (PS * ps, Lit ** l, Lit ** end)
1082 {
1083 int first;
1084 Lit ** p;
1085
1086 if (l == end)
1087 {
1088 /* empty clause */
1089 }
1090 else if (l + 1 == end)
1091 {
1092 fprintf (ps->out, "%d ", LIT2INT (l[0]));
1093 }
1094 else
1095 {
1096 assert (l + 2 <= end);
1097 first = (abs (LIT2INT (l[0])) > abs (LIT2INT (l[1])));
1098 fprintf (ps->out, "%d ", LIT2INT (l[first]));
1099 fprintf (ps->out, "%d ", LIT2INT (l[!first]));
1100 for (p = l + 2; p < end; p++)
1101 fprintf (ps->out, "%d ", LIT2INT (*p));
1102 }
1103
1104 fputc ('0', ps->out);
1105 }
1106
1107 static void
1108 dumpcls (PS * ps, Cls * c)
1109 {
1110 Lit **end;
1111
1112 if (c)
1113 {
1114 end = end_of_lits (c);
1115 dumplits (ps, c->lits, end);
1116 #ifdef TRACE
1117 if (ps->trace)
1118 fprintf (ps->out, " clause(%u)", CLS2IDX (c));
1119 #endif
1120 }
1121 else
1122 fputs ("DECISION", ps->out);
1123 }
1124
1125 static void
1126 dumpclsnl (PS * ps, Cls * c)
1127 {
1128 dumpcls (ps, c);
1129 fputc ('\n', ps->out);
1130 }
1131
1132 void
1133 dumpcnf (PS * ps)
1134 {
1135 Cls **p, *c;
1136
1137 for (p = SOC; p != EOC; p = NXC (p))
1138 {
1139 c = *p;
1140
1141 if (!c)
1142 continue;
1143
1144 #ifdef TRACE
1145 if (c->collected)
1146 continue;
1147 #endif
1148
1149 dumpclsnl (ps, *p);
1150 }
1151 }
1152
1153 #endif
1154
1155 static void
1156 delete_prefix (PS * ps)
1157 {
1158 if (!ps->prefix)
1159 return;
1160
1161 delete (ps, ps->prefix, strlen (ps->prefix) + 1);
1162 ps->prefix = 0;
1163 }
1164
1165 static void
1166 new_prefix (PS * ps, const char * str)
1167 {
1168 delete_prefix (ps);
1169 assert (str);
1170 ps->prefix = new (ps, strlen (str) + 1);
1171 strcpy (ps->prefix, str);
1172 }
1173
1174 static PS *
1175 init (void * pmgr,
1176 picosat_malloc pnew, picosat_realloc presize, picosat_free pdelete)
1177 {
1178 PS * ps;
1179
1180 #if 0
1181 int count = 3 - !pnew - !presize - !pdelete;
1182
1183 ABORTIF (count && !pnew, "API usage: missing 'picosat_set_new'");
1184 ABORTIF (count && !presize, "API usage: missing 'picosat_set_resize'");
1185 ABORTIF (count && !pdelete, "API usage: missing 'picosat_set_delete'");
1186 #endif
1187
1188 ps = pnew ? pnew (pmgr, sizeof *ps) : malloc (sizeof *ps);
1189 ABORTIF (!ps, "failed to allocate memory for PicoSAT manager");
1190 memset (ps, 0, sizeof *ps);
1191
1192 ps->emgr = pmgr;
1193 ps->enew = pnew;
1194 ps->eresize = presize;
1195 ps->edelete = pdelete;
1196
1197 ps->size_vars = 1;
1198 ps->state = RESET;
1199 ps->defaultphase = JWLPHASE;
1200 #ifdef TRACE
1201 ps->ocore = -1;
1202 #endif
1203 ps->lastrheader = -2;
1204 #ifndef NADC
1205 ps->adoconflictlimit = UINT_MAX;
1206 #endif
1207 ps->min_flipped = UINT_MAX;
1208
1209 NEWN (ps->lits, 2 * ps->size_vars);
1210 NEWN (ps->jwh, 2 * ps->size_vars);
1211 NEWN (ps->htps, 2 * ps->size_vars);
1212 #ifndef NDSC
1213 NEWN (ps->dhtps, 2 * ps->size_vars);
1214 #endif
1215 NEWN (ps->impls, 2 * ps->size_vars);
1216 NEWN (ps->vars, ps->size_vars);
1217 NEWN (ps->rnks, ps->size_vars);
1218
1219 /* because '0' pos denotes not on heap
1220 */
1221 ENLARGE (ps->heap, ps->hhead, ps->eoh);
1222 ps->hhead = ps->heap + 1;
1223
1224 ps->vinc = base2flt (1, 0); /* initial var activity */
1225 ps->ifvinc = ascii2flt ("1.05"); /* var score rescore factor */
1226 #ifdef VISCORES
1227 ps->fvinc = ascii2flt ("0.9523809"); /* 1/f = 1/1.05 */
1228 ps->nvinc = ascii2flt ("0.0476191"); /* 1 - 1/f = 1 - 1/1.05 */
1229 #endif
1230 ps->lscore = base2flt (1, 90); /* var activity rescore limit */
1231 ps->ilvinc = base2flt (1, -90); /* inverse of 'lscore' */
1232
1233 ps->cinc = base2flt (1, 0); /* initial clause activity */
1234 ps->fcinc = ascii2flt ("1.001"); /* cls activity rescore factor */
1235 ps->lcinc = base2flt (1, 90); /* cls activity rescore limit */
1236 ps->ilcinc = base2flt (1, -90); /* inverse of 'ilcinc' */
1237
1238 ps->lreduceadjustcnt = ps->lreduceadjustinc = 100;
1239 ps->lpropagations = ~0ull;
1240
1241 #ifndef RCODE
1242 ps->out = stdout;
1243 #else
1244 ps->out = 0;
1245 #endif
1246 new_prefix (ps, "c ");
1247 ps->verbosity = 0;
1248 ps->plain = 0;
1249
1250 #ifdef NO_BINARY_CLAUSES
1251 memset (&ps->impl, 0, sizeof (ps->impl));
1252 ps->impl.size = 2;
1253
1254 memset (&ps->cimpl, 0, sizeof (ps->impl));
1255 ps->cimpl.size = 2;
1256 #endif
1257
1258 #ifdef VISCORES
1259 ps->fviscores = popen (
1260 "/usr/bin/gnuplot -background black"
1261 " -xrm 'gnuplot*textColor:white'"
1262 " -xrm 'gnuplot*borderColor:white'"
1263 " -xrm 'gnuplot*axisColor:white'"
1264 , "w");
1265 fprintf (ps->fviscores, "unset key\n");
1266 // fprintf (ps->fviscores, "set log y\n");
1267 fflush (ps->fviscores);
1268 system ("rm -rf /tmp/picosat-viscores");
1269 system ("mkdir /tmp/picosat-viscores");
1270 system ("mkdir /tmp/picosat-viscores/data");
1271 #ifdef WRITEGIF
1272 system ("mkdir /tmp/picosat-viscores/gif");
1273 fprintf (ps->fviscores,
1274 "set terminal gif giant animate opt size 1024,768 x000000 xffffff"
1275 "\n");
1276
1277 fprintf (ps->fviscores,
1278 "set output \"/tmp/picosat-viscores/gif/animated.gif\"\n");
1279 #endif
1280 #endif
1281 ps->defaultphase = JWLPHASE;
1282 ps->state = READY;
1283 ps->last_sat_call_result = 0;
1284
1285 return ps;
1286 }
1287
1288 static size_t
1289 bytes_clause (PS * ps, unsigned size, unsigned learned)
1290 {
1291 size_t res;
1292
1293 res = sizeof (Cls);
1294 res += size * sizeof (Lit *);
1295 res -= 2 * sizeof (Lit *);
1296
1297 if (learned && size > 2)
1298 res += sizeof (Act); /* add activity */
1299
1300 #ifdef TRACE
1301 if (ps->trace)
1302 res += sizeof (Trd); /* add trace data */
1303 #else
1304 (void) ps;
1305 #endif
1306
1307 return res;
1308 }
1309
1310 static Cls *
1311 new_clause (PS * ps, unsigned size, unsigned learned)
1312 {
1313 size_t bytes;
1314 void * tmp;
1315 #ifdef TRACE
1316 Trd *trd;
1317 #endif
1318 Cls *res;
1319
1320 bytes = bytes_clause (ps, size, learned);
1321 tmp = new (ps, bytes);
1322
1323 #ifdef TRACE
1324 if (ps->trace)
1325 {
1326 trd = tmp;
1327
1328 if (learned)
1329 trd->idx = LIDX2IDX (ps->lhead - ps->lclauses);
1330 else
1331 trd->idx = OIDX2IDX (ps->ohead - ps->oclauses);
1332
1333 res = trd->cls;
1334 }
1335 else
1336 #endif
1337 res = tmp;
1338
1339 res->size = size;
1340 res->learned = learned;
1341
1342 res->collect = 0;
1343 #ifndef NDEBUG
1344 res->connected = 0;
1345 #endif
1346 res->locked = 0;
1347 res->used = 0;
1348 #ifdef TRACE
1349 res->core = 0;
1350 res->collected = 0;
1351 #endif
1352
1353 if (learned && size > 2)
1354 {
1355 Act * p = CLS2ACT (res);
1356 *p = ps->cinc;
1357 }
1358
1359 return res;
1360 }
1361
1362 static void
1363 delete_clause (PS * ps, Cls * c)
1364 {
1365 size_t bytes;
1366 #ifdef TRACE
1367 Trd *trd;
1368 #endif
1369
1370 bytes = bytes_clause (ps, c->size, c->learned);
1371
1372 #ifdef TRACE
1373 if (ps->trace)
1374 {
1375 trd = CLS2TRD (c);
1376 delete (ps, trd, bytes);
1377 }
1378 else
1379 #endif
1380 delete (ps, c, bytes);
1381 }
1382
1383 static void
1384 delete_clauses (PS * ps)
1385 {
1386 Cls **p;
1387 for (p = SOC; p != EOC; p = NXC (p))
1388 if (*p)
1389 delete_clause (ps, *p);
1390
1391 DELETEN (ps->oclauses, ps->eoo - ps->oclauses);
1392 DELETEN (ps->lclauses, ps->EOL - ps->lclauses);
1393
1394 ps->ohead = ps->eoo = ps->lhead = ps->EOL = 0;
1395 }
1396
1397 #ifdef TRACE
1398
1399 static void
1400 delete_zhain (PS * ps, Zhn * zhain)
1401 {
1402 const Znt *p, *znt;
1403
1404 assert (zhain);
1405
1406 znt = zhain->znt;
1407 for (p = znt; *p; p++)
1408 ;
1409
1410 delete (ps, zhain, sizeof (Zhn) + (p - znt) + 1);
1411 }
1412
1413 static void
1414 delete_zhains (PS * ps)
1415 {
1416 Zhn **p, *z;
1417 for (p = ps->zhains; p < ps->zhead; p++)
1418 if ((z = *p))
1419 delete_zhain (ps, z);
1420
1421 DELETEN (ps->zhains, ps->eoz - ps->zhains);
1422 ps->eoz = ps->zhead = 0;
1423 }
1424
1425 #endif
1426
1427 #ifdef NO_BINARY_CLAUSES
1428 static void
1429 lrelease (PS * ps, Ltk * stk)
1430 {
1431 if (stk->start)
1432 DELETEN (stk->start, (1 << (stk->ldsize)));
1433 memset (stk, 0, sizeof (*stk));
1434 }
1435 #endif
1436
1437 #ifndef NADC
1438
1439 static unsigned
1440 llength (Lit ** a)
1441 {
1442 Lit ** p;
1443 for (p = a; *p; p++)
1444 ;
1445 return p - a;
1446 }
1447
1448 static void
1449 resetadoconflict (PS * ps)
1450 {
1451 assert (ps->adoconflict);
1452 delete_clause (ps, ps->adoconflict);
1453 ps->adoconflict = 0;
1454 }
1455
1456 static void
1457 reset_ados (PS * ps)
1458 {
1459 Lit *** p;
1460
1461 for (p = ps->ados; p < ps->hados; p++)
1462 DELETEN (*p, llength (*p) + 1);
1463
1464 DELETEN (ps->ados, ps->eados - ps->ados);
1465 ps->hados = ps->eados = 0;
1466
1467 DELETEN (ps->adotab, ps->szadotab);
1468 ps->szadotab = ps->nadotab = 0;
1469
1470 if (ps->adoconflict)
1471 resetadoconflict (ps);
1472
1473 ps->adoconflicts = 0;
1474 ps->adoconflictlimit = UINT_MAX;
1475 ps->adodisabled = 0;
1476 }
1477
1478 #endif
1479
1480 static void
1481 reset (PS * ps)
1482 {
1483 ABORTIF (!ps ||
1484 ps->state == RESET, "API usage: reset without initialization");
1485
1486 delete_clauses (ps);
1487 #ifdef TRACE
1488 delete_zhains (ps);
1489 #endif
1490 #ifdef NO_BINARY_CLAUSES
1491 {
1492 unsigned i;
1493 for (i = 2; i <= 2 * ps->max_var + 1; i++)
1494 lrelease (ps, ps->impls + i);
1495 }
1496 #endif
1497 #ifndef NADC
1498 reset_ados (ps);
1499 #endif
1500 #ifndef NFL
1501 DELETEN (ps->saved, ps->saved_size);
1502 #endif
1503 DELETEN (ps->htps, 2 * ps->size_vars);
1504 #ifndef NDSC
1505 DELETEN (ps->dhtps, 2 * ps->size_vars);
1506 #endif
1507 DELETEN (ps->impls, 2 * ps->size_vars);
1508 DELETEN (ps->lits, 2 * ps->size_vars);
1509 DELETEN (ps->jwh, 2 * ps->size_vars);
1510 DELETEN (ps->vars, ps->size_vars);
1511 DELETEN (ps->rnks, ps->size_vars);
1512 DELETEN (ps->trail, ps->eot - ps->trail);
1513 DELETEN (ps->heap, ps->eoh - ps->heap);
1514 DELETEN (ps->als, ps->eoals - ps->als);
1515 DELETEN (ps->CLS, ps->eocls - ps->CLS);
1516 DELETEN (ps->rils, ps->eorils - ps->rils);
1517 DELETEN (ps->cils, ps->eocils - ps->cils);
1518 DELETEN (ps->fals, ps->eofals - ps->fals);
1519 DELETEN (ps->mass, ps->szmass);
1520 DELETEN (ps->mssass, ps->szmssass);
1521 DELETEN (ps->mcsass, ps->szmcsass);
1522 DELETEN (ps->humus, ps->szhumus);
1523 DELETEN (ps->added, ps->eoa - ps->added);
1524 DELETEN (ps->marked, ps->eom - ps->marked);
1525 DELETEN (ps->dfs, ps->eod - ps->dfs);
1526 DELETEN (ps->resolved, ps->eor - ps->resolved);
1527 DELETEN (ps->levels, ps->eolevels - ps->levels);
1528 DELETEN (ps->dused, ps->eodused - ps->dused);
1529 DELETEN (ps->buffer, ps->eob - ps->buffer);
1530 DELETEN (ps->indices, ps->eoi - ps->indices);
1531 DELETEN (ps->soclauses, ps->eoso - ps->soclauses);
1532 delete_prefix (ps);
1533 delete (ps, ps->rline[0], ps->szrline);
1534 delete (ps, ps->rline[1], ps->szrline);
1535 assert (getenv ("LEAK") || !ps->current_bytes); /* found leak if failing */
1536 #ifdef VISCORES
1537 pclose (ps->fviscores);
1538 #endif
1539 if (ps->edelete)
1540 ps->edelete (ps->emgr, ps, sizeof *ps);
1541 else
1542 free (ps);
1543 }
1544
1545 inline static void
1546 tpush (PS * ps, Lit * lit)
1547 {
1548 assert (ps->lits < lit && lit <= ps->lits + 2* ps->max_var + 1);
1549 if (ps->thead == ps->eot)
1550 {
1551 unsigned ttail2count = ps->ttail2 - ps->trail;
1552 unsigned ttailcount = ps->ttail - ps->trail;
1553 #ifndef NADC
1554 unsigned ttailadocount = ps->ttailado - ps->trail;
1555 #endif
1556 ENLARGE (ps->trail, ps->thead, ps->eot);
1557 ps->ttail = ps->trail + ttailcount;
1558 ps->ttail2 = ps->trail + ttail2count;
1559 #ifndef NADC
1560 ps->ttailado = ps->trail + ttailadocount;
1561 #endif
1562 }
1563
1564 *ps->thead++ = lit;
1565 }
1566
1567 static void
1568 assign_reason (PS * ps, Var * v, Cls * reason)
1569 {
1570 #if defined(NO_BINARY_CLAUSES) && !defined(NDEBUG)
1571 assert (reason != &ps->impl);
1572 #else
1573 (void) ps;
1574 #endif
1575 v->reason = reason;
1576 }
1577
1578 static void
1579 assign_phase (PS * ps, Lit * lit)
1580 {
1581 unsigned new_phase, idx;
1582 Var * v = LIT2VAR (lit);
1583
1584 #ifndef NFL
1585 /* In 'simplifying' mode we only need to keep 'min_flipped' up to date if
1586 * we force assignments on the top level. The other assignments will be
1587 * undone and thus we can keep the old saved value of the phase.
1588 */
1589 if (!ps->LEVEL || !ps->simplifying)
1590 #endif
1591 {
1592 new_phase = (LIT2SGN (lit) > 0);
1593
1594 if (v->assigned)
1595 {
1596 ps->sdflips -= ps->sdflips/FFLIPPED;
1597
1598 if (new_phase != v->phase)
1599 {
1600 assert (FFLIPPEDPREC >= FFLIPPED);
1601 ps->sdflips += FFLIPPEDPREC / FFLIPPED;
1602 ps->flips++;
1603
1604 idx = LIT2IDX (lit);
1605 if (idx < ps->min_flipped)
1606 ps->min_flipped = idx;
1607
1608 NOLOG (fprintf (ps->out,
1609 "%sflipped %d\n",
1610 ps->prefix, LIT2INT (lit)));
1611 }
1612 }
1613
1614 v->phase = new_phase;
1615 v->assigned = 1;
1616 }
1617
1618 lit->val = TRUE;
1619 NOTLIT (lit)->val = FALSE;
1620 }
1621
1622 inline static void
1623 assign (PS * ps, Lit * lit, Cls * reason)
1624 {
1625 Var * v = LIT2VAR (lit);
1626 assert (lit->val == UNDEF);
1627 #ifdef STATS
1628 ps->assignments++;
1629 #endif
1630 v->level = ps->LEVEL;
1631 assign_phase (ps, lit);
1632 assign_reason (ps, v, reason);
1633 tpush (ps, lit);
1634 }
1635
1636 inline static int
1637 cmp_added (PS * ps, Lit * k, Lit * l)
1638 {
1639 Val a = k->val, b = l->val;
1640 Var *u, *v;
1641 int res;
1642
1643 if (a == UNDEF && b != UNDEF)
1644 return -1;
1645
1646 if (a != UNDEF && b == UNDEF)
1647 return 1;
1648
1649 u = LIT2VAR (k);
1650 v = LIT2VAR (l);
1651
1652 if (a != UNDEF)
1653 {
1654 assert (b != UNDEF);
1655 res = v->level - u->level;
1656 if (res)
1657 return res; /* larger level first */
1658 }
1659
1660 res = cmpflt (VAR2RNK (u)->score, VAR2RNK (v)->score);
1661 if (res)
1662 return res; /* smaller activity first */
1663
1664 return u - v; /* smaller index first */
1665 }
1666
1667 static void
1668 sorttwolits (Lit ** v)
1669 {
1670 Lit * a = v[0], * b = v[1];
1671
1672 assert (a != b);
1673
1674 if (a < b)
1675 return;
1676
1677 v[0] = b;
1678 v[1] = a;
1679 }
1680
1681 inline static void
1682 sortlits (PS * ps, Lit ** v, unsigned size)
1683 {
1684 if (size == 2)
1685 sorttwolits (v); /* same order with and with out 'NO_BINARY_CLAUSES' */
1686 else
1687 SORT (Lit *, cmp_added, v, size);
1688 }
1689
1690 #ifdef NO_BINARY_CLAUSES
1691 static Cls *
1692 setimpl (PS * ps, Lit * a, Lit * b)
1693 {
1694 assert (!ps->implvalid);
1695 assert (ps->impl.size == 2);
1696
1697 ps->impl.lits[0] = a;
1698 ps->impl.lits[1] = b;
1699
1700 sorttwolits (ps->impl.lits);
1701 ps->implvalid = 1;
1702
1703 return &ps->impl;
1704 }
1705
1706 static void
1707 resetimpl (PS * ps)
1708 {
1709 ps->implvalid = 0;
1710 }
1711
1712 static Cls *
1713 setcimpl (PS * ps, Lit * a, Lit * b)
1714 {
1715 assert (!ps->cimplvalid);
1716 assert (ps->cimpl.size == 2);
1717
1718 ps->cimpl.lits[0] = a;
1719 ps->cimpl.lits[1] = b;
1720
1721 sorttwolits (ps->cimpl.lits);
1722 ps->cimplvalid = 1;
1723
1724 return &ps->cimpl;
1725 }
1726
1727 static void
1728 resetcimpl (PS * ps)
1729 {
1730 assert (ps->cimplvalid);
1731 ps->cimplvalid = 0;
1732 }
1733
1734 #endif
1735
1736 static int
1737 cmp_ptr (PS * ps, void *l, void *k)
1738 {
1739 (void) ps;
1740 return ((char*)l) - (char*)k; /* arbitrarily already reverse */
1741 }
1742
1743 static int
1744 cmp_rnk (Rnk * r, Rnk * s)
1745 {
1746 if (!r->moreimportant && s->moreimportant)
1747 return -1;
1748
1749 if (r->moreimportant && !s->moreimportant)
1750 return 1;
1751
1752 if (!r->lessimportant && s->lessimportant)
1753 return 1;
1754
1755 if (r->lessimportant && !s->lessimportant)
1756 return -1;
1757
1758 if (r->score < s->score)
1759 return -1;
1760
1761 if (r->score > s->score)
1762 return 1;
1763
1764 return -cmp_ptr (0, r, s);
1765 }
1766
1767 static void
1768 hup (PS * ps, Rnk * v)
1769 {
1770 int upos, vpos;
1771 Rnk *u;
1772
1773 #ifndef NFL
1774 assert (!ps->simplifying);
1775 #endif
1776
1777 vpos = v->pos;
1778
1779 assert (0 < vpos);
1780 assert (vpos < ps->hhead - ps->heap);
1781 assert (ps->heap[vpos] == v);
1782
1783 while (vpos > 1)
1784 {
1785 upos = vpos / 2;
1786
1787 u = ps->heap[upos];
1788
1789 if (cmp_rnk (u, v) > 0)
1790 break;
1791
1792 ps->heap[vpos] = u;
1793 u->pos = vpos;
1794
1795 vpos = upos;
1796 }
1797
1798 ps->heap[vpos] = v;
1799 v->pos = vpos;
1800 }
1801
1802 static Cls *add_simplified_clause (PS *, int);
1803
1804 inline static void
1805 add_antecedent (PS * ps, Cls * c)
1806 {
1807 assert (c);
1808
1809 #ifdef NO_BINARY_CLAUSES
1810 if (ISLITREASON (c))
1811 return;
1812
1813 if (c == &ps->impl)
1814 return;
1815 #elif defined(STATS) && defined(TRACE)
1816 ps->antecedents++;
1817 #endif
1818 if (ps->rhead == ps->eor)
1819 ENLARGE (ps->resolved, ps->rhead, ps->eor);
1820
1821 assert (ps->rhead < ps->eor);
1822 *ps->rhead++ = c;
1823 }
1824
1825 #ifdef TRACE
1826
1827 #ifdef NO_BINARY_CLAUSES
1828 #error "can not combine TRACE and NO_BINARY_CLAUSES"
1829 #endif
1830
1831 #endif /* TRACE */
1832
1833 static void
1834 add_lit (PS * ps, Lit * lit)
1835 {
1836 assert (lit);
1837
1838 if (ps->ahead == ps->eoa)
1839 ENLARGE (ps->added, ps->ahead, ps->eoa);
1840
1841 *ps->ahead++ = lit;
1842 }
1843
1844 static void
1845 push_var_as_marked (PS * ps, Var * v)
1846 {
1847 if (ps->mhead == ps->eom)
1848 ENLARGE (ps->marked, ps->mhead, ps->eom);
1849
1850 *ps->mhead++ = v;
1851 }
1852
1853 static void
1854 mark_var (PS * ps, Var * v)
1855 {
1856 assert (!v->mark);
1857 v->mark = 1;
1858 push_var_as_marked (ps, v);
1859 }
1860
1861 #ifdef NO_BINARY_CLAUSES
1862
1863 static Cls *
1864 impl2reason (PS * ps, Lit * lit)
1865 {
1866 Lit * other;
1867 Cls * res;
1868 other = ps->impl.lits[0];
1869 if (lit == other)
1870 other = ps->impl.lits[1];
1871 assert (other->val == FALSE);
1872 res = LIT2REASON (NOTLIT (other));
1873 resetimpl (ps);
1874 return res;
1875 }
1876
1877 #endif
1878
1879 /* Whenever we have a top level derived unit we really should derive a unit
1880 * clause otherwise the resolutions in 'add_simplified_clause' become
1881 * incorrect.
1882 */
1883 static Cls *
1884 resolve_top_level_unit (PS * ps, Lit * lit, Cls * reason)
1885 {
1886 unsigned count_resolved;
1887 Lit **p, **eol, *other;
1888 Var *u, *v;
1889
1890 assert (ps->rhead == ps->resolved);
1891 assert (ps->ahead == ps->added);
1892
1893 add_lit (ps, lit);
1894 add_antecedent (ps, reason);
1895 count_resolved = 1;
1896 v = LIT2VAR (lit);
1897
1898 eol = end_of_lits (reason);
1899 for (p = reason->lits; p < eol; p++)
1900 {
1901 other = *p;
1902 u = LIT2VAR (other);
1903 if (u == v)
1904 continue;
1905
1906 add_antecedent (ps, u->reason);
1907 count_resolved++;
1908 }
1909
1910 /* Some of the literals could be assumptions. If at least one
1911 * variable is not an assumption, we should resolve.
1912 */
1913 if (count_resolved >= 2)
1914 {
1915 #ifdef NO_BINARY_CLAUSES
1916 if (reason == &ps->impl)
1917 resetimpl (ps);
1918 #endif
1919 reason = add_simplified_clause (ps, 1);
1920 #ifdef NO_BINARY_CLAUSES
1921 if (reason->size == 2)
1922 {
1923 assert (reason == &ps->impl);
1924 reason = impl2reason (ps, lit);
1925 }
1926 #endif
1927 assign_reason (ps, v, reason);
1928 }
1929 else
1930 {
1931 ps->ahead = ps->added;
1932 ps->rhead = ps->resolved;
1933 }
1934
1935 return reason;
1936 }
1937
1938 static void
1939 fixvar (PS * ps, Var * v)
1940 {
1941 Rnk * r;
1942
1943 assert (VAR2LIT (v) != UNDEF);
1944 assert (!v->level);
1945
1946 ps->fixed++;
1947
1948 r = VAR2RNK (v);
1949 r->score = INFFLT;
1950
1951 #ifndef NFL
1952 if (ps->simplifying)
1953 return;
1954 #endif
1955
1956 if (!r->pos)
1957 return;
1958
1959 hup (ps, r);
1960 }
1961
1962 static void
1963 use_var (PS * ps, Var * v)
1964 {
1965 if (v->used)
1966 return;
1967
1968 v->used = 1;
1969 ps->vused++;
1970 }
1971
1972 static void
1973 assign_forced (PS * ps, Lit * lit, Cls * reason)
1974 {
1975 Var *v;
1976
1977 assert (reason);
1978 assert (lit->val == UNDEF);
1979
1980 #ifdef STATS
1981 ps->FORCED++;
1982 #endif
1983 assign (ps, lit, reason);
1984
1985 #ifdef NO_BINARY_CLAUSES
1986 assert (reason != &ps->impl);
1987 if (ISLITREASON (reason))
1988 {
1989 reason = setimpl (ps, lit, NOTLIT (REASON2LIT (reason)));
1990 assert (reason);
1991 }
1992 #endif
1993 LOG ( fprintf (ps->out,
1994 "%sassign %d at level %d by ",
1995 ps->prefix, LIT2INT (lit), ps->LEVEL);
1996 dumpclsnl (ps, reason));
1997
1998 v = LIT2VAR (lit);
1999 if (!ps->LEVEL)
2000 use_var (ps, v);
2001
2002 if (!ps->LEVEL && reason->size > 1)
2003 {
2004 reason = resolve_top_level_unit (ps, lit, reason);
2005 assert (reason);
2006 }
2007
2008 #ifdef NO_BINARY_CLAUSES
2009 if (ISLITREASON (reason) || reason == &ps->impl)
2010 {
2011 /* DO NOTHING */
2012 }
2013 else
2014 #endif
2015 {
2016 assert (!reason->locked);
2017 reason->locked = 1;
2018 if (reason->learned && reason->size > 2)
2019 ps->llocked++;
2020 }
2021
2022 #ifdef NO_BINARY_CLAUSES
2023 if (reason == &ps->impl)
2024 resetimpl (ps);
2025 #endif
2026
2027 if (!ps->LEVEL)
2028 fixvar (ps, v);
2029 }
2030
2031 #ifdef NO_BINARY_CLAUSES
2032
2033 static void
2034 lpush (PS * ps, Lit * lit, Cls * c)
2035 {
2036 int pos = (c->lits[0] == lit);
2037 Ltk * s = LIT2IMPLS (lit);
2038 unsigned oldsize, newsize;
2039
2040 assert (c->size == 2);
2041
2042 if (!s->start)
2043 {
2044 assert (!s->count);
2045 assert (!s->ldsize);
2046 NEWN (s->start, 1);
2047 }
2048 else
2049 {
2050 oldsize = (1 << (s->ldsize));
2051 assert (s->count <= oldsize);
2052 if (s->count == oldsize)
2053 {
2054 newsize = 2 * oldsize;
2055 RESIZEN (s->start, oldsize, newsize);
2056 s->ldsize++;
2057 }
2058 }
2059
2060 s->start[s->count++] = c->lits[pos];
2061 }
2062
2063 #endif
2064
2065 static void
2066 connect_head_tail (PS * ps, Lit * lit, Cls * c)
2067 {
2068 Cls ** s;
2069 assert (c->size >= 1);
2070 if (c->size == 2)
2071 {
2072 #ifdef NO_BINARY_CLAUSES
2073 lpush (ps, lit, c);
2074 return;
2075 #else
2076 s = LIT2IMPLS (lit);
2077 #endif
2078 }
2079 else
2080 s = LIT2HTPS (lit);
2081
2082 if (c->lits[0] != lit)
2083 {
2084 assert (c->size >= 2);
2085 assert (c->lits[1] == lit);
2086 c->next[1] = *s;
2087 }
2088 else
2089 c->next[0] = *s;
2090
2091 *s = c;
2092 }
2093
2094 #ifdef TRACE
2095 static void
2096 zpush (PS * ps, Zhn * zhain)
2097 {
2098 assert (ps->trace);
2099
2100 if (ps->zhead == ps->eoz)
2101 ENLARGE (ps->zhains, ps->zhead, ps->eoz);
2102
2103 *ps->zhead++ = zhain;
2104 }
2105
2106 static int
2107 cmp_resolved (PS * ps, Cls * c, Cls * d)
2108 {
2109 #ifndef NDEBUG
2110 assert (ps->trace);
2111 #else
2112 (void) ps;
2113 #endif
2114 return CLS2IDX (c) - CLS2IDX (d);
2115 }
2116
2117 static void
2118 bpushc (PS * ps, unsigned char ch)
2119 {
2120 if (ps->bhead == ps->eob)
2121 ENLARGE (ps->buffer, ps->bhead, ps->eob);
2122
2123 *ps->bhead++ = ch;
2124 }
2125
2126 static void
2127 bpushu (PS * ps, unsigned u)
2128 {
2129 while (u & ~0x7f)
2130 {
2131 bpushc (ps, u | 0x80);
2132 u >>= 7;
2133 }
2134
2135 bpushc (ps, u);
2136 }
2137
2138 static void
2139 bpushd (PS * ps, unsigned prev, unsigned this)
2140 {
2141 unsigned delta;
2142 assert (prev < this);
2143 delta = this - prev;
2144 bpushu (ps, delta);
2145 }
2146
2147 static void
2148 add_zhain (PS * ps)
2149 {
2150 unsigned prev, this, count, rcount;
2151 Cls **p, *c;
2152 Zhn *res;
2153
2154 assert (ps->trace);
2155 assert (ps->bhead == ps->buffer);
2156 assert (ps->rhead > ps->resolved);
2157
2158 rcount = ps->rhead - ps->resolved;
2159 SORT (Cls *, cmp_resolved, ps->resolved, rcount);
2160
2161 prev = 0;
2162 for (p = ps->resolved; p < ps->rhead; p++)
2163 {
2164 c = *p;
2165 this = CLS2TRD (c)->idx;
2166 bpushd (ps, prev, this);
2167 prev = this;
2168 }
2169 bpushc (ps, 0);
2170
2171 count = ps->bhead - ps->buffer;
2172
2173 res = new (ps, sizeof (Zhn) + count);
2174 res->core = 0;
2175 res->ref = 0;
2176 memcpy (res->znt, ps->buffer, count);
2177
2178 ps->bhead = ps->buffer;
2179 #ifdef STATS
2180 ps->znts += count - 1;
2181 #endif
2182 zpush (ps, res);
2183 }
2184
2185 #endif
2186
2187 static void
2188 add_resolved (PS * ps, int learned)
2189 {
2190 #if defined(STATS) || defined(TRACE)
2191 Cls **p, *c;
2192
2193 for (p = ps->resolved; p < ps->rhead; p++)
2194 {
2195 c = *p;
2196 if (c->used)
2197 continue;
2198
2199 c->used = 1;
2200
2201 if (c->size <= 2)
2202 continue;
2203
2204 #ifdef STATS
2205 if (c->learned)
2206 ps->llused++;
2207 else
2208 ps->loused++;
2209 #endif
2210 }
2211 #endif
2212
2213 #ifdef TRACE
2214 if (learned && ps->trace)
2215 add_zhain (ps);
2216 #else
2217 (void) learned;
2218 #endif
2219 ps->rhead = ps->resolved;
2220 }
2221
2222 static void
2223 incjwh (PS * ps, Cls * c)
2224 {
2225 Lit **p, *lit, ** eol;
2226 Flt * f, inc, sum;
2227 unsigned size = 0;
2228 Var * v;
2229 Val val;
2230
2231 eol = end_of_lits (c);
2232
2233 for (p = c->lits; p < eol; p++)
2234 {
2235 lit = *p;
2236 val = lit->val;
2237
2238 if (val && ps->LEVEL > 0)
2239 {
2240 v = LIT2VAR (lit);
2241 if (v->level > 0)
2242 val = UNDEF;
2243 }
2244
2245 if (val == TRUE)
2246 return;
2247
2248 if (val != FALSE)
2249 size++;
2250 }
2251
2252 inc = base2flt (1, -size);
2253
2254 for (p = c->lits; p < eol; p++)
2255 {
2256 lit = *p;
2257 f = LIT2JWH (lit);
2258 sum = addflt (*f, inc);
2259 *f = sum;
2260 }
2261 }
2262
2263 static void
2264 write_rup_header (PS * ps, FILE * file)
2265 {
2266 char line[80];
2267 int i;
2268
2269 sprintf (line, "%%RUPD32 %u %u", ps->rupvariables, ps->rupclauses);
2270
2271 fputs (line, file);
2272 for (i = 255 - strlen (line); i >= 0; i--)
2273 fputc (' ', file);
2274
2275 fputc ('\n', file);
2276 fflush (file);
2277 }
2278
2279 static Cls *
2280 add_simplified_clause (PS * ps, int learned)
2281 {
2282 unsigned num_true, num_undef, num_false, size, count_resolved;
2283 Lit **p, **q, *lit, ** end;
2284 unsigned litlevel, glue;
2285 Cls *res, * reason;
2286 int reentered;
2287 Val val;
2288 Var *v;
2289 #if !defined(NDEBUG) && defined(TRACE)
2290 unsigned idx;
2291 #endif
2292
2293 reentered = 0;
2294
2295 REENTER:
2296
2297 size = ps->ahead - ps->added;
2298
2299 add_resolved (ps, learned);
2300
2301 if (learned)
2302 {
2303 ps->ladded++;
2304 ps->llitsadded += size;
2305 if (size > 2)
2306 {
2307 ps->lladded++;
2308 ps->nlclauses++;
2309 ps->llits += size;
2310 }
2311 }
2312 else
2313 {
2314 ps->oadded++;
2315 if (size > 2)
2316 {
2317 ps->loadded++;
2318 ps->noclauses++;
2319 ps->olits += size;
2320 }
2321 }
2322
2323 ps->addedclauses++;
2324 assert (ps->addedclauses == ps->ladded + ps->oadded);
2325
2326 #ifdef NO_BINARY_CLAUSES
2327 if (size == 2)
2328 res = setimpl (ps, ps->added[0], ps->added[1]);
2329 else
2330 #endif
2331 {
2332 sortlits (ps, ps->added, size);
2333
2334 if (learned)
2335 {
2336 if (ps->lhead == ps->EOL)
2337 {
2338 ENLARGE (ps->lclauses, ps->lhead, ps->EOL);
2339
2340 /* A very difficult to find bug, which only occurs if the
2341 * learned clauses stack is immediately allocated before the
2342 * original clauses stack without padding. In this case, we
2343 * have 'SOC == EOC', which terminates all loops using the
2344 * idiom 'for (p = SOC; p != EOC; p = NXC(p))' immediately.
2345 * Unfortunately this occurred in 'fix_clause_lits' after
2346 * using a recent version of the memory allocator of 'Google'
2347 * perftools in the context of one large benchmark for
2348 * our SMT solver 'Boolector'.
2349 */
2350 if (ps->EOL == ps->oclauses)
2351 ENLARGE (ps->lclauses, ps->lhead, ps->EOL);
2352 }
2353
2354 #if !defined(NDEBUG) && defined(TRACE)
2355 idx = LIDX2IDX (ps->lhead - ps->lclauses);
2356 #endif
2357 }
2358 else
2359 {
2360 if (ps->ohead == ps->eoo)
2361 {
2362 ENLARGE (ps->oclauses, ps->ohead, ps->eoo);
2363 if (ps->EOL == ps->oclauses)
2364 ENLARGE (ps->oclauses, ps->ohead, ps->eoo); /* ditto */
2365 }
2366
2367 #if !defined(NDEBUG) && defined(TRACE)
2368 idx = OIDX2IDX (ps->ohead - ps->oclauses);
2369 #endif
2370 }
2371
2372 assert (ps->EOL != ps->oclauses); /* ditto */
2373
2374 res = new_clause (ps, size, learned);
2375
2376 glue = 0;
2377
2378 if (learned)
2379 {
2380 assert (ps->dusedhead == ps->dused);
2381
2382 for (p = ps->added; p < ps->ahead; p++)
2383 {
2384 lit = *p;
2385 if (lit->val)
2386 {
2387 litlevel = LIT2VAR (lit)->level;
2388 assert (litlevel <= ps->LEVEL);
2389 while (ps->levels + litlevel >= ps->levelshead)
2390 {
2391 if (ps->levelshead >= ps->eolevels)
2392 ENLARGE (ps->levels, ps->levelshead, ps->eolevels);
2393 assert (ps->levelshead < ps->eolevels);
2394 *ps->levelshead++ = 0;
2395 }
2396 if (!ps->levels[litlevel])
2397 {
2398 if (ps->dusedhead >= ps->eodused)
2399 ENLARGE (ps->dused, ps->dusedhead, ps->eodused);
2400 assert (ps->dusedhead < ps->eodused);
2401 *ps->dusedhead++ = litlevel;
2402 ps->levels[litlevel] = 1;
2403 glue++;
2404 }
2405 }
2406 else
2407 glue++;
2408 }
2409
2410 while (ps->dusedhead > ps->dused)
2411 {
2412 litlevel = *--ps->dusedhead;
2413 assert (ps->levels + litlevel < ps->levelshead);
2414 assert (ps->levels[litlevel]);
2415 ps->levels[litlevel] = 0;
2416 }
2417 }
2418
2419 assert (glue <= MAXGLUE);
2420 res->glue = glue;
2421
2422 #if !defined(NDEBUG) && defined(TRACE)
2423 if (ps->trace)
2424 assert (CLS2IDX (res) == idx);
2425 #endif
2426 if (learned)
2427 *ps->lhead++ = res;
2428 else
2429 *ps->ohead++ = res;
2430
2431 #if !defined(NDEBUG) && defined(TRACE)
2432 if (ps->trace && learned)
2433 assert (ps->zhead - ps->zhains == ps->lhead - ps->lclauses);
2434 #endif
2435 assert (ps->lhead != ps->oclauses); /* ditto */
2436 }
2437
2438 if (learned && ps->rup)
2439 {
2440 if (!ps->rupstarted)
2441 {
2442 write_rup_header (ps, ps->rup);
2443 ps->rupstarted = 1;
2444 }
2445 }
2446
2447 num_true = num_undef = num_false = 0;
2448
2449 q = res->lits;
2450 for (p = ps->added; p < ps->ahead; p++)
2451 {
2452 lit = *p;
2453 *q++ = lit;
2454
2455 if (learned && ps->rup)
2456 fprintf (ps->rup, "%d ", LIT2INT (lit));
2457
2458 val = lit->val;
2459
2460 num_true += (val == TRUE);
2461 num_undef += (val == UNDEF);
2462 num_false += (val == FALSE);
2463 }
2464 assert (num_false + num_true + num_undef == size);
2465
2466 if (learned && ps->rup)
2467 fputs ("0\n", ps->rup);
2468
2469 ps->ahead = ps->added; /* reset */
2470
2471 if (!reentered) // TODO merge
2472 if (size > 0)
2473 {
2474 assert (size <= 2 || !reentered); // TODO remove
2475 connect_head_tail (ps, res->lits[0], res);
2476 if (size > 1)
2477 connect_head_tail (ps, res->lits[1], res);
2478 }
2479
2480 if (size == 0)
2481 {
2482 if (!ps->mtcls)
2483 ps->mtcls = res;
2484 }
2485
2486 #ifdef NO_BINARY_CLAUSES
2487 if (size != 2)
2488 #endif
2489 #ifndef NDEBUG
2490 res->connected = 1;
2491 #endif
2492
2493 LOG ( fprintf (ps->out, "%s%s ", ps->prefix, learned ? "learned" : "original");
2494 dumpclsnl (ps, res));
2495
2496 /* Shrink clause by resolving it against top level assignments.
2497 */
2498 if (!ps->LEVEL && num_false > 0)
2499 {
2500 assert (ps->ahead == ps->added);
2501 assert (ps->rhead == ps->resolved);
2502
2503 count_resolved = 1;
2504 add_antecedent (ps, res);
2505
2506 end = end_of_lits (res);
2507 for (p = res->lits; p < end; p++)
2508 {
2509 lit = *p;
2510 v = LIT2VAR (lit);
2511 use_var (ps, v);
2512
2513 if (lit->val == FALSE)
2514 {
2515 add_antecedent (ps, v->reason);
2516 count_resolved++;
2517 }
2518 else
2519 add_lit (ps, lit);
2520 }
2521
2522 assert (count_resolved >= 2);
2523
2524 learned = 1;
2525 #ifdef NO_BINARY_CLAUSES
2526 if (res == &ps->impl)
2527 resetimpl (ps);
2528 #endif
2529 reentered = 1;
2530 goto REENTER; /* and return simplified clause */
2531 }
2532
2533 if (!num_true && num_undef == 1) /* unit clause */
2534 {
2535 lit = 0;
2536 for (p = res->lits; p < res->lits + size; p++)
2537 {
2538 if ((*p)->val == UNDEF)
2539 lit = *p;
2540
2541 v = LIT2VAR (*p);
2542 use_var (ps, v);
2543 }
2544 assert (lit);
2545
2546 reason = res;
2547 #ifdef NO_BINARY_CLAUSES
2548 if (size == 2)
2549 {
2550 Lit * other = res->lits[0];
2551 if (other == lit)
2552 other = res->lits[1];
2553
2554 assert (other->val == FALSE);
2555 reason = LIT2REASON (NOTLIT (other));
2556 }
2557 #endif
2558 assign_forced (ps, lit, reason);
2559 num_true++;
2560 }
2561
2562 if (num_false == size && !ps->conflict)
2563 {
2564 #ifdef NO_BINARY_CLAUSES
2565 if (res == &ps->impl)
2566 ps->conflict = setcimpl (ps, res->lits[0], res->lits[1]);
2567 else
2568 #endif
2569 ps->conflict = res;
2570 }
2571
2572 if (!learned && !num_true && num_undef)
2573 incjwh (ps, res);
2574
2575 #ifdef NO_BINARY_CLAUSES
2576 if (res == &ps->impl)
2577 resetimpl (ps);
2578 #endif
2579 return res;
2580 }
2581
2582 static int
2583 trivial_clause (PS * ps)
2584 {
2585 Lit **p, **q, *prev;
2586 Var *v;
2587
2588 SORT (Lit *, cmp_ptr, ps->added, ps->ahead - ps->added);
2589
2590 prev = 0;
2591 q = ps->added;
2592 for (p = q; p < ps->ahead; p++)
2593 {
2594 Lit *this = *p;
2595
2596 v = LIT2VAR (this);
2597
2598 if (prev == this) /* skip repeated literals */
2599 continue;
2600
2601 /* Top level satisfied ?
2602 */
2603 if (this->val == TRUE && !v->level)
2604 return 1;
2605
2606 if (prev == NOTLIT (this))/* found pair of dual literals */
2607 return 1;
2608
2609 *q++ = prev = this;
2610 }
2611
2612 ps->ahead = q; /* shrink */
2613
2614 return 0;
2615 }
2616
2617 static void
2618 simplify_and_add_original_clause (PS * ps)
2619 {
2620 #ifdef NO_BINARY_CLAUSES
2621 Cls * c;
2622 #endif
2623 if (trivial_clause (ps))
2624 {
2625 ps->ahead = ps->added;
2626
2627 if (ps->ohead == ps->eoo)
2628 ENLARGE (ps->oclauses, ps->ohead, ps->eoo);
2629
2630 *ps->ohead++ = 0;
2631
2632 ps->addedclauses++;
2633 ps->oadded++;
2634 }
2635 else
2636 {
2637 if (ps->CLS != ps->clshead)
2638 add_lit (ps, NOTLIT (ps->clshead[-1]));
2639
2640 #ifdef NO_BINARY_CLAUSES
2641 c =
2642 #endif
2643 add_simplified_clause (ps, 0);
2644 #ifdef NO_BINARY_CLAUSES
2645 if (c == &ps->impl) assert (!ps->implvalid);
2646 #endif
2647 }
2648 }
2649
2650 #ifndef NADC
2651
2652 static void
2653 add_ado (PS * ps)
2654 {
2655 unsigned len = ps->ahead - ps->added;
2656 Lit ** ado, ** p, ** q, *lit;
2657 Var * v, * u;
2658
2659 #ifdef TRACE
2660 assert (!ps->trace);
2661 #endif
2662
2663 ABORTIF (ps->ados < ps->hados && llength (ps->ados[0]) != len,
2664 "internal: non matching all different constraint object lengths");
2665
2666 if (ps->hados == ps->eados)
2667 ENLARGE (ps->ados, ps->hados, ps->eados);
2668
2669 NEWN (ado, len + 1);
2670 *ps->hados++ = ado;
2671
2672 p = ps->added;
2673 q = ado;
2674 u = 0;
2675 while (p < ps->ahead)
2676 {
2677 lit = *p++;
2678 v = LIT2VAR (lit);
2679 ABORTIF (v->inado,
2680 "internal: variable in multiple all different objects");
2681 v->inado = ado;
2682 if (!u && !lit->val)
2683 u = v;
2684 *q++ = lit;
2685 }
2686
2687 assert (q == ado + len);
2688 *q++ = 0;
2689
2690 /* TODO simply do a conflict test as in propado */
2691
2692 ABORTIF (!u,
2693 "internal: "
2694 "adding fully instantiated all different object not implemented yet");
2695
2696 assert (u);
2697 assert (u->inado == ado);
2698 assert (!u->ado);
2699 u->ado = ado;
2700
2701 ps->ahead = ps->added;
2702 }
2703
2704 #endif
2705
2706 static void
2707 hdown (PS * ps, Rnk * r)
2708 {
2709 unsigned end, rpos, cpos, opos;
2710 Rnk *child, *other;
2711
2712 assert (r->pos > 0);
2713 assert (ps->heap[r->pos] == r);
2714
2715 end = ps->hhead - ps->heap;
2716 rpos = r->pos;
2717
2718 for (;;)
2719 {
2720 cpos = 2 * rpos;
2721 if (cpos >= end)
2722 break;
2723
2724 opos = cpos + 1;
2725 child = ps->heap[cpos];
2726
2727 if (cmp_rnk (r, child) < 0)
2728 {
2729 if (opos < end)
2730 {
2731 other = ps->heap[opos];
2732
2733 if (cmp_rnk (child, other) < 0)
2734 {
2735 child = other;
2736 cpos = opos;
2737 }
2738 }
2739 }
2740 else if (opos < end)
2741 {
2742 child = ps->heap[opos];
2743
2744 if (cmp_rnk (r, child) >= 0)
2745 break;
2746
2747 cpos = opos;
2748 }
2749 else
2750 break;
2751
2752 ps->heap[rpos] = child;
2753 child->pos = rpos;
2754 rpos = cpos;
2755 }
2756
2757 r->pos = rpos;
2758 ps->heap[rpos] = r;
2759 }
2760
2761 static Rnk *
2762 htop (PS * ps)
2763 {
2764 assert (ps->hhead > ps->heap + 1);
2765 return ps->heap[1];
2766 }
2767
2768 static Rnk *
2769 hpop (PS * ps)
2770 {
2771 Rnk *res, *last;
2772 unsigned end;
2773
2774 assert (ps->hhead > ps->heap + 1);
2775
2776 res = ps->heap[1];
2777 res->pos = 0;
2778
2779 end = --ps->hhead - ps->heap;
2780 if (end == 1)
2781 return res;
2782
2783 last = ps->heap[end];
2784
2785 ps->heap[last->pos = 1] = last;
2786 hdown (ps, last);
2787
2788 return res;
2789 }
2790
2791 inline static void
2792 hpush (PS * ps, Rnk * r)
2793 {
2794 assert (!r->pos);
2795
2796 if (ps->hhead == ps->eoh)
2797 ENLARGE (ps->heap, ps->hhead, ps->eoh);
2798
2799 r->pos = ps->hhead++ - ps->heap;
2800 ps->heap[r->pos] = r;
2801 hup (ps, r);
2802 }
2803
2804 static void
2805 fix_trail_lits (PS * ps, long delta)
2806 {
2807 Lit **p;
2808 for (p = ps->trail; p < ps->thead; p++)
2809 *p += delta;
2810 }
2811
2812 #ifdef NO_BINARY_CLAUSES
2813 static void
2814 fix_impl_lits (PS * ps, long delta)
2815 {
2816 Ltk * s;
2817 Lit ** p;
2818
2819 for (s = ps->impls + 2; s <= ps->impls + 2 * ps->max_var + 1; s++)
2820 for (p = s->start; p < s->start + s->count; p++)
2821 *p += delta;
2822 }
2823 #endif
2824
2825 static void
2826 fix_clause_lits (PS * ps, long delta)
2827 {
2828 Cls **p, *clause;
2829 Lit **q, *lit, **eol;
2830
2831 for (p = SOC; p != EOC; p = NXC (p))
2832 {
2833 clause = *p;
2834 if (!clause)
2835 continue;
2836
2837 q = clause->lits;
2838 eol = end_of_lits (clause);
2839 while (q < eol)
2840 {
2841 assert (q - clause->lits <= (int) clause->size);
2842 lit = *q;
2843 lit += delta;
2844 *q++ = lit;
2845 }
2846 }
2847 }
2848
2849 static void
2850 fix_added_lits (PS * ps, long delta)
2851 {
2852 Lit **p;
2853 for (p = ps->added; p < ps->ahead; p++)
2854 *p += delta;
2855 }
2856
2857 static void
2858 fix_assumed_lits (PS * ps, long delta)
2859 {
2860 Lit **p;
2861 for (p = ps->als; p < ps->alshead; p++)
2862 *p += delta;
2863 }
2864
2865 static void
2866 fix_cls_lits (PS * ps, long delta)
2867 {
2868 Lit **p;
2869 for (p = ps->CLS; p < ps->clshead; p++)
2870 *p += delta;
2871 }
2872
2873 static void
2874 fix_heap_rnks (PS * ps, long delta)
2875 {
2876 Rnk **p;
2877
2878 for (p = ps->heap + 1; p < ps->hhead; p++)
2879 *p += delta;
2880 }
2881
2882 #ifndef NADC
2883
2884 static void
2885 fix_ado (long delta, Lit ** ado)
2886 {
2887 Lit ** p;
2888 for (p = ado; *p; p++)
2889 *p += delta;
2890 }
2891
2892 static void
2893 fix_ados (PS * ps, long delta)
2894 {
2895 Lit *** p;
2896
2897 for (p = ps->ados; p < ps->hados; p++)
2898 fix_ado (delta, *p);
2899 }
2900
2901 #endif
2902
2903 static void
2904 enlarge (PS * ps, unsigned new_size_vars)
2905 {
2906 long rnks_delta, lits_delta;
2907 Lit *old_lits = ps->lits;
2908 Rnk *old_rnks = ps->rnks;
2909
2910 RESIZEN (ps->lits, 2 * ps->size_vars, 2 * new_size_vars);
2911 RESIZEN (ps->jwh, 2 * ps->size_vars, 2 * new_size_vars);
2912 RESIZEN (ps->htps, 2 * ps->size_vars, 2 * new_size_vars);
2913 #ifndef NDSC
2914 RESIZEN (ps->dhtps, 2 * ps->size_vars, 2 * new_size_vars);
2915 #endif
2916 RESIZEN (ps->impls, 2 * ps->size_vars, 2 * new_size_vars);
2917 RESIZEN (ps->vars, ps->size_vars, new_size_vars);
2918 RESIZEN (ps->rnks, ps->size_vars, new_size_vars);
2919
2920 if ((lits_delta = ps->lits - old_lits))
2921 {
2922 fix_trail_lits (ps, lits_delta);
2923 fix_clause_lits (ps, lits_delta);
2924 fix_added_lits (ps, lits_delta);
2925 fix_assumed_lits (ps, lits_delta);
2926 fix_cls_lits (ps, lits_delta);
2927 #ifdef NO_BINARY_CLAUSES
2928 fix_impl_lits (ps, lits_delta);
2929 #endif
2930 #ifndef NADC
2931 fix_ados (ps, lits_delta);
2932 #endif
2933 }
2934
2935 if ((rnks_delta = ps->rnks - old_rnks))
2936 {
2937 fix_heap_rnks (ps, rnks_delta);
2938 }
2939
2940 assert (ps->mhead == ps->marked);
2941
2942 ps->size_vars = new_size_vars;
2943 }
2944
2945 static void
2946 unassign (PS * ps, Lit * lit)
2947 {
2948 Cls *reason;
2949 Var *v;
2950 Rnk *r;
2951
2952 assert (lit->val == TRUE);
2953
2954 LOG ( fprintf (ps->out, "%sunassign %d\n", ps->prefix, LIT2INT (lit)));
2955
2956 v = LIT2VAR (lit);
2957 reason = v->reason;
2958
2959 #ifdef NO_BINARY_CLAUSES
2960 assert (reason != &ps->impl);
2961 if (ISLITREASON (reason))
2962 {
2963 /* DO NOTHING */
2964 }
2965 else
2966 #endif
2967 if (reason)
2968 {
2969 assert (reason->locked);
2970 reason->locked = 0;
2971 if (reason->learned && reason->size > 2)
2972 {
2973 assert (ps->llocked > 0);
2974 ps->llocked--;
2975 }
2976 }
2977
2978 lit->val = UNDEF;
2979 NOTLIT (lit)->val = UNDEF;
2980
2981 r = VAR2RNK (v);
2982 if (!r->pos)
2983 hpush (ps, r);
2984
2985 #ifndef NDSC
2986 {
2987 Cls * p, * next, ** q;
2988
2989 q = LIT2DHTPS (lit);
2990 p = *q;
2991 *q = 0;
2992
2993 while (p)
2994 {
2995 Lit * other = p->lits[0];
2996
2997 if (other == lit)
2998 {
2999 other = p->lits[1];
3000 q = p->next + 1;
3001 }
3002 else
3003 {
3004 assert (p->lits[1] == lit);
3005 q = p->next;
3006 }
3007
3008 next = *q;
3009 *q = *LIT2HTPS (other);
3010 *LIT2HTPS (other) = p;
3011 p = next;
3012 }
3013 }
3014 #endif
3015
3016 #ifndef NADC
3017 if (v->adotabpos)
3018 {
3019 assert (ps->nadotab);
3020 assert (*v->adotabpos == v->ado);
3021
3022 *v->adotabpos = 0;
3023 v->adotabpos = 0;
3024
3025 ps->nadotab--;
3026 }
3027 #endif
3028 }
3029
3030 static Cls *
3031 var2reason (PS * ps, Var * var)
3032 {
3033 Cls * res = var->reason;
3034 #ifdef NO_BINARY_CLAUSES
3035 Lit * this, * other;
3036 if (ISLITREASON (res))
3037 {
3038 this = VAR2LIT (var);
3039 if (this->val == FALSE)
3040 this = NOTLIT (this);
3041
3042 other = REASON2LIT (res);
3043 assert (other->val == TRUE);
3044 assert (this->val == TRUE);
3045 res = setimpl (ps, NOTLIT (other), this);
3046 }
3047 #else
3048 (void) ps;
3049 #endif
3050 return res;
3051 }
3052
3053 static void
3054 mark_clause_to_be_collected (Cls * c)
3055 {
3056 assert (!c->collect);
3057 c->collect = 1;
3058 }
3059
3060 static void
3061 undo (PS * ps, unsigned new_level)
3062 {
3063 Lit *lit;
3064 Var *v;
3065
3066 while (ps->thead > ps->trail)
3067 {
3068 lit = *--ps->thead;
3069 v = LIT2VAR (lit);
3070 if (v->level == new_level)
3071 {
3072 ps->thead++; /* fix pre decrement */
3073 break;
3074 }
3075
3076 unassign (ps, lit);
3077 }
3078
3079 ps->LEVEL = new_level;
3080 ps->ttail = ps->thead;
3081 ps->ttail2 = ps->thead;
3082 #ifndef NADC
3083 ps->ttailado = ps->thead;
3084 #endif
3085
3086 #ifdef NO_BINARY_CLAUSES
3087 if (ps->conflict == &ps->cimpl)
3088 resetcimpl (ps);
3089 #endif
3090 #ifndef NADC
3091 if (ps->conflict && ps->conflict == ps->adoconflict)
3092 resetadoconflict (ps);
3093 #endif
3094 ps->conflict = ps->mtcls;
3095 if (ps->LEVEL < ps->adecidelevel)
3096 {
3097 assert (ps->als < ps->alshead);
3098 ps->adecidelevel = 0;
3099 ps->alstail = ps->als;
3100 }
3101 LOG ( fprintf (ps->out, "%sback to level %u\n", ps->prefix, ps->LEVEL));
3102 }
3103
3104 #ifndef NDEBUG
3105
3106 static int
3107 clause_satisfied (Cls * c)
3108 {
3109 Lit **p, **eol, *lit;
3110
3111 eol = end_of_lits (c);
3112 for (p = c->lits; p < eol; p++)
3113 {
3114 lit = *p;
3115 if (lit->val == TRUE)
3116 return 1;
3117 }
3118
3119 return 0;
3120 }
3121
3122 static void
3123 original_clauses_satisfied (PS * ps)
3124 {
3125 Cls **p, *c;
3126
3127 for (p = ps->oclauses; p < ps->ohead; p++)
3128 {
3129 c = *p;
3130
3131 if (!c)
3132 continue;
3133
3134 if (c->learned)
3135 continue;
3136
3137 assert (clause_satisfied (c));
3138 }
3139 }
3140
3141 static void
3142 assumptions_satisfied (PS * ps)
3143 {
3144 Lit *lit, ** p;
3145
3146 for (p = ps->als; p < ps->alshead; p++)
3147 {
3148 lit = *p;
3149 assert (lit->val == TRUE);
3150 }
3151 }
3152
3153 #endif
3154
3155 static void
3156 sflush (PS * ps)
3157 {
3158 double now = picosat_time_stamp ();
3159 double delta = now - ps->entered;
3160 delta = (delta < 0) ? 0 : delta;
3161 ps->seconds += delta;
3162 ps->entered = now;
3163 }
3164
3165 static double
3166 mb (PS * ps)
3167 {
3168 return ps->current_bytes / (double) (1 << 20);
3169 }
3170
3171 static double
3172 avglevel (PS * ps)
3173 {
3174 return ps->decisions ? ps->levelsum / ps->decisions : 0.0;
3175 }
3176
3177 static void
3178 rheader (PS * ps)
3179 {
3180 assert (ps->lastrheader <= ps->reports);
3181
3182 if (ps->lastrheader == ps->reports)
3183 return;
3184
3185 ps->lastrheader = ps->reports;
3186
3187 fprintf (ps->out, "%s\n", ps->prefix);
3188 fprintf (ps->out, "%s %s\n", ps->prefix, ps->rline[0]);
3189 fprintf (ps->out, "%s %s\n", ps->prefix, ps->rline[1]);
3190 fprintf (ps->out, "%s\n", ps->prefix);
3191 }
3192
3193 static unsigned
3194 dynamic_flips_per_assignment_per_mille (PS * ps)
3195 {
3196 assert (FFLIPPEDPREC >= 1000);
3197 return ps->sdflips / (FFLIPPEDPREC / 1000);
3198 }
3199
3200 #ifdef NLUBY
3201
3202 static int
3203 high_agility (PS * ps)
3204 {
3205 return dynamic_flips_per_assignment_per_mille (ps) >= 200;
3206 }
3207
3208 static int
3209 very_high_agility (PS * ps)
3210 {
3211 return dynamic_flips_per_assignment_per_mille (ps) >= 250;
3212 }
3213
3214 #else
3215
3216 static int
3217 medium_agility (PS * ps)
3218 {
3219 return dynamic_flips_per_assignment_per_mille (ps) >= 230;
3220 }
3221
3222 #endif
3223
3224 static void
3225 relemdata (PS * ps)
3226 {
3227 char *p;
3228 int x;
3229
3230 if (ps->reports < 0)
3231 {
3232 /* strip trailing white space
3233 */
3234 for (x = 0; x <= 1; x++)
3235 {
3236 p = ps->rline[x] + strlen (ps->rline[x]);
3237 while (p-- > ps->rline[x])
3238 {
3239 if (*p != ' ')
3240 break;
3241
3242 *p = 0;
3243 }
3244 }
3245
3246 rheader (ps);
3247 }
3248 else
3249 fputc ('\n', ps->out);
3250
3251 ps->RCOUNT = 0;
3252 }
3253
3254 static void
3255 relemhead (PS * ps, const char * name, int fp, double val)
3256 {
3257 int x, y, len, size;
3258 const char *fmt;
3259 unsigned tmp, e;
3260
3261 if (ps->reports < 0)
3262 {
3263 x = ps->RCOUNT & 1;
3264 y = (ps->RCOUNT / 2) * 12 + x * 6;
3265
3266 if (ps->RCOUNT == 1)
3267 sprintf (ps->rline[1], "%6s", "");
3268
3269 len = strlen (name);
3270 while (ps->szrline <= len + y + 1)
3271 {
3272 size = ps->szrline ? 2 * ps->szrline : 128;
3273 ps->rline[0] = resize (ps, ps->rline[0], ps->szrline, size);
3274 ps->rline[1] = resize (ps, ps->rline[1], ps->szrline, size);
3275 ps->szrline = size;
3276 }
3277
3278 fmt = (len <= 6) ? "%6s%10s" : "%-10s%4s";
3279 sprintf (ps->rline[x] + y, fmt, name, "");
3280 }
3281 else if (val < 0)
3282 {
3283 assert (fp);
3284
3285 if (val > -100 && (tmp = val * 10.0 - 0.5) > -1000.0)
3286 {
3287 fprintf (ps->out, "-%4.1f ", -tmp / 10.0);
3288 }
3289 else
3290 {
3291 tmp = -val / 10.0 + 0.5;
3292 e = 1;
3293 while (tmp >= 100)
3294 {
3295 tmp /= 10;
3296 e++;
3297 }
3298
3299 fprintf (ps->out, "-%2ue%u ", tmp, e);
3300 }
3301 }
3302 else
3303 {
3304 if (fp && val < 1000 && (tmp = val * 10.0 + 0.5) < 10000)
3305 {
3306 fprintf (ps->out, "%5.1f ", tmp / 10.0);
3307 }
3308 else if (!fp && (tmp = val) < 100000)
3309 {
3310 fprintf (ps->out, "%5u ", tmp);
3311 }
3312 else
3313 {
3314 tmp = val / 10.0 + 0.5;
3315 e = 1;
3316
3317 while (tmp >= 1000)
3318 {
3319 tmp /= 10;
3320 e++;
3321 }
3322
3323 fprintf (ps->out, "%3ue%u ", tmp, e);
3324 }
3325 }
3326
3327 ps->RCOUNT++;
3328 }
3329
3330 inline static void
3331 relem (PS * ps, const char *name, int fp, double val)
3332 {
3333 if (name)
3334 relemhead (ps, name, fp, val);
3335 else
3336 relemdata (ps);
3337 }
3338
3339 static unsigned
3340 reduce_limit_on_lclauses (PS * ps)
3341 {
3342 unsigned res = ps->lreduce;
3343 res += ps->llocked;
3344 return res;
3345 }
3346
3347 static void
3348 report (PS * ps, int replevel, char type)
3349 {
3350 int rounds;
3351
3352 #ifdef RCODE
3353 (void) type;
3354 #endif
3355
3356 if (ps->verbosity < replevel)
3357 return;
3358
3359 sflush (ps);
3360
3361 if (!ps->reports)
3362 ps->reports = -1;
3363
3364 for (rounds = (ps->reports < 0) ? 2 : 1; rounds; rounds--)
3365 {
3366 if (ps->reports >= 0)
3367 fprintf (ps->out, "%s%c ", ps->prefix, type);
3368
3369 relem (ps, "seconds", 1, ps->seconds);
3370 relem (ps, "level", 1, avglevel (ps));
3371 assert (ps->fixed <= ps->max_var);
3372 relem (ps, "variables", 0, ps->max_var - ps->fixed);
3373 relem (ps, "used", 1, PERCENT (ps->vused, ps->max_var));
3374 relem (ps, "original", 0, ps->noclauses);
3375 relem (ps, "conflicts", 0, ps->conflicts);
3376 // relem (ps, "decisions", 0, ps->decisions);
3377 // relem (ps, "conf/dec", 1, PERCENT(ps->conflicts,ps->decisions));
3378 // relem (ps, "limit", 0, reduce_limit_on_lclauses (ps));
3379 relem (ps, "learned", 0, ps->nlclauses);
3380 // relem (ps, "limit", 1, PERCENT (ps->nlclauses, reduce_limit_on_lclauses (ps)));
3381 relem (ps, "limit", 0, ps->lreduce);
3382 #ifdef STATS
3383 relem (ps, "learning", 1, PERCENT (ps->llused, ps->lladded));
3384 #endif
3385 relem (ps, "agility", 1, dynamic_flips_per_assignment_per_mille (ps) / 10.0);
3386 // relem (ps, "original", 0, ps->noclauses);
3387 relem (ps, "MB", 1, mb (ps));
3388 // relem (ps, "lladded", 0, ps->lladded);
3389 // relem (ps, "llused", 0, ps->llused);
3390
3391 relem (ps, 0, 0, 0);
3392
3393 ps->reports++;
3394 }
3395
3396 /* Adapt this to the number of rows in your terminal.
3397 */
3398 #define ROWS 25
3399
3400 if (ps->reports % (ROWS - 3) == (ROWS - 4))
3401 rheader (ps);
3402
3403 fflush (ps->out);
3404 }
3405
3406 static int
3407 bcp_queue_is_empty (PS * ps)
3408 {
3409 if (ps->ttail != ps->thead)
3410 return 0;
3411
3412 if (ps->ttail2 != ps->thead)
3413 return 0;
3414
3415 #ifndef NADC
3416 if (ps->ttailado != ps->thead)
3417 return 0;
3418 #endif
3419
3420 return 1;
3421 }
3422
3423 static int
3424 satisfied (PS * ps)
3425 {
3426 assert (!ps->mtcls);
3427 assert (!ps->failed_assumption);
3428 if (ps->alstail < ps->alshead)
3429 return 0;
3430 assert (!ps->conflict);
3431 assert (bcp_queue_is_empty (ps));
3432 return ps->thead == ps->trail + ps->max_var; /* all assigned */
3433 }
3434
3435 static void
3436 vrescore (PS * ps)
3437 {
3438 Rnk *p, *eor = ps->rnks + ps->max_var;
3439 for (p = ps->rnks + 1; p <= eor; p++)
3440 if (p->score != INFFLT)
3441 p->score = mulflt (p->score, ps->ilvinc);
3442 ps->vinc = mulflt (ps->vinc, ps->ilvinc);;
3443 #ifdef VISCORES
3444 ps->nvinc = mulflt (ps->nvinc, ps->lscore);;
3445 #endif
3446 }
3447
3448 static void
3449 inc_score (PS * ps, Var * v)
3450 {
3451 Flt score;
3452 Rnk *r;
3453
3454 #ifndef NFL
3455 if (ps->simplifying)
3456 return;
3457 #endif
3458
3459 if (!v->level)
3460 return;
3461
3462 if (v->internal)
3463 return;
3464
3465 r = VAR2RNK (v);
3466 score = r->score;
3467
3468 assert (score != INFFLT);
3469
3470 score = addflt (score, ps->vinc);
3471 assert (score < INFFLT);
3472 r->score = score;
3473 if (r->pos > 0)
3474 hup (ps, r);
3475
3476 if (score > ps->lscore)
3477 vrescore (ps);
3478 }
3479
3480 static void
3481 inc_activity (PS * ps, Cls * c)
3482 {
3483 Act *p;
3484
3485 if (!c->learned)
3486 return;
3487
3488 if (c->size <= 2)
3489 return;
3490
3491 p = CLS2ACT (c);
3492 *p = addflt (*p, ps->cinc);
3493 }
3494
3495 static unsigned
3496 hashlevel (unsigned l)
3497 {
3498 return 1u << (l & 31);
3499 }
3500
3501 static void
3502 push (PS * ps, Var * v)
3503 {
3504 if (ps->dhead == ps->eod)
3505 ENLARGE (ps->dfs, ps->dhead, ps->eod);
3506
3507 *ps->dhead++ = v;
3508 }
3509
3510 static Var *
3511 pop (PS * ps)
3512 {
3513 assert (ps->dfs < ps->dhead);
3514 return *--ps->dhead;
3515 }
3516
3517 static void
3518 analyze (PS * ps)
3519 {
3520 unsigned open, minlevel, siglevels, l, old, i, orig;
3521 Lit *this, *other, **p, **q, **eol;
3522 Var *v, *u, **m, *start, *uip;
3523 Cls *c;
3524
3525 assert (ps->conflict);
3526
3527 assert (ps->ahead == ps->added);
3528 assert (ps->mhead == ps->marked);
3529 assert (ps->rhead == ps->resolved);
3530
3531 /* First, search for First UIP variable and mark all resolved variables.
3532 * At the same time determine the minimum decision level involved.
3533 * Increase activities of resolved variables.
3534 */
3535 q = ps->thead;
3536 open = 0;
3537 minlevel = ps->LEVEL;
3538 siglevels = 0;
3539 uip = 0;
3540
3541 c = ps->conflict;
3542
3543 for (;;)
3544 {
3545 add_antecedent (ps, c);
3546 inc_activity (ps, c);
3547 eol = end_of_lits (c);
3548 for (p = c->lits; p < eol; p++)
3549 {
3550 other = *p;
3551
3552 if (other->val == TRUE)
3553 continue;
3554
3555 assert (other->val == FALSE);
3556
3557 u = LIT2VAR (other);
3558 if (u->mark)
3559 continue;
3560
3561 u->mark = 1;
3562 inc_score (ps, u);
3563 use_var (ps, u);
3564
3565 if (u->level == ps->LEVEL)
3566 {
3567 open++;
3568 }
3569 else
3570 {
3571 push_var_as_marked (ps, u);
3572
3573 if (u->level)
3574 {
3575 /* The statistics counter 'nonminimizedllits' sums up the
3576 * number of literals that would be added if only the
3577 * 'first UIP' scheme for learned clauses would be used
3578 * and no clause minimization.
3579 */
3580 ps->nonminimizedllits++;
3581
3582 if (u->level < minlevel)
3583 minlevel = u->level;
3584
3585 siglevels |= hashlevel (u->level);
3586 }
3587 else
3588 {
3589 assert (!u->level);
3590 assert (u->reason);
3591 }
3592 }
3593 }
3594
3595 do
3596 {
3597 if (q == ps->trail)
3598 {
3599 uip = 0;
3600 goto DONE_FIRST_UIP;
3601 }
3602
3603 this = *--q;
3604 uip = LIT2VAR (this);
3605 }
3606 while (!uip->mark);
3607
3608 uip->mark = 0;
3609
3610 c = var2reason (ps, uip);
3611 #ifdef NO_BINARY_CLAUSES
3612 if (c == &ps->impl)
3613 resetimpl (ps);
3614 #endif
3615 open--;
3616 if ((!open && ps->LEVEL) || !c)
3617 break;
3618
3619 assert (c);
3620 }
3621
3622 DONE_FIRST_UIP:
3623
3624 if (uip)
3625 {
3626 assert (ps->LEVEL);
3627 this = VAR2LIT (uip);
3628 this += (this->val == TRUE);
3629 ps->nonminimizedllits++;
3630 ps->minimizedllits++;
3631 add_lit (ps, this);
3632 #ifdef STATS
3633 if (uip->reason)
3634 ps->uips++;
3635 #endif
3636 }
3637 else
3638 assert (!ps->LEVEL);
3639
3640 /* Second, try to mark more intermediate variables, with the goal to
3641 * minimize the conflict clause. This is a DFS from already marked
3642 * variables backward through the implication graph. It tries to reach
3643 * other marked variables. If the search reaches an unmarked decision
3644 * variable or a variable assigned below the minimum level of variables in
3645 * the first uip learned clause or a level on which no variable has been
3646 * marked, then the variable from which the DFS is started is not
3647 * redundant. Otherwise the start variable is redundant and will
3648 * eventually be removed from the learned clause in step 4. We initially
3649 * implemented BFS, but then profiling revelead that this step is a bottle
3650 * neck for certain incremental applications. After switching to DFS this
3651 * hot spot went away.
3652 */
3653 orig = ps->mhead - ps->marked;
3654 for (i = 0; i < orig; i++)
3655 {
3656 start = ps->marked[i];
3657
3658 assert (start->mark);
3659 assert (start != uip);
3660 assert (start->level < ps->LEVEL);
3661
3662 if (!start->reason)
3663 continue;
3664
3665 old = ps->mhead - ps->marked;
3666 assert (ps->dhead == ps->dfs);
3667 push (ps, start);
3668
3669 while (ps->dhead > ps->dfs)
3670 {
3671 u = pop (ps);
3672 assert (u->mark);
3673
3674 c = var2reason (ps, u);
3675 #ifdef NO_BINARY_CLAUSES
3676 if (c == &ps->impl)
3677 resetimpl (ps);
3678 #endif
3679 if (!c ||
3680 ((l = u->level) &&
3681 (l < minlevel || ((hashlevel (l) & ~siglevels)))))
3682 {
3683 while (ps->mhead > ps->marked + old) /* reset all marked */
3684 (*--ps->mhead)->mark = 0;
3685
3686 ps->dhead = ps->dfs; /* and DFS stack */
3687 break;
3688 }
3689
3690 eol = end_of_lits (c);
3691 for (p = c->lits; p < eol; p++)
3692 {
3693 v = LIT2VAR (*p);
3694 if (v->mark)
3695 continue;
3696
3697 mark_var (ps, v);
3698 push (ps, v);
3699 }
3700 }
3701 }
3702
3703 for (m = ps->marked; m < ps->mhead; m++)
3704 {
3705 v = *m;
3706
3707 assert (v->mark);
3708 assert (!v->resolved);
3709
3710 use_var (ps, v);
3711
3712 c = var2reason (ps, v);
3713 if (!c)
3714 continue;
3715
3716 #ifdef NO_BINARY_CLAUSES
3717 if (c == &ps->impl)
3718 resetimpl (ps);
3719 #endif
3720 eol = end_of_lits (c);
3721 for (p = c->lits; p < eol; p++)
3722 {
3723 other = *p;
3724
3725 u = LIT2VAR (other);
3726 if (!u->level)
3727 continue;
3728
3729 if (!u->mark) /* 'MARKTEST' */
3730 break;
3731 }
3732
3733 if (p != eol)
3734 continue;
3735
3736 add_antecedent (ps, c);
3737 v->resolved = 1;
3738 }
3739
3740 for (m = ps->marked; m < ps->mhead; m++)
3741 {
3742 v = *m;
3743
3744 assert (v->mark);
3745 v->mark = 0;
3746
3747 if (v->resolved)
3748 {
3749 v->resolved = 0;
3750 continue;
3751 }
3752
3753 this = VAR2LIT (v);
3754 if (this->val == TRUE)
3755 this++; /* actually NOTLIT */
3756
3757 add_lit (ps, this);
3758 ps->minimizedllits++;
3759 }
3760
3761 assert (ps->ahead <= ps->eoa);
3762 assert (ps->rhead <= ps->eor);
3763
3764 ps->mhead = ps->marked;
3765 }
3766
3767 static void
3768 fanalyze (PS * ps)
3769 {
3770 Lit ** eol, ** p, * lit;
3771 Cls * c, * reason;
3772 Var * v, * u;
3773 int next;
3774
3775 #ifndef RCODE
3776 double start = picosat_time_stamp ();
3777 #endif
3778
3779 assert (ps->failed_assumption);
3780 assert (ps->failed_assumption->val == FALSE);
3781
3782 v = LIT2VAR (ps->failed_assumption);
3783 reason = var2reason (ps, v);
3784 if (!reason) return;
3785 #ifdef NO_BINARY_CLAUSES
3786 if (reason == &ps->impl)
3787 resetimpl (ps);
3788 #endif
3789
3790 eol = end_of_lits (reason);
3791 for (p = reason->lits; p != eol; p++)
3792 {
3793 lit = *p;
3794 u = LIT2VAR (lit);
3795 if (u == v) continue;
3796 if (u->reason) break;
3797 }
3798 if (p == eol) return;
3799
3800 assert (ps->ahead == ps->added);
3801 assert (ps->mhead == ps->marked);
3802 assert (ps->rhead == ps->resolved);
3803
3804 next = 0;
3805 mark_var (ps, v);
3806 add_lit (ps, NOTLIT (ps->failed_assumption));
3807
3808 do
3809 {
3810 v = ps->marked[next++];
3811 use_var (ps, v);
3812 if (v->reason)
3813 {
3814 reason = var2reason (ps, v);
3815 #ifdef NO_BINARY_CLAUSES
3816 if (reason == &ps->impl)
3817 resetimpl (ps);
3818 #endif
3819 add_antecedent (ps, reason);
3820 eol = end_of_lits (reason);
3821 for (p = reason->lits; p != eol; p++)
3822 {
3823 lit = *p;
3824 u = LIT2VAR (lit);
3825 if (u == v) continue;
3826 if (u->mark) continue;
3827 mark_var (ps, u);
3828 }
3829 }
3830 else
3831 {
3832 lit = VAR2LIT (v);
3833 if (lit->val == TRUE) lit = NOTLIT (lit);
3834 add_lit (ps, lit);
3835 }
3836 }
3837 while (ps->marked + next < ps->mhead);
3838
3839 c = add_simplified_clause (ps, 1);
3840 v = LIT2VAR (ps->failed_assumption);
3841 reason = v->reason;
3842 #ifdef NO_BINARY_CLAUSES
3843 if (!ISLITREASON (reason))
3844 #endif
3845 {
3846 assert (reason->locked);
3847 reason->locked = 0;
3848 if (reason->learned && reason->size > 2)
3849 {
3850 assert (ps->llocked > 0);
3851 ps->llocked--;
3852 }
3853 }
3854
3855 #ifdef NO_BINARY_CLAUSES
3856 if (c == &ps->impl)
3857 {
3858 c = impl2reason (ps, NOTLIT (ps->failed_assumption));
3859 }
3860 else
3861 #endif
3862 {
3863 assert (c->learned);
3864 assert (!c->locked);
3865 c->locked = 1;
3866 if (c->size > 2)
3867 {
3868 ps->llocked++;
3869 assert (ps->llocked > 0);
3870 }
3871 }
3872
3873 v->reason = c;
3874
3875 while (ps->mhead > ps->marked)
3876 (*--ps->mhead)->mark = 0;
3877
3878 if (ps->verbosity)
3879 fprintf (ps->out, "%sfanalyze took %.1f seconds\n",
3880 ps->prefix, picosat_time_stamp () - start);
3881 }
3882
3883 /* Propagate assignment of 'this' to 'FALSE' by visiting all binary clauses in
3884 * which 'this' occurs.
3885 */
3886 inline static void
3887 prop2 (PS * ps, Lit * this)
3888 {
3889 #ifdef NO_BINARY_CLAUSES
3890 Lit ** l, ** start;
3891 Ltk * lstk;
3892 #else
3893 Cls * c, ** p;
3894 Cls * next;
3895 #endif
3896 Lit * other;
3897 Val tmp;
3898
3899 assert (this->val == FALSE);
3900
3901 #ifdef NO_BINARY_CLAUSES
3902 lstk = LIT2IMPLS (this);
3903 start = lstk->start;
3904 l = start + lstk->count;
3905 while (l != start)
3906 {
3907 /* The counter 'visits' is the number of clauses that are
3908 * visited during propagations of assignments.
3909 */
3910 ps->visits++;
3911 #ifdef STATS
3912 ps->bvisits++;
3913 #endif
3914 other = *--l;
3915 tmp = other->val;
3916
3917 if (tmp == TRUE)
3918 {
3919 #ifdef STATS
3920 ps->othertrue++;
3921 ps->othertrue2++;
3922 if (LIT2VAR (other)->level < ps->LEVEL)
3923 ps->othertrue2u++;
3924 #endif
3925 continue;
3926 }
3927
3928 if (tmp != FALSE)
3929 {
3930 assign_forced (ps, other, LIT2REASON (NOTLIT(this)));
3931 continue;
3932 }
3933
3934 if (ps->conflict == &ps->cimpl)
3935 resetcimpl (ps);
3936 ps->conflict = setcimpl (ps, this, other);
3937 }
3938 #else
3939 /* Traverse all binary clauses with 'this'. Head/Tail pointers for binary
3940 * clauses do not have to be modified here.
3941 */
3942 p = LIT2IMPLS (this);
3943 for (c = *p; c; c = next)
3944 {
3945 ps->visits++;
3946 #ifdef STATS
3947 ps->bvisits++;
3948 #endif
3949 assert (!c->collect);
3950 #ifdef TRACE
3951 assert (!c->collected);
3952 #endif
3953 assert (c->size == 2);
3954
3955 other = c->lits[0];
3956 if (other == this)
3957 {
3958 next = c->next[0];
3959 other = c->lits[1];
3960 }
3961 else
3962 next = c->next[1];
3963
3964 tmp = other->val;
3965
3966 if (tmp == TRUE)
3967 {
3968 #ifdef STATS
3969 ps->othertrue++;
3970 ps->othertrue2++;
3971 if (LIT2VAR (other)->level < ps->LEVEL)
3972 ps->othertrue2u++;
3973 #endif
3974 continue;
3975 }
3976
3977 if (tmp == FALSE)
3978 ps->conflict = c;
3979 else
3980 assign_forced (ps, other, c); /* unit clause */
3981 }
3982 #endif /* !defined(NO_BINARY_CLAUSES) */
3983 }
3984
3985 #ifndef NDSC
3986 static int
3987 should_disconnect_head_tail (PS * ps, Lit * lit)
3988 {
3989 unsigned litlevel;
3990 Var * v;
3991
3992 assert (lit->val == TRUE);
3993
3994 v = LIT2VAR (lit);
3995 litlevel = v->level;
3996
3997 if (!litlevel)
3998 return 1;
3999
4000 #ifndef NFL
4001 if (ps->simplifying)
4002 return 0;
4003 #endif
4004
4005 return litlevel < ps->LEVEL;
4006 }
4007 #endif
4008
4009 inline static void
4010 propl (PS * ps, Lit * this)
4011 {
4012 Lit **l, *other, *prev, *new_lit, **eol;
4013 Cls *next, **htp_ptr, **new_htp_ptr;
4014 Cls *c;
4015 #ifdef STATS
4016 unsigned size;
4017 #endif
4018
4019 htp_ptr = LIT2HTPS (this);
4020 assert (this->val == FALSE);
4021
4022 /* Traverse all non binary clauses with 'this'. Head/Tail pointers are
4023 * updated as well.
4024 */
4025 for (c = *htp_ptr; c; c = next)
4026 {
4027 ps->visits++;
4028 #ifdef STATS
4029 size = c->size;
4030 assert (size >= 3);
4031 ps->traversals++; /* other is dereferenced at least */
4032
4033 if (size == 3)
4034 ps->tvisits++;
4035 else if (size >= 4)
4036 {
4037 ps->lvisits++;
4038 ps->ltraversals++;
4039 }
4040 #endif
4041 #ifdef TRACE
4042 assert (!c->collected);
4043 #endif
4044 assert (c->size > 0);
4045
4046 other = c->lits[0];
4047 if (other != this)
4048 {
4049 assert (c->size != 1);
4050 c->lits[0] = this;
4051 c->lits[1] = other;
4052 next = c->next[1];
4053 c->next[1] = c->next[0];
4054 c->next[0] = next;
4055 }
4056 else if (c->size == 1) /* With assumptions we need to
4057 * traverse unit clauses as well.
4058 */
4059 {
4060 assert (!ps->conflict);
4061 ps->conflict = c;
4062 break;
4063 }
4064 else
4065 {
4066 assert (other == this && c->size > 1);
4067 other = c->lits[1];
4068 next = c->next[0];
4069 }
4070 assert (other == c->lits[1]);
4071 assert (this == c->lits[0]);
4072 assert (next == c->next[0]);
4073 assert (!c->collect);
4074
4075 if (other->val == TRUE)
4076 {
4077 #ifdef STATS
4078 ps->othertrue++;
4079 ps->othertruel++;
4080 #endif
4081 #ifndef NDSC
4082 if (should_disconnect_head_tail (ps, other))
4083 {
4084 new_htp_ptr = LIT2DHTPS (other);
4085 c->next[0] = *new_htp_ptr;
4086 *new_htp_ptr = c;
4087 #ifdef STATS
4088 ps->othertruelu++;
4089 #endif
4090 *htp_ptr = next;
4091 continue;
4092 }
4093 #endif
4094 htp_ptr = c->next;
4095 continue;
4096 }
4097
4098 l = c->lits + 1;
4099 eol = (Lit**) c->lits + c->size;
4100 prev = this;
4101
4102 while (++l != eol)
4103 {
4104 #ifdef STATS
4105 if (size >= 3)
4106 {
4107 ps->traversals++;
4108 if (size > 3)
4109 ps->ltraversals++;
4110 }
4111 #endif
4112 new_lit = *l;
4113 *l = prev;
4114 prev = new_lit;
4115 if (new_lit->val != FALSE) break;
4116 }
4117
4118 if (l == eol)
4119 {
4120 while (l > c->lits + 2)
4121 {
4122 new_lit = *--l;
4123 *l = prev;
4124 prev = new_lit;
4125 }
4126 assert (c->lits[0] == this);
4127
4128 assert (other == c->lits[1]);
4129 if (other->val == FALSE) /* found conflict */
4130 {
4131 assert (!ps->conflict);
4132 ps->conflict = c;
4133 return;
4134 }
4135
4136 assign_forced (ps, other, c); /* unit clause */
4137 htp_ptr = c->next;
4138 }
4139 else
4140 {
4141 assert (new_lit->val == TRUE || new_lit->val == UNDEF);
4142 c->lits[0] = new_lit;
4143 // *l = this;
4144 new_htp_ptr = LIT2HTPS (new_lit);
4145 c->next[0] = *new_htp_ptr;
4146 *new_htp_ptr = c;
4147 *htp_ptr = next;
4148 }
4149 }
4150 }
4151
4152 #ifndef NADC
4153
4154 static unsigned primes[] = { 996293, 330643, 753947, 500873 };
4155
4156 #define PRIMES ((sizeof primes)/sizeof *primes)
4157
4158 static unsigned
4159 hash_ado (PS * ps, Lit ** ado, unsigned salt)
4160 {
4161 unsigned i, res, tmp;
4162 Lit ** p, * lit;
4163
4164 assert (salt < PRIMES);
4165
4166 i = salt;
4167 res = 0;
4168
4169 for (p = ado; (lit = *p); p++)
4170 {
4171 assert (lit->val);
4172
4173 tmp = res >> 31;
4174 res <<= 1;
4175
4176 if (lit->val > 0)
4177 res |= 1;
4178
4179 assert (i < PRIMES);
4180 res *= primes[i++];
4181 if (i == PRIMES)
4182 i = 0;
4183
4184 res += tmp;
4185 }
4186
4187 return res & (ps->szadotab - 1);
4188 }
4189
4190 static unsigned
4191 cmp_ado (Lit ** a, Lit ** b)
4192 {
4193 Lit ** p, ** q, * l, * k;
4194 int res;
4195
4196 for (p = a, q = b; (l = *p); p++, q++)
4197 {
4198 k = *q;
4199 assert (k);
4200 if ((res = (l->val - k->val)))
4201 return res;
4202 }
4203
4204 assert (!*q);
4205
4206 return 0;
4207 }
4208
4209 static Lit ***
4210 find_ado (PS * ps, Lit ** ado)
4211 {
4212 Lit *** res, ** other;
4213 unsigned pos, delta;
4214
4215 pos = hash_ado (ps, ado, 0);
4216 assert (pos < ps->szadotab);
4217 res = ps->adotab + pos;
4218
4219 other = *res;
4220 if (!other || !cmp_ado (other, ado))
4221 return res;
4222
4223 delta = hash_ado (ps, ado, 1);
4224 if (!(delta & 1))
4225 delta++;
4226
4227 assert (delta & 1);
4228 assert (delta < ps->szadotab);
4229
4230 for (;;)
4231 {
4232 pos += delta;
4233 if (pos >= ps->szadotab)
4234 pos -= ps->szadotab;
4235
4236 assert (pos < ps->szadotab);
4237 res = ps->adotab + pos;
4238 other = *res;
4239 if (!other || !cmp_ado (other, ado))
4240 return res;
4241 }
4242 }
4243
4244 static void
4245 enlarge_adotab (PS * ps)
4246 {
4247 /* TODO make this generic */
4248
4249 ABORTIF (ps->szadotab,
4250 "internal: all different objects table needs larger initial size");
4251 assert (!ps->nadotab);
4252 ps->szadotab = 10000;
4253 NEWN (ps->adotab, ps->szadotab);
4254 CLRN (ps->adotab, ps->szadotab);
4255 }
4256
4257 static int
4258 propado (PS * ps, Var * v)
4259 {
4260 Lit ** p, ** q, *** adotabpos, **ado, * lit;
4261 Var * u;
4262
4263 if (ps->LEVEL && ps->adodisabled)
4264 return 1;
4265
4266 assert (!ps->conflict);
4267 assert (!ps->adoconflict);
4268 assert (VAR2LIT (v)->val != UNDEF);
4269 assert (!v->adotabpos);
4270
4271 if (!v->ado)
4272 return 1;
4273
4274 assert (v->inado);
4275
4276 for (p = v->ado; (lit = *p); p++)
4277 if (lit->val == UNDEF)
4278 {
4279 u = LIT2VAR (lit);
4280 assert (!u->ado);
4281 u->ado = v->ado;
4282 v->ado = 0;
4283
4284 return 1;
4285 }
4286
4287 if (4 * ps->nadotab >= 3 * ps->szadotab) /* at least 75% filled */
4288 enlarge_adotab (ps);
4289
4290 adotabpos = find_ado (ps, v->ado);
4291 ado = *adotabpos;
4292
4293 if (!ado)
4294 {
4295 ps->nadotab++;
4296 v->adotabpos = adotabpos;
4297 *adotabpos = v->ado;
4298 return 1;
4299 }
4300
4301 assert (ado != v->ado);
4302
4303 ps->adoconflict = new_clause (ps, 2 * llength (ado), 1);
4304 q = ps->adoconflict->lits;
4305
4306 for (p = ado; (lit = *p); p++)
4307 *q++ = lit->val == FALSE ? lit : NOTLIT (lit);
4308
4309 for (p = v->ado; (lit = *p); p++)
4310 *q++ = lit->val == FALSE ? lit : NOTLIT (lit);
4311
4312 assert (q == ENDOFCLS (ps->adoconflict));
4313 ps->conflict = ps->adoconflict;
4314 ps->adoconflicts++;
4315 return 0;
4316 }
4317
4318 #endif
4319
4320 static void
4321 bcp (PS * ps)
4322 {
4323 int props = 0;
4324 assert (!ps->conflict);
4325
4326 if (ps->mtcls)
4327 return;
4328
4329 for (;;)
4330 {
4331 if (ps->ttail2 < ps->thead) /* prioritize implications */
4332 {
4333 props++;
4334 prop2 (ps, NOTLIT (*ps->ttail2++));
4335 }
4336 else if (ps->ttail < ps->thead) /* unit clauses or clauses with length > 2 */
4337 {
4338 if (ps->conflict) break;
4339 propl (ps, NOTLIT (*ps->ttail++));
4340 if (ps->conflict) break;
4341 }
4342 #ifndef NADC
4343 else if (ps->ttailado < ps->thead)
4344 {
4345 if (ps->conflict) break;
4346 propado (ps, LIT2VAR (*ps->ttailado++));
4347 if (ps->conflict) break;
4348 }
4349 #endif
4350 else
4351 break; /* all assignments propagated, so break */
4352 }
4353
4354 ps->propagations += props;
4355 }
4356
4357 static unsigned
4358 drive (PS * ps)
4359 {
4360 unsigned res, vlevel;
4361 Lit **p;
4362 Var *v;
4363
4364 res = 0;
4365 for (p = ps->added; p < ps->ahead; p++)
4366 {
4367 v = LIT2VAR (*p);
4368 vlevel = v->level;
4369 assert (vlevel <= ps->LEVEL);
4370 if (vlevel < ps->LEVEL && vlevel > res)
4371 res = vlevel;
4372 }
4373
4374 return res;
4375 }
4376
4377 #ifdef VISCORES
4378
4379 static void
4380 viscores (PS * ps)
4381 {
4382 Rnk *p, *eor = ps->rnks + ps->max_var;
4383 char name[100], cmd[200];
4384 FILE * data;
4385 Flt s;
4386 int i;
4387
4388 for (p = ps->rnks + 1; p <= ps->eor; p++)
4389 {
4390 s = p->score;
4391 if (s == INFFLT)
4392 continue;
4393 s = mulflt (s, ps->nvinc);
4394 assert (flt2double (s) <= 1.0);
4395 }
4396
4397 sprintf (name, "/tmp/picosat-viscores/data/%08u", ps->conflicts);
4398 sprintf (cmd, "sort -n|nl>%s", name);
4399
4400 data = popen (cmd, "w");
4401 for (p = ps->rnks + 1; p <= ps->eor; p++)
4402 {
4403 s = p->score;
4404 if (s == INFFLT)
4405 continue;
4406 s = mulflt (s, ps->nvinc);
4407 fprintf (data, "%lf %d\n", 100.0 * flt2double (s), (int)(p - ps->rnks));
4408 }
4409 fflush (data);
4410 pclose (data);
4411
4412 for (i = 0; i < 8; i++)
4413 {
4414 sprintf (cmd, "awk '$3%%8==%d' %s>%s.%d", i, name, name, i);
4415 system (cmd);
4416 }
4417
4418 fprintf (ps->fviscores, "set title \"%u\"\n", ps->conflicts);
4419 fprintf (ps->fviscores, "plot [0:%u] 0, 100 * (1 - 1/1.1), 100", ps->max_var);
4420
4421 for (i = 0; i < 8; i++)
4422 fprintf (ps->fviscores,
4423 ", \"%s.%d\" using 1:2:3 with labels tc lt %d",
4424 name, i, i + 1);
4425
4426 fputc ('\n', ps->fviscores);
4427 fflush (ps->fviscores);
4428 #ifndef WRITEGIF
4429 usleep (50000); /* refresh rate of 20 Hz */
4430 #endif
4431 }
4432
4433 #endif
4434
4435 static void
4436 crescore (PS * ps)
4437 {
4438 Cls **p, *c;
4439 Act *a;
4440 Flt factor;
4441 int l = log2flt (ps->cinc);
4442 assert (l > 0);
4443 factor = base2flt (1, -l);
4444
4445 for (p = ps->lclauses; p != ps->lhead; p++)
4446 {
4447 c = *p;
4448
4449 if (!c)
4450 continue;
4451
4452 #ifdef TRACE
4453 if (c->collected)
4454 continue;
4455 #endif
4456 assert (c->learned);
4457
4458 if (c->size <= 2)
4459 continue;
4460
4461 a = CLS2ACT (c);
4462 *a = mulflt (*a, factor);
4463 }
4464
4465 ps->cinc = mulflt (ps->cinc, factor);
4466 }
4467
4468 static void
4469 inc_vinc (PS * ps)
4470 {
4471 #ifdef VISCORES
4472 ps->nvinc = mulflt (ps->nvinc, ps->fvinc);
4473 #endif
4474 ps->vinc = mulflt (ps->vinc, ps->ifvinc);
4475 }
4476
4477 inline static void
4478 inc_max_var (PS * ps)
4479 {
4480 Lit *lit;
4481 Rnk *r;
4482 Var *v;
4483
4484 assert (ps->max_var < ps->size_vars);
4485
4486 if (ps->max_var + 1 == ps->size_vars)
4487 enlarge (ps, ps->size_vars + 2*(ps->size_vars + 3) / 4); /* +25% */
4488
4489 ps->max_var++; /* new index of variable */
4490 assert (ps->max_var); /* no unsigned overflow */
4491
4492 assert (ps->max_var < ps->size_vars);
4493
4494 lit = ps->lits + 2 * ps->max_var;
4495 lit[0].val = lit[1].val = UNDEF;
4496
4497 memset (ps->htps + 2 * ps->max_var, 0, 2 * sizeof *ps->htps);
4498 #ifndef NDSC
4499 memset (ps->dhtps + 2 * ps->max_var, 0, 2 * sizeof *ps->dhtps);
4500 #endif
4501 memset (ps->impls + 2 * ps->max_var, 0, 2 * sizeof *ps->impls);
4502 memset (ps->jwh + 2 * ps->max_var, 0, 2 * sizeof *ps->jwh);
4503
4504 v = ps->vars + ps->max_var; /* initialize variable components */
4505 CLR (v);
4506
4507 r = ps->rnks + ps->max_var; /* initialize rank */
4508 CLR (r);
4509
4510 hpush (ps, r);
4511 }
4512
4513 static void
4514 force (PS * ps, Cls * c)
4515 {
4516 Lit ** p, ** eol, * lit, * forced;
4517 Cls * reason;
4518
4519 forced = 0;
4520 reason = c;
4521
4522 eol = end_of_lits (c);
4523 for (p = c->lits; p < eol; p++)
4524 {
4525 lit = *p;
4526 if (lit->val == UNDEF)
4527 {
4528 assert (!forced);
4529 forced = lit;
4530 #ifdef NO_BINARY_CLAUSES
4531 if (c == &ps->impl)
4532 reason = LIT2REASON (NOTLIT (p[p == c->lits ? 1 : -1]));
4533 #endif
4534 }
4535 else
4536 assert (lit->val == FALSE);
4537 }
4538
4539 #ifdef NO_BINARY_CLAUSES
4540 if (c == &ps->impl)
4541 resetimpl (ps);
4542 #endif
4543 if (!forced)
4544 return;
4545
4546 assign_forced (ps, forced, reason);
4547 }
4548
4549 static void
4550 inc_lreduce (PS * ps)
4551 {
4552 #ifdef STATS
4553 ps->inclreduces++;
4554 #endif
4555 ps->lreduce *= FREDUCE;
4556 ps->lreduce /= 100;
4557 report (ps, 1, '+');
4558 }
4559
4560 static void
4561 backtrack (PS * ps)
4562 {
4563 unsigned new_level;
4564 Cls * c;
4565
4566 ps->conflicts++;
4567 LOG ( fprintf (ps->out, "%sconflict ", ps->prefix); dumpclsnl (ps, ps->conflict));
4568
4569 analyze (ps);
4570 new_level = drive (ps);
4571 // TODO: why not? assert (new_level != 1 || (ps->ahead - ps->added) == 2);
4572 c = add_simplified_clause (ps, 1);
4573 undo (ps, new_level);
4574 force (ps, c);
4575
4576 if (
4577 #ifndef NFL
4578 !ps->simplifying &&
4579 #endif
4580 !--ps->lreduceadjustcnt)
4581 {
4582 /* With FREDUCE==110 and FREDADJ=121 we stir 'lreduce' to be
4583 * proportional to 'sqrt(conflicts)'. In earlier version we actually
4584 * used 'FREDADJ=150', which results in 'lreduce' to approximate
4585 * 'conflicts^(log(1.1)/log(1.5))' which is close to the fourth root
4586 * of 'conflicts', since log(1.1)/log(1.5)=0.235 (as observed by
4587 * Donald Knuth). The square root is the same we get by a Glucose
4588 * style increase, which simply adds a constant at every reduction.
4589 * This would be way simpler to implement but for now we keep the more
4590 * complicated code using the adjust increments and counters.
4591 */
4592 ps->lreduceadjustinc *= FREDADJ; ps->lreduceadjustinc /= 100; ps->lreduceadjustcnt
4593 = ps->lreduceadjustinc;
4594 inc_lreduce (ps);
4595 }
4596
4597 if (ps->verbosity >= 4 && !(ps->conflicts % 1000))
4598 report (ps, 4, 'C');
4599 }
4600
4601 static void
4602 inc_cinc (PS * ps)
4603 {
4604 ps->cinc = mulflt (ps->cinc, ps->fcinc);
4605 if (ps->lcinc < ps->cinc)
4606 crescore (ps);
4607 }
4608
4609 static void
4610 incincs (PS * ps)
4611 {
4612 inc_vinc (ps);
4613 inc_cinc (ps);
4614 #ifdef VISCORES
4615 viscores (ps);
4616 #endif
4617 }
4618
4619 static void
4620 disconnect_clause (PS * ps, Cls * c)
4621 {
4622 assert (c->connected);
4623
4624 if (c->size > 2)
4625 {
4626 if (c->learned)
4627 {
4628 assert (ps->nlclauses > 0);
4629 ps->nlclauses--;
4630
4631 assert (ps->llits >= c->size);
4632 ps->llits -= c->size;
4633 }
4634 else
4635 {
4636 assert (ps->noclauses > 0);
4637 ps->noclauses--;
4638
4639 assert (ps->olits >= c->size);
4640 ps->olits -= c->size;
4641 }
4642 }
4643
4644 #ifndef NDEBUG
4645 c->connected = 0;
4646 #endif
4647 }
4648
4649 static int
4650 clause_is_toplevel_satisfied (PS * ps, Cls * c)
4651 {
4652 Lit *lit, **p, **eol = end_of_lits (c);
4653 Var *v;
4654
4655 for (p = c->lits; p < eol; p++)
4656 {
4657 lit = *p;
4658 if (lit->val == TRUE)
4659 {
4660 v = LIT2VAR (lit);
4661 if (!v->level)
4662 return 1;
4663 }
4664 }
4665
4666 return 0;
4667 }
4668
4669 static int
4670 collect_clause (PS * ps, Cls * c)
4671 {
4672 assert (c->collect);
4673 c->collect = 0;
4674
4675 #ifdef TRACE
4676 assert (!c->collected);
4677 c->collected = 1;
4678 #endif
4679 disconnect_clause (ps, c);
4680
4681 #ifdef TRACE
4682 if (ps->trace && (!c->learned || c->used))
4683 return 0;
4684 #endif
4685 delete_clause (ps, c);
4686
4687 return 1;
4688 }
4689
4690 static size_t
4691 collect_clauses (PS * ps)
4692 {
4693 Cls *c, **p, **q, * next;
4694 Lit * lit, * eol;
4695 size_t res;
4696 int i;
4697
4698 res = ps->current_bytes;
4699
4700 eol = ps->lits + 2 * ps->max_var + 1;
4701 for (lit = ps->lits + 2; lit <= eol; lit++)
4702 {
4703 for (i = 0; i <= 1; i++)
4704 {
4705 if (i)
4706 {
4707 #ifdef NO_BINARY_CLAUSES
4708 Ltk * lstk = LIT2IMPLS (lit);
4709 Lit ** r, ** s;
4710 r = lstk->start;
4711 if (lit->val != TRUE || LIT2VAR (lit)->level)
4712 for (s = r; s < lstk->start + lstk->count; s++)
4713 {
4714 Lit * other = *s;
4715 Var *v = LIT2VAR (other);
4716 if (v->level ||
4717 other->val != TRUE)
4718 *r++ = other;
4719 }
4720 lstk->count = r - lstk->start;
4721 continue;
4722 #else
4723 p = LIT2IMPLS (lit);
4724 #endif
4725 }
4726 else
4727 p = LIT2HTPS (lit);
4728
4729 for (c = *p; c; c = next)
4730 {
4731 q = c->next;
4732 if (c->lits[0] != lit)
4733 q++;
4734
4735 next = *q;
4736 if (c->collect)
4737 *p = next;
4738 else
4739 p = q;
4740 }
4741 }
4742 }
4743
4744 #ifndef NDSC
4745 for (lit = ps->lits + 2; lit <= eol; lit++)
4746 {
4747 p = LIT2DHTPS (lit);
4748 while ((c = *p))
4749 {
4750 Lit * other = c->lits[0];
4751 if (other == lit)
4752 {
4753 q = c->next + 1;
4754 }
4755 else
4756 {
4757 assert (c->lits[1] == lit);
4758 q = c->next;
4759 }
4760
4761 if (c->collect)
4762 *p = *q;
4763 else
4764 p = q;
4765 }
4766 }
4767 #endif
4768
4769 for (p = SOC; p != EOC; p = NXC (p))
4770 {
4771 c = *p;
4772
4773 if (!c)
4774 continue;
4775
4776 if (!c->collect)
4777 continue;
4778
4779 if (collect_clause (ps, c))
4780 *p = 0;
4781 }
4782
4783 #ifdef TRACE
4784 if (!ps->trace)
4785 #endif
4786 {
4787 q = ps->oclauses;
4788 for (p = q; p < ps->ohead; p++)
4789 if ((c = *p))
4790 *q++ = c;
4791 ps->ohead = q;
4792
4793 q = ps->lclauses;
4794 for (p = q; p < ps->lhead; p++)
4795 if ((c = *p))
4796 *q++ = c;
4797 ps->lhead = q;
4798 }
4799
4800 assert (ps->current_bytes <= res);
4801 res -= ps->current_bytes;
4802 ps->recycled += res;
4803
4804 LOG ( fprintf (ps->out, "%scollected %ld bytes\n", ps->prefix, (long)res));
4805
4806 return res;
4807 }
4808
4809 static int
4810 need_to_reduce (PS * ps)
4811 {
4812 return ps->nlclauses >= reduce_limit_on_lclauses (ps);
4813 }
4814
4815 #ifdef NLUBY
4816
4817 static void
4818 inc_drestart (PS * ps)
4819 {
4820 ps->drestart *= FRESTART;
4821 ps->drestart /= 100;
4822
4823 if (ps->drestart >= MAXRESTART)
4824 ps->drestart = MAXRESTART;
4825 }
4826
4827 static void
4828 inc_ddrestart (PS * ps)
4829 {
4830 ps->ddrestart *= FRESTART;
4831 ps->ddrestart /= 100;
4832
4833 if (ps->ddrestart >= MAXRESTART)
4834 ps->ddrestart = MAXRESTART;
4835 }
4836
4837 #else
4838
4839 static unsigned
4840 luby (unsigned i)
4841 {
4842 unsigned k;
4843 for (k = 1; k < 32; k++)
4844 if (i == (1u << k) - 1)
4845 return 1u << (k - 1);
4846
4847 for (k = 1;; k++)
4848 if ((1u << (k - 1)) <= i && i < (1u << k) - 1)
4849 return luby (i - (1u << (k-1)) + 1);
4850 }
4851
4852 #endif
4853
4854 #ifndef NLUBY
4855 static void
4856 inc_lrestart (PS * ps, int skip)
4857 {
4858 unsigned delta;
4859
4860 delta = 100 * luby (++ps->lubycnt);
4861 ps->lrestart = ps->conflicts + delta;
4862
4863 if (ps->waslubymaxdelta)
4864 report (ps, 1, skip ? 'N' : 'R');
4865 else
4866 report (ps, 2, skip ? 'n' : 'r');
4867
4868 if (delta > ps->lubymaxdelta)
4869 {
4870 ps->lubymaxdelta = delta;
4871 ps->waslubymaxdelta = 1;
4872 }
4873 else
4874 ps->waslubymaxdelta = 0;
4875 }
4876 #endif
4877
4878 static void
4879 init_restart (PS * ps)
4880 {
4881 #ifdef NLUBY
4882 /* TODO: why is it better in incremental usage to have smaller initial
4883 * outer restart interval?
4884 */
4885 ps->ddrestart = ps->calls > 1 ? MINRESTART : 1000;
4886 ps->drestart = MINRESTART;
4887 ps->lrestart = ps->conflicts + ps->drestart;
4888 #else
4889 ps->lubycnt = 0;
4890 ps->lubymaxdelta = 0;
4891 ps->waslubymaxdelta = 0;
4892 inc_lrestart (ps, 0);
4893 #endif
4894 }
4895
4896 static void
4897 restart (PS * ps)
4898 {
4899 int skip;
4900 #ifdef NLUBY
4901 char kind;
4902 int outer;
4903
4904 inc_drestart (ps);
4905 outer = (ps->drestart >= ps->ddrestart);
4906
4907 if (outer)
4908 skip = very_high_agility (ps);
4909 else
4910 skip = high_agility (ps);
4911 #else
4912 skip = medium_agility (ps);
4913 #endif
4914
4915 #ifdef STATS
4916 if (skip)
4917 ps->skippedrestarts++;
4918 #endif
4919
4920 assert (ps->conflicts >= ps->lrestart);
4921
4922 if (!skip)
4923 {
4924 ps->restarts++;
4925 assert (ps->LEVEL > 1);
4926 LOG ( fprintf (ps->out, "%srestart %u\n", ps->prefix, ps->restarts));
4927 undo (ps, 0);
4928 }
4929
4930 #ifdef NLUBY
4931 if (outer)
4932 {
4933 kind = skip ? 'N' : 'R';
4934 inc_ddrestart (ps);
4935 ps->drestart = MINRESTART;
4936 }
4937 else if (skip)
4938 {
4939 kind = 'n';
4940 }
4941 else
4942 {
4943 kind = 'r';
4944 }
4945
4946 assert (ps->drestart <= MAXRESTART);
4947 ps->lrestart = ps->conflicts + ps->drestart;
4948 assert (ps->lrestart > ps->conflicts);
4949
4950 report (outer ? 1 : 2, kind);
4951 #else
4952 inc_lrestart (ps, skip);
4953 #endif
4954 }
4955
4956 inline static void
4957 assign_decision (PS * ps, Lit * lit)
4958 {
4959 assert (!ps->conflict);
4960
4961 ps->LEVEL++;
4962
4963 LOG ( fprintf (ps->out, "%snew level %u\n", ps->prefix, ps->LEVEL));
4964 LOG ( fprintf (ps->out,
4965 "%sassign %d at level %d <= DECISION\n",
4966 ps->prefix, LIT2INT (lit), ps->LEVEL));
4967
4968 assign (ps, lit, 0);
4969 }
4970
4971 #ifndef NFL
4972
4973 static int
4974 lit_has_binary_clauses (PS * ps, Lit * lit)
4975 {
4976 #ifdef NO_BINARY_CLAUSES
4977 Ltk* lstk = LIT2IMPLS (lit);
4978 return lstk->count != 0;
4979 #else
4980 return *LIT2IMPLS (lit) != 0;
4981 #endif
4982 }
4983
4984 static void
4985 flbcp (PS * ps)
4986 {
4987 #ifdef STATS
4988 unsigned long long propagaions_before_bcp = ps->propagations;
4989 #endif
4990 bcp (ps);
4991 #ifdef STATS
4992 ps->flprops += ps->propagations - propagaions_before_bcp;
4993 #endif
4994 }
4995
4996 inline static int
4997 cmp_inverse_rnk (PS * ps, Rnk * a, Rnk * b)
4998 {
4999 (void) ps;
5000 return -cmp_rnk (a, b);
5001 }
5002
5003 inline static Flt
5004 rnk2jwh (PS * ps, Rnk * r)
5005 {
5006 Flt res, sum, pjwh, njwh;
5007 Lit * plit, * nlit;
5008
5009 plit = RNK2LIT (r);
5010 nlit = plit + 1;
5011
5012 pjwh = *LIT2JWH (plit);
5013 njwh = *LIT2JWH (nlit);
5014
5015 res = mulflt (pjwh, njwh);
5016
5017 sum = addflt (pjwh, njwh);
5018 sum = mulflt (sum, base2flt (1, -10));
5019 res = addflt (res, sum);
5020
5021 return res;
5022 }
5023
5024 static int
5025 cmp_inverse_jwh_rnk (PS * ps, Rnk * r, Rnk * s)
5026 {
5027 Flt a = rnk2jwh (ps, r);
5028 Flt b = rnk2jwh (ps, s);
5029 int res = cmpflt (a, b);
5030
5031 if (res)
5032 return -res;
5033
5034 return cmp_inverse_rnk (ps, r, s);
5035 }
5036
5037 static void
5038 faillits (PS * ps)
5039 {
5040 unsigned i, j, old_trail_count, common, saved_count;
5041 unsigned new_saved_size, oldladded = ps->ladded;
5042 unsigned long long limit, delta;
5043 Lit * lit, * other, * pivot;
5044 Rnk * r, ** p, ** q;
5045 int new_trail_count;
5046 double started;
5047
5048 if (ps->plain)
5049 return;
5050
5051 if (ps->heap + 1 >= ps->hhead)
5052 return;
5053
5054 if (ps->propagations < ps->fllimit)
5055 return;
5056
5057 sflush (ps);
5058 started = ps->seconds;
5059
5060 ps->flcalls++;
5061 #ifdef STATSA
5062 ps->flrounds++;
5063 #endif
5064 delta = ps->propagations/10;
5065 if (delta >= 100*1000*1000) delta = 100*1000*1000;
5066 else if (delta <= 100*1000) delta = 100*1000;
5067
5068 limit = ps->propagations + delta;
5069 ps->fllimit = ps->propagations;
5070
5071 assert (!ps->LEVEL);
5072 assert (ps->simplifying);
5073
5074 if (ps->flcalls <= 1)
5075 SORT (Rnk *, cmp_inverse_jwh_rnk, ps->heap + 1, ps->hhead - (ps->heap + 1));
5076 else
5077 SORT (Rnk *, cmp_inverse_rnk, ps->heap + 1, ps->hhead - (ps->heap + 1));
5078
5079 i = 1; /* NOTE: heap starts at position '1' */
5080
5081 while (ps->propagations < limit)
5082 {
5083 if (ps->heap + i == ps->hhead)
5084 {
5085 if (ps->ladded == oldladded)
5086 break;
5087
5088 i = 1;
5089 #ifdef STATS
5090 ps->flrounds++;
5091 #endif
5092 oldladded = ps->ladded;
5093 }
5094
5095 assert (ps->heap + i < ps->hhead);
5096
5097 r = ps->heap[i++];
5098 lit = RNK2LIT (r);
5099
5100 if (lit->val)
5101 continue;
5102
5103 if (!lit_has_binary_clauses (ps, NOTLIT (lit)))
5104 {
5105 #ifdef STATS
5106 ps->flskipped++;
5107 #endif
5108 continue;
5109 }
5110
5111 #ifdef STATS
5112 ps->fltried++;
5113 #endif
5114 LOG ( fprintf (ps->out, "%strying %d as failed literal\n",
5115 ps->prefix, LIT2INT (lit)));
5116
5117 assign_decision (ps, lit);
5118 old_trail_count = ps->thead - ps->trail;
5119 flbcp (ps);
5120
5121 if (ps->conflict)
5122 {
5123 EXPLICITLY_FAILED_LITERAL:
5124 LOG ( fprintf (ps->out, "%sfound explicitly failed literal %d\n",
5125 ps->prefix, LIT2INT (lit)));
5126
5127 ps->failedlits++;
5128 ps->efailedlits++;
5129
5130 backtrack (ps);
5131 flbcp (ps);
5132
5133 if (!ps->conflict)
5134 continue;
5135
5136 CONTRADICTION:
5137 assert (!ps->LEVEL);
5138 backtrack (ps);
5139 assert (ps->mtcls);
5140
5141 goto RETURN;
5142 }
5143
5144 if (ps->propagations >= limit)
5145 {
5146 undo (ps, 0);
5147 break;
5148 }
5149
5150 lit = NOTLIT (lit);
5151
5152 if (!lit_has_binary_clauses (ps, NOTLIT (lit)))
5153 {
5154 #ifdef STATS
5155 ps->flskipped++;
5156 #endif
5157 undo (ps, 0);
5158 continue;
5159 }
5160
5161 #ifdef STATS
5162 ps->fltried++;
5163 #endif
5164 LOG ( fprintf (ps->out, "%strying %d as failed literals\n",
5165 ps->prefix, LIT2INT (lit)));
5166
5167 new_trail_count = ps->thead - ps->trail;
5168 saved_count = new_trail_count - old_trail_count;
5169
5170 if (saved_count > ps->saved_size)
5171 {
5172 new_saved_size = ps->saved_size ? 2 * ps->saved_size : 1;
5173 while (saved_count > new_saved_size)
5174 new_saved_size *= 2;
5175
5176 RESIZEN (ps->saved, ps->saved_size, new_saved_size);
5177 ps->saved_size = new_saved_size;
5178 }
5179
5180 for (j = 0; j < saved_count; j++)
5181 ps->saved[j] = ps->trail[old_trail_count + j];
5182
5183 undo (ps, 0);
5184
5185 assign_decision (ps, lit);
5186 flbcp (ps);
5187
5188 if (ps->conflict)
5189 goto EXPLICITLY_FAILED_LITERAL;
5190
5191 pivot = (ps->thead - ps->trail <= new_trail_count) ? lit : NOTLIT (lit);
5192
5193 common = 0;
5194 for (j = 0; j < saved_count; j++)
5195 if ((other = ps->saved[j])->val == TRUE)
5196 ps->saved[common++] = other;
5197
5198 undo (ps, 0);
5199
5200 LOG (if (common)
5201 fprintf (ps->out,
5202 "%sfound %d literals implied by %d and %d\n",
5203 ps->prefix, common,
5204 LIT2INT (NOTLIT (lit)), LIT2INT (lit)));
5205
5206 #if 1 // set to zero to disable 'lifting'
5207 for (j = 0;
5208 j < common
5209 /* TODO: For some Velev benchmarks, extracting the common implicit
5210 * failed literals took quite some time. This needs to be fixed by
5211 * a dedicated analyzer. Up to then we bound the number of
5212 * propagations in this loop as well.
5213 */
5214 && ps->propagations < limit + delta
5215 ; j++)
5216 {
5217 other = ps->saved[j];
5218
5219 if (other->val == TRUE)
5220 continue;
5221
5222 assert (!other->val);
5223
5224 LOG ( fprintf (ps->out,
5225 "%sforcing %d as forced implicitly failed literal\n",
5226 ps->prefix, LIT2INT (other)));
5227
5228 assert (pivot != NOTLIT (other));
5229 assert (pivot != other);
5230
5231 assign_decision (ps, NOTLIT (other));
5232 flbcp (ps);
5233
5234 assert (ps->LEVEL == 1);
5235
5236 if (ps->conflict)
5237 {
5238 backtrack (ps);
5239 assert (!ps->LEVEL);
5240 }
5241 else
5242 {
5243 assign_decision (ps, pivot);
5244 flbcp (ps);
5245
5246 backtrack (ps);
5247
5248 if (ps->LEVEL)
5249 {
5250 assert (ps->LEVEL == 1);
5251
5252 flbcp (ps);
5253
5254 if (ps->conflict)
5255 {
5256 backtrack (ps);
5257 assert (!ps->LEVEL);
5258 }
5259 else
5260 {
5261 assign_decision (ps, NOTLIT (pivot));
5262 flbcp (ps);
5263 backtrack (ps);
5264
5265 if (ps->LEVEL)
5266 {
5267 assert (ps->LEVEL == 1);
5268 flbcp (ps);
5269
5270 if (!ps->conflict)
5271 {
5272 #ifdef STATS
5273 ps->floopsed++;
5274 #endif
5275 undo (ps, 0);
5276 continue;
5277 }
5278
5279 backtrack (ps);
5280 }
5281
5282 assert (!ps->LEVEL);
5283 }
5284
5285 assert (!ps->LEVEL);
5286 }
5287 }
5288 assert (!ps->LEVEL);
5289 flbcp (ps);
5290
5291 ps->failedlits++;
5292 ps->ifailedlits++;
5293
5294 if (ps->conflict)
5295 goto CONTRADICTION;
5296 }
5297 #endif
5298 }
5299
5300 ps->fllimit += 9 * (ps->propagations - ps->fllimit); /* 10% for failed literals */
5301
5302 RETURN:
5303
5304 /* First flush top level assigned literals. Those are prohibited from
5305 * being pushed up the heap during 'faillits' since 'simplifying' is set.
5306 */
5307 assert (ps->heap < ps->hhead);
5308 for (p = q = ps->heap + 1; p < ps->hhead; p++)
5309 {
5310 r = *p;
5311 lit = RNK2LIT (r);
5312 if (lit->val)
5313 r->pos = 0;
5314 else
5315 *q++ = r;
5316 }
5317
5318 /* Then resort with respect to EVSIDS score and fix positions.
5319 */
5320 SORT (Rnk *, cmp_inverse_rnk, ps->heap + 1, ps->hhead - (ps->heap + 1));
5321 for (p = ps->heap + 1; p < ps->hhead; p++)
5322 (*p)->pos = p - ps->heap;
5323
5324 sflush (ps);
5325 ps->flseconds += ps->seconds - started;
5326 }
5327
5328 #endif
5329
5330 static void
5331 simplify (PS * ps, int forced)
5332 {
5333 Lit * lit, * notlit, ** t;
5334 unsigned collect, delta;
5335 #ifdef STATS
5336 size_t bytes_collected;
5337 #endif
5338 int * q, ilit;
5339 Cls **p, *c;
5340 Var * v;
5341
5342 #ifndef NDEDBUG
5343 (void) forced;
5344 #endif
5345
5346 assert (!ps->mtcls);
5347 assert (!satisfied (ps));
5348 assert (forced || ps->lsimplify <= ps->propagations);
5349 assert (forced || ps->fsimplify <= ps->fixed);
5350
5351 if (ps->LEVEL)
5352 undo (ps, 0);
5353 #ifndef NFL
5354 ps->simplifying = 1;
5355 faillits (ps);
5356 ps->simplifying = 0;
5357
5358 if (ps->mtcls)
5359 return;
5360 #endif
5361
5362 if (ps->cils != ps->cilshead)
5363 {
5364 assert (ps->ttail == ps->thead);
5365 assert (ps->ttail2 == ps->thead);
5366 ps->ttail = ps->trail;
5367 for (t = ps->trail; t < ps->thead; t++)
5368 {
5369 lit = *t;
5370 v = LIT2VAR (lit);
5371 if (v->internal)
5372 {
5373 assert (LIT2INT (lit) < 0);
5374 assert (lit->val == TRUE);
5375 unassign (ps, lit);
5376 }
5377 else
5378 *ps->ttail++ = lit;
5379 }
5380 ps->ttail2 = ps->thead = ps->ttail;
5381
5382 for (q = ps->cils; q != ps->cilshead; q++)
5383 {
5384 ilit = *q;
5385 assert (0 < ilit && ilit <= (int) ps->max_var);
5386 v = ps->vars + ilit;
5387 assert (v->internal);
5388 v->level = 0;
5389 v->reason = 0;
5390 lit = int2lit (ps, -ilit);
5391 assert (lit->val == UNDEF);
5392 lit->val = TRUE;
5393 notlit = NOTLIT (lit);
5394 assert (notlit->val == UNDEF);
5395 notlit->val = FALSE;
5396 }
5397 }
5398
5399 collect = 0;
5400 for (p = SOC; p != EOC; p = NXC (p))
5401 {
5402 c = *p;
5403 if (!c)
5404 continue;
5405
5406 #ifdef TRACE
5407 if (c->collected)
5408 continue;
5409 #endif
5410
5411 if (c->locked)
5412 continue;
5413
5414 assert (!c->collect);
5415 if (clause_is_toplevel_satisfied (ps, c))
5416 {
5417 mark_clause_to_be_collected (c);
5418 collect++;
5419 }
5420 }
5421
5422 LOG ( fprintf (ps->out, "%scollecting %d clauses\n", ps->prefix, collect));
5423 #ifdef STATS
5424 bytes_collected =
5425 #endif
5426 collect_clauses (ps);
5427 #ifdef STATS
5428 ps->srecycled += bytes_collected;
5429 #endif
5430
5431 if (ps->cils != ps->cilshead)
5432 {
5433 for (q = ps->cils; q != ps->cilshead; q++)
5434 {
5435 ilit = *q;
5436 assert (0 < ilit && ilit <= (int) ps->max_var);
5437 assert (ps->vars[ilit].internal);
5438 if (ps->rilshead == ps->eorils)
5439 ENLARGE (ps->rils, ps->rilshead, ps->eorils);
5440 *ps->rilshead++ = ilit;
5441 lit = int2lit (ps, -ilit);
5442 assert (lit->val == TRUE);
5443 lit->val = UNDEF;
5444 notlit = NOTLIT (lit);
5445 assert (notlit->val == FALSE);
5446 notlit->val = UNDEF;
5447 }
5448 ps->cilshead = ps->cils;
5449 }
5450
5451 delta = 10 * (ps->olits + ps->llits) + 100000;
5452 if (delta > 2000000)
5453 delta = 2000000;
5454 ps->lsimplify = ps->propagations + delta;
5455 ps->fsimplify = ps->fixed;
5456 ps->simps++;
5457
5458 report (ps, 1, 's');
5459 }
5460
5461 static void
5462 iteration (PS * ps)
5463 {
5464 assert (!ps->LEVEL);
5465 assert (bcp_queue_is_empty (ps));
5466 assert (ps->isimplify < ps->fixed);
5467
5468 ps->iterations++;
5469 report (ps, 2, 'i');
5470 #ifdef NLUBY
5471 ps->drestart = MINRESTART;
5472 ps->lrestart = ps->conflicts + ps->drestart;
5473 #else
5474 init_restart (ps);
5475 #endif
5476 ps->isimplify = ps->fixed;
5477 }
5478
5479 static int
5480 cmp_glue_activity_size (PS * ps, Cls * c, Cls * d)
5481 {
5482 Act a, b, * p, * q;
5483
5484 (void) ps;
5485
5486 assert (c->learned);
5487 assert (d->learned);
5488
5489 if (c->glue < d->glue) // smaller glue preferred
5490 return 1;
5491
5492 if (c->glue > d->glue)
5493 return -1;
5494
5495 p = CLS2ACT (c);
5496 q = CLS2ACT (d);
5497 a = *p;
5498 b = *q;
5499
5500 if (a < b) // then higher activity
5501 return -1;
5502
5503 if (b < a)
5504 return 1;
5505
5506 if (c->size < d->size) // then smaller size
5507 return 1;
5508
5509 if (c->size > d->size)
5510 return -1;
5511
5512 return 0;
5513 }
5514
5515 static void
5516 reduce (PS * ps, unsigned percentage)
5517 {
5518 unsigned redcount, lcollect, collect, target;
5519 #ifdef STATS
5520 size_t bytes_collected;
5521 #endif
5522 Cls **p, *c;
5523
5524 assert (ps->rhead == ps->resolved);
5525
5526 ps->lastreduceconflicts = ps->conflicts;
5527
5528 assert (percentage <= 100);
5529 LOG ( fprintf (ps->out,
5530 "%sreducing %u%% learned clauses\n",
5531 ps->prefix, percentage));
5532
5533 while (ps->nlclauses - ps->llocked > (unsigned)(ps->eor - ps->resolved))
5534 ENLARGE (ps->resolved, ps->rhead, ps->eor);
5535
5536 collect = 0;
5537 lcollect = 0;
5538
5539 for (p = ((ps->fsimplify < ps->fixed) ? SOC : ps->lclauses); p != EOC; p = NXC (p))
5540 {
5541 c = *p;
5542 if (!c)
5543 continue;
5544
5545 #ifdef TRACE
5546 if (c->collected)
5547 continue;
5548 #endif
5549
5550 if (c->locked)
5551 continue;
5552
5553 assert (!c->collect);
5554 if (ps->fsimplify < ps->fixed && clause_is_toplevel_satisfied (ps, c))
5555 {
5556 mark_clause_to_be_collected (c);
5557 collect++;
5558
5559 if (c->learned && c->size > 2)
5560 lcollect++;
5561
5562 continue;
5563 }
5564
5565 if (!c->learned)
5566 continue;
5567
5568 if (c->size <= 2)
5569 continue;
5570
5571 assert (ps->rhead < ps->eor);
5572 *ps->rhead++ = c;
5573 }
5574 assert (ps->rhead <= ps->eor);
5575
5576 ps->fsimplify = ps->fixed;
5577
5578 redcount = ps->rhead - ps->resolved;
5579 SORT (Cls *, cmp_glue_activity_size, ps->resolved, redcount);
5580
5581 assert (ps->nlclauses >= lcollect);
5582 target = ps->nlclauses - lcollect + 1;
5583
5584 target = (percentage * target + 99) / 100;
5585
5586 if (target >= redcount)
5587 target = redcount;
5588
5589 ps->rhead = ps->resolved + target;
5590 while (ps->rhead > ps->resolved)
5591 {
5592 c = *--ps->rhead;
5593 mark_clause_to_be_collected (c);
5594
5595 collect++;
5596 if (c->learned && c->size > 2) /* just for consistency */
5597 lcollect++;
5598 }
5599
5600 if (collect)
5601 {
5602 ps->reductions++;
5603 #ifdef STATS
5604 bytes_collected =
5605 #endif
5606 collect_clauses (ps);
5607 #ifdef STATS
5608 ps->rrecycled += bytes_collected;
5609 #endif
5610 report (ps, 2, '-');
5611 }
5612
5613 if (!lcollect)
5614 inc_lreduce (ps); /* avoid dead lock */
5615
5616 assert (ps->rhead == ps->resolved);
5617 }
5618
5619 static void
5620 init_reduce (PS * ps)
5621 {
5622 // lreduce = loadded / 2;
5623 ps->lreduce = 1000;
5624
5625 if (ps->lreduce < 100)
5626 ps->lreduce = 100;
5627
5628 if (ps->verbosity)
5629 fprintf (ps->out,
5630 "%s\n%sinitial reduction limit %u clauses\n%s\n",
5631 ps->prefix, ps->prefix, ps->lreduce, ps->prefix);
5632 }
5633
5634 static unsigned
5635 rng (PS * ps)
5636 {
5637 unsigned res = ps->srng;
5638 ps->srng *= 1664525u;
5639 ps->srng += 1013904223u;
5640 NOLOG ( fprintf (ps->out, "%srng () = %u\n", ps->prefix, res));
5641 return res;
5642 }
5643
5644 static unsigned
5645 rrng (PS * ps, unsigned low, unsigned high)
5646 {
5647 unsigned long long tmp;
5648 unsigned res, elements;
5649 assert (low <= high);
5650 elements = high - low + 1;
5651 tmp = rng (ps);
5652 tmp *= elements;
5653 tmp >>= 32;
5654 tmp += low;
5655 res = tmp;
5656 NOLOG ( fprintf (ps->out, "%srrng (ps, %u, %u) = %u\n", ps->prefix, low, high, res));
5657 assert (low <= res);
5658 assert (res <= high);
5659 return res;
5660 }
5661
5662 static Lit *
5663 decide_phase (PS * ps, Lit * lit)
5664 {
5665 Lit * not_lit = NOTLIT (lit);
5666 Var *v = LIT2VAR (lit);
5667
5668 assert (LIT2SGN (lit) > 0);
5669 if (v->usedefphase)
5670 {
5671 if (v->defphase)
5672 {
5673 /* assign to TRUE */
5674 }
5675 else
5676 {
5677 /* assign to FALSE */
5678 lit = not_lit;
5679 }
5680 }
5681 else if (!v->assigned)
5682 {
5683 #ifdef STATS
5684 ps->staticphasedecisions++;
5685 #endif
5686 if (ps->defaultphase == POSPHASE)
5687 {
5688 /* assign to TRUE */
5689 }
5690 else if (ps->defaultphase == NEGPHASE)
5691 {
5692 /* assign to FALSE */
5693 lit = not_lit;
5694 }
5695 else if (ps->defaultphase == RNDPHASE)
5696 {
5697 /* randomly assign default phase */
5698 if (rrng (ps, 1, 2) != 2)
5699 lit = not_lit;
5700 }
5701 else if (*LIT2JWH(lit) <= *LIT2JWH (not_lit))
5702 {
5703 /* assign to FALSE (Jeroslow-Wang says there are more short
5704 * clauses with negative occurence of this variable, so satisfy
5705 * those, to minimize BCP)
5706 */
5707 lit = not_lit;
5708 }
5709 else
5710 {
5711 /* assign to TRUE (... but strictly more positive occurrences) */
5712 }
5713 }
5714 else
5715 {
5716 /* repeat last phase: phase saving heuristic */
5717
5718 if (v->phase)
5719 {
5720 /* assign to TRUE (last phase was TRUE as well) */
5721 }
5722 else
5723 {
5724 /* assign to FALSE (last phase was FALSE as well) */
5725 lit = not_lit;
5726 }
5727 }
5728
5729 return lit;
5730 }
5731
5732 static unsigned
5733 gcd (unsigned a, unsigned b)
5734 {
5735 unsigned tmp;
5736
5737 assert (a);
5738 assert (b);
5739
5740 if (a < b)
5741 {
5742 tmp = a;
5743 a = b;
5744 b = tmp;
5745 }
5746
5747 while (b)
5748 {
5749 assert (a >= b);
5750 tmp = b;
5751 b = a % b;
5752 a = tmp;
5753 }
5754
5755 return a;
5756 }
5757
5758 static Lit *
5759 rdecide (PS * ps)
5760 {
5761 unsigned idx, delta, spread;
5762 Lit * res;
5763
5764 spread = RDECIDE;
5765 if (rrng (ps, 1, spread) != 2)
5766 return 0;
5767
5768 assert (1 <= ps->max_var);
5769 idx = rrng (ps, 1, ps->max_var);
5770 res = int2lit (ps, idx);
5771
5772 if (res->val != UNDEF)
5773 {
5774 delta = rrng (ps, 1, ps->max_var);
5775 while (gcd (delta, ps->max_var) != 1)
5776 delta--;
5777
5778 assert (1 <= delta);
5779 assert (delta <= ps->max_var);
5780
5781 do {
5782 idx += delta;
5783 if (idx > ps->max_var)
5784 idx -= ps->max_var;
5785 res = int2lit (ps, idx);
5786 } while (res->val != UNDEF);
5787 }
5788
5789 #ifdef STATS
5790 ps->rdecisions++;
5791 #endif
5792 res = decide_phase (ps, res);
5793 LOG ( fprintf (ps->out, "%srdecide %d\n", ps->prefix, LIT2INT (res)));
5794
5795 return res;
5796 }
5797
5798 static Lit *
5799 sdecide (PS * ps)
5800 {
5801 Lit *res;
5802 Rnk *r;
5803
5804 for (;;)
5805 {
5806 r = htop (ps);
5807 res = RNK2LIT (r);
5808 if (res->val == UNDEF) break;
5809 (void) hpop (ps);
5810 NOLOG ( fprintf (ps->out,
5811 "%shpop %u %u %u\n",
5812 ps->prefix, r - ps->rnks,
5813 FLTMANTISSA(r->score),
5814 FLTEXPONENT(r->score)));
5815 }
5816
5817 #ifdef STATS
5818 ps->sdecisions++;
5819 #endif
5820 res = decide_phase (ps, res);
5821
5822 LOG ( fprintf (ps->out, "%ssdecide %d\n", ps->prefix, LIT2INT (res)));
5823
5824 return res;
5825 }
5826
5827 static Lit *
5828 adecide (PS * ps)
5829 {
5830 Lit *lit;
5831 Var * v;
5832
5833 assert (ps->als < ps->alshead);
5834 assert (!ps->failed_assumption);
5835
5836 while (ps->alstail < ps->alshead)
5837 {
5838 lit = *ps->alstail++;
5839
5840 if (lit->val == FALSE)
5841 {
5842 ps->failed_assumption = lit;
5843 v = LIT2VAR (lit);
5844
5845 use_var (ps, v);
5846
5847 LOG ( fprintf (ps->out, "%sfirst failed assumption %d\n",
5848 ps->prefix, LIT2INT (ps->failed_assumption)));
5849 fanalyze (ps);
5850 return 0;
5851 }
5852
5853 if (lit->val == TRUE)
5854 {
5855 v = LIT2VAR (lit);
5856 if (v->level > ps->adecidelevel)
5857 ps->adecidelevel = v->level;
5858 continue;
5859 }
5860
5861 #ifdef STATS
5862 ps->assumptions++;
5863 #endif
5864 LOG ( fprintf (ps->out, "%sadecide %d\n", ps->prefix, LIT2INT (lit)));
5865 ps->adecidelevel = ps->LEVEL + 1;
5866
5867 return lit;
5868 }
5869
5870 return 0;
5871 }
5872
5873 static void
5874 decide (PS * ps)
5875 {
5876 Lit * lit;
5877
5878 assert (!satisfied (ps));
5879 assert (!ps->conflict);
5880
5881 if (ps->alstail < ps->alshead && (lit = adecide (ps)))
5882 ;
5883 else if (ps->failed_assumption)
5884 return;
5885 else if (satisfied (ps))
5886 return;
5887 else if (!(lit = rdecide (ps)))
5888 lit = sdecide (ps);
5889
5890 assert (lit);
5891 assign_decision (ps, lit);
5892
5893 ps->levelsum += ps->LEVEL;
5894 ps->decisions++;
5895 }
5896
5897 static int
5898 sat (PS * ps, int l)
5899 {
5900 int count = 0, backtracked;
5901
5902 if (!ps->conflict)
5903 bcp (ps);
5904
5905 if (ps->conflict)
5906 backtrack (ps);
5907
5908 if (ps->mtcls)
5909 return PICOSAT_UNSATISFIABLE;
5910
5911 if (satisfied (ps))
5912 goto SATISFIED;
5913
5914 if (ps->lsimplify <= ps->propagations)
5915 simplify (ps, 0);
5916
5917 if (ps->mtcls)
5918 return PICOSAT_UNSATISFIABLE;
5919
5920 if (satisfied (ps))
5921 goto SATISFIED;
5922
5923 init_restart (ps);
5924
5925 if (!ps->lreduce)
5926 init_reduce (ps);
5927
5928 ps->isimplify = ps->fixed;
5929 backtracked = 0;
5930
5931 for (;;)
5932 {
5933 if (!ps->conflict)
5934 bcp (ps);
5935
5936 if (ps->conflict)
5937 {
5938 incincs (ps);
5939 backtrack (ps);
5940
5941 if (ps->mtcls)
5942 return PICOSAT_UNSATISFIABLE;
5943 backtracked = 1;
5944 continue;
5945 }
5946
5947 if (satisfied (ps))
5948 {
5949 SATISFIED:
5950 #ifndef NDEBUG
5951 original_clauses_satisfied (ps);
5952 assumptions_satisfied (ps);
5953 #endif
5954 return PICOSAT_SATISFIABLE;
5955 }
5956
5957 if (backtracked)
5958 {
5959 backtracked = 0;
5960 if (!ps->LEVEL && ps->isimplify < ps->fixed)
5961 iteration (ps);
5962 }
5963
5964 if (l >= 0 && count >= l) /* decision limit reached ? */
5965 return PICOSAT_UNKNOWN;
5966
5967 if (ps->interrupt.function && /* external interrupt */
5968 count > 0 && !(count % INTERRUPTLIM) &&
5969 ps->interrupt.function (ps->interrupt.state))
5970 return PICOSAT_UNKNOWN;
5971
5972 if (ps->propagations >= ps->lpropagations)/* propagation limit reached ? */
5973 return PICOSAT_UNKNOWN;
5974
5975 #ifndef NADC
5976 if (!ps->adodisabled && ps->adoconflicts >= ps->adoconflictlimit)
5977 {
5978 assert (bcp_queue_is_empty (ps));
5979 return PICOSAT_UNKNOWN;
5980 }
5981 #endif
5982
5983 if (ps->fsimplify < ps->fixed && ps->lsimplify <= ps->propagations)
5984 {
5985 simplify (ps, 0);
5986 if (!bcp_queue_is_empty (ps))
5987 continue;
5988 #ifndef NFL
5989 if (ps->mtcls)
5990 return PICOSAT_UNSATISFIABLE;
5991
5992 if (satisfied (ps))
5993 return PICOSAT_SATISFIABLE;
5994
5995 assert (!ps->LEVEL);
5996 #endif
5997 }
5998
5999 if (need_to_reduce (ps))
6000 reduce (ps, 50);
6001
6002 if (ps->conflicts >= ps->lrestart && ps->LEVEL > 2)
6003 restart (ps);
6004
6005 decide (ps);
6006 if (ps->failed_assumption)
6007 return PICOSAT_UNSATISFIABLE;
6008 count++;
6009 }
6010 }
6011
6012 static void
6013 rebias (PS * ps)
6014 {
6015 Cls ** p, * c;
6016 Var * v;
6017
6018 for (v = ps->vars + 1; v <= ps->vars + ps->max_var; v++)
6019 v->assigned = 0;
6020
6021 memset (ps->jwh, 0, 2 * (ps->max_var + 1) * sizeof *ps->jwh);
6022
6023 for (p = ps->oclauses; p < ps->ohead; p++)
6024 {
6025 c = *p;
6026
6027 if (!c)
6028 continue;
6029
6030 if (c->learned)
6031 continue;
6032
6033 incjwh (ps, c);
6034 }
6035 }
6036
6037 #ifdef TRACE
6038
6039 static unsigned
6040 core (PS * ps)
6041 {
6042 unsigned idx, prev, this, delta, i, lcore, vcore;
6043 unsigned *stack, *shead, *eos;
6044 Lit **q, **eol, *lit;
6045 Cls *c, *reason;
6046 Znt *p, byte;
6047 Zhn *zhain;
6048 Var *v;
6049
6050 assert (ps->trace);
6051
6052 assert (ps->mtcls || ps->failed_assumption);
6053 if (ps->ocore >= 0)
6054 return ps->ocore;
6055
6056 lcore = ps->ocore = vcore = 0;
6057
6058 stack = shead = eos = 0;
6059 ENLARGE (stack, shead, eos);
6060
6061 if (ps->mtcls)
6062 {
6063 idx = CLS2IDX (ps->mtcls);
6064 *shead++ = idx;
6065 }
6066 else
6067 {
6068 assert (ps->failed_assumption);
6069 v = LIT2VAR (ps->failed_assumption);
6070 reason = v->reason;
6071 assert (reason);
6072 idx = CLS2IDX (reason);
6073 *shead++ = idx;
6074 }
6075
6076 while (shead > stack)
6077 {
6078 idx = *--shead;
6079 zhain = IDX2ZHN (idx);
6080
6081 if (zhain)
6082 {
6083 if (zhain->core)
6084 continue;
6085
6086 zhain->core = 1;
6087 lcore++;
6088
6089 c = IDX2CLS (idx);
6090 if (c)
6091 {
6092 assert (!c->core);
6093 c->core = 1;
6094 }
6095
6096 i = 0;
6097 delta = 0;
6098 prev = 0;
6099 for (p = zhain->znt; (byte = *p); p++, i += 7)
6100 {
6101 delta |= (byte & 0x7f) << i;
6102 if (byte & 0x80)
6103 continue;
6104
6105 this = prev + delta;
6106 assert (prev < this); /* no overflow */
6107
6108 if (shead == eos)
6109 ENLARGE (stack, shead, eos);
6110 *shead++ = this;
6111
6112 prev = this;
6113 delta = 0;
6114 i = -7;
6115 }
6116 }
6117 else
6118 {
6119 c = IDX2CLS (idx);
6120
6121 assert (c);
6122 assert (!c->learned);
6123
6124 if (c->core)
6125 continue;
6126
6127 c->core = 1;
6128 ps->ocore++;
6129
6130 eol = end_of_lits (c);
6131 for (q = c->lits; q < eol; q++)
6132 {
6133 lit = *q;
6134 v = LIT2VAR (lit);
6135 if (v->core)
6136 continue;
6137
6138 v->core = 1;
6139 vcore++;
6140
6141 if (!ps->failed_assumption) continue;
6142 if (lit != ps->failed_assumption) continue;
6143
6144 reason = v->reason;
6145 if (!reason) continue;
6146 if (reason->core) continue;
6147
6148 idx = CLS2IDX (reason);
6149 if (shead == eos)
6150 ENLARGE (stack, shead, eos);
6151 *shead++ = idx;
6152 }
6153 }
6154 }
6155
6156 DELETEN (stack, eos - stack);
6157
6158 if (ps->verbosity)
6159 fprintf (ps->out,
6160 "%s%u core variables out of %u (%.1f%%)\n"
6161 "%s%u core original clauses out of %u (%.1f%%)\n"
6162 "%s%u core learned clauses out of %u (%.1f%%)\n",
6163 ps->prefix, vcore, ps->max_var, PERCENT (vcore, ps->max_var),
6164 ps->prefix, ps->ocore, ps->oadded, PERCENT (ps->ocore, ps->oadded),
6165 ps->prefix, lcore, ps->ladded, PERCENT (lcore, ps->ladded));
6166
6167 return ps->ocore;
6168 }
6169
6170 static void
6171 trace_lits (PS * ps, Cls * c, FILE * file)
6172 {
6173 Lit **p, **eol = end_of_lits (c);
6174
6175 assert (c);
6176 assert (c->core);
6177
6178 for (p = c->lits; p < eol; p++)
6179 fprintf (file, "%d ", LIT2INT (*p));
6180
6181 fputc ('0', file);
6182 }
6183
6184 static void
6185 write_idx (PS * ps, unsigned idx, FILE * file)
6186 {
6187 fprintf (file, "%ld", EXPORTIDX (idx));
6188 }
6189
6190 static void
6191 trace_clause (PS * ps, unsigned idx, Cls * c, FILE * file, int fmt)
6192 {
6193 assert (c);
6194 assert (c->core);
6195 assert (fmt == RUP_TRACE_FMT || !c->learned);
6196 assert (CLS2IDX (c) == idx);
6197
6198 if (fmt != RUP_TRACE_FMT)
6199 {
6200 write_idx (ps, idx, file);
6201 fputc (' ', file);
6202 }
6203
6204 trace_lits (ps, c, file);
6205
6206 if (fmt != RUP_TRACE_FMT)
6207 fputs (" 0", file);
6208
6209 fputc ('\n', file);
6210 }
6211
6212 static void
6213 trace_zhain (PS * ps, unsigned idx, Zhn * zhain, FILE * file, int fmt)
6214 {
6215 unsigned prev, this, delta, i;
6216 Znt *p, byte;
6217 Cls * c;
6218
6219 assert (zhain);
6220 assert (zhain->core);
6221
6222 write_idx (ps, idx, file);
6223 fputc (' ', file);
6224
6225 if (fmt == EXTENDED_TRACECHECK_TRACE_FMT)
6226 {
6227 c = IDX2CLS (idx);
6228 assert (c);
6229 trace_lits (ps, c, file);
6230 }
6231 else
6232 {
6233 assert (fmt == COMPACT_TRACECHECK_TRACE_FMT);
6234 putc ('*', file);
6235 }
6236
6237 i = 0;
6238 delta = 0;
6239 prev = 0;
6240
6241 for (p = zhain->znt; (byte = *p); p++, i += 7)
6242 {
6243 delta |= (byte & 0x7f) << i;
6244 if (byte & 0x80)
6245 continue;
6246
6247 this = prev + delta;
6248
6249 putc (' ', file);
6250 write_idx (ps, this, file);
6251
6252 prev = this;
6253 delta = 0;
6254 i = -7;
6255 }
6256
6257 fputs (" 0\n", file);
6258 }
6259
6260 static void
6261 write_core (PS * ps, FILE * file)
6262 {
6263 Lit **q, **eol;
6264 Cls **p, *c;
6265
6266 fprintf (file, "p cnf %u %u\n", ps->max_var, core (ps));
6267
6268 for (p = SOC; p != EOC; p = NXC (p))
6269 {
6270 c = *p;
6271
6272 if (!c || c->learned || !c->core)
6273 continue;
6274
6275 eol = end_of_lits (c);
6276 for (q = c->lits; q < eol; q++)
6277 fprintf (file, "%d ", LIT2INT (*q));
6278
6279 fputs ("0\n", file);
6280 }
6281 }
6282
6283 #endif
6284
6285 static void
6286 write_trace (PS * ps, FILE * file, int fmt)
6287 {
6288 #ifdef TRACE
6289 Cls *c, ** p;
6290 Zhn *zhain;
6291 unsigned i;
6292
6293 core (ps);
6294
6295 if (fmt == RUP_TRACE_FMT)
6296 {
6297 ps->rupvariables = picosat_variables (ps),
6298 ps->rupclauses = picosat_added_original_clauses (ps);
6299 write_rup_header (ps, file);
6300 }
6301
6302 for (p = SOC; p != EOC; p = NXC (p))
6303 {
6304 c = *p;
6305
6306 if (ps->oclauses <= p && p < ps->eoo)
6307 {
6308 i = OIDX2IDX (p - ps->oclauses);
6309 assert (!c || CLS2IDX (c) == i);
6310 }
6311 else
6312 {
6313 assert (ps->lclauses <= p && p < ps->EOL);
6314 i = LIDX2IDX (p - ps->lclauses);
6315 }
6316
6317 zhain = IDX2ZHN (i);
6318
6319 if (zhain)
6320 {
6321 if (zhain->core)
6322 {
6323 if (fmt == RUP_TRACE_FMT)
6324 trace_clause (ps,i, c, file, fmt);
6325 else
6326 trace_zhain (ps, i, zhain, file, fmt);
6327 }
6328 }
6329 else if (c)
6330 {
6331 if (fmt != RUP_TRACE_FMT && c)
6332 {
6333 if (c->core)
6334 trace_clause (ps, i, c, file, fmt);
6335 }
6336 }
6337 }
6338 #else
6339 (void) file;
6340 (void) fmt;
6341 (void) ps;
6342 #endif
6343 }
6344
6345 static void
6346 write_core_wrapper (PS * ps, FILE * file, int fmt)
6347 {
6348 (void) fmt;
6349 #ifdef TRACE
6350 write_core (ps, file);
6351 #else
6352 (void) ps;
6353 (void) file;
6354 #endif
6355 }
6356
6357 static Lit *
6358 import_lit (PS * ps, int lit, int nointernal)
6359 {
6360 Lit * res;
6361 Var * v;
6362
6363 ABORTIF (lit == INT_MIN, "API usage: INT_MIN literal");
6364 ABORTIF (abs (lit) > (int) ps->max_var && ps->CLS != ps->clshead,
6365 "API usage: new variable index after 'picosat_push'");
6366
6367 if (abs (lit) <= (int) ps->max_var)
6368 {
6369 res = int2lit (ps, lit);
6370 v = LIT2VAR (res);
6371 if (nointernal && v->internal)
6372 ABORT ("API usage: trying to import invalid literal");
6373 else if (!nointernal && !v->internal)
6374 ABORT ("API usage: trying to import invalid context");
6375 }
6376 else
6377 {
6378 while (abs (lit) > (int) ps->max_var)
6379 inc_max_var (ps);
6380 res = int2lit (ps, lit);
6381 }
6382
6383 return res;
6384 }
6385
6386 #ifdef TRACE
6387 static void
6388 reset_core (PS * ps)
6389 {
6390 Cls ** p, * c;
6391 Zhn ** q, * z;
6392 unsigned i;
6393
6394 for (i = 1; i <= ps->max_var; i++)
6395 ps->vars[i].core = 0;
6396
6397 for (p = SOC; p != EOC; p = NXC (p))
6398 if ((c = *p))
6399 c->core = 0;
6400
6401 for (q = ps->zhains; q != ps->zhead; q++)
6402 if ((z = *q))
6403 z->core = 0;
6404
6405 ps->ocore = -1;
6406 }
6407 #endif
6408
6409 static void
6410 reset_assumptions (PS * ps)
6411 {
6412 Lit ** p;
6413
6414 ps->failed_assumption = 0;
6415
6416 if (ps->extracted_all_failed_assumptions)
6417 {
6418 for (p = ps->als; p < ps->alshead; p++)
6419 LIT2VAR (*p)->failed = 0;
6420
6421 ps->extracted_all_failed_assumptions = 0;
6422 }
6423
6424 ps->alstail = ps->alshead = ps->als;
6425 ps->adecidelevel = 0;
6426 }
6427
6428 static void
6429 check_ready (PS * ps)
6430 {
6431 ABORTIF (!ps || ps->state == RESET, "API usage: uninitialized");
6432 }
6433
6434 static void
6435 check_sat_state (PS * ps)
6436 {
6437 ABORTIF (ps->state != SAT, "API usage: expected to be in SAT state");
6438 }
6439
6440 static void
6441 check_unsat_state (PS * ps)
6442 {
6443 ABORTIF (ps->state != UNSAT, "API usage: expected to be in UNSAT state");
6444 }
6445
6446 static void
6447 check_sat_or_unsat_or_unknown_state (PS * ps)
6448 {
6449 ABORTIF (ps->state != SAT && ps->state != UNSAT && ps->state != UNKNOWN,
6450 "API usage: expected to be in SAT, UNSAT, or UNKNOWN state");
6451 }
6452
6453 static void
6454 reset_partial (PS * ps)
6455 {
6456 unsigned idx;
6457 if (!ps->partial)
6458 return;
6459 for (idx = 1; idx <= ps->max_var; idx++)
6460 ps->vars[idx].partial = 0;
6461 ps->partial = 0;
6462 }
6463
6464 static void
6465 reset_incremental_usage (PS * ps)
6466 {
6467 unsigned num_non_false;
6468 Lit * lit, ** q;
6469
6470 check_sat_or_unsat_or_unknown_state (ps);
6471
6472 LOG ( fprintf (ps->out, "%sRESET incremental usage\n", ps->prefix));
6473
6474 if (ps->LEVEL)
6475 undo (ps, 0);
6476
6477 reset_assumptions (ps);
6478
6479 if (ps->conflict)
6480 {
6481 num_non_false = 0;
6482 for (q = ps->conflict->lits; q < end_of_lits (ps->conflict); q++)
6483 {
6484 lit = *q;
6485 if (lit->val != FALSE)
6486 num_non_false++;
6487 }
6488
6489 // assert (num_non_false >= 2); // TODO: why this assertion?
6490 #ifdef NO_BINARY_CLAUSES
6491 if (ps->conflict == &ps->cimpl)
6492 resetcimpl (ps);
6493 #endif
6494 #ifndef NADC
6495 if (ps->conflict == ps->adoconflict)
6496 resetadoconflict (ps);
6497 #endif
6498 ps->conflict = 0;
6499 }
6500
6501 #ifdef TRACE
6502 reset_core (ps);
6503 #endif
6504
6505 reset_partial (ps);
6506
6507 ps->saved_flips = ps->flips;
6508 ps->min_flipped = UINT_MAX;
6509 ps->saved_max_var = ps->max_var;
6510
6511 ps->state = READY;
6512 }
6513
6514 static void
6515 enter (PS * ps)
6516 {
6517 if (ps->nentered++)
6518 return;
6519
6520 check_ready (ps);
6521 ps->entered = picosat_time_stamp ();
6522 }
6523
6524 static void
6525 leave (PS * ps)
6526 {
6527 assert (ps->nentered);
6528 if (--ps->nentered)
6529 return;
6530
6531 sflush (ps);
6532 }
6533
6534 static void
6535 check_trace_support_and_execute (PS * ps,
6536 FILE * file,
6537 void (*f)(PS*,FILE*,int), int fmt)
6538 {
6539 check_ready (ps);
6540 check_unsat_state (ps);
6541 #ifdef TRACE
6542 ABORTIF (!ps->trace, "API usage: tracing disabled");
6543 enter (ps);
6544 f (ps, file, fmt);
6545 leave (ps);
6546 #else
6547 (void) file;
6548 (void) fmt;
6549 (void) f;
6550 ABORT ("compiled without trace support");
6551 #endif
6552 }
6553
6554 static void
6555 extract_all_failed_assumptions (PS * ps)
6556 {
6557 Lit ** p, ** eol;
6558 Var * v, * u;
6559 int pos;
6560 Cls * c;
6561
6562 assert (!ps->extracted_all_failed_assumptions);
6563
6564 assert (ps->failed_assumption);
6565 assert (ps->mhead == ps->marked);
6566
6567 if (ps->marked == ps->eom)
6568 ENLARGE (ps->marked, ps->mhead, ps->eom);
6569
6570 v = LIT2VAR (ps->failed_assumption);
6571 mark_var (ps, v);
6572 pos = 0;
6573
6574 while (pos < ps->mhead - ps->marked)
6575 {
6576 v = ps->marked[pos++];
6577 assert (v->mark);
6578 c = var2reason (ps, v);
6579 if (!c)
6580 continue;
6581 eol = end_of_lits (c);
6582 for (p = c->lits; p < eol; p++)
6583 {
6584 u = LIT2VAR (*p);
6585 if (!u->mark)
6586 mark_var (ps, u);
6587 }
6588 #ifdef NO_BINARY_CLAUSES
6589 if (c == &ps->impl)
6590 resetimpl (ps);
6591 #endif
6592 }
6593
6594 for (p = ps->als; p < ps->alshead; p++)
6595 {
6596 u = LIT2VAR (*p);
6597 if (!u->mark) continue;
6598 u->failed = 1;
6599 LOG ( fprintf (ps->out,
6600 "%sfailed assumption %d\n",
6601 ps->prefix, LIT2INT (*p)));
6602 }
6603
6604 while (ps->mhead > ps->marked)
6605 (*--ps->mhead)->mark = 0;
6606
6607 ps->extracted_all_failed_assumptions = 1;
6608 }
6609
6610 const char *
6611 picosat_copyright (void)
6612 {
6613 return "Copyright (c) 2006 - 2014 Armin Biere JKU Linz";
6614 }
6615
6616 PicoSAT *
6617 picosat_init (void)
6618 {
6619 return init (0, 0, 0, 0);
6620 }
6621
6622 PicoSAT *
6623 picosat_minit (void * pmgr,
6624 picosat_malloc pnew,
6625 picosat_realloc presize,
6626 picosat_free pfree)
6627 {
6628 ABORTIF (!pnew, "API usage: zero 'picosat_malloc' argument");
6629 ABORTIF (!presize, "API usage: zero 'picosat_realloc' argument");
6630 ABORTIF (!pfree, "API usage: zero 'picosat_free' argument");
6631 return init (pmgr, pnew, presize, pfree);
6632 }
6633
6634
6635 void
6636 picosat_adjust (PS * ps, int new_max_var)
6637 {
6638 unsigned new_size_vars;
6639
6640 ABORTIF (abs (new_max_var) > (int) ps->max_var && ps->CLS != ps->clshead,
6641 "API usage: adjusting variable index after 'picosat_push'");
6642 enter (ps);
6643
6644 new_max_var = abs (new_max_var);
6645 new_size_vars = new_max_var + 1;
6646
6647 if (ps->size_vars < new_size_vars)
6648 enlarge (ps, new_size_vars);
6649
6650 while (ps->max_var < (unsigned) new_max_var)
6651 inc_max_var (ps);
6652
6653 leave (ps);
6654 }
6655
6656 int
6657 picosat_inc_max_var (PS * ps)
6658 {
6659 if (ps->measurealltimeinlib)
6660 enter (ps);
6661 else
6662 check_ready (ps);
6663
6664 inc_max_var (ps);
6665
6666 if (ps->measurealltimeinlib)
6667 leave (ps);
6668
6669 return ps->max_var;
6670 }
6671
6672 int
6673 picosat_context (PS * ps)
6674 {
6675 return ps->clshead == ps->CLS ? 0 : LIT2INT (ps->clshead[-1]);
6676 }
6677
6678 int
6679 picosat_push (PS * ps)
6680 {
6681 int res;
6682 Lit *lit;
6683 Var * v;
6684
6685 if (ps->measurealltimeinlib)
6686 enter (ps);
6687 else
6688 check_ready (ps);
6689
6690 if (ps->state != READY)
6691 reset_incremental_usage (ps);
6692
6693 if (ps->rils != ps->rilshead)
6694 {
6695 res = *--ps->rilshead;
6696 assert (ps->vars[res].internal);
6697 }
6698 else
6699 {
6700 inc_max_var (ps);
6701 res = ps->max_var;
6702 v = ps->vars + res;
6703 assert (!v->internal);
6704 v->internal = 1;
6705 ps->internals++;
6706 LOG ( fprintf (ps->out, "%snew internal variable index %d\n", ps->prefix, res));
6707 }
6708
6709 lit = int2lit (ps, res);
6710
6711 if (ps->clshead == ps->eocls)
6712 ENLARGE (ps->CLS, ps->clshead, ps->eocls);
6713 *ps->clshead++ = lit;
6714
6715 ps->contexts++;
6716
6717 LOG ( fprintf (ps->out, "%snew context %d at depth %ld after push\n",
6718 ps->prefix, res, (long)(ps->clshead - ps->CLS)));
6719
6720 if (ps->measurealltimeinlib)
6721 leave (ps);
6722
6723 return res;
6724 }
6725
6726 int
6727 picosat_pop (PS * ps)
6728 {
6729 Lit * lit;
6730 int res;
6731 ABORTIF (ps->CLS == ps->clshead, "API usage: too many 'picosat_pop'");
6732 ABORTIF (ps->added != ps->ahead, "API usage: incomplete clause");
6733
6734 if (ps->measurealltimeinlib)
6735 enter (ps);
6736 else
6737 check_ready (ps);
6738
6739 if (ps->state != READY)
6740 reset_incremental_usage (ps);
6741
6742 assert (ps->CLS < ps->clshead);
6743 lit = *--ps->clshead;
6744 LOG ( fprintf (ps->out, "%sclosing context %d at depth %ld after pop\n",
6745 ps->prefix, LIT2INT (lit), (long)(ps->clshead - ps->CLS) + 1));
6746
6747 if (ps->cilshead == ps->eocils)
6748 ENLARGE (ps->cils, ps->cilshead, ps->eocils);
6749 *ps->cilshead++ = LIT2INT (lit);
6750
6751 if (ps->cilshead - ps->cils > MAXCILS) {
6752 LOG ( fprintf (ps->out,
6753 "%srecycling %ld interals with forced simplification\n",
6754 ps->prefix, (long)(ps->cilshead - ps->cils)));
6755 simplify (ps, 1);
6756 }
6757
6758 res = picosat_context (ps);
6759 if (res)
6760 LOG ( fprintf (ps->out, "%snew context %d at depth %ld after pop\n",
6761 ps->prefix, res, (long)(ps->clshead - ps->CLS)));
6762 else
6763 LOG ( fprintf (ps->out, "%souter most context reached after pop\n", ps->prefix));
6764
6765 if (ps->measurealltimeinlib)
6766 leave (ps);
6767
6768 return res;
6769 }
6770
6771 void
6772 picosat_set_verbosity (PS * ps, int new_verbosity_level)
6773 {
6774 check_ready (ps);
6775 ps->verbosity = new_verbosity_level;
6776 }
6777
6778 void
6779 picosat_set_plain (PS * ps, int new_plain_value)
6780 {
6781 check_ready (ps);
6782 ps->plain = new_plain_value;
6783 }
6784
6785 int
6786 picosat_enable_trace_generation (PS * ps)
6787 {
6788 int res = 0;
6789 check_ready (ps);
6790 #ifdef TRACE
6791 ABORTIF (ps->addedclauses,
6792 "API usage: trace generation enabled after adding clauses");
6793 res = ps->trace = 1;
6794 #endif
6795 return res;
6796 }
6797
6798 void
6799 picosat_set_incremental_rup_file (PS * ps, FILE * rup_file, int m, int n)
6800 {
6801 check_ready (ps);
6802 assert (!ps->rupstarted);
6803 ps->rup = rup_file;
6804 ps->rupvariables = m;
6805 ps->rupclauses = n;
6806 }
6807
6808 void
6809 picosat_set_output (PS * ps, FILE * output_file)
6810 {
6811 check_ready (ps);
6812 ps->out = output_file;
6813 }
6814
6815 void
6816 picosat_measure_all_calls (PS * ps)
6817 {
6818 check_ready (ps);
6819 ps->measurealltimeinlib = 1;
6820 }
6821
6822 void
6823 picosat_set_prefix (PS * ps, const char * str)
6824 {
6825 check_ready (ps);
6826 new_prefix (ps, str);
6827 }
6828
6829 void
6830 picosat_set_seed (PS * ps, unsigned s)
6831 {
6832 check_ready (ps);
6833 ps->srng = s;
6834 }
6835
6836 void
6837 picosat_reset (PS * ps)
6838 {
6839 check_ready (ps);
6840 reset (ps);
6841 }
6842
6843 int
6844 picosat_add (PS * ps, int int_lit)
6845 {
6846 int res = ps->oadded;
6847 Lit *lit;
6848
6849 if (ps->measurealltimeinlib)
6850 enter (ps);
6851 else
6852 check_ready (ps);
6853
6854 ABORTIF (ps->rup && ps->rupstarted && ps->oadded >= (unsigned)ps->rupclauses,
6855 "API usage: adding too many clauses after RUP header written");
6856 #ifndef NADC
6857 ABORTIF (ps->addingtoado,
6858 "API usage: 'picosat_add' and 'picosat_add_ado_lit' mixed");
6859 #endif
6860 if (ps->state != READY)
6861 reset_incremental_usage (ps);
6862
6863 if (ps->saveorig)
6864 {
6865 if (ps->sohead == ps->eoso)
6866 ENLARGE (ps->soclauses, ps->sohead, ps->eoso);
6867
6868 *ps->sohead++ = int_lit;
6869 }
6870
6871 if (int_lit)
6872 {
6873 lit = import_lit (ps, int_lit, 1);
6874 add_lit (ps, lit);
6875 }
6876 else
6877 simplify_and_add_original_clause (ps);
6878
6879 if (ps->measurealltimeinlib)
6880 leave (ps);
6881
6882 return res;
6883 }
6884
6885 int
6886 picosat_add_arg (PS * ps, ...)
6887 {
6888 int lit;
6889 va_list ap;
6890 va_start (ap, ps);
6891 while ((lit = va_arg (ap, int)))
6892 (void) picosat_add (ps, lit);
6893 va_end (ap);
6894 return picosat_add (ps, 0);
6895 }
6896
6897 int
6898 picosat_add_lits (PS * ps, int * lits)
6899 {
6900 const int * p;
6901 int lit;
6902 for (p = lits; (lit = *p); p++)
6903 (void) picosat_add (ps, lit);
6904 return picosat_add (ps, 0);
6905 }
6906
6907 void
6908 picosat_add_ado_lit (PS * ps, int external_lit)
6909 {
6910 #ifndef NADC
6911 Lit * internal_lit;
6912
6913 if (ps->measurealltimeinlib)
6914 enter (ps);
6915 else
6916 check_ready (ps);
6917
6918 if (ps->state != READY)
6919 reset_incremental_usage (ps);
6920
6921 ABORTIF (!ps->addingtoado && ps->ahead > ps->added,
6922 "API usage: 'picosat_add' and 'picosat_add_ado_lit' mixed");
6923
6924 if (external_lit)
6925 {
6926 ps->addingtoado = 1;
6927 internal_lit = import_lit (ps, external_lit, 1);
6928 add_lit (ps, internal_lit);
6929 }
6930 else
6931 {
6932 ps->addingtoado = 0;
6933 add_ado (ps);
6934 }
6935 if (ps->measurealltimeinlib)
6936 leave (ps);
6937 #else
6938 (void) ps;
6939 (void) external_lit;
6940 ABORT ("compiled without all different constraint support");
6941 #endif
6942 }
6943
6944 static void
6945 assume (PS * ps, Lit * lit)
6946 {
6947 if (ps->alshead == ps->eoals)
6948 {
6949 assert (ps->alstail == ps->als);
6950 ENLARGE (ps->als, ps->alshead, ps->eoals);
6951 ps->alstail = ps->als;
6952 }
6953
6954 *ps->alshead++ = lit;
6955 LOG ( fprintf (ps->out, "%sassumption %d\n", ps->prefix, LIT2INT (lit)));
6956 }
6957
6958 static void
6959 assume_contexts (PS * ps)
6960 {
6961 Lit ** p;
6962 if (ps->als != ps->alshead)
6963 return;
6964 for (p = ps->CLS; p != ps->clshead; p++)
6965 assume (ps, *p);
6966 }
6967
6968 #ifndef RCODE
6969 static const char * enumstr (int i) {
6970 int last = i % 10;
6971 if (last == 1) return "st";
6972 if (last == 2) return "nd";
6973 if (last == 3) return "rd";
6974 return "th";
6975 }
6976 #endif
6977
6978 static int
6979 tderef (PS * ps, int int_lit)
6980 {
6981 Lit * lit;
6982 Var * v;
6983
6984 assert (abs (int_lit) <= (int) ps->max_var);
6985
6986 lit = int2lit (ps, int_lit);
6987
6988 v = LIT2VAR (lit);
6989 if (v->level > 0)
6990 return 0;
6991
6992 if (lit->val == TRUE)
6993 return 1;
6994
6995 if (lit->val == FALSE)
6996 return -1;
6997
6998 return 0;
6999 }
7000
7001 static int
7002 pderef (PS * ps, int int_lit)
7003 {
7004 Lit * lit;
7005 Var * v;
7006
7007 assert (abs (int_lit) <= (int) ps->max_var);
7008
7009 v = ps->vars + abs (int_lit);
7010 if (!v->partial)
7011 return 0;
7012
7013 lit = int2lit (ps, int_lit);
7014
7015 if (lit->val == TRUE)
7016 return 1;
7017
7018 if (lit->val == FALSE)
7019 return -1;
7020
7021 return 0;
7022 }
7023
7024 static void
7025 minautarky (PS * ps)
7026 {
7027 unsigned * occs, maxoccs, tmpoccs, npartial;
7028 int * p, * c, lit, best, val;
7029 #ifdef LOGGING
7030 int tl;
7031 #endif
7032
7033 assert (!ps->partial);
7034
7035 npartial = 0;
7036
7037 NEWN (occs, 2*ps->max_var + 1);
7038 CLRN (occs, 2*ps->max_var + 1);
7039 occs += ps->max_var;
7040 for (p = ps->soclauses; p < ps->sohead; p++)
7041 occs[*p]++;
7042 assert (occs[0] == ps->oadded);
7043
7044 for (c = ps->soclauses; c < ps->sohead; c = p + 1)
7045 {
7046 #ifdef LOGGING
7047 tl = 0;
7048 #endif
7049 best = 0;
7050 maxoccs = 0;
7051 for (p = c; (lit = *p); p++)
7052 {
7053 val = tderef (ps, lit);
7054 if (val < 0)
7055 continue;
7056 if (val > 0)
7057 {
7058 #ifdef LOGGING
7059 tl = 1;
7060 #endif
7061 best = lit;
7062 maxoccs = occs[lit];
7063 }
7064
7065 val = pderef (ps, lit);
7066 if (val > 0)
7067 break;
7068 if (val < 0)
7069 continue;
7070 val = int2lit (ps, lit)->val;
7071 assert (val);
7072 if (val < 0)
7073 continue;
7074 tmpoccs = occs[lit];
7075 if (best && tmpoccs <= maxoccs)
7076 continue;
7077 best = lit;
7078 maxoccs = tmpoccs;
7079 }
7080 if (!lit)
7081 {
7082 assert (best);
7083 LOG ( fprintf (ps->out, "%sautark %d with %d occs%s\n",
7084 ps->prefix, best, maxoccs, tl ? " (top)" : ""));
7085 ps->vars[abs (best)].partial = 1;
7086 npartial++;
7087 }
7088 for (p = c; (lit = *p); p++)
7089 {
7090 assert (occs[lit] > 0);
7091 occs[lit]--;
7092 }
7093 }
7094 occs -= ps->max_var;
7095 DELETEN (occs, 2*ps->max_var + 1);
7096 ps->partial = 1;
7097
7098 if (ps->verbosity)
7099 fprintf (ps->out,
7100 "%sautarky of size %u out of %u satisfying all clauses (%.1f%%)\n",
7101 ps->prefix, npartial, ps->max_var, PERCENT (npartial, ps->max_var));
7102 }
7103
7104 void
7105 picosat_assume (PS * ps, int int_lit)
7106 {
7107 Lit *lit;
7108
7109 if (ps->measurealltimeinlib)
7110 enter (ps);
7111 else
7112 check_ready (ps);
7113
7114 if (ps->state != READY)
7115 reset_incremental_usage (ps);
7116
7117 assume_contexts (ps);
7118 lit = import_lit (ps, int_lit, 1);
7119 assume (ps, lit);
7120
7121 if (ps->measurealltimeinlib)
7122 leave (ps);
7123 }
7124
7125 int
7126 picosat_sat (PS * ps, int l)
7127 {
7128 int res;
7129 char ch;
7130
7131 enter (ps);
7132
7133 ps->calls++;
7134 LOG ( fprintf (ps->out, "%sSTART call %u\n", ps->prefix, ps->calls));
7135
7136 if (ps->added < ps->ahead)
7137 {
7138 #ifndef NADC
7139 if (ps->addingtoado)
7140 ABORT ("API usage: incomplete all different constraint");
7141 else
7142 #endif
7143 ABORT ("API usage: incomplete clause");
7144 }
7145
7146 if (ps->state != READY)
7147 reset_incremental_usage (ps);
7148
7149 assume_contexts (ps);
7150
7151 res = sat (ps, l);
7152
7153 assert (ps->state == READY);
7154
7155 switch (res)
7156 {
7157 case PICOSAT_UNSATISFIABLE:
7158 ch = '0';
7159 ps->state = UNSAT;
7160 break;
7161 case PICOSAT_SATISFIABLE:
7162 ch = '1';
7163 ps->state = SAT;
7164 break;
7165 default:
7166 ch = '?';
7167 ps->state = UNKNOWN;
7168 break;
7169 }
7170
7171 if (ps->verbosity)
7172 {
7173 report (ps, 1, ch);
7174 rheader (ps);
7175 }
7176
7177 leave (ps);
7178 LOG ( fprintf (ps->out, "%sEND call %u result %d\n", ps->prefix, ps->calls, res));
7179
7180 ps->last_sat_call_result = res;
7181
7182 return res;
7183 }
7184
7185 int
7186 picosat_res (PS * ps)
7187 {
7188 return ps->last_sat_call_result;
7189 }
7190
7191 int
7192 picosat_deref (PS * ps, int int_lit)
7193 {
7194 Lit *lit;
7195
7196 check_ready (ps);
7197 check_sat_state (ps);
7198 ABORTIF (!int_lit, "API usage: can not deref zero literal");
7199 ABORTIF (ps->mtcls, "API usage: deref after empty clause generated");
7200
7201 #ifdef STATS
7202 ps->derefs++;
7203 #endif
7204
7205 if (abs (int_lit) > (int) ps->max_var)
7206 return 0;
7207
7208 lit = int2lit (ps, int_lit);
7209
7210 if (lit->val == TRUE)
7211 return 1;
7212
7213 if (lit->val == FALSE)
7214 return -1;
7215
7216 return 0;
7217 }
7218
7219 int
7220 picosat_deref_toplevel (PS * ps, int int_lit)
7221 {
7222 check_ready (ps);
7223 ABORTIF (!int_lit, "API usage: can not deref zero literal");
7224
7225 #ifdef STATS
7226 ps->derefs++;
7227 #endif
7228 if (abs (int_lit) > (int) ps->max_var)
7229 return 0;
7230
7231 return tderef (ps, int_lit);
7232 }
7233
7234 int
7235 picosat_inconsistent (PS * ps)
7236 {
7237 check_ready (ps);
7238 return ps->mtcls != 0;
7239 }
7240
7241 int
7242 picosat_corelit (PS * ps, int int_lit)
7243 {
7244 check_ready (ps);
7245 check_unsat_state (ps);
7246 ABORTIF (!int_lit, "API usage: zero literal can not be in core");
7247
7248 assert (ps->mtcls || ps->failed_assumption);
7249
7250 #ifdef TRACE
7251 {
7252 int res = 0;
7253 ABORTIF (!ps->trace, "tracing disabled");
7254 if (ps->measurealltimeinlib)
7255 enter (ps);
7256 core (ps);
7257 if (abs (int_lit) <= (int) ps->max_var)
7258 res = ps->vars[abs (int_lit)].core;
7259 assert (!res || ps->failed_assumption || ps->vars[abs (int_lit)].used);
7260 if (ps->measurealltimeinlib)
7261 leave (ps);
7262 return res;
7263 }
7264 #else
7265 ABORT ("compiled without trace support");
7266 return 0;
7267 #endif
7268 }
7269
7270 int
7271 picosat_coreclause (PS * ps, int ocls)
7272 {
7273 check_ready (ps);
7274 check_unsat_state (ps);
7275
7276 ABORTIF (ocls < 0, "API usage: negative original clause index");
7277 ABORTIF (ocls >= (int)ps->oadded, "API usage: original clause index exceeded");
7278
7279 assert (ps->mtcls || ps->failed_assumption);
7280
7281 #ifdef TRACE
7282 {
7283 Cls ** clsptr, * c;
7284 int res = 0;
7285
7286 ABORTIF (!ps->trace, "tracing disabled");
7287 if (ps->measurealltimeinlib)
7288 enter (ps);
7289 core (ps);
7290 clsptr = ps->oclauses + ocls;
7291 assert (clsptr < ps->ohead);
7292 c = *clsptr;
7293 if (c)
7294 res = c->core;
7295 if (ps->measurealltimeinlib)
7296 leave (ps);
7297
7298 return res;
7299 }
7300 #else
7301 ABORT ("compiled without trace support");
7302 return 0;
7303 #endif
7304 }
7305
7306 int
7307 picosat_failed_assumption (PS * ps, int int_lit)
7308 {
7309 Lit * lit;
7310 Var * v;
7311 ABORTIF (!int_lit, "API usage: zero literal as assumption");
7312 check_ready (ps);
7313 check_unsat_state (ps);
7314 if (ps->mtcls)
7315 return 0;
7316 assert (ps->failed_assumption);
7317 if (abs (int_lit) > (int) ps->max_var)
7318 return 0;
7319 if (!ps->extracted_all_failed_assumptions)
7320 extract_all_failed_assumptions (ps);
7321 lit = import_lit (ps, int_lit, 1);
7322 v = LIT2VAR (lit);
7323 return v->failed;
7324 }
7325
7326 int
7327 picosat_failed_context (PS * ps, int int_lit)
7328 {
7329 Lit * lit;
7330 Var * v;
7331 ABORTIF (!int_lit, "API usage: zero literal as context");
7332 ABORTIF (abs (int_lit) > (int) ps->max_var, "API usage: invalid context");
7333 check_ready (ps);
7334 check_unsat_state (ps);
7335 assert (ps->failed_assumption);
7336 if (!ps->extracted_all_failed_assumptions)
7337 extract_all_failed_assumptions (ps);
7338 lit = import_lit (ps, int_lit, 0);
7339 v = LIT2VAR (lit);
7340 return v->failed;
7341 }
7342
7343 const int *
7344 picosat_failed_assumptions (PS * ps)
7345 {
7346 Lit ** p, * lit;
7347 Var * v;
7348 int ilit;
7349
7350 ps->falshead = ps->fals;
7351 check_ready (ps);
7352 check_unsat_state (ps);
7353 if (!ps->mtcls)
7354 {
7355 assert (ps->failed_assumption);
7356 if (!ps->extracted_all_failed_assumptions)
7357 extract_all_failed_assumptions (ps);
7358
7359 for (p = ps->als; p < ps->alshead; p++)
7360 {
7361 lit = *p;
7362 v = LIT2VAR (*p);
7363 if (!v->failed)
7364 continue;
7365 ilit = LIT2INT (lit);
7366 if (ps->falshead == ps->eofals)
7367 ENLARGE (ps->fals, ps->falshead, ps->eofals);
7368 *ps->falshead++ = ilit;
7369 }
7370 }
7371 if (ps->falshead == ps->eofals)
7372 ENLARGE (ps->fals, ps->falshead, ps->eofals);
7373 *ps->falshead++ = 0;
7374 return ps->fals;
7375 }
7376
7377 const int *
7378 picosat_mus_assumptions (PS * ps, void * s, void (*cb)(void*,const int*), int fix)
7379 {
7380 int i, j, ilit, len, nwork, * work, res;
7381 signed char * redundant;
7382 Lit ** p, * lit;
7383 int failed;
7384 Var * v;
7385 #ifndef NDEBUG
7386 int oldlen;
7387 #endif
7388 #ifndef RCODE
7389 int norig = ps->alshead - ps->als;
7390 #endif
7391
7392 check_ready (ps);
7393 check_unsat_state (ps);
7394 len = 0;
7395 if (!ps->mtcls)
7396 {
7397 assert (ps->failed_assumption);
7398 if (!ps->extracted_all_failed_assumptions)
7399 extract_all_failed_assumptions (ps);
7400
7401 for (p = ps->als; p < ps->alshead; p++)
7402 if (LIT2VAR (*p)->failed)
7403 len++;
7404 }
7405
7406 if (ps->mass)
7407 DELETEN (ps->mass, ps->szmass);
7408 ps->szmass = len + 1;
7409 NEWN (ps->mass, ps->szmass);
7410
7411 i = 0;
7412 for (p = ps->als; p < ps->alshead; p++)
7413 {
7414 lit = *p;
7415 v = LIT2VAR (lit);
7416 if (!v->failed)
7417 continue;
7418 ilit = LIT2INT (lit);
7419 assert (i < len);
7420 ps->mass[i++] = ilit;
7421 }
7422 assert (i == len);
7423 ps->mass[i] = 0;
7424 if (ps->verbosity)
7425 fprintf (ps->out,
7426 "%sinitial set of failed assumptions of size %d out of %d (%.0f%%)\n",
7427 ps->prefix, len, norig, PERCENT (len, norig));
7428 if (cb)
7429 cb (s, ps->mass);
7430
7431 nwork = len;
7432 NEWN (work, nwork);
7433 for (i = 0; i < len; i++)
7434 work[i] = ps->mass[i];
7435
7436 NEWN (redundant, nwork);
7437 CLRN (redundant, nwork);
7438
7439 for (i = 0; i < nwork; i++)
7440 {
7441 if (redundant[i])
7442 continue;
7443
7444 if (ps->verbosity > 1)
7445 fprintf (ps->out,
7446 "%strying to drop %d%s assumption %d\n",
7447 ps->prefix, i, enumstr (i), work[i]);
7448 for (j = 0; j < nwork; j++)
7449 {
7450 if (i == j) continue;
7451 if (j < i && fix) continue;
7452 if (redundant[j]) continue;
7453 picosat_assume (ps, work[j]);
7454 }
7455
7456 res = picosat_sat (ps, -1);
7457 if (res == 10)
7458 {
7459 if (ps->verbosity > 1)
7460 fprintf (ps->out,
7461 "%sfailed to drop %d%s assumption %d\n",
7462 ps->prefix, i, enumstr (i), work[i]);
7463
7464 if (fix)
7465 {
7466 picosat_add (ps, work[i]);
7467 picosat_add (ps, 0);
7468 }
7469 }
7470 else
7471 {
7472 assert (res == 20);
7473 if (ps->verbosity > 1)
7474 fprintf (ps->out,
7475 "%ssuceeded to drop %d%s assumption %d\n",
7476 ps->prefix, i, enumstr (i), work[i]);
7477 redundant[i] = 1;
7478 for (j = 0; j < nwork; j++)
7479 {
7480 failed = picosat_failed_assumption (ps, work[j]);
7481 if (j <= i)
7482 {
7483 assert ((j < i && fix) || redundant[j] == !failed);
7484 continue;
7485 }
7486
7487 if (!failed)
7488 {
7489 redundant[j] = -1;
7490 if (ps->verbosity > 1)
7491 fprintf (ps->out,
7492 "%salso suceeded to drop %d%s assumption %d\n",
7493 ps->prefix, j, enumstr (j), work[j]);
7494 }
7495 }
7496
7497 #ifndef NDEBUG
7498 oldlen = len;
7499 #endif
7500 len = 0;
7501 for (j = 0; j < nwork; j++)
7502 if (!redundant[j])
7503 ps->mass[len++] = work[j];
7504 ps->mass[len] = 0;
7505 assert (len < oldlen);
7506
7507 if (fix)
7508 {
7509 picosat_add (ps, -work[i]);
7510 picosat_add (ps, 0);
7511 }
7512
7513 #ifndef NDEBUG
7514 for (j = 0; j <= i; j++)
7515 assert (redundant[j] >= 0);
7516 #endif
7517 for (j = i + 1; j < nwork; j++)
7518 {
7519 if (redundant[j] >= 0)
7520 continue;
7521
7522 if (fix)
7523 {
7524 picosat_add (ps, -work[j]);
7525 picosat_add (ps, 0);
7526 }
7527
7528 redundant[j] = 1;
7529 }
7530
7531 if (ps->verbosity)
7532 fprintf (ps->out,
7533 "%sreduced set of failed assumptions of size %d out of %d (%.0f%%)\n",
7534 ps->prefix, len, norig, PERCENT (len, norig));
7535 if (cb)
7536 cb (s, ps->mass);
7537 }
7538 }
7539
7540 DELETEN (work, nwork);
7541 DELETEN (redundant, nwork);
7542
7543 if (ps->verbosity)
7544 {
7545 fprintf (ps->out, "%sreinitializing unsat state\n", ps->prefix);
7546 fflush (ps->out);
7547 }
7548
7549 for (i = 0; i < len; i++)
7550 picosat_assume (ps, ps->mass[i]);
7551
7552 #ifndef NDEBUG
7553 res =
7554 #endif
7555 picosat_sat (ps, -1);
7556 assert (res == 20);
7557
7558 if (!ps->mtcls)
7559 {
7560 assert (!ps->extracted_all_failed_assumptions);
7561 extract_all_failed_assumptions (ps);
7562 }
7563
7564 return ps->mass;
7565 }
7566
7567 static const int *
7568 mss (PS * ps, int * a, int size)
7569 {
7570 int i, j, k, res;
7571
7572 assert (!ps->mtcls);
7573
7574 if (ps->szmssass)
7575 DELETEN (ps->mssass, ps->szmssass);
7576
7577 ps->szmssass = 0;
7578 ps->mssass = 0;
7579
7580 ps->szmssass = size + 1;
7581 NEWN (ps->mssass, ps->szmssass);
7582
7583 LOG ( fprintf (ps->out, "%ssearch MSS over %d assumptions\n", ps->prefix, size));
7584
7585 k = 0;
7586 for (i = k; i < size; i++)
7587 {
7588 for (j = 0; j < k; j++)
7589 picosat_assume (ps, ps->mssass[j]);
7590
7591 LOG ( fprintf (ps->out,
7592 "%strying to add assumption %d to MSS : %d\n",
7593 ps->prefix, i, a[i]));
7594
7595 picosat_assume (ps, a[i]);
7596
7597 res = picosat_sat (ps, -1);
7598 if (res == 10)
7599 {
7600 LOG ( fprintf (ps->out,
7601 "%sadding assumption %d to MSS : %d\n", ps->prefix, i, a[i]));
7602
7603 ps->mssass[k++] = a[i];
7604
7605 for (j = i + 1; j < size; j++)
7606 {
7607 if (picosat_deref (ps, a[j]) <= 0)
7608 continue;
7609
7610 LOG ( fprintf (ps->out,
7611 "%salso adding assumption %d to MSS : %d\n",
7612 ps->prefix, j, a[j]));
7613
7614 ps->mssass[k++] = a[j];
7615
7616 if (++i != j)
7617 {
7618 int tmp = a[i];
7619 a[i] = a[j];
7620 a[j] = tmp;
7621 }
7622 }
7623 }
7624 else
7625 {
7626 assert (res == 20);
7627
7628 LOG ( fprintf (ps->out,
7629 "%signoring assumption %d in MSS : %d\n", ps->prefix, i, a[i]));
7630 }
7631 }
7632 ps->mssass[k] = 0;
7633 LOG ( fprintf (ps->out, "%sfound MSS of size %d\n", ps->prefix, k));
7634
7635 return ps->mssass;
7636 }
7637
7638 static void
7639 reassume (PS * ps, const int * a, int size)
7640 {
7641 int i;
7642 LOG ( fprintf (ps->out, "%sreassuming all assumptions\n", ps->prefix));
7643 for (i = 0; i < size; i++)
7644 picosat_assume (ps, a[i]);
7645 }
7646
7647 const int *
7648 picosat_maximal_satisfiable_subset_of_assumptions (PS * ps)
7649 {
7650 const int * res;
7651 int i, *a, size;
7652
7653 ABORTIF (ps->mtcls,
7654 "API usage: CNF inconsistent (use 'picosat_inconsistent')");
7655
7656 enter (ps);
7657
7658 size = ps->alshead - ps->als;
7659 NEWN (a, size);
7660
7661 for (i = 0; i < size; i++)
7662 a[i] = LIT2INT (ps->als[i]);
7663
7664 res = mss (ps, a, size);
7665 reassume (ps, a, size);
7666
7667 DELETEN (a, size);
7668
7669 leave (ps);
7670
7671 return res;
7672 }
7673
7674 static void
7675 check_mss_flags_clean (PS * ps)
7676 {
7677 #ifndef NDEBUG
7678 unsigned i;
7679 for (i = 1; i <= ps->max_var; i++)
7680 {
7681 assert (!ps->vars[i].msspos);
7682 assert (!ps->vars[i].mssneg);
7683 }
7684 #else
7685 (void) ps;
7686 #endif
7687 }
7688
7689 static void
7690 push_mcsass (PS * ps, int lit)
7691 {
7692 if (ps->nmcsass == ps->szmcsass)
7693 {
7694 ps->szmcsass = ps->szmcsass ? 2*ps->szmcsass : 1;
7695 RESIZEN (ps->mcsass, ps->nmcsass, ps->szmcsass);
7696 }
7697
7698 ps->mcsass[ps->nmcsass++] = lit;
7699 }
7700
7701 static const int *
7702 next_mss (PS * ps, int mcs)
7703 {
7704 int i, *a, size, mssize, mcsize, lit, inmss;
7705 const int * res, * p;
7706 Var * v;
7707
7708 if (ps->mtcls) return 0;
7709
7710 check_mss_flags_clean (ps);
7711
7712 if (mcs && ps->mcsass)
7713 {
7714 DELETEN (ps->mcsass, ps->szmcsass);
7715 ps->nmcsass = ps->szmcsass = 0;
7716 ps->mcsass = 0;
7717 }
7718
7719 size = ps->alshead - ps->als;
7720 NEWN (a, size);
7721
7722 for (i = 0; i < size; i++)
7723 a[i] = LIT2INT (ps->als[i]);
7724
7725 (void) picosat_sat (ps, -1);
7726
7727 //TODO short cut for 'picosat_res () == 10'?
7728
7729 if (ps->mtcls)
7730 {
7731 assert (picosat_res (ps) == 20);
7732 res = 0;
7733 goto DONE;
7734 }
7735
7736 res = mss (ps, a, size);
7737
7738 if (ps->mtcls)
7739 {
7740 res = 0;
7741 goto DONE;
7742 }
7743
7744 for (p = res; (lit = *p); p++)
7745 {
7746 v = ps->vars + abs (lit);
7747 if (lit < 0)
7748 {
7749 assert (!v->msspos);
7750 v->mssneg = 1;
7751 }
7752 else
7753 {
7754 assert (!v->mssneg);
7755 v->msspos = 1;
7756 }
7757 }
7758
7759 mssize = p - res;
7760 mcsize = INT_MIN;
7761
7762 for (i = 0; i < size; i++)
7763 {
7764 lit = a[i];
7765 v = ps->vars + abs (lit);
7766 if (lit > 0 && v->msspos)
7767 inmss = 1;
7768 else if (lit < 0 && v->mssneg)
7769 inmss = 1;
7770 else
7771 inmss = 0;
7772
7773 if (mssize < mcsize)
7774 {
7775 if (inmss)
7776 picosat_add (ps, -lit);
7777 }
7778 else
7779 {
7780 if (!inmss)
7781 picosat_add (ps, lit);
7782 }
7783
7784 if (!inmss && mcs)
7785 push_mcsass (ps, lit);
7786 }
7787 picosat_add (ps, 0);
7788 if (mcs)
7789 push_mcsass (ps, 0);
7790
7791 for (i = 0; i < size; i++)
7792 {
7793 lit = a[i];
7794 v = ps->vars + abs (lit);
7795 v->msspos = 0;
7796 v->mssneg = 0;
7797 }
7798
7799 DONE:
7800
7801 reassume (ps, a, size);
7802 DELETEN (a, size);
7803
7804 return res;
7805 }
7806
7807 const int *
7808 picosat_next_maximal_satisfiable_subset_of_assumptions (PS * ps)
7809 {
7810 const int * res;
7811 enter (ps);
7812 res = next_mss (ps, 0);
7813 leave (ps);
7814 return res;
7815 }
7816
7817 const int *
7818 picosat_next_minimal_correcting_subset_of_assumptions (PS * ps)
7819 {
7820 const int * res, * tmp;
7821 enter (ps);
7822 tmp = next_mss (ps, 1);
7823 res = tmp ? ps->mcsass : 0;
7824 leave (ps);
7825 return res;
7826 }
7827
7828 const int *
7829 picosat_humus (PS * ps,
7830 void (*callback)(void*state,int nmcs,int nhumus),
7831 void * state)
7832 {
7833 int lit, nmcs, j, nhumus;
7834 const int * mcs, * p;
7835 unsigned i;
7836 Var * v;
7837 enter (ps);
7838 #ifndef NDEBUG
7839 for (i = 1; i <= ps->max_var; i++)
7840 {
7841 v = ps->vars + i;
7842 assert (!v->humuspos);
7843 assert (!v->humusneg);
7844 }
7845 #endif
7846 nhumus = nmcs = 0;
7847 while ((mcs = picosat_next_minimal_correcting_subset_of_assumptions (ps)))
7848 {
7849 for (p = mcs; (lit = *p); p++)
7850 {
7851 v = ps->vars + abs (lit);
7852 if (lit < 0)
7853 {
7854 if (!v->humusneg)
7855 {
7856 v->humusneg = 1;
7857 nhumus++;
7858 }
7859 }
7860 else
7861 {
7862 if (!v->humuspos)
7863 {
7864 v->humuspos = 1;
7865 nhumus++;
7866 }
7867 }
7868 }
7869 nmcs++;
7870 LOG ( fprintf (ps->out,
7871 "%smcs %d of size %d humus %d\n",
7872 ps->prefix, nmcs, (int)(p - mcs), nhumus));
7873 if (callback)
7874 callback (state, nmcs, nhumus);
7875 }
7876 assert (!ps->szhumus);
7877 ps->szhumus = 1;
7878 for (i = 1; i <= ps->max_var; i++)
7879 {
7880 v = ps->vars + i;
7881 if (v->humuspos)
7882 ps->szhumus++;
7883 if (v->humusneg)
7884 ps->szhumus++;
7885 }
7886 assert (nhumus + 1 == ps->szhumus);
7887 NEWN (ps->humus, ps->szhumus);
7888 j = 0;
7889 for (i = 1; i <= ps->max_var; i++)
7890 {
7891 v = ps->vars + i;
7892 if (v->humuspos)
7893 {
7894 assert (j < nhumus);
7895 ps->humus[j++] = (int) i;
7896 }
7897 if (v->humusneg)
7898 {
7899 assert (j < nhumus);
7900 assert (i < INT_MAX);
7901 ps->humus[j++] = - (int) i;
7902 }
7903 }
7904 assert (j == nhumus);
7905 assert (j < ps->szhumus);
7906 ps->humus[j] = 0;
7907 leave (ps);
7908 return ps->humus;
7909 }
7910
7911 int
7912 picosat_usedlit (PS * ps, int int_lit)
7913 {
7914 int res;
7915 check_ready (ps);
7916 check_sat_or_unsat_or_unknown_state (ps);
7917 ABORTIF (!int_lit, "API usage: zero literal can not be used");
7918 int_lit = abs (int_lit);
7919 res = (int_lit <= (int) ps->max_var) ? ps->vars[int_lit].used : 0;
7920 return res;
7921 }
7922
7923 void
7924 picosat_write_clausal_core (PS * ps, FILE * file)
7925 {
7926 check_trace_support_and_execute (ps, file, write_core_wrapper, 0);
7927 }
7928
7929 void
7930 picosat_write_compact_trace (PS * ps, FILE * file)
7931 {
7932 check_trace_support_and_execute (ps, file, write_trace,
7933 COMPACT_TRACECHECK_TRACE_FMT);
7934 }
7935
7936 void
7937 picosat_write_extended_trace (PS * ps, FILE * file)
7938 {
7939 check_trace_support_and_execute (ps, file, write_trace,
7940 EXTENDED_TRACECHECK_TRACE_FMT);
7941 }
7942
7943 void
7944 picosat_write_rup_trace (PS * ps, FILE * file)
7945 {
7946 check_trace_support_and_execute (ps, file, write_trace, RUP_TRACE_FMT);
7947 }
7948
7949 size_t
7950 picosat_max_bytes_allocated (PS * ps)
7951 {
7952 check_ready (ps);
7953 return ps->max_bytes;
7954 }
7955
7956 void
7957 picosat_set_propagation_limit (PS * ps, unsigned long long l)
7958 {
7959 ps->lpropagations = l;
7960 }
7961
7962 unsigned long long
7963 picosat_propagations (PS * ps)
7964 {
7965 return ps->propagations;
7966 }
7967
7968 unsigned long long
7969 picosat_visits (PS * ps)
7970 {
7971 return ps->visits;
7972 }
7973
7974 unsigned long long
7975 picosat_decisions (PS * ps)
7976 {
7977 return ps->decisions;
7978 }
7979
7980 int
7981 picosat_variables (PS * ps)
7982 {
7983 check_ready (ps);
7984 return (int) ps->max_var;
7985 }
7986
7987 int
7988 picosat_added_original_clauses (PS * ps)
7989 {
7990 check_ready (ps);
7991 return (int) ps->oadded;
7992 }
7993
7994 void
7995 picosat_stats (PS * ps)
7996 {
7997 #ifndef RCODE
7998 unsigned redlits;
7999 #endif
8000 #ifdef STATS
8001 check_ready (ps);
8002 assert (ps->sdecisions + ps->rdecisions + ps->assumptions == ps->decisions);
8003 #endif
8004 if (ps->calls > 1)
8005 fprintf (ps->out, "%s%u calls\n", ps->prefix, ps->calls);
8006 if (ps->contexts)
8007 {
8008 fprintf (ps->out, "%s%u contexts", ps->prefix, ps->contexts);
8009 #ifdef STATS
8010 fprintf (ps->out, " %u internal variables", ps->internals);
8011 #endif
8012 fprintf (ps->out, "\n");
8013 }
8014 fprintf (ps->out, "%s%u iterations\n", ps->prefix, ps->iterations);
8015 fprintf (ps->out, "%s%u restarts", ps->prefix, ps->restarts);
8016 #ifdef STATS
8017 fprintf (ps->out, " (%u skipped)", ps->skippedrestarts);
8018 #endif
8019 fputc ('\n', ps->out);
8020 #ifndef NFL
8021 fprintf (ps->out, "%s%u failed literals", ps->prefix, ps->failedlits);
8022 #ifdef STATS
8023 fprintf (ps->out,
8024 ", %u calls, %u rounds, %llu propagations",
8025 ps->flcalls, ps->flrounds, ps->flprops);
8026 #endif
8027 fputc ('\n', ps->out);
8028 #ifdef STATS
8029 fprintf (ps->out,
8030 "%sfl: %u = %.1f%% implicit, %llu oopsed, %llu tried, %llu skipped\n",
8031 ps->prefix,
8032 ps->ifailedlits, PERCENT (ps->ifailedlits, ps->failedlits),
8033 ps->floopsed, ps->fltried, ps->flskipped);
8034 #endif
8035 #endif
8036 fprintf (ps->out, "%s%u conflicts", ps->prefix, ps->conflicts);
8037 #ifdef STATS
8038 fprintf (ps->out, " (%u uips = %.1f%%)\n", ps->uips, PERCENT(ps->uips,ps->conflicts));
8039 #else
8040 fputc ('\n', ps->out);
8041 #endif
8042 #ifndef NADC
8043 fprintf (ps->out, "%s%u adc conflicts\n", ps->prefix, ps->adoconflicts);
8044 #endif
8045 #ifdef STATS
8046 fprintf (ps->out, "%s%llu dereferenced literals\n", ps->prefix, ps->derefs);
8047 #endif
8048 fprintf (ps->out, "%s%u decisions", ps->prefix, ps->decisions);
8049 #ifdef STATS
8050 fprintf (ps->out, " (%u random = %.2f%%",
8051 ps->rdecisions, PERCENT (ps->rdecisions, ps->decisions));
8052 fprintf (ps->out, ", %u assumptions", ps->assumptions);
8053 fputc (')', ps->out);
8054 #endif
8055 fputc ('\n', ps->out);
8056 #ifdef STATS
8057 fprintf (ps->out,
8058 "%s%u static phase decisions (%.1f%% of all variables)\n",
8059 ps->prefix,
8060 ps->staticphasedecisions, PERCENT (ps->staticphasedecisions, ps->max_var));
8061 #endif
8062 fprintf (ps->out, "%s%u fixed variables\n", ps->prefix, ps->fixed);
8063 assert (ps->nonminimizedllits >= ps->minimizedllits);
8064 #ifndef RCODE
8065 redlits = ps->nonminimizedllits - ps->minimizedllits;
8066 #endif
8067 fprintf (ps->out, "%s%u learned literals\n", ps->prefix, ps->llitsadded);
8068 fprintf (ps->out, "%s%.1f%% deleted literals\n",
8069 ps->prefix, PERCENT (redlits, ps->nonminimizedllits));
8070
8071 #ifdef STATS
8072 #ifdef TRACE
8073 fprintf (ps->out,
8074 "%s%llu antecedents (%.1f antecedents per clause",
8075 ps->prefix, ps->antecedents, AVERAGE (ps->antecedents, ps->conflicts));
8076 if (ps->trace)
8077 fprintf (ps->out, ", %.1f bytes/antecedent)", AVERAGE (ps->znts, ps->antecedents));
8078 fputs (")\n", ps->out);
8079 #endif
8080
8081 fprintf (ps->out, "%s%llu propagations (%.1f propagations per decision)\n",
8082 ps->prefix, ps->propagations, AVERAGE (ps->propagations, ps->decisions));
8083 fprintf (ps->out, "%s%llu visits (%.1f per propagation)\n",
8084 ps->prefix, ps->visits, AVERAGE (ps->visits, ps->propagations));
8085 fprintf (ps->out,
8086 "%s%llu binary clauses visited (%.1f%% %.1f per propagation)\n",
8087 ps->prefix, ps->bvisits,
8088 PERCENT (ps->bvisits, ps->visits),
8089 AVERAGE (ps->bvisits, ps->propagations));
8090 fprintf (ps->out,
8091 "%s%llu ternary clauses visited (%.1f%% %.1f per propagation)\n",
8092 ps->prefix, ps->tvisits,
8093 PERCENT (ps->tvisits, ps->visits),
8094 AVERAGE (ps->tvisits, ps->propagations));
8095 fprintf (ps->out,
8096 "%s%llu large clauses visited (%.1f%% %.1f per propagation)\n",
8097 ps->prefix, ps->lvisits,
8098 PERCENT (ps->lvisits, ps->visits),
8099 AVERAGE (ps->lvisits, ps->propagations));
8100 fprintf (ps->out, "%s%llu other true (%.1f%% of visited clauses)\n",
8101 ps->prefix, ps->othertrue, PERCENT (ps->othertrue, ps->visits));
8102 fprintf (ps->out,
8103 "%s%llu other true in binary clauses (%.1f%%)"
8104 ", %llu upper (%.1f%%)\n",
8105 ps->prefix, ps->othertrue2, PERCENT (ps->othertrue2, ps->othertrue),
8106 ps->othertrue2u, PERCENT (ps->othertrue2u, ps->othertrue2));
8107 fprintf (ps->out,
8108 "%s%llu other true in large clauses (%.1f%%)"
8109 ", %llu upper (%.1f%%)\n",
8110 ps->prefix, ps->othertruel, PERCENT (ps->othertruel, ps->othertrue),
8111 ps->othertruelu, PERCENT (ps->othertruelu, ps->othertruel));
8112 fprintf (ps->out, "%s%llu ternary and large traversals (%.1f per visit)\n",
8113 ps->prefix, ps->traversals, AVERAGE (ps->traversals, ps->visits));
8114 fprintf (ps->out, "%s%llu large traversals (%.1f per large visit)\n",
8115 ps->prefix, ps->ltraversals, AVERAGE (ps->ltraversals, ps->lvisits));
8116 fprintf (ps->out, "%s%llu assignments\n", ps->prefix, ps->assignments);
8117 #else
8118 fprintf (ps->out, "%s%llu propagations\n", ps->prefix, picosat_propagations (ps));
8119 fprintf (ps->out, "%s%llu visits\n", ps->prefix, picosat_visits (ps));
8120 #endif
8121 fprintf (ps->out, "%s%.1f%% variables used\n", ps->prefix, PERCENT (ps->vused, ps->max_var));
8122
8123 sflush (ps);
8124 fprintf (ps->out, "%s%.1f seconds in library\n", ps->prefix, ps->seconds);
8125 fprintf (ps->out, "%s%.1f megaprops/second\n",
8126 ps->prefix, AVERAGE (ps->propagations / 1e6f, ps->seconds));
8127 fprintf (ps->out, "%s%.1f megavisits/second\n",
8128 ps->prefix, AVERAGE (ps->visits / 1e6f, ps->seconds));
8129 fprintf (ps->out, "%sprobing %.1f seconds %.0f%%\n",
8130 ps->prefix, ps->flseconds, PERCENT (ps->flseconds, ps->seconds));
8131 #ifdef STATS
8132 fprintf (ps->out,
8133 "%srecycled %.1f MB in %u reductions\n",
8134 ps->prefix, ps->rrecycled / (double) (1 << 20), ps->reductions);
8135 fprintf (ps->out,
8136 "%srecycled %.1f MB in %u simplifications\n",
8137 ps->prefix, ps->srecycled / (double) (1 << 20), ps->simps);
8138 #else
8139 fprintf (ps->out, "%s%u simplifications\n", ps->prefix, ps->simps);
8140 fprintf (ps->out, "%s%u reductions\n", ps->prefix, ps->reductions);
8141 fprintf (ps->out, "%s%.1f MB recycled\n", ps->prefix, ps->recycled / (double) (1 << 20));
8142 #endif
8143 fprintf (ps->out, "%s%.1f MB maximally allocated\n",
8144 ps->prefix, picosat_max_bytes_allocated (ps) / (double) (1 << 20));
8145 }
8146
8147 #ifndef NGETRUSAGE
8148 #include <sys/time.h>
8149 #include <sys/resource.h>
8150 #include <sys/unistd.h>
8151 #endif
8152
8153 double
8154 picosat_time_stamp (void)
8155 {
8156 double res = -1;
8157 #ifndef NGETRUSAGE
8158 struct rusage u;
8159 res = 0;
8160 if (!getrusage (RUSAGE_SELF, &u))
8161 {
8162 res += u.ru_utime.tv_sec + 1e-6 * u.ru_utime.tv_usec;
8163 res += u.ru_stime.tv_sec + 1e-6 * u.ru_stime.tv_usec;
8164 }
8165 #endif
8166 return res;
8167 }
8168
8169 double
8170 picosat_seconds (PS * ps)
8171 {
8172 check_ready (ps);
8173 return ps->seconds;
8174 }
8175
8176 void
8177 picosat_print (PS * ps, FILE * file)
8178 {
8179 #ifdef NO_BINARY_CLAUSES
8180 Lit * lit, *other, * last;
8181 Ltk * stack;
8182 #endif
8183 Lit **q, **eol;
8184 Cls **p, *c;
8185 unsigned n;
8186
8187 if (ps->measurealltimeinlib)
8188 enter (ps);
8189 else
8190 check_ready (ps);
8191
8192 n = 0;
8193 n += ps->alshead - ps->als;
8194
8195 for (p = SOC; p != EOC; p = NXC (p))
8196 {
8197 c = *p;
8198
8199 if (!c)
8200 continue;
8201
8202 #ifdef TRACE
8203 if (c->collected)
8204 continue;
8205 #endif
8206 n++;
8207 }
8208
8209 #ifdef NO_BINARY_CLAUSES
8210 last = int2lit (ps, -ps->max_var);
8211 for (lit = int2lit (ps, 1); lit <= last; lit++)
8212 {
8213 stack = LIT2IMPLS (lit);
8214 eol = stack->start + stack->count;
8215 for (q = stack->start; q < eol; q++)
8216 if (*q >= lit)
8217 n++;
8218 }
8219 #endif
8220
8221 fprintf (file, "p cnf %d %u\n", ps->max_var, n);
8222
8223 for (p = SOC; p != EOC; p = NXC (p))
8224 {
8225 c = *p;
8226 if (!c)
8227 continue;
8228
8229 #ifdef TRACE
8230 if (c->collected)
8231 continue;
8232 #endif
8233
8234 eol = end_of_lits (c);
8235 for (q = c->lits; q < eol; q++)
8236 fprintf (file, "%d ", LIT2INT (*q));
8237
8238 fputs ("0\n", file);
8239 }
8240
8241 #ifdef NO_BINARY_CLAUSES
8242 last = int2lit (ps, -ps->max_var);
8243 for (lit = int2lit (ps, 1); lit <= last; lit++)
8244 {
8245 stack = LIT2IMPLS (lit);
8246 eol = stack->start + stack->count;
8247 for (q = stack->start; q < eol; q++)
8248 if ((other = *q) >= lit)
8249 fprintf (file, "%d %d 0\n", LIT2INT (lit), LIT2INT (other));
8250 }
8251 #endif
8252
8253 {
8254 Lit **r;
8255 for (r = ps->als; r < ps->alshead; r++)
8256 fprintf (file, "%d 0\n", LIT2INT (*r));
8257 }
8258
8259 fflush (file);
8260
8261 if (ps->measurealltimeinlib)
8262 leave (ps);
8263 }
8264
8265 void
8266 picosat_enter (PS * ps)
8267 {
8268 enter (ps);
8269 }
8270
8271 void
8272 picosat_leave (PS * ps)
8273 {
8274 leave (ps);
8275 }
8276
8277 void
8278 picosat_message (PS * ps, int vlevel, const char * fmt, ...)
8279 {
8280 va_list ap;
8281
8282 if (vlevel > ps->verbosity)
8283 return;
8284
8285 fputs (ps->prefix, ps->out);
8286 va_start (ap, fmt);
8287 vfprintf (ps->out, fmt, ap);
8288 va_end (ap);
8289 fputc ('\n', ps->out);
8290 }
8291
8292 int
8293 picosat_changed (PS * ps)
8294 {
8295 int res;
8296
8297 check_ready (ps);
8298 check_sat_state (ps);
8299
8300 res = (ps->min_flipped <= ps->saved_max_var);
8301 assert (!res || ps->saved_flips != ps->flips);
8302
8303 return res;
8304 }
8305
8306 void
8307 picosat_reset_phases (PS * ps)
8308 {
8309 rebias (ps);
8310 }
8311
8312 void
8313 picosat_reset_scores (PS * ps)
8314 {
8315 Rnk * r;
8316 ps->hhead = ps->heap + 1;
8317 for (r = ps->rnks + 1; r <= ps->rnks + ps->max_var; r++)
8318 {
8319 CLR (r);
8320 hpush (ps, r);
8321 }
8322 }
8323
8324 void
8325 picosat_remove_learned (PS * ps, unsigned percentage)
8326 {
8327 enter (ps);
8328 reset_incremental_usage (ps);
8329 reduce (ps, percentage);
8330 leave (ps);
8331 }
8332
8333 void
8334 picosat_set_global_default_phase (PS * ps, int phase)
8335 {
8336 check_ready (ps);
8337 ABORTIF (phase < 0, "API usage: 'picosat_set_global_default_phase' "
8338 "with negative argument");
8339 ABORTIF (phase > 3, "API usage: 'picosat_set_global_default_phase' "
8340 "with argument > 3");
8341 ps->defaultphase = phase;
8342 }
8343
8344 void
8345 picosat_set_default_phase_lit (PS * ps, int int_lit, int phase)
8346 {
8347 unsigned newphase;
8348 Lit * lit;
8349 Var * v;
8350
8351 check_ready (ps);
8352
8353 lit = import_lit (ps, int_lit, 1);
8354 v = LIT2VAR (lit);
8355
8356 if (phase)
8357 {
8358 newphase = (int_lit < 0) == (phase < 0);
8359 v->defphase = v->phase = newphase;
8360 v->usedefphase = v->assigned = 1;
8361 }
8362 else
8363 {
8364 v->usedefphase = v->assigned = 0;
8365 }
8366 }
8367
8368 void
8369 picosat_set_more_important_lit (PS * ps, int int_lit)
8370 {
8371 Lit * lit;
8372 Var * v;
8373 Rnk * r;
8374
8375 check_ready (ps);
8376
8377 lit = import_lit (ps, int_lit, 1);
8378 v = LIT2VAR (lit);
8379 r = VAR2RNK (v);
8380
8381 ABORTIF (r->lessimportant, "can not mark variable more and less important");
8382
8383 if (r->moreimportant)
8384 return;
8385
8386 r->moreimportant = 1;
8387
8388 if (r->pos)
8389 hup (ps, r);
8390 }
8391
8392 void
8393 picosat_set_less_important_lit (PS * ps, int int_lit)
8394 {
8395 Lit * lit;
8396 Var * v;
8397 Rnk * r;
8398
8399 check_ready (ps);
8400
8401 lit = import_lit (ps, int_lit, 1);
8402 v = LIT2VAR (lit);
8403 r = VAR2RNK (v);
8404
8405 ABORTIF (r->moreimportant, "can not mark variable more and less important");
8406
8407 if (r->lessimportant)
8408 return;
8409
8410 r->lessimportant = 1;
8411
8412 if (r->pos)
8413 hdown (ps, r);
8414 }
8415
8416 #ifndef NADC
8417
8418 unsigned
8419 picosat_ado_conflicts (PS * ps)
8420 {
8421 check_ready (ps);
8422 return ps->adoconflicts;
8423 }
8424
8425 void
8426 picosat_disable_ado (PS * ps)
8427 {
8428 check_ready (ps);
8429 assert (!ps->adodisabled);
8430 ps->adodisabled = 1;
8431 }
8432
8433 void
8434 picosat_enable_ado (PS * ps)
8435 {
8436 check_ready (ps);
8437 assert (ps->adodisabled);
8438 ps->adodisabled = 0;
8439 }
8440
8441 void
8442 picosat_set_ado_conflict_limit (PS * ps, unsigned newadoconflictlimit)
8443 {
8444 check_ready (ps);
8445 ps->adoconflictlimit = newadoconflictlimit;
8446 }
8447
8448 #endif
8449
8450 void
8451 picosat_simplify (PS * ps)
8452 {
8453 enter (ps);
8454 reset_incremental_usage (ps);
8455 simplify (ps, 1);
8456 leave (ps);
8457 }
8458
8459 int
8460 picosat_haveados (void)
8461 {
8462 #ifndef NADC
8463 return 1;
8464 #else
8465 return 0;
8466 #endif
8467 }
8468
8469 void
8470 picosat_save_original_clauses (PS * ps)
8471 {
8472 if (ps->saveorig) return;
8473 ABORTIF (ps->oadded, "API usage: 'picosat_save_original_clauses' too late");
8474 ps->saveorig = 1;
8475 }
8476
8477 void picosat_set_interrupt (PicoSAT * ps,
8478 void * external_state,
8479 int (*interrupted)(void * external_state))
8480 {
8481 ps->interrupt.state = external_state;
8482 ps->interrupt.function = interrupted;
8483 }
8484
8485 int
8486 picosat_deref_partial (PS * ps, int int_lit)
8487 {
8488 check_ready (ps);
8489 check_sat_state (ps);
8490 ABORTIF (!int_lit, "API usage: can not partial deref zero literal");
8491 ABORTIF (ps->mtcls, "API usage: deref partial after empty clause generated");
8492 ABORTIF (!ps->saveorig, "API usage: 'picosat_save_original_clauses' missing");
8493
8494 #ifdef STATS
8495 ps->derefs++;
8496 #endif
8497
8498 if (!ps->partial)
8499 minautarky (ps);
8500
8501 return pderef (ps, int_lit);
8502 }
8503