source: vis_dev/vis-2.3/src/sat/satImplication.c @ 97

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

vis2.3
File size: 22.1 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [satImplication.c]
4
5  PackageName [sat]
6
7  Synopsis    [Routines for BCP.]
8
9  Author      [HoonSang Jin]
10
11  Copyright [ This file was created at the University of Colorado at
12  Boulder.  The University of Colorado at Boulder makes no warranty
13  about the suitability of this software for any purpose.  It is
14  presented on an AS IS basis.]
15
16
17******************************************************************************/
18
19#include "satInt.h"
20#include "baig.h"
21
22static char rcsid[] UNUSED = "$Id: satImplication.c,v 1.10 2009/04/11 18:26:37 fabio Exp $";
23
24/*---------------------------------------------------------------------------*/
25/* Constant declarations                                                     */
26/*---------------------------------------------------------------------------*/
27
28/**AutomaticStart*************************************************************/
29
30/*---------------------------------------------------------------------------*/
31/* Static function prototypes                                                */
32/*---------------------------------------------------------------------------*/
33
34
35/**AutomaticEnd***************************************************************/
36
37typedef int (*IMPLY_FN)
38    (satManager_t *cm, satLevel_t *d, long v, long left, long right);
39
40
41IMPLY_FN satImplicationFN[64]= {
42  sat_ImplyStop,                 /* 0    */
43  sat_ImplyConflict,             /* 1  */
44  sat_ImplyLeftForward,          /* 2  */
45  sat_ImplyLeftForward,          /* 3  */
46  sat_ImplyStop,                 /* 4  */
47  sat_ImplyConflict,             /* 5  */
48  sat_ImplyLeftForward,          /* 6  */
49  sat_ImplyLeftForward,          /* 7  */
50  sat_ImplySplit,                /* 8  */
51  sat_ImplyConflict,             /* 9  */
52  sat_ImplyLeftForward,          /* 10  */
53  sat_ImplyLeftForward,          /* 11  */
54  sat_ImplySplit,                /* 12  */
55  sat_ImplyConflict,             /* 13  */
56  sat_ImplyLeftForward,          /* 14  */
57  sat_ImplyLeftForward,          /* 15  */
58  sat_ImplyStop,                 /* 16  */
59  sat_ImplyConflict,             /* 17  */
60  sat_ImplyRightForward,         /* 18  */
61  sat_ImplyRightForward,         /* 19  */
62  sat_ImplyConflict,             /* 20  */
63  sat_ImplyStop,                 /* 21  */
64  sat_ImplyForwardOne,           /* 22  */
65  sat_ImplyForwardOne,           /* 23  */
66  sat_ImplyPropRight,            /* 24  */
67  sat_ImplyPropRightOne,         /* 25  */
68  sat_ImplyStop,                 /* 26  */
69  sat_ImplyStop,                 /* 27  */
70  sat_ImplyPropRight,            /* 28  */
71  sat_ImplyPropRightOne,         /* 29  */
72  sat_ImplyStop,                 /* 30  */
73  sat_ImplyStop,                 /* 31  */
74  sat_ImplySplit,                /* 32  */
75  sat_ImplyConflict,             /* 33  */
76  sat_ImplyRightForward,         /* 34  */
77  sat_ImplyRightForward,         /* 35  */
78  sat_ImplyPropLeft,             /* 36  */
79  sat_ImplyPropLeftOne,          /* 37  */
80  sat_ImplyStop,                 /* 38  */
81  sat_ImplyStop,                 /* 39  */
82  sat_ImplySplit,                /* 40  */
83  sat_ImplyPropLeftRight,        /* 41  */
84  sat_ImplyStop,                 /* 42  */
85  sat_ImplyStop,                 /* 43  */
86  sat_ImplySplit,                /* 44  */
87  sat_ImplyPropLeftRight,        /* 45  */
88  sat_ImplyStop,                 /* 46  */
89  sat_ImplyStop,                 /* 47  */
90  sat_ImplySplit,                /* 48  */
91  sat_ImplyConflict,             /* 49  */
92  sat_ImplyRightForward,         /* 50  */
93  sat_ImplyRightForward,         /* 51  */
94  sat_ImplyPropLeft,             /* 52  */
95  sat_ImplyPropLeftOne,          /* 53  */
96  sat_ImplyStop,                 /* 54  */
97  sat_ImplyStop,                 /* 55  */
98  sat_ImplySplit,                /* 56  */
99  sat_ImplyPropLeftRight,        /* 57  */
100  sat_ImplyStop,                 /* 58  */
101  sat_ImplyStop,                 /* 59  */
102  sat_ImplySplit,                /* 60  */
103  sat_ImplyPropLeftRight,        /* 61  */
104  sat_ImplyStop,                 /* 62  */
105  sat_ImplyStop,                 /* 63  */
106};
107
108
109
110/*---------------------------------------------------------------------------*/
111/* Definition of exported functions                                          */
112/*---------------------------------------------------------------------------*/
113
114
115/**Function********************************************************************
116
117  Synopsis    [No further implcation when this function is called.]
118
119  Description [No further implcation when this function is called.
120                      0       0       0       1
121                      |       |       |       |
122                     ---     ---     ---     ---
123                     / \     / \     / \     / \
124                    0   X   X   0   0   0   1   1
125              ]
126
127  SideEffects []
128
129  SeeAlso     []
130
131******************************************************************************/
132
133int
134sat_ImplyStop(
135        satManager_t *cm,
136        satLevel_t *d,
137        long v,
138        long left,
139        long right)
140{
141  return(0);
142}
143
144/**Function********************************************************************
145
146  Synopsis    [No further implcation when this function is called.]
147
148  Description [No further implcation when this function is called.
149               and need split on output.
150                      0
151                      |
152                     ---
153                     / \
154                    X   X
155              ]
156
157  SideEffects []
158
159  SeeAlso     []
160
161******************************************************************************/
162int
163sat_ImplySplit(
164        satManager_t *cm,
165        satLevel_t *d,
166        long v,
167        long left,
168        long right)
169{
170  return(0);
171}
172
173/**Function********************************************************************
174
175  Synopsis    [The conflict happens.]
176
177  Description [The conflict happens when
178                      0       1       1       1       1
179                      |       |       |       |       |
180                     ---     ---     ---     ---     ---
181                     / \     / \     / \     / \     / \
182                    1   1   X   0   0   X   1   0   0   1
183              ]
184
185  SideEffects []
186
187  SeeAlso     []
188
189******************************************************************************/
190int
191sat_ImplyConflict(
192        satManager_t *cm,
193        satLevel_t *d,
194        long v,
195        long left,
196        long right)
197{
198  if(left != 2)  {
199    d->conflict = SATnormalNode(v);
200  }
201  return(0);
202}
203
204
205/**Function********************************************************************
206
207  Synopsis    [A value implied to output due to left child.]
208
209  Description [A value implied to output due to left child
210                      X       X
211                      |       |
212                     ---     ---
213                     / \     / \
214                    0   1   0   X
215              ]
216
217  SideEffects []
218
219  SeeAlso     []
220
221******************************************************************************/
222int
223sat_ImplyLeftForward(
224        satManager_t *cm,
225        satLevel_t *d,
226        long v,
227        long left,
228        long right)
229{
230
231  v = SATnormalNode(v);
232  left = SATnormalNode(left);
233
234  SATvalue(v) = 0;
235  SATmakeImplied(v, d);
236  SATante(v) = left;
237
238  sat_Enqueue(cm->queue, v);
239  SATflags(v) |= InQueueMask;
240
241  SATflags(v) |= (SATflags(left) & ObjMask);
242
243  cm->each->nAigImplications++;
244  return(0);
245}
246
247/**Function********************************************************************
248
249  Synopsis    [A value implied to output due to right child.]
250
251  Description [A value implied to output due to right child
252                      X       X
253                      |       |
254                     ---     ---
255                     / \     / \
256                    1   0   X   0
257              ]
258
259  SideEffects []
260
261  SeeAlso     []
262
263******************************************************************************/
264int
265sat_ImplyRightForward(
266        satManager_t *cm,
267        satLevel_t *d,
268        long v,
269        long left,
270        long right)
271{
272  v = SATnormalNode(v);
273  right = SATnormalNode(right);
274
275  SATvalue(v) = 0;
276  SATmakeImplied(v, d);
277  SATante(v) = right;
278
279  sat_Enqueue(cm->queue, v);
280  SATflags(v) |= InQueueMask;
281
282  SATflags(v) |= (SATflags(right) & ObjMask);
283  cm->each->nAigImplications++;
284
285  return(0);
286}
287
288
289/**Function********************************************************************
290
291  Synopsis    [A value implied to output due to both child.]
292
293  Description [A value implied to output due to both child
294                      X
295                      |
296                     ---
297                     / \
298                    1   1
299              ]
300
301  SideEffects []
302
303  SeeAlso     []
304
305******************************************************************************/
306int
307sat_ImplyForwardOne(
308        satManager_t *cm,
309        satLevel_t *d,
310        long v,
311        long left,
312        long right)
313{
314  v = SATnormalNode(v);
315  left = SATnormalNode(left);
316  right = SATnormalNode(right);
317
318  SATvalue(v) = 1;
319  SATmakeImplied(v, d);
320  SATante(v) = right;
321  SATante2(v) = left;
322
323  sat_Enqueue(cm->queue, v);
324  SATflags(v) |= InQueueMask;
325
326  SATflags(v) |= (SATflags(right) & ObjMask);
327  SATflags(v) |= (SATflags(left) & ObjMask);
328  cm->each->nAigImplications++;
329
330  return(0);
331}
332
333/**Function********************************************************************
334
335  Synopsis    [A value implied to right child due to both output and left.]
336
337  Description [A value implied to right child due to both output and left
338                      0
339                      |
340                     ---
341                     / \
342                    1   X
343              ]
344
345  SideEffects []
346
347  SeeAlso     []
348
349******************************************************************************/
350int
351sat_ImplyPropRight(
352        satManager_t *cm,
353        satLevel_t *d,
354        long v,
355        long left,
356        long right)
357{
358  int isInverted;
359
360  isInverted = SATisInverted(right);
361  v = SATnormalNode(v);
362  left = SATnormalNode(left);
363  right = SATnormalNode(right);
364
365  SATmakeImplied(right, d);
366  SATvalue(right) = isInverted;
367
368  SATante(right) = left;
369  SATante2(right) = v;
370
371  sat_Enqueue(cm->queue, right);
372  SATflags(right) |= InQueueMask;
373
374  SATflags(right) |= (SATflags(left) & ObjMask);
375  SATflags(right) |= (SATflags(v) & ObjMask);
376  cm->each->nAigImplications++;
377  return(0);
378}
379
380/**Function********************************************************************
381
382  Synopsis    [A value implied to right child due to both output and left.]
383
384  Description [A value implied to right child due to both output and left
385                      1
386                      |
387                     ---
388                     / \
389                    1   X
390              ]
391
392  SideEffects []
393
394  SeeAlso     []
395
396******************************************************************************/
397int
398sat_ImplyPropRightOne(
399        satManager_t *cm,
400        satLevel_t *d,
401        long v,
402        long left,
403        long right)
404{
405  int isInverted;
406
407  isInverted = SATisInverted(right);
408  v = SATnormalNode(v);
409  left = SATnormalNode(left);
410  right = SATnormalNode(right);
411
412  SATmakeImplied(right, d);
413
414  SATante(right) = v;
415
416  SATvalue(right) = !isInverted;
417
418  sat_Enqueue(cm->queue, right);
419  SATflags(right) |= InQueueMask;
420
421  SATflags(right) |= (SATflags(v) & ObjMask);
422  cm->each->nAigImplications++;
423  return(0);
424}
425
426
427/**Function********************************************************************
428
429  Synopsis    [A value implied to left child due to both output and right.]
430
431  Description [A value implied to left child due to both output and right
432                      0
433                      |
434                     ---
435                     / \
436                    X   1
437              ]
438
439  SideEffects []
440
441  SeeAlso     []
442
443******************************************************************************/
444int
445sat_ImplyPropLeft(
446        satManager_t *cm,
447        satLevel_t *d,
448        long v,
449        long left,
450        long right)
451{
452  int isInverted;
453
454  isInverted = SATisInverted(left);
455  v = SATnormalNode(v);
456  left = SATnormalNode(left);
457  right = SATnormalNode(right);
458
459  SATmakeImplied(left, d);
460
461  SATante(left) = v;
462  SATante2(left) = right;
463
464  SATvalue(left) = isInverted;
465
466  sat_Enqueue(cm->queue, left);
467  SATflags(left) |= InQueueMask;
468
469  SATflags(left) |= (SATflags(v) & ObjMask);
470  SATflags(left) |= (SATflags(right) & ObjMask);
471  cm->each->nAigImplications++;
472  return(0);
473}
474
475
476
477/**Function********************************************************************
478
479  Synopsis    [A value implied to left child due to both output and right.]
480
481  Description [A value implied to left child due to both output and right
482                      1
483                      |
484                     ---
485                     / \
486                    X   1
487              ]
488
489  SideEffects []
490
491  SeeAlso     []
492
493******************************************************************************/
494int
495sat_ImplyPropLeftOne(
496        satManager_t *cm,
497        satLevel_t *d,
498        long v,
499        long left,
500        long right)
501{
502  int isInverted;
503
504  isInverted = SATisInverted(left);
505  v = SATnormalNode(v);
506  left = SATnormalNode(left);
507  right = SATnormalNode(right);
508
509  SATmakeImplied(left, d);
510
511  SATante(left) = v;
512
513  SATvalue(left) = !isInverted;
514
515  sat_Enqueue(cm->queue, left);
516  SATflags(left) |= InQueueMask;
517
518  SATflags(left) |= (SATflags(v) & ObjMask);
519  cm->each->nAigImplications++;
520  return(0);
521}
522
523
524
525/**Function********************************************************************
526
527  Synopsis    [A value implied to left and right child due to output.]
528
529  Description [A value implied to left and right child due to output
530                      1
531                      |
532                     ---
533                     / \
534                    X   X
535              ]
536
537  SideEffects []
538
539  SeeAlso     []
540
541******************************************************************************/
542int
543sat_ImplyPropLeftRight(
544        satManager_t *cm,
545        satLevel_t *d,
546        long v,
547        long left,
548        long right)
549{
550  int isLeftInverted;
551  int isRightInverted;
552
553  if(left == right)     return 1;
554
555  isLeftInverted = SATisInverted(left);
556  isRightInverted = SATisInverted(right);
557
558  v = SATnormalNode(v);
559  left = SATnormalNode(left);
560  right = SATnormalNode(right);
561
562  SATmakeImplied(left, d);
563  SATmakeImplied(right, d);
564
565  SATante(left) = v;
566  SATante(right) = v;
567
568  SATvalue(left) = !isLeftInverted;
569  SATvalue(right) = !isRightInverted;
570
571  sat_Enqueue(cm->queue, left);
572  SATflags(left) |= InQueueMask;
573
574  sat_Enqueue(cm->queue, right);
575  SATflags(right) |= InQueueMask;
576
577  SATflags(left) |= (SATflags(v) & ObjMask);
578  SATflags(right) |= (SATflags(v) & ObjMask);
579  cm->each->nAigImplications += 2;
580  return(0);
581}
582
583
584/**Function********************************************************************
585
586  Synopsis    [Implication based on clause.]
587
588  Description [Implication based two watched literal scheme ]
589
590  SideEffects []
591
592  SeeAlso     []
593
594******************************************************************************/
595void
596sat_ImplyCNF(
597        satManager_t *cm,
598        satLevel_t *d,
599        long v,
600        satArray_t *wl)
601{
602int size, i, j;
603long *space;
604long lit, *plit, *tplit;
605int dir;
606long nv, tv, *oplit, *wlit;
607int isInverted, value;
608int tsize, inverted;
609long cur, clit;
610satStatistics_t *stats;
611satOption_t *option;
612satQueue_t *Q;
613satVariable_t *var;
614
615  size = wl->num;
616  space = wl->space;
617  Q = cm->queue;
618  stats = cm->each;
619  option = cm->option;
620  nv = 0;
621  wlit = 0;
622
623  for(i=0; i<size; i++) {
624    plit = (long*)space[i];
625
626    if(plit == 0 || *plit == 0) {
627      size--;
628      space[i] = space[size];
629      i--;
630      continue;
631    }
632
633    lit = *plit;
634    dir = SATgetDir(lit);
635    oplit = plit;
636
637    while(1) {
638      oplit += dir;
639      if(*oplit <=0) {
640        if(dir == 1) nv =- (*oplit);
641        if(dir == SATgetDir(lit)) {
642          oplit = plit;
643          dir = -dir;
644          continue;
645        }
646
647        tv = SATgetNode(*wlit);
648        isInverted = SATisInverted(tv);
649        tv = SATnormalNode(tv);
650        value = SATvalue(tv) ^ isInverted;
651        if(value == 0) {  /** conflict happens **/
652          d->conflict = nv;
653          wl->num = size;
654          return;
655        }
656        else if(value > 1) { /** implication **/
657          SATvalue(tv) = !isInverted;
658          SATmakeImplied(tv, d);
659          SATante(tv) = nv;
660
661          if((SATflags(tv) & InQueueMask) == 0) {
662            sat_Enqueue(Q, tv);
663            SATflags(tv) |= InQueueMask;
664          }
665
666          stats->nCNFImplications++;
667
668          /** to identify the objective dependent clause for incremental
669          * SAT
670          **/
671          if(option->incTraceObjective == 1) {
672            tsize = SATnumLits(nv);
673            for(j=0, tplit=(long*)SATfirstLit(nv); j<tsize; j++, tplit++) {
674              cur = SATgetNode(*tplit);
675              cur = SATnormalNode(cur);
676              if(SATflags(cur) & ObjMask) {
677                SATflags(tv) |= ObjMask;
678                break;
679              }
680            }
681          }
682        }
683
684        break;
685      }
686
687      clit = *oplit;
688
689      tv = SATgetNode(clit);
690      inverted = SATisInverted(tv);
691      tv = SATnormalNode(tv);
692      value = SATvalue(tv) ^ inverted;
693
694      if(SATisWL(clit)) { /* found other watched literal */
695        wlit = oplit;
696        if(value == 1)  {
697          break;
698        }
699        continue;
700      }
701
702      if(value == 0)
703        continue;
704
705      SATunsetWL(plit);
706
707      size--;
708      space[i] = space[size];
709      i--;
710
711      /** move watched literal */
712      var = SATgetVariable(tv);
713      SATsetWL(oplit, dir);
714
715      inverted = !inverted;
716      if(var->wl[inverted]) {
717        sat_ArrayInsert(var->wl[inverted], (long)oplit);
718      }
719      else {
720        var->wl[inverted] = sat_ArrayAlloc(4);
721        sat_ArrayInsert(var->wl[inverted], (long)oplit);
722      }
723
724      break;
725    }
726  }
727  wl->num = size;
728}
729
730
731/**Function********************************************************************
732
733  Synopsis    [Apply implication on node. If the conflict happens then
734               return 0, otherwise return 1]
735
736  Description [Apply implication on node.
737               Since the node can be part of AIG and CNF and BDD,
738               the implications on three representation are applied]
739
740  SideEffects []
741
742  SeeAlso     []
743
744******************************************************************************/
745int
746sat_ImplyNode(
747        satManager_t *cm,
748        satLevel_t *d,
749        long v)
750{
751long *fan, cur;
752int value;
753int i, size;
754long left, right;
755satVariable_t *var;
756satArray_t *wlArray;
757
758  value = SATvalue(v) ^ 1;
759  var = SATgetVariable(v);
760  wlArray = var->wl[value];
761
762  /** implcation on CNF **/
763  if(wlArray && wlArray->size) {
764    sat_ImplyCNF(cm, d, v, wlArray);
765  }
766
767  if(d->conflict)
768    return(0);
769
770  /** implication on AIG **/
771  fan = (long *)SATfanout(v);
772  size = SATnFanout(v);
773  for(i=0; i<size; i++, fan++) {
774    cur = *fan;
775    cur = cur >> 1;
776    cur = SATnormalNode(cur);
777    left = SATleftChild(cur);
778    right = SATrightChild(cur);
779    value = SATgetValue(left, right, cur);
780
781    (satImplicationFN[value])(cm, d, cur, left, right);
782
783    if(d->conflict)
784      return(0);
785  }
786
787  left = SATleftChild(v);
788  right = SATrightChild(v);
789  value = SATgetValue(left, right, v);
790
791  (satImplicationFN[value])(cm, d, v, left, right);
792
793  if(d->conflict)
794    return(0);
795
796
797  return(1);
798}
799
800
801/**Function********************************************************************
802
803  Synopsis    [Apply implication until the implication queue is empty. ]
804
805  Description [ Apply implication until the implication queue is empty.
806               Since the node can be part of AIG and CNF and BDD,
807               the implications on three representation are applied]
808
809  SideEffects []
810
811  SeeAlso     []
812
813******************************************************************************/
814void
815sat_ImplicationMain(
816        satManager_t *cm,
817        satLevel_t *d)
818{
819satQueue_t *Q, *BDDQ;
820long v;
821
822  Q = cm->queue;
823  BDDQ = cm->BDDQueue;
824
825  while(1) {
826    v = sat_Dequeue(Q);
827    while(v && d->conflict == 0) {
828      sat_ImplyNode(cm, d, v);
829      SATflags(v) &= ResetInQueueMask;
830
831      v = sat_Dequeue(Q);
832    }
833
834    if(d->conflict)
835      break;
836
837    if(cm->option->BDDImplication) {
838      v = sat_Dequeue(Q);
839      while(v && d->conflict == 0) {
840        sat_ImplyBDD(cm, d, v);
841        SATflags(v) &= ResetInQueueMask;
842
843        v = sat_Dequeue(Q);
844      }
845    }
846
847    if(Q->size == 0 && BDDQ->size == 0)
848      break;
849  }
850
851  sat_CleanImplicationQueue(cm);
852  cm->implicatedSoFar += d->implied->num;
853}
854
855
856
857/**Function********************************************************************
858
859  Synopsis    [Clean implication queue. ]
860
861  Description [Clean implication queue. ]
862
863  SideEffects []
864
865  SeeAlso     []
866
867******************************************************************************/
868void
869sat_CleanImplicationQueue(
870        satManager_t *cm)
871{
872satQueue_t *Q;
873 int i;
874 bAigEdge_t v;
875
876  Q = cm->queue;
877
878  if(Q->size <=0)       return;
879
880  //Bing: important, can't be zero, since some var's value,which are now in
881  //implication queue will be erased. This may lead to not being able to
882  //identify conflict
883  if(cm->option->AbRf || cm->option->IP || cm->option->arosat){
884    if(Q->front <= Q->rear) {
885      for(i=Q->front; i<=Q->rear; i++) {
886        v = Q->array[i];
887        SATflags(v) &= ResetInQueueMask;
888      }
889    }
890    else {
891      for(i=Q->front; i<Q->max; i++) {
892        v = Q->array[i];
893        SATflags(v) &= ResetInQueueMask;
894      }
895      for(i=0; i<Q->rear; i++) {
896        v = Q->array[i];
897        SATflags(v) &= ResetInQueueMask;
898      }
899    }
900  }
901#if 0
902  if(Q->front <= Q->rear) {
903    for(i=Q->front; i<=Q->rear; i++) {
904      v = Q->array[i];
905      SATflags(v) &= ResetInQueueMask;
906      SATante(v) = 0;
907      SATante2(v) = 0;
908      SATvalue(v) = 2;
909    }
910  }
911  else {
912    for(i=Q->front; i<Q->max; i++) {
913      v = Q->array[i];
914      SATflags(v) &= ResetInQueueMask;
915      SATante(v) = 0;
916      SATante2(v) = 0;
917      SATvalue(v) = 2;
918    }
919    for(i=0; i<Q->rear; i++) {
920      v = Q->array[i];
921      SATflags(v) &= ResetInQueueMask;
922      SATante(v) = 0;
923      SATante2(v) = 0;
924      SATvalue(v) = 2;
925    }
926  }
927#endif
928
929  Q->size = 0;
930  Q->front = 1;
931  Q->rear = 0;
932}
933
934
935/**Function********************************************************************
936
937  Synopsis    [Add nodes in array into implication queue. ]
938
939  Description [Add nodes in array into implication queue. ]
940
941  SideEffects []
942
943  SeeAlso     []
944
945******************************************************************************/
946void
947sat_ImplyArray(
948        satManager_t *cm,
949        satLevel_t *d,
950        satArray_t *arr)
951{
952int i, size;
953long v;
954int inverted, value;
955satQueue_t *Q;
956
957  if(arr == 0)  return;
958  if(cm->status)return;
959
960  size = arr->num;
961  Q = cm->queue;
962  for(i=0; i<size; i++) {
963    v = arr->space[i];
964    inverted = SATisInverted(v);
965    v = SATnormalNode(v);
966
967    value = !inverted;
968    if(SATvalue(v) < 2) {
969      if(SATvalue(v) == value)  continue;
970      else {
971        cm->status = SAT_UNSAT;
972        d->conflict = v;
973        //Bing:
974        return;
975      }
976    }
977
978    SATvalue(v) = value;
979    SATmakeImplied(v, d);
980    //Bing:
981    cm->each->nCNFImplications++;
982    if(cm->option->coreGeneration && cm->option->IP){
983      st_insert(cm->anteTable,(char *)SATnormalNode(v),(char *)SATnormalNode(v));
984    }
985
986    if((SATflags(v) & InQueueMask) == 0) {
987      sat_Enqueue(Q, v);
988      SATflags(v) |= InQueueMask;
989    }
990  }
991}
992
993/**Function********************************************************************
994
995  Synopsis    [Apply implication on  BDD node. ]
996
997  Description [Apply implication on  BDD node. ]
998
999
1000  SideEffects []
1001
1002  SeeAlso     []
1003
1004******************************************************************************/
1005void
1006sat_ImplyBDD(
1007        satManager_t *cm,
1008        satLevel_t *d,
1009        long v)
1010{
1011    /** CONSIDER ... **/
1012}
1013
1014/**Function********************************************************************
1015
1016  Synopsis    [Build level zero hyper implication graph. ]
1017
1018  Description [Build level zero hyper implication graph. ]
1019
1020
1021  SideEffects []
1022
1023  SeeAlso     []
1024
1025******************************************************************************/
1026void
1027sat_BuildLevelZeroHyperImplicationGraph(
1028        satManager_t *cm)
1029{
1030    /** CONSIDER...  **/
1031}
Note: See TracBrowser for help on using the repository browser.