#include "satInt.h"
Include dependency graph for satDebug.c:
Go to the source code of this file.
Functions | |
| static int | numCompareInt (const void *x, const void *y) |
| void | sat_PrintNode (satManager_t *cm, long v) |
| void | sat_PrintFlag (satManager_t *cm, long v) |
| void | sat_PrintNodeAlone (satManager_t *cm, long v) |
| void | sat_PrintLiteral (satManager_t *cm, long lit) |
| void | sat_PrintImplicationGraph (satManager_t *cm, satLevel_t *d) |
| void | sat_CheckFlagsOnConflict (satManager_t *cm) |
| void | sat_PrintScore (satManager_t *cm) |
| void | sat_PrintDotForConflict (satManager_t *cm, satLevel_t *d, long conflict, int includePreviousLevel) |
| void | sat_PrintDotForWholeGraph (satManager_t *cm, satLevel_t *d, int includePreviousLevel) |
| void | sat_PrintDotForImplicationGraph (satManager_t *cm, satLevel_t *d, satArray_t *root, int includePreviousLevel) |
| void | sat_CheckNonobjConflictClause (satManager_t *cm, long v) |
| void | sat_CheckNonobjUnitClause (satManager_t *cm) |
| void | sat_CheckInitialCondition (satManager_t *cm) |
| void | sat_CheckConflictClause (satManager_t *cm, satArray_t *clauseArray) |
| void | sat_PrintClauseArray (satManager_t *cm, satArray_t *clauseArray) |
| void | sat_PrintProfileForNumConflict (satManager_t *cm) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: satDebug.c,v 1.14 2009/04/11 18:26:37 fabio Exp $" |
Function Documentation
| static int numCompareInt | ( | const void * | x, |
| const void * | y | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [ Compare integer number]
Description [ Compare integer number]
SideEffects []
SeeAlso []
Definition at line 914 of file satDebug.c.
{
long n1, n2;
n1 = *(int *)x;
n2 = *(int *)y;
return(n1 > n2);
}
Here is the caller graph for this function:
| void sat_CheckConflictClause | ( | satManager_t * | cm, |
| satArray_t * | clauseArray | ||
| ) |
Function********************************************************************
Synopsis [ Check whether inverse assignment of literals in conflict clause create conflict]
Description [ Check whether inverse assignment of literals in conflict clause create conflict]
SideEffects []
SeeAlso []
Definition at line 713 of file satDebug.c.
{
satArray_t *decisionArray;
satLevel_t *d;
int i, value, inverted;
long v;
int conflictFlag, tvalue;
decisionArray = sat_ArrayAlloc(cm->currentDecision);
for(i=1; i<=cm->currentDecision; i++) {
v = cm->decisionHead[i].decisionNode;
value = SATvalue(v);
sat_ArrayInsert(decisionArray, v^(!value));
}
sat_Backtrack(cm, 0);
conflictFlag = 0;
for(i=0; i<clauseArray->num; i++) {
v = clauseArray->space[i];
inverted = SATisInverted(v);
v = SATnormalNode(v);
d = sat_AllocLevel(cm);
d->decisionNode = v;
value = !inverted;
tvalue = SATvalue(v);
if(tvalue < 2 && tvalue != value) {
fprintf(cm->stdOut, "ERROR : Early conflict condition detect\n");
break;
}
SATvalue(v) = value;
SATmakeImplied(v, d);
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
sat_ImplicationMain(cm, d);
if(d->conflict) {
conflictFlag = 1;
break;
}
}
if(conflictFlag == 0) {
fprintf(cm->stdOut, "ERROR : Wrong conflict clause\n");
sat_PrintClauseArray(cm, clauseArray);
}
sat_Backtrack(cm, 0);
conflictFlag = 0;
for(i=0; i<decisionArray->num; i++) {
v = decisionArray->space[i];
inverted = SATisInverted(v);
v = SATnormalNode(v);
d = sat_AllocLevel(cm);
d->decisionNode = v;
value = !inverted;
SATvalue(v) = value;
SATmakeImplied(v, d);
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
sat_ImplicationMain(cm, d);
if(d->conflict) {
conflictFlag = 1;
}
}
if(conflictFlag == 0) {
fprintf(cm->stdOut, "ERROR : Can't produce conflict\n");
exit(0);
}
}
Here is the call graph for this function:
| void sat_CheckFlagsOnConflict | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [ Check flags then is used for conflict analysis. ]
Description [ Check flags then is used for conflict analysis. After conflict analysis, these flags has to be reset ]
SideEffects []
SeeAlso []
Definition at line 297 of file satDebug.c.
{
long i;
for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
if(!(SATflags(i) & CoiMask))
continue;
if(SATflags(i) & VisitedMask || SATflags(i) & NewMask) {
fprintf(cm->stdOut, "%s ERROR : %ld has flag\n",
cm->comment, i);
sat_PrintNode(cm, i);
}
}
}
Here is the call graph for this function:
| void sat_CheckInitialCondition | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [ Check initial condition of SAT solving ]
Description [ Check initial condition of SAT solving ]
SideEffects []
SeeAlso []
Definition at line 678 of file satDebug.c.
{
long i;
for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
if(!(SATflags(i) & CoiMask))
continue;
if(SATvalue(i) != 2) {
fprintf(cm->stdOut, "%s ERROR : %ld has value %ld\n",
cm->comment, i, SATvalue(i));
}
if(SATflags(i) & VisitedMask || SATflags(i) & NewMask) {
fprintf(cm->stdOut, "%s ERROR : %ld has flag\n",
cm->comment, i);
sat_PrintNode(cm, i);
}
}
}
Here is the call graph for this function:
| void sat_CheckNonobjConflictClause | ( | satManager_t * | cm, |
| long | v | ||
| ) |
Function********************************************************************
Synopsis [ Check whether the given conflict clauses are objective independent ]
Description [ Check whether the given conflict clauses are objective independent ]
SideEffects []
SeeAlso []
Definition at line 582 of file satDebug.c.
{
int i, size, inverted;
long *plit, nv;
satLevel_t *d;
d = 0;
size = SATnumLits(v);
for(i=0, plit = (long*)SATfirstLit(v); i<size; i++, plit++) {
nv = SATgetNode(*plit);
inverted = SATisInverted(nv);
nv = SATnormalNode(nv);
d = sat_AllocLevel(cm);
d->decisionNode = nv;
SATvalue(nv) = inverted;
SATmakeImplied(nv, d);
sat_Enqueue(cm->queue, nv);
SATflags(nv) |= InQueueMask;
sat_ImplicationMain(cm, d);
if(d->conflict) break;
}
if(d->conflict == 0) {
fprintf(cm->stdOut, "%s ERROR : %ld does not result in conflict\n",
cm->comment, v);
sat_PrintNode(cm, v);
}
sat_Backtrack(cm, -1);
}
Here is the call graph for this function:
| void sat_CheckNonobjUnitClause | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [ Check whether the given conflict clauses are objective independent ]
Description [ Check whether the given conflict clauses are objective independent ]
SideEffects []
SeeAlso []
Definition at line 632 of file satDebug.c.
{
int v, i;
int inverted;
satLevel_t *d;
satArray_t *arr;
arr = cm->nonobjUnitLitArray;
for(i=0; i<arr->num; i++) {
v = arr->space[i];
inverted = SATisInverted(v);
v = SATnormalNode(v);
d = sat_AllocLevel(cm);
d->decisionNode = v;
SATvalue(v) = inverted;
SATmakeImplied(v, d);
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
sat_ImplicationMain(cm, d);
if(d->conflict == 0) {
fprintf(cm->stdOut, "%s ERROR : %d unit literal does not result in conflict\n",
cm->comment, v);
}
sat_Backtrack(cm, -1);
}
}
Here is the call graph for this function:
| void sat_PrintClauseArray | ( | satManager_t * | cm, |
| satArray_t * | clauseArray | ||
| ) |
Function********************************************************************
Synopsis [ Print clause array ]
Description [ Print clause array ]
SideEffects []
SeeAlso []
Definition at line 807 of file satDebug.c.
{
int i, inverted;
long v;
fprintf(cm->stdOut, " ");
for(i=0; i<clauseArray->num; i++) {
v = clauseArray->space[i];
inverted = SATisInverted(v);
v = SATnormalNode(v);
if(i!=0 && i%5 == 0)
fprintf(cm->stdOut, "\n ");
sat_PrintNodeAlone(cm, v);
}
fprintf(cm->stdOut, "\n");
fflush(cm->stdOut);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_PrintDotForConflict | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | conflict, | ||
| int | includePreviousLevel | ||
| ) |
Function********************************************************************
Synopsis [ Print dot file of implication graph]
Description [ Print dot file of implication graph ]
SideEffects []
SeeAlso []
Definition at line 355 of file satDebug.c.
{
satArray_t *root;
long left, right, nv;
int inverted, size, value, i;
long *plit;
satOption_t *option;
root = sat_ArrayAlloc(8);
conflict = d->conflict;
inverted = SATisInverted(conflict);
conflict = SATnormalNode(conflict);
option = cm->option;
if(SATflags(conflict) & IsCNFMask) {
size = SATnumLits(conflict);
for(i=0, plit=(long*)SATfirstLit(conflict); i<size; i++, plit++) {
nv = SATgetNode(*plit);
if(d->level == SATlevel(nv))
sat_ArrayInsert(root, nv);
}
}
else {
value = SATvalue(conflict);
if(value == 1) {
if(d->level == SATlevel(conflict))
sat_ArrayInsert(root, conflict);
left = SATleftChild(conflict);
inverted = SATisInverted(left);
left = SATnormalNode(left);
value = SATvalue(left) ^ inverted;
if(value == 0) {
if(d->level == SATlevel(left))
sat_ArrayInsert(root, left);
}
else {
right = SATrightChild(conflict);
inverted = SATisInverted(right);
right = SATnormalNode(right);
value = SATvalue(right) ^ inverted;
if(value == 0) {
if(d->level == SATlevel(right))
sat_ArrayInsert(root, right);
}
}
}
else if(value == 0) {
left = SATleftChild(conflict);
right = SATrightChild(conflict);
if(d->level == SATlevel(conflict))
sat_ArrayInsert(root, conflict);
if(d->level == SATlevel(left))
sat_ArrayInsert(root, left);
if(d->level == SATlevel(right))
sat_ArrayInsert(root, right);
}
}
sat_PrintDotForImplicationGraph(cm, d, root, includePreviousLevel);
sat_ArrayFree(root);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_PrintDotForImplicationGraph | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| satArray_t * | root, | ||
| int | includePreviousLevel | ||
| ) |
Function********************************************************************
Synopsis [ Print dot file of implication graph]
Description [ Print dot file of implication graph ]
SideEffects []
SeeAlso []
Definition at line 464 of file satDebug.c.
{
char name[1024];
long v, nv, *plit, lit;
int i, j, size;
int inverted;
long ante, ante2;
st_table *table;
FILE *fp;
satArray_t *implied;
for(i=0; i<root->num; i++) {
v = root->space[i];
v = SATnormalNode(v);
SATflags(v) |= VisitedMask;
}
sprintf(name, "%d_%ld_%d_%d.dot",
d->level, d->decisionNode, cm->each->nDecisions, includePreviousLevel);
fp = fopen(name, "w");
fprintf(fp, "digraph \"AndInv\" {\n rotate=90;\n");
fprintf(fp, " margin=0.5;\n label=\"AndInv\";\n");
fprintf(fp, " size=\"10,7.5\";\n ratio=\"fill\";\n");
table = st_init_table(st_numcmp, st_numhash);
implied = d->implied;
for(i=implied->num-1; i>=0; i--) {
v = implied->space[i];
if(!(SATflags(v) & VisitedMask)) continue;
if((SATflags(v) & NewMask)) continue;
st_insert(table, (char *)(long)v, (char *)(long)v);
ante = SATante(v);
if(SATflags(ante) & IsCNFMask) {
size = SATnumLits(ante);
for(j=0, plit=(long *)SATfirstLit(ante); j<size; j++) {
lit = plit[j];
nv = SATgetNode(lit);
inverted = SATisInverted(nv);
nv = SATnormalNode(nv);
if(nv == v) continue;
st_insert(table, (char *)nv, (char *)nv);
if(SATlevel(nv) == d->level) {
fprintf(fp,"%ld.%d -> %ld.%d [color = red];\n",
nv, SATlevel(nv), v, SATlevel(v));
SATflags(nv) |= VisitedMask;
}
else if(includePreviousLevel) {
fprintf(fp,"%ld.%d -> %ld.%d [color = black];\n",
nv, SATlevel(nv), v, SATlevel(v));
}
}
}
else {
fprintf(fp,"%ld.%d [label=\"%ld.%d \"];\n", v, SATlevel(v), v, SATlevel(v));
ante2 = SATnormalNode(SATante2(v));
if(ante2) {
st_insert(table, (char *)ante2, (char *)ante2);
if(SATlevel(ante2) == d->level) {
fprintf(fp,"%ld.%d -> %ld.%d [color = red];\n", ante2, SATlevel(ante2), v, SATlevel(v));
SATflags(ante2) |= VisitedMask;
}
else if(includePreviousLevel && SATlevel(ante2)>=0) {
fprintf(fp,"%ld.%d -> %ld.%d [color = black];\n", ante2, SATlevel(ante2), v, SATlevel(v));
}
}
if(ante) {
st_insert(table, (char *)ante, (char *)ante);
if(SATlevel(ante) == d->level) {
fprintf(fp,"%ld.%d -> %ld.%d [color = red];\n", ante, SATlevel(ante), v, SATlevel(v));
SATflags(ante) |= VisitedMask;
}
else if(includePreviousLevel && SATlevel(ante)>=0) {
fprintf(fp,"%ld.%d -> %ld.%d [color = black];\n", ante, SATlevel(ante), v, SATlevel(v));
}
}
}
SATflags(v) |= NewMask;
}
fprintf(fp, "}\n");
fclose(fp);
for(i=implied->num-1; i>=0; i--) {
v = implied->space[i];
SATflags(v) &= ResetNewVisitedMask;
}
for(i=0; i<root->num; i++) {
v = root->space[i];
SATflags(v) &= ResetVisitedMask;
}
st_free_table(table);
}
Here is the caller graph for this function:
| void sat_PrintDotForWholeGraph | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| int | includePreviousLevel | ||
| ) |
Function********************************************************************
Synopsis [ Print dot file of whole implication graph]
Description [ Print dot file of whole implication graph ]
SideEffects []
SeeAlso []
Definition at line 435 of file satDebug.c.
{
satArray_t *root, *implied;
int v, i;
root = sat_ArrayAlloc(8);
implied = d->implied;
for(i=implied->num-1; i>=0; i--) {
v = implied->space[i];
sat_ArrayInsert(root, v);
}
sat_PrintDotForImplicationGraph(cm, d, root, includePreviousLevel);
sat_ArrayFree(root);
}
Here is the call graph for this function:
| void sat_PrintFlag | ( | satManager_t * | cm, |
| long | v | ||
| ) |
Function********************************************************************
Synopsis [ Print flag infomation]
Description [ Print flag infomation]
SideEffects []
SeeAlso []
Definition at line 157 of file satDebug.c.
{
int flag;
flag = SATflags(SATnormalNode(v));
fprintf(cm->stdOut, "%c%c%c%c%c%c%c%c%c%c%c%c%c%c\n",
(flag & CoiMask) ? 'C' : ' ',
(flag & VisitedMask) ? 'V' : ' ',
(flag & NewMask) ? 'N' : ' ',
(flag & InQueueMask) ? 'Q' : ' ',
(flag & ObjMask) ? 'o' : ' ',
(flag & NonobjMask) ? 'n' : ' ',
(flag & IsSystemMask) ? 'S' : ' ',
(flag & IsConflictMask) ? 'c' : ' ',
(flag & InUseMask) ? 'U' : ' ',
(flag & StaticLearnMask) ? 's' : ' ',
(flag & StateBitMask) ? 'T' : ' ',
(flag & IsBlockingMask) ? 'B' : ' ',
(flag & IsFrontierMask) ? 'F' : ' ',
(flag & LeafNodeMask) ? 'L' : ' ');
}
Here is the caller graph for this function:
| void sat_PrintImplicationGraph | ( | satManager_t * | cm, |
| satLevel_t * | d | ||
| ) |
Function********************************************************************
Synopsis [ Print implication graph ]
Description [ Print implication graph.]
SideEffects []
SeeAlso []
Definition at line 245 of file satDebug.c.
{
long ante, ante2, v;
int i;
satArray_t *implied;
fprintf(cm->stdOut, "++++++++++++++++++++++++++++++++\n");
fprintf(cm->stdOut, "* Level %d %ld->%ld\n",
d->level, d->decisionNode, SATvalue(d->decisionNode));
fprintf(cm->stdOut, "++++++++++++++++++++++++++++++++\n");
implied = d->implied;
for(i=0; i<implied->num; i++) {
v = implied->space[i];
ante = SATante(v);
if(SATflags(ante) & IsCNFMask) {
sat_PrintNodeAlone(cm, v);
fprintf(cm->stdOut, "<= %6ld %c(%cCNF)\n",
ante, (SATflags(ante) & ObjMask) ? '*' : ' ',
(SATflags(ante) & IsConflictMask) ? 'c' : ' ');
sat_PrintNode(cm, ante);
}
else if(SATflags(ante) & IsBDDMask) {
}
else {
sat_PrintNodeAlone(cm, v);
fprintf(cm->stdOut, "<= ");
sat_PrintNodeAlone(cm, ante);
ante2 = SATante2(v);
if(ante2)
sat_PrintNodeAlone(cm, ante2);
fprintf(cm->stdOut, "\n");
}
}
fflush(cm->stdOut);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_PrintLiteral | ( | satManager_t * | cm, |
| long | lit | ||
| ) |
Function********************************************************************
Synopsis [ Print literal information.]
Description [ Print literal information.]
SideEffects []
SeeAlso []
Definition at line 218 of file satDebug.c.
{
int value, level, inverted;
long v;
v = SATgetNode(lit);
inverted = SATisInverted(v);
v = SATnormalNode(v);
value = SATvalue(v);
level = value>1 ? -1 : SATlevel(v);
fprintf(cm->stdOut, "%6ld%c@%d=%c%c ",
v, inverted ? '\'' : ' ', level, SATgetValueChar(value),
SATisWL(lit) ? '*' : ' ');
}
Here is the caller graph for this function:
| void sat_PrintNode | ( | satManager_t * | cm, |
| long | v | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [ Print node infomation]
Description [ Print node infomation]
SideEffects []
SeeAlso []
Definition at line 55 of file satDebug.c.
{
int inverted, i, size;
long ante, cur, *fan, *plit;
satVariable_t *var;
satArray_t *wl;
inverted = SATisInverted(v);
v = SATnormalNode(v);
if(SATflags(v) & IsCNFMask) {
size = SATnumLits(v);
fprintf(cm->stdOut, "CNF %6ld (%4ld) U(%ld)", v, SATnumConflict(v), SATconflictUsage(v));
sat_PrintFlag(cm, v);
fprintf(cm->stdOut, " ");
for(i=0, plit = (long*)SATfirstLit(v); i<size; i++, plit++) {
if(i!=0 && i%5 == 0)
fprintf(cm->stdOut, "\n ");
sat_PrintLiteral(cm, *plit);
}
fprintf(cm->stdOut, "\n");
}
else if(SATflags(v) & IsBDDMask) {
}
else {
fprintf(cm->stdOut, "AIG ");
sat_PrintFlag(cm, SATnormalNode(v));
fprintf(cm->stdOut, " ");
sat_PrintNodeAlone(cm, v);
sat_PrintNodeAlone(cm, SATleftChild(v));
sat_PrintNodeAlone(cm, SATrightChild(v));
fprintf(cm->stdOut, "\n");
size = SATnFanout(v);
fprintf(cm->stdOut, "%4d ", size);
for(i=0, fan=SATfanout(v); i<size; i++, fan++) {
cur = (*fan) >>1;
fprintf(cm->stdOut, "%6ld ", cur);
}
fprintf(cm->stdOut, "\n");
fprintf(cm->stdOut, " canonocal : %ld\n", sat_GetCanonical(cm, v));
if(cm->variableArray && SATvalue(v) < 2) {
ante = SATante(v);
if(SATflags(ante) & IsCNFMask) {
fprintf(cm->stdOut, " ante CNF : %ld\n", SATante(v));
}
else{
fprintf(cm->stdOut, " ante : %ld\n", SATante(v));
fprintf(cm->stdOut, " ante2 : %ld\n", SATante2(v));
}
}
if(cm->variableArray) {
var = SATgetVariable(v);
wl = var->wl[0];
if(wl && wl->num) {
fprintf(cm->stdOut, " 0 wl : ");
for(i=0; i<wl->num; i++) {
plit = (long *)(wl->space[i]);
if(plit == 0) continue;
fprintf(cm->stdOut, "%ld", (*plit)>>2);
while(1) {
plit++;
if(*plit < 0) break;
}
fprintf(cm->stdOut, "(%ld) ", -(*plit));
}
fprintf(cm->stdOut, "\n");
}
wl = var->wl[1];
if(wl && wl->num) {
fprintf(cm->stdOut, " 1 wl : ");
for(i=0; i<wl->num; i++) {
plit = (long *)(wl->space[i]);
if(plit == 0) continue;
fprintf(cm->stdOut, "%ld", (*plit)>>2);
while(1) {
plit++;
if(*plit < 0) break;
}
fprintf(cm->stdOut, "(%ld) ", -(*plit));
}
fprintf(cm->stdOut, "\n");
}
}
}
fflush(cm->stdOut);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_PrintNodeAlone | ( | satManager_t * | cm, |
| long | v | ||
| ) |
Function********************************************************************
Synopsis [ Print node infomation in the form of (id' = value)]
Description [ Print node infomation in the form of (id' = value)]
SideEffects []
SeeAlso []
Definition at line 192 of file satDebug.c.
{
int value, level, inverted;
inverted = SATisInverted(v);
v = SATnormalNode(v);
value = SATvalue(v);
level = value>1 ? -1 : (cm->variableArray ? SATlevel(v) : -1);
fprintf(cm->stdOut, "%6ld%c@%d=%c%c ",
v, inverted ? '\'' : ' ', level,
SATgetValueChar(value),
(SATflags(v)&ObjMask) ? '*' : ' ');
}
Here is the caller graph for this function:
| void sat_PrintProfileForNumConflict | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [ Print profile of the number of conflict on each clause]
Description [ Print profile of the number of conflict on each clause]
SideEffects []
SeeAlso []
Definition at line 839 of file satDebug.c.
{
char filename[1024];
FILE *fout;
int i, index;
satArray_t *arr;
long count;
long total, part;
long v;
long maxValue;
sprintf(filename, "nConflict.dat");
fout = fopen(filename, "w");
index = 1;
maxValue = 0;
arr = sat_ArrayAlloc(1024);
for(v=satNodeSize; v<cm->nodesArraySize; v+=satNodeSize) {
if(!(SATflags(v) & IsCNFMask)) continue;
if(SATnumConflict(v) == 0) continue;
if(SATnumConflict(v) > maxValue)
maxValue = SATnumConflict(v);
sat_ArrayInsert(arr, SATnumConflict(v));
}
qsort(arr->space, arr->num, sizeof(int), numCompareInt);
total = 0;
part = 0;
for(i=0; i<arr->num; i++) {
count = arr->space[i];
if(count == 0) continue;
total += count;
if(count > 1) {
part += count;
}
fprintf(fout, "%d %ld\n", i, count);
}
index = i;
sat_ArrayFree(arr);
fclose(fout);
sprintf(filename, "nConflict.gp");
fout = fopen(filename, "w");
fprintf(fout, "set xlabel \"Conflict Index\"\n");
fprintf(fout, "set ylabel \"Number of Conflicting %ld/%ld\"\n", part, total);
fprintf(fout, "set nokey\n");
fprintf(fout, "set size square 0.8,1\n");
fprintf(fout, "set xrange [0:%d]\n", index+1);
fprintf(fout, "set yrange [0:%ld]\n", maxValue+1);
fprintf(fout, "set grid\n");
fprintf(fout, "set border 3 linewidth 0.5\n");
fprintf(fout, "set xtics nomirror\n");
fprintf(fout, "set ytics nomirror\n");
fprintf(fout, "set mxtics 2\n");
fprintf(fout, "set mytics 2\n");
fprintf(fout, "set pointsize 2\n");
fprintf(fout, "set terminal postscript eps enhanced color solid \"Times-Roman\" 24\n");
fprintf(fout, "set output \"nConflict.eps\"\n");
fprintf(fout, "plot \"nConflict.dat\" using 1:2 with line linetype 3\n");
fclose(fout);
}
Here is the call graph for this function:
| void sat_PrintScore | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [ Print score]
Description [ Print score]
SideEffects []
SeeAlso []
Definition at line 325 of file satDebug.c.
{
int i;
long v;
satArray_t *ordered;
satVariable_t *var;
fprintf(cm->stdOut, "------------Print Score-----------\n");
ordered = cm->orderedVariableArray;
for(i=0; i<ordered->num; i++) {
v = ordered->space[i];
var = SATgetVariable(v);
fprintf(cm->stdOut, "%5ld : %3d %3d\n", v, var->scores[0], var->scores[1]);
}
fflush(cm->stdOut);
}
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: satDebug.c,v 1.14 2009/04/11 18:26:37 fabio Exp $" [static] |
CFile***********************************************************************
FileName [satDebug.c]
PackageName [sat]
Synopsis [Routines for various debug function.]
Author [HoonSang Jin]
Copyright [ This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
Definition at line 21 of file satDebug.c.
