source: vis_dev/vis-2.3/src/sat/satDecision.c @ 84

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

vis2.3
File size: 21.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [satDecision.c]
4
5  PackageName [sat]
6
7  Synopsis    [Routines for various decision heuristics.]
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: satDecision.c,v 1.28 2009/04/11 18:26:37 fabio Exp $";
22static  satManager_t *SatCm;
23
24/*---------------------------------------------------------------------------*/
25/* Constant declarations                                                     */
26/*---------------------------------------------------------------------------*/
27
28/**AutomaticStart*************************************************************/
29
30/*---------------------------------------------------------------------------*/
31/* Static function prototypes                                                */
32/*---------------------------------------------------------------------------*/
33
34static int ScoreCompare(const void * node1, const void * node2);
35
36/**AutomaticEnd***************************************************************/
37
38
39/*---------------------------------------------------------------------------*/
40/* Definition of exported functions                                          */
41/*---------------------------------------------------------------------------*/
42
43
44/**Function********************************************************************
45
46  Synopsis    [ Select decision variable]
47
48  Description [ Select decision variable]
49
50  SideEffects []
51
52  SeeAlso     []
53
54******************************************************************************/
55satLevel_t *
56sat_MakeDecision(satManager_t *cm)
57{
58satLevel_t *d;
59int value;
60long v;
61satStatistics_t *stats;
62
63  d = SATgetDecision(cm->currentDecision);
64
65  if(cm->queue->size)
66    return(d);
67
68  d = sat_AllocLevel(cm);
69
70  v = 0;
71  v = sat_DecisionBasedOnBDD(cm, d);
72
73  if(v == 0)
74    v = sat_DecisionBasedOnLatestConflict(cm, d);
75
76  if(v == 0)
77    v = sat_DecisionBasedOnScore(cm, d);
78
79  if(v == 0)
80    return(0);
81
82
83  stats = cm->each;
84
85  stats->nDecisions++;
86
87  value = !(SATisInverted(v));
88  v = SATnormalNode(v);
89  d->decisionNode = v;
90  d->nConflict = cm->each->nConflictCl;
91
92  SATvalue(v) = value;
93  /**
94  if(cm->option->verbose > 1) {
95    var = SATgetVariable(v);
96    fprintf(cm->stdOut, "decision at %3d on %6d <- %d score(%d %d) %d\n",
97            d->level, v, value, var->scores[0], var->scores[1],
98            cm->each->nDecisions);
99    fflush(cm->stdOut);
100  }
101  **/
102  SATmakeImplied(v, d);
103
104  sat_Enqueue(cm->queue, v);
105  SATflags(v) |= InQueueMask;
106
107  return(d);
108}
109
110
111/**Function********************************************************************
112
113  Synopsis    [ Decision making based on current top clause ]
114
115  Description [ Decision making based on current top clause ]
116
117  SideEffects []
118
119  SeeAlso     []
120
121******************************************************************************/
122long
123sat_DecisionBasedOnLatestConflict(
124        satManager_t *cm,
125        satLevel_t *d)
126{
127satOption_t *option;
128satStatistics_t *stats;
129satLiteralDB_t *literals;
130satVariable_t *var;
131int size, limit;
132long *plit, *tplit;
133long v, lit, tv, maxV;
134int tsize, count;
135int inverted, value;
136int i, j, satisfied;
137int tmpScore, maxScore;
138
139  option = cm->option;
140  stats = cm->each;
141
142  if(!(option->decisionHeuristic & LATEST_CONFLICT_DECISION))
143    return(0);
144
145  /** CONSIDER
146  if(stats->nConflictCl < option->minConflictForDecision)
147    return(0);
148
149  **/
150
151
152  if(cm->currentTopConflict == 0)
153    return(0);
154
155  literals = cm->literals;
156  size = literals->last - literals->begin;
157
158  limit = MAXINT;
159  if(option->maxConflictForDecision > 0)
160    limit = option->maxConflictForDecision;
161
162  count = cm->currentTopConflictCount;
163  tv = -(*(cm->currentTopConflict));
164  tsize = SATnumLits(tv);
165  tplit = (long*)SATfirstLit(tv);
166  plit = tplit + tsize;
167
168  for(i=plit-literals->begin; i>=0; i--, plit--) {
169/**  for(plit =literals->last-1, i=literals->last - literals->begin; i>=0; i--, plit--) { */
170    if(count > limit)   break;
171
172    lit = *plit;
173    if(lit < 0) {
174      tv = -lit;
175
176      if(!(SATflags(tv) & IsConflictMask))
177        return(0);
178
179      if(plit < (long*)SATfirstLit(tv))
180        continue;
181
182      count++;
183
184      if(option->skipSatisfiedClauseForDecision) {
185        tsize = SATnumLits(tv);
186        tplit = (long *)SATfirstLit(tv);
187        satisfied = 0;
188        maxScore = -1;
189        maxV = 0;
190        for(j=0; j<tsize; j++, tplit++) {
191          v = SATgetNode(*tplit);
192          inverted = SATisInverted(v);
193          v = SATnormalNode(v);
194          value = SATvalue(v) ^ inverted;
195          if(value == 1) {
196            satisfied = 1;
197            break;
198          }
199          else if(value == 0) {
200            continue;
201          }
202          var = SATgetVariable(v);
203          tmpScore = (var->scores[0] >= var->scores[1]) ? var->scores[0] : var->scores[1];
204          if(tmpScore > maxScore) {
205            maxScore = tmpScore;
206            maxV = v;
207          }
208        }
209        if(satisfied) {
210          i = i - tsize - 1;
211          plit = plit - tsize -1;
212        }
213        else {
214          var = SATgetVariable(maxV);
215          value = (var->scores[0] >= var->scores[1]) ? 0 : 1;
216
217          cm->currentTopConflict = (long*)SATfirstLit(tv) + SATnumLits(tv);
218          cm->currentTopConflictCount = count;
219
220          stats = cm->each;
221          stats->nLatestConflictDecisions++;
222          return(maxV ^ !value);
223        }
224      }
225      continue;
226    }
227    else if(lit == 0)
228      continue;
229
230    v = SATgetNode(lit);
231    inverted = SATisInverted(v);
232    v = SATnormalNode(v);
233    value = SATvalue(v) ^ inverted;
234
235    if(value >= 2) {
236      var = SATgetVariable(v);
237      value = (var->conflictLits[0] >= var->conflictLits[1]) ? 0 : 1;
238
239      cm->currentTopConflict = (long*)SATfirstLit(tv) + SATnumLits(tv);
240      cm->currentTopConflictCount = count;
241
242      stats = cm->each;
243      stats->nLatestConflictDecisions++;
244      return(v ^ !value);
245    }
246  }
247  return(0);
248}
249
250/**Function********************************************************************
251
252  Synopsis    [ Check decision variable to check correctness of currentVarPos,
253                since currentVarPos has to point lowest variable that are
254                not implied.]
255
256  Description [ Check decision variable to check correctness of currentVarPos,
257                since currentVarPos has to point lowest variable that are
258                not implied.]
259
260  SideEffects []
261
262  SeeAlso     []
263
264******************************************************************************/
265void
266sat_CheckDecisonVariableArray(
267        satManager_t *cm)
268{
269satArray_t *orderedVariableArray;
270int size, i;
271long v;
272
273  orderedVariableArray = cm->orderedVariableArray;
274  size = orderedVariableArray->num;
275  for(i=0; i<cm->currentVarPos; i++) {
276    v = orderedVariableArray->space[i];
277    if(SATvalue(v) > 1) {
278      fprintf(stdout, " ERROR : wrong current variable pos %d at %d\n",
279              cm->currentVarPos, i);
280    }
281  }
282}
283
284/**Function********************************************************************
285
286  Synopsis    [ Decision making based on score based heuristic ]
287
288  Description [ Decision making based on score based heuristic ]
289
290  SideEffects []
291
292  SeeAlso     []
293
294******************************************************************************/
295long
296sat_DecisionBasedOnScore(
297        satManager_t *cm,
298        satLevel_t *d)
299{
300int size, i;
301long v;
302int value;
303satVariable_t *var;
304satArray_t *orderedVariableArray;
305satStatistics_t *stats;
306satOption_t *option;
307
308
309  option = cm->option;
310  orderedVariableArray = cm->orderedVariableArray;
311  size = orderedVariableArray->num;
312
313  for(i=cm->currentVarPos; i<size; i++) {
314    v = orderedVariableArray->space[i];
315    if(SATvalue(v) < 2) continue;
316
317    var = SATgetVariable(v);
318    value = (var->scores[0] >= var->scores[1]) ? 0 : 1;
319
320    stats = cm->each;
321    if((var->scores[0]+var->scores[1]) < 1) {
322      stats->nLowScoreDecisions++;
323    }
324
325
326    if((option->decisionHeuristic & DVH_DECISION))
327      stats->nDVHDecisions++;
328    else
329      stats->nVSIDSDecisions++;
330
331    cm->currentVarPos = i;
332    d->currentVarPos = i;
333
334    return(v ^ !value);
335  }
336
337  return(0);
338}
339
340/**Function********************************************************************
341
342  Synopsis    [ Take care of decision by BDD based mathod ]
343
344  Description [ Take care of decision by BDD based mathod ]
345
346  SideEffects []
347
348  SeeAlso     []
349
350******************************************************************************/
351long
352sat_DecisionBasedOnBDD(
353        satManager_t *cm,
354        satLevel_t *d)
355{
356satArray_t *arr;
357long nv, v;
358
359  if(cm->assignByBDD == 0)
360    return(0);
361
362  arr = cm->assignByBDD;
363  if(arr->num == 0)
364    return(0);
365
366  /**
367  for(i=0; i<arr->num; i++) {
368    v = arr->space[i];
369    nv = SATnormalNode(v);
370    if(SATvalue(nv) > 1)
371      return(v);
372  }
373  **/
374
375  while(arr->num) {
376    v = arr->space[arr->num-1];
377    nv = SATnormalNode(v);
378    arr->num--;
379    if(SATvalue(nv) > 1)
380      return(v);
381  }
382  return(0);
383}
384
385
386long
387sat_DecisionBasedOnShrink(
388        satManager_t *cm)
389{
390satArray_t *arr;
391long nv, v;
392
393  if(cm->shrinkArray == 0)
394    return(0);
395
396  arr = cm->shrinkArray;
397  if(arr->num == 0)
398    return(0);
399
400  while(arr->num) {
401    v = arr->space[arr->num-1];
402    nv = SATnormalNode(v);
403    arr->num--;
404    if(SATvalue(nv) > 1)
405      return(v);
406  }
407  return(0);
408}
409
410
411/**Function********************************************************************
412
413  Synopsis    [ Update the score of variables ]
414
415  Description [ Update the score of variables ]
416
417  SideEffects []
418
419  SeeAlso     []
420
421******************************************************************************/
422void
423sat_UpdateScore(
424        satManager_t *cm)
425{
426satArray_t *one, *tmp;
427satArray_t *ordered;
428satVariable_t *var;
429int size, i;
430long v;
431int value;
432
433  ordered = cm->orderedVariableArray;
434
435  one = sat_ArrayAlloc(ordered->num);
436  tmp = sat_ArrayAlloc(ordered->num);
437
438  size = ordered->num;
439  for(i=0; i<size; i++) {
440    v = ordered->space[i];
441
442    if(SATvalue(v) < 2 && SATlevel(v) == 0)
443      continue;
444
445    var = SATgetVariable(v);
446    var->scores[0] = (var->scores[0]>>1) + var->litsCount[0] - var->lastLitsCount[0];
447    var->scores[1] = (var->scores[1]>>1) + var->litsCount[1] - var->lastLitsCount[1];
448    var->lastLitsCount[0] = var->litsCount[0];
449    var->lastLitsCount[1] = var->litsCount[1];
450
451
452    if((var->scores[0] + var->scores[1]) < 1) {
453      sat_ArrayInsert(one, v);
454    }
455    else {
456      value = (var->scores[0] > var->scores[1]) ? var->scores[0] : var->scores[1];
457      sat_ArrayInsert(tmp, v);
458      sat_ArrayInsert(tmp, value);
459    }
460  }
461
462  SatCm = cm;
463  qsort(tmp->space, (tmp->num)>>1, sizeof(long)*2, ScoreCompare);
464
465  ordered->num = 0;
466  size = tmp->num;
467  for(i=0; i<size; i++) {
468    v = tmp->space[i];
469    sat_ArrayInsert(ordered, v);
470    var = SATgetVariable(v);
471    var->pos = (i>>1);
472    i++;
473  }
474
475  size = one->num;
476  for(i=0; i<size; i++) {
477    v = one->space[i];
478    var = SATgetVariable(v);
479    var->pos = ordered->num;
480    sat_ArrayInsert(ordered, v);
481  }
482
483  sat_ArrayFree(one);
484  sat_ArrayFree(tmp);
485
486  cm->orderedVariableArray = ordered;
487  cm->currentVarPos = 0;
488
489  for(i=1; i<cm->currentDecision; i++) {
490    cm->decisionHead[i].currentVarPos = 0;
491  }
492
493  if(cm->option->verbose > 3)
494    sat_PrintScore(cm);
495
496}
497
498
499/**Function********************************************************************
500
501  Synopsis    [ Update the score of variables by deepest variable hike]
502
503  Description [ Update the score of variables by deepest variable hike]
504
505  SideEffects []
506
507  SeeAlso     []
508
509******************************************************************************/
510void
511sat_UpdateDVH(
512        satManager_t *cm,
513        satLevel_t *d,
514        satArray_t *clauseArray,
515        int bLevel,
516        long unitLit)
517{
518satArray_t *ordered;
519satLevel_t *td;
520satVariable_t *var, *tvar, *ttvar;
521int score, tscore, ttscore;
522int value;
523long v;
524int gap, i, insert;
525
526
527  ordered = cm->orderedVariableArray;
528
529  unitLit = SATnormalNode(unitLit);
530  gap = cm->currentDecision - bLevel;
531  td = SATgetDecision(bLevel+1);
532
533  if(gap <= 1) {
534      /** CONSIDER .... */
535  }
536  var = SATgetVariable(unitLit);
537  tvar = SATgetVariable(td->decisionNode);
538
539  score = (var->scores[1] > var->scores[0]) ? var->scores[1] : var->scores[0];
540  tscore = (tvar->scores[1] > tvar->scores[0]) ? tvar->scores[1] : tvar->scores[0];
541
542  if(score >= tscore)   {
543    return;
544  }
545
546  tscore += 1;
547
548  value = SATvalue(unitLit);
549  if(value == 0)var->scores[1] = tscore;
550  else          var->scores[0] = tscore;
551
552  ordered = cm->orderedVariableArray;
553  insert = 0;
554  for(i=var->pos; i>=1; i--) {
555    v = ordered->space[i-1];
556    ttvar = SATgetVariable(v);
557    ttscore = (ttvar->scores[1] > ttvar->scores[0]) ? ttvar->scores[1] : ttvar->scores[0];
558    if(tscore > ttscore && i>1) {
559      ttvar->pos = i;
560      ordered->space[i] = v;
561      continue;
562    }
563
564    var->pos = i;
565    ordered->space[i] = unitLit;
566    insert = 1;
567    break;
568  }
569
570  if(insert == 0) {
571    var->pos = i;
572    ordered->space[0] = unitLit;
573  }
574
575  for(i=d->level; i>0; i--) {
576    td = SATgetDecision(i);
577    if(td->currentVarPos < var->pos)
578      break;
579    td->currentVarPos = var->pos;
580  }
581  cm->currentVarPos = td->currentVarPos;
582
583}
584
585/**Function********************************************************************
586
587  Synopsis    [ Check correctness of variable order ]
588
589  Description [ Check correctness of variable order ]
590
591  SideEffects []
592
593  SeeAlso     []
594
595******************************************************************************/
596void
597sat_CheckOrderedVariableArray(satManager_t *cm)
598{
599satArray_t *ordered;
600satVariable_t *var;
601int i;
602long v;
603
604  ordered = cm->orderedVariableArray;
605  for(i=0; i<ordered->num; i++) {
606    v = ordered->space[i];
607    var = SATgetVariable(v);
608    if(i != var->pos) {
609      fprintf(cm->stdOut, "Error : wrong variable position %d %d in ordered array\n", i, var->pos);
610
611    }
612  }
613}
614
615/**Function********************************************************************
616
617  Synopsis    [ Generate initial score ]
618
619  Description [ Generate initial score ]
620
621  SideEffects []
622
623  SeeAlso     []
624
625******************************************************************************/
626void
627sat_InitScore(satManager_t *cm)
628{
629int objExist;
630int j, inverted;
631long *plit, v, nv, i;
632int size;
633int count0, count1;
634satArray_t *ordered, *newOrdered;
635satVariable_t *var;
636
637  ordered = cm->orderedVariableArray;
638  if(ordered == 0)
639    ordered = sat_ArrayAlloc(cm->initNumVariables);
640  else
641    ordered->num = 0;
642  cm->orderedVariableArray = ordered;
643
644  objExist = 0;
645  /**
646  if(cm->obj && cm->obj->num) {
647    sat_MarkTransitiveFaninForArray(cm, cm->obj, VisitedMask);
648    objExist = 1;
649  }
650  **/
651
652
653  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
654    v = i;
655    if((SATflags(v) & IsBDDMask)) {
656      continue;
657    }
658    if((SATflags(v) & IsCNFMask)) {
659      size = SATnumLits(v);
660      plit = (long*)SATfirstLit(v);
661      for(j=0; j<size; j++, plit++) {
662        nv = SATgetNode(*plit);
663        inverted = !(SATisInverted(nv));
664        nv = SATnormalNode(nv);
665        var = SATgetVariable(nv);
666        var->litsCount[inverted]++;
667      }
668      continue;
669    }
670    if(!(SATflags(v) & CoiMask))        continue;
671    if(!(SATflags(v) & VisitedMask) && objExist)        continue;
672
673    if(SATvalue(v) != 2 && SATlevel(v) == 0)    continue;
674
675    count0 = count1 = SATnFanout(v);
676    if(count0 == 0 && SATleftChild(v) == 2 && SATrightChild(v) == 2) {
677      count0 = 0;
678      count1 = 0;
679    }
680    else if(SATleftChild(v) != 2) {
681      count0 += 2;
682      count1++;
683    }
684    else {
685      count0 += 3;
686      count1 += 3;
687    }
688
689    var = SATgetVariable(v);
690    var->litsCount[0] += count0;
691    var->litsCount[1] += count1;
692
693    sat_ArrayInsert(ordered, v);
694  }
695
696  //Bing:
697  if(cm->unitLits){
698    for(i=0; i<cm->unitLits->num; i++) {
699      v = cm->unitLits->space[i];
700      v = SATnormalNode(v);
701      SATflags(v) |= NewMask;
702    }
703  }
704
705  if(cm->assertion) {
706    for(i=0; i<cm->assertion->num; i++) {
707      v = cm->assertion->space[i];
708      v = SATnormalNode(v);
709      SATflags(v) |= NewMask;
710    }
711  }
712
713  newOrdered = sat_ArrayAlloc((ordered->num) * 2);
714  size = ordered->num;
715  for(i=0; i<size; i++) {
716    v = ordered->space[i];
717    var = SATgetVariable(v);
718    var->scores[0] = var->lastLitsCount[0] = var->litsCount[0];
719    var->scores[1] = var->lastLitsCount[1] = var->litsCount[1];
720
721    if(SATflags(v) & NewMask);
722    else if(var->scores[0] == 0 && var->scores[1] == 0 && !(SATflags(v) & NewMask)) {
723      sat_ArrayInsert(cm->pureLits, (v));
724    }
725    else if(var->scores[0] == 0 && !(SATflags(v) & NewMask)) {
726      sat_ArrayInsert(cm->pureLits, (v));
727    }
728    else if(var->scores[1] == 0 && !(SATflags(v) & NewMask)) {
729      sat_ArrayInsert(cm->pureLits, SATnot(v));
730    }
731    else {
732      sat_ArrayInsert(newOrdered, v);
733      sat_ArrayInsert(newOrdered, (var->scores[0] > var->scores[1]) ? var->scores[0] : var->scores[1]);
734    }
735  }
736
737  //Bing:
738  if(cm->unitLits){
739    for(i=0; i<cm->unitLits->num; i++) {
740      v = cm->unitLits->space[i];
741      v = SATnormalNode(v);
742      SATflags(v) &= ResetNewMask;
743    }
744  }
745
746  if(cm->assertion) {
747    for(i=0; i<cm->assertion->num; i++) {
748      v = cm->assertion->space[i];
749      v = SATnormalNode(v);
750      SATflags(v) &= ResetNewMask;
751    }
752  }
753
754  cm->orderedVariableArray = ordered;
755  size = newOrdered->num;
756  qsort(newOrdered->space, size>>1, sizeof(long)*2, ScoreCompare);
757
758  cm->currentVarPos = 0;
759  ordered->num = 0;
760  for(i=0; i<size; i++) {
761    v = newOrdered->space[i];
762    var = SATgetVariable(v);
763    var->pos = (i>>1);
764    sat_ArrayInsert(ordered, v);
765    i++;
766  }
767
768  sat_ArrayFree(newOrdered);
769
770  /**
771  if(cm->obj && cm->obj->num) {
772    sat_UnmarkTransitiveFaninForArray(
773            cm, cm->obj, VisitedMask, ResetVisitedMask);
774  }
775  **/
776
777  if(cm->option->verbose > 3)
778    sat_PrintScore(cm);
779}
780
781/**Function********************************************************************
782
783  Synopsis    [ Generate initial score for CNF and AIG ]
784
785  Description [ Generate initial score for CNF and AIG]
786
787  SideEffects []
788
789  SeeAlso     []
790
791******************************************************************************/
792void
793sat_InitScoreForMixed(satManager_t *cm)
794{
795int j, inverted;
796long *plit, v, nv, i;
797int size;
798int count0, count1;
799satArray_t *ordered, *newOrdered;
800satVariable_t *var;
801
802  ordered = cm->orderedVariableArray;
803  if(ordered == 0)
804    ordered = sat_ArrayAlloc(cm->initNumVariables);
805  else
806    ordered->num = 0;
807  cm->orderedVariableArray = ordered;
808
809  /**
810  objExist = 0;
811  if(cm->obj && cm->obj->num) {
812    sat_MarkTransitiveFaninForArray(cm, cm->obj, VisitedMask);
813    objExist = 1;
814  }
815  **/
816
817
818  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
819    v = i;
820    if((SATflags(v) & IsBDDMask)) {
821      continue;
822    }
823    if((SATflags(v) & IsCNFMask)) {
824      size = SATnumLits(v);
825      plit =(long*) SATfirstLit(v);
826      for(j=0; j<size; j++, plit++) {
827        nv = SATgetNode(*plit);
828        inverted = !(SATisInverted(nv));
829        nv = SATnormalNode(nv);
830        var = SATgetVariable(nv);
831        var->litsCount[inverted]++;
832      }
833      continue;
834    }
835    if(!(SATflags(v) & CoiMask))        continue;
836    /**
837    if(!(SATflags(v) & VisitedMask) && objExist)        continue;
838    **/
839
840    if(SATvalue(v) != 2 && SATlevel(v) == 0)    continue;
841
842    count0 = count1 = SATnFanout(v);
843    if(count0 == 0 && SATleftChild(v) == 2 && SATrightChild(v) == 2) {
844      count0 = 0;
845      count1 = 0;
846    }
847    else if(SATleftChild(v) != 2) {
848      count0 += 2;
849      count1++;
850    }
851    else {
852      count0 += 3;
853      count1 += 3;
854    }
855
856    var = SATgetVariable(v);
857    var->litsCount[0] += count0;
858    var->litsCount[1] += count1;
859
860    sat_ArrayInsert(ordered, v);
861  }
862
863  for(i=0; i<cm->unitLits->num; i++) {
864    v = cm->unitLits->space[i];
865    v = SATnormalNode(v);
866    SATflags(v) |= NewMask;
867  }
868  if(cm->assertion) {
869    for(i=0; i<cm->assertion->num; i++) {
870      v = cm->assertion->space[i];
871      v = SATnormalNode(v);
872      SATflags(v) |= NewMask;
873    }
874  }
875
876  newOrdered = sat_ArrayAlloc((ordered->num) * 2);
877  size = ordered->num;
878  for(i=0; i<size; i++) {
879    v = ordered->space[i];
880    var = SATgetVariable(v);
881    var->scores[0] = var->lastLitsCount[0] = var->litsCount[0];
882    var->scores[1] = var->lastLitsCount[1] = var->litsCount[1];
883
884    if(SATflags(v) & NewMask);
885    else if(var->scores[0] == 0 && var->scores[1] == 0 && !(SATflags(v) & NewMask)) {
886      sat_ArrayInsert(cm->pureLits, (v));
887    }
888    else if(var->scores[0] == 0 && !(SATflags(v) & NewMask)) {
889      sat_ArrayInsert(cm->pureLits, (v));
890    }
891    else if(var->scores[1] == 0 && !(SATflags(v) & NewMask)) {
892      sat_ArrayInsert(cm->pureLits, SATnot(v));
893    }
894    else {
895      sat_ArrayInsert(newOrdered, v);
896      sat_ArrayInsert(newOrdered, (var->scores[0] > var->scores[1]) ? var->scores[0] : var->scores[1]);
897    }
898  }
899
900  for(i=0; i<cm->unitLits->num; i++) {
901    v = cm->unitLits->space[i];
902    v = SATnormalNode(v);
903    SATflags(v) &= ResetNewMask;
904  }
905  if(cm->assertion) {
906    for(i=0; i<cm->assertion->num; i++) {
907      v = cm->assertion->space[i];
908      v = SATnormalNode(v);
909      SATflags(v) &= ResetNewMask;
910    }
911  }
912
913  cm->orderedVariableArray = ordered;
914  size = newOrdered->num;
915  qsort(newOrdered->space, size>>1, sizeof(long)*2, ScoreCompare);
916
917  cm->currentVarPos = 0;
918  ordered->num = 0;
919  for(i=0; i<size; i++) {
920    v = newOrdered->space[i];
921    var = SATgetVariable(v);
922    var->pos = (i>>1);
923    sat_ArrayInsert(ordered, v);
924    i++;
925  }
926
927  sat_ArrayFree(newOrdered);
928
929  /**
930  if(cm->obj && cm->obj->num) {
931    sat_UnmarkTransitiveFaninForArray(
932            cm, cm->obj, VisitedMask, ResetVisitedMask);
933  }
934  **/
935
936  if(cm->option->verbose > 3)
937    sat_PrintScore(cm);
938
939}
940/**Function********************************************************************
941
942  Synopsis    [ Compare score to sort variable array]
943
944  Description [ Compare score to sort variable array]
945
946  SideEffects []
947
948  SeeAlso     []
949
950******************************************************************************/
951static int
952ScoreCompare(
953  const void * node1,
954  const void * node2)
955{
956int v1;
957int v2;
958int s1, s2;
959
960  v1 = *(int *)(node1);
961  v2 = *(int *)(node2);
962  s1 = *((int *)(node1) + 1);
963  s2 = *((int *)(node2) + 1);
964  /**
965  var1 = SatCm->variableArray[SATnodeID(v1)];
966  var2 = SatCm->variableArray[SATnodeID(v2)];
967  s1 = (var1.scores[0] > var1.scores[1]) ? var1.scores[0] : var1.scores[1];
968  s2 = (var2.scores[0] > var2.scores[1]) ? var2.scores[0] : var2.scores[1];
969  **/
970  if(s1 == s2) {
971    return(v1 > v2);
972  }
973  return(s1 < s2);
974}
Note: See TracBrowser for help on using the repository browser.