source: vis_dev/vis-2.3/src/sat/satDebug.c @ 56

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

vis2.3

File size: 22.8 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [satDebug.c]
4
5  PackageName [sat]
6
7  Synopsis    [Routines for various debug 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: satDebug.c,v 1.14 2009/04/11 18:26:37 fabio Exp $";
22
23/*---------------------------------------------------------------------------*/
24/* Constant declarations                                                     */
25/*---------------------------------------------------------------------------*/
26
27/**AutomaticStart*************************************************************/
28
29/*---------------------------------------------------------------------------*/
30/* Static function prototypes                                                */
31/*---------------------------------------------------------------------------*/
32static int numCompareInt(const void *x, const void *y);
33
34
35/**AutomaticEnd***************************************************************/
36
37
38/*---------------------------------------------------------------------------*/
39/* Definition of exported functions                                          */
40/*---------------------------------------------------------------------------*/
41
42
43/**Function********************************************************************
44
45  Synopsis    [ Print node infomation]
46
47  Description [ Print node infomation]
48
49  SideEffects []
50
51  SeeAlso     []
52
53******************************************************************************/
54void
55sat_PrintNode(
56        satManager_t *cm,
57        long v)
58{
59int inverted, i, size;
60long ante, cur, *fan, *plit;
61satVariable_t *var;
62satArray_t *wl;
63
64  inverted = SATisInverted(v);
65  v = SATnormalNode(v);
66  if(SATflags(v) & IsCNFMask) {
67    size = SATnumLits(v);
68    fprintf(cm->stdOut, "CNF %6ld (%4ld) U(%ld)", v, SATnumConflict(v), SATconflictUsage(v));
69    sat_PrintFlag(cm, v);
70    fprintf(cm->stdOut, "    ");
71    for(i=0, plit = (long*)SATfirstLit(v); i<size; i++, plit++) {
72      if(i!=0 && i%5 == 0)
73        fprintf(cm->stdOut, "\n    ");
74      sat_PrintLiteral(cm, *plit);
75    }
76    fprintf(cm->stdOut, "\n");
77  }
78  else if(SATflags(v) & IsBDDMask) {
79  }
80  else {
81    fprintf(cm->stdOut, "AIG ");
82    sat_PrintFlag(cm, SATnormalNode(v));
83    fprintf(cm->stdOut, "    ");
84    sat_PrintNodeAlone(cm, v);
85    sat_PrintNodeAlone(cm, SATleftChild(v));
86    sat_PrintNodeAlone(cm, SATrightChild(v));
87    fprintf(cm->stdOut, "\n");
88    size = SATnFanout(v);
89    fprintf(cm->stdOut, "%4d ", size);
90    for(i=0, fan=SATfanout(v); i<size; i++, fan++) {
91      cur = (*fan) >>1;
92      fprintf(cm->stdOut, "%6ld ", cur);
93    }
94    fprintf(cm->stdOut, "\n");
95
96    fprintf(cm->stdOut, "  canonocal : %ld\n", sat_GetCanonical(cm, v));
97    if(cm->variableArray && SATvalue(v) < 2) {
98      ante = SATante(v);
99      if(SATflags(ante) & IsCNFMask) {
100        fprintf(cm->stdOut, "  ante CNF  : %ld\n", SATante(v));
101      }
102      else{
103        fprintf(cm->stdOut, "  ante      : %ld\n", SATante(v));
104        fprintf(cm->stdOut, "  ante2     : %ld\n", SATante2(v));
105      }
106    }
107
108    if(cm->variableArray) {
109    var = SATgetVariable(v);
110    wl = var->wl[0];
111    if(wl && wl->num) {
112      fprintf(cm->stdOut, "  0 wl : ");
113      for(i=0; i<wl->num; i++) {
114        plit = (long *)(wl->space[i]);
115        if(plit == 0)   continue;
116        fprintf(cm->stdOut, "%ld", (*plit)>>2);
117        while(1) {
118          plit++;
119          if(*plit < 0) break;
120        }
121        fprintf(cm->stdOut, "(%ld) ", -(*plit));
122      }
123      fprintf(cm->stdOut, "\n");
124    }
125    wl = var->wl[1];
126    if(wl && wl->num) {
127      fprintf(cm->stdOut, "  1 wl : ");
128      for(i=0; i<wl->num; i++) {
129        plit = (long *)(wl->space[i]);
130        if(plit == 0)   continue;
131        fprintf(cm->stdOut, "%ld", (*plit)>>2);
132        while(1) {
133          plit++;
134          if(*plit < 0) break;
135        }
136        fprintf(cm->stdOut, "(%ld) ", -(*plit));
137      }
138      fprintf(cm->stdOut, "\n");
139    }
140    }
141  }
142  fflush(cm->stdOut);
143}
144
145/**Function********************************************************************
146
147  Synopsis    [ Print flag infomation]
148
149  Description [ Print flag infomation]
150
151  SideEffects []
152
153  SeeAlso     []
154
155******************************************************************************/
156void
157sat_PrintFlag(satManager_t *cm, long v)
158{
159int flag;
160
161  flag = SATflags(SATnormalNode(v));
162  fprintf(cm->stdOut, "%c%c%c%c%c%c%c%c%c%c%c%c%c%c\n",
163          (flag & CoiMask)           ? 'C' : ' ',
164          (flag & VisitedMask)       ? 'V' : ' ',
165          (flag & NewMask)           ? 'N' : ' ',
166          (flag & InQueueMask)       ? 'Q' : ' ',
167          (flag & ObjMask)           ? 'o' : ' ',
168          (flag & NonobjMask)        ? 'n' : ' ',
169          (flag & IsSystemMask)      ? 'S' : ' ',
170          (flag & IsConflictMask)    ? 'c' : ' ',
171          (flag & InUseMask)         ? 'U' : ' ',
172          (flag & StaticLearnMask)   ? 's' : ' ',
173          (flag & StateBitMask)      ? 'T' : ' ',
174          (flag & IsBlockingMask)    ? 'B' : ' ',
175          (flag & IsFrontierMask)    ? 'F' : ' ',
176          (flag & LeafNodeMask)      ? 'L' : ' ');
177
178}
179
180/**Function********************************************************************
181
182  Synopsis    [ Print node infomation in the form of (id'@level = value)]
183
184  Description [ Print node infomation in the form of (id'@level = value)]
185
186  SideEffects []
187
188  SeeAlso     []
189
190******************************************************************************/
191void
192sat_PrintNodeAlone(satManager_t *cm, long v)
193{
194int value, level, inverted;
195
196  inverted = SATisInverted(v);
197  v = SATnormalNode(v);
198  value = SATvalue(v);
199  level = value>1 ? -1 : (cm->variableArray ? SATlevel(v) : -1);
200  fprintf(cm->stdOut, "%6ld%c@%d=%c%c ",
201          v, inverted ? '\'' : ' ', level,
202          SATgetValueChar(value),
203          (SATflags(v)&ObjMask) ? '*' : ' ');
204}
205
206/**Function********************************************************************
207
208  Synopsis    [ Print literal information.]
209
210  Description [ Print literal information.]
211
212  SideEffects []
213
214  SeeAlso     []
215
216******************************************************************************/
217void
218sat_PrintLiteral(satManager_t *cm, long lit)
219{
220int value, level, inverted;
221long v;
222
223  v = SATgetNode(lit);
224  inverted = SATisInverted(v);
225  v = SATnormalNode(v);
226  value = SATvalue(v);
227  level = value>1 ? -1 : SATlevel(v);
228  fprintf(cm->stdOut, "%6ld%c@%d=%c%c ",
229          v, inverted ? '\'' : ' ', level, SATgetValueChar(value),
230          SATisWL(lit) ? '*' : ' ');
231}
232
233/**Function********************************************************************
234
235  Synopsis    [ Print implication graph ]
236
237  Description [ Print implication graph.]
238
239  SideEffects []
240
241  SeeAlso     []
242
243******************************************************************************/
244void
245sat_PrintImplicationGraph(
246        satManager_t *cm,
247        satLevel_t *d)
248{
249long ante, ante2, v;
250int i;
251satArray_t *implied;
252
253  fprintf(cm->stdOut, "++++++++++++++++++++++++++++++++\n");
254  fprintf(cm->stdOut, "* Level %d %ld->%ld\n",
255                d->level, d->decisionNode, SATvalue(d->decisionNode));
256  fprintf(cm->stdOut, "++++++++++++++++++++++++++++++++\n");
257
258  implied = d->implied;
259  for(i=0; i<implied->num; i++) {
260    v = implied->space[i];
261    ante = SATante(v);
262    if(SATflags(ante) & IsCNFMask) {
263      sat_PrintNodeAlone(cm, v);
264      fprintf(cm->stdOut, "<= %6ld %c(%cCNF)\n",
265              ante, (SATflags(ante) & ObjMask) ? '*' : ' ',
266              (SATflags(ante) & IsConflictMask) ? 'c' : ' ');
267      sat_PrintNode(cm, ante);
268    }
269    else if(SATflags(ante) & IsBDDMask) {
270    }
271    else {
272      sat_PrintNodeAlone(cm, v);
273      fprintf(cm->stdOut, "<= ");
274      sat_PrintNodeAlone(cm, ante);
275      ante2 = SATante2(v);
276      if(ante2)
277        sat_PrintNodeAlone(cm, ante2);
278      fprintf(cm->stdOut, "\n");
279    }
280  }
281  fflush(cm->stdOut);
282}
283
284/**Function********************************************************************
285
286  Synopsis    [ Check flags then is used for conflict analysis. ]
287
288  Description [ Check flags then is used for conflict analysis.
289                After conflict analysis, these flags has to be reset ]
290
291  SideEffects []
292
293  SeeAlso     []
294
295******************************************************************************/
296void
297sat_CheckFlagsOnConflict(satManager_t *cm)
298{
299long i;
300
301  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
302    if(!(SATflags(i) & CoiMask))
303      continue;
304
305    if(SATflags(i) & VisitedMask || SATflags(i) & NewMask) {
306      fprintf(cm->stdOut, "%s ERROR : %ld has flag\n",
307              cm->comment, i);
308      sat_PrintNode(cm, i);
309    }
310  }
311}
312
313/**Function********************************************************************
314
315  Synopsis    [ Print score]
316
317  Description [ Print score]
318
319  SideEffects []
320
321  SeeAlso     []
322
323******************************************************************************/
324void
325sat_PrintScore(satManager_t *cm)
326{
327int i;
328long v;
329satArray_t *ordered;
330satVariable_t *var;
331
332  fprintf(cm->stdOut, "------------Print Score-----------\n");
333  ordered = cm->orderedVariableArray;
334  for(i=0; i<ordered->num; i++) {
335    v = ordered->space[i];
336    var = SATgetVariable(v);
337    fprintf(cm->stdOut, "%5ld : %3d %3d\n", v, var->scores[0], var->scores[1]);
338  }
339  fflush(cm->stdOut);
340}
341
342
343/**Function********************************************************************
344
345  Synopsis    [ Print dot file of implication graph]
346
347  Description [ Print dot file of implication graph ]
348
349  SideEffects []
350
351  SeeAlso     []
352
353******************************************************************************/
354void
355sat_PrintDotForConflict(
356        satManager_t *cm,
357        satLevel_t *d,
358        long conflict,
359        int includePreviousLevel)
360{
361satArray_t *root;
362long left, right, nv;
363int inverted, size, value, i;
364long *plit;
365satOption_t *option;
366
367  root = sat_ArrayAlloc(8);
368
369  conflict = d->conflict;
370  inverted = SATisInverted(conflict);
371  conflict = SATnormalNode(conflict);
372
373  option = cm->option;
374  if(SATflags(conflict) & IsCNFMask) {
375    size = SATnumLits(conflict);
376    for(i=0, plit=(long*)SATfirstLit(conflict); i<size; i++, plit++) {
377      nv = SATgetNode(*plit);
378      if(d->level == SATlevel(nv))
379        sat_ArrayInsert(root, nv);
380    }
381  }
382  else {
383    value = SATvalue(conflict);
384    if(value == 1) {
385      if(d->level == SATlevel(conflict))
386        sat_ArrayInsert(root, conflict);
387
388      left = SATleftChild(conflict);
389      inverted = SATisInverted(left);
390      left = SATnormalNode(left);
391      value = SATvalue(left) ^ inverted;
392      if(value == 0) {
393        if(d->level == SATlevel(left))
394          sat_ArrayInsert(root, left);
395      }
396      else {
397        right = SATrightChild(conflict);
398        inverted = SATisInverted(right);
399        right = SATnormalNode(right);
400        value = SATvalue(right) ^ inverted;
401        if(value == 0) {
402          if(d->level == SATlevel(right))
403            sat_ArrayInsert(root, right);
404        }
405      }
406    }
407    else if(value == 0) {
408      left = SATleftChild(conflict);
409      right = SATrightChild(conflict);
410      if(d->level == SATlevel(conflict))
411        sat_ArrayInsert(root, conflict);
412      if(d->level == SATlevel(left))
413        sat_ArrayInsert(root, left);
414      if(d->level == SATlevel(right))
415        sat_ArrayInsert(root, right);
416    }
417  }
418
419  sat_PrintDotForImplicationGraph(cm, d, root, includePreviousLevel);
420  sat_ArrayFree(root);
421}
422
423/**Function********************************************************************
424
425  Synopsis    [ Print dot file of whole implication graph]
426
427  Description [ Print dot file of whole implication graph ]
428
429  SideEffects []
430
431  SeeAlso     []
432
433******************************************************************************/
434void
435sat_PrintDotForWholeGraph(
436        satManager_t *cm,
437        satLevel_t *d,
438        int includePreviousLevel)
439{
440satArray_t *root, *implied;
441int v, i;
442
443  root = sat_ArrayAlloc(8);
444  implied = d->implied;
445  for(i=implied->num-1; i>=0; i--) {
446    v = implied->space[i];
447    sat_ArrayInsert(root, v);
448  }
449  sat_PrintDotForImplicationGraph(cm, d, root, includePreviousLevel);
450  sat_ArrayFree(root);
451}
452/**Function********************************************************************
453
454  Synopsis    [ Print dot file of implication graph]
455
456  Description [ Print dot file of implication graph ]
457
458  SideEffects []
459
460  SeeAlso     []
461
462******************************************************************************/
463void
464sat_PrintDotForImplicationGraph(
465        satManager_t *cm,
466        satLevel_t *d,
467        satArray_t *root,
468        int includePreviousLevel)
469{
470char name[1024];
471long v, nv, *plit, lit;
472int i, j, size;
473int inverted;
474long ante, ante2;
475st_table *table;
476FILE *fp;
477satArray_t *implied;
478
479
480  for(i=0; i<root->num; i++) {
481    v = root->space[i];
482    v  = SATnormalNode(v);
483    SATflags(v) |= VisitedMask;
484  }
485
486  sprintf(name, "%d_%ld_%d_%d.dot",
487          d->level, d->decisionNode, cm->each->nDecisions, includePreviousLevel);
488  fp = fopen(name, "w");
489
490  fprintf(fp, "digraph \"AndInv\" {\n  rotate=90;\n");
491  fprintf(fp, "  margin=0.5;\n  label=\"AndInv\";\n");
492  fprintf(fp, "  size=\"10,7.5\";\n  ratio=\"fill\";\n");
493
494  table = st_init_table(st_numcmp, st_numhash);
495  implied = d->implied;
496  for(i=implied->num-1; i>=0; i--) {
497    v = implied->space[i];
498    if(!(SATflags(v) & VisitedMask)) continue;
499    if((SATflags(v) & NewMask)) continue;
500
501    st_insert(table, (char *)(long)v, (char *)(long)v);
502
503    ante = SATante(v);
504    if(SATflags(ante) & IsCNFMask) {
505      size = SATnumLits(ante);
506      for(j=0, plit=(long *)SATfirstLit(ante); j<size; j++) {
507        lit = plit[j];
508        nv = SATgetNode(lit);
509        inverted = SATisInverted(nv);
510        nv = SATnormalNode(nv);
511        if(nv == v)     continue;
512
513        st_insert(table, (char *)nv, (char *)nv);
514        if(SATlevel(nv) == d->level) {
515          fprintf(fp,"%ld.%d -> %ld.%d [color = red];\n",
516                  nv, SATlevel(nv), v, SATlevel(v));
517          SATflags(nv) |= VisitedMask;
518        }
519        else if(includePreviousLevel) {
520          fprintf(fp,"%ld.%d -> %ld.%d [color = black];\n",
521                  nv, SATlevel(nv), v, SATlevel(v));
522        }
523      }
524    }
525    else {
526      fprintf(fp,"%ld.%d  [label=\"%ld.%d \"];\n", v, SATlevel(v), v, SATlevel(v));
527      ante2 = SATnormalNode(SATante2(v));
528      if(ante2) {
529        st_insert(table, (char *)ante2, (char *)ante2);
530        if(SATlevel(ante2) == d->level) {
531          fprintf(fp,"%ld.%d -> %ld.%d [color = red];\n", ante2, SATlevel(ante2), v, SATlevel(v));
532          SATflags(ante2) |= VisitedMask;
533        }
534        else if(includePreviousLevel && SATlevel(ante2)>=0) {
535          fprintf(fp,"%ld.%d -> %ld.%d [color = black];\n", ante2, SATlevel(ante2), v, SATlevel(v));
536        }
537      }
538
539      if(ante) {
540        st_insert(table, (char *)ante, (char *)ante);
541        if(SATlevel(ante) == d->level) {
542          fprintf(fp,"%ld.%d -> %ld.%d [color = red];\n", ante, SATlevel(ante), v, SATlevel(v));
543          SATflags(ante) |= VisitedMask;
544        }
545        else if(includePreviousLevel && SATlevel(ante)>=0) {
546          fprintf(fp,"%ld.%d -> %ld.%d [color = black];\n", ante, SATlevel(ante), v, SATlevel(v));
547        }
548      }
549    }
550    SATflags(v) |= NewMask;
551  }
552  fprintf(fp, "}\n");
553  fclose(fp);
554
555  for(i=implied->num-1; i>=0; i--) {
556    v = implied->space[i];
557    SATflags(v) &= ResetNewVisitedMask;
558  }
559  for(i=0; i<root->num; i++) {
560    v = root->space[i];
561    SATflags(v) &= ResetVisitedMask;
562  }
563
564  st_free_table(table);
565
566}
567
568/**Function********************************************************************
569
570  Synopsis    [ Check whether the given conflict clauses are
571                objective independent ]
572
573  Description [ Check whether the given conflict clauses are
574                objective independent ]
575
576  SideEffects []
577
578  SeeAlso     []
579
580******************************************************************************/
581void
582sat_CheckNonobjConflictClause(
583        satManager_t *cm,
584        long v)
585{
586int i, size, inverted;
587long *plit, nv;
588satLevel_t *d;
589
590  d = 0;
591  size = SATnumLits(v);
592  for(i=0, plit = (long*)SATfirstLit(v); i<size; i++, plit++) {
593    nv = SATgetNode(*plit);
594    inverted = SATisInverted(nv);
595    nv = SATnormalNode(nv);
596
597    d = sat_AllocLevel(cm);
598    d->decisionNode = nv;
599
600    SATvalue(nv) = inverted;
601    SATmakeImplied(nv, d);
602
603    sat_Enqueue(cm->queue, nv);
604    SATflags(nv) |= InQueueMask;
605
606    sat_ImplicationMain(cm, d);
607    if(d->conflict)     break;
608  }
609
610  if(d->conflict == 0) {
611    fprintf(cm->stdOut, "%s ERROR : %ld does not result in conflict\n",
612            cm->comment, v);
613    sat_PrintNode(cm, v);
614  }
615  sat_Backtrack(cm, -1);
616}
617
618/**Function********************************************************************
619
620  Synopsis    [ Check whether the given conflict clauses are
621                objective independent ]
622
623  Description [ Check whether the given conflict clauses are
624                objective independent ]
625
626  SideEffects []
627
628  SeeAlso     []
629
630******************************************************************************/
631void
632sat_CheckNonobjUnitClause(
633        satManager_t *cm)
634{
635int v, i;
636int inverted;
637satLevel_t *d;
638satArray_t *arr;
639
640  arr = cm->nonobjUnitLitArray;
641
642  for(i=0; i<arr->num; i++) {
643    v = arr->space[i];
644    inverted = SATisInverted(v);
645    v = SATnormalNode(v);
646
647    d = sat_AllocLevel(cm);
648    d->decisionNode = v;
649
650    SATvalue(v) = inverted;
651    SATmakeImplied(v, d);
652
653    sat_Enqueue(cm->queue, v);
654    SATflags(v) |= InQueueMask;
655
656    sat_ImplicationMain(cm, d);
657    if(d->conflict == 0) {
658      fprintf(cm->stdOut, "%s ERROR : %d unit literal does not result in conflict\n",
659            cm->comment, v);
660    }
661    sat_Backtrack(cm, -1);
662
663  }
664}
665
666/**Function********************************************************************
667
668  Synopsis    [ Check initial condition of SAT solving ]
669
670  Description [ Check initial condition of SAT solving ]
671
672  SideEffects []
673
674  SeeAlso     []
675
676******************************************************************************/
677void
678sat_CheckInitialCondition(
679        satManager_t *cm)
680{
681long i;
682
683  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
684    if(!(SATflags(i) & CoiMask))
685      continue;
686
687    if(SATvalue(i) != 2) {
688      fprintf(cm->stdOut, "%s ERROR : %ld has value %ld\n",
689              cm->comment, i, SATvalue(i));
690    }
691    if(SATflags(i) & VisitedMask || SATflags(i) & NewMask) {
692      fprintf(cm->stdOut, "%s ERROR : %ld has flag\n",
693              cm->comment, i);
694      sat_PrintNode(cm, i);
695    }
696  }
697}
698
699/**Function********************************************************************
700
701  Synopsis    [ Check whether inverse assignment of literals
702                in conflict clause create conflict]
703
704  Description [ Check whether inverse assignment of literals
705                in conflict clause create conflict]
706
707  SideEffects []
708
709  SeeAlso     []
710
711******************************************************************************/
712void
713sat_CheckConflictClause(
714        satManager_t *cm,
715        satArray_t *clauseArray)
716{
717satArray_t *decisionArray;
718satLevel_t *d;
719int i, value, inverted;
720long v;
721int conflictFlag, tvalue;
722
723  decisionArray = sat_ArrayAlloc(cm->currentDecision);
724  for(i=1; i<=cm->currentDecision; i++) {
725    v = cm->decisionHead[i].decisionNode;
726    value = SATvalue(v);
727    sat_ArrayInsert(decisionArray, v^(!value));
728  }
729
730  sat_Backtrack(cm, 0);
731
732  conflictFlag = 0;
733  for(i=0; i<clauseArray->num; i++) {
734    v = clauseArray->space[i];
735    inverted = SATisInverted(v);
736    v = SATnormalNode(v);
737
738    d = sat_AllocLevel(cm);
739    d->decisionNode = v;
740
741    value = !inverted;
742    tvalue = SATvalue(v);
743    if(tvalue < 2 && tvalue !=  value) {
744      fprintf(cm->stdOut, "ERROR : Early conflict condition detect\n");
745      break;
746    }
747    SATvalue(v) = value;
748    SATmakeImplied(v, d);
749
750    sat_Enqueue(cm->queue, v);
751    SATflags(v) |= InQueueMask;
752
753    sat_ImplicationMain(cm, d);
754
755    if(d->conflict) {
756      conflictFlag = 1;
757      break;
758    }
759  }
760
761  if(conflictFlag == 0) {
762    fprintf(cm->stdOut, "ERROR : Wrong conflict clause\n");
763    sat_PrintClauseArray(cm, clauseArray);
764  }
765
766  sat_Backtrack(cm, 0);
767
768  conflictFlag = 0;
769  for(i=0; i<decisionArray->num; i++) {
770    v = decisionArray->space[i];
771    inverted = SATisInverted(v);
772    v = SATnormalNode(v);
773
774    d = sat_AllocLevel(cm);
775    d->decisionNode = v;
776
777    value = !inverted;
778    SATvalue(v) = value;
779    SATmakeImplied(v, d);
780
781    sat_Enqueue(cm->queue, v);
782    SATflags(v) |= InQueueMask;
783
784    sat_ImplicationMain(cm, d);
785    if(d->conflict) {
786      conflictFlag = 1;
787    }
788  }
789  if(conflictFlag == 0) {
790    fprintf(cm->stdOut, "ERROR : Can't produce conflict\n");
791    exit(0);
792  }
793}
794
795/**Function********************************************************************
796
797  Synopsis    [ Print clause array ]
798
799  Description [ Print clause array ]
800
801  SideEffects []
802
803  SeeAlso     []
804
805******************************************************************************/
806void
807sat_PrintClauseArray(
808        satManager_t *cm,
809        satArray_t *clauseArray)
810{
811int i, inverted;
812long v;
813
814  fprintf(cm->stdOut, "    ");
815  for(i=0; i<clauseArray->num; i++) {
816    v = clauseArray->space[i];
817    inverted = SATisInverted(v);
818    v = SATnormalNode(v);
819    if(i!=0 && i%5 == 0)
820      fprintf(cm->stdOut, "\n    ");
821    sat_PrintNodeAlone(cm, v);
822  }
823  fprintf(cm->stdOut, "\n");
824  fflush(cm->stdOut);
825}
826
827/**Function********************************************************************
828
829  Synopsis    [ Print profile of the number of conflict on each clause]
830
831  Description [ Print profile of the number of conflict on each clause]
832
833  SideEffects []
834
835  SeeAlso     []
836
837******************************************************************************/
838void
839sat_PrintProfileForNumConflict(satManager_t *cm)
840{
841char filename[1024];
842FILE *fout;
843int i, index;
844satArray_t *arr;
845long count;
846long total, part;
847long v;
848long maxValue;
849
850
851  sprintf(filename, "nConflict.dat");
852  fout = fopen(filename, "w");
853  index = 1;
854  maxValue = 0;
855  arr = sat_ArrayAlloc(1024);
856  for(v=satNodeSize; v<cm->nodesArraySize; v+=satNodeSize) {
857    if(!(SATflags(v) & IsCNFMask))      continue;
858    if(SATnumConflict(v) == 0)  continue;
859    if(SATnumConflict(v) > maxValue)
860      maxValue = SATnumConflict(v);
861    sat_ArrayInsert(arr, SATnumConflict(v));
862  }
863
864  qsort(arr->space, arr->num, sizeof(int), numCompareInt);
865  total = 0;
866  part = 0;
867  for(i=0; i<arr->num; i++) {
868    count = arr->space[i];
869    if(count == 0)      continue;
870    total += count;
871    if(count > 1) {
872      part += count;
873    }
874    fprintf(fout, "%d %ld\n", i, count);
875  }
876  index = i;
877  sat_ArrayFree(arr);
878  fclose(fout);
879
880
881  sprintf(filename, "nConflict.gp");
882  fout = fopen(filename, "w");
883  fprintf(fout, "set xlabel \"Conflict Index\"\n");
884  fprintf(fout, "set ylabel \"Number of Conflicting %ld/%ld\"\n", part, total);
885  fprintf(fout, "set nokey\n");
886  fprintf(fout, "set size square 0.8,1\n");
887  fprintf(fout, "set xrange [0:%d]\n", index+1);
888  fprintf(fout, "set yrange [0:%ld]\n", maxValue+1);
889  fprintf(fout, "set grid\n");
890  fprintf(fout, "set border 3 linewidth 0.5\n");
891  fprintf(fout, "set xtics nomirror\n");
892  fprintf(fout, "set ytics nomirror\n");
893  fprintf(fout, "set mxtics 2\n");
894  fprintf(fout, "set mytics 2\n");
895  fprintf(fout, "set pointsize 2\n");
896  fprintf(fout, "set terminal postscript eps enhanced color solid \"Times-Roman\" 24\n");
897  fprintf(fout, "set output \"nConflict.eps\"\n");
898  fprintf(fout, "plot \"nConflict.dat\" using 1:2 with line linetype 3\n");
899  fclose(fout);
900}
901
902/**Function********************************************************************
903
904  Synopsis    [ Compare integer number]
905
906  Description [ Compare integer number]
907
908  SideEffects []
909
910  SeeAlso     []
911
912******************************************************************************/
913static int
914numCompareInt(const void *x, const void *y)
915{
916long n1, n2;
917
918  n1 = *(int *)x;
919  n2 = *(int *)y;
920  return(n1 > n2);
921}
Note: See TracBrowser for help on using the repository browser.