source: vis_dev/vis-2.3/src/sat/satUtil.c @ 101

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

vis2.3
File size: 70.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [satUtil.c]
4
5  PackageName [sat]
6
7  Synopsis    [Routines for various utility function.]
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
21static char rcsid[] UNUSED = "$Id: satUtil.c,v 1.37 2009/04/11 18:26:37 fabio Exp $";
22
23/*---------------------------------------------------------------------------*/
24/* Constant declarations                                                     */
25/*---------------------------------------------------------------------------*/
26
27/**AutomaticStart*************************************************************/
28
29/*---------------------------------------------------------------------------*/
30/* Static function prototypes                                                */
31/*---------------------------------------------------------------------------*/
32
33static int NodeIndexCompare(const void *x, const void *y);
34
35/**AutomaticEnd***************************************************************/
36
37
38/*---------------------------------------------------------------------------*/
39/* Definition of exported functions                                          */
40/*---------------------------------------------------------------------------*/
41
42
43/**Function********************************************************************
44
45  Synopsis    [ Add conflict clause into clause database]
46
47  Description [ Add conflict clause into clause database]
48
49  SideEffects []
50
51  SeeAlso     []
52
53******************************************************************************/
54long
55sat_AddConflictClause(
56        satManager_t *cm,
57        satArray_t *clauseArray,
58        int objectFlag)
59{
60satStatistics_t *stats;
61satLiteralDB_t *literals;
62satVariable_t *var;
63long v, c;
64int inverted;
65long *last;
66long *space;
67int i, size;
68int maxLevel, maxIndex;
69int value, level;
70int otherWLIndex;
71
72  literals = cm->literals;
73
74  while(literals->last + clauseArray->num + 2 >= literals->end) {
75    if(!sat_EnlargeLiteralDB(cm)) {
76      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
77              cm->comment);
78      exit(0);
79    }
80  }
81
82  c = 0;
83  if(cm->unusedAigQueue)
84    c = sat_Dequeue(cm->unusedAigQueue);
85  if(c == 0)
86    c = sat_CreateNode(cm, 2, 2);
87
88
89  last = literals->last;
90  *(last) = (-c);
91  last++;
92
93  /**
94  SATfirstLit(c) = (int)last;
95  **/
96  (cm->nodesArray[c+satFirstLit]) = (long)last;
97  SATnumLits(c) = clauseArray->num;
98  SATflags(c) |= IsCNFMask;
99  SATsetInUse(c);
100  SATnumConflict(c) = 0;
101
102  size = clauseArray->num;
103  space = clauseArray->space;
104  for(i=0; i<size; i++, space++) {
105    v = *space;
106    inverted = !SATisInverted(v);
107    v = SATnormalNode(v);
108
109    *(last) = ((v^inverted) << 2);
110    last++;
111
112    var = SATgetVariable(v);
113
114    if(inverted){
115      (var->litsCount[0])++;
116      (var->conflictLits[0])++;
117    }
118    else        {
119      (var->litsCount[1])++;
120      (var->conflictLits[1])++;
121    }
122  }
123  *(last) = (-c);
124  last++;
125
126  literals->last = last;
127
128  maxLevel = -1;
129  maxIndex = -1;
130  otherWLIndex = -1;
131  space = clauseArray->space;
132  for(i=0; i<size; i++, space++) {
133    v = *space;
134    inverted = SATisInverted(v);
135    v = SATnormalNode(v);
136    value = SATvalue(v);
137    if(value == 2) {
138      sat_AddWL(cm, c, i, 1);
139      otherWLIndex = i;
140      break;
141    }
142    else {
143      level = SATlevel(v);
144      if(level > maxLevel) {
145        maxLevel = level;
146        maxIndex = i;
147      }
148    }
149  }
150  if(i >= size) {
151    sat_AddWL(cm, c, maxIndex, 1);
152    otherWLIndex = maxIndex;
153  }
154
155  maxLevel = -1;
156  maxIndex = -1;
157  space = clauseArray->space+size-1;
158  for(i=size-1; i>=0; i--, space--) {
159    v = *space;
160    inverted = SATisInverted(v);
161    v = SATnormalNode(v);
162    value = SATvalue(v);
163    if(i != otherWLIndex) {
164      if(value == 2) {
165        sat_AddWL(cm, c, i, -1);
166        break;
167      }
168      else {
169        level = SATlevel(v);
170        if(level > maxLevel) {
171          maxLevel = level;
172          maxIndex = i;
173        }
174      }
175    }
176  }
177  if(i < 0)
178    sat_AddWL(cm, c, maxIndex, -1);
179
180
181  SATflags(c) |= IsConflictMask;
182
183  stats = cm->each;
184  stats->nConflictCl++;
185  stats->nConflictLit += clauseArray->num;
186  if(objectFlag) {
187    stats->nObjConflictCl++;
188    stats->nObjConflictLit += clauseArray->num;
189    SATflags(c) |= ObjMask;
190  }
191  else {
192    stats->nNonobjConflictCl++;
193    stats->nNonobjConflictLit += clauseArray->num;
194    SATflags(c) |= NonobjMask;
195  }
196
197
198  return(c);
199}
200
201/**Function********************************************************************
202
203  Synopsis    [ Add conflict clause into clause database without updating score]
204
205  Description [ Add conflict clause into clause database without updating score]
206
207  SideEffects []
208
209  SeeAlso     []
210
211******************************************************************************/
212long
213sat_AddConflictClauseNoScoreUpdate(
214        satManager_t *cm,
215        satArray_t *clauseArray,
216        int objectFlag)
217{
218satStatistics_t *stats;
219satLiteralDB_t *literals;
220satVariable_t *var;
221long v, c;
222int inverted;
223long *last;
224long *space;
225int i, size;
226int maxLevel, maxIndex;
227int value, level;
228int otherWLIndex;
229
230  literals = cm->literals;
231
232  while(literals->last + clauseArray->num + 2 >= literals->end) {
233    if(!sat_EnlargeLiteralDB(cm)) {
234      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
235              cm->comment);
236      exit(0);
237    }
238  }
239
240  c = 0;
241  if(cm->unusedAigQueue)
242    c = sat_Dequeue(cm->unusedAigQueue);
243  if(c == 0)
244    c = sat_CreateNode(cm, 2, 2);
245
246
247  last = literals->last;
248  *(last) = (-c);
249  last++;
250
251  /**
252  SATfirstLit(c) = (int)last;
253  **/
254  (cm->nodesArray[c+satFirstLit]) = (long)last;
255  SATnumLits(c) = clauseArray->num;
256  SATflags(c) |= IsCNFMask;
257  SATsetInUse(c);
258  SATnumConflict(c) = 0;
259
260  size = clauseArray->num;
261  space = clauseArray->space;
262  for(i=0; i<size; i++, space++) {
263    v = *space;
264    inverted = !SATisInverted(v);
265    v = SATnormalNode(v);
266
267    *(last) = ((v^inverted) << 2);
268    last++;
269
270    var = SATgetVariable(v);
271
272    if(inverted){
273      (var->litsCount[0])++;
274      (var->conflictLits[0])++;
275    }
276    else        {
277      (var->litsCount[1])++;
278      (var->conflictLits[1])++;
279    }
280  }
281  *(last) = (-c);
282  last++;
283
284  literals->last = last;
285
286  maxLevel = -1;
287  maxIndex = -1;
288  otherWLIndex = -1;
289  space = clauseArray->space;
290  for(i=0; i<size; i++, space++) {
291    v = *space;
292    inverted = SATisInverted(v);
293    v = SATnormalNode(v);
294    value = SATvalue(v);
295    if(value == 2) {
296      sat_AddWL(cm, c, i, 1);
297      otherWLIndex = i;
298      break;
299    }
300    else {
301      level = SATlevel(v);
302      if(level > maxLevel) {
303        maxLevel = level;
304        maxIndex = i;
305      }
306    }
307  }
308  if(i >= size) {
309    sat_AddWL(cm, c, maxIndex, 1);
310    otherWLIndex = maxIndex;
311  }
312
313  maxLevel = -1;
314  maxIndex = -1;
315  space = clauseArray->space+size-1;
316  for(i=size-1; i>=0; i--, space--) {
317    v = *space;
318    inverted = SATisInverted(v);
319    v = SATnormalNode(v);
320    value = SATvalue(v);
321    if(i != otherWLIndex) {
322      if(value == 2) {
323        sat_AddWL(cm, c, i, -1);
324        break;
325      }
326      else {
327        level = SATlevel(v);
328        if(level > maxLevel) {
329          maxLevel = level;
330          maxIndex = i;
331        }
332      }
333    }
334  }
335  if(i < 0)
336    sat_AddWL(cm, c, maxIndex, -1);
337
338
339  SATflags(c) |= IsConflictMask;
340
341  stats = cm->each;
342  stats->nConflictCl++;
343  stats->nConflictLit += clauseArray->num;
344  if(objectFlag) {
345    stats->nObjConflictCl++;
346    stats->nObjConflictLit += clauseArray->num;
347    SATflags(c) |= ObjMask;
348  }
349  else {
350    stats->nNonobjConflictCl++;
351    stats->nNonobjConflictLit += clauseArray->num;
352    SATflags(c) |= NonobjMask;
353  }
354
355
356  return(c);
357}
358/**Function********************************************************************
359
360  Synopsis    [ Add unit conflict clause into clause database]
361
362  Description [ Add unit conflict clause into clause database]
363
364  SideEffects []
365
366  SeeAlso     []
367
368******************************************************************************/
369long
370sat_AddUnitConflictClause(
371        satManager_t *cm,
372        satArray_t *clauseArray,
373        int objectFlag)
374{
375satLiteralDB_t *literals;
376satStatistics_t *stats;
377long c, v;
378int inverted;
379long *last, *space;
380int i, size;
381
382  literals = cm->literals;
383
384  while(literals->last + clauseArray->num + 2 >= literals->end) {
385    if(!sat_EnlargeLiteralDB(cm)) {
386      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
387              cm->comment);
388      exit(0);
389    }
390  }
391
392  c = 0;
393  if(cm->unusedAigQueue)
394    c = sat_Dequeue(cm->unusedAigQueue);
395  if(c == 0)
396    c = sat_CreateNode(cm, 2, 2);
397
398
399  last = literals->last;
400  *(last) = (-c);
401  last++;
402
403  /**
404  SATfirstLit(c) = (int)last;
405  **/
406  (cm->nodesArray[c+satFirstLit]) = (long)last;
407  SATnumLits(c) = clauseArray->num;
408  SATflags(c) |= IsCNFMask;
409  SATsetInUse(c);
410  SATnumConflict(c) = 0;
411
412  size = clauseArray->num;
413  space = clauseArray->space;
414  for(i=0; i<size; i++, space++) {
415    v = *space;
416    inverted = !SATisInverted(v);
417    v = SATnormalNode(v);
418
419    *(last) = ((v^inverted) << 2);
420    last++;
421  }
422  *(last) = (-c);
423  last++;
424
425  literals->last = last;
426
427  SATflags(c) |= IsConflictMask;
428  stats = cm->each;
429  stats->nConflictCl++;
430  stats->nConflictLit += clauseArray->num;
431  if(objectFlag) {
432    stats->nObjConflictCl++;
433    stats->nObjConflictLit += clauseArray->num;
434    SATflags(c) |= ObjMask;
435  }
436  else {
437    stats->nNonobjConflictCl++;
438    stats->nNonobjConflictLit += clauseArray->num;
439    SATflags(c) |= NonobjMask;
440  }
441
442  return(c);
443}
444/**Function********************************************************************
445
446  Synopsis    [ Add unit blocking clause into clause database]
447
448  Description [ Add unit blocking clause into clause database]
449
450  SideEffects []
451
452  SeeAlso     []
453
454******************************************************************************/
455long
456sat_AddUnitBlockingClause(
457        satManager_t *cm,
458        satArray_t *clauseArray)
459{
460satLiteralDB_t *literals;
461satStatistics_t *stats;
462long c, v;
463int inverted;
464long *last, *space;
465int i, size;
466
467  literals = cm->literals;
468  stats = cm->each;
469
470  while(literals->last + clauseArray->num + 2 >= literals->end) {
471    if(!sat_EnlargeLiteralDB(cm)) {
472      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
473              cm->comment);
474      exit(0);
475    }
476  }
477
478  c = 0;
479  if(cm->unusedAigQueue)
480    c = sat_Dequeue(cm->unusedAigQueue);
481  if(c == 0)
482    c = sat_CreateNode(cm, 2, 2);
483
484
485  last = literals->last;
486  *(last) = (-c);
487  last++;
488
489  /**
490  SATfirstLit(c) = (int)last;
491  **/
492  (cm->nodesArray[c+satFirstLit]) = (long)last;
493  SATnumLits(c) = clauseArray->num;
494  SATflags(c) |= IsCNFMask;
495  SATsetInUse(c);
496  SATnumConflict(c) = 0;
497
498  size = clauseArray->num;
499  space = clauseArray->space;
500  for(i=0; i<size; i++, space++) {
501    v = *space;
502    inverted = !SATisInverted(v);
503    v = SATnormalNode(v);
504
505    *(last) = ((v^inverted) << 2);
506    last++;
507  }
508  *(last) = (-c);
509  last++;
510
511  literals->last = last;
512
513  SATflags(c) |= IsBlockingMask;
514
515  stats = cm->each;
516  stats->nBlockingCl++;
517  stats->nBlockingLit += clauseArray->num;
518  return(c);
519}
520
521
522/**Function********************************************************************
523
524  Synopsis    [ Add unit conflict clause into clause database]
525
526  Description [ Add unit conflict clause into clause database]
527
528  SideEffects [ UNSAT Core generation]
529
530  SeeAlso     []
531
532******************************************************************************/
533long
534sat_AddUnitClause(
535        satManager_t *cm,
536        satArray_t *clauseArray)
537{
538satLiteralDB_t *literals;
539long c = 0, v;
540int inverted;
541long *last, *space;
542int i, size;
543
544  literals = cm->literals;
545
546  while(literals->last + clauseArray->num + 2 >= literals->end) {
547    if(!sat_EnlargeLiteralDB(cm)) {
548      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
549              cm->comment);
550      exit(0);
551    }
552  }
553
554
555  c = 0;
556  if(cm->unusedAigQueue)
557    c = sat_Dequeue(cm->unusedAigQueue);
558  if(c == 0)
559    c = sat_CreateNode(cm, 2, 2);
560
561
562  last = literals->last;
563  *(last) = (-c);
564  last++;
565
566  /**
567  SATfirstLit(c) = (int)last;
568  **/
569  (cm->nodesArray[c+satFirstLit]) = (long)last;
570  SATnumLits(c) = clauseArray->num;
571  SATflags(c) |= IsCNFMask;
572  SATsetInUse(c);
573  SATnumConflict(c) = 0;
574
575  size = clauseArray->num;
576  space = clauseArray->space;
577  for(i=0; i<size; i++, space++) {
578    v = *space;
579    inverted = !SATisInverted(v);
580    v = SATnormalNode(v);
581
582    *(last) = ((v^inverted) << 2);
583    last++;
584  }
585  *(last) = (-c);
586  last++;
587
588  literals->last = last;
589
590  return(c);
591}
592
593/**Function********************************************************************
594
595  Synopsis    [ Add conflict clause into clause database]
596
597  Description [ Add conflict clause into clause database]
598
599  SideEffects []
600
601  SeeAlso     []
602
603******************************************************************************/
604long
605sat_AddClauseIncremental(
606        satManager_t *cm,
607        satArray_t *clauseArray,
608        int objectFlag,
609        int fromDistill)
610{
611satLiteralDB_t *literals;
612satStatistics_t *stats;
613satVariable_t *var;
614long c, v;
615int inverted;
616long *last, *space;
617int i, size;
618int maxLevel, maxIndex;
619int value, level;
620int otherWLIndex;
621
622  literals = cm->literals;
623  stats = cm->each;
624
625  while(literals->last + clauseArray->num + 2 >= literals->end) {
626    if(!sat_EnlargeLiteralDB(cm)) {
627      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
628              cm->comment);
629      exit(0);
630    }
631  }
632
633  c = 0;
634  if(cm->unusedAigQueue)
635    c = sat_Dequeue(cm->unusedAigQueue);
636  if(c == 0)
637    c = sat_CreateNode(cm, 2, 2);
638
639  last = literals->last;
640  *(last) = (-c);
641  last++;
642
643
644  /**
645  SATfirstLit(c) = (int)last;
646  **/
647  (cm->nodesArray[c+satFirstLit]) = (long)last;
648  SATnumLits(c) = clauseArray->num;
649  SATflags(c) |= IsCNFMask;
650  SATsetInUse(c);
651  SATnumConflict(c) = 0;
652
653  size = clauseArray->num;
654  space = clauseArray->space;
655  for(i=0; i<size; i++, space++) {
656    v = *space;
657    inverted = !SATisInverted(v);
658    v = SATnormalNode(v);
659
660    *(last) = ((v^inverted) << 2);
661    last++;
662
663    var = SATgetVariable(v);
664    if(inverted){
665      if(fromDistill)
666        (var->litsCount[0])++;
667      (var->conflictLits[0])++;
668    }
669    else        {
670      if(fromDistill)
671        (var->litsCount[1])++;
672      (var->conflictLits[1])++;
673    }
674  }
675  *(last) = (-c);
676  last++;
677
678  literals->last = last;
679
680
681  /* Bing: UNSAT core generation */
682 if(clauseArray->num>1){
683  maxLevel = -1;
684  maxIndex = -1;
685  otherWLIndex = -1;
686  space = clauseArray->space;
687  for(i=0; i<size; i++, space++) {
688    v = *space;
689    inverted = SATisInverted(v);
690    v = SATnormalNode(v);
691    value = SATvalue(v);
692    if(value == 2) {
693      sat_AddWL(cm, c, i, 1);
694      otherWLIndex = i;
695      break;
696    }
697    else {
698      level = SATlevel(v);
699      if(level > maxLevel) {
700        maxLevel = level;
701        maxIndex = i;
702      }
703    }
704  }
705  if(i >= size) {
706    sat_AddWL(cm, c, maxIndex, 1);
707    otherWLIndex = maxIndex;
708  }
709
710  maxLevel = -1;
711  maxIndex = -1;
712  space = clauseArray->space+size-1;
713  for(i=size-1; i>=0; i--, space--) {
714    v = *space;
715    inverted = SATisInverted(v);
716    v = SATnormalNode(v);
717    value = SATvalue(v);
718    if(i != otherWLIndex) {
719      if(value == 2) {
720        sat_AddWL(cm, c, i, -1);
721        break;
722      }
723      else {
724        level = SATlevel(v);
725        if(level > maxLevel) {
726          maxLevel = level;
727          maxIndex = i;
728        }
729      }
730    }
731  }
732  if(i < 0)
733    sat_AddWL(cm, c, maxIndex, -1);
734 }
735
736  if(objectFlag)SATflags(c) |= ObjMask;
737  else          SATflags(c) |= NonobjMask;
738  /*SATflags(c) |= IsConflictMask;*/
739  //Bing:change??
740  if(!cm->option->coreGeneration)
741    SATflags(c) |= IsConflictMask;
742
743  if(objectFlag) {
744    stats->nInitObjConflictCl++;
745    stats->nInitObjConflictLit += clauseArray->num;
746    stats->nObjConflictCl++;
747    stats->nObjConflictLit += clauseArray->num;
748  }
749  else {
750    stats->nInitNonobjConflictCl++;
751    stats->nInitNonobjConflictLit += clauseArray->num;
752    stats->nObjConflictCl++;
753    stats->nObjConflictLit += clauseArray->num;
754  }
755  stats->nConflictCl++;
756  stats->nConflictLit += clauseArray->num;
757
758  return(c);
759}
760
761/**Function********************************************************************
762
763  Synopsis    [ Add clause into clause database]
764
765  Description [ Add clause into clause database]
766
767  SideEffects []
768
769  SeeAlso     []
770
771******************************************************************************/
772long
773sat_AddClause(
774        satManager_t *cm,
775        satArray_t *clauseArray)
776{
777satLiteralDB_t *literals;
778long c, v;
779int inverted;
780long *last, *space;
781int i, size;
782int maxLevel, maxIndex;
783int value, level;
784int otherWLIndex;
785
786  literals = cm->literals;
787
788  while(literals->last + clauseArray->num + 2 >= literals->end) {
789    if(!sat_EnlargeLiteralDB(cm)) {
790      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
791              cm->comment);
792      exit(0);
793    }
794  }
795  c = 0;
796  if(cm->unusedAigQueue)
797    c = sat_Dequeue(cm->unusedAigQueue);
798  if(c == 0)
799    c = sat_CreateNode(cm, 2, 2);
800
801  last = literals->last;
802  *(last) = (-c);
803  last++;
804
805  /**
806  SATfirstLit(c) = (int)last;
807  **/
808  (cm->nodesArray[c+satFirstLit]) = (long)last;
809  SATnumLits(c) = clauseArray->num;
810  SATflags(c) |= IsCNFMask;
811  SATsetInUse(c);
812  SATnumConflict(c) = 0;
813
814  size = clauseArray->num;
815  space = clauseArray->space;
816  for(i=0; i<size; i++, space++) {
817    v = *space;
818    inverted = !SATisInverted(v);
819    v = SATnormalNode(v);
820
821    *(last) = ((v^inverted) << 2);
822    last++;
823  }
824  *(last) = (-c);
825  last++;
826
827  literals->last = last;
828
829  maxLevel = -1;
830  maxIndex = -1;
831  otherWLIndex = -1;
832  space = clauseArray->space;
833  for(i=0; i<size; i++, space++) {
834    v = *space;
835    inverted = SATisInverted(v);
836    v = SATnormalNode(v);
837    value = SATvalue(v);
838    if(value == 2) {
839      sat_AddWL(cm, c, i, 1);
840      otherWLIndex = i;
841      break;
842    }
843    else {
844      level = SATlevel(v);
845      if(level > maxLevel) {
846        maxLevel = level;
847        maxIndex = i;
848      }
849    }
850  }
851  if(i >= size) {
852    sat_AddWL(cm, c, maxIndex, 1);
853    otherWLIndex = maxIndex;
854  }
855
856  maxLevel = -1;
857  maxIndex = -1;
858  space = clauseArray->space+size-1;
859  for(i=size-1; i>=0; i--, space--) {
860    v = *space;
861    inverted = SATisInverted(v);
862    v = SATnormalNode(v);
863    value = SATvalue(v);
864    if(i != otherWLIndex) {
865      if(value == 2) {
866        sat_AddWL(cm, c, i, -1);
867        break;
868      }
869      else {
870        level = SATlevel(v);
871        if(level > maxLevel) {
872          maxLevel = level;
873          maxIndex = i;
874        }
875      }
876    }
877  }
878  if(i < 0)
879    sat_AddWL(cm, c, maxIndex, -1);
880
881
882  return(c);
883}
884
885/**Function********************************************************************
886
887  Synopsis    [ Add clause into clause database]
888
889  Description [ Add clause into clause database]
890
891  SideEffects []
892
893  SeeAlso     []
894
895******************************************************************************/
896long
897sat_AddBlockingClause(
898        satManager_t *cm,
899        satArray_t *clauseArray)
900{
901satLiteralDB_t *literals;
902satStatistics_t *stats;
903long c, v;
904int inverted;
905long *last, *space;
906int i, size;
907int maxLevel, maxIndex;
908int value, level;
909int otherWLIndex;
910
911  literals = cm->literals;
912  stats = cm->each;
913
914  while(literals->last + clauseArray->num + 2 >= literals->end) {
915    if(!sat_EnlargeLiteralDB(cm)) {
916      fprintf(cm->stdErr, "%s ERROR : Cannot alloc memory for LiteralDB\n",
917              cm->comment);
918      exit(0);
919    }
920  }
921
922  if(clauseArray->num == 1)
923    return(sat_AddUnitBlockingClause(cm, clauseArray));
924
925  c = 0;
926  if(cm->unusedAigQueue)
927    c = sat_Dequeue(cm->unusedAigQueue);
928  if(c == 0)
929    c = sat_CreateNode(cm, 2, 2);
930
931  last = literals->last;
932  *(last) = (-c);
933  last++;
934
935  /**
936  SATfirstLit(c) = (int)last;
937  **/
938  (cm->nodesArray[c+satFirstLit]) = (long)last;
939  SATnumLits(c) = clauseArray->num;
940  SATflags(c) |= IsCNFMask;
941  SATsetInUse(c);
942  SATnumConflict(c) = 0;
943
944  size = clauseArray->num;
945  space = clauseArray->space;
946  for(i=0; i<size; i++, space++) {
947    v = *space;
948    inverted = !SATisInverted(v);
949    v = SATnormalNode(v);
950
951    *(last) = ((v^inverted) << 2);
952    last++;
953  }
954  *(last) = (-c);
955  last++;
956
957  literals->last = last;
958
959  maxLevel = -1;
960  maxIndex = -1;
961  otherWLIndex = -1;
962  space = clauseArray->space;
963  for(i=0; i<size; i++, space++) {
964    v = *space;
965    inverted = SATisInverted(v);
966    v = SATnormalNode(v);
967    value = SATvalue(v);
968    if(value == 2) {
969      sat_AddWL(cm, c, i, 1);
970      otherWLIndex = i;
971      break;
972    }
973    else {
974      level = SATlevel(v);
975      if(level > maxLevel) {
976        maxLevel = level;
977        maxIndex = i;
978      }
979    }
980  }
981  if(i >= size) {
982    sat_AddWL(cm, c, maxIndex, 1);
983    otherWLIndex = maxIndex;
984  }
985
986  maxLevel = -1;
987  maxIndex = -1;
988  space = clauseArray->space+size-1;
989  for(i=size-1; i>=0; i--, space--) {
990    v = *space;
991    inverted = SATisInverted(v);
992    v = SATnormalNode(v);
993    value = SATvalue(v);
994    if(i != otherWLIndex) {
995      if(value == 2) {
996        sat_AddWL(cm, c, i, -1);
997        break;
998      }
999      else {
1000        level = SATlevel(v);
1001        if(level > maxLevel) {
1002          maxLevel = level;
1003          maxIndex = i;
1004        }
1005      }
1006    }
1007  }
1008  if(i < 0)
1009    sat_AddWL(cm, c, maxIndex, -1);
1010
1011  SATflags(c) |= IsBlockingMask;
1012
1013  stats = cm->each;
1014  stats->nBlockingCl++;
1015  stats->nBlockingLit += clauseArray->num;
1016
1017  return(c);
1018}
1019
1020
1021/**Function********************************************************************
1022
1023  Synopsis    [ Make literal watched ]
1024
1025  Description [ Make literal watched ]
1026
1027  SideEffects []
1028
1029  SeeAlso     []
1030
1031******************************************************************************/
1032void
1033sat_AddWL(
1034        satManager_t *cm,
1035        long c,
1036        int index,
1037        int dir)
1038{
1039long *plit, v;
1040int inverted;
1041satVariable_t *var;
1042
1043  plit = (long*)SATfirstLit(c) + index;
1044  v = SATgetNode(*plit);
1045  inverted = !SATisInverted(v);
1046  v = SATnormalNode(v);
1047  var = SATgetVariable(v);
1048
1049  if(var->wl[inverted] == 0)
1050    var->wl[inverted] = sat_ArrayAlloc(4);
1051  sat_ArrayInsert(var->wl[inverted], (long)plit);
1052  SATsetWL(plit, dir);
1053}
1054
1055
1056/**Function********************************************************************
1057
1058  Synopsis    [ Allocate array ]
1059
1060  Description [ Allocate array ]
1061
1062  SideEffects []
1063
1064  SeeAlso     []
1065
1066******************************************************************************/
1067satArray_t *
1068sat_ArrayAlloc(long number)
1069{
1070satArray_t *array;
1071
1072  array = ALLOC(satArray_t, 1);
1073  if (array) {
1074    array->num = 0;
1075    array->size = number;
1076    array->space = ALLOC(long, number);
1077    if (array->space) {
1078      return array;
1079    }
1080  }
1081  //Bing: To avoid segmentation fault
1082  if(array==0 || (number>0&&array->space==0)){
1083    printf("can't alloc mem, exit\n");
1084    exit(0);
1085  }
1086  return 0;
1087}
1088
1089/**Function********************************************************************
1090
1091  Synopsis    [ Duplicate array ]
1092
1093  Description [ Duplicate array ]
1094
1095  SideEffects []
1096
1097  SeeAlso     []
1098
1099******************************************************************************/
1100satArray_t *
1101sat_ArrayDuplicate(satArray_t *old)
1102{
1103satArray_t *array;
1104
1105  array = (satArray_t *)malloc(sizeof(satArray_t));
1106  if (array) {
1107    array->num = old->num;
1108    array->size = old->num;
1109    array->space = (long *)malloc(sizeof(long) * old->num);
1110    memcpy(array->space, old->space, sizeof(long)*old->num);
1111    if (array->space) {
1112      return array;
1113    }
1114  }
1115  return 0;
1116}
1117
1118/**Function********************************************************************
1119
1120  Synopsis    [ Insert entries to array ]
1121
1122  Description [ Insert entries to array ]
1123
1124  SideEffects []
1125
1126  SeeAlso     []
1127
1128******************************************************************************/
1129void
1130sat_ArrayInsert(satArray_t *array, long datum)
1131{
1132  if(array->num < array->size) {
1133    array->space[array->num++] = datum;
1134  }
1135  else {
1136    array->size <<= 1;
1137    array->space = REALLOC(long, array->space, array->size);
1138    if(array->space == 0) {
1139      fprintf(stdout, "ERROR : Can't allocate memory in sat_ArrayInsert\n");
1140      exit(0);
1141    }
1142    array->space[array->num++] = datum;
1143  }
1144}
1145
1146/**Function********************************************************************
1147
1148  Synopsis    [ Free array ]
1149
1150  Description [ Free array ]
1151
1152  SideEffects []
1153
1154  SeeAlso     []
1155
1156******************************************************************************/
1157void
1158sat_ArrayFree(satArray_t *array)
1159{
1160  free(array->space);
1161  free(array);
1162}
1163
1164
1165/**Function********************************************************************
1166
1167  Synopsis    [ Create queue ]
1168
1169  Description [ Create queue ]
1170
1171  SideEffects []
1172
1173  SeeAlso     []
1174
1175******************************************************************************/
1176satQueue_t *
1177sat_CreateQueue( long MaxElements )
1178{
1179satQueue_t *Q;
1180
1181  Q = ALLOC(satQueue_t, 1);
1182  if( Q == NULL )
1183    fprintf(stderr, "Out of space!!!\n" );
1184
1185  Q->array = ALLOC(long, MaxElements );
1186  if( Q->array == NULL )
1187    fprintf(stderr, "Out of space!!!\n" );
1188  Q->max = MaxElements;
1189  Q->size = 0;
1190  Q->front = 1;
1191  Q->rear = 0;
1192  return Q;
1193}
1194
1195/**Function********************************************************************
1196
1197  Synopsis    [ Free queue ]
1198
1199  Description [ Free queue ]
1200
1201  SideEffects []
1202
1203  SeeAlso     []
1204
1205******************************************************************************/
1206void
1207sat_FreeQueue( satQueue_t *Q )
1208{
1209  if( Q != NULL ) {
1210    free( Q->array );
1211    free( Q );
1212  }
1213}
1214
1215
1216/**Function********************************************************************
1217
1218  Synopsis    [ Enqueue node ]
1219
1220  Description [ Enqueue node ]
1221
1222  SideEffects []
1223
1224  SeeAlso     []
1225
1226******************************************************************************/
1227void
1228sat_Enqueue(satQueue_t *Q, long v)
1229{
1230  long *arr, *oarr;
1231  long rear;
1232
1233  if(Q->size < Q->max) {
1234    Q->size++;
1235    rear = Q->rear;
1236    rear = (++(rear) == Q->max) ? 0 : rear;
1237    Q->array[rear] = v;
1238    Q->rear = rear;
1239  }
1240  else {
1241    arr = ALLOC(long, Q->size * 2 );
1242    if(arr == NULL )
1243       fprintf(stderr, "Out of space!!!\n" );
1244    oarr = Q->array;
1245    if(Q->front > Q->rear) {
1246       memcpy(&(arr[1]), &(oarr[Q->front]),
1247               sizeof(long) *(Q->max-Q->front));
1248       memcpy(&(arr[Q->size-Q->front+1]), &(oarr[0]),
1249               sizeof(long) *(Q->rear+1));
1250    }
1251    else if(Q->front < Q->rear) {
1252       memcpy(&(arr[1]), &(oarr[Q->front]), sizeof(long) *(Q->size));
1253    }
1254    free(oarr);
1255    Q->array = arr;
1256    Q->front = 1;
1257    Q->rear = Q->size;
1258    Q->max *= 2;
1259
1260    Q->size++;
1261    rear = Q->rear;
1262    rear = (++(rear) == Q->max) ? 0 : rear;
1263    Q->array[rear] = v;
1264    Q->rear = rear;
1265  }
1266}
1267
1268
1269/**Function********************************************************************
1270
1271  Synopsis    [ Dequeue ]
1272
1273  Description [ Dequeue ]
1274
1275  SideEffects []
1276
1277  SeeAlso     []
1278
1279******************************************************************************/
1280long
1281sat_Dequeue( satQueue_t * Q )
1282{
1283  long front;
1284  long v;
1285
1286  if(Q->size > 0) {
1287    Q->size--;
1288    front = Q->front;
1289    v = Q->array[front];
1290    Q->front = (++(front) == Q->max) ? 0 : front;
1291    return v;
1292  }
1293  else
1294    return(0);
1295}
1296
1297
1298/**Function********************************************************************
1299
1300  Synopsis    [ Allocate decision level ]
1301
1302  Description [ Allocate decision level ]
1303
1304  SideEffects []
1305
1306  SeeAlso     []
1307
1308******************************************************************************/
1309satLevel_t *
1310sat_AllocLevel(
1311        satManager_t *cm)
1312{
1313satStatistics_t *stats;
1314satLevel_t *d;
1315satArray_t *implied;
1316int size;
1317
1318  if(cm->decisionHeadSize == 0) {
1319    size = cm->currentDecision+2;
1320    cm->decisionHeadSize = size;
1321    cm->decisionHead = REALLOC(satLevel_t, cm->decisionHead, size);
1322    memset(cm->decisionHead, 0, sizeof(satLevel_t) * size);
1323  }
1324
1325  if(cm->currentDecision+1 >= cm->decisionHeadSize) {
1326    size = cm->decisionHeadSize;
1327    cm->decisionHeadSize <<=1;
1328    cm->decisionHead = REALLOC(satLevel_t, cm->decisionHead,
1329                               cm->decisionHeadSize);
1330    memset(cm->decisionHead+size, 0, sizeof(satLevel_t) * size);
1331  }
1332
1333  cm->currentDecision++;
1334  d = &(cm->decisionHead[cm->currentDecision]);
1335  implied = d->implied;
1336  memset(d, 0, sizeof(satLevel_t));
1337  d->implied = implied;
1338  if(d->implied == 0){
1339    d->implied = sat_ArrayAlloc(64);
1340    //Bing: avoid seg fault
1341    if(d->implied == 0){
1342      printf("out of mem, exit\n");
1343      exit(0);
1344    }
1345  }
1346
1347  d->level = cm->currentDecision;
1348  d->conflict = 0;
1349
1350  stats = cm->each;
1351  if(stats->maxDecisionLevel < d->level)
1352    stats->maxDecisionLevel = d->level;
1353
1354  return(d);
1355
1356}
1357
1358/**Function********************************************************************
1359
1360  Synopsis    [ Clean decision level when backtracking ]
1361
1362  Description [ Clean decision level when backtracking ]
1363
1364  SideEffects []
1365
1366  SeeAlso     []
1367
1368******************************************************************************/
1369void
1370sat_CleanLevel(
1371        satLevel_t *d)
1372{
1373  if(d->implied)
1374    d->implied->num = 0;
1375  if(d->satisfied)
1376    d->satisfied->num = 0;
1377  d->currentVarPos = 0;
1378}
1379
1380/**Function********************************************************************
1381
1382  Synopsis    [ Delete conflict clauses ]
1383
1384  Description [ Delete conflict clauses ]
1385
1386  SideEffects []
1387
1388  SeeAlso     []
1389
1390******************************************************************************/
1391void
1392sat_ClauseDeletion(satManager_t *cm)
1393{
1394satLiteralDB_t *literals;
1395satOption_t *option;
1396long v, *plit, nv, lit;
1397int size, n0, n1x, deleteFlag;
1398int unrelevance;
1399int inverted, i;
1400int value;
1401double ratio;
1402
1403/**
1404LATEST_ACTIVITY_DELETION
1405MAX_UNRELEVANCE_DELETION
1406SIMPLE_LATEST_DELETION
1407**/
1408
1409  option = cm->option;
1410  if(option->clauseDeletionHeuristic == 0)      return;
1411
1412  literals = cm->literals;
1413  for(v=cm->beginConflict; v<cm->nodesArraySize; v+=satNodeSize) {
1414    if(!(SATflags(v) & IsCNFMask))      continue;
1415    if(SATreadInUse(v) == 0)            continue;
1416
1417    if(option->incPreserveNonobjective && (SATflags(v) & NonobjMask))
1418      continue;
1419
1420    size = SATnumLits(v);
1421    if(size < option->minLitsLimit)     continue;
1422
1423    plit = (long*)SATfirstLit(v);
1424
1425    unrelevance = option->unrelevance;
1426    if(option->clauseDeletionHeuristic & SIMPLE_LATEST_DELETION) {
1427      ratio = (double)(plit-literals->initialSize)/
1428          (double)(literals->last-literals->initialSize);
1429      if(ratio > 0.8)   unrelevance <<= 3;
1430    }
1431    if(!(option->clauseDeletionHeuristic & MAX_UNRELEVANCE_DELETION)) {
1432      unrelevance = MAXINT;
1433    }
1434
1435    n0 = n1x = 0;
1436    deleteFlag = 0;
1437    for(i=0; i<size; i++, plit++) {
1438      lit = *plit;
1439      nv = SATgetNode(lit);
1440      inverted = SATisInverted(nv);
1441      nv = SATnormalNode(nv);
1442      value = SATvalue(nv) ^ inverted;
1443
1444      if(value == 0)    n0++;
1445      else if(value == 1) {
1446        n1x++;
1447        if(SATlevel(nv) == 0 && cm->option->coreGeneration == 0)
1448          deleteFlag = 1;
1449      }
1450      else      n1x++;
1451
1452      if(deleteFlag) {
1453        sat_DeleteClause(cm, v);
1454        sat_Enqueue(cm->unusedAigQueue, v);
1455        break;
1456      }
1457      if((size > option->maxLitsLimit) && (n1x > 1)) {
1458        sat_DeleteClause(cm, v);
1459        sat_Enqueue(cm->unusedAigQueue, v);
1460        break;
1461      }
1462      if(n1x > unrelevance) {
1463        sat_DeleteClause(cm, v);
1464        sat_Enqueue(cm->unusedAigQueue, v);
1465        break;
1466      }
1467    }
1468
1469  }
1470}
1471
1472/**Function********************************************************************
1473
1474  Synopsis    [ Delete conflict clauses ]
1475
1476  Description [ Delete conflict clauses ]
1477
1478  SideEffects []
1479
1480  SeeAlso     []
1481
1482******************************************************************************/
1483void
1484sat_DeleteClause(
1485        satManager_t *cm,
1486        long v)
1487{
1488satStatistics_t *stats;
1489int size, i;
1490long nv, *plit;
1491
1492  stats = cm->each;
1493  size = SATnumLits(v);
1494  stats->nDeletedCl++;
1495  stats->nDeletedLit += size;
1496
1497/**  SATresetInUse(v); **/
1498  SATflags(v) = 0;
1499  SATflags(v) |= IsCNFMask;
1500
1501  for(i=0, plit=(long*)SATfirstLit(v); i<size; i++, plit++) {
1502    nv = SATgetNode(*plit);
1503    *plit = 0;
1504  }
1505}
1506
1507/**Function********************************************************************
1508
1509  Synopsis    [ Compact clause database ]
1510
1511  Description [ Compact clause database ]
1512
1513  SideEffects []
1514
1515  SeeAlso     []
1516
1517******************************************************************************/
1518void
1519sat_CompactClauses(satManager_t *cm)
1520{
1521satLiteralDB_t *literals;
1522long *plit, v, lit;
1523int i, size, index;
1524int inverted;
1525satVariable_t *var;
1526
1527  literals = cm->literals;
1528  size = literals->last - literals->begin;
1529
1530  plit = literals->begin;
1531  index = literals->initialSize-literals->begin;
1532  for(i=literals->initialSize-literals->begin; i<size; i++) {
1533    if(i < 2) {
1534      plit[index] = plit[i];
1535      index++;
1536      continue;
1537    }
1538
1539    if(plit[i-1] == 0 && plit[i] < 0)   continue;
1540    else if(plit[i-1] == 0 && plit[i] == 0)     continue;
1541    else if(plit[i-1] < 0 && plit[i] == 0)      continue;
1542    else if(plit[i-1] < 0 && plit[i] < 0 && plit[i+1] == 0)     continue;
1543    else {
1544      plit[index] = plit[i];
1545      index++;
1546    }
1547  }
1548
1549  literals->last = literals->begin + index;
1550  for(v=satNodeSize; v<cm->beginConflict; v+=satNodeSize) {
1551    if(SATflags(v) & IsCNFMask) continue;
1552    var = SATgetVariable(v);
1553    if(var->wl[0]) var->wl[0]->num = 0;
1554    if(var->wl[1]) var->wl[1]->num = 0;
1555  }
1556
1557  size = literals->last - literals->begin;
1558  plit = literals->begin;
1559  for(i=0; i<size; i++) {
1560    lit = plit[i];
1561    if(lit > 0 && SATisWL(lit)) {
1562      v = SATgetNode(lit);
1563      inverted = !(SATisInverted(v));
1564      v = SATnormalNode(v);
1565      var = SATgetVariable(v);
1566      if(var->wl[inverted] == 0)
1567        var->wl[inverted] = sat_ArrayAlloc(4);
1568      sat_ArrayInsert(var->wl[inverted], (long)(&(plit[i])));
1569    }
1570
1571    if(lit <= 0) {
1572      v = -lit;
1573      /**
1574      SATfirstLit(v) = (int)(&(plit[i]) - SATnumLits(v));
1575      **/
1576      (cm->nodesArray[v+satFirstLit]) = (long)(&(plit[i]) - SATnumLits(v));
1577    }
1578  }
1579
1580  plit = literals->last - 1;
1581  cm->currentTopConflict = plit;
1582  cm->currentTopConflictCount = 0;
1583
1584}
1585
1586/**Function********************************************************************
1587
1588  Synopsis    [ Enlarge clause database ]
1589
1590  Description [ Enlarge clause database ]
1591
1592  SideEffects []
1593
1594  SeeAlso     []
1595
1596******************************************************************************/
1597int
1598sat_EnlargeLiteralDB(satManager_t *cm)
1599{
1600satLiteralDB_t *literals;
1601int nLiveConflictCl, nLiveConflictLit;
1602double ratio, growRatio;
1603double memUsage;
1604long *oldBegin, *oldEnd;
1605long newSize, oldSize;
1606int offset, index, size;
1607int i, j, nodesSize;
1608long tv;
1609int arrSize;
1610satVariable_t *var;
1611satArray_t *wl;
1612satStatistics_t *stats;
1613satOption_t *option;
1614
1615
1616  literals = cm->literals;
1617  option = cm->option;
1618  stats = cm->each;
1619
1620  size = literals->last - literals->begin;
1621  nLiveConflictCl = cm->initNumClauses + stats->nConflictCl + stats->nBlockingCl - stats->nDeletedCl;
1622  nLiveConflictLit = cm->initNumLiterals + stats->nBlockingLit +
1623                     stats->nConflictLit - stats->nDeletedLit ;
1624  ratio = (double)(nLiveConflictLit + (nLiveConflictCl << 1)) /
1625          (double)(size);
1626
1627  if(ratio < 0.8) {
1628    sat_CompactClauses(cm);
1629    return(1);
1630  }
1631
1632  memUsage = (double)sat_MemUsage(cm);
1633  growRatio = 1.0;
1634  if(memUsage < (double)option->memoryLimit/4.0)        growRatio = 2.0;
1635  else if(memUsage < (double)option->memoryLimit/2.0)   growRatio = 1.5;
1636  else if(memUsage < (double)option->memoryLimit*0.8)   growRatio = 1.2;
1637
1638  if(growRatio < 1.5) {
1639    if(ratio < 0.9) {
1640      sat_CompactClauses(cm);
1641      return(1);
1642    }
1643  }
1644
1645  oldBegin = literals->begin;
1646  oldEnd = literals->end;
1647  oldSize = literals->last - literals->begin;
1648  newSize = oldSize * (int)growRatio;
1649
1650  literals->begin = REALLOC(long, oldBegin, newSize);
1651  literals->last = literals->begin + oldSize;
1652  literals->end = literals->begin + newSize;
1653
1654  offset = literals->begin - oldBegin;
1655  nodesSize = cm->nodesArraySize;
1656  for(i=satNodeSize; i<nodesSize; i+= satNodeSize) {
1657    tv = i;
1658    if(SATflags(tv) & IsCNFMask) {
1659      if(SATreadInUse(tv))
1660        (cm->nodesArray[tv+satFirstLit]) = (long)((long*)(SATfirstLit(tv)) + offset);
1661      /**
1662        SATfirstLit(tv) = (int)((int*)(SATfirstLit(tv)) + offset);
1663        **/
1664    }
1665    else if(SATflags(tv) & IsBDDMask) {
1666      (cm->nodesArray[tv+satFirstLit]) = (long)((long*)(SATfirstLit(tv)) + offset);
1667        /**
1668      SATfirstLit(tv) = (int)((int*)(SATfirstLit(tv)) + offset);
1669      **/
1670    }
1671    else {
1672      var = SATgetVariable(tv);
1673      wl = var->wl[0];
1674      if(wl) {
1675        arrSize = wl->num;
1676        for(j=0, index=0; j<arrSize; j++) {
1677          if(wl->space[j] == 0) continue;
1678          wl->space[j] = (long)(((long*)(wl->space[j])) + offset);
1679        }
1680      }
1681      wl = var->wl[1];
1682      if(wl) {
1683        arrSize = wl->num;
1684        for(j=0, index=0; j<arrSize; j++) {
1685          if(wl->space[j] == 0) continue;
1686          wl->space[j] = (long)(((long*)(wl->space[j])) + offset);
1687        }
1688      }
1689    }
1690  }
1691  literals->initialSize = literals->initialSize + offset;
1692  cm->currentTopConflict += offset;
1693
1694  return(1);
1695}
1696
1697/**Function********************************************************************
1698
1699  Synopsis    [ Allocate clause database ]
1700
1701  Description [ Allocate clause database ]
1702
1703  SideEffects []
1704
1705  SeeAlso     []
1706
1707******************************************************************************/
1708void
1709sat_AllocLiteralsDB(satManager_t *cm)
1710{
1711satLiteralDB_t *literals;
1712int size;
1713
1714  literals = cm->literals;
1715  if(literals)  return;
1716
1717  literals = ALLOC(satLiteralDB_t, 1);
1718  cm->literals = literals;
1719
1720  size = 1024 * 1024;
1721  literals->begin = ALLOC(long, size);
1722  *(literals->begin) = 0;
1723  literals->last = literals->begin + 1;
1724  literals->end = literals->begin + size;
1725  /** CONSIDER... **/
1726  literals->initialSize = literals->last;
1727
1728}
1729
1730
1731/**Function********************************************************************
1732
1733  Synopsis    [ Free clause database ]
1734
1735  Description [ Free clause database ]
1736
1737  SideEffects []
1738
1739  SeeAlso     []
1740
1741******************************************************************************/
1742void
1743sat_FreeLiteralsDB(satLiteralDB_t *literals)
1744{
1745
1746  if(literals == 0)     return;
1747  free(literals->begin);
1748  literals->begin = 0;
1749  free(literals);
1750}
1751
1752/**Function********************************************************************
1753
1754  Synopsis    [ clean value and flag of node ]
1755
1756  Description [ clean value and flag of node ]
1757
1758  SideEffects []
1759
1760  SeeAlso     []
1761
1762******************************************************************************/
1763void
1764sat_CleanDatabase(satManager_t *cm)
1765{
1766long v, i;
1767
1768  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
1769    v = i;
1770    SATvalue(v) = 2;
1771    SATflags(v) &= PreserveMask;
1772  }
1773}
1774
1775/**Function********************************************************************
1776
1777  Synopsis    [ Compact fanout of AIG node ]
1778
1779  Description [ Compact fanout of AIG node ]
1780
1781  SideEffects []
1782
1783  SeeAlso     []
1784
1785******************************************************************************/
1786void
1787sat_CompactFanout(satManager_t *cm)
1788{
1789int bufSize, bufIndex;
1790long *buf, *fan;
1791long i, v, cur;
1792int j, size, tsize;
1793
1794  bufSize = 1024;
1795  bufIndex = 0;
1796  buf = ALLOC(long, bufSize);
1797  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
1798    v = i;
1799
1800    if(!(SATflags(v) & CoiMask))
1801      continue;
1802
1803    size = SATnFanout(v);
1804    if(size >= bufSize) {
1805      bufSize <<= 1;
1806      if(size >= bufSize)
1807        bufSize = size + 1;
1808      buf = REALLOC(long, buf, bufSize);
1809    }
1810
1811    bufIndex = 0;
1812    for(j=0, fan = SATfanout(v); j<size; j++) {
1813      cur = fan[j];
1814      cur >>= 1;
1815      cur = SATnormalNode(cur);
1816      if(!(SATflags(cur) & CoiMask))
1817        continue;
1818      buf[bufIndex++] = fan[j];
1819    }
1820
1821    if(bufIndex > 0) {
1822      tsize = bufIndex;
1823      for(j=0, fan=SATfanout(v); j<size; j++) {
1824        cur = fan[j];
1825        cur >>= 1;
1826        cur = SATnormalNode(cur);
1827        if(!(SATflags(cur) & CoiMask))  {
1828          buf[bufIndex++] = fan[j];
1829          continue;
1830        }
1831      }
1832      buf[bufIndex] = 0;
1833      memcpy(fan, buf, sizeof(long)*(size+1));
1834      SATnFanout(v) = tsize;
1835    }
1836    else {
1837      SATnFanout(v) = 0;
1838    }
1839  }
1840
1841  free(buf);
1842
1843  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
1844    v = i;
1845    if(!(SATflags(v) & CoiMask))
1846      continue;
1847    fan = SATfanout(v);
1848    size = SATnFanout(v);
1849    qsort(fan, size, sizeof(long), NodeIndexCompare);
1850  }
1851}
1852
1853
1854
1855/**Function********************************************************************
1856
1857  Synopsis    [ Restore fanout of AIG node ]
1858
1859  Description [ Restore fanout of AIG node ]
1860
1861  SideEffects []
1862
1863  SeeAlso     []
1864
1865******************************************************************************/
1866void
1867sat_RestoreFanout(satManager_t *cm)
1868{
1869long i, v;
1870
1871  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
1872    v = i;
1873    if((SATflags(v) & IsCNFMask))
1874      continue;
1875    SATnFanout(v) = sat_GetFanoutSize(cm, v);
1876  }
1877}
1878
1879/**Function********************************************************************
1880
1881  Synopsis    [ Get fanout size of AIG node ]
1882
1883  Description [ Get fanout size of AIG node ]
1884
1885  SideEffects []
1886
1887  SeeAlso     []
1888
1889******************************************************************************/
1890int
1891sat_GetFanoutSize(
1892        satManager_t *cm,
1893        long v)
1894{
1895long *fan;
1896int i;
1897
1898  fan = SATfanout(v);
1899  if(fan == 0)  return(0);
1900
1901  for(i=0; fan[i]!=0; i++);
1902  return(i);
1903}
1904
1905/**Function********************************************************************
1906
1907  Synopsis    [ Mark transitive fanin of given array of node ]
1908
1909  Description [ Mark transitive fanin of given array of node ]
1910
1911  SideEffects []
1912
1913  SeeAlso     []
1914
1915******************************************************************************/
1916void
1917sat_MarkTransitiveFaninForArray(
1918        satManager_t *cm,
1919        satArray_t *arr,
1920        unsigned int mask)
1921{
1922long v;
1923int i, size;
1924
1925  if(arr == 0)  return;
1926  size = arr->num;
1927
1928  for(i=0; i<size; i++) {
1929    v = arr->space[i];
1930    sat_MarkTransitiveFaninForNode(cm, v, mask);
1931  }
1932}
1933
1934/**Function********************************************************************
1935
1936  Synopsis    [ Mark transitive fanin of given node ]
1937
1938  Description [ Mark transitive fanin of given node ]
1939
1940  SideEffects []
1941
1942  SeeAlso     []
1943
1944******************************************************************************/
1945void
1946sat_MarkTransitiveFaninForNode(
1947        satManager_t *cm,
1948        long v,
1949        unsigned int mask)
1950{
1951  if(v == 2)    return;
1952
1953  v = SATnormalNode(v);
1954
1955  if(SATflags(v) & mask)        return;
1956
1957  SATflags(v) |= mask;
1958
1959  sat_MarkTransitiveFaninForNode(cm, SATleftChild(v), mask);
1960  sat_MarkTransitiveFaninForNode(cm, SATrightChild(v), mask);
1961}
1962
1963/**Function********************************************************************
1964
1965  Synopsis    [ Unmark transitive fanin of given array of node ]
1966
1967  Description [ Unmark transitive fanin of given array of node ]
1968
1969  SideEffects []
1970
1971  SeeAlso     []
1972
1973******************************************************************************/
1974void
1975sat_UnmarkTransitiveFaninForArray(
1976        satManager_t *cm,
1977        satArray_t *arr,
1978        unsigned int mask,
1979        unsigned int resetMask)
1980{
1981long v;
1982int i, size;
1983
1984  size = arr->num;
1985
1986  for(i=0; i<size; i++) {
1987    v = arr->space[i];
1988    sat_UnmarkTransitiveFaninForNode(cm, v, mask, resetMask);
1989  }
1990}
1991
1992/**Function********************************************************************
1993
1994  Synopsis    [ Unmark transitive fanin of given node ]
1995
1996  Description [ Unmark transitive fanin of given node ]
1997
1998  SideEffects []
1999
2000  SeeAlso     []
2001
2002******************************************************************************/
2003void
2004sat_UnmarkTransitiveFaninForNode(
2005        satManager_t *cm,
2006        long v,
2007        unsigned int mask,
2008        unsigned int resetMask)
2009{
2010  if(v == 2)    return;
2011
2012  v = SATnormalNode(v);
2013
2014  if(!(SATflags(v) & mask))     return;
2015
2016  SATflags(v) &= resetMask;
2017  sat_UnmarkTransitiveFaninForNode(cm, SATleftChild(v), mask, resetMask);
2018  sat_UnmarkTransitiveFaninForNode(cm, SATrightChild(v), mask, resetMask);
2019}
2020
2021
2022/**Function********************************************************************
2023
2024  Synopsis    [ Set COIMask ]
2025
2026  Description [ Set COIMask. The COIMask of flags of node has be set to
2027                apply implication on it ]
2028
2029  SideEffects []
2030
2031  SeeAlso     []
2032
2033******************************************************************************/
2034void
2035sat_SetConeOfInfluence(satManager_t *cm)
2036{
2037  sat_MarkTransitiveFaninForArray(cm, cm->assertion, CoiMask);
2038  sat_MarkTransitiveFaninForArray(cm, cm->auxObj, CoiMask);
2039  sat_MarkTransitiveFaninForArray(cm, cm->obj, CoiMask);
2040  //Bing:
2041  sat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);
2042}
2043
2044
2045/**Function********************************************************************
2046
2047  Synopsis    [ Allocate manager for SAT solving]
2048
2049  Description [  Allocate manager for SAT solving]
2050
2051  SideEffects []
2052
2053  SeeAlso     []
2054
2055******************************************************************************/
2056satManager_t *
2057sat_InitManager(satInterface_t *interface)
2058{
2059satManager_t *cm;
2060
2061  cm = ALLOC(satManager_t, 1);
2062  memset(cm, 0, sizeof(satManager_t));
2063
2064  if(interface) {
2065    cm->total = interface->total;
2066    cm->nonobjUnitLitArray = interface->nonobjUnitLitArray;
2067    cm->savedConflictClauses = interface->savedConflictClauses;
2068    cm->trieArray = interface->trieArray;
2069    cm->objUnitLitArray = sat_ArrayAlloc(8);
2070  }
2071  else {
2072    cm->total = sat_InitStatistics();
2073    cm->objUnitLitArray = sat_ArrayAlloc(8);
2074    cm->nonobjUnitLitArray = sat_ArrayAlloc(8);
2075  }
2076
2077  return(cm);
2078}
2079
2080/**Function********************************************************************
2081
2082  Synopsis    [ Free manager after SAT solving]
2083
2084  Description [ Free manager after SAT solving]
2085
2086  SideEffects []
2087
2088  SeeAlso     []
2089
2090******************************************************************************/
2091void
2092sat_FreeManager(satManager_t *cm)
2093{
2094satVariable_t *var;
2095satLevel_t *d;
2096int i;
2097
2098  if(cm->option)        sat_FreeOption(cm->option);
2099  if(cm->total)         sat_FreeStatistics(cm->total);
2100  if(cm->each)          sat_FreeStatistics(cm->each);
2101
2102  if(cm->literals)      sat_FreeLiteralsDB(cm->literals);
2103
2104  if(cm->decisionHead) {
2105    for(i=0; i<cm->decisionHeadSize; i++) {
2106      d = &(cm->decisionHead[i]);
2107      if(d->implied)
2108        sat_ArrayFree(d->implied);
2109      if(d->satisfied)
2110        sat_ArrayFree(d->satisfied);
2111    }
2112    free(cm->decisionHead);
2113    cm->decisionHead = 0;
2114    cm->decisionHeadSize = 0;
2115  }
2116
2117  if(cm->queue)         sat_FreeQueue(cm->queue);
2118  if(cm->BDDQueue)      sat_FreeQueue(cm->BDDQueue);
2119  if(cm->unusedAigQueue)sat_FreeQueue(cm->unusedAigQueue);
2120  cm->queue = 0;
2121  cm->BDDQueue = 0;
2122  cm->unusedAigQueue = 0;
2123
2124  if(cm->auxObj)               sat_ArrayFree(cm->auxObj);
2125  if(cm->obj)                  sat_ArrayFree(cm->obj);
2126  if(cm->unitLits)             sat_ArrayFree(cm->unitLits);
2127  if(cm->pureLits)             sat_ArrayFree(cm->pureLits);
2128  if(cm->assertion)            sat_ArrayFree(cm->assertion);
2129  if(cm->auxArray)             sat_ArrayFree(cm->auxArray);
2130  if(cm->nonobjUnitLitArray)   sat_ArrayFree(cm->nonobjUnitLitArray);
2131  if(cm->objUnitLitArray)      sat_ArrayFree(cm->objUnitLitArray);
2132  if(cm->orderedVariableArray) sat_ArrayFree(cm->orderedVariableArray);
2133  if(cm->clauseIndexInCore)    sat_ArrayFree(cm->clauseIndexInCore);
2134  cm->auxObj = 0;
2135  cm->obj = 0;
2136  cm->unitLits = 0;
2137  cm->pureLits = 0;
2138  cm->assertion = 0;
2139  cm->auxArray = 0;
2140  cm->nonobjUnitLitArray = 0;
2141  cm->objUnitLitArray = 0;
2142  cm->orderedVariableArray = 0;
2143
2144  if(cm->variableArray) {
2145    for(i=0; i<=cm->initNumVariables; i++) {
2146      var = &(cm->variableArray[i]);
2147      if(var->wl[0]) {
2148        sat_ArrayFree(var->wl[0]);
2149        var->wl[0] = 0;
2150      }
2151      if(var->wl[1]) {
2152        sat_ArrayFree(var->wl[1]);
2153        var->wl[1] = 0;
2154      }
2155    }
2156    free(cm->variableArray);
2157    cm->variableArray = 0;
2158  }
2159
2160
2161  if(cm->comment)       free(cm->comment);
2162
2163  if(cm->nodesArray)    free(cm->nodesArray);
2164  free(cm);
2165}
2166
2167/**Function********************************************************************
2168
2169  Synopsis    [ Free option after SAT solving]
2170
2171  Description [ Free option after SAT solving]
2172
2173  SideEffects []
2174
2175  SeeAlso     []
2176
2177******************************************************************************/
2178void
2179sat_FreeOption(satOption_t * option)
2180{
2181  if(option)
2182    free(option);
2183}
2184
2185/**Function********************************************************************
2186
2187  Synopsis    [ Free statistic after SAT solving]
2188
2189  Description [ Free statistic after SAT solving]
2190
2191  SideEffects []
2192
2193  SeeAlso     []
2194
2195******************************************************************************/
2196void
2197sat_FreeStatistics(satStatistics_t * stats)
2198{
2199  if(stats)
2200    free(stats);
2201}
2202
2203
2204/**Function********************************************************************
2205
2206  Synopsis    [ Allocate option]
2207
2208  Description [ Allocate option ]
2209
2210  SideEffects []
2211
2212  SeeAlso     []
2213
2214******************************************************************************/
2215satOption_t *
2216sat_InitOption()
2217{
2218satOption_t *option;
2219
2220  option = ALLOC(satOption_t, 1);
2221  memset(option, 0, sizeof(satOption_t));
2222
2223  option->decisionHeuristic |= LATEST_CONFLICT_DECISION;
2224/**
2225  option->decisionHeuristic |= DVH_DECISION;
2226**/
2227  option->decisionAgeInterval = 0xff;
2228  option->decisionAgeRestart = 1;
2229  option->minConflictForDecision = 50;
2230  option->maxConflictForDecision = 10000;
2231  option->skipSatisfiedClauseForDecision = 0;
2232
2233
2234  /**
2235  option->clauseDeletionHeuristic |= MAX_UNRELEVANCE_DELETION;
2236  option->clauseDeletionHeuristic |= SIMPLE_LATEST_DELETION;
2237  **/
2238  option->clauseDeletionHeuristic |= LATEST_ACTIVITY_DELETION;
2239  option->clauseDeletionInterval = 2500;
2240  option->nextClauseDeletion = option->clauseDeletionInterval*5;
2241  option->unrelevance = 20;
2242  option->minLitsLimit = 20;
2243  option->maxLitsLimit = 1000;
2244
2245  option->latestUnrelevance = 45;
2246  option->obsoleteUnrelevance = 20;//6
2247  option->latestUsage = 100;
2248  option->obsoleteUsage = 2;
2249  option->latestRate = 16;
2250
2251  option->incNumObjLitsLimit = 20; /** 50 **/
2252  option->incNumNonobjLitsLimit = 50;
2253
2254  option->incPreserveNonobjective = 1;
2255  option->minimizeConflictClause = 1;
2256
2257
2258  option->BDDMonolithic = 0;
2259  option->BDDDPLL = 0;
2260  option->maxLimitOfVariablesForMonolithicBDD = 2000;
2261  option->maxLimitOfClausesForMonolithicBDD = 20000;
2262  option->maxLimitOfCutSizeForMonolithicBDD = 2000;
2263
2264  option->maxLimitOfVariablesForBDDDPLL = 200;
2265  option->maxLimitOfClausesForBDDDPLL = 2000;
2266  option->maxLimitOfCutSizeForBDDDPLL = 500;
2267
2268  option->maxLimitOfVariablesForBDD = 50;
2269
2270  option->memoryLimit = 1024 * 1024 * 1024;
2271
2272  return(option);
2273}
2274
2275/**Function********************************************************************
2276
2277  Synopsis    [ Report statistics]
2278
2279  Description [ Report statistics]
2280
2281  SideEffects []
2282
2283  SeeAlso     []
2284
2285******************************************************************************/
2286void
2287sat_ReportStatistics(
2288        satManager_t *cm,
2289        satStatistics_t *stats)
2290{
2291satOption_t *option;
2292
2293  option = cm->option;
2294  fprintf(cm->stdOut, "%s Number of decisions %d\n",
2295              cm->comment, stats->nDecisions);
2296  if(option->decisionHeuristic & DVH_DECISION) {
2297    fprintf(cm->stdOut, "%s Number of DVH decisions %d\n",
2298              cm->comment, stats->nDVHDecisions);
2299  }
2300  if(option->decisionHeuristic & LATEST_CONFLICT_DECISION) {
2301    fprintf(cm->stdOut, "%s Number of latest conflict decisions %d\n",
2302              cm->comment, stats->nLatestConflictDecisions);
2303  }
2304  fprintf(cm->stdOut, "%s Number of backtracks %d\n",
2305              cm->comment, stats->nBacktracks);
2306
2307  fprintf(cm->stdOut, "%s Number of CNF implications %d\n",
2308              cm->comment, stats->nCNFImplications);
2309  fprintf(cm->stdOut, "%s Number of Aig implications %d\n",
2310              cm->comment, stats->nAigImplications);
2311  fprintf(cm->stdOut, "%s Number of BDD implications %d\n",
2312              cm->comment, stats->nBDDImplications);
2313
2314  fprintf(cm->stdOut, "%s Number of unit conflict clauses %d\n",
2315              cm->comment, stats->nUnitConflictCl);
2316  fprintf(cm->stdOut, "%s Number of conflict clauses %d\n",
2317              cm->comment, stats->nConflictCl);
2318  fprintf(cm->stdOut, "%s Number of conflict literals %d\n",
2319              cm->comment, stats->nConflictLit);
2320  fprintf(cm->stdOut, "%s Number of deleted clauses %d\n",
2321              cm->comment, stats->nDeletedCl);
2322  fprintf(cm->stdOut, "%s Number of deleted literals %d\n",
2323              cm->comment, stats->nDeletedLit);
2324
2325  if(option->incTraceObjective + option->incDistill) {
2326    fprintf(cm->stdOut, "%s Number of init object conflict clauses %d\n",
2327              cm->comment, stats->nInitObjConflictCl);
2328    fprintf(cm->stdOut, "%s Number of init object conflict literals %d\n",
2329              cm->comment, stats->nInitObjConflictLit);
2330    fprintf(cm->stdOut, "%s Number of init non-object conflict clauses %d\n",
2331              cm->comment, stats->nInitNonobjConflictCl);
2332    fprintf(cm->stdOut, "%s Number of init non-object conflict literals %d\n",
2333              cm->comment, stats->nInitNonobjConflictLit);
2334    fprintf(cm->stdOut, "%s Number of object conflict clauses %d\n",
2335              cm->comment, stats->nObjConflictCl);
2336    fprintf(cm->stdOut, "%s Number of object conflict literals %d\n",
2337              cm->comment, stats->nObjConflictLit);
2338    fprintf(cm->stdOut, "%s Number of non-object conflict clauses %d\n",
2339              cm->comment, stats->nNonobjConflictCl);
2340    fprintf(cm->stdOut, "%s Number of non-object conflict literals %d\n",
2341              cm->comment, stats->nNonobjConflictLit);
2342  }
2343  if(option->incDistill) {
2344    fprintf(cm->stdOut, "%s Number of distill object conflict clauses %d\n",
2345              cm->comment, stats->nDistillObjConflictCl);
2346    fprintf(cm->stdOut, "%s Number of distill object conflict literals %d\n",
2347              cm->comment, stats->nDistillObjConflictLit);
2348    fprintf(cm->stdOut, "%s Number of distill non-object conflict clauses %d\n",
2349              cm->comment, stats->nDistillNonobjConflictCl);
2350    fprintf(cm->stdOut, "%s Number of distill non-object conflict literals %d\n",
2351              cm->comment, stats->nDistillNonobjConflictLit);
2352  }
2353  if(option->allSatMode) {
2354    fprintf(cm->stdOut, "%s Number of blocking clauses %d\n",
2355              cm->comment, stats->nBlockingCl);
2356    fprintf(cm->stdOut, "%s Number of blocking literals %d\n",
2357              cm->comment, stats->nBlockingLit);
2358  }
2359
2360  fprintf(cm->stdOut, "%s Maximum decision level %d\n",
2361              cm->comment, stats->maxDecisionLevel);
2362  fprintf(cm->stdOut, "%s Number of low score decisions %d\n",
2363              cm->comment, stats->nLowScoreDecisions);
2364  fprintf(cm->stdOut, "%s Total nonchronological backtracks %d\n",
2365              cm->comment, stats->nNonchonologicalBacktracks);
2366  fprintf(cm->stdOut, "%s Total run time %10g\n", cm->comment, stats->satTime);
2367  fflush(cm->stdOut);
2368
2369}
2370
2371/**Function********************************************************************
2372
2373  Synopsis    [ Allocate statistics]
2374
2375  Description [ Allocate statistics]
2376
2377  SideEffects []
2378
2379  SeeAlso     []
2380
2381******************************************************************************/
2382satStatistics_t *
2383sat_InitStatistics(void)
2384{
2385satStatistics_t *stats;
2386
2387  stats = ALLOC(satStatistics_t, 1);
2388  memset(stats, 0, sizeof(satStatistics_t));
2389
2390  return(stats);
2391}
2392
2393
2394/**Function********************************************************************
2395
2396  Synopsis    [ Set incremental option ]
2397
2398  Description [ Set incremental option ]
2399
2400  SideEffects []
2401
2402  SeeAlso     []
2403
2404******************************************************************************/
2405void
2406sat_SetIncrementalOption(satOption_t *option, int incFlag)
2407{
2408  if(incFlag == 0) return;
2409
2410  if(incFlag == 1)  { /* TraceObjective */
2411    option->incTraceObjective = 1;
2412  }
2413  else if(incFlag == 2)  { /* Distill */
2414    option->incDistill = 1;
2415  }
2416  else if(incFlag == 3)  { /* TraceObjective & Distill */
2417    option->incTraceObjective = 1;
2418    option->incDistill = 1;
2419  }
2420
2421}
2422
2423/**Function********************************************************************
2424
2425  Synopsis    [ Restore blocking clauses]
2426
2427  Description [ Restore blocking clauses]
2428
2429  SideEffects []
2430
2431  SeeAlso     []
2432
2433******************************************************************************/
2434void
2435sat_RestoreBlockingClauses(satManager_t *cm)
2436{
2437long *space, *start;
2438long c, v;
2439int i;
2440satArray_t *reached;
2441satArray_t *clause;
2442satArray_t *unitLits;
2443
2444  reached = cm->reached;
2445  if(reached == 0)
2446    return;
2447
2448  unitLits = cm->unitLits;
2449  if(unitLits == 0)
2450    unitLits = cm->unitLits = sat_ArrayAlloc(16);
2451
2452  clause = sat_ArrayAlloc(50);
2453
2454  for(i=0, space=reached->space; i<reached->num; i++, space++){
2455    if(*space <= 0) {
2456      space++;
2457      i++;
2458      if(i>=reached->num)
2459        break;
2460      start = space;
2461      clause->num = 0;
2462      while(*space > 0) {
2463        v = (*space);
2464        sat_ArrayInsert(clause, SATnot(v));
2465        i++;
2466        space++;
2467      }
2468
2469      c = sat_AddBlockingClause(cm, clause);
2470
2471      /**
2472        fprintf(stdout, "NOTICE : forwarded blocking clause\n");
2473        sat_PrintNode(cm, c);
2474        **/
2475
2476      if(clause->num == 1)
2477        sat_ArrayInsert(unitLits, (v));
2478      i--;
2479      space--;
2480    }
2481  }
2482  sat_ArrayFree(clause);
2483}
2484
2485/**Function********************************************************************
2486
2487  Synopsis    [ Restore Frontier clauses]
2488
2489  Description [ Restore Frontier clauses]
2490
2491  SideEffects []
2492
2493  SeeAlso     []
2494
2495******************************************************************************/
2496void
2497sat_RestoreFrontierClauses(satManager_t *cm)
2498{
2499long *space, *start;
2500long c, v;
2501int i;
2502satArray_t *frontier;
2503satArray_t *clause;
2504satArray_t *unitLits;
2505
2506  frontier = cm->frontier;
2507  cm->frontierNodesEnd = cm->nodesArraySize;
2508  if(frontier == 0)
2509    return;
2510
2511  unitLits = cm->unitLits;
2512  if(unitLits == 0)
2513    unitLits = cm->unitLits = sat_ArrayAlloc(16);
2514
2515  clause = sat_ArrayAlloc(50);
2516
2517  for(i=0, space=frontier->space; i<frontier->num; i++, space++){
2518    if(*space <= 0) {
2519      space++;
2520      i++;
2521      if(i>=frontier->num)
2522        break;
2523      start = space;
2524      clause->num = 0;
2525      while(*space > 0) {
2526        v = (*space);
2527        sat_ArrayInsert(clause, SATnot(v));
2528        i++;
2529        space++;
2530      }
2531
2532      c = sat_AddClause(cm, clause);
2533
2534      /**
2535      sat_PrintNode(cm, c);
2536      **/
2537
2538      cm->initNumClauses++;
2539      cm->initNumLiterals += clause->num;
2540      if(clause->num == 1)
2541        sat_ArrayInsert(unitLits, (v));
2542
2543      i--;
2544      space--;
2545    }
2546  }
2547  sat_ArrayFree(clause);
2548  cm->frontierNodesEnd = cm->nodesArraySize;
2549}
2550
2551/**Function********************************************************************
2552
2553  Synopsis    [ Restore clauses]
2554
2555  Description [ Restore clauses]
2556
2557  SideEffects []
2558
2559  SeeAlso     []
2560
2561******************************************************************************/
2562void
2563sat_RestoreClauses(satManager_t *cm, satArray_t *cnfArray)
2564{
2565long *space, *start;
2566long c, v;
2567int i;
2568satArray_t *clause;
2569satArray_t *unitLits;
2570
2571
2572  unitLits = cm->unitLits;
2573  if(unitLits == 0)
2574    unitLits = cm->unitLits = sat_ArrayAlloc(16);
2575
2576  clause = sat_ArrayAlloc(50);
2577
2578  for(i=0, space=cnfArray->space; i<cnfArray->num; i++, space++){
2579    if(*space <= 0) {
2580      space++;
2581      i++;
2582      if(i>=cnfArray->num)
2583        break;
2584      start = space;
2585      clause->num = 0;
2586      while(*space > 0) {
2587        v = (*space);
2588        sat_ArrayInsert(clause, SATnot(v));
2589        i++;
2590        space++;
2591      }
2592
2593      if(clause->num == 1) {
2594        sat_ArrayInsert(unitLits, (v));
2595      }
2596      else {
2597        c = sat_AddClause(cm, clause);
2598      }
2599
2600      cm->initNumClauses++;
2601      cm->initNumLiterals += clause->num;
2602
2603      i--;
2604      space--;
2605    }
2606  }
2607  sat_ArrayFree(clause);
2608}
2609
2610/**Function********************************************************************
2611
2612  Synopsis    [ Collect blocking clauses]
2613
2614  Description [ Collect blocking clauses]
2615
2616  SideEffects []
2617
2618  SeeAlso     []
2619
2620******************************************************************************/
2621void
2622sat_CollectBlockingClause(satManager_t *cm)
2623{
2624satArray_t *reached, *frontier;
2625long i, v, tv, *plit;
2626int j, size;
2627int inverted, num;
2628int nReachs, nFrontiers;
2629
2630  if(cm->reached == 0)  cm->reached = sat_ArrayAlloc(1024);
2631  if(cm->frontier == 0) cm->frontier = sat_ArrayAlloc(1024);
2632
2633  frontier = cm->frontier;
2634  reached = cm->reached;
2635
2636  frontier->num = 0;
2637  reached->num = 0;
2638  sat_ArrayInsert(frontier, 0);
2639  sat_ArrayInsert(reached, 0);
2640  nReachs = nFrontiers = 0;
2641
2642  for(i=cm->beginConflict; i<cm->nodesArraySize; i+=satNodeSize) {
2643    if(!(SATflags(i) & IsBlockingMask))
2644      continue;
2645
2646    if(SATreadInUse(i) == 0)            continue;
2647
2648    if((SATflags(i) & IsFrontierMask)) {
2649
2650      /**
2651      fprintf(stdout, "Frontier processed\n");
2652      sat_PrintNode(cm, i);
2653      **/
2654      plit = (long*)SATfirstLit(i);
2655      size = SATnumLits(i);
2656      num = frontier->num;
2657      for(j=0; j<size; j++, plit++) {
2658        v = SATgetNode(*plit);
2659        inverted = SATisInverted(v);
2660        tv = SATnormalNode(v);
2661        sat_ArrayInsert(frontier, v);
2662      }
2663      nFrontiers++;
2664      sat_ArrayInsert(frontier, 0);
2665    }
2666
2667    plit = (long*)SATfirstLit(i);
2668    size = SATnumLits(i);
2669    for(j=0; j<size; j++, plit++) {
2670      v = SATgetNode(*plit);
2671      sat_ArrayInsert(reached, v);
2672    }
2673    sat_ArrayInsert(reached, 0);
2674    nReachs ++;
2675  }
2676
2677
2678
2679  cm->frontier = frontier;
2680  cm->reached = reached;
2681  fprintf(stdout, "NOTICE : %d frontier are collected\n", nFrontiers);
2682  fprintf(stdout, "NOTICE : %d blocking clauses are collected\n", nReachs);
2683}
2684
2685
2686/**Function********************************************************************
2687
2688  Synopsis    [ Free interface]
2689
2690  Description [ Free interface]
2691
2692  SideEffects []
2693
2694  SeeAlso     []
2695
2696******************************************************************************/
2697void
2698sat_FreeInterface(satInterface_t *interface)
2699{
2700  if(interface == 0)    return;
2701
2702  if(interface->total)
2703    free(interface->total);
2704  if(interface->nonobjUnitLitArray)
2705    sat_ArrayFree(interface->nonobjUnitLitArray);
2706  if(interface->objUnitLitArray)
2707    sat_ArrayFree(interface->objUnitLitArray);
2708  if(interface->savedConflictClauses)
2709    free(interface->savedConflictClauses);
2710  free(interface);
2711}
2712
2713/**Function********************************************************************
2714
2715  Synopsis    [ Create AIG node ]
2716
2717  Description [ Create AIG node,
2718                This function is identical with bAig_CreateNode,
2719                We have this function here to isolate this package from baig]
2720
2721  SideEffects []
2722
2723  SeeAlso     []
2724
2725******************************************************************************/
2726long
2727sat_CreateNode(
2728        satManager_t *cm,
2729        long left,
2730        long right)
2731{
2732long newNode;
2733
2734  newNode = cm->nodesArraySize;
2735  //Bing: to deal with the case that cm->maxNodesArraySize is not multiple of
2736  // satNodeSize
2737  cm->nodesArraySize += satNodeSize;
2738
2739  if(cm->nodesArraySize >= cm->maxNodesArraySize) {
2740    cm->maxNodesArraySize = 2* cm->maxNodesArraySize;
2741    cm->nodesArray = REALLOC(long, cm->nodesArray, cm->maxNodesArraySize);
2742  }
2743  cm->nodesArray[newNode + satRight] = right;
2744  cm->nodesArray[newNode + satLeft] = left;
2745
2746  //cm->nodesArraySize += satNodeSize;
2747
2748  SATflags(newNode) = 0;
2749  SATnext(newNode) = 2;
2750  SATnFanout(newNode) = 0;
2751  /**
2752  SATfanout(newNode) = 0;
2753  **/
2754  (cm->nodesArray[newNode+satFanout]) = 0;
2755  //Bing:
2756  SATvalue(newNode) = 2;
2757
2758  return(newNode);
2759}
2760
2761/**Function********************************************************************
2762
2763  Synopsis    [ Usage of memory ]
2764
2765  Description [ Usage of memory ]
2766
2767  SideEffects []
2768
2769  SeeAlso     []
2770
2771******************************************************************************/
2772int
2773sat_MemUsage(satManager_t *cm)
2774{
2775satLiteralDB_t *literals;
2776satStatistics_t *stats;
2777int aigSize, cnfSize, watchedSize;
2778
2779  literals = cm->literals;
2780  stats = cm->each;
2781  aigSize = sizeof(int) * cm->maxNodesArraySize;
2782  cnfSize = sizeof(int) * (literals->end - literals->begin);
2783  watchedSize = sizeof(int) * 2 *
2784                 (stats->nConflictCl - stats->nDeletedCl);
2785  return(aigSize + cnfSize + watchedSize);
2786}
2787
2788
2789
2790/**Function********************************************************************
2791
2792  Synopsis    [ Get canonical node ]
2793
2794  Description [ Get canonical node ]
2795
2796  SideEffects []
2797
2798  SeeAlso     []
2799
2800******************************************************************************/
2801long
2802sat_GetCanonical(satManager_t *cm, long v)
2803{
2804long nv;
2805int inverted;
2806
2807  if(v == 2)    return(2);
2808
2809  while(!(SATflags(SATnormalNode(v))) & CanonicalBitMask) {
2810    inverted = SATisInverted(v);
2811    v = SATnormalNode(v);
2812    nv = SATcanonical(v);
2813    if(inverted)
2814      nv = SATnot(nv);
2815    v = nv;
2816  }
2817  return(v);
2818}
2819
2820
2821/**Function********************************************************************
2822
2823  Synopsis    [ Combine statistics of several runs]
2824
2825  Description [ Combine statistics of several runs]
2826
2827  SideEffects []
2828
2829  SeeAlso     []
2830
2831******************************************************************************/
2832void
2833sat_CombineStatistics(satManager_t *cm)
2834{
2835    /* CONSIDER ... */
2836}
2837
2838/**Function********************************************************************
2839
2840  Synopsis    [ Get the number of initial clauses ]
2841
2842  Description [ Get the number of initial clauses.
2843                This function works properly only CNF sat case]
2844
2845  SideEffects []
2846
2847  SeeAlso     []
2848
2849******************************************************************************/
2850int
2851sat_GetNumberOfInitialClauses(satManager_t *cm)
2852{
2853  return(cm->initNumClauses);
2854}
2855
2856/**Function********************************************************************
2857
2858  Synopsis    [ Get the number of initial variables ]
2859
2860  Description [ Get the number of initial variables.
2861                This function works properly only CNF sat case]
2862
2863  SideEffects []
2864
2865  SeeAlso     []
2866
2867******************************************************************************/
2868int
2869sat_GetNumberOfInitialVariables(satManager_t *cm)
2870{
2871  return(cm->initNumVariables);
2872}
2873
2874/**Function********************************************************************
2875
2876  Synopsis    [ Read forced assignments.]
2877
2878  Description [ Read forced assignments.]
2879
2880  SideEffects []
2881
2882  SeeAlso     []
2883
2884******************************************************************************/
2885satArray_t *
2886sat_ReadForcedAssignment(
2887        char *filename)
2888{
2889FILE *fin;
2890char line[102400], word[1024];
2891char *lp;
2892satArray_t *arr;
2893long v;
2894
2895  if(!(fin = fopen(filename, "r"))) {
2896    fprintf(stdout, "ERROR : Can't open file %s\n", filename);
2897    return(0);
2898  }
2899
2900  arr = sat_ArrayAlloc(64);
2901  while(fgets(line, 102400, fin)) {
2902    lp = sat_RemoveSpace(line);
2903    if(lp[0] == '\n')   continue;
2904    while(1) {
2905      lp = sat_RemoveSpace(lp);
2906      lp = sat_CopyWord(lp, word);
2907      if(strlen(word)) {
2908        v = atoi(word);
2909        v *= satNodeSize;
2910        if(v < 0)       v = SATnot(-v);
2911        sat_ArrayInsert(arr, v);
2912      }
2913      else {
2914        break;
2915      }
2916    }
2917  }
2918  fclose(fin);
2919
2920  return(arr);
2921}
2922
2923/**Function********************************************************************
2924
2925  Synopsis    [ Apply forced assignments.]
2926
2927  Description [ Apply forced assignments.]
2928
2929  SideEffects []
2930
2931  SeeAlso     []
2932
2933******************************************************************************/
2934int
2935sat_ApplyForcedAssigment(
2936        satManager_t *cm,
2937        satArray_t *arr,
2938        satLevel_t *d)
2939{
2940long v;
2941int i, inverted, errorFlag;
2942
2943  errorFlag = 0;
2944  for(i=0; i<arr->num; i++) {
2945    v = arr->space[i];
2946    inverted = SATisInverted(v);
2947    v = SATnormalNode(v);
2948
2949    SATvalue(v) = !inverted;
2950    SATmakeImplied(v, d);
2951    sat_Enqueue(cm->queue, v);
2952    SATflags(v) |= InQueueMask;
2953    sat_ImplicationMain(cm, d);
2954    if(d->conflict) {
2955      fprintf(cm->stdOut,
2956              "%s WARNING : conflict happens at level %d while applying forced assignments\n", cm->comment, d->level);
2957      errorFlag = 1;
2958      break;
2959    }
2960  }
2961  if(errorFlag)
2962    return(SAT_UNSAT);
2963  else
2964    return(0);
2965}
2966
2967/**Function********************************************************************
2968
2969  Synopsis    [ Apply forced assignments.]
2970
2971  Description [ Apply forced assignments.]
2972
2973  SideEffects []
2974
2975  SeeAlso     []
2976
2977******************************************************************************/
2978void
2979sat_ApplyForcedAssignmentMain(
2980        satManager_t *cm,
2981        satLevel_t *d)
2982{
2983satArray_t *forcedArr;
2984int flag;
2985
2986  forcedArr = cm->option->forcedAssignArr;
2987  flag = 0;
2988  if(forcedArr) {
2989    flag = sat_ApplyForcedAssigment(cm, forcedArr, d);
2990  }
2991
2992  if(flag == SAT_UNSAT) {
2993    cm->status = SAT_UNSAT;
2994    return;
2995  }
2996}
2997
2998/**Function********************************************************************
2999
3000  Synopsis    [ Put assignments.]
3001
3002  Description [ Put assignments.]
3003
3004  SideEffects []
3005
3006  SeeAlso     []
3007
3008******************************************************************************/
3009void
3010sat_PutAssignmentValueMain(
3011        satManager_t *cm,
3012        satLevel_t *d,
3013        satArray_t *arr)
3014{
3015long v;
3016int i;
3017int inverted;
3018
3019  if(arr == 0)  return;
3020
3021  if(cm->variableArray == 0) {
3022    cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
3023    memset(cm->variableArray, 0,
3024            sizeof(satVariable_t) * (cm->initNumVariables+1));
3025  }
3026
3027  for(i=0; i<arr->num; i++) {
3028    v = arr->space[i];
3029    inverted = SATisInverted(v);
3030    v = SATnormalNode(v);
3031
3032    SATvalue(v) = !inverted;
3033  }
3034}
3035
3036/**Function********************************************************************
3037
3038  Synopsis    [ Clause deletion heuristic based on usage of conflict clause ]
3039
3040  Description [ Clause deletion heuristic based on usage of conflict clause ]
3041
3042  SideEffects []
3043
3044  SeeAlso     []
3045
3046******************************************************************************/
3047void
3048sat_ClauseDeletionLatestActivity(satManager_t *cm)
3049{
3050satLiteralDB_t *literals;
3051satOption_t *option;
3052long nv, v, *plit, *clit;
3053long usage, totalConflictCl;
3054long index, lit;
3055
3056int size, n0, n1x, deleteFlag;
3057int unrelevance;
3058int usedLimit;
3059int inverted, i;
3060int value;
3061int nLatestCl;
3062int nDeletedCl;
3063double ratio;
3064
3065/**
3066 LATEST_ACTIVITY_DELETION
3067 MAX_UNRELEVANCE_DELETION
3068 SIMPLE_LATEST_DELETION
3069**/
3070
3071  option = cm->option;
3072  if(option->clauseDeletionHeuristic == 0)      return;
3073
3074  totalConflictCl = (cm->nodesArraySize - cm->beginConflict)/satNodeSize;
3075  nDeletedCl = cm->each->nDeletedCl;
3076  nLatestCl = totalConflictCl/option->latestRate;
3077  literals = cm->literals;
3078  index = 0;
3079  for(clit = literals->last-1; clit > literals->begin; clit--){
3080    if(*clit == 0)
3081      continue;
3082    if(index >= totalConflictCl)
3083      break;
3084    v = -(*clit);
3085
3086    plit = (long*)SATfirstLit(v);
3087    clit = plit - 1;
3088    index++;
3089
3090    if(nLatestCl > 0) {
3091      nLatestCl--;
3092      unrelevance = option->latestUnrelevance;
3093    }
3094    else {
3095      unrelevance = option->obsoleteUnrelevance;
3096    }
3097
3098    if(!(SATflags(v) & IsConflictMask)) continue;
3099    if((SATflags(v) & IsFrontierMask))  continue;
3100
3101    if(option->incPreserveNonobjective && (SATflags(v) & NonobjMask))
3102      continue;
3103
3104    usage = SATconflictUsage(v);
3105    SATconflictUsage(v) = usage/2;
3106    size = SATnumLits(v);
3107//    if(size < option->minLitsLimit)   continue;
3108    if(size < unrelevance)
3109      continue;
3110
3111    usedLimit = option->obsoleteUsage +
3112        (option->latestUsage-option->obsoleteUsage)*index/totalConflictCl;
3113    if(usage > usedLimit)
3114      continue;
3115
3116
3117    n0 = n1x = 0;
3118    deleteFlag = 0;
3119    for(i=0; i<size; i++, plit++) {
3120      lit = *plit;
3121      nv = SATgetNode(lit);
3122      inverted = SATisInverted(nv);
3123      nv = SATnormalNode(nv);
3124      value = SATvalue(nv) ^ inverted;
3125
3126      if(value == 0)    n0++;
3127      else if(value == 1) {
3128        n1x++;
3129        if(SATlevel(nv) == 0)   deleteFlag = 1;
3130      }
3131      else      n1x++;
3132
3133      if(deleteFlag) {
3134        sat_DeleteClause(cm, v);
3135        sat_Enqueue(cm->unusedAigQueue, v);
3136        break;
3137      }
3138      if((size > option->maxLitsLimit) && (n1x > 1)) {
3139        sat_DeleteClause(cm, v);
3140        sat_Enqueue(cm->unusedAigQueue, v);
3141        break;
3142      }
3143      if(n1x > unrelevance) {
3144        sat_DeleteClause(cm, v);
3145        sat_Enqueue(cm->unusedAigQueue, v);
3146        break;
3147      }
3148    }
3149
3150  }
3151
3152  cm->each->nDeletedButUncompacted += cm->each->nDeletedCl - nDeletedCl;
3153  ratio = (double)cm->each->nDeletedButUncompacted/
3154          (double)(cm->each->nConflictCl-cm->each->nDeletedCl);
3155
3156  if(ratio> 0.2) {
3157    sat_CompactClauses(cm);
3158    cm->each->nDeletedButUncompacted = 0;
3159  }
3160
3161}
3162
3163
3164/**Function********************************************************************
3165
3166  Synopsis    [ Find a clause index from literal pointer.]
3167
3168  Description [ Find a clause index from literal pointer.]
3169
3170  SideEffects []
3171
3172  SeeAlso     []
3173
3174******************************************************************************/
3175long
3176sat_GetClauseFromLit(
3177        satManager_t *cm,
3178        long *lit)
3179{
3180  while(*lit > 0) {
3181    lit++;
3182  }
3183  return(-(*lit));
3184}
3185/**Function********************************************************************
3186
3187  Synopsis    [ Compare node index to sort ]
3188
3189  Description [ Compare node index to sort ]
3190
3191  SideEffects []
3192
3193  SeeAlso     []
3194
3195******************************************************************************/
3196static int
3197NodeIndexCompare(const void *x, const void *y)
3198{
3199long n1, n2;
3200
3201  n1 = *(long *)x;
3202  n2 = *(long *)y;
3203  return(n1 > n2);
3204}
Note: See TracBrowser for help on using the repository browser.