1 /****************************************************************************
2 Copyright (c) 2006 - 2009, Armin Biere, Johannes Kepler University.
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:
11 The above copyright notice and this permission notice shall be included in
12 all copies or substantial portions of the Software.
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
21 ****************************************************************************/
33 /* By default code for 'all different constraints' is disabled, since 'NADC'
38 /* By default we enable failed literals, since 'NFL' is undefined.
43 /* By default we 'detach satisfied (large) clauses', e.g. NDSC undefined.
48 /* Do not use luby restart schedule instead of inner/outer.
53 // #define VISCORES /* keep this disabled */
61 #include <unistd.h> /* for 'usleep' */
65 #define MINRESTART 100 /* minimum restart interval */
66 #define MAXRESTART 1000000 /* maximum restart interval */
67 #define RDECIDE 1000 /* interval of random decisions */
68 #define FRESTART 110 /* restart increase factor in percent */
69 #define FREDUCE 110 /* reduce increase factor in percent */
70 #define FFLIPPED 10000 /* flipped reduce factor */
71 #define FFLIPPEDPREC 10000000/* flipped reduce factor precision */
74 #define NO_BINARY_CLAUSES /* store binary clauses more compactly */
77 /* For debugging purposes you may want to define 'LOGGING', which actually
78 * can be enforced by using the '--log' option for the configure script.
81 #define LOG(code) do { code; } while (0)
83 #define LOG(code) do { } while (0)
85 #define NOLOG(code) do { } while (0) /* log exception */
86 #define ONLYLOG(code) do { code; } while (0) /* force logging */
88 #define FALSE ((Val)-1)
89 #define UNDEF ((Val)0)
92 #define COMPACT_TRACECHECK_TRACE_FMT 0
93 #define EXTENDED_TRACECHECK_TRACE_FMT 1
94 #define RUP_TRACE_FMT 2
96 #define NEWN(p,n) do { (p) = new (sizeof (*(p)) * (n)); } while (0)
97 #define CLRN(p,n) do { memset ((p), 0, sizeof (*(p)) * (n)); } while (0)
98 #define CLR(p) CLRN(p,1)
99 #define DELETEN(p,n) \
100 do { delete (p, sizeof (*(p)) * (n)); (p) = 0; } while (0)
102 #define RESIZEN(p,old_num,new_num) \
104 size_t old_size = sizeof (*(p)) * (old_num); \
105 size_t new_size = sizeof (*(p)) * (new_num); \
106 (p) = resize ((p), old_size, new_size) ; \
109 #define ENLARGE(start,head,end) \
111 unsigned old_num = (unsigned)((end) - (start)); \
112 size_t new_num = old_num ? (2 * old_num) : 1; \
113 unsigned count = (head) - (start); \
114 assert ((start) <= (start)); \
115 RESIZEN((start),old_num,new_num); \
116 (head) = (start) + count; \
117 (end) = (start) + new_num; \
120 #define NOTLIT(l) (lits + (1 ^ ((l) - lits)))
122 #define LIT2IDX(l) ((unsigned)((l) - lits) / 2)
123 #define LIT2IMPLS(l) (impls + (unsigned)((l) - lits))
124 #define LIT2INT(l) (LIT2SGN(l) * LIT2IDX(l))
125 #define LIT2SGN(l) (((unsigned)((l) - lits) & 1) ? -1 : 1)
126 #define LIT2VAR(l) (vars + LIT2IDX(l))
127 #define LIT2HTPS(l) (htps + (unsigned)((l) - lits))
128 #define LIT2JWH(l) (jwh + ((l) - lits))
131 #define LIT2DHTPS(l) (dhtps + (unsigned)((l) - lits))
134 #ifdef NO_BINARY_CLAUSES
135 typedef unsigned long Wrd
;
136 #define ISLITREASON(cls) (1&(Wrd)cls)
137 #define LIT2REASON(lit) \
138 (assert (lit->val==TRUE), ((Cls*)(1 + (2*(lit - lits)))))
139 #define REASON2LIT(cls) ((Lit*)(lits + ((Wrd)cls)/2))
142 #define ENDOFCLS(c) ((void*)((c)->lits + (c)->size))
144 #define SOC ((oclauses == ohead) ? lclauses : oclauses)
146 #define NXC(p) (((p) + 1 == ohead) ? lclauses : (p) + 1)
148 #define OIDX2IDX(idx) (2 * ((idx) + 1))
149 #define LIDX2IDX(idx) (2 * (idx) + 1)
151 #define ISLIDX(idx) ((idx)&1)
153 #define IDX2OIDX(idx) (assert(!ISLIDX(idx)), (idx)/2 - 1)
154 #define IDX2LIDX(idx) (assert(ISLIDX(idx)), (idx)/2)
156 #define EXPORTIDX(idx) \
157 ((ISLIDX(idx) ? (IDX2LIDX (idx) + (ohead - oclauses)) : IDX2OIDX(idx)) + 1)
160 (assert(i), (ISLIDX(i) ? lclauses : oclauses)[(i)/2 - !ISLIDX(i)])
162 #define IDX2ZHN(i) (assert(i), (ISLIDX(i) ? zhains[(i)/2] : 0))
164 #define CLS2TRD(c) (((Trd*)(c)) - 1)
165 #define CLS2IDX(c) ((((Trd*)(c)) - 1)->idx)
168 ((Act*)((assert((c)->learned)),assert((c)->size>2),ENDOFCLS(c)))
170 #define VAR2LIT(v) (lits + 2 * ((v) - vars))
171 #define VAR2RNK(v) (rnks + ((v) - vars))
173 #define RNK2LIT(r) (lits + 2 * ((r) - rnks))
174 #define RNK2VAR(r) (vars + ((r) - rnks))
176 #define PTR2BLK(void_ptr) \
177 ((void_ptr) ? (Blk*)(((char*)(void_ptr)) - sizeof(Blk)) : 0)
179 #define AVERAGE(a,b) ((b) ? (((double)a) / (double)(b)) : 0.0)
180 #define PERCENT(a,b) (100.0 * AVERAGE(a,b))
184 fputs ("*** picosat: " msg "\n", stderr); \
188 #define ABORTIF(cond,msg) \
190 if (!(cond)) break; \
194 #define ZEROFLT (0x00000000u)
195 #define INFFLT (0xffffffffu)
197 #define FLTCARRY (1u << 25)
198 #define FLTMSB (1u << 24)
199 #define FLTMAXMANTISSA (FLTMSB - 1)
201 #define FLTMANTISSA(d) ((d) & FLTMAXMANTISSA)
202 #define FLTEXPONENT(d) ((int)((d) >> 24) - 128)
204 #define FLTMINEXPONENT (-128)
205 #define FLTMAXEXPONENT (127)
207 #define cmpswapflt(a,b) \
218 #define unpackflt(u,m,e) \
220 (m) = FLTMANTISSA(u); \
221 (e) = FLTEXPONENT(u); \
225 #define INSERTION_SORT_LIMIT 10
227 #define internal_sorting_swap(T,p,q) \
234 #define internal_sorting_cmpswap(T,cmp,p,q) \
236 if ((cmp) (*(p), *(q)) > 0) \
237 internal_sorting_swap (T, p, q); \
240 #define internal_quicksort_partition(T,cmp,a,l,r) \
244 i = (l) - 1; /* result in 'i' */ \
249 while ((cmp) ((a)[++i], pivot) < 0) \
251 while ((cmp) (pivot, (a)[--j]) < 0) \
256 internal_sorting_swap (T, (a) + i, (a) + j); \
258 internal_sorting_swap (T, (a) + i, (a) + (r)); \
261 #define internal_quicksort(T,cmp,a,n) \
263 int l = 0, r = (n) - 1, m, ll, rr, i; \
264 assert (ihead == indices); \
265 if (r - l <= INSERTION_SORT_LIMIT) \
270 internal_sorting_swap (T, (a) + m, (a) + r - 1); \
271 internal_sorting_cmpswap (T, cmp, (a) + l, (a) + r - 1); \
272 internal_sorting_cmpswap (T, cmp, (a) + l, (a) + r); \
273 internal_sorting_cmpswap (T, cmp, (a) + r - 1, (a) + r); \
274 internal_quicksort_partition (T, cmp, (a), l + 1, r - 1); \
287 if (r - l > INSERTION_SORT_LIMIT) \
289 assert (rr - ll > INSERTION_SORT_LIMIT); \
291 ENLARGE (indices, ihead, eoi); \
294 ENLARGE (indices, ihead, eoi); \
297 else if (rr - ll > INSERTION_SORT_LIMIT) \
302 else if (ihead > indices) \
312 #define internal_insertion_sort(T,cmp,a,n) \
315 int l = 0, r = (n) - 1, i, j; \
316 for (i = r; i > l; i--) \
317 internal_sorting_cmpswap (T, cmp, (a) + i - 1, (a) + i); \
318 for (i = l + 2; i <= r; i++) \
322 while ((cmp) (pivot, (a)[j - 1]) < 0) \
324 (a)[j] = (a)[j - 1]; \
332 #define check_sorted(cmp,a,n) do { } while(0)
334 #define check_sorted(cmp,a,n) \
337 for (i = 0; i < (n) - 1; i++) \
338 assert ((cmp) ((a)[i], (a)[i + 1]) <= 0); \
342 #define sort(T,cmp,a,n) \
346 internal_quicksort (T, cmp, aa, nn); \
347 internal_insertion_sort (T, cmp, aa, nn); \
348 assert (ihead == indices); \
349 check_sorted (cmp, aa, nn); \
352 #define WRDSZ (sizeof (long) * 8)
354 typedef unsigned Flt
; /* 32 bit deterministic soft float */
355 typedef Flt Act
; /* clause and variable activity */
356 typedef struct Blk Blk
; /* allocated memory block */
357 typedef struct Cls Cls
; /* clause */
358 typedef struct Lit Lit
; /* literal */
359 typedef struct Rnk Rnk
; /* variable to score mapping */
360 typedef signed char Val
; /* TRUE, UNDEF, FALSE */
361 typedef struct Var Var
; /* variable */
363 typedef struct Trd Trd
; /* trace data for clauses */
364 typedef struct Zhn Zhn
; /* compressed chain (=zain) data */
365 typedef unsigned char Znt
; /* compressed antecedent data */
368 #ifdef NO_BINARY_CLAUSES
369 typedef struct Ltk Ltk
;
374 unsigned count
: WRDSZ
== 32 ? 27 : 32;
375 unsigned ldsize
: WRDSZ
== 32 ? 5 : 32;
387 unsigned resolved
: 1;
389 unsigned assigned
: 1;
395 unsigned level
: WRDSZ
== 32 ? 24 : 32;
407 unsigned pos
; /* 0 iff not on heap */
419 unsigned connected
:1;
423 unsigned collected
:1;
450 size_t size
; /* this is what we really use */
451 void *as_two_ptrs
[2]; /* 2 * sizeof (void*) alignment of data */
469 static char * prefix
;
470 static int verbosity
;
471 static unsigned level
;
472 static unsigned max_var
;
473 static unsigned size_vars
;
475 static Lit
* __attribute__((aligned(64))) lits
;
483 #ifdef NO_BINARY_CLAUSES
485 static Cls impl
, cimpl
;
486 static int implvalid
, cimplvalid
;
490 static Lit
**trail
, **thead
, **eot
, **ttail
, ** ttail2
;
492 static Lit
**ttailado
;
494 static unsigned adecidelevel
;
495 static Lit
**als
, **alshead
, **alstail
, **eoals
;
496 static Lit
*failed_assumption
;
497 static int extracted_all_failed_assumptions
;
498 static Rnk
**heap
, **hhead
, **eoh
;
499 static Cls
**oclauses
, **ohead
, **eoo
; /* original clauses */
500 static Cls
**lclauses
, **lhead
, ** eol
; /* learned clauses */
503 static Zhn
**zhains
, **zhead
, **eoz
;
504 static int ocore
= -1;
507 static int rupstarted
;
508 static int rupvariables
;
509 static int rupclauses
;
511 static Cls
*conflict
;
512 static Lit
**added
, **ahead
, **eoa
;
513 static Var
**marked
, **mhead
, **eom
;
514 static Var
**dfs
, **dhead
, **eod
;
515 static Cls
**resolved
, **rhead
, **eor
;
516 static unsigned char *buffer
, *bhead
, *eob
;
517 static Act vinc
, lscore
, ilvinc
, ifvinc
;
519 static Act fvinc
, nvinc
;
521 static Act cinc
, lcinc
, ilcinc
, fcinc
;
522 static unsigned srng
;
523 static size_t current_bytes
;
524 static size_t max_bytes
;
525 static size_t recycled
;
526 static double seconds
;
527 static double entered
;
528 static unsigned nentered
;
529 static int measurealltimeinlib
;
530 static char *rline
[2];
531 static int szrline
, rcount
;
532 static double levelsum
;
533 static unsigned iterations
;
535 static int lastrheader
= -2;
536 static unsigned calls
;
537 static unsigned decisions
;
538 static unsigned restarts
;
539 static unsigned simps
;
540 static unsigned fsimplify
;
541 static unsigned isimplify
;
542 static unsigned reductions
;
543 static unsigned lreduce
;
544 static unsigned lreduceadjustcnt
;
545 static unsigned lreduceadjustinc
;
546 static unsigned lastreduceconflicts
;
547 static unsigned llocked
; /* locked large learned clauses */
548 static unsigned lrestart
;
550 static unsigned drestart
;
551 static unsigned ddrestart
;
553 static unsigned lubycnt
;
554 static unsigned lubymaxdelta
;
555 static int waslubymaxdelta
;
557 static unsigned long long lsimplify
;
558 static unsigned long long propagations
;
559 static unsigned fixed
; /* top level assignments */
561 static unsigned failedlits
;
562 static unsigned ifailedlits
;
563 static unsigned efailedlits
;
564 static unsigned flcalls
;
566 static unsigned flrounds
;
567 static unsigned long long flprops
;
568 static unsigned long long floopsed
, fltried
, flskipped
;
570 static unsigned long long fllimit
;
571 static int simplifying
;
573 static unsigned saved_size
;
575 static unsigned conflicts
;
576 static unsigned noclauses
; /* current number large original clauses */
577 static unsigned nlclauses
; /* current number large learned clauses */
578 static unsigned olits
; /* current literals in large original clauses */
579 static unsigned llits
; /* current literals in large learned clauses */
580 static unsigned oadded
; /* added original clauses */
581 static unsigned ladded
; /* added learned clauses */
582 static unsigned loadded
; /* added original large clauses */
583 static unsigned lladded
; /* added learned large clauses */
584 static unsigned addedclauses
; /* oadded + ladded */
585 static unsigned vused
; /* used variables */
586 static unsigned llitsadded
; /* added learned literals */
588 static unsigned loused
; /* used large original clauses */
589 static unsigned llused
; /* used large learned clauses */
590 static unsigned long long visits
;
591 static unsigned long long bvisits
;
592 static unsigned long long tvisits
;
593 static unsigned long long lvisits
;
594 static unsigned long long othertrue
;
595 static unsigned long long othertrue2
;
596 static unsigned long long othertruel
;
597 static unsigned long long othertrue2u
;
598 static unsigned long long othertruelu
;
599 static unsigned long long ltraversals
;
600 static unsigned long long traversals
;
602 static unsigned long long antecedents
;
604 static unsigned uips
;
605 static unsigned znts
;
606 static unsigned assumptions
;
607 static unsigned rdecisions
;
608 static unsigned sdecisions
;
609 static size_t srecycled
;
610 static size_t rrecycled
;
611 static unsigned long long derefs
;
613 static unsigned minimizedllits
;
614 static unsigned nonminimizedllits
;
616 static Lit
*** ados
, *** hados
, *** eados
;
617 static Lit
*** adotab
;
618 static unsigned nadotab
;
619 static unsigned szadotab
;
620 static Cls
* adoconflict
;
621 static unsigned adoconflicts
;
622 static unsigned adoconflictlimit
= UINT_MAX
;
623 static int addingtoado
;
624 static int adodisabled
;
626 static unsigned long long flips
;
628 static unsigned long long forced
;
629 static unsigned long long assignments
;
630 static unsigned inclreduces
;
631 static unsigned staticphasedecisions
;
632 static unsigned skippedrestarts
;
634 static int * indices
, * ihead
, *eoi
;
635 static unsigned sdflips
;
636 static int defaultphase
;
638 static unsigned long long saved_flips
;
639 static unsigned saved_max_var
;
640 static unsigned min_flipped
= UINT_MAX
;
643 static void * (*enew
)(void*,size_t);
644 static void * (*eresize
)(void*,void*,size_t,size_t);
645 static void (*edelete
)(void*,void*,size_t);
648 static FILE * fviscores
;
652 packflt (unsigned m
, int e
)
656 assert (FLTMINEXPONENT
<= e
);
657 assert (e
<= FLTMAXEXPONENT
);
658 res
= m
| ((e
+ 128) << 24);
663 base2flt (unsigned m
, int e
)
672 if (e
<= FLTMINEXPONENT
)
683 while (m
>= FLTCARRY
)
685 if (e
>= FLTMAXEXPONENT
)
694 return packflt (m
, e
);
698 addflt (Flt a
, Flt b
)
700 unsigned ma
, mb
, delta
;
707 unpackflt (a
, ma
, ea
);
708 unpackflt (b
, mb
, eb
);
719 if (ea
== FLTMAXEXPONENT
)
726 assert (ma
< FLTCARRY
);
727 ma
&= FLTMAXMANTISSA
;
729 return packflt (ma
, ea
);
733 mulflt (Flt a
, Flt b
)
736 unsigned long long accu
;
743 unpackflt (a
, ma
, ea
);
744 unpackflt (b
, mb
, eb
);
748 if (ea
> FLTMAXEXPONENT
)
751 if (ea
< FLTMINEXPONENT
)
758 if (accu
>= FLTCARRY
)
760 if (ea
== FLTMAXEXPONENT
)
766 if (accu
>= FLTCARRY
)
770 assert (accu
< FLTCARRY
);
771 assert (accu
& FLTMSB
);
776 return packflt (ma
, ea
);
782 return '0' <= c
&& c
<= '9';
786 ascii2flt (const char *str
)
788 Flt ten
= base2flt (10, 0);
789 Flt onetenth
= base2flt (26843546, -28);
790 Flt res
= ZEROFLT
, tmp
, base
;
799 return INFFLT
; /* better abort ? */
801 res
= base2flt (ch
- '0', 0);
809 return INFFLT
; /* better abort? */
811 res
= mulflt (res
, ten
);
812 tmp
= base2flt (ch
- '0', 0);
813 res
= addflt (res
, tmp
);
821 return INFFLT
; /* better abort ? */
824 tmp
= mulflt (base2flt (ch
- '0', 0), base
);
825 res
= addflt (res
, tmp
);
830 return INFFLT
; /* better abort? */
832 base
= mulflt (base
, onetenth
);
833 tmp
= mulflt (base2flt (ch
- '0', 0), base
);
834 res
= addflt (res
, tmp
);
841 #if defined(VISCORES)
855 for (i
= e
; i
< 0; i
++)
860 for (i
= 0; i
< e
; i
++)
872 return FLTEXPONENT (a
) + 24;
876 cmpflt (Flt a
, Flt b
)
896 bytes
= size
+ sizeof *b
;
899 b
= enew (emgr
, bytes
);
903 ABORTIF (!b
, "out of memory in 'new'");
905 b
->header
.size
= size
;
907 current_bytes
+= size
;
908 if (current_bytes
> max_bytes
)
909 max_bytes
= current_bytes
;
914 delete (void *void_ptr
, size_t size
)
926 b
= PTR2BLK (void_ptr
);
928 assert (size
<= current_bytes
);
929 current_bytes
-= size
;
931 assert (b
->header
.size
== size
);
933 bytes
= size
+ sizeof *b
;
935 edelete (emgr
, b
, bytes
);
941 resize (void *void_ptr
, size_t old_size
, size_t new_size
)
943 size_t old_bytes
, new_bytes
;
946 b
= PTR2BLK (void_ptr
);
948 assert (old_size
<= current_bytes
);
949 current_bytes
-= old_size
;
952 if ((old_bytes
= old_size
))
954 assert (old_size
&& b
->header
.size
== old_size
);
955 old_bytes
+= sizeof *b
;
960 if ((new_bytes
= new_size
))
961 new_bytes
+= sizeof *b
;
964 b
= eresize (emgr
, b
, old_bytes
, new_bytes
);
966 b
= realloc (b
, new_bytes
);
974 ABORTIF (!b
, "out of memory in 'resize'");
976 b
->header
.size
= new_size
;
979 current_bytes
+= new_size
;
980 if (current_bytes
> max_bytes
)
981 max_bytes
= current_bytes
;
989 return (l
< 0) ? 1 + 2 * -l
: 2 * l
;
995 return lits
+ int2unsigned (l
);
999 end_of_lits (Cls
* cls
)
1001 return cls
->lits
+ cls
->size
;
1007 return (lit
- lits
) / 2;
1011 lit2sign (Lit
* lit
)
1013 return ((lit
- lits
) & 1) ? -1 : 1;
1020 return lit2idx (l
) * lit2sign (l
);
1023 #if !defined(NDEBUG) || defined(LOGGING)
1026 dumplits (Lit
** lits
, Lit
** eol
)
1035 else if (lits
+ 1 == eol
)
1037 fprintf (out
, "%d ", lit2int (lits
[0]));
1041 assert (lits
+ 2 <= eol
);
1042 first
= (abs (lit2int (lits
[0])) > abs (lit2int (lits
[1])));
1043 fprintf (out
, "%d ", lit2int (lits
[first
]));
1044 fprintf (out
, "%d ", lit2int (lits
[!first
]));
1045 for (p
= lits
+ 2; p
< eol
; p
++)
1046 fprintf (out
, "%d ", lit2int (*p
));
1059 eol
= end_of_lits (cls
);
1060 dumplits (cls
->lits
, eol
);
1063 fprintf (out
, " clause(%u)", CLS2IDX (cls
));
1067 fputs ("DECISION", out
);
1071 dumpclsnl (Cls
* cls
)
1082 for (p
= SOC
; p
!= EOC
; p
= NXC (p
))
1101 delete_prefix (void)
1106 delete (prefix
, strlen (prefix
) + 1);
1111 new_prefix (const char * str
)
1115 prefix
= new (strlen (str
) + 1);
1116 strcpy (prefix
, str
);
1124 ABORTIF (state
!= RESET
, "API usage: multiple initializations");
1126 count
= 3 - !enew
- !eresize
- !edelete
;
1127 ABORTIF (count
&& !enew
, "API usage: missing 'picosat_set_new'");
1128 ABORTIF (count
&& !eresize
, "API usage: missing 'picosat_set_resize'");
1129 ABORTIF (count
&& !edelete
, "API usage: missing 'picosat_set_delete'");
1131 assert (!max_var
); /* check for proper reset */
1132 assert (!size_vars
); /* check for proper reset */
1136 NEWN (lits
, 2 * size_vars
);
1137 NEWN (jwh
, 2 * size_vars
);
1138 NEWN (htps
, 2 * size_vars
);
1140 NEWN (dhtps
, 2 * size_vars
);
1142 NEWN (impls
, 2 * size_vars
);
1143 NEWN (vars
, size_vars
);
1144 NEWN (rnks
, size_vars
);
1146 ENLARGE (heap
, hhead
, eoh
); /* because '0' pos denotes not on heap */
1149 vinc
= base2flt (1, 0); /* initial variable activity */
1150 ifvinc
= ascii2flt ("1.05"); /* variable score rescore factor */
1152 fvinc
= ascii2flt ("0.9523809"); /* 1/f = 1/1.1 */
1153 nvinc
= ascii2flt ("0.0476191"); /* 1 - 1/f = 1 - 1/1.1 */
1155 lscore
= base2flt (1, 90); /* variable activity rescore limit */
1156 ilvinc
= base2flt (1, -90); /* inverse of 'lscore' */
1158 cinc
= base2flt (1, 0); /* initial clause activity */
1159 fcinc
= ascii2flt ("1.001"); /* clause activity rescore factor */
1160 lcinc
= base2flt (1, 90); /* clause activity rescore limit */
1161 ilcinc
= base2flt (1, -90); /* inverse of 'ilcinc' */
1163 lreduceadjustcnt
= lreduceadjustinc
= 100;
1169 #ifdef NO_BINARY_CLAUSES
1170 memset (&impl
, 0, sizeof (impl
));
1173 memset (&cimpl
, 0, sizeof (impl
));
1179 "/usr/bin/gnuplot -background black"
1180 " -xrm 'gnuplot*textColor:white'"
1181 " -xrm 'gnuplot*borderColor:white'"
1182 " -xrm 'gnuplot*axisColor:white'"
1184 fprintf (fviscores
, "unset key\n");
1185 // fprintf (fviscores, "set log y\n");
1187 system ("rm -rf /tmp/picosat-viscores");
1188 system ("mkdir /tmp/picosat-viscores");
1189 system ("mkdir /tmp/picosat-viscores/data");
1191 system ("mkdir /tmp/picosat-viscores/gif");
1193 "set terminal gif giant animate opt size 1024,768 x000000 xffffff"
1197 "set output \"/tmp/picosat-viscores/gif/animated.gif\"\n");
1204 bytes_clause (unsigned size
, unsigned learned
)
1209 res
+= size
* sizeof (Lit
*);
1210 res
-= 2 * sizeof (Lit
*);
1212 if (learned
&& size
> 2)
1213 res
+= sizeof (Act
); /* add activity */
1217 res
+= sizeof (Trd
); /* add trace data */
1224 new_clause (unsigned size
, unsigned learned
)
1233 bytes
= bytes_clause (size
, learned
);
1242 trd
->idx
= LIDX2IDX (lhead
- lclauses
);
1244 trd
->idx
= OIDX2IDX (ohead
- oclauses
);
1253 res
->learned
= learned
;
1269 if (learned
&& size
> 2)
1270 *CLS2ACT (res
) = cinc
;
1276 delete_clause (Cls
* cls
)
1283 bytes
= bytes_clause (cls
->size
, cls
->learned
);
1288 trd
= CLS2TRD (cls
);
1289 delete (trd
, bytes
);
1293 delete (cls
, bytes
);
1297 delete_clauses (void)
1300 for (p
= SOC
; p
!= EOC
; p
= NXC (p
))
1304 DELETEN (oclauses
, eoo
- oclauses
);
1305 DELETEN (lclauses
, eol
- lclauses
);
1307 ohead
= eoo
= lhead
= eol
= 0;
1313 delete_zhain (Zhn
* zhain
)
1320 for (p
= znt
; *p
; p
++)
1323 delete (zhain
, sizeof (Zhn
) + (p
- znt
) + 1);
1327 delete_zhains (void)
1330 for (p
= zhains
; p
< zhead
; p
++)
1334 DELETEN (zhains
, eoz
- zhains
);
1340 #ifdef NO_BINARY_CLAUSES
1342 lrelease (Ltk
* stk
)
1345 DELETEN (stk
->start
, (1 << (stk
->ldsize
)));
1346 memset (stk
, 0, sizeof (*stk
));
1356 for (p
= a
; *p
; p
++)
1362 resetadoconflict (void)
1364 assert (adoconflict
);
1365 delete_clause (adoconflict
);
1374 for (p
= ados
; p
< hados
; p
++)
1375 DELETEN (*p
, llength (*p
) + 1);
1377 DELETEN (ados
, eados
- ados
);
1380 DELETEN (adotab
, szadotab
);
1381 szadotab
= nadotab
= 0;
1384 resetadoconflict ();
1387 adoconflictlimit
= UINT_MAX
;
1396 ABORTIF (state
== RESET
, "API usage: reset without initialization");
1402 #ifdef NO_BINARY_CLAUSES
1407 for (i
= 2; i
<= 2 * max_var
+ 1; i
++)
1408 lrelease (impls
+ i
);
1415 DELETEN (saved
, saved_size
);
1418 DELETEN (htps
, 2 * size_vars
);
1420 DELETEN (dhtps
, 2 * size_vars
);
1422 DELETEN (impls
, 2 * size_vars
);
1423 DELETEN (lits
, 2 * size_vars
);
1424 DELETEN (jwh
, 2 * size_vars
);
1425 DELETEN (vars
, size_vars
);
1426 DELETEN (rnks
, size_vars
);
1428 DELETEN (trail
, eot
- trail
);
1429 trail
= ttail
= ttail2
= thead
= eot
= 0;
1434 DELETEN (heap
, eoh
- heap
);
1435 heap
= hhead
= eoh
= 0;
1437 DELETEN (als
, eoals
- als
);
1438 als
= eoals
= alshead
= alstail
= 0;
1439 extracted_all_failed_assumptions
= 0;
1440 failed_assumption
= 0;
1452 DELETEN (added
, eoa
- added
);
1455 DELETEN (marked
, eom
- marked
);
1458 DELETEN (dfs
, eod
- dfs
);
1461 DELETEN (resolved
, eor
- resolved
);
1464 DELETEN (buffer
, eob
- buffer
);
1467 DELETEN (indices
, eoi
- indices
);
1472 delete (rline
[0], szrline
);
1473 delete (rline
[1], szrline
);
1474 rline
[0] = rline
[1] = 0;
1475 szrline
= rcount
= 0;
1476 assert (getenv ("LEAK") || !current_bytes
); /* found leak if failing */
1483 lastreduceconflicts
= 0;
1491 measurealltimeinlib
= 0;
1507 efailedlits
= ifailedlits
= 0;
1508 fltried
= flskipped
= floopsed
= 0;
1509 flcalls
= flrounds
= 0;
1552 #ifndef NO_BINARY_CLAUSES
1564 nonminimizedllits
= 0;
1570 min_flipped
= UINT_MAX
;
1582 staticphasedecisions
= 0;
1584 skippedrestarts
= 0;
1600 assert (lits
< lit
&& lit
<= lits
+ 2* max_var
+ 1);
1603 unsigned ttail2count
= ttail2
- trail
;
1604 unsigned ttailcount
= ttail
- trail
;
1606 unsigned ttailadocount
= ttailado
- trail
;
1608 ENLARGE (trail
, thead
, eot
);
1609 ttail
= trail
+ ttailcount
;
1610 ttail2
= trail
+ ttail2count
;
1612 ttailado
= trail
+ ttailadocount
;
1620 assign_reason (Var
* v
, Cls
* reason
)
1622 #ifdef NO_BINARY_CLAUSES
1623 assert (reason
!= &impl
);
1629 assign_phase (Lit
* lit
)
1631 unsigned new_phase
, idx
;
1632 Var
* v
= LIT2VAR (lit
);
1635 /* In 'simplifying' mode we only need to keep 'min_flipped' up to date if
1636 * we force assignments on the top level. The other assignments will be
1637 * undone and thus we can keep the old saved value of the phase.
1639 if (!level
|| !simplifying
)
1642 new_phase
= (LIT2SGN (lit
) > 0);
1646 sdflips
-= sdflips
/FFLIPPED
;
1648 if (new_phase
!= v
->phase
)
1650 assert (FFLIPPEDPREC
>= FFLIPPED
);
1651 sdflips
+= FFLIPPEDPREC
/ FFLIPPED
;
1654 idx
= lit2idx (lit
);
1655 if (idx
< min_flipped
)
1658 NOLOG (fprintf (out
, "%sflipped %d\n", prefix
, lit2int (lit
)));
1662 v
->phase
= new_phase
;
1667 NOTLIT (lit
)->val
= FALSE
;
1671 assign (Lit
* lit
, Cls
* reason
)
1673 Var
* v
= LIT2VAR (lit
);
1674 assert (lit
->val
== UNDEF
);
1680 assign_reason (v
, reason
);
1685 cmp_added (Lit
* k
, Lit
* l
)
1687 Val a
= k
->val
, b
= l
->val
;
1691 if (a
== UNDEF
&& b
!= UNDEF
)
1694 if (a
!= UNDEF
&& b
== UNDEF
)
1702 assert (b
!= UNDEF
);
1703 res
= v
->level
- u
->level
;
1705 return res
; /* larger level first */
1708 res
= cmpflt (VAR2RNK (v
)->score
, VAR2RNK (u
)->score
);
1710 return res
; /* larger activity first */
1712 return u
- v
; /* smaller index first */
1716 sorttwolits (Lit
** v
)
1718 Lit
* a
= v
[0], * b
= v
[1];
1730 sortlits (Lit
** v
, unsigned size
)
1733 sorttwolits (v
); /* same order with and with out 'NO_BINARY_CLAUSES' */
1735 sort (Lit
*, cmp_added
, v
, size
);
1738 #ifdef NO_BINARY_CLAUSES
1740 setimpl (Lit
* a
, Lit
* b
)
1742 assert (!implvalid
);
1743 assert (impl
.size
== 2);
1748 sorttwolits (impl
.lits
);
1762 setcimpl (Lit
* a
, Lit
* b
)
1764 assert (!cimplvalid
);
1765 assert (cimpl
.size
== 2);
1770 sorttwolits (cimpl
.lits
);
1779 assert (cimplvalid
);
1786 cmp_ptr (void *l
, void *k
)
1788 return ((char*)l
) - (char*)k
; /* arbitrarily already reverse */
1792 cmp_rnk (Rnk
* r
, Rnk
* s
)
1794 if (r
->score
< s
->score
)
1797 if (r
->score
> s
->score
)
1800 return -cmp_ptr (r
, s
);
1810 assert (!simplifying
);
1816 assert (vpos
< hhead
- heap
);
1817 assert (heap
[vpos
] == v
);
1825 if (cmp_rnk (u
, v
) > 0)
1838 static Cls
*add_simplified_clause (int learned
);
1841 add_antecedent (Cls
* c
)
1845 #ifdef NO_BINARY_CLAUSES
1846 if (ISLITREASON (c
))
1857 ENLARGE (resolved
, rhead
, eor
);
1859 assert (rhead
< eor
);
1865 #ifdef NO_BINARY_CLAUSES
1866 #error "can not combine TRACE and NO_BINARY_CLAUSES"
1877 ENLARGE (added
, ahead
, eoa
);
1883 push_var_as_marked (Var
* v
)
1886 ENLARGE (marked
, mhead
, eom
);
1896 push_var_as_marked (v
);
1899 /* Whenever we have a top level derived unit we really should derive a unit
1900 * clause otherwise the resolutions in 'add_simplified_clause' become
1904 resolve_top_level_unit (Lit
* lit
, Cls
* reason
)
1906 unsigned count_resolved
;
1907 Lit
**p
, **eol
, *other
;
1910 assert (rhead
== resolved
);
1911 assert (ahead
== added
);
1914 add_antecedent (reason
);
1918 eol
= end_of_lits (reason
);
1919 for (p
= reason
->lits
; p
< eol
; p
++)
1922 u
= LIT2VAR (other
);
1926 add_antecedent (u
->reason
);
1930 /* Some of the literals could be assumptions. If at least one
1931 * variable is not an assumption, we should resolve.
1933 if (count_resolved
>= 2)
1935 #ifdef NO_BINARY_CLAUSES
1936 if (reason
== &impl
)
1939 reason
= add_simplified_clause (1);
1940 #ifdef NO_BINARY_CLAUSES
1941 if (reason
->size
== 2)
1943 assert (reason
== &impl
);
1944 other
= reason
->lits
[0];
1946 other
= reason
->lits
[1];
1947 assert (other
->val
== FALSE
);
1948 reason
= LIT2REASON (NOTLIT (other
));
1952 assign_reason (v
, reason
);
1968 assert (VAR2LIT (v
) != UNDEF
);
1998 assign_forced (Lit
* lit
, Cls
* reason
)
2003 assert (lit
->val
== UNDEF
);
2008 assign (lit
, reason
);
2010 #ifdef NO_BINARY_CLAUSES
2011 assert (reason
!= &impl
);
2012 if (ISLITREASON (reason
))
2013 reason
= setimpl (lit
, NOTLIT (REASON2LIT (reason
)));
2016 "%sassign %d at level %d by ",
2017 prefix
, lit2int (lit
), level
);
2018 dumpclsnl (reason
));
2024 if (reason
&& !level
&& reason
->size
> 1)
2025 reason
= resolve_top_level_unit (lit
, reason
);
2027 #ifdef NO_BINARY_CLAUSES
2028 if (ISLITREASON (reason
) || reason
== &impl
)
2036 assert (!reason
->locked
);
2039 if (reason
->learned
&& reason
->size
> 2)
2043 #ifdef NO_BINARY_CLAUSES
2044 if (reason
== &impl
)
2052 #ifdef NO_BINARY_CLAUSES
2055 lpush (Lit
* lit
, Cls
* cls
)
2057 int pos
= (cls
->lits
[0] == lit
);
2058 Ltk
* s
= LIT2IMPLS (lit
);
2059 unsigned oldsize
, newsize
;
2061 assert (cls
->size
== 2);
2066 assert (!s
->ldsize
);
2071 oldsize
= (1 << (s
->ldsize
));
2072 assert (s
->count
<= oldsize
);
2073 if (s
->count
== oldsize
)
2075 newsize
= 2 * oldsize
;
2076 RESIZEN (s
->start
, oldsize
, newsize
);
2081 s
->start
[s
->count
++] = cls
->lits
[pos
];
2087 connect_head_tail (Lit
* lit
, Cls
* cls
)
2090 assert (cls
->size
>= 1);
2093 #ifdef NO_BINARY_CLAUSES
2097 s
= LIT2IMPLS (lit
);
2103 if (cls
->lits
[0] != lit
)
2105 assert (cls
->size
>= 2);
2106 assert (cls
->lits
[1] == lit
);
2122 ENLARGE (zhains
, zhead
, eoz
);
2128 cmp_resolved (Cls
* c
, Cls
* d
)
2132 return CLS2IDX (c
) - CLS2IDX (d
);
2136 bpushc (unsigned char ch
)
2139 ENLARGE (buffer
, bhead
, eob
);
2157 bpushd (unsigned prev
, unsigned this)
2160 assert (prev
< this);
2161 delta
= this - prev
;
2168 unsigned prev
, this, count
, rcount
;
2173 assert (bhead
== buffer
);
2174 assert (rhead
> resolved
);
2176 rcount
= rhead
- resolved
;
2177 sort (Cls
*, cmp_resolved
, resolved
, rcount
);
2180 for (p
= resolved
; p
< rhead
; p
++)
2183 this = CLS2TRD (c
)->idx
;
2184 bpushd (prev
, this);
2189 count
= bhead
- buffer
;
2191 res
= new (sizeof (Zhn
) + count
);
2194 memcpy (res
->znt
, buffer
, count
);
2206 add_resolved (int learned
)
2208 #if defined(STATS) || defined(TRACE)
2211 for (p
= resolved
; p
< rhead
; p
++)
2232 if (learned
&& trace
)
2243 Lit
**p
, *lit
, ** eol
;
2249 eol
= end_of_lits (cls
);
2251 for (p
= cls
->lits
; p
< eol
; p
++)
2255 if (lit
->val
== TRUE
)
2258 if (lit
->val
!= FALSE
)
2262 inc
= base2flt (1, -size
);
2264 for (p
= cls
->lits
; p
< eol
; p
++)
2268 sum
= addflt (*f
, inc
);
2274 write_rup_header (FILE * file
)
2279 sprintf (line
, "%%RUPD32 %u %u", rupvariables
, rupclauses
);
2282 for (i
= 255 - strlen (line
); i
>= 0; i
--)
2290 write_int (int d
, FILE * file
)
2292 static char write_int_buffer
[16];
2297 assert (sizeof d
<= 4);
2299 res
= write_int_buffer
+ sizeof write_int_buffer
;
2305 tmp
= (unsigned) -d
;
2310 assert (res
> write_int_buffer
);
2311 *--res
= '0' + (tmp
% 10);
2317 assert (res
> write_int_buffer
);
2325 add_simplified_clause (int learned
)
2327 unsigned num_true
, num_undef
, num_false
, idx
, size
, count_resolved
;
2328 Lit
**p
, **q
, *lit
, ** end
;
2335 size
= ahead
- added
;
2337 add_resolved (learned
);
2362 assert (addedclauses
== ladded
+ oadded
);
2364 #ifdef NO_BINARY_CLAUSES
2366 res
= setimpl (added
[0], added
[1]);
2370 sortlits (added
, size
);
2376 ENLARGE (lclauses
, lhead
, eol
);
2378 /* A very difficult to find bug, which only occurs if the
2379 * learned clauses stack is immediately allocated before the
2380 * original clauses stack without padding. In this case, we
2381 * have 'SOC == EOC', which terminates all loops using the
2382 * idiom 'for (p = SOC; p != EOC; p = NXC(p))' immediately.
2383 * Unfortunately this occurred in 'fix_clause_lits' after
2384 * using a recent version of the memory allocator of 'Google'
2385 * perftools in the context of one large benchmark for
2388 if (eol
== oclauses
)
2389 ENLARGE (lclauses
, lhead
, eol
);
2392 idx
= LIDX2IDX (lhead
- lclauses
);
2398 ENLARGE (oclauses
, ohead
, eoo
);
2399 if (eol
== oclauses
)
2400 ENLARGE (oclauses
, ohead
, eoo
); /* dito */
2403 idx
= OIDX2IDX (ohead
- oclauses
);
2406 assert (eol
!= oclauses
); /* dito */
2408 res
= new_clause (size
, learned
);
2410 #if !defined(NDEBUG) && defined(TRACE)
2412 assert (CLS2IDX (res
) == idx
);
2419 #if !defined(NDEBUG) && defined(TRACE)
2420 if (trace
&& learned
)
2421 assert (zhead
- zhains
== lhead
- lclauses
);
2423 assert (lhead
!= oclauses
); /* dito */
2430 write_rup_header (rup
);
2435 num_true
= num_undef
= num_false
= 0;
2438 for (p
= added
; p
< ahead
; p
++)
2445 write_int (lit2int (lit
), rup
);
2451 num_true
+= (val
== TRUE
);
2452 num_undef
+= (val
== UNDEF
);
2453 num_false
+= (val
== FALSE
);
2457 assert (num_false
+ num_true
+ num_undef
== size
);
2462 ahead
= added
; /* reset */
2466 connect_head_tail (res
->lits
[0], res
);
2468 connect_head_tail (res
->lits
[1], res
);
2477 #ifdef NO_BINARY_CLAUSES
2484 LOG (fprintf (out
, "%s%s ", prefix
, learned
? "learned" : "original");
2487 /* Shrink clause by resolving it against top level assignments.
2489 if (!level
&& num_false
> 0)
2491 assert (ahead
== added
);
2492 assert (rhead
== resolved
);
2495 add_antecedent (res
);
2497 end
= end_of_lits (res
);
2498 for (p
= res
->lits
; p
< end
; p
++)
2504 if (lit
->val
== FALSE
)
2506 add_antecedent (v
->reason
);
2513 assert (count_resolved
>= 2);
2516 #ifdef NO_BINARY_CLAUSES
2520 goto REENTER
; /* and return simplified clause */
2523 if (!num_true
&& num_undef
== 1) /* unit clause */
2526 for (p
= res
->lits
; p
< res
->lits
+ size
; p
++)
2528 if ((*p
)->val
== UNDEF
)
2537 #ifdef NO_BINARY_CLAUSES
2540 Lit
* other
= res
->lits
[0];
2542 other
= res
->lits
[1];
2544 assert (other
->val
== FALSE
);
2545 reason
= LIT2REASON (NOTLIT (other
));
2548 assign_forced (lit
, reason
);
2552 if (num_false
== size
&& !conflict
)
2554 #ifdef NO_BINARY_CLAUSES
2556 conflict
= setcimpl (res
->lits
[0], res
->lits
[1]);
2562 if (!num_true
&& num_undef
)
2569 trivial_clause (void)
2571 Lit
**p
, **q
, *prev
;
2574 sort (Lit
*, cmp_ptr
, added
, ahead
- added
);
2578 for (p
= q
; p
< ahead
; p
++)
2584 if (prev
== this) /* skip repeated literals */
2587 /* Top level satisfied ?
2589 if (this->val
== TRUE
&& !v
->level
)
2592 if (prev
== NOTLIT (this))/* found pair of dual literals */
2598 ahead
= q
; /* shrink */
2604 simplify_and_add_original_clause (void)
2608 if (trivial_clause ())
2613 ENLARGE (oclauses
, ohead
, eoo
);
2622 cls
= add_simplified_clause (0);
2623 #ifdef NO_BINARY_CLAUSES
2635 unsigned len
= ahead
- added
;
2636 Lit
** ado
, ** p
, ** q
, *lit
;
2643 ABORTIF (ados
< hados
&& llength (ados
[0]) != len
,
2644 "internal: non matching all different constraint object lengths");
2647 ENLARGE (ados
, hados
, eados
);
2649 NEWN (ado
, len
+ 1);
2660 "internal: variable in multiple all different objects");
2662 if (!u
&& !lit
->val
)
2667 assert (q
== ado
+ len
);
2670 /* TODO simply do a conflict test as in propado */
2674 "adding fully instantiated all different object not implemented yet");
2677 assert (u
->inado
== ado
);
2689 unsigned end
, rpos
, cpos
, opos
;
2692 assert (r
->pos
> 0);
2693 assert (heap
[r
->pos
] == r
);
2707 if (cmp_rnk (r
, child
) < 0)
2713 if (cmp_rnk (child
, other
) < 0)
2720 else if (opos
< end
)
2724 if (cmp_rnk (r
, child
) >= 0)
2744 assert (hhead
> heap
);
2754 assert (hhead
> heap
);
2759 end
= --hhead
- heap
;
2765 heap
[last
->pos
= 1] = last
;
2777 ENLARGE (heap
, hhead
, eoh
);
2779 r
->pos
= hhead
++ - heap
;
2785 fix_trail_lits (long delta
)
2788 for (p
= trail
; p
< thead
; p
++)
2792 #ifdef NO_BINARY_CLAUSES
2794 fix_impl_lits (long delta
)
2799 for (s
= impls
+ 2; s
< impls
+ 2 * max_var
; s
++)
2800 for (p
= s
->start
; p
< s
->start
+ s
->count
; p
++)
2806 fix_clause_lits (long delta
)
2809 Lit
**q
, *lit
, **eol
;
2811 for (p
= SOC
; p
!= EOC
; p
= NXC (p
))
2818 eol
= end_of_lits (clause
);
2821 assert (q
- clause
->lits
<= (int) clause
->size
);
2830 fix_added_lits (long delta
)
2833 for (p
= added
; p
< ahead
; p
++)
2838 fix_assumed_lits (long delta
)
2841 for (p
= als
; p
< alshead
; p
++)
2846 fix_heap_rnks (long delta
)
2850 for (p
= heap
+ 1; p
< hhead
; p
++)
2857 fix_ado (long delta
, Lit
** ado
)
2860 for (p
= ado
; *p
; p
++)
2865 fix_ados (long delta
)
2869 for (p
= ados
; p
< hados
; p
++)
2870 fix_ado (delta
, *p
);
2876 enlarge (unsigned new_size_vars
)
2878 long rnks_delta
, lits_delta
, vars_delta
;
2879 Lit
*old_lits
= lits
;
2880 Rnk
*old_rnks
= rnks
;
2881 Var
*old_vars
= vars
;
2883 RESIZEN (lits
, 2 * size_vars
, 2 * new_size_vars
);
2884 RESIZEN (jwh
, 2 * size_vars
, 2 * new_size_vars
);
2885 RESIZEN (htps
, 2 * size_vars
, 2 * new_size_vars
);
2887 RESIZEN (dhtps
, 2 * size_vars
, 2 * new_size_vars
);
2889 RESIZEN (impls
, 2 * size_vars
, 2 * new_size_vars
);
2890 RESIZEN (vars
, size_vars
, new_size_vars
);
2891 RESIZEN (rnks
, size_vars
, new_size_vars
);
2893 lits_delta
= lits
- old_lits
;
2894 rnks_delta
= rnks
- old_rnks
;
2895 vars_delta
= vars
- old_vars
;
2897 fix_trail_lits (lits_delta
);
2898 fix_clause_lits (lits_delta
);
2899 fix_added_lits (lits_delta
);
2900 fix_assumed_lits (lits_delta
);
2901 #ifdef NO_BINARY_CLAUSES
2902 fix_impl_lits (lits_delta
);
2905 fix_ados (lits_delta
);
2907 fix_heap_rnks (rnks_delta
);
2908 assert (mhead
== marked
);
2910 size_vars
= new_size_vars
;
2914 unassign (Lit
* lit
)
2920 assert (lit
->val
== TRUE
);
2922 LOG (fprintf (out
, "%sunassign %d\n", prefix
, lit2int (lit
)));
2927 #ifdef NO_BINARY_CLAUSES
2928 assert (reason
!= &impl
);
2929 if (ISLITREASON (reason
))
2937 assert (reason
->locked
);
2940 if (reason
->learned
&& reason
->size
> 2)
2942 assert (llocked
> 0);
2948 NOTLIT (lit
)->val
= UNDEF
;
2956 Cls
* p
, * next
, ** q
;
2958 q
= LIT2DHTPS (lit
);
2964 Lit
* other
= p
->lits
[0];
2973 assert (p
->lits
[1] == lit
);
2978 *q
= *LIT2HTPS (other
);
2979 *LIT2HTPS (other
) = p
;
2989 assert (*v
->adotabpos
== v
->ado
);
3000 var2reason (Var
* var
)
3002 Cls
* res
= var
->reason
;
3003 #ifdef NO_BINARY_CLAUSES
3004 Lit
* this, * other
;
3005 if (ISLITREASON (res
))
3007 this = VAR2LIT (var
);
3008 if (this->val
== FALSE
)
3009 this = NOTLIT (this);
3011 other
= REASON2LIT (res
);
3012 assert (other
->val
== TRUE
);
3013 assert (this->val
== TRUE
);
3014 res
= setimpl (NOTLIT (other
), this);
3021 mark_clause_to_be_collected (Cls
* cls
)
3023 assert (!cls
->collect
);
3028 undo (unsigned new_level
)
3033 while (thead
> trail
)
3037 if (v
->level
== new_level
)
3039 thead
++; /* fix pre decrement */
3053 #ifdef NO_BINARY_CLAUSES
3054 if (conflict
== &cimpl
)
3058 if (conflict
&& conflict
== adoconflict
)
3059 resetadoconflict ();
3062 if (level
< adecidelevel
)
3064 assert (als
< alshead
);
3068 LOG (fprintf (out
, "%sback to level %u\n", prefix
, level
));
3074 clause_satisfied (Cls
* cls
)
3076 Lit
**p
, **eol
, *lit
;
3078 eol
= end_of_lits (cls
);
3079 for (p
= cls
->lits
; p
< eol
; p
++)
3082 if (lit
->val
== TRUE
)
3090 original_clauses_satisfied (void)
3094 for (p
= oclauses
; p
< ohead
; p
++)
3104 assert (clause_satisfied (cls
));
3109 assumptions_satisfied (void)
3113 for (p
= als
; p
< alshead
; p
++)
3116 assert (lit
->val
== TRUE
);
3125 double now
= picosat_time_stamp ();
3126 double delta
= now
- entered
;
3127 delta
= (delta
< 0) ? 0 : delta
;
3135 return current_bytes
/ (double) (1 << 20);
3141 return decisions
? levelsum
/ decisions
: 0.0;
3147 assert (lastrheader
<= reports
);
3149 if (lastrheader
== reports
)
3152 lastrheader
= reports
;
3154 fprintf (out
, "%s\n", prefix
);
3155 fprintf (out
, "%s %s\n", prefix
, rline
[0]);
3156 fprintf (out
, "%s %s\n", prefix
, rline
[1]);
3157 fprintf (out
, "%s\n", prefix
);
3161 dynamic_flips_per_assignment_per_mille (void)
3163 assert (FFLIPPEDPREC
>= 1000);
3164 return sdflips
/ (FFLIPPEDPREC
/ 1000);
3172 return dynamic_flips_per_assignment_per_mille () >= 200;
3176 very_high_agility (void)
3178 return dynamic_flips_per_assignment_per_mille () >= 250;
3184 medium_agility (void)
3186 return dynamic_flips_per_assignment_per_mille () >= 230;
3199 /* strip trailing white space
3201 for (x
= 0; x
<= 1; x
++)
3203 p
= rline
[x
] + strlen (rline
[x
]);
3204 while (p
-- > rline
[x
])
3222 relemhead (const char * name
, int fp
, double val
)
3224 int x
, y
, len
, size
;
3231 y
= (rcount
/ 2) * 12 + x
* 6;
3234 sprintf (rline
[1], "%6s", "");
3236 len
= strlen (name
);
3237 while (szrline
<= len
+ y
+ 1)
3239 size
= szrline
? 2 * szrline
: 128;
3240 rline
[0] = resize (rline
[0], szrline
, size
);
3241 rline
[1] = resize (rline
[1], szrline
, size
);
3245 fmt
= (len
<= 6) ? "%6s%10s" : "%-10s%4s";
3246 sprintf (rline
[x
] + y
, fmt
, name
, "");
3252 if (val
> -100 && (tmp
= val
* 10.0 - 0.5) > -1000.0)
3254 fprintf (out
, "-%4.1f ", -tmp
/ 10.0);
3258 tmp
= -val
/ 10.0 + 0.5;
3266 fprintf (out
, "-%2ue%u ", tmp
, e
);
3271 if (fp
&& val
< 1000 && (tmp
= val
* 10.0 + 0.5) < 10000)
3273 fprintf (out
, "%5.1f ", tmp
/ 10.0);
3275 else if (!fp
&& (tmp
= val
) < 100000)
3277 fprintf (out
, "%5u ", tmp
);
3281 tmp
= val
/ 10.0 + 0.5;
3290 fprintf (out
, "%3ue%u ", tmp
, e
);
3298 relem (const char *name
, int fp
, double val
)
3301 relemhead (name
, fp
, val
);
3307 reduce_limit_on_lclauses (void)
3309 unsigned res
= lreduce
;
3315 report (int level
, char type
)
3319 if (verbosity
< level
)
3327 for (rounds
= (reports
< 0) ? 2 : 1; rounds
; rounds
--)
3330 fprintf (out
, "%s%c ", prefix
, type
);
3332 relem ("seconds", 1, seconds
);
3333 relem ("level", 1, avglevel ());
3334 assert (fixed
<= max_var
);
3335 relem ("variables", 0, max_var
- fixed
);
3336 relem ("used", 1, PERCENT (vused
, max_var
));
3337 relem ("original", 0, noclauses
);
3338 relem ("conflicts", 0, conflicts
);
3339 //relem ("decisions", 0, decisions);
3340 // relem ("conf/dec", 1, PERCENT(conflicts,decisions));
3341 // relem ("limit", 0, reduce_limit_on_lclauses ());
3342 relem ("learned", 0, nlclauses
);
3343 // relem ("limit", 1, PERCENT (nlclauses, reduce_limit_on_lclauses ()));
3344 relem ("limit", 0, lreduce
);
3346 relem ("learning", 1, PERCENT (llused
, lladded
));
3348 relem ("agility", 1, dynamic_flips_per_assignment_per_mille () / 10.0);
3349 // relem ("original", 0, noclauses);
3350 relem ("MB", 1, mb ());
3351 // relem ("lladded", 0, lladded);
3352 // relem ("llused", 0, llused);
3359 /* Adapt this to the number of rows in your terminal.
3363 if (reports
% (ROWS
- 3) == (ROWS
- 4))
3370 bcp_queue_is_empty (void)
3375 if (ttail2
!= thead
)
3379 if (ttailado
!= thead
)
3390 assert (!failed_assumption
);
3391 if (alstail
< alshead
)
3394 assert (bcp_queue_is_empty ());
3395 return thead
== trail
+ max_var
; /* all assigned */
3401 Rnk
*p
, *eor
= rnks
+ max_var
;
3402 for (p
= rnks
+ 1; p
<= eor
; p
++)
3403 if (p
->score
!= INFFLT
)
3404 p
->score
= mulflt (p
->score
, ilvinc
);
3405 vinc
= mulflt (vinc
, ilvinc
);;
3407 nvinc
= mulflt (nvinc
, lscore
);;
3428 assert (score
!= INFFLT
);
3430 score
= addflt (score
, vinc
);
3431 assert (score
< INFFLT
);
3441 inc_activity (Cls
* cls
)
3452 *p
= addflt (*p
, cinc
);
3456 hashlevel (unsigned l
)
3458 return 1u << (l
& 31);
3465 ENLARGE (dfs
, dhead
, eod
);
3473 assert (dfs
< dhead
);
3480 unsigned open
, minlevel
, siglevels
, l
, old
, i
, orig
;
3481 Lit
*this, *other
, **p
, **q
, **eol
;
3482 Var
*v
, *u
, **m
, *start
, *uip
;
3487 assert (ahead
== added
);
3488 assert (mhead
== marked
);
3489 assert (rhead
== resolved
);
3491 /* 2. Search for First UIP variable and mark all resolved variables. At
3492 * the same time determine the minimum decision level involved. Increase
3493 * activities of resolved variables.
3507 eol
= end_of_lits (c
);
3508 for (p
= c
->lits
; p
< eol
; p
++)
3512 if (other
->val
== TRUE
)
3515 assert (other
->val
== FALSE
);
3517 u
= LIT2VAR (other
);
3525 if (u
->level
== level
)
3531 push_var_as_marked (u
);
3535 /* The statistics counter 'nonminimizedllits' sums up the
3536 * number of literals that would be added if only the
3537 * 'first UIP' scheme for learned clauses would be used
3538 * and no clause minimization.
3540 nonminimizedllits
++;
3542 if (u
->level
< minlevel
)
3543 minlevel
= u
->level
;
3545 siglevels
|= hashlevel (u
->level
);
3560 goto DONE_FIRST_UIP
;
3564 uip
= LIT2VAR (this);
3570 c
= var2reason (uip
);
3571 #ifdef NO_BINARY_CLAUSES
3576 if ((!open
&& level
) || !c
)
3587 this = VAR2LIT (uip
);
3588 this += (this->val
== TRUE
);
3589 nonminimizedllits
++;
3600 /* 3. Try to mark more intermediate variables, with the goal to minimize
3601 * the conflict clause. This is a DFS from already marked variables
3602 * backward through the implication graph. It tries to reach other marked
3603 * variables. If the search reaches an unmarked decision variable or a
3604 * variable assigned below the minimum level of variables in the first uip
3605 * learned clause or a level on which no variable has been marked, then
3606 * the variable from which the DFS is started is not redundant. Otherwise
3607 * the start variable is redundant and will eventually be removed from the
3608 * learned clause in step 4. We initially implemented BFS, but then
3609 * profiling revelead that this step is a bottle neck for certain
3610 * incremental applications. After switching to DFS this hot spot went
3613 orig
= mhead
- marked
;
3614 for (i
= 0; i
< orig
; i
++)
3618 assert (start
->mark
);
3619 assert (start
!= uip
);
3620 assert (start
->level
< level
);
3625 old
= mhead
- marked
;
3626 assert (dhead
== dfs
);
3635 #ifdef NO_BINARY_CLAUSES
3641 (l
< minlevel
|| ((hashlevel (l
) & ~siglevels
)))))
3643 while (mhead
> marked
+ old
) /* reset all marked */
3644 (*--mhead
)->mark
= 0;
3646 dhead
= dfs
; /* and DFS stack */
3650 eol
= end_of_lits (c
);
3651 for (p
= c
->lits
; p
< eol
; p
++)
3663 for (m
= marked
; m
< mhead
; m
++)
3668 assert (!v
->resolved
);
3676 #ifdef NO_BINARY_CLAUSES
3680 eol
= end_of_lits (c
);
3681 for (p
= c
->lits
; p
< eol
; p
++)
3685 u
= LIT2VAR (other
);
3689 if (!u
->mark
) /* 'MARKTEST' */
3700 for (m
= marked
; m
< mhead
; m
++)
3714 if (this->val
== TRUE
)
3715 this++; /* actually NOTLIT */
3721 assert (ahead
<= eoa
);
3722 assert (rhead
<= eor
);
3727 /* Propagate assignment of 'this' to 'FALSE' by visiting all binary clauses in
3728 * which 'this' occurs.
3733 #ifdef NO_BINARY_CLAUSES
3743 assert (this->val
== FALSE
);
3745 #ifdef NO_BINARY_CLAUSES
3746 lstk
= LIT2IMPLS (this);
3747 start
= lstk
->start
;
3748 l
= start
+ lstk
->count
;
3752 /* The counter 'visits' is the number of clauses that are
3753 * visited during propagations of assignments.
3766 if (LIT2VAR (other
)->level
< level
)
3774 assign_forced (other
, LIT2REASON (NOTLIT(this)));
3778 if (conflict
== &cimpl
)
3780 conflict
= setcimpl (this, other
);
3783 /* Traverse all binary clauses with 'this'. Head/Tail pointers for binary
3784 * clauses do not have to be modified here.
3786 p
= LIT2IMPLS (this);
3787 for (cls
= *p
; cls
; cls
= next
)
3793 assert (!cls
->collect
);
3795 assert (!cls
->collected
);
3797 assert (cls
->size
== 2);
3799 other
= cls
->lits
[0];
3802 next
= cls
->next
[0];
3803 other
= cls
->lits
[1];
3808 next
= cls
->next
[1];
3817 if (LIT2VAR (other
)->level
< level
)
3826 assign_forced (other
, cls
); /* unit clause */
3828 #endif /* !defined(NO_BINARY_CLAUSES) */
3833 should_disconnect_head_tail (Lit
* lit
)
3838 assert (lit
->val
== TRUE
);
3841 lit_level
= v
->level
;
3851 return lit_level
< level
;
3858 Lit
**l
, *other
, *prev
, *new_lit
, **eol
;
3859 Cls
*next
, **htp_ptr
, **new_htp_ptr
;
3865 htp_ptr
= LIT2HTPS (this);
3866 assert (this->val
== FALSE
);
3868 /* Traverse all non binary clauses with 'this'. Head/Tail pointers are
3871 for (cls
= *htp_ptr
; cls
; cls
= next
)
3880 traversals
++; /* other is dereferenced at least */
3892 assert (!cls
->collected
);
3894 assert (cls
->size
> 0);
3896 /* With assumptions we need to traverse unit clauses as well.
3905 other
= cls
->lits
[0];
3908 cls
->lits
[0] = this;
3909 cls
->lits
[1] = other
;
3910 next
= cls
->next
[1];
3911 cls
->next
[1] = cls
->next
[0];
3912 cls
->next
[0] = next
;
3916 other
= cls
->lits
[1];
3917 next
= cls
->next
[0];
3919 assert (other
== cls
->lits
[1]);
3920 assert (this == cls
->lits
[0]);
3921 assert (next
== cls
->next
[0]);
3922 assert (!cls
->collect
);
3924 if (other
->val
== TRUE
)
3931 if (should_disconnect_head_tail (other
))
3933 new_htp_ptr
= LIT2DHTPS (other
);
3934 cls
->next
[0] = *new_htp_ptr
;
3943 htp_ptr
= cls
->next
;
3948 eol
= cls
->lits
+ cls
->size
;
3964 if (new_lit
->val
!= FALSE
) break;
3969 while (l
> cls
->lits
+ 2)
3975 assert (cls
->lits
[0] == this);
3977 assert (other
== cls
->lits
[1]);
3978 if (other
->val
== FALSE
) /* found conflict */
3985 assign_forced (other
, cls
); /* unit clause */
3986 htp_ptr
= cls
->next
;
3990 assert (new_lit
->val
== TRUE
|| new_lit
->val
== UNDEF
);
3991 cls
->lits
[0] = new_lit
;
3993 new_htp_ptr
= LIT2HTPS (new_lit
);
3994 cls
->next
[0] = *new_htp_ptr
;
4003 static unsigned primes
[] = { 996293, 330643, 753947, 500873 };
4005 #define PRIMES ((sizeof primes)/sizeof *primes)
4008 hash_ado (Lit
** ado
, unsigned salt
)
4010 unsigned i
, res
, tmp
;
4013 assert (salt
< PRIMES
);
4018 for (p
= ado
; (lit
= *p
); p
++)
4028 assert (i
< PRIMES
);
4036 return res
& (szadotab
- 1);
4040 cmp_ado (Lit
** a
, Lit
** b
)
4042 Lit
** p
, ** q
, * l
, * k
;
4045 for (p
= a
, q
= b
; (l
= *p
); p
++, q
++)
4049 if ((res
= (l
->val
- k
->val
)))
4059 find_ado (Lit
** ado
)
4061 Lit
*** res
, ** other
;
4062 unsigned pos
, delta
;
4064 pos
= hash_ado (ado
, 0);
4065 assert (pos
< szadotab
);
4069 if (!other
|| !cmp_ado (other
, ado
))
4072 delta
= hash_ado (ado
, 1);
4077 assert (delta
< szadotab
);
4082 if (pos
>= szadotab
)
4085 assert (pos
< szadotab
);
4088 if (!other
|| !cmp_ado (other
, ado
))
4094 enlarge_adotab (void)
4096 /* TODO make this generic */
4099 "internal: all different objects table needs larger initial size");
4102 NEWN (adotab
, szadotab
);
4103 CLRN (adotab
, szadotab
);
4109 Lit
** p
, ** q
, *** adotabpos
, **ado
, * lit
;
4112 if (level
&& adodisabled
)
4116 assert (!adoconflict
);
4117 assert (VAR2LIT (v
)->val
!= UNDEF
);
4118 assert (!v
->adotabpos
);
4125 for (p
= v
->ado
; (lit
= *p
); p
++)
4126 if (lit
->val
== UNDEF
)
4136 if (4 * nadotab
>= 3 * szadotab
) /* at least 75% filled */
4139 adotabpos
= find_ado (v
->ado
);
4145 v
->adotabpos
= adotabpos
;
4146 *adotabpos
= v
->ado
;
4150 assert (ado
!= v
->ado
);
4152 adoconflict
= new_clause (2 * llength (ado
), 1);
4153 q
= adoconflict
->lits
;
4155 for (p
= ado
; (lit
= *p
); p
++)
4156 *q
++ = lit
->val
== FALSE
? lit
: NOTLIT (lit
);
4158 for (p
= v
->ado
; (lit
= *p
); p
++)
4159 *q
++ = lit
->val
== FALSE
? lit
: NOTLIT (lit
);
4161 assert (q
== ENDOFCLS (adoconflict
));
4162 conflict
= adoconflict
;
4175 if (mtcls
|| conflict
)
4180 if (ttail2
< thead
) /* prioritize implications */
4183 prop2 (NOTLIT (*ttail2
++));
4185 else if (ttail
< thead
) /* unit clauses or clauses with length > 2 */
4187 if (conflict
) break;
4188 propl (NOTLIT (*ttail
++));
4189 if (conflict
) break;
4192 else if (ttailado
< thead
)
4194 if (conflict
) break;
4195 propado (LIT2VAR (*ttailado
++));
4196 if (conflict
) break;
4200 break; /* all assignments propagated, so break */
4203 propagations
+= props
;
4206 /* This version of 'drive' is independent of the global variable 'level' and
4207 * thus even works if we resolve ala 'relsat' without driving an assignment.
4212 Var
*v
, *first
, *second
;
4216 for (p
= added
; p
< ahead
; p
++)
4219 if (!first
|| v
->level
> first
->level
)
4227 for (p
= added
; p
< ahead
; p
++)
4231 if (v
->level
== first
->level
)
4234 if (!second
|| v
->level
> second
->level
)
4241 return second
->level
;
4249 Rnk
*p
, *eor
= rnks
+ max_var
;
4250 char name
[100], cmd
[200];
4255 for (p
= rnks
+ 1; p
<= eor
; p
++)
4260 s
= mulflt (s
, nvinc
);
4261 assert (flt2double (s
) <= 1.0);
4264 sprintf (name
, "/tmp/picosat-viscores/data/%08u", conflicts
);
4265 sprintf (cmd
, "sort -n|nl>%s", name
);
4267 data
= popen (cmd
, "w");
4268 for (p
= rnks
+ 1; p
<= eor
; p
++)
4273 s
= mulflt (s
, nvinc
);
4274 fprintf (data
, "%lf %d\n", 100.0 * flt2double (s
), (int)(p
- rnks
));
4279 for (i
= 0; i
< 8; i
++)
4281 sprintf (cmd
, "awk '$3%%8==%d' %s>%s.%d", i
, name
, name
, i
);
4285 fprintf (fviscores
, "set title \"%u\"\n", conflicts
);
4286 fprintf (fviscores
, "plot [0:%u] 0, 100 * (1 - 1/1.1), 100", max_var
);
4288 for (i
= 0; i
< 8; i
++)
4290 ", \"%s.%d\" using 1:2:3 with labels tc lt %d",
4293 fputc ('\n', fviscores
);
4296 usleep (50000); /* refresh rate of 20 Hz */
4308 int l
= log2flt (cinc
);
4310 factor
= base2flt (1, -l
);
4312 for (p
= lclauses
; p
!= lhead
; p
++)
4323 assert (cls
->learned
);
4329 *a
= mulflt (*a
, factor
);
4332 cinc
= mulflt (cinc
, factor
);
4339 nvinc
= mulflt (nvinc
, fvinc
);
4341 vinc
= mulflt (vinc
, ifvinc
);
4351 assert (max_var
< size_vars
);
4353 max_var
++; /* new index of variable */
4354 assert (max_var
); /* no unsigned overflow */
4356 if (max_var
== size_vars
)
4357 enlarge (size_vars
+ (size_vars
+ 3) / 4); /* increase by 25% */
4359 assert (max_var
< size_vars
);
4361 lit
= lits
+ 2 * max_var
;
4362 lit
[0].val
= lit
[1].val
= UNDEF
;
4364 memset (htps
+ 2 * max_var
, 0, 2 * sizeof *htps
);
4366 memset (dhtps
+ 2 * max_var
, 0, 2 * sizeof *dhtps
);
4368 memset (impls
+ 2 * max_var
, 0, 2 * sizeof *impls
);
4369 memset (jwh
+ 2 * max_var
, 0, 2 * sizeof *jwh
);
4371 v
= vars
+ max_var
; /* initialize variable components */
4374 r
= rnks
+ max_var
; /* initialize rank */
4383 Lit
** p
, ** eol
, * lit
, * forced
;
4390 eol
= end_of_lits (cls
);
4391 for (p
= cls
->lits
; p
< eol
; p
++)
4394 if (lit
->val
== UNDEF
)
4398 #ifdef NO_BINARY_CLAUSES
4400 reason
= LIT2REASON (NOTLIT (p
[p
== cls
->lits
? 1 : -1]));
4404 assert (lit
->val
== FALSE
);
4407 #ifdef NO_BINARY_CLAUSES
4414 assign_forced (forced
, reason
);
4415 v
= LIT2VAR (forced
);
4436 LOG (fprintf (out
, "%sconflict ", prefix
); dumpclsnl (conflict
));
4439 new_level
= drive ();
4440 // TODO: why not? assert (new_level != 1 || (ahead - added) == 2);
4441 cls
= add_simplified_clause (1);
4449 !--lreduceadjustcnt
)
4451 lreduceadjustinc
*= 15;
4452 lreduceadjustinc
/= 10;
4453 lreduceadjustcnt
= lreduceadjustinc
;
4457 if (verbosity
>= 4 && !(conflicts
% 1000))
4464 cinc
= mulflt (cinc
, fcinc
);
4480 disconnect_clause (Cls
* cls
)
4482 assert (cls
->connected
);
4488 assert (nlclauses
> 0);
4491 assert (llits
>= cls
->size
);
4496 assert (noclauses
> 0);
4499 assert (olits
>= cls
->size
);
4510 clause_is_toplevel_satisfied (Cls
* cls
)
4512 Lit
*lit
, **p
, **eol
= end_of_lits (cls
);
4515 for (p
= cls
->lits
; p
< eol
; p
++)
4518 if (lit
->val
== TRUE
)
4530 collect_clause (Cls
* cls
)
4532 assert (cls
->collect
);
4536 assert (!cls
->collected
);
4539 disconnect_clause (cls
);
4542 if (trace
&& (!cls
->learned
|| cls
->used
))
4545 delete_clause (cls
);
4551 collect_clauses (void)
4553 Cls
*cls
, **p
, **q
, * next
;
4559 res
= current_bytes
;
4561 eol
= lits
+ 2 * max_var
+ 1;
4562 for (lit
= lits
+ 2; lit
<= eol
; lit
++)
4564 for (i
= 0; i
<= 1; i
++)
4568 #ifdef NO_BINARY_CLAUSES
4569 Ltk
* lstk
= LIT2IMPLS (lit
);
4572 for (s
= r
; s
< lstk
->start
+ lstk
->count
; s
++)
4575 Var
*v
= LIT2VAR (other
);
4576 if (v
->level
|| other
->val
!= TRUE
)
4579 lstk
->count
= r
- lstk
->start
;
4582 p
= LIT2IMPLS (lit
);
4588 for (cls
= *p
; cls
; cls
= next
)
4591 if (cls
->lits
[0] != lit
)
4604 for (lit
= lits
+ 2; lit
<= eol
; lit
++)
4606 p
= LIT2DHTPS (lit
);
4609 Lit
* other
= cls
->lits
[0];
4616 assert (cls
->lits
[1] == lit
);
4628 for (v
= vars
+ 1; v
<= vars
+ max_var
; v
++)
4634 #ifdef NO_BINARY_CLAUSES
4635 if (ISLITREASON (cls
))
4642 for (p
= SOC
; p
!= EOC
; p
= NXC (p
))
4652 if (collect_clause (cls
))
4661 for (p
= q
; p
< ohead
; p
++)
4667 for (p
= q
; p
< lhead
; p
++)
4673 assert (current_bytes
<= res
);
4674 res
-= current_bytes
;
4681 need_to_reduce (void)
4683 return nlclauses
>= reduce_limit_on_lclauses ();
4691 drestart
*= FRESTART
;
4694 if (drestart
>= MAXRESTART
)
4695 drestart
= MAXRESTART
;
4699 inc_ddrestart (void)
4701 ddrestart
*= FRESTART
;
4704 if (ddrestart
>= MAXRESTART
)
4705 ddrestart
= MAXRESTART
;
4714 for (k
= 1; k
< 32; k
++)
4715 if (i
== (1 << k
) - 1)
4716 return 1 << (k
- 1);
4719 if ((1 << (k
- 1)) <= i
&& i
< (1 << k
) - 1)
4720 return luby (i
- (1 << (k
-1)) + 1);
4727 inc_lrestart (int skip
)
4731 delta
= 100 * luby (++lubycnt
);
4732 lrestart
= conflicts
+ delta
;
4734 if (waslubymaxdelta
)
4735 report (1, skip
? 'N' : 'R');
4737 report (2, skip
? 'n' : 'r');
4739 if (delta
> lubymaxdelta
)
4741 lubymaxdelta
= delta
;
4742 waslubymaxdelta
= 1;
4745 waslubymaxdelta
= 0;
4753 /* TODO: why is it better in incremental usage to have smaller initial
4754 * outer restart interval?
4756 ddrestart
= calls
> 1 ? MINRESTART
: 1000;
4757 drestart
= MINRESTART
;
4758 lrestart
= conflicts
+ drestart
;
4762 waslubymaxdelta
= 0;
4776 outer
= (drestart
>= ddrestart
);
4779 skip
= very_high_agility ();
4781 skip
= high_agility ();
4783 skip
= medium_agility ();
4791 assert (conflicts
>= lrestart
);
4797 LOG (fprintf (out
, "%srestart %u\n", prefix
, restarts
));
4804 kind
= skip
? 'N' : 'R';
4806 drestart
= MINRESTART
;
4817 assert (drestart
<= MAXRESTART
);
4818 lrestart
= conflicts
+ drestart
;
4819 assert (lrestart
> conflicts
);
4821 report (outer
? 1 : 2, kind
);
4823 inc_lrestart (skip
);
4828 assign_decision (Lit
* lit
)
4834 LOG (fprintf (out
, "%snew level %u\n", prefix
, level
));
4836 "%sassign %d at level %d <= DECISION\n",
4837 prefix
, lit2int (lit
), level
));
4845 lit_has_binary_clauses (Lit
* lit
)
4847 #ifdef NO_BINARY_CLAUSES
4848 Ltk
* lstk
= LIT2IMPLS (lit
);
4849 return lstk
->count
!= 0;
4851 return *LIT2IMPLS (lit
) != 0;
4859 unsigned long long propagaions_before_bcp
= propagations
;
4863 flprops
+= propagations
- propagaions_before_bcp
;
4868 cmp_inverse_rnk (Rnk
* a
, Rnk
* b
)
4870 return -cmp_rnk (a
, b
);
4876 Flt res
, sum
, pjwh
, njwh
;
4882 pjwh
= *LIT2JWH (plit
);
4883 njwh
= *LIT2JWH (nlit
);
4885 res
= mulflt (pjwh
, njwh
);
4887 sum
= addflt (pjwh
, njwh
);
4888 sum
= mulflt (sum
, base2flt (1, -10));
4889 res
= addflt (res
, sum
);
4895 cmp_inverse_jwh_rnk (Rnk
* r
, Rnk
* s
)
4897 Flt a
= rnk2jwh (r
);
4898 Flt b
= rnk2jwh (s
);
4899 int res
= cmpflt (a
, b
);
4904 return cmp_inverse_rnk (r
, s
);
4910 unsigned i
, j
, old_trail_count
, common
, saved_count
;
4911 unsigned new_saved_size
, oldladded
= ladded
;
4912 unsigned long long limit
, delta
;
4913 Lit
* lit
, * other
, * pivot
;
4914 int new_trail_count
;
4915 Rnk
* r
, ** p
, ** q
;
4918 if (heap
+ 1 >= hhead
)
4921 if (propagations
< fllimit
)
4929 delta
= 10 * 1000 * 1000;
4931 delta
= 1000 * 1000;
4933 limit
= propagations
+ delta
;
4934 fllimit
= propagations
;
4937 assert (simplifying
);
4940 sort (Rnk
*, cmp_inverse_jwh_rnk
, heap
+ 1, hhead
- (heap
+ 1));
4942 sort (Rnk
*, cmp_inverse_rnk
, heap
+ 1, hhead
- (heap
+ 1));
4944 i
= 1; /* NOTE: heap starts at position '1' */
4946 while (propagations
< limit
)
4948 if (heap
+ i
== hhead
)
4950 if (ladded
== oldladded
)
4960 assert (heap
+ i
< hhead
);
4968 if (!lit_has_binary_clauses (NOTLIT (lit
)))
4979 LOG (fprintf (out
, "%strying %d as failed literal\n",
4980 prefix
, lit2int (lit
)));
4982 assign_decision (lit
);
4983 old_trail_count
= thead
- trail
;
4988 EXPLICITLY_FAILED_LITERAL
:
4989 LOG (fprintf (out
, "%sfound explicitly failed literal %d\n",
4990 prefix
, lit2int (lit
)));
5009 if (propagations
>= limit
)
5017 if (!lit_has_binary_clauses (NOTLIT (lit
)))
5029 LOG (fprintf (out
, "%strying %d as failed literals\n",
5030 prefix
, lit2int (lit
)));
5032 new_trail_count
= thead
- trail
;
5033 saved_count
= new_trail_count
- old_trail_count
;
5035 if (saved_count
> saved_size
)
5037 new_saved_size
= saved_size
? 2 * saved_size
: 1;
5038 while (saved_count
> new_saved_size
)
5039 new_saved_size
*= 2;
5041 RESIZEN (saved
, saved_size
, new_saved_size
);
5042 saved_size
= new_saved_size
;
5045 for (j
= 0; j
< saved_count
; j
++)
5047 other
= trail
[old_trail_count
+ j
];
5048 saved
[j
] = trail
[old_trail_count
+ j
];
5053 assign_decision (lit
);
5057 goto EXPLICITLY_FAILED_LITERAL
;
5059 pivot
= (thead
- trail
<= new_trail_count
) ? lit
: NOTLIT (lit
);
5062 for (j
= 0; j
< saved_count
; j
++)
5063 if ((other
= saved
[j
])->val
== TRUE
)
5064 saved
[common
++] = other
;
5070 "%sfound %d literals implied by %d and %d\n",
5072 lit2int (NOTLIT (lit
)), lit2int (lit
)));
5076 /* TODO: For some Velev benchmarks, extracting the common implicit
5077 * failed literals took quite some time. This needs to be fixed by
5078 * a dedicated analyzer. Up to then we bound the number of
5079 * propagations in this loop as well.
5081 && propagations
< limit
+ delta
5086 if (other
->val
== TRUE
)
5089 assert (!other
->val
);
5092 "%sforcing %d as forced implicitly failed literal\n",
5093 prefix
, lit2int (other
)));
5095 assert (pivot
!= NOTLIT (other
));
5096 assert (pivot
!= other
);
5098 assign_decision (NOTLIT (other
));
5101 assert (level
== 1);
5110 assign_decision (pivot
);
5117 assert (level
== 1);
5128 assign_decision (NOTLIT (pivot
));
5134 assert (level
== 1);
5166 fllimit
+= 9 * (propagations
- fllimit
); /* 10% for failed literals */
5170 /* First flush top level assigned literals. Those are prohibited from
5171 * being pushed up the heap during 'faillits' since 'simplifying' is set.
5173 assert (heap
< hhead
);
5174 for (p
= q
= heap
+ 1; p
< hhead
; p
++)
5177 v
= vars
+ (r
- rnks
);
5185 /* Then resort with respect to EVSIDS score and fix positions.
5187 sort (Rnk
*, cmp_inverse_rnk
, heap
+ 1, hhead
- (heap
+ 1));
5188 for (p
= heap
+ 1; p
< hhead
; p
++)
5189 (*p
)->pos
= p
- heap
;
5197 unsigned collect
, delta
;
5198 size_t bytes_collected
;
5202 assert (!satisfied ());
5203 assert (lsimplify
<= propagations
);
5204 assert (fsimplify
<= fixed
);
5219 for (p
= SOC
; p
!= EOC
; p
= NXC (p
))
5233 assert (!cls
->collect
);
5234 if (clause_is_toplevel_satisfied (cls
))
5236 mark_clause_to_be_collected (cls
);
5243 bytes_collected
= collect_clauses ();
5245 srecycled
+= bytes_collected
;
5249 delta
= 10 * (olits
+ llits
) + 100000;
5250 if (delta
> 2000000)
5252 lsimplify
= propagations
+ delta
;
5263 assert (bcp_queue_is_empty ());
5264 assert (isimplify
< fixed
);
5269 drestart
= MINRESTART
;
5270 lrestart
= conflicts
+ drestart
;
5278 cmp_activity (Cls
* c
, Cls
* d
)
5283 assert (c
->learned
);
5284 assert (d
->learned
);
5295 /* Prefer shorter clauses.
5297 if (c
->size
< d
->size
)
5300 if (c
->size
> d
->size
)
5309 unsigned rcount
, lcollect
, collect
, target
, ld
;
5310 size_t bytes_collected
;
5314 lastreduceconflicts
= conflicts
;
5316 assert (rhead
== resolved
);
5318 while (nlclauses
- llocked
> (unsigned)(eor
- resolved
))
5319 ENLARGE (resolved
, rhead
, eor
);
5324 for (p
= ((fsimplify
< fixed
) ? SOC
: lclauses
); p
!= EOC
; p
= NXC (p
))
5338 assert (!cls
->collect
);
5339 if (fsimplify
< fixed
&& clause_is_toplevel_satisfied (cls
))
5341 mark_clause_to_be_collected (cls
);
5344 if (cls
->learned
&& cls
->size
> 2)
5359 assert (rhead
< eor
);
5362 assert (rhead
<= eor
);
5366 rcount
= rhead
- resolved
;
5367 sort (Cls
*, cmp_activity
, resolved
, rcount
);
5369 assert (nlclauses
>= lcollect
);
5370 target
= nlclauses
- lcollect
+ 1;
5372 for (ld
= 1; ld
< 32 && ((unsigned) (1 << ld
)) < target
; ld
++)
5374 minact
= mulflt (cinc
, base2flt (1, -ld
));
5378 if (target
>= rcount
)
5382 else if (*CLS2ACT (resolved
[target
]) < minact
)
5384 /* If the distribution of clause activities is skewed and the median
5385 * is actually below the maximum average activity, then we collect all
5386 * clauses below this activity.
5388 while (++target
< rcount
&& *CLS2ACT (resolved
[target
]) < minact
)
5393 while (target
> 0 &&
5394 !cmp_activity (resolved
[target
- 1], resolved
[target
]))
5398 rhead
= resolved
+ target
;
5399 while (rhead
> resolved
)
5402 mark_clause_to_be_collected (cls
);
5405 if (cls
->learned
&& cls
->size
> 2) /* just for consistency */
5412 bytes_collected
= collect_clauses ();
5414 rrecycled
+= bytes_collected
;
5420 inc_lreduce (); /* avoid dead lock */
5422 assert (rhead
== resolved
);
5428 lreduce
= loadded
/ 2;
5434 if (lreduce
> 10000)
5440 "%s\n%sinitial reduction limit %u clauses\n%s\n",
5441 prefix
, prefix
, lreduce
, prefix
);
5447 unsigned res
= srng
;
5449 srng
+= 1013904223u;
5450 NOLOG (fprintf (out
, "%srng () = %u\n", prefix
, res
));
5455 rrng (unsigned low
, unsigned high
)
5457 unsigned long long tmp
;
5458 unsigned res
, elements
;
5459 assert (low
<= high
);
5460 elements
= high
- low
+ 1;
5466 NOLOG (fprintf (out
, "%srrng (%u, %u) = %u\n", prefix
, low
, high
, res
));
5467 assert (low
<= res
);
5468 assert (res
<= high
);
5473 decide_phase (Lit
* lit
)
5475 Lit
* not_lit
= NOTLIT (lit
);
5476 Var
*v
= LIT2VAR (lit
);
5478 assert (LIT2SGN (lit
) > 0);
5482 staticphasedecisions
++;
5484 if (defaultphase
> 0)
5486 /* assign to TRUE */
5488 else if (defaultphase
< 0)
5490 /* assign to FALSE */
5493 else if (*LIT2JWH(lit
) <= *LIT2JWH (not_lit
))
5495 /* assign to FALSE (Jeroslow-Wang says there are more short
5496 * clauses with negative occurence of this variable, so satisfy
5497 * those, to minimize BCP)
5503 /* assign to TRUE (... but strictly more positive occurrences) */
5508 /* repeat last phase: phase saving heuristic */
5512 /* assign to TRUE (last phase was TRUE as well) */
5516 /* assign to FALSE (last phase was FALSE as well) */
5525 gcd (unsigned a
, unsigned b
)
5553 unsigned idx
, delta
, spread
;
5557 if (rrng (1, spread
) != 2)
5560 assert (1 <= max_var
);
5561 idx
= rrng (1, max_var
);
5562 res
= int2lit (idx
);
5564 if (res
->val
!= UNDEF
)
5566 delta
= rrng (1, max_var
);
5567 while (gcd (delta
, max_var
) != 1)
5570 assert (1 <= delta
);
5571 assert (delta
<= max_var
);
5577 res
= int2lit (idx
);
5578 } while (res
->val
!= UNDEF
);
5584 res
= decide_phase (res
);
5585 LOG (fprintf (out
, "%srdecide %d\n", prefix
, lit2int (res
)));
5600 if (res
->val
== UNDEF
) break;
5603 NOLOG (fprintf (out
,
5604 "%shpop %u %u %u\n",
5606 FLTMANTISSA(r
->score
),
5607 FLTEXPONENT(r
->score
)));
5613 res
= decide_phase (res
);
5615 LOG (fprintf (out
, "%ssdecide %d\n", prefix
, lit2int (res
)));
5626 assert (als
< alshead
);
5627 assert (!failed_assumption
);
5629 while (alstail
< alshead
)
5633 if (lit
->val
== FALSE
)
5635 failed_assumption
= lit
;
5640 LOG (fprintf (out
, "%sfailed assumption %d\n",
5641 prefix
, lit2int (failed_assumption
)));
5645 if (lit
->val
== TRUE
)
5651 LOG (fprintf (out
, "%sadecide %d\n", prefix
, lit2int (lit
)));
5652 adecidelevel
= level
+ 1;
5665 assert (!satisfied ());
5668 if (alstail
< alshead
&& (lit
= adecide ()))
5670 else if (failed_assumption
)
5672 else if (satisfied ())
5674 else if (!(lit
= rdecide ()))
5678 assign_decision (lit
);
5687 int count
= 0, backtracked
;
5696 return PICOSAT_UNSATISFIABLE
;
5701 if (lsimplify
<= propagations
)
5705 return PICOSAT_UNSATISFIABLE
;
5728 return PICOSAT_UNSATISFIABLE
;
5737 original_clauses_satisfied ();
5738 assumptions_satisfied ();
5740 return PICOSAT_SATISFIABLE
;
5746 if (!level
&& isimplify
< fixed
)
5750 if (count
>= l
) /* decision limit reached ? */
5751 return PICOSAT_UNKNOWN
;
5754 if (!adodisabled
&& adoconflicts
>= adoconflictlimit
)
5756 assert (bcp_queue_is_empty ());
5757 return PICOSAT_UNKNOWN
;
5761 if (fsimplify
< fixed
&& lsimplify
<= propagations
)
5764 if (!bcp_queue_is_empty ())
5768 return PICOSAT_UNSATISFIABLE
;
5771 return PICOSAT_SATISFIABLE
;
5780 if (need_to_reduce ())
5783 if (conflicts
>= lrestart
&& level
> 2)
5787 if (failed_assumption
)
5788 return PICOSAT_UNSATISFIABLE
;
5798 unsigned idx
, prev
, this, delta
, i
, lcore
, vcore
;
5799 unsigned *stack
, *shead
, *eos
;
5808 assert (mtcls
|| failed_assumption
);
5812 lcore
= ocore
= vcore
= 0;
5814 stack
= shead
= eos
= 0;
5815 ENLARGE (stack
, shead
, eos
);
5819 idx
= CLS2IDX (mtcls
);
5824 assert (failed_assumption
);
5825 v
= LIT2VAR (failed_assumption
);
5828 idx
= CLS2IDX (v
->reason
);
5833 while (shead
> stack
)
5836 zhain
= IDX2ZHN (idx
);
5846 cls
= IDX2CLS (idx
);
5849 assert (!cls
->core
);
5856 for (p
= zhain
->znt
; (byte
= *p
); p
++, i
+= 7)
5858 delta
|= (byte
& 0x7f) << i
;
5862 this = prev
+ delta
;
5863 assert (prev
< this); /* no overflow */
5866 ENLARGE (stack
, shead
, eos
);
5876 cls
= IDX2CLS (idx
);
5879 assert (!cls
->learned
);
5887 eol
= end_of_lits (cls
);
5888 for (q
= cls
->lits
; q
< eol
; q
++)
5900 DELETEN (stack
, eos
- stack
);
5904 "%s%u core variables out of %u (%.1f%%)\n"
5905 "%s%u core original clauses out of %u (%.1f%%)\n"
5906 "%s%u core learned clauses out of %u (%.1f%%)\n",
5907 prefix
, vcore
, max_var
, PERCENT (vcore
, max_var
),
5908 prefix
, ocore
, oadded
, PERCENT (ocore
, oadded
),
5909 prefix
, lcore
, ladded
, PERCENT (lcore
, ladded
));
5915 write_unsigned (unsigned d
, FILE * file
)
5917 static char write_unsigned_buffer
[20];
5921 assert (sizeof d
<= 4);
5923 res
= write_unsigned_buffer
+ sizeof write_unsigned_buffer
;
5927 assert (res
> write_unsigned_buffer
);
5928 *--res
= '0' + (tmp
% 10);
5936 trace_lits (Cls
* cls
, FILE * file
)
5938 Lit
**p
, **eol
= end_of_lits (cls
);
5943 for (p
= cls
->lits
; p
< eol
; p
++)
5945 write_int (LIT2INT (*p
), file
);
5953 write_idx (unsigned idx
, FILE * file
)
5955 write_unsigned (EXPORTIDX (idx
), file
);
5959 trace_clause (unsigned idx
, Cls
* cls
, FILE * file
, int fmt
)
5963 assert (fmt
== RUP_TRACE_FMT
|| !cls
->learned
);
5964 assert (CLS2IDX (cls
) == idx
);
5966 if (fmt
!= RUP_TRACE_FMT
)
5968 write_idx (idx
, file
);
5972 trace_lits (cls
, file
);
5974 if (fmt
!= RUP_TRACE_FMT
)
5981 trace_zhain (unsigned idx
, Zhn
* zhain
, FILE * file
, int fmt
)
5983 unsigned prev
, this, delta
, i
;
5988 assert (zhain
->core
);
5990 write_idx (idx
, file
);
5993 if (fmt
== EXTENDED_TRACECHECK_TRACE_FMT
)
5995 cls
= IDX2CLS (idx
);
5997 trace_lits (cls
, file
);
6001 assert (fmt
== COMPACT_TRACECHECK_TRACE_FMT
);
6009 for (p
= zhain
->znt
; (byte
= *p
); p
++, i
+= 7)
6011 delta
|= (byte
& 0x7f) << i
;
6015 this = prev
+ delta
;
6018 write_idx (this, file
);
6025 fputs (" 0\n", file
);
6029 write_core (FILE * file
)
6034 fprintf (file
, "p cnf %u %u\n", max_var
, core ());
6036 for (p
= SOC
; p
!= EOC
; p
= NXC (p
))
6040 if (!cls
|| cls
->learned
|| !cls
->core
)
6043 eol
= end_of_lits (cls
);
6044 for (q
= cls
->lits
; q
< eol
; q
++)
6046 write_int (LIT2INT (*q
), file
);
6050 fputs ("0\n", file
);
6057 write_trace (FILE * file
, int fmt
)
6066 if (fmt
== RUP_TRACE_FMT
)
6068 rupvariables
= picosat_variables (),
6069 rupclauses
= picosat_added_original_clauses ();
6070 write_rup_header (file
);
6073 for (p
= SOC
; p
!= EOC
; p
= NXC (p
))
6077 if (oclauses
<= p
&& p
< eoo
)
6079 i
= OIDX2IDX (p
- oclauses
);
6080 assert (!cls
|| CLS2IDX (cls
) == i
);
6084 assert (lclauses
<= p
&& p
< eol
);
6085 i
= LIDX2IDX (p
- lclauses
);
6088 zhain
= IDX2ZHN (i
);
6094 if (fmt
== RUP_TRACE_FMT
)
6095 trace_clause (i
, cls
, file
, fmt
);
6097 trace_zhain (i
, zhain
, file
, fmt
);
6102 if (fmt
!= RUP_TRACE_FMT
&& cls
)
6105 trace_clause (i
, cls
, file
, fmt
);
6116 write_core_wrapper (FILE * file
, int fmt
)
6127 import_lit (int lit
)
6129 ABORTIF (lit
== INT_MIN
, "API usage: INT_MIN literal");
6131 while (abs (lit
) > (int) max_var
)
6134 return int2lit (lit
);
6145 for (i
= 1; i
<= max_var
; i
++)
6148 for (p
= SOC
; p
!= EOC
; p
= NXC (p
))
6152 for (q
= zhains
; q
!= zhead
; q
++)
6161 reset_assumptions (void)
6165 failed_assumption
= 0;
6166 alstail
= alshead
= als
;
6169 if (extracted_all_failed_assumptions
)
6171 for (p
= als
; p
< alshead
; p
++)
6172 LIT2VAR (*p
)->failed
= 0;
6174 extracted_all_failed_assumptions
= 0;
6181 ABORTIF (state
== RESET
, "API usage: uninitialized");
6185 check_sat_state (void)
6187 ABORTIF (state
!= SAT
, "API usage: expected to be in SAT state");
6191 check_unsat_state (void)
6193 ABORTIF (state
!= UNSAT
, "API usage: expected to be in UNSAT state");
6197 check_sat_or_unsat_or_unknown_state (void)
6199 ABORTIF (state
!= SAT
&& state
!= UNSAT
&& state
!= UNKNOWN
,
6200 "API usage: expected to be in SAT, UNSAT, or UNKNOWN state");
6204 reset_incremental_usage (void)
6206 unsigned num_non_false
;
6209 check_sat_or_unsat_or_unknown_state ();
6211 LOG (fprintf (out
, "%sRESET incremental usage\n", prefix
));
6216 reset_assumptions ();
6221 for (q
= conflict
->lits
; q
< end_of_lits (conflict
); q
++)
6224 if (lit
->val
!= FALSE
)
6228 // assert (num_non_false >= 2); // TODO: why this assertion?
6229 #ifdef NO_BINARY_CLAUSES
6230 if (conflict
== &cimpl
)
6234 if (conflict
== adoconflict
)
6235 resetadoconflict ();
6244 saved_flips
= flips
;
6245 min_flipped
= UINT_MAX
;
6246 saved_max_var
= max_var
;
6258 entered
= picosat_time_stamp ();
6272 check_trace_support_and_execute (FILE * file
, void (*f
)(FILE*,int), int fmt
)
6275 check_unsat_state ();
6277 ABORTIF (!trace
, "API usage: tracing disabled");
6285 ABORT ("compiled without trace support");
6290 extract_all_failed_assumptions (void)
6297 assert (failed_assumption
);
6298 assert (mhead
== marked
);
6301 ENLARGE (marked
, mhead
, eom
);
6303 v
= LIT2VAR (failed_assumption
);
6307 while (pos
< mhead
- marked
)
6314 eol
= end_of_lits (c
);
6315 for (p
= c
->lits
; p
< eol
; p
++)
6323 for (p
= als
; p
< alshead
; p
++)
6330 while (mhead
> marked
)
6331 (*--mhead
)->mark
= 0;
6335 picosat_copyright (void)
6337 return "Copyright (c) 2006 - 2009 Armin Biere JKU Linz";
6347 picosat_adjust (int new_max_var
)
6349 unsigned new_size_vars
;
6353 new_max_var
= abs (new_max_var
);
6354 new_size_vars
= new_max_var
+ 1;
6356 if (size_vars
< new_size_vars
)
6357 enlarge (new_size_vars
);
6359 while (max_var
< (unsigned) new_max_var
)
6366 picosat_inc_max_var (void)
6368 if (measurealltimeinlib
)
6375 if (measurealltimeinlib
)
6382 picosat_set_verbosity (int new_verbosity_level
)
6385 verbosity
= new_verbosity_level
;
6389 picosat_enable_trace_generation (void)
6393 ABORTIF (addedclauses
,
6394 "API usage: trace generation enabled after adding clauses");
6400 picosat_set_incremental_rup_file (FILE * rup_file
, int m
, int n
)
6403 assert (!rupstarted
);
6410 picosat_set_output (FILE * output_file
)
6417 picosat_measure_all_calls (void)
6420 measurealltimeinlib
= 1;
6424 picosat_set_prefix (const char * str
)
6431 picosat_set_seed (unsigned s
)
6438 picosat_reset (void)
6445 picosat_add (int int_lit
)
6449 if (measurealltimeinlib
)
6454 ABORTIF (rup
&& rupstarted
&& oadded
>= (unsigned)rupclauses
,
6455 "API usage: adding too many clauses after RUP header written");
6457 ABORTIF (addingtoado
,
6458 "API usage: 'picosat_add' and 'picosat_add_ado_lit' mixed");
6461 reset_incremental_usage ();
6463 lit
= import_lit (int_lit
);
6468 simplify_and_add_original_clause ();
6470 if (measurealltimeinlib
)
6475 picosat_add_ado_lit (int external_lit
)
6480 if (measurealltimeinlib
)
6486 reset_incremental_usage ();
6488 ABORTIF (!addingtoado
&& ahead
> added
,
6489 "API usage: 'picosat_add' and 'picosat_add_ado_lit' mixed");
6494 internal_lit
= import_lit (external_lit
);
6495 add_lit (internal_lit
);
6502 if (measurealltimeinlib
)
6505 (void) external_lit
;
6506 ABORT ("compiled without all different constraint support");
6511 picosat_assume (int int_lit
)
6515 if (measurealltimeinlib
)
6521 reset_incremental_usage ();
6523 lit
= import_lit (int_lit
);
6524 if (alshead
== eoals
)
6526 assert (alstail
== als
);
6527 ENLARGE (als
, alshead
, eoals
);
6533 if (measurealltimeinlib
)
6546 LOG (fprintf (out
, "%sSTART call %u\n", prefix
, calls
));
6552 ABORT ("API usage: incomplete all different constraint");
6555 ABORT ("API usage: incomplete clause");
6559 reset_incremental_usage ();
6563 assert (state
== READY
);
6567 case PICOSAT_UNSATISFIABLE
:
6571 case PICOSAT_SATISFIABLE
:
6588 LOG (fprintf (out
, "%sEND call %u\n", prefix
, calls
));
6594 picosat_deref (int int_lit
)
6600 ABORTIF (!int_lit
, "API usage: can not deref zero literal");
6601 ABORTIF (mtcls
, "API usage: deref after empty clause generated");
6607 if (abs (int_lit
) > (int) max_var
)
6610 lit
= int2lit (int_lit
);
6612 if (lit
->val
== TRUE
)
6615 if (lit
->val
== FALSE
)
6622 picosat_deref_toplevel (int int_lit
)
6628 ABORTIF (!int_lit
, "API usage: can not deref zero literal");
6629 ABORTIF (mtcls
, "API usage: deref after empty clause generated");
6634 if (abs (int_lit
) > (int) max_var
)
6637 lit
= int2lit (int_lit
);
6643 if (lit
->val
== TRUE
)
6646 if (lit
->val
== FALSE
)
6653 picosat_inconsistent (void)
6660 picosat_corelit (int int_lit
)
6665 check_unsat_state ();
6666 ABORTIF (!int_lit
, "API usage: zero literal can not be in core");
6668 assert (mtcls
|| failed_assumption
);
6674 ABORTIF (!trace
, "tracing disabled");
6675 if (measurealltimeinlib
)
6678 if (abs (int_lit
) <= (int) max_var
)
6679 res
= vars
[abs (int_lit
)].core
;
6680 assert (!res
|| vars
[abs (int_lit
)].used
);
6681 if (measurealltimeinlib
)
6685 ABORT ("compiled without trace support");
6692 picosat_failed_assumption (int int_lit
)
6696 ABORTIF (!int_lit
, "API usage: zero literal as assumption");
6698 check_unsat_state ();
6701 assert (failed_assumption
);
6702 if (abs (int_lit
) > (int) max_var
)
6704 if (!extracted_all_failed_assumptions
)
6705 extract_all_failed_assumptions ();
6706 lit
= import_lit (int_lit
);
6712 picosat_usedlit (int int_lit
)
6716 check_sat_or_unsat_or_unknown_state ();
6717 ABORTIF (!int_lit
, "API usage: zero literal can not be used");
6718 int_lit
= abs (int_lit
);
6719 res
= (int_lit
<= (int) max_var
) ? vars
[int_lit
].used
: 0;
6724 picosat_write_clausal_core (FILE * file
)
6726 check_trace_support_and_execute (file
, write_core_wrapper
, 0);
6730 picosat_write_compact_trace (FILE * file
)
6732 check_trace_support_and_execute (file
, write_trace
,
6733 COMPACT_TRACECHECK_TRACE_FMT
);
6737 picosat_write_extended_trace (FILE * file
)
6739 check_trace_support_and_execute (file
, write_trace
,
6740 EXTENDED_TRACECHECK_TRACE_FMT
);
6744 picosat_write_rup_trace (FILE * file
)
6746 check_trace_support_and_execute (file
, write_trace
, RUP_TRACE_FMT
);
6750 picosat_max_bytes_allocated (void)
6757 picosat_variables (void)
6760 return (int) max_var
;
6764 picosat_added_original_clauses (void)
6767 return (int) oadded
;
6771 picosat_stats (void)
6776 assert (sdecisions
+ rdecisions
+ assumptions
== decisions
);
6779 fprintf (out
, "%s%u calls\n", prefix
, calls
);
6780 fprintf (out
, "%s%u iterations\n", prefix
, iterations
);
6781 fprintf (out
, "%s%u restarts", prefix
, restarts
);
6783 fprintf (out
, " (%u skipped)", skippedrestarts
);
6787 fprintf (out
, "%s%u failed literals", prefix
, failedlits
);
6790 ", %u calls, %u rounds, %llu propagations",
6791 flcalls
, flrounds
, flprops
);
6796 "%sfl: %u = %.1f%% implicit, %llu oopsed, %llu tried, %llu skipped\n",
6798 ifailedlits
, PERCENT (ifailedlits
, failedlits
),
6799 floopsed
, fltried
, flskipped
);
6802 fprintf (out
, "%s%u conflicts", prefix
, conflicts
);
6804 fprintf (out
, " (%u uips = %.1f%%)\n", uips
, PERCENT(uips
,conflicts
));
6809 fprintf (out
, "%s%u adc conflicts\n", prefix
, adoconflicts
);
6812 fprintf (out
, "%s%llu dereferenced literals\n", prefix
, derefs
);
6814 fprintf (out
, "%s%u decisions", prefix
, decisions
);
6816 fprintf (out
, " (%u random = %.2f%%",
6817 rdecisions
, PERCENT (rdecisions
, decisions
));
6818 fprintf (out
, ", %u assumptions", assumptions
);
6824 "%s%u static phase decisions (%.1f%% of all variables)\n",
6826 staticphasedecisions
, PERCENT (staticphasedecisions
, max_var
));
6828 fprintf (out
, "%s%u fixed variables\n", prefix
, fixed
);
6829 assert (nonminimizedllits
>= minimizedllits
);
6830 redlits
= nonminimizedllits
- minimizedllits
;
6831 fprintf (out
, "%s%u learned literals\n", prefix
, llitsadded
);
6832 fprintf (out
, "%s%.1f%% deleted literals\n",
6833 prefix
, PERCENT (redlits
, nonminimizedllits
));
6836 #ifndef NO_BINARY_CLAUSES
6838 "%s%llu antecedents (%.1f antecedents per clause",
6839 prefix
, antecedents
, AVERAGE (antecedents
, conflicts
));
6843 fprintf (out
, ", %.1f bytes/antecedent)", AVERAGE (znts
, antecedents
));
6845 #if !defined(NO_BINARY_CLAUSES) || defined(TRACE)
6849 fprintf (out
, "%s%llu propagations (%.1f propagations per decision)\n",
6850 prefix
, propagations
, AVERAGE (propagations
, decisions
));
6851 fprintf (out
, "%s%llu visits (%.1f per propagation)\n",
6852 prefix
, visits
, AVERAGE (visits
, propagations
));
6854 "%s%llu binary clauses visited (%.1f%% %.1f per propagation)\n",
6856 PERCENT (bvisits
, visits
),
6857 AVERAGE (bvisits
, propagations
));
6859 "%s%llu ternary clauses visited (%.1f%% %.1f per propagation)\n",
6861 PERCENT (tvisits
, visits
),
6862 AVERAGE (tvisits
, propagations
));
6864 "%s%llu large clauses visited (%.1f%% %.1f per propagation)\n",
6866 PERCENT (lvisits
, visits
),
6867 AVERAGE (lvisits
, propagations
));
6868 fprintf (out
, "%s%llu other true (%.1f%% of visited clauses)\n",
6869 prefix
, othertrue
, PERCENT (othertrue
, visits
));
6871 "%s%llu other true in binary clauses (%.1f%%)"
6872 ", %llu upper (%.1f%%)\n",
6873 prefix
, othertrue2
, PERCENT (othertrue2
, othertrue
),
6874 othertrue2u
, PERCENT (othertrue2u
, othertrue2
));
6876 "%s%llu other true in large clauses (%.1f%%)"
6877 ", %llu upper (%.1f%%)\n",
6878 prefix
, othertruel
, PERCENT (othertruel
, othertrue
),
6879 othertruelu
, PERCENT (othertruelu
, othertruel
));
6880 fprintf (out
, "%s%llu ternary and large traversals (%.1f per visit)\n",
6881 prefix
, traversals
, AVERAGE (traversals
, visits
));
6882 fprintf (out
, "%s%llu large traversals (%.1f per large visit)\n",
6883 prefix
, ltraversals
, AVERAGE (ltraversals
, lvisits
));
6884 fprintf (out
, "%s%llu assignments\n", prefix
, assignments
);
6886 fprintf (out
, "%s%llu propagations\n", prefix
, propagations
);
6888 fprintf (out
, "%s%.1f%% variables used\n", prefix
, PERCENT (vused
, max_var
));
6891 fprintf (out
, "%s%.1f seconds in library\n", prefix
, seconds
);
6892 fprintf (out
, "%s%.1f megaprops/second\n",
6893 prefix
, AVERAGE (propagations
/ 1e6f
, seconds
));
6895 fprintf (out
, "%s%.1f million visits per second\n",
6896 prefix
, AVERAGE (visits
/ 1e6f
, seconds
));
6898 "%srecycled %.1f MB in %u reductions\n",
6899 prefix
, rrecycled
/ (double) (1 << 20), reductions
);
6901 "%srecycled %.1f MB in %u simplifications\n",
6902 prefix
, srecycled
/ (double) (1 << 20), simps
);
6904 fprintf (out
, "%s%u simplifications\n", prefix
, simps
);
6905 fprintf (out
, "%s%u reductions\n", prefix
, reductions
);
6906 fprintf (out
, "%s%.1f MB recycled\n", prefix
, recycled
/ (double) (1 << 20));
6908 fprintf (out
, "%s%.1f MB maximally allocated\n",
6909 prefix
, picosat_max_bytes_allocated () / (double) (1 << 20));
6913 #include <sys/time.h>
6914 #include <sys/resource.h>
6915 #include <sys/unistd.h>
6919 picosat_time_stamp (void)
6925 if (!getrusage (RUSAGE_SELF
, &u
))
6927 res
+= u
.ru_utime
.tv_sec
+ 1e-6 * u
.ru_utime
.tv_usec
;
6928 res
+= u
.ru_stime
.tv_sec
+ 1e-6 * u
.ru_stime
.tv_usec
;
6935 picosat_seconds (void)
6942 picosat_print (FILE * file
)
6944 #ifdef NO_BINARY_CLAUSES
6945 Lit
* lit
, *other
, * last
;
6952 if (measurealltimeinlib
)
6960 for (p
= SOC
; p
!= EOC
; p
= NXC (p
))
6974 #ifdef NO_BINARY_CLAUSES
6975 last
= int2lit (-max_var
);
6976 for (lit
= int2lit (1); lit
<= last
; lit
++)
6978 stack
= LIT2IMPLS (lit
);
6979 eol
= stack
->start
+ stack
->count
;
6980 for (q
= stack
->start
; q
< eol
; q
++)
6986 fprintf (file
, "p cnf %d %u\n", max_var
, n
);
6988 for (p
= SOC
; p
!= EOC
; p
= NXC (p
))
6999 eol
= end_of_lits (cls
);
7000 for (q
= cls
->lits
; q
< eol
; q
++)
7002 write_int (lit2int (*q
), file
);
7006 fputs ("0\n", file
);
7009 #ifdef NO_BINARY_CLAUSES
7010 last
= int2lit (-max_var
);
7011 for (lit
= int2lit (1); lit
<= last
; lit
++)
7013 stack
= LIT2IMPLS (lit
);
7014 eol
= stack
->start
+ stack
->count
;
7015 for (q
= stack
->start
; q
< eol
; q
++)
7016 if ((other
= *q
) >= lit
)
7017 fprintf (file
, "%d %d 0\n", lit2int (lit
), lit2int (other
));
7023 for (r
= als
; r
< alshead
; r
++)
7024 fprintf (file
, "%d 0\n", lit2int (*r
));
7029 if (measurealltimeinlib
)
7034 picosat_enter (void)
7040 picosat_leave (void)
7046 picosat_message (int level
, const char * fmt
, ...)
7050 if (level
> verbosity
)
7053 fputs (prefix
, out
);
7055 vfprintf (out
, fmt
, ap
);
7061 picosat_changed (void)
7068 res
= (min_flipped
<= saved_max_var
);
7069 assert (!res
|| saved_flips
!= flips
);
7075 setemgr (void * nmgr
)
7077 ABORTIF (emgr
&& emgr
!= nmgr
,
7078 "API usage: mismatched external memory managers");
7083 picosat_set_new (void * nmgr
, void * (*nnew
)(void*,size_t))
7085 ABORTIF (state
!= RESET
,
7086 "API usage: 'picosat_set_new' after 'picosat_init'");
7092 picosat_set_resize (void * nmgr
, void * (*nresize
)(void*,void*,size_t,size_t))
7094 ABORTIF (state
!= RESET
,
7095 "API usage: 'picosat_set_resize' after 'picosat_init'");
7101 picosat_set_delete (void * nmgr
, void (*ndelete
)(void*,void*,size_t))
7103 ABORTIF (state
!= RESET
,
7104 "API usage: 'picosat_set_delete' after 'picosat_init'");
7110 picosat_set_global_default_phase (int phase
)
7113 defaultphase
= phase
;
7117 picosat_set_default_phase_lit (int int_lit
, int phase
)
7125 lit
= import_lit (int_lit
);
7130 newphase
= (int_lit
< 0) == (phase
< 0);
7131 v
->phase
= newphase
;
7141 picosat_ado_conflicts (void)
7144 return adoconflicts
;
7148 picosat_disable_ado (void)
7151 assert (!adodisabled
);
7156 picosat_enable_ado (void)
7159 assert (adodisabled
);
7164 picosat_set_ado_conflict_limit (unsigned newadoconflictlimit
)
7167 adoconflictlimit
= newadoconflictlimit
;