source: vis_dev/vis-2.3/src/puresat/puresatArosat.c @ 43

Last change on this file since 43 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 48.9 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [puresatArosat.c]
4
5  PackageName [puresat]
6
7  Synopsis    [Abstraction refinement for large scale invariant checking.]
8
9  Description [This file contains the functions to check invariant properties
10  by the PureSAT abstraction refinement algorithm, which is entirely based on
11  SAT solver, the input of which could be either CNF or AIG. It has several
12  parts:
13
14  * Localization-reduction base Abstraction
15  * K-induction or interpolation to prove the truth of a property
16  * Bounded Model Checking to find bugs
17  * Incremental concretization based methods to verify abstract bugs
18  * Incremental SAT solver to improve efficiency
19  * UNSAT proof based method to obtain refinement
20  * AROSAT to bring in only necessary latches into unsat proofs
21  * Bridge abstraction to get compact coarse refinement
22  * Refinement minization to guarrantee minimal refinements
23  * Unsat proof-based refinement minimization to eliminate multiple candidate
24    by on SAT test
25  * Refinement prediction to decrease the number of refinement iterations
26  * Dynamic switching to redistribute computional resources to improve
27    efficiency
28
29  For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05
30  paper of Li et al., "A satisfiability-based appraoch to abstraction
31  refinement in model checking", " Abstraction in symbolic model checking
32  using satisfiability as the only decision procedure", "Efficient computation
33  of small abstraction refinements", and "Efficient abstraction refinement in
34  interpolation-based unbounded model checking"]
35
36  Author      [Bing Li]
37
38  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
39  All rights reserved.
40
41  Permission is hereby granted, without written agreement and without
42  license or royalty fees, to use, copy, modify, and distribute this
43  software and its documentation for any purpose, provided that the
44  above copyright notice and the following two paragraphs appear in
45  all copies of this software.]
46
47******************************************************************************/
48
49#include "puresatInt.h"
50/*---------------------------------------------------------------------------*/
51/* Constant declarations                                                     */
52/*---------------------------------------------------------------------------*/
53
54/*---------------------------------------------------------------------------*/
55/* Type declarations                                                         */
56/*---------------------------------------------------------------------------*/
57
58
59/*---------------------------------------------------------------------------*/
60/* Structure declarations                                                    */
61/*---------------------------------------------------------------------------*/
62
63
64/*---------------------------------------------------------------------------*/
65/* Variable declarations                                                     */
66/*---------------------------------------------------------------------------*/
67
68/*---------------------------------------------------------------------------*/
69/* Macro declarations                                                        */
70/*---------------------------------------------------------------------------*/
71
72/**AutomaticStart*************************************************************/
73
74/*---------------------------------------------------------------------------*/
75/* Static function prototypes                                                */
76/*---------------------------------------------------------------------------*/
77
78
79/**Function********************************************************************
80
81  Synopsis    [comparing score for sorting]
82
83  Description []
84
85  SideEffects []
86
87  SeeAlso     []
88
89******************************************************************************/
90
91static int
92ScoreCompare(
93  const void * node1,
94  const void * node2)
95{
96int v1;
97int v2;
98int s1, s2;
99
100  v1 = *(int *)(node1);
101  v2 = *(int *)(node2);
102  s1 = *((int *)(node1) + 1);
103  s2 = *((int *)(node2) + 1);
104
105  if(s1 == s2) {
106    return(v1 > v2);
107  }
108  return(s1 < s2);
109}
110
111/**AutomaticEnd***************************************************************/
112
113/*---------------------------------------------------------------------------*/
114/* Definition of exported functions                                          */
115/*---------------------------------------------------------------------------*/
116
117
118/*---------------------------------------------------------------------------*/
119/* Definition of internal functions                                          */
120/*---------------------------------------------------------------------------*/
121
122
123typedef int (*ASIMPLY_FN)
124    (satManager_t *cm, satLevel_t *d, long v, long left, long right);
125
126
127ASIMPLY_FN ASImplicationFN[64]= {
128  AS_ImplyStop,                 /* 0    */
129  AS_ImplyConflict,             /* 1  */
130  AS_ImplyLeftForward,          /* 2  */
131  AS_ImplyLeftForward,          /* 3  */
132  AS_ImplyStop,                 /* 4  */
133  AS_ImplyConflict,             /* 5  */
134  AS_ImplyLeftForward,          /* 6  */
135  AS_ImplyLeftForward,          /* 7  */
136  AS_ImplySplit,                /* 8  */
137  AS_ImplyConflict,             /* 9  */
138  AS_ImplyLeftForward,          /* 10  */
139  AS_ImplyLeftForward,          /* 11  */
140  AS_ImplySplit,                /* 12  */
141  AS_ImplyConflict,             /* 13  */
142  AS_ImplyLeftForward,          /* 14  */
143  AS_ImplyLeftForward,          /* 15  */
144  AS_ImplyStop,                 /* 16  */
145  AS_ImplyConflict,             /* 17  */
146  AS_ImplyRightForward,         /* 18  */
147  AS_ImplyRightForward,         /* 19  */
148  AS_ImplyConflict,             /* 20  */
149  AS_ImplyStop,                 /* 21  */
150  AS_ImplyForwardOne,           /* 22  */
151  AS_ImplyForwardOne,           /* 23  */
152  AS_ImplyPropRight,            /* 24  */
153  AS_ImplyPropRightOne,         /* 25  */
154  AS_ImplyStop,                 /* 26  */
155  AS_ImplyStop,                 /* 27  */
156  AS_ImplyPropRight,            /* 28  */
157  AS_ImplyPropRightOne,         /* 29  */
158  AS_ImplyStop,                 /* 30  */
159  AS_ImplyStop,                 /* 31  */
160  AS_ImplySplit,                /* 32  */
161  AS_ImplyConflict,             /* 33  */
162  AS_ImplyRightForward,         /* 34  */
163  AS_ImplyRightForward,         /* 35  */
164  AS_ImplyPropLeft,             /* 36  */
165  AS_ImplyPropLeftOne,          /* 37  */
166  AS_ImplyStop,                 /* 38  */
167  AS_ImplyStop,                 /* 39  */
168  AS_ImplySplit,                /* 40  */
169  AS_ImplyPropLeftRight,        /* 41  */
170  AS_ImplyStop,                 /* 42  */
171  AS_ImplyStop,                 /* 43  */
172  AS_ImplySplit,                /* 44  */
173  AS_ImplyPropLeftRight,        /* 45  */
174  AS_ImplyStop,                 /* 46  */
175  AS_ImplyStop,                 /* 47  */
176  AS_ImplySplit,                /* 48  */
177  AS_ImplyConflict,             /* 49  */
178  AS_ImplyRightForward,         /* 50  */
179  AS_ImplyRightForward,         /* 51  */
180  AS_ImplyPropLeft,             /* 52  */
181  AS_ImplyPropLeftOne,          /* 53  */
182  AS_ImplyStop,                 /* 54  */
183  AS_ImplyStop,                 /* 55  */
184  AS_ImplySplit,                /* 56  */
185  AS_ImplyPropLeftRight,        /* 57  */
186  AS_ImplyStop,                 /* 58  */
187  AS_ImplyStop,                 /* 59  */
188  AS_ImplySplit,                /* 60  */
189  AS_ImplyPropLeftRight,        /* 61  */
190  AS_ImplyStop,                 /* 62  */
191  AS_ImplyStop,                 /* 63  */
192};
193
194
195
196/*---------------------------------------------------------------------------*/
197/* Definition of exported functions                                          */
198/*---------------------------------------------------------------------------*/
199
200
201/**Function********************************************************************
202
203  Synopsis    [No further implcation when this function is called.]
204
205  Description [No further implcation when this function is called.
206                      0       0       0       1
207                      |       |       |       |
208                     ---     ---     ---     ---
209                     / \     / \     / \     / \
210                    0   X   X   0   0   0   1   1
211              ]
212
213  SideEffects []
214
215  SeeAlso     []
216
217******************************************************************************/
218
219int
220AS_ImplyStop(
221        satManager_t *cm,
222        satLevel_t *d,
223        long v,
224        long left,
225        long right)
226{
227  return(0);
228}
229
230/**Function********************************************************************
231
232  Synopsis    [No further implcation when this function is called.]
233
234  Description [No further implcation when this function is called.
235               and need split on output.
236                      0
237                      |
238                     ---
239                     / \
240                    X   X
241              ]
242
243  SideEffects []
244
245  SeeAlso     []
246
247******************************************************************************/
248int
249AS_ImplySplit(
250        satManager_t *cm,
251        satLevel_t *d,
252        long v,
253        long left,
254        long right)
255{
256  return(0);
257}
258
259/**Function********************************************************************
260
261  Synopsis    [The conflict happens.]
262
263  Description [The conflict happens when
264                      0       1       1       1       1
265                      |       |       |       |       |
266                     ---     ---     ---     ---     ---
267                     / \     / \     / \     / \     / \
268                    1   1   X   0   0   X   1   0   0   1
269              ]
270
271  SideEffects []
272
273  SeeAlso     []
274
275******************************************************************************/
276int
277AS_ImplyConflict(
278        satManager_t *cm,
279        satLevel_t *d,
280        long v,
281        long left,
282        long right)
283{
284  if(left != 2)  {
285    d->conflict = SATnormalNode(v);
286  }
287  return(0);
288}
289
290
291/**Function********************************************************************
292
293  Synopsis    [A value implied to output due to left child.]
294
295  Description [A value implied to output due to left child
296                      X       X
297                      |       |
298                     ---     ---
299                     / \     / \
300                    0   1   0   X
301              ]
302
303  SideEffects []
304
305  SeeAlso     []
306
307******************************************************************************/
308int
309AS_ImplyLeftForward(
310        satManager_t *cm,
311        satLevel_t *d,
312        long v,
313        long left,
314        long right)
315{
316  if(sat_ASImp(cm,d,v,0))
317    return(0);
318
319  v = SATnormalNode(v);
320  left = SATnormalNode(left);
321
322  SATvalue(v) = 0;
323  SATmakeImplied(v, d);
324  SATante(v) = left;
325
326  sat_Enqueue(cm->queue, v);
327  SATflags(v) |= InQueueMask;
328
329  SATflags(v) |= (SATflags(left) & ObjMask);
330
331  cm->each->nAigImplications++;
332
333  return(0);
334}
335
336/**Function********************************************************************
337
338  Synopsis    [A value implied to output due to right child.]
339
340  Description [A value implied to output due to right child
341                      X       X
342                      |       |
343                     ---     ---
344                     / \     / \
345                    1   0   X   0
346              ]
347
348  SideEffects []
349
350  SeeAlso     []
351
352******************************************************************************/
353int
354AS_ImplyRightForward(
355        satManager_t *cm,
356        satLevel_t *d,
357        long v,
358        long left,
359        long right)
360{
361
362  if(sat_ASImp(cm,d,v,0))
363    return(0);
364
365  v = SATnormalNode(v);
366  right = SATnormalNode(right);
367
368  SATvalue(v) = 0;
369  SATmakeImplied(v, d);
370  SATante(v) = right;
371
372  sat_Enqueue(cm->queue, v);
373  SATflags(v) |= InQueueMask;
374
375  SATflags(v) |= (SATflags(right) & ObjMask);
376  cm->each->nAigImplications++;
377
378  return(0);
379}
380
381
382/**Function********************************************************************
383
384  Synopsis    [A value implied to output due to both child.]
385
386  Description [A value implied to output due to both child
387                      X
388                      |
389                     ---
390                     / \
391                    1   1
392              ]
393
394  SideEffects []
395
396  SeeAlso     []
397
398******************************************************************************/
399int
400AS_ImplyForwardOne(
401        satManager_t *cm,
402        satLevel_t *d,
403        long v,
404        long left,
405        long right)
406{
407
408  if(sat_ASImp(cm,d,v,1))
409    return(0);
410
411  v = SATnormalNode(v);
412  left = SATnormalNode(left);
413  right = SATnormalNode(right);
414
415  SATvalue(v) = 1;
416  SATmakeImplied(v, d);
417  SATante(v) = right;
418  SATante2(v) = left;
419
420  sat_Enqueue(cm->queue, v);
421  SATflags(v) |= InQueueMask;
422
423  SATflags(v) |= (SATflags(right) & ObjMask);
424  SATflags(v) |= (SATflags(left) & ObjMask);
425  cm->each->nAigImplications++;
426
427  return(0);
428}
429
430/**Function********************************************************************
431
432  Synopsis    [A value implied to right child due to both output and left.]
433
434  Description [A value implied to right child due to both output and left
435                      0
436                      |
437                     ---
438                     / \
439                    1   X
440              ]
441
442  SideEffects []
443
444  SeeAlso     []
445
446******************************************************************************/
447int
448AS_ImplyPropRight(
449        satManager_t *cm,
450        satLevel_t *d,
451        long v,
452        long left,
453        long right)
454{
455  int isInverted;
456
457  isInverted = SATisInverted(right);
458
459
460  if(sat_ASImp(cm,d,right, isInverted))
461    return(0);
462
463  v = SATnormalNode(v);
464  left = SATnormalNode(left);
465  right = SATnormalNode(right);
466
467  SATmakeImplied(right, d);
468  SATvalue(right) = isInverted;
469
470  SATante(right) = left;
471  SATante2(right) = v;
472
473  sat_Enqueue(cm->queue, right);
474  SATflags(right) |= InQueueMask;
475
476  SATflags(right) |= (SATflags(left) & ObjMask);
477  SATflags(right) |= (SATflags(v) & ObjMask);
478  cm->each->nAigImplications++;
479
480  return(0);
481}
482
483/**Function********************************************************************
484
485  Synopsis    [A value implied to right child due to both output and left.]
486
487  Description [A value implied to right child due to both output and left
488                      1
489                      |
490                     ---
491                     / \
492                    1   X
493              ]
494
495  SideEffects []
496
497  SeeAlso     []
498
499******************************************************************************/
500int
501AS_ImplyPropRightOne(
502        satManager_t *cm,
503        satLevel_t *d,
504        long v,
505        long left,
506        long right)
507{
508  int isInverted;
509
510
511  if(sat_ASImp(cm,d,right,!SATisInverted(right)))
512    return(0);
513
514  isInverted = SATisInverted(right);
515  v = SATnormalNode(v);
516  left = SATnormalNode(left);
517  right = SATnormalNode(right);
518
519  SATmakeImplied(right, d);
520
521  SATante(right) = v;
522
523  SATvalue(right) = !isInverted;
524
525  sat_Enqueue(cm->queue, right);
526  SATflags(right) |= InQueueMask;
527
528  SATflags(right) |= (SATflags(v) & ObjMask);
529  cm->each->nAigImplications++;
530
531  return(0);
532}
533
534
535/**Function********************************************************************
536
537  Synopsis    [A value implied to left child due to both output and right.]
538
539  Description [A value implied to left child due to both output and right
540                      0
541                      |
542                     ---
543                     / \
544                    X   1
545              ]
546
547  SideEffects []
548
549  SeeAlso     []
550
551******************************************************************************/
552int
553AS_ImplyPropLeft(
554        satManager_t *cm,
555        satLevel_t *d,
556        long v,
557        long left,
558        long right)
559{
560  int isInverted;
561
562
563  if(sat_ASImp(cm,d,left,SATisInverted(left)))
564    return(0);
565
566  isInverted = SATisInverted(left);
567  v = SATnormalNode(v);
568  left = SATnormalNode(left);
569  right = SATnormalNode(right);
570
571  SATmakeImplied(left, d);
572
573  SATante(left) = v;
574  SATante2(left) = right;
575
576  SATvalue(left) = isInverted;
577
578  sat_Enqueue(cm->queue, left);
579  SATflags(left) |= InQueueMask;
580
581  SATflags(left) |= (SATflags(v) & ObjMask);
582  SATflags(left) |= (SATflags(right) & ObjMask);
583  cm->each->nAigImplications++;
584
585  return(0);
586}
587
588
589
590/**Function********************************************************************
591
592  Synopsis    [A value implied to left child due to both output and right.]
593
594  Description [A value implied to left child due to both output and right
595                      1
596                      |
597                     ---
598                     / \
599                    X   1
600              ]
601
602  SideEffects []
603
604  SeeAlso     []
605
606******************************************************************************/
607int
608AS_ImplyPropLeftOne(
609        satManager_t *cm,
610        satLevel_t *d,
611        long v,
612        long left,
613        long right)
614{
615  int isInverted;
616
617
618  if(sat_ASImp(cm,d,left,!SATisInverted(left)))
619    return(0);
620
621  isInverted = SATisInverted(left);
622  v = SATnormalNode(v);
623  left = SATnormalNode(left);
624  right = SATnormalNode(right);
625
626  SATmakeImplied(left, d);
627
628  SATante(left) = v;
629
630  SATvalue(left) = !isInverted;
631
632  sat_Enqueue(cm->queue, left);
633  SATflags(left) |= InQueueMask;
634
635  SATflags(left) |= (SATflags(v) & ObjMask);
636  cm->each->nAigImplications++;
637
638  return(0);
639}
640
641
642
643/**Function********************************************************************
644
645  Synopsis    [A value implied to left and right child due to output.]
646
647  Description [A value implied to left and right child due to output
648                      1
649                      |
650                     ---
651                     / \
652                    X   X
653              ]
654
655  SideEffects []
656
657  SeeAlso     []
658
659******************************************************************************/
660int
661AS_ImplyPropLeftRight(
662        satManager_t *cm,
663        satLevel_t *d,
664        long v,
665        long left,
666        long right)
667{
668  int isLeftInverted;
669  int isRightInverted;
670
671  int lImp=1,rImp=1;
672
673  if(left == right)     return 1;
674
675
676  if(sat_ASImp(cm,d,left,!SATisInverted(left)))
677    lImp = 0;
678  if(sat_ASImp(cm,d,right,!SATisInverted(right)))
679    rImp = 0;
680
681
682  isLeftInverted = SATisInverted(left);
683  isRightInverted = SATisInverted(right);
684
685  v = SATnormalNode(v);
686  left = SATnormalNode(left);
687  right = SATnormalNode(right);
688
689  if(lImp){
690    SATmakeImplied(left, d);
691    SATante(left) = v;
692    SATvalue(left) = !isLeftInverted;
693    sat_Enqueue(cm->queue, left);
694    SATflags(left) |= InQueueMask;
695    SATflags(left) |= (SATflags(v) & ObjMask);
696    cm->each->nAigImplications ++;
697  }
698
699  if(rImp){
700    SATmakeImplied(right, d);
701    SATante(right) = v;
702    SATvalue(right) = !isRightInverted;
703    sat_Enqueue(cm->queue, right);
704    SATflags(right) |= InQueueMask;
705    SATflags(right) |= (SATflags(v) & ObjMask);
706    cm->each->nAigImplications ++;
707  }
708
709  return(0);
710}
711
712/**Function********************************************************************
713
714  Synopsis    [erase previous assignments by arosat]
715
716  Description []
717
718  SideEffects []
719
720  SeeAlso     []
721
722******************************************************************************/
723
724void
725AS_Undo(
726        satManager_t *cm,
727        satLevel_t *d)
728{
729satArray_t *implied, *satisfied;
730int size, i;
731long *space, v;
732 satVariable_t *var;
733 int dfs;
734
735  implied = d->implied;
736  space = implied->space;
737  size = implied->num;
738  for(i=0; i<size; i++, space++) {
739    v = *space;
740
741    SATvalue(v) = 2;
742    SATflags(v) &= ResetNewVisitedObjInQueueMask;
743    SATante(v) = 0;
744    SATante2(v) = 0;
745    SATlevel(v) = -1;
746
747
748    if(SATflags(SATnormalNode(v))&AssignedMask){
749      SATflags(SATnormalNode(v))&=ResetAssignedMask;
750      var=SATgetVariable(v);
751      dfs = var->scores[0]/SCOREUNIT;
752      cm->assignedArray[dfs]--;
753
754#if DBG
755      assert(cm->assignedArray[dfs]>=0);
756#endif
757    }
758
759  }
760
761  cm->implicatedSoFar -= size;
762
763  if(d->satisfied) {
764    satisfied = d->implied;
765    space = satisfied->space;
766    size = satisfied->num;
767    for(i=0; i<size; i++, space++) {
768      v = *space;
769
770      SATflags(v) &= ResetBDDSatisfiedMask;
771    }
772    d->satisfied->num = 0;
773  }
774  if(d->level > 0) {
775    if((cm->decisionHead[d->level-1]).currentVarPos < cm->currentVarPos)
776      cm->currentVarPos = (cm->decisionHead[d->level-1]).currentVarPos;
777  }
778  else
779    cm->currentVarPos = d->currentVarPos;
780
781  d->implied->num = 0;
782  d->currentVarPos = 0;
783
784  d->conflict = 0;
785
786
787
788}
789
790
791/**Function********************************************************************
792
793  Synopsis    [implication for cnf]
794
795  Description []
796
797  SideEffects []
798
799  SeeAlso     []
800
801******************************************************************************/
802
803void
804AS_ImplyCNF(
805        satManager_t *cm,
806        satLevel_t *d,
807        long v,
808        satArray_t *wl)
809{
810int size, i, j;
811long *space;
812long lit, *plit, *tplit;
813int dir;
814long nv, tv, *oplit, *wlit;
815int isInverted, value;
816int tsize, inverted;
817long cur, clit;
818satStatistics_t *stats;
819satOption_t *option;
820satQueue_t *Q;
821satVariable_t *var;
822
823 long tmpv;
824
825  size = wl->num;
826  space = wl->space;
827  Q = cm->queue;
828  stats = cm->each;
829  option = cm->option;
830  nv = 0;
831  wlit = 0;
832
833  for(i=0; i<size; i++) {
834    plit = (long*)space[i];
835
836    if(plit == 0 || *plit == 0) {
837      size--;
838      space[i] = space[size];
839      i--;
840      continue;
841    }
842
843    lit = *plit;
844    dir = SATgetDir(lit);
845    oplit = plit;
846
847    while(1) {
848      oplit += dir;
849      if(*oplit <=0) {
850        if(dir == 1) nv =- (*oplit);
851        if(dir == SATgetDir(lit)) {
852          oplit = plit;
853          dir = -dir;
854          continue;
855        }
856
857        tv = SATgetNode(*wlit);
858
859        tmpv = tv;
860        isInverted = SATisInverted(tv);
861        tv = SATnormalNode(tv);
862        value = SATvalue(tv) ^ isInverted;
863        if(value == 0) {  /** conflict happens **/
864          d->conflict = nv;
865          wl->num = size;
866          return;
867        }
868        else if(value > 1) { /** implication **/
869
870          if(sat_ASImp(cm,d,tmpv,!isInverted))
871            break;
872
873          SATvalue(tv) = !isInverted;
874          SATmakeImplied(tv, d);
875          SATante(tv) = nv;
876
877          if((SATflags(tv) & InQueueMask) == 0) {
878            sat_Enqueue(Q, tv);
879            SATflags(tv) |= InQueueMask;
880          }
881
882          stats->nCNFImplications++;
883
884          /** to identify the objective dependent clause for incremental
885          * SAT
886          **/
887          if(option->incTraceObjective == 1) {
888            tsize = SATnumLits(nv);
889            for(j=0, tplit=(long*)SATfirstLit(nv); j<tsize; j++, tplit++) {
890              cur = SATgetNode(*tplit);
891              cur = SATnormalNode(cur);
892              if(SATflags(cur) & ObjMask) {
893                SATflags(tv) |= ObjMask;
894                break;
895              }
896            }
897          }
898        }
899
900        break;
901      }
902
903      clit = *oplit;
904
905      tv = SATgetNode(clit);
906      inverted = SATisInverted(tv);
907      tv = SATnormalNode(tv);
908      value = SATvalue(tv) ^ inverted;
909
910      if(SATisWL(clit)) { /* found other watched literal */
911        wlit = oplit;
912        if(value == 1)  {
913          break;
914        }
915        continue;
916      }
917
918      if(value == 0)
919        continue;
920
921      SATunsetWL(plit);
922
923      size--;
924      space[i] = space[size];
925      i--;
926
927      /** move watched literal */
928      var = SATgetVariable(tv);
929      SATsetWL(oplit, dir);
930
931      inverted = !inverted;
932      if(var->wl[inverted]) {
933        sat_ArrayInsert(var->wl[inverted], (long)oplit);
934      }
935      else {
936        var->wl[inverted] = sat_ArrayAlloc(4);
937        sat_ArrayInsert(var->wl[inverted], (long)oplit);
938      }
939
940      break;
941    }
942  }
943  wl->num = size;
944}
945
946
947/**Function********************************************************************
948
949  Synopsis    [implication for aig node and cnf ]
950
951  Description []
952
953  SideEffects []
954
955  SeeAlso     []
956
957******************************************************************************/
958
959int
960AS_ImplyNode(
961        satManager_t *cm,
962        satLevel_t *d,
963        long v)
964{
965long *fan, cur;
966int value;
967int i, size;
968long left, right;
969satVariable_t *var;
970satArray_t *wlArray;
971
972  value = SATvalue(v) ^ 1;
973  var = SATgetVariable(v);
974  wlArray = var->wl[value];
975
976  /** implcation on CNF **/
977  if(wlArray && wlArray->size) {
978    AS_ImplyCNF(cm, d, v, wlArray);
979  }
980
981  if(d->conflict)
982    return(0);
983
984  /** implication on AIG **/
985  fan = (long *)SATfanout(v);
986  size = SATnFanout(v);
987  for(i=0; i<size; i++, fan++) {
988    cur = *fan;
989    cur = cur >> 1;
990    cur = SATnormalNode(cur);
991    left = SATleftChild(cur);
992    right = SATrightChild(cur);
993    value = SATgetValue(left, right, cur);
994#if DBG
995
996    assert(SATflags(SATnormalNode(left))&CoiMask);
997    assert(SATflags(SATnormalNode(right))&CoiMask);
998#endif
999    (ASImplicationFN[value])(cm, d, cur, left, right);
1000
1001    if(d->conflict)
1002      return(0);
1003  }
1004
1005  left = SATleftChild(v);
1006  right = SATrightChild(v);
1007  value = SATgetValue(left, right, v);
1008#if DBG
1009
1010  assert(left==bAig_NULL||SATflags(SATnormalNode(left))&CoiMask);
1011  assert(right==bAig_NULL||SATflags(SATnormalNode(right))&CoiMask);
1012#endif
1013
1014
1015  (ASImplicationFN[value])(cm, d, v, left, right);
1016
1017  if(d->conflict)
1018    return(0);
1019
1020
1021  return(1);
1022}
1023
1024
1025/**Function********************************************************************
1026
1027  Synopsis    [The main procedure of implication propogation]
1028
1029  Description []
1030
1031  SideEffects []
1032
1033  SeeAlso     []
1034
1035******************************************************************************/
1036
1037void
1038AS_ImplicationMain(
1039        satManager_t *cm,
1040        satLevel_t *d)
1041{
1042satQueue_t *Q, *BDDQ;
1043long v;
1044
1045  Q = cm->queue;
1046  BDDQ = cm->BDDQueue;
1047
1048  while(1) {
1049    v = sat_Dequeue(Q);
1050    while(v && d->conflict == 0) {
1051      AS_ImplyNode(cm, d, v);
1052      SATflags(v) &= ResetInQueueMask;
1053
1054      v = sat_Dequeue(Q);
1055    }
1056
1057    if(d->conflict)
1058      break;
1059
1060    if(cm->option->BDDImplication) {
1061      v = sat_Dequeue(Q);
1062      while(v && d->conflict == 0) {
1063        sat_ImplyBDD(cm, d, v);
1064        SATflags(v) &= ResetInQueueMask;
1065
1066        v = sat_Dequeue(Q);
1067      }
1068    }
1069
1070    if(Q->size == 0 && BDDQ->size == 0)
1071      break;
1072  }
1073
1074  sat_CleanImplicationQueue(cm);
1075  cm->implicatedSoFar += d->implied->num;
1076}
1077
1078
1079/**Function********************************************************************
1080
1081  Synopsis    [Implication for assertation in one array]
1082
1083  Description []
1084
1085  SideEffects []
1086
1087  SeeAlso     []
1088
1089******************************************************************************/
1090
1091void
1092AS_ImplyArray(
1093        satManager_t *cm,
1094        satLevel_t *d,
1095        satArray_t *arr)
1096{
1097int i, size;
1098long v;
1099int inverted, value;
1100satQueue_t *Q;
1101 satVariable_t *var;
1102
1103 int dfs;
1104
1105  if(arr == 0)  return;
1106  if(cm->status)return;
1107
1108  size = arr->num;
1109  Q = cm->queue;
1110  for(i=0; i<size; i++) {
1111    v = arr->space[i];
1112    inverted = SATisInverted(v);
1113    v = SATnormalNode(v);
1114
1115    value = !inverted;
1116    if(SATvalue(v) < 2) {
1117      if(SATvalue(v) == value)  continue;
1118      else {
1119        cm->status = SAT_UNSAT;
1120        d->conflict = v;
1121
1122        return;
1123      }
1124    }
1125
1126
1127    var = SATgetVariable(v);
1128    dfs = var->scores[0]/SCOREUNIT;
1129    if(dfs==cm->LatchLevel){
1130      if(!(SATflags(SATnormalNode(v))&AssignedMask)){
1131        SATflags(SATnormalNode(v))|=AssignedMask;
1132        cm->assignedArray[dfs]++;
1133
1134#if DBG
1135        assert(cm->assignedArray[dfs]<=cm->numArray[dfs]);
1136#endif
1137        if(cm->assignedArray[dfs]==cm->numArray[dfs])
1138          sat_ASmergeLevel(cm);
1139      }
1140    }
1141
1142
1143    SATvalue(v) = value;
1144    SATmakeImplied(v, d);
1145
1146    if(cm->option->coreGeneration){
1147      st_insert(cm->anteTable,(char *)SATnormalNode(v),(char *)SATnormalNode(v));
1148    }
1149
1150    if((SATflags(v) & InQueueMask) == 0) {
1151      sat_Enqueue(Q, v);
1152      SATflags(v) |= InQueueMask;
1153    }
1154  }
1155}
1156
1157/**Function********************************************************************
1158
1159  Synopsis    [Preprocessing step for AROSAT]
1160
1161  Description []
1162
1163  SideEffects []
1164
1165  SeeAlso     []
1166
1167******************************************************************************/
1168
1169void
1170AS_PreProcessing(satManager_t *cm)
1171{
1172satLevel_t *d;
1173
1174
1175  /** create implication queue **/
1176  cm->queue = sat_CreateQueue(1024);
1177  cm->BDDQueue = sat_CreateQueue(1024);
1178  cm->unusedAigQueue = sat_CreateQueue(1024);
1179
1180  /**
1181  create variable array : one can reduce size of variable array using
1182  mapping. for fanout free internal node....
1183  **/
1184
1185  if(cm->variableArray == 0) {
1186    cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
1187    memset(cm->variableArray, 0,
1188            sizeof(satVariable_t) * (cm->initNumVariables+1));
1189  }
1190
1191  cm->auxArray = sat_ArrayAlloc(1024);
1192  cm->nonobjUnitLitArray = sat_ArrayAlloc(128);
1193  cm->objUnitLitArray = sat_ArrayAlloc(128);
1194
1195
1196
1197  if(cm->option->AbRf == 0)
1198    sat_CompactFanout(cm);
1199
1200
1201  /*assign initial layer score to variables*/
1202   sat_InitLayerScore(cm);
1203
1204  /** create decision stack **/
1205  if(cm->decisionHeadSize == 0) {
1206    cm->decisionHeadSize = 32;
1207    cm->decisionHead = ALLOC(satLevel_t, cm->decisionHeadSize);
1208    memset(cm->decisionHead, 0, sizeof(satLevel_t) * cm->decisionHeadSize);
1209  }
1210  cm->currentDecision = -1;
1211
1212  /** to avoid purify warning **/
1213  SATvalue(2) = 2;
1214  SATflags(0) = 0;
1215
1216  cm->initNodesArraySize = cm->nodesArraySize;
1217  cm->beginConflict = cm->nodesArraySize;
1218
1219  /** incremental SAT.... **/
1220  if(cm->option->incTraceObjective) {
1221    sat_RestoreForwardedClauses(cm, 0);
1222  }
1223  else if(cm->option->incAll) {
1224    sat_RestoreForwardedClauses(cm, 1);
1225  }
1226
1227  if(cm->option->incTraceObjective) {
1228    sat_MarkObjectiveFlagToArray(cm, cm->obj);
1229    sat_MarkObjectiveFlagToArray(cm, cm->objCNF);
1230  }
1231
1232
1233  /** Level 0 decision.... **/
1234  d = sat_AllocLevel(cm);
1235
1236  sat_ApplyForcedAssignmentMain(cm, d);
1237
1238  if(cm->status == SAT_UNSAT)
1239    return;
1240
1241
1242  if(cm->option->coreGeneration){
1243    cm->rm = ALLOC(RTManager_t, 1);
1244    memset(cm->rm,0,sizeof(RTManager_t));
1245  }
1246
1247
1248  AS_ImplyArray(cm, d, cm->auxObj);
1249  AS_ImplyArray(cm, d, cm->obj);
1250  AS_ImplyArray(cm,d,cm->assertArray);
1251
1252
1253  AS_ImplicationMain(cm, d);
1254  if(d->conflict) {
1255    cm->status = SAT_UNSAT;
1256  }
1257
1258  if(cm->status == 0) {
1259    if(cm->option->incDistill) {
1260      sat_IncrementalUsingDistill(cm);
1261    }
1262  }
1263
1264}
1265
1266
1267/**Function********************************************************************
1268
1269  Synopsis    [backtrack procedure for arosat]
1270
1271  Description []
1272
1273  SideEffects []
1274
1275  SeeAlso     []
1276
1277******************************************************************************/
1278
1279
1280void
1281AS_Backtrack(
1282        satManager_t *cm,
1283        int level)
1284{
1285satLevel_t *d;
1286
1287
1288  d = SATgetDecision(cm->currentDecision);
1289  while(1) {
1290    if(d->level <= level)
1291      break;
1292
1293    AS_Undo(cm, d);
1294    cm->currentDecision--;
1295    if(cm->currentDecision == -1)
1296      break;
1297    d = SATgetDecision(cm->currentDecision);
1298  }
1299  return;
1300}
1301
1302
1303/**Function********************************************************************
1304
1305  Synopsis    [procedure for updating score]
1306
1307  Description []
1308
1309  SideEffects []
1310
1311  SeeAlso     []
1312
1313******************************************************************************/
1314
1315
1316void
1317AS_UpdateScore(
1318        satManager_t *cm)
1319{
1320satArray_t *one, *tmp;
1321satArray_t *ordered;
1322satVariable_t *var;
1323int size, i;
1324long v;
1325int value;
1326
1327 int baseScore,realScore,newNum;
1328
1329  ordered = cm->orderedVariableArray;
1330
1331  one = sat_ArrayAlloc(ordered->num);
1332  tmp = sat_ArrayAlloc(ordered->num);
1333
1334  size = ordered->num;
1335  for(i=0; i<size; i++) {
1336    v = ordered->space[i];
1337
1338    if(SATvalue(v) < 2 && SATlevel(v) == 0)
1339      continue;
1340
1341    var = SATgetVariable(v);
1342
1343    baseScore =(var->scores[0]/SCOREUNIT)*SCOREUNIT;
1344    realScore = var->scores[0]%SCOREUNIT;
1345    newNum = var->litsCount[0] - var->lastLitsCount[0];
1346    var->scores[0] =  baseScore + (realScore>>1) + newNum;
1347    baseScore =(var->scores[1]/SCOREUNIT)*SCOREUNIT;
1348    realScore = var->scores[1]%SCOREUNIT;
1349    newNum = var->litsCount[1] - var->lastLitsCount[1];
1350    var->scores[1] =  baseScore + (realScore>>1) + newNum;
1351
1352    var->lastLitsCount[0] = var->litsCount[0];
1353    var->lastLitsCount[1] = var->litsCount[1];
1354
1355
1356    if((var->scores[0] + var->scores[1]) < 1) {
1357      sat_ArrayInsert(one, v);
1358    }
1359    else {
1360      value = (var->scores[0] > var->scores[1]) ? var->scores[0] : var->scores[1];
1361      sat_ArrayInsert(tmp, v);
1362      sat_ArrayInsert(tmp, value);
1363    }
1364  }
1365
1366  qsort(tmp->space, (tmp->num)>>1, sizeof(long)*2, ScoreCompare);
1367
1368  ordered->num = 0;
1369  size = tmp->num;
1370  for(i=0; i<size; i++) {
1371    v = tmp->space[i];
1372    sat_ArrayInsert(ordered, v);
1373    var = SATgetVariable(v);
1374    var->pos = (i>>1);
1375    i++;
1376  }
1377
1378  size = one->num;
1379  for(i=0; i<size; i++) {
1380    v = one->space[i];
1381    var = SATgetVariable(v);
1382    var->pos = ordered->num;
1383    sat_ArrayInsert(ordered, v);
1384  }
1385
1386  sat_ArrayFree(one);
1387  sat_ArrayFree(tmp);
1388
1389  cm->orderedVariableArray = ordered;
1390  cm->currentVarPos = 0;
1391
1392  for(i=1; i<cm->currentDecision; i++) {
1393    cm->decisionHead[i].currentVarPos = 0;
1394  }
1395
1396  if(cm->option->verbose > 3)
1397    sat_PrintScore(cm);
1398
1399}
1400
1401
1402/**Function********************************************************************
1403
1404  Synopsis    [Periodically executed operations]
1405
1406  Description []
1407
1408  SideEffects []
1409
1410  SeeAlso     []
1411
1412******************************************************************************/
1413
1414void
1415AS_PeriodicFunctions(satManager_t *cm)
1416{
1417satStatistics_t *stats;
1418satOption_t *option;
1419int nDecisions;
1420int gap;
1421
1422  stats = cm->each;
1423  option = cm->option;
1424  nDecisions = stats->nDecisions-stats->nShrinkDecisions;
1425  if(nDecisions && !(nDecisions % option->decisionAgeInterval)) {
1426    if(option->decisionAgeRestart) {
1427      gap = stats->nConflictCl-stats->nOldConflictCl;
1428      if(gap > option->decisionAgeInterval>>2)  {
1429
1430        AS_UpdateScore(cm);
1431
1432        AS_Backtrack(cm, cm->lowestBacktrackLevel);
1433        cm->currentTopConflict = cm->literals->last-1;
1434        cm->currentTopConflictCount = 0;
1435        cm->lowestBacktrackLevel = MAXINT;
1436      }
1437      stats->nOldConflictCl = stats->nConflictCl;
1438    }
1439    else {
1440
1441      AS_UpdateScore(cm);
1442    }
1443
1444  }
1445
1446  if(stats->nBacktracks > option->nextClauseDeletion) {
1447    option->nextClauseDeletion += option->clauseDeletionInterval;
1448    sat_ClauseDeletion(cm);
1449  }
1450}
1451
1452/**Function********************************************************************
1453
1454  Synopsis    [Decision procedure]
1455
1456  Description []
1457
1458  SideEffects []
1459
1460  SeeAlso     []
1461
1462******************************************************************************/
1463
1464satLevel_t *
1465AS_MakeDecision(satManager_t *cm)
1466{
1467satLevel_t *d;
1468int value;
1469long v;
1470satStatistics_t *stats;
1471
1472  d = SATgetDecision(cm->currentDecision);
1473
1474  if(cm->queue->size)
1475    return(d);
1476
1477  d = sat_AllocLevel(cm);
1478
1479  v = 0;
1480  v = sat_DecisionBasedOnBDD(cm, d);
1481
1482  if(v == 0)
1483    v = sat_DecisionBasedOnScore(cm, d);
1484
1485  if(v == 0)
1486    return(0);
1487
1488
1489  sat_ASDec(cm,d,v);
1490
1491  stats = cm->each;
1492
1493  stats->nDecisions++;
1494
1495  value = !(SATisInverted(v));
1496  v = SATnormalNode(v);
1497  d->decisionNode = v;
1498
1499
1500    if((SATgetVariable(v)->RecVal)!=0){
1501      if(SATgetVariable(v)->RecVal==-1)
1502        value=0;
1503      else{
1504#if DBG
1505        assert(SATgetVariable(v)->RecVal==1);
1506#endif
1507        value=1;
1508      }
1509
1510    }
1511
1512
1513  SATvalue(v) = value;
1514
1515  SATmakeImplied(v, d);
1516#if DBG
1517
1518  assert(SATflags(v)&CoiMask);
1519#endif
1520
1521  sat_Enqueue(cm->queue, v);
1522  SATflags(v) |= InQueueMask;
1523
1524  return(d);
1525}
1526
1527/**Function********************************************************************
1528
1529  Synopsis    [Find UIP for generating conflict clauses]
1530
1531  Description []
1532
1533  SideEffects []
1534
1535  SeeAlso     []
1536
1537******************************************************************************/
1538
1539void
1540AS_FindUIP(
1541        satManager_t *cm,
1542        satArray_t *clauseArray,
1543        satLevel_t *d,
1544        int *objectFlag,
1545        int *bLevel,
1546        long *fdaLit)
1547{
1548long conflicting;
1549int nMarked, value;
1550int first, i,j;
1551long *space, v,left,right,inverted,result,*tmp;
1552satArray_t *implied;
1553satOption_t *option;
1554RTnode_t  tmprt;
1555int size = 0;
1556long *lp, *tmpIP,ante,ante2,node;
1557 RTManager_t * rm = cm->rm;
1558
1559  conflicting = d->conflict;
1560  nMarked = 0;
1561  option = cm->option;
1562  if(option->incTraceObjective) *objectFlag = 0;
1563  else                          *objectFlag = ObjMask;
1564
1565  (*objectFlag) |= (SATflags(conflicting) & ObjMask);
1566
1567  /* find seed from conflicting clause to find unique implication point.
1568   * */
1569  clauseArray->num = 0;
1570  sat_MarkNodeInConflict(
1571          cm, d, &nMarked, objectFlag, bLevel, clauseArray);
1572
1573  /* Traverse implication graph backward */
1574  first = 1;
1575  implied = d->implied;
1576  space = implied->space+implied->num-1;
1577
1578
1579  if(cm->option->coreGeneration){
1580    /*if last conflict is CNF*/
1581    if(SATflags(conflicting)&IsCNFMask){
1582      /*is conflict CNF*/
1583      if(SATflags(conflicting)&IsConflictMask){
1584         if(!st_lookup(cm->RTreeTable,(char*)conflicting,&tmprt)){
1585            fprintf(vis_stderr,"RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
1586            exit(0);
1587          }
1588          else{
1589            rm->root = tmprt;
1590          }
1591      }
1592      /*CNF but not conflict*/
1593      else{
1594        rm->root = RTCreateNode(rm);
1595        RT_oriClsIdx(rm->root) = conflicting;
1596        size = SATnumLits(conflicting);
1597        RT_fSize(rm->root) = size;
1598      }
1599    }
1600    /*if last conflict is AIG*/
1601    else{
1602      rm->root = RTCreateNode(rm);
1603      node = SATnormalNode(conflicting);
1604      left = SATleftChild(node);
1605      right = SATrightChild(node);
1606      result = PureSat_IdentifyConflict(cm,left,right,conflicting);
1607      inverted = SATisInverted(left);
1608      left = SATnormalNode(left);
1609      left = inverted ? SATnot(left) : left;
1610
1611      inverted = SATisInverted(right);
1612      right = SATnormalNode(right);
1613      right = inverted ? SATnot(right) : right;
1614
1615      j = node;
1616
1617      if(result == 1){
1618        tmp = ALLOC(long,3);
1619        tmp[0] = left;
1620        tmp[1] = SATnot(j);
1621        size = 2;
1622      }
1623      else if(result == 2){
1624        tmp = ALLOC(long,3);
1625        tmp[0] = right;
1626        tmp[1] = SATnot(j);
1627        size = 2;
1628      }
1629      else if(result == 3){
1630        tmp = ALLOC(long,4);
1631        tmp[0] = SATnot(left);
1632        tmp[1] = SATnot(right);
1633        tmp[2] = j;
1634        size = 3;
1635      }
1636      else{
1637        fprintf(vis_stderr,"wrong returned result value, exit\n");
1638        exit(0);
1639      }
1640
1641      lp = tmp;
1642      sat_BuildRT(cm,rm->root, lp, tmpIP,size,1);
1643      FREE(tmp);
1644    }
1645  }
1646
1647
1648  for(i=implied->num-1; i>=0; i--, space--) {
1649    v = *space;
1650    if(SATflags(v) & VisitedMask) {
1651      SATflags(v) &= ResetVisitedMask;
1652      --nMarked;
1653
1654      if(nMarked == 0 && (!first || i==0))  {
1655        value = SATvalue(v);
1656        *fdaLit = v^(!value);
1657        sat_ArrayInsert(clauseArray, *fdaLit);
1658        break;
1659      }
1660
1661
1662
1663      if(cm->option->coreGeneration){
1664        ante = SATante(v);
1665        if(ante==0){
1666          if(!(st_lookup(cm->anteTable, (char *)SATnormalNode(v),&ante))){
1667            fprintf(vis_stderr,"ante = 0 and is not in anteTable %ld\n",v);
1668            exit(0);
1669          }
1670        }
1671
1672        /*build non-leaf node*/
1673        tmprt = RTCreateNode(rm);
1674        RT_pivot(tmprt) = SATnormalNode(v);
1675        RT_right(tmprt) = rm->root;
1676        rm->root = tmprt;
1677
1678        if((SATflags(ante)&IsConflictMask)&&(SATflags(ante)&IsCNFMask)){
1679          if(!st_lookup(cm->RTreeTable,(char*)ante,&tmprt)){
1680            fprintf(vis_stderr,"RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
1681            exit(0);
1682          }
1683          else{
1684            RT_left(rm->root) = tmprt;
1685          }
1686        }
1687        else{ /* if not conflict CNF*/
1688          /*left */
1689          tmprt = RTCreateNode(rm);
1690          RT_left(rm->root) = tmprt;
1691          /*left is AIG*/
1692          if(!(SATflags(ante) & IsCNFMask)){
1693            /*generate formula for left*/
1694            tmp = ALLOC(long,3);
1695            value = SATvalue(v);
1696            node = SATnormalNode(v);
1697            node = value==1?node:SATnot(node);
1698            tmp[0] = node;
1699
1700            size = 1;
1701            if(ante != SATnormalNode(v)){
1702              value = SATvalue(ante);
1703              node = SATnormalNode(ante);
1704              node = value==1?SATnot(node):node;
1705              tmp[1] = node;
1706              size++;
1707              ante2 = SATante2(v);
1708              if(ante2){
1709                value = SATvalue(ante2);
1710                node = SATnormalNode(ante2);
1711                node = value==1?SATnot(node):node;
1712                tmp[2] = node;
1713                size++;
1714              }
1715            }
1716            /*generate p1 and p2*/
1717            lp = tmp;
1718            sat_BuildRT(cm,tmprt,lp,tmpIP,size,1);
1719            FREE(tmp);
1720          }
1721          /* left is CNF*/
1722          else{
1723            RT_oriClsIdx(tmprt) = ante;
1724            //generate p1 and p2 for left
1725            lp = (long*)SATfirstLit(ante);
1726            size = SATnumLits(ante);
1727            RT_fSize(tmprt) = size;
1728          }
1729        } /*else{  if not conflict CNF*/
1730
1731      }/*if(cm->option->coreGeneration){*/
1732
1733
1734      sat_MarkNodeInImpliedNode(
1735              cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
1736      /*Bing:Important for EffIP*/
1737      first = 0;
1738    }
1739    /* first = 0;*/
1740  }
1741
1742
1743  /* Minimize conflict clause */
1744  if(option->minimizeConflictClause)
1745    sat_MinimizeConflictClause(cm, clauseArray);
1746  else
1747    sat_ResetFlagForClauseArray(cm, clauseArray);
1748
1749  return;
1750}
1751
1752
1753/**Function********************************************************************
1754
1755  Synopsis    [Conflict analysis procedure]
1756
1757  Description []
1758
1759  SideEffects []
1760
1761  SeeAlso     []
1762
1763******************************************************************************/
1764
1765int
1766AS_ConflictAnalysis(
1767        satManager_t *cm,
1768        satLevel_t *d)
1769{
1770satStatistics_t *stats;
1771satOption_t *option;
1772satArray_t *clauseArray;
1773int objectFlag;
1774int bLevel;
1775long fdaLit, learned, conflicting;
1776int inverted;
1777RTManager_t * rm = cm->rm;
1778
1779
1780  conflicting = d->conflict;
1781
1782  if(d->level == 0) {
1783      /** Bing : UNSAT core generation */
1784    if(cm->option->coreGeneration)
1785      sat_ConflictAnalysisForCoreGen(cm, d);
1786    cm->currentDecision--;
1787    return (-1);
1788  }
1789
1790  stats = cm->each;
1791  option = cm->option;
1792
1793
1794  stats->nBacktracks++;
1795
1796  clauseArray = cm->auxArray;
1797
1798  bLevel = 0;
1799  fdaLit = -1;
1800  clauseArray->num = 0;
1801
1802  /*  Find Unique Implication Point */
1803  AS_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
1804  stats->nNonchonologicalBacktracks += (d->level - bLevel);
1805
1806
1807  if(clauseArray->num == 0) {
1808    sat_PrintImplicationGraph(cm, d);
1809    sat_PrintNode(cm, conflicting);
1810  }
1811
1812  /* If we could find UIP then it is critical error...
1813  * at lease the decision node has to be detected as UIP.
1814  */
1815  if(fdaLit == -1) {
1816    fprintf(vis_stdout, "%s ERROR : Illegal unit literal\n", cm->comment);
1817    fflush(vis_stdout);
1818    sat_PrintNode(cm, conflicting);
1819    sat_PrintImplicationGraph(cm, d);
1820    sat_PrintDotForConflict(cm, d, conflicting, 0);
1821    exit(0);
1822  }
1823
1824  if(bLevel && cm->lowestBacktrackLevel > bLevel)
1825    cm->lowestBacktrackLevel = bLevel;
1826
1827
1828  inverted = SATisInverted(fdaLit);
1829  fdaLit = SATnormalNode(fdaLit);
1830
1831  if(option->verbose > 2) {
1832    if(option->verbose > 4)
1833      sat_PrintNode(cm, conflicting);
1834    fprintf(vis_stdout, "conflict at %3d on %6ld  bLevel %d UnitLit ",
1835            d->level, conflicting, bLevel);
1836    sat_PrintNodeAlone(cm, fdaLit);
1837    fprintf(vis_stdout, "\n");
1838  }
1839
1840  d->conflict = 0;
1841
1842  /* unit literal conflict clause */
1843  if(clauseArray->num == 1) {
1844    learned = sat_AddUnitConflictClause(cm, clauseArray, objectFlag);
1845
1846    stats->nUnitConflictCl++;
1847    cm->currentTopConflict = cm->literals->last-1;
1848    cm->currentTopConflictCount = 0;
1849
1850    AS_Backtrack(cm, 0);
1851
1852    d = SATgetDecision(cm->currentDecision);
1853    cm->implicatedSoFar -= d->implied->num;
1854    SATante(fdaLit) = 0;
1855
1856
1857    if(!(SATflags(SATnormalNode(fdaLit))&AssignedMask)){
1858      satVariable_t *var = SATgetVariable(fdaLit);
1859      int dfs = var->scores[0]/SCOREUNIT;
1860#if DBG
1861      assert(dfs==cm->LatchLevel);
1862#endif
1863      SATflags(SATnormalNode(fdaLit))|=AssignedMask;
1864      cm->assignedArray[dfs]++;
1865      if(cm->assignedArray[dfs]==cm->numArray[dfs])
1866        sat_ASmergeLevel(cm);
1867    }
1868
1869
1870    SATvalue(fdaLit) = inverted;
1871    SATmakeImplied(fdaLit, d);
1872
1873    if((SATflags(fdaLit) & InQueueMask)  == 0) {
1874      sat_Enqueue(cm->queue, fdaLit);
1875      SATflags(fdaLit) |= InQueueMask;
1876    }
1877
1878    clauseArray->num = 0;
1879
1880    if(option->incTraceObjective && objectFlag == 0)
1881      sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(fdaLit));
1882
1883    if(option->incDistill && objectFlag)
1884      sat_ArrayInsert(cm->objUnitLitArray, SATnot(fdaLit));
1885
1886    if(objectFlag)
1887      SATflags(fdaLit) |= ObjMask;
1888
1889    /* Bing: UNSAT core generation */
1890    if(cm->option->coreGeneration){
1891
1892      st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
1893      st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
1894      RT_oriClsIdx(rm->root) = learned;
1895    }
1896
1897    return(bLevel);
1898  }
1899
1900  /* add conflict learned clause */
1901  learned = sat_AddConflictClause(cm, clauseArray, objectFlag);
1902
1903  cm->currentTopConflict = cm->literals->last-1;
1904  cm->currentTopConflictCount = 0;
1905
1906   /* Bing: UNSAT core generation */
1907  if(cm->option->coreGeneration){
1908   st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
1909   RT_oriClsIdx(rm->root) = learned;
1910  }
1911
1912  if(option->verbose > 2) {
1913    sat_PrintNode(cm, learned);
1914    fflush(vis_stdout);
1915  }
1916
1917
1918  /* apply Deepest Variable Hike decision heuristic */
1919  if(option->decisionHeuristic & DVH_DECISION)
1920   sat_UpdateDVH(cm, d, clauseArray, bLevel, fdaLit);
1921
1922
1923  /* Backtrack and failure driven assertion */
1924  AS_Backtrack(cm, bLevel);
1925
1926  d = SATgetDecision(bLevel);
1927  cm->implicatedSoFar -= d->implied->num;
1928
1929
1930    if(!(SATflags(SATnormalNode(fdaLit))&AssignedMask)){
1931      satVariable_t *var = SATgetVariable(fdaLit);
1932      int dfs = var->scores[0]/SCOREUNIT;
1933#if DBG
1934      assert(dfs==cm->LatchLevel);
1935#endif
1936      SATflags(SATnormalNode(fdaLit))|=AssignedMask;
1937      cm->assignedArray[dfs]++;
1938      if(cm->assignedArray[dfs]==cm->numArray[dfs])
1939        sat_ASmergeLevel(cm);
1940    }
1941
1942
1943  SATante(fdaLit) = learned;
1944  SATvalue(fdaLit) = inverted;
1945  SATmakeImplied(fdaLit, d);
1946
1947  if((SATflags(fdaLit) & InQueueMask)  == 0) {
1948    sat_Enqueue(cm->queue, fdaLit);
1949    SATflags(fdaLit) |= InQueueMask;
1950  }
1951
1952  clauseArray->num = 0;
1953  if(objectFlag)
1954    SATflags(fdaLit) |= ObjMask;
1955
1956  return(bLevel);
1957}
1958
1959
1960/**Function********************************************************************
1961
1962  Synopsis    [Main solving procedure]
1963
1964  Description []
1965
1966  SideEffects []
1967
1968  SeeAlso     []
1969
1970******************************************************************************/
1971
1972void
1973AS_Solve(satManager_t *cm)
1974{
1975satLevel_t *d;
1976satOption_t *option;
1977satVariable_t *var;
1978int level;
1979
1980  d = SATgetDecision(0);
1981  cm->implicatedSoFar = d->implied->num;
1982  cm->currentTopConflict = 0;
1983
1984  option = cm->option;
1985  if(option->BDDMonolithic) {
1986    sat_TryToBuildMonolithicBDD(cm);
1987  }
1988
1989  if(cm->status == SAT_UNSAT) {
1990    AS_Undo(cm, SATgetDecision(0));
1991    return;
1992  }
1993
1994  while(1) {
1995    AS_PeriodicFunctions(cm);
1996
1997    if(cm->currentDecision == 0)
1998      sat_BuildLevelZeroHyperImplicationGraph(cm);
1999
2000    d = AS_MakeDecision(cm);
2001
2002    if(d == 0)  {
2003      cm->status = SAT_SAT;
2004      return;
2005    }
2006
2007    while(1) {
2008      AS_ImplicationMain(cm, d);
2009
2010      if(d->conflict == 0)      {
2011        if(cm->option->verbose > 2) {
2012          var = SATgetVariable(d->decisionNode);
2013          fprintf(vis_stdout, "decision at %3d on %6ld <- %ld score(%d %d) %d %ld implied %.3f %%\n",
2014            d->level, d->decisionNode, SATvalue(d->decisionNode),
2015            var->scores[0], var->scores[1],
2016            cm->each->nDecisions, d->implied->num,
2017            (double)cm->implicatedSoFar/(double)cm->initNumVariables * 100);
2018          fflush(vis_stdout);
2019        }
2020
2021        break;
2022      }
2023        if(cm->option->verbose > 2) {
2024          var = SATgetVariable(d->decisionNode);
2025          fprintf(vis_stdout, "decision at %3d on %6ld <- %ld score(%d %d) %d %ld implied  %.3f %% Conflict\n",
2026            d->level, d->decisionNode, SATvalue(d->decisionNode),
2027            var->scores[0], var->scores[1],
2028            cm->each->nDecisions, d->implied->num,
2029            (double)cm->implicatedSoFar/(double)cm->initNumVariables * 100);
2030          fflush(vis_stdout);
2031        }
2032
2033      level = AS_ConflictAnalysis(cm, d);
2034
2035      if(cm->currentDecision == -1) {
2036        if(cm->option->incDistill) {
2037          sat_BuildTrieForDistill(cm);
2038        }
2039        AS_Undo(cm, SATgetDecision(0));
2040        cm->status = SAT_UNSAT;
2041        return;
2042      }
2043
2044      d = SATgetDecision(cm->currentDecision);
2045    }
2046
2047  }
2048}
2049
2050
2051/**Function********************************************************************
2052
2053  Synopsis    [The main procedure of AROSAT solver]
2054
2055  Description []
2056
2057  SideEffects []
2058
2059  SeeAlso     []
2060
2061******************************************************************************/
2062
2063void AS_Main(satManager_t *cm)
2064{
2065long btime, etime;
2066
2067  btime = util_cpu_time();
2068  AS_PreProcessing(cm);
2069
2070  if(cm->status == 0)
2071    AS_Solve(cm);
2072
2073  /** Bing: UNSAT core generation **/
2074  if(cm->option->coreGeneration && cm->status == SAT_UNSAT){
2075
2076    sat_GenerateCore_All(cm);
2077  }
2078
2079  sat_PostProcessing(cm);
2080
2081  etime = util_cpu_time();
2082  cm->each->satTime = (double)(etime - btime) / 1000.0 ;
2083
2084}
2085
2086
2087/**Function********************************************************************
2088
2089  Synopsis    [Create one layer for AROSAT]
2090
2091  Description []
2092
2093  SideEffects []
2094
2095  SeeAlso     []
2096
2097******************************************************************************/
2098
2099
2100void PureSatCreateOneLayer(Ntk_Network_t *network,
2101                           PureSat_Manager_t *pm,
2102                           satManager_t *cm,
2103                           array_t * latchArray,
2104                           int layer)
2105{
2106  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
2107  st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
2108                                                         MVFAIG_NETWORK_APPL_KEY);
2109  MvfAig_Function_t *mvfAig;
2110  bAigTimeFrame_t * tf = manager->timeframeWOI;
2111  mAigMvar_t lmVar;
2112  mAigBvar_t bVar;
2113  array_t *bVarList,*mVarList;
2114  int i,j,k,lmAigId,index,index1;
2115  char * name;
2116  Ntk_Node_t * latch;
2117  bAigEdge_t node,v, *li, *bli;
2118  st_table *table = st_init_table(st_numcmp,st_numhash);
2119
2120  bVarList = mAigReadBinVarList(manager);
2121  mVarList = mAigReadMulVarList(manager);
2122
2123  arrayForEachItem(char*,latchArray,i,name){
2124
2125    latch = Ntk_NetworkFindNodeByName(network,name);
2126    st_lookup(node2MvfAigTable,latch,&mvfAig);
2127    for(j=0;j<mvfAig->num;j++){
2128      int retVal;
2129      v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
2130      if(v==bAig_Zero||v==bAig_One)
2131        continue;
2132      retVal = st_lookup(tf->li2index,(char *)v,&index);
2133      assert(retVal);
2134      for(k=1;k<=pm->Length;k++){
2135        li = tf->latchInputs[k];
2136        if(li[index]==bAig_Zero||li[index]==bAig_One)
2137          continue;
2138        node = bAig_NonInvertedEdge(li[index]);
2139        st_insert(table,(char*)node,(char*)(long)layer);
2140
2141      }
2142    }
2143
2144    lmAigId = Ntk_NodeReadMAigId(latch);
2145    lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
2146    for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
2147      int retVal;
2148      bVar = array_fetch(mAigBvar_t,bVarList,index1);
2149      if(bVar.node==bAig_Zero||bVar.node==bAig_One)
2150        continue;
2151      retVal = st_lookup(tf->bli2index,(char *)bVar.node,&index);
2152      assert(retVal);
2153      for(k=1;k<=pm->Length;k++){
2154        bli = tf->blatchInputs[k];
2155        if(bli[index]==bAig_Zero||bli[index]==bAig_One)
2156          continue;
2157        node = bAig_NonInvertedEdge(bli[index]);
2158        st_insert(table,(char*)node,(char*)(long)layer);
2159
2160      }
2161    }
2162  }
2163
2164  st_insert(cm->layerTable,table,(char*)(long)layer);
2165
2166}
2167
2168
2169
2170/**Function********************************************************************
2171
2172  Synopsis    [Create all the layers]
2173
2174  Description []
2175
2176  SideEffects []
2177
2178  SeeAlso     []
2179
2180******************************************************************************/
2181
2182
2183void PureSatCreateLayer(Ntk_Network_t *network,
2184                        PureSat_Manager_t *pm,
2185                        satManager_t *cm,
2186                        array_t *absModel,
2187                        array_t *sufArray)
2188{
2189  int layer;
2190  char* name;
2191  int i,j,threshold;
2192  array_t *tmpArray;
2193
2194  if(sufArray->num<4)
2195    layer = 1;
2196  else if(sufArray->num<6)
2197    layer = 2;
2198  else if(sufArray->num<10)
2199    layer = 3;
2200  else if(sufArray->num<20)
2201    layer = 5;
2202  else if(sufArray->num<50)
2203    layer = 8;
2204  else
2205    layer = 10;
2206
2207  threshold = sufArray->num/layer;
2208  layer = array_n(sufArray)/threshold;
2209  layer = sufArray->num%threshold?layer+1:layer;
2210
2211  cm->LatchLevel = layer;
2212  cm->OriLevel = layer;
2213  cm->layerTable = st_init_table(st_ptrcmp,st_ptrhash);
2214
2215  layer = layer+1;
2216  for(i=0;i<array_n(sufArray);i=i+threshold){
2217    if(i==0)
2218      tmpArray = array_dup(absModel);
2219    else
2220      tmpArray = array_alloc(char*,0);
2221    layer = layer-1;
2222    for(j=0;j<threshold;j++){
2223      if(i+j>=array_n(sufArray))
2224        break;
2225      name = array_fetch(char*,sufArray,i+j);
2226      array_insert_last(char*,tmpArray,name);
2227
2228    }
2229    PureSatCreateOneLayer(network,pm,cm,tmpArray,layer);
2230    array_free(tmpArray);
2231  }
2232  assert(layer==1);
2233  cm->assignedArray = ALLOC(int,cm->LatchLevel+1);
2234  cm->numArray = ALLOC(int,cm->LatchLevel+1);
2235
2236}
Note: See TracBrowser for help on using the repository browser.