1 /***************************************************************************
2 Copyright (c) 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 ****************************************************************************/
23 #ifndef PrecoSat_hh_INCLUDED
24 #define PrecoSat_hh_INCLUDED
35 void die (const char *, ...);
39 typedef void * (*NewFun
)(void *, size_t);
40 typedef void (*DeleteFun
)(void *, void*, size_t);
41 typedef void * (*ResizeFun
)(void *, void *, size_t, size_t);
44 void * emgr
; NewFun newfun
; DeleteFun deletefun
; ResizeFun resizefun
;
45 void operator += (size_t b
) { if ((cur
+= b
) > max
) max
= cur
; }
46 void operator -= (size_t b
) { assert (cur
>= b
); cur
-= b
; }
48 Mem () : cur(0), max(0), emgr(0), newfun(0), deletefun(0), resizefun(0) { }
49 void set (void * e
, NewFun n
, DeleteFun d
, ResizeFun r
) {
50 assert (e
&& n
&& d
&& r
);
51 emgr
= e
; newfun
= n
; deletefun
= d
; resizefun
= r
;
53 operator size_t () const { return cur
; }
54 size_t getCurrent () const { return cur
; }
55 size_t getMax () const { return max
; }
56 void * allocate (size_t bytes
) {
57 size_t mb
= bytes
>> 20;
59 res
= newfun
? newfun (emgr
, bytes
) : malloc (bytes
);
60 if (!res
) die ("out of memory allocating %d MB", mb
);
64 void * callocate (size_t bytes
) {
65 void * res
= allocate (bytes
);
66 memset (res
, 0, bytes
);
69 void * reallocate (void * ptr
, size_t old_bytes
, size_t new_bytes
) {
70 size_t mb
= new_bytes
>> 20;
72 void * res
= resizefun
? resizefun (emgr
, ptr
, old_bytes
, new_bytes
) :
73 realloc (ptr
, new_bytes
);
74 if (!res
) die ("out of memory reallocating %ld MB", (long) mb
);
78 void * recallocate (void * ptr
, size_t o
, size_t n
) {
79 char * res
= (char*) reallocate (ptr
, o
, n
);
80 if (n
> o
) memset (res
+ o
, 0, n
- o
);
83 void deallocate (void * ptr
, size_t bytes
) {
85 if (deletefun
) deletefun (emgr
, ptr
, bytes
);
90 template<class T
> class Stack
{
92 int size () const { return e
- a
; }
94 size_t bytes () const { return size () * sizeof (T
); }
96 void enlarge (Mem
& m
) {
100 int s
= o
? 2 * o
: 1;
101 size_t nb
= s
* sizeof (T
);
102 a
= (T
*) m
.reallocate (a
, ob
, nb
);
107 Stack () : a (0), t (0), e (0) { }
108 ~Stack () { free (a
); }
109 operator int () const { return t
- a
; }
110 void push (Mem
& m
, const T
& d
) { if (t
== e
) enlarge (m
); *t
++ = d
; }
111 const T
& pop () { assert (a
< t
); return *--t
; }
112 const T
& top () { assert (a
< t
); return t
[-1]; }
113 T
& operator [] (int i
) { assert (i
< *this); return a
[i
]; }
114 void shrink (int m
= 0) { assert (m
<= *this); t
= a
+ m
; }
115 void shrink (T
* nt
) { assert (a
<= nt
); assert (nt
<= t
); t
= nt
; }
116 void release (Mem
& m
) { m
.deallocate (a
, bytes ()); a
= t
= e
= 0; }
117 const T
* begin () const { return a
; }
118 const T
* end () const { return t
; }
119 T
* begin () { return a
; }
120 T
* end () { return t
; }
121 void remove (const T
& d
) {
124 if (prev
== d
) return;
130 if (next
== d
) return;
136 template<class T
, class L
> class Heap
{
138 static int left (int p
) { return 2 * p
+ 1; }
139 static int right (int p
) { return 2 * p
+ 2; }
140 static int parent (int c
) { return (c
- 1) / 2; }
141 static void fix (T
* & ptr
, ptrdiff_t diff
) {
142 char * charptr
= (char *) ptr
;
147 void release (Mem
& mem
) { stack
.release (mem
); }
148 operator int () const { return stack
; }
149 T
* operator [] (int i
) { return stack
[i
]; }
150 bool contains (T
* e
) const { return e
->pos
>= 0; }
154 int ppos
= parent (epos
);
155 T
* p
= stack
[ppos
];
157 stack
[epos
] = p
, stack
[ppos
] = e
;
158 p
->pos
= epos
, epos
= ppos
;
163 assert (contains (e
));
164 int epos
= e
->pos
, size
= stack
;
166 int cpos
= left (epos
);
167 if (cpos
>= size
) break;
168 T
* c
= stack
[cpos
], * o
;
169 int opos
= right (epos
);
171 if (opos
>= size
) break;
175 } else if (opos
< size
) {
177 if (!L (c
, o
)) { cpos
= opos
; c
= o
; }
179 stack
[cpos
] = e
, stack
[epos
] = c
;
180 c
->pos
= epos
, epos
= cpos
;
186 for (int ppos
= 0; ppos
< stack
; ppos
++) {
188 int lpos
= left (ppos
);
193 int rpos
= right (ppos
);
202 for (int cpos
= parent (stack
-1); cpos
>= 0; cpos
--) {
203 T
* e
= stack
[cpos
]; assert (cpos
>= 0); down (e
);
207 T
* max () { assert (stack
); return stack
[0]; }
208 void push (Mem
& mem
, T
* e
) {
209 assert (!contains (e
));
220 T
* other
= stack
[size
];
221 assert (other
->pos
== size
);
222 stack
[0] = other
, other
->pos
= 0;
230 void remove (T
* e
) {
233 assert (contains (e
));
236 if (--size
== epos
) {
239 T
* last
= stack
[size
];
240 if (size
== epos
) return;
241 stack
[last
->pos
= epos
] = last
;
247 void fix (ptrdiff_t diff
) {
248 for (T
** p
= stack
.begin (); p
< stack
.end (); p
++)
253 template<class A
, class E
>
254 void dequeue (A
& anchor
, E
* e
) {
255 if (anchor
.head
== e
) { assert (!e
->next
); anchor
.head
= e
->prev
; }
256 else { assert (e
->next
); e
->next
->prev
= e
->prev
; }
257 if (anchor
.tail
== e
) { assert (!e
->prev
); anchor
.tail
= e
->next
; }
258 else { assert (e
->prev
); e
->prev
->next
= e
->next
; }
259 e
->prev
= e
->next
= 0;
260 assert (anchor
.count
> 0);
264 template<class A
, class E
>
265 bool connected (A
& anchor
, E
* e
) {
266 if (e
->prev
) return true;
267 if (e
->next
) return true;
268 return anchor
.head
== e
;
271 template<class A
, class E
>
272 void push (A
& anchor
, E
* e
) {
274 if (anchor
.head
) anchor
.head
->next
= e
;
275 e
->prev
= anchor
.head
;
277 if (!anchor
.tail
) anchor
.tail
= e
;
281 template<class A
, class E
>
282 void enqueue (A
& anchor
, E
* e
) {
284 if (anchor
.tail
) anchor
.tail
->prev
= e
;
285 e
->next
= anchor
.tail
;
287 if (!anchor
.head
) anchor
.head
= e
;
291 template<class A
, class E
>
292 void mtf (A
& a
, E
* e
) { dequeue (a
, e
); push (a
, e
); }
296 template<class E
> struct Anchor
{
299 Anchor () : head (0), tail (0), count (0) { }
302 struct Rnk
{ int heat
; int pos
; };
306 Hotter (Rnk
* r
, Rnk
* s
) : a (r
), b (s
) { }
307 operator bool () const {
308 if (a
->heat
> b
->heat
) return true;
309 if (a
->heat
< b
->heat
) return false;
314 typedef signed char Val
;
325 typedef enum Vrt Vrt
;
329 bool onstack
:1,removable
:1,poison
:1;
333 int tlevel
, dlevel
, dominator
;
334 union { Cls
* cls
; int lit
; } reason
;
338 static const unsigned LDMAXGLUE
= 4, MAXGLUE
= (1<<LDMAXGLUE
)-1;
339 bool locked
:1,lnd
:1,garbage
:1;
340 bool binary
:1,trash
:1,dirty
:1;
341 bool gate
:1,str
:1,fresh
:1;
342 static const int LDMAXSZ
= 32 - 10 - LDMAXGLUE
, MAXSZ
= (1<<LDMAXSZ
)-1;
344 unsigned glue
:LDMAXGLUE
, size
:LDMAXSZ
, sig
;
347 static size_t bytes (int n
);
348 size_t bytes () const;
349 Cls (int l0
= 0, int l1
= 0, int l2
= 0)
350 { lits
[0] = l0
; lits
[1] = l1
; lits
[2] = l2
; lits
[3] = 0; }
352 bool contains (int) const;
353 void print (const char * prefix
= "") const;
357 bool pulled
: 1, contained
:1;
359 Frame (int t
) : pulled (false), contained (false), tlevel (t
) { }
362 struct GateStats
{ int count
, len
; };
365 struct { int fixed
, equiv
, elim
, subst
, zombies
, pure
, merged
; } vars
;
366 struct { int orig
, bin
, lnd
, irr
, lckd
, gc
; } clauses
;
367 struct { long long added
; int bssrs
, ssrs
; } lits
;
368 struct { long long deleted
, strong
, inverse
; int depth
; } mins
;
369 int conflicts
, decisions
, random
, enlarged
, shrunken
, rescored
, iter
;
370 struct { int count
, skipped
, maxdelta
; } restart
;
371 struct { int count
, level1
, probing
; } doms
;
372 struct { GateStats nots
, ites
, ands
, xors
; } subst
;
373 struct { int fw
, bw
, dyn
, org
, doms
, red
; } subs
;
374 struct { long long resolutions
; int impl
, expl
, phases
, rounds
; } blkd
;
375 struct { int fw
, bw
, dyn
, org
, asym
; } str
;
376 struct { struct { int bin
, trn
, large
; } dyn
, stat
; } otfs
;
377 struct { long long slimmed
, sum
, count
; } glue
;
378 struct { int count
, maxdelta
; } rebias
;
379 struct { int variables
, phases
, rounds
, failed
, lifted
, merged
; } probe
;
380 struct { int nontriv
, fixed
, merged
; } sccs
;
381 struct { int forced
, assumed
, flipped
; } extend
;
382 struct { long long resolutions
; int phases
, rounds
; } elim
;
383 struct { struct { struct { long long srch
,hits
; } l1
,l2
;} fw
,bw
;} sigs
;
384 struct { int expl
, elim
, blkd
; } pure
;
385 struct { int expl
, elim
, blkd
; } zombies
;
386 struct { long long srch
, simp
; } props
;
387 long long visits
, ternaryvisits
, blocked
, sumheight
, collected
;
388 int simps
, reductions
, gcs
, reports
, maxdepth
, printed
;
389 double entered
, time
, simptime
, srchtime
, entered2
;
390 static double now ();
399 int decisions
, simp
, strength
;
400 struct { int conflicts
, inc
, init
; } enlarge
;
401 struct { int conflicts
, lcnt
, inner
, outer
; } restart
;
402 struct { int conflicts
, lcnt
; } rebias
;
403 struct { int learned
, fresh
, init
; } reduce
;
404 struct { int iter
, reduce
, probe
, elim
, block
, simp
; } fixed
;
405 struct { long long simp
, probe
, elim
, block
, asym
; } props
;
407 struct { int sub
, str
; } fw
;
408 struct { int sub
, str
; } bw
;
416 int * valptr
, min
, max
;
417 Opt (const char * n
, int v
, int * vp
, int mi
, int ma
);
421 int quiet
, verbose
, print
;
422 int dominate
, maxdoms
;
427 int block
,blockimpl
,blockprd
,blockint
,blockrtc
,blockclim
,blockotfs
;
428 int blockreward
,blockboost
;
429 int simprd
, simpinc
, simprtc
;
430 int probe
,probeprd
,probeint
,probertc
,probereward
,probeboost
;
432 int inverse
,inveager
,mtfall
,mtfrev
;
433 int bumpuip
,bumpsort
,bumprev
,bumpbulk
,bumpturbo
;
434 int glue
, slim
, sticky
;
435 int elim
,elimgain
,elimin
,elimprd
,elimint
,elimrtc
,elimclim
;
436 int elimreward
,elimboost
,elimasym
,elimasymint
,elimasymreward
;
437 int subst
, ands
, xors
, ites
;
438 int fwmaxlen
,bwmaxlen
,reslim
,blkmaxlen
;
440 int restart
, restartint
, luby
, restartinner
, restartouter
;
441 int rebias
, rebiasint
;
442 int minlimit
, maxlimit
;
444 int liminitmode
;//0=constant,1=relative
445 int liminitmax
, liminitconst
, liminitpercent
;
446 int limincmode
;//0=constant,1=relative
447 int liminconst1
, liminconst2
;
450 int shrink
,shrinkfactor
;
452 int random
, spread
, seed
;
454 enum MinMode
{ NONE
=0, LOCAL
=1, RECUR
=2, STRONG
=3, STRONGER
=4 };
455 int minimize
, maxdepth
, strength
;
458 const char * output
;//for 'print'
461 Opts () : fixed (false) { }
462 bool set (const char *, int);
463 bool set (const char *, const char *);
464 void add (Mem
&, const char * name
, int, int *, int, int);
465 void printoptions (FILE *, const char *prfx
) const;
468 struct SCC
{ unsigned idx
, min
: 31; bool done
: 1; };
473 RNG () : state (0) { }
475 bool oneoutof (unsigned);
476 void init (unsigned seed
) { state
= seed
; }
482 Occ (int b
, Cls
* c
) : blit (b
), cls (c
) { }
483 bool operator == (const Occ
& o
) const
484 { return cls
? o
.cls
== cls
: o
.blit
== blit
; }
492 typedef Stack
<Cls
*> Orgs
;
493 typedef Stack
<Cls
*> Fwds
;
499 int * jwhs
, * repr
, * iirfs
;
503 unsigned * bwsigs
, * fwsigs
;
504 Rnk
* rnks
, * prbs
, * elms
, * blks
;
505 struct { Heap
<Rnk
,Hotter
> decide
, probe
, elim
, block
; } schedule
;
506 int maxvar
, size
, queue
, queue2
, level
, jlevel
, uip
, open
, resolved
;
507 Stack
<int> trail
, lits
, units
, levels
, saved
, elits
, plits
, check
;
510 Stack
<Cls
*> trash
, gate
, strnd
;
511 Cls
* conflict
, empty
, dummy
;
512 Anchor
<Cls
> original
, binary
, fresh
, learned
[Cls::MAXGLUE
+1];
513 int hinc
, simprd
, agility
, spread
, posgate
, gatepivot
, gatelen
, typecount
;
516 GateStats
* gatestats
;
517 bool terminal
, iterating
, blkmode
, extending
;
518 bool resotfs
, reslimhit
, simplified
, needrescore
;
519 bool measure
, elimode
, bkdmode
, puremode
, asymode
;
528 Rnk
* prb (const Rnk
*);
529 Rnk
* rnk (const Var
*);
530 Var
* var (const Rnk
*);
532 int & iirf (Var
*, int);
534 Val
fixed (int lit
) const;
543 void rszbwsigs (int newsize
);
544 void rsziirfs (int newsize
);
550 void delclauses (Anchor
<Cls
> &);
551 Anchor
<Cls
> & anchor (Cls
*);
553 void initprfx (const char *);
562 void initlimit (int);
563 void initsearch (int);
565 long long clauses () const;
566 int recyclelimit () const;
567 bool recycling () const;
568 bool reducing () const;
569 bool eliminating () const;
570 bool blocking () const;
571 bool simplifying () const;
572 bool restarting () const;
573 bool rebiasing () const;
574 bool probing () const;
575 bool enlarging () const;
576 bool exhausted () const;
578 int remvars () const;
580 void marklits (Cls
*);
583 void unmarklits (Cls
*);
587 void bwoccs (bool & learned
);
588 Cls
* clause (bool learned
, unsigned glue
);
590 int redundant (Cls
*);
591 void recycle (Cls
*);
595 unsigned gluelits ();
596 bool clt (int, int) const;
597 void connect (Cls
*);
598 void connect (Anchor
<Cls
>&, bool orgonly
= false);
599 void disconnect (Cls
*);
601 void collect (Cls
*);
602 int bwstr (unsigned sig
, Cls
*);
603 int fwstr (unsigned sig
, Cls
*);
604 void remove (int lit
, Cls
*);
605 bool fwsub (unsigned sig
, Cls
*);
606 bool bwsub (unsigned sig
, Cls
*);
608 void assume (int l
, bool inclevel
= true);
609 void imply (int l
, int reason
);
610 int dominator (int l
, Cls
* reason
, bool &);
611 void force (int l
, Cls
* reason
);
613 bool min2 (int lit
, int other
, int depth
);
614 bool minl (int lit
, Cls
*, int depth
);
615 bool strengthen (int lit
, int depth
);
616 bool inverse (int lit
);
617 bool minimize (Var
*, int depth
);
619 void report (int v
, char ch
);
620 void prop2 (int lit
);
621 void propl (int lit
);
624 bool needtoflush () const;
626 void touchpure (int lit
);
627 void touchelim (int lit
);
628 void touchblkd (int lit
);
629 void touch (int lit
);
633 void bump (Var
*, int add
);
641 void merge (int, int, int & merged
);
644 void checkvarstats ();
646 bool resolve (int l
, int pivot
, int k
, bool tryonly
);
647 bool resolve (int l
, int pivot
, Cls
*, bool tryonly
);
648 bool resolve (Cls
*, int pivot
, Cls
*, bool tryonly
);
649 bool andgate (int lit
);
650 Cls
* find (int a
, int b
, int c
);
651 int itegate (int lit
, int cond
, int t
);
652 bool itegate (int lit
);
653 bool xorgate (int lit
);
654 bool hasgate (int idx
);
655 bool trelim (int idx
);
658 void block (Cls
*, int lit
);
659 void block (int lit
);
671 void strcls (Cls
*c
);
672 void gc (Anchor
<Cls
> &, const char*);
681 void undo (int newlevel
, bool save
= false);
685 void checkeliminated ();
691 bool satisfied (const Cls
*);
692 bool satisfied (Anchor
<Cls
> &);
696 void dbgprint (const char *, Cls
*);
697 void dbgprint (const char *, Anchor
<Cls
> &);
699 void dbgprintgate ();
705 Solver () : initialized (false) { }
707 void set (void * e
, Mem::NewFun n
, Mem::DeleteFun d
, Mem::ResizeFun r
) {
708 mem
.set (e
, n
, d
, r
);
710 void setprfx (const char* newprfx
) { delprfx (); initprfx (newprfx
); }
711 bool set (const char * option
, int arg
) { return opts
.set (option
, arg
); }
712 bool set (const char * o
, const char * a
) { return opts
.set (o
, a
); }
713 void set (FILE * file
) { out
= file
; initerm (); }
715 void init (int initial_maxvar
= 0);
718 void add (int lit
) { if (lit
) lits
.push (mem
, lit
); else import (); }
719 int next () { int res
= maxvar
+ 1; resize (res
); return res
; }
720 int solve (int decision_limit
= INT_MAX
);
721 int val (int l
) { return vals
[find (l
)]; }
722 double seconds () { return stats
.seconds (); }
727 int getMaxVar () const { return maxvar
; }