#include "satInt.h"
Include dependency graph for satInterface.c:
Go to the source code of this file.
Functions | |
| void | sat_SetOptionForUP (satManager_t *cm) |
| int | sat_ReadCNF (satManager_t *cm, char *filename) |
| int | sat_ReadCNFFromArray (satManager_t *cm, satArray_t *cnfArray, st_table *mappedTable) |
| int | sat_WriteCNFFromArray (satArray_t *cnfArray, char *filename) |
| char * | sat_CopyWord (char *lp, char *word) |
| char * | sat_RemoveSpace (char *line) |
| void | sat_WriteCNFWithPartialAssignment (satManager_t *cm, char *filename) |
| void | sat_WriteCNF (satManager_t *cm, char *filename) |
| void | sat_WriteCNFWithPointer (satManager_t *cm, FILE *fout) |
| void | sat_CountUnitLiteralClauses (satManager_t *cm, satArray_t *arr, int *nCl) |
| void | sat_PrintUnitLiteralClauses (satManager_t *cm, satArray_t *arr, FILE *fout) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: satInterface.c,v 1.20 2009/04/11 18:26:37 fabio Exp $" |
Function Documentation
| char* sat_CopyWord | ( | char * | lp, |
| char * | word | ||
| ) |
Function********************************************************************
Synopsis [Copy word from lp to word]
Description [Copy word from lp to word and lp moved to next word.]
SideEffects []
SeeAlso []
Definition at line 355 of file satInterface.c.
{
char *wp;
for(wp = word; ; lp++, wp++) {
if((*lp == ' ') || (*lp == '\t') || (*lp == '\n')) break;
*wp = *lp;
}
*wp = '\0';
return(lp);
}
Here is the caller graph for this function:
| void sat_CountUnitLiteralClauses | ( | satManager_t * | cm, |
| satArray_t * | arr, | ||
| int * | nCl | ||
| ) |
Function********************************************************************
Synopsis [ Count the number of unit literal clauses ]
Description [ Count the number of unit literal clauses ]
SideEffects []
SeeAlso []
Definition at line 680 of file satInterface.c.
{
int i, count;
long v;
if(arr == 0) return;
count = 0;
for(i=0; i<arr->num; i++) {
v = arr->space[i];
if(v == 1) count++;
}
*nCl += arr->num - count;
}
Here is the caller graph for this function:
| void sat_PrintUnitLiteralClauses | ( | satManager_t * | cm, |
| satArray_t * | arr, | ||
| FILE * | fout | ||
| ) |
Function********************************************************************
Synopsis [ Print unit literal clauses ]
Description [ Print unit literal clauses ]
SideEffects []
SeeAlso []
Definition at line 710 of file satInterface.c.
{
int i, inverted;
long v;
if(arr == 0) return;
for(i=0; i<arr->num; i++) {
v = arr->space[i];
if(v == 1) continue;
inverted = SATisInverted(v);
v = SATnormalNode(v);
v = SATnodeID(v);
fprintf(fout, "%ld 0\n", inverted ? -v : v);
}
}
Here is the caller graph for this function:
| int sat_ReadCNF | ( | satManager_t * | cm, |
| char * | filename | ||
| ) |
Function********************************************************************
Synopsis [Read CNF]
Description [Read CNF]
SideEffects []
SeeAlso []
Definition at line 73 of file satInterface.c.
{
FILE *fin;
satArray_t *clauseArray;
char line[16384], word[1024], *lp;
int nVar, nCl, nArg;
int i, id, sign;
long v;
int begin;
long cls_idx;
if(!(fin = fopen(filename, "r"))) {
fprintf(cm->stdOut, "%s ERROR : Can't open CNF file %s\n",
cm->comment, filename);
return(0);
}
//Bing: for unsat core
if(cm->option->coreGeneration)
sat_SetOptionForUP(cm);
begin = 0;
clauseArray = sat_ArrayAlloc(1024);
while(fgets(line, 16384, fin)) {
lp = sat_RemoveSpace(line);
if(lp[0] == '\n') continue;
if(lp[0] == '#') continue;
if(lp[0] == 'c') continue;
if(lp[0] == 'p') {
nArg = sscanf(line, "p cnf %d %d", &nVar, &nCl);
if(nArg < 2) {
fprintf(cm->stdErr, "ERROR : Unable to read the number of variables and clauses from CNF file %s\n", filename);
fclose(fin);
sat_ArrayFree(clauseArray);
return(0);
}
begin = 1;
for(i=1; i<=nVar; i++) {
v = sat_CreateNode(cm, 2, 2);
SATflags(v) |= CoiMask;
SATvalue(v) = 2;
}
cm->initNumVariables = nVar;
cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
memset(cm->variableArray, 0, sizeof(satVariable_t) * (cm->initNumVariables+1));
continue;
}
else if(begin == 0) continue;
clauseArray->num = 0;
while(1) {
lp = sat_RemoveSpace(lp);
lp = sat_CopyWord(lp, word);
if(strlen(word)) {
id = atoi(word);
sign = 1;
if(id != 0) {
if(id < 0) {
id = -id;
sign = 0;
}
sat_ArrayInsert(clauseArray, (id*satNodeSize + sign));
}
else {
if(clauseArray->num == 1) {
v = clauseArray->space[0];
sat_ArrayInsert(cm->unitLits, SATnot(v));
cm->initNumClauses++;
cm->initNumLiterals += clauseArray->num;
//Bing: for unsat core
if(cm->option->coreGeneration){
cls_idx = sat_AddUnitClause(cm, clauseArray);
if(cm->option->coreGeneration){
v = SATnormalNode(v);
st_insert(cm->anteTable,(char *)v,(char *)cls_idx);
}
}
}
else {
sat_AddClause(cm, clauseArray);
cm->initNumClauses++;
cm->initNumLiterals += clauseArray->num;
}
break;
}
}
}
}
if(cm->initNumClauses == 0) {
fprintf(cm->stdOut, "%s ERROR : CNF is not valid\n", cm->comment);
return(0);
}
if(cm->initNumClauses != nCl) {
fprintf(cm->stdOut, "%s WARNING : wrong number of clauses\n", cm->comment);
}
fclose(fin);
sat_ArrayFree(clauseArray);
return(1);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int sat_ReadCNFFromArray | ( | satManager_t * | cm, |
| satArray_t * | cnfArray, | ||
| st_table * | mappedTable | ||
| ) |
Function********************************************************************
Synopsis [Read CNF from Array]
Description [Read CNF from Array]
SideEffects []
SeeAlso []
If clause is blocking clause then it has clause index in it.
Definition at line 192 of file satInterface.c.
{
satArray_t *clauseArray;
int nVar, nCl;
int i;
long tv, v, c, *space;
if(cnfArray == 0) {
fprintf(cm->stdOut, "%s ERROR : Can't find CNF array \n", cm->comment);
return(0);
}
nVar = 0;
nCl = 0;
for(i=1; i<cnfArray->num; i++) {
v = cnfArray->space[i];
if(v <= 0) nCl++;
else {
v = SATnormalNode(v);
if(v > nVar) nVar = v;
}
}
nVar = nVar / satNodeSize;
for(i=1; i<=nVar; i++) {
v = sat_CreateNode(cm, 2, 2);
SATflags(v) |= CoiMask;
SATvalue(v) = 2;
}
cm->initNumVariables = nVar;
cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
memset(cm->variableArray, 0, sizeof(satVariable_t) * (cm->initNumVariables+1));
clauseArray = sat_ArrayAlloc(1024);
for(i=0, space=cnfArray->space; i<cnfArray->num; i++, space++){
if(*space <= 0) {
space++;
i++;
if(i>=cnfArray->num)
break;
clauseArray->num = 0;
while(*space > 0) {
v = (*space);
sat_ArrayInsert(clauseArray, SATnot(v));
i++;
space++;
}
tv = *space;
if(clauseArray->num > 1)
c = sat_AddClause(cm, clauseArray);
else {
c = sat_AddUnitClause(cm, clauseArray);
if(cm->option->coreGeneration) {
st_insert(cm->anteTable,(char *)(long)(SATnormalNode(v)),(char *)(long)c);
}
}
if(clauseArray->num == 1)
sat_ArrayInsert(cm->unitLits, (v));
if(tv < -1) { /* this is blocking clause */
st_insert(mappedTable, (char *)c, (char *)(-tv));
}
cm->initNumClauses++;
cm->initNumLiterals += clauseArray->num;
i--;
space--;
}
}
sat_ArrayFree(clauseArray);
return(1);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| char* sat_RemoveSpace | ( | char * | line | ) |
Function********************************************************************
Synopsis [skip space and return the beginning of word ]
Description [skip space and return the beginning of word ]
SideEffects []
SeeAlso []
Definition at line 379 of file satInterface.c.
{
int i;
for(i=0; ; i++) {
if(line[i] == ' ') continue;
else if(line[i] == '\t') continue;
return(&(line[i]));
}
}
Here is the caller graph for this function:
| void sat_SetOptionForUP | ( | satManager_t * | cm | ) |
AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Set option for unsat core generation]
Description [Set option for unsat core generation]
SideEffects []
SeeAlso []
Definition at line 51 of file satInterface.c.
{
cm->option->includeLevelZeroLiteral = 1;
cm->option->minimizeConflictClause = 0;
cm->option->clauseDeletionHeuristic = 0;
cm->dependenceTable = st_init_table(st_ptrcmp, st_ptrhash);
cm->anteTable = st_init_table(st_numcmp, st_numhash);
cm->fp = fopen(cm->option->unsatCoreFileName, "w");
}
Here is the caller graph for this function:
| void sat_WriteCNF | ( | satManager_t * | cm, |
| char * | filename | ||
| ) |
Function********************************************************************
Synopsis [ Write CNF ]
Description [ Write CNF ]
SideEffects []
SeeAlso []
Definition at line 505 of file satInterface.c.
{
FILE *fout;
long i, tv, *plit, size, j;
int csize, inverted;
int nVar, nCl;
long left, right;
if(!(fout = fopen(filename, "w"))) {
fprintf(cm->stdOut, "%s ERROR : Can't open file %s\n",
cm->comment, filename);
exit(0);
}
nVar = cm->initNumVariables;
nCl = 0;
size = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
for(i=satNodeSize; i<size; i+=satNodeSize) {
if(SATleftChild(i) == 2 && SATrightChild(i) == 2) continue;
if(SATflags(i) & IsCNFMask) {
if(SATreadInUse(i) == 0) continue;
nCl++;
continue;
}
if(!(SATflags(i) & CoiMask)) continue;
nCl += 3;
}
sat_CountUnitLiteralClauses(cm, cm->assertion, &nCl);
sat_CountUnitLiteralClauses(cm, cm->unitLits, &nCl);
sat_CountUnitLiteralClauses(cm, cm->auxObj, &nCl);
sat_CountUnitLiteralClauses(cm, cm->obj, &nCl);
fprintf(fout, "p cnf %d %d\n", nVar, nCl);
sat_PrintUnitLiteralClauses(cm, cm->assertion, fout);
sat_PrintUnitLiteralClauses(cm, cm->unitLits, fout);
sat_PrintUnitLiteralClauses(cm, cm->auxObj, fout);
sat_PrintUnitLiteralClauses(cm, cm->obj, fout);
size = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
for(i=satNodeSize; i<size; i+=satNodeSize) {
if(SATleftChild(i) == 2 && SATrightChild(i) == 2) continue;
if(SATflags(i) & IsCNFMask) {
csize = SATnumLits(i);
plit = (long*)SATfirstLit(i);
for(j=0; j<csize; j++, plit++) {
tv = SATgetNode(*plit);
inverted = SATisInverted(tv);
tv = SATnormalNode(tv);
tv = SATnodeID(tv);
fprintf(fout, "%ld ", inverted ? -tv : tv);
}
fprintf(fout, "0\n");
continue;
}
if(!(SATflags(i) & CoiMask)) continue;
left = SATleftChild(i);
inverted = SATisInverted(left);
left = SATnormalNode(left);
left = SATnodeID(left);
left = inverted ? -left : left;
right = SATrightChild(i);
inverted = SATisInverted(right);
right = SATnormalNode(right);
right = SATnodeID(right);
right = inverted ? -right : right;
j = SATnodeID(i);
fprintf(fout, "%ld %ld %ld 0\n", -left, -right, j);
fprintf(fout, "%ld %ld 0\n", left, -j);
fprintf(fout, "%ld %ld 0\n", right, -j);
}
fclose(fout);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int sat_WriteCNFFromArray | ( | satArray_t * | cnfArray, |
| char * | filename | ||
| ) |
Function********************************************************************
Synopsis [Write CNF from Array]
Description [Write CNF from Array]
SideEffects []
SeeAlso []
Definition at line 287 of file satInterface.c.
{
FILE *fin;
int nVar, nCl;
int i ;
long v, *space;
if(cnfArray == 0) {
fprintf(stdout, "ERROR : Can't find CNF array \n");
return(0);
}
if(!(fin=fopen(filename, "w"))) {
fprintf(stdout, "ERROR : Can't find file %s\n", filename);
return(0);
}
nVar = 0;
nCl = 0;
for(i=1; i<cnfArray->num; i++) {
v = cnfArray->space[i];
if(v <= 0) nCl++;
else {
v = SATnormalNode(v);
if(v > nVar) nVar = v;
}
}
nVar = nVar / satNodeSize;
fprintf(fin, "p cnf %d %d\n", nVar, nCl);
for(i=0, space=cnfArray->space; i<cnfArray->num; i++, space++){
if(*space <= 0) {
space++;
i++;
if(i>=cnfArray->num)
break;
while(*space > 0) {
v = (*space);
if(SATisInverted(v)) v = -(SATnodeID(v));
else v = SATnodeID(v);
fprintf(fin, "%ld ", v);
i++;
space++;
}
fprintf(fin, "0\n");
i--;
space--;
}
}
fclose(fin);
return(1);
}
Here is the caller graph for this function:
| void sat_WriteCNFWithPartialAssignment | ( | satManager_t * | cm, |
| char * | filename | ||
| ) |
Function********************************************************************
Synopsis [Write CNF file under partial assignment]
Description [Write CNF file under partial assignment. If a literal in a clause is satisfied then the clause is ignored. If a literal in a clause is unsatisfied then the literal is ignored.]
SideEffects []
SeeAlso []
Definition at line 406 of file satInterface.c.
{
int nVars, nCls, j;
int size, satisfied;
int inverted, value;
long *plit, v, tv, tsize, i;
FILE *fout;
nVars = 0;
nCls = 0;
tsize = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
for(i=satNodeSize; i<tsize; i+=satNodeSize) {
if(SATleftChild(i) == 2 && SATrightChild(i) == 2) continue;
if(!(SATflags(i) & IsCNFMask)) {
if(!(SATflags(i) & CoiMask)) continue;
fprintf(cm->stdOut, "Warning : current implementation can't take care of AIG node\n");
continue;
}
if(SATreadInUse(i) == 0) continue;
size = SATnumLits(i);
satisfied = 0;
plit = (long *)SATfirstLit(i);
for(j=0; j<size; j++, plit++) {
v = SATgetNode(*plit);
inverted = SATisInverted(v);
v = SATnormalNode(v);
value = SATvalue(v) ^ inverted;
if(value == 1) {
satisfied = 1;
break;
}
if(v > nVars) nVars = v;
}
if(satisfied) continue;
nCls++;
}
nVars /= satNodeSize;
if(!(fout = fopen(filename, "w"))) {
fprintf(cm->stdOut, "%s ERROR : Can't open file %s\n",
cm->comment, filename);
exit(0);
}
fprintf(fout, "p cnf %d %d\n", nVars, nCls);
tsize = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
for(i=satNodeSize; i<tsize; i+=satNodeSize) {
if(SATleftChild(i) == 2 && SATrightChild(i) == 2) continue;
if(!(SATflags(i) & IsCNFMask)) {
if(!(SATflags(i) & CoiMask)) continue;
continue;
}
if(SATreadInUse(i) == 0) continue;
satisfied = 0;
size = SATnumLits(i);
plit = (long *)SATfirstLit(i);
for(j=0; j<size; j++, plit++) {
v = SATgetNode(*plit);
inverted = SATisInverted(v);
v = SATnormalNode(v);
value = SATvalue(v) ^ inverted;
if(value == 1) {
satisfied = 1;
break;
}
}
if(satisfied) continue;
plit = (long *)SATfirstLit(i);
for(j=0; j<size; j++, plit++) {
v = SATgetNode(*plit);
inverted = SATisInverted(v);
v = SATnormalNode(v);
value = SATvalue(v) ^ inverted;
if(value < 2) {
continue;
}
tv = SATnodeID(v);
fprintf(fout, "%ld ", inverted ? -tv : tv);
}
fprintf(fout, "0\n");
}
fclose(fout);
}
| void sat_WriteCNFWithPointer | ( | satManager_t * | cm, |
| FILE * | fout | ||
| ) |
Function********************************************************************
Synopsis [ Write CNF ]
Description [ Write CNF ]
SideEffects []
SeeAlso []
Definition at line 597 of file satInterface.c.
{
long i, j, size, tv, *plit;
int csize, inverted;
int nVar, nCl;
long left, right;
nVar = cm->initNumVariables;
nCl = 0;
size = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
for(i=satNodeSize; i<size; i+=satNodeSize) {
if(SATleftChild(i) == 2 && SATrightChild(i) == 2) continue;
if(SATflags(i) & IsCNFMask) {
if(SATreadInUse(i) == 0) continue;
nCl++;
continue;
}
if(!(SATflags(i) & CoiMask)) continue;
nCl += 3;
}
sat_CountUnitLiteralClauses(cm, cm->assertion, &nCl);
sat_CountUnitLiteralClauses(cm, cm->unitLits, &nCl);
sat_CountUnitLiteralClauses(cm, cm->auxObj, &nCl);
sat_CountUnitLiteralClauses(cm, cm->obj, &nCl);
fprintf(fout, "p cnf %d %d\n", nVar, nCl);
sat_PrintUnitLiteralClauses(cm, cm->assertion, fout);
sat_PrintUnitLiteralClauses(cm, cm->unitLits, fout);
sat_PrintUnitLiteralClauses(cm, cm->auxObj, fout);
sat_PrintUnitLiteralClauses(cm, cm->obj, fout);
size = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict;
for(i=satNodeSize; i<size; i+=satNodeSize) {
if(SATleftChild(i) == 2 && SATrightChild(i) == 2) continue;
if(SATflags(i) & IsCNFMask) {
csize = SATnumLits(i);
plit = (long*)SATfirstLit(i);
for(j=0; j<csize; j++, plit++) {
tv = SATgetNode(*plit);
inverted = SATisInverted(tv);
tv = SATnormalNode(tv);
tv = SATnodeID(tv);
fprintf(fout, "%ld ", inverted ? -tv : tv);
}
fprintf(fout, "0\n");
continue;
}
if(!(SATflags(i) & CoiMask)) continue;
left = SATleftChild(i);
inverted = SATisInverted(left);
left = SATnormalNode(left);
left = SATnodeID(left);
left = inverted ? -left : left;
right = SATrightChild(i);
inverted = SATisInverted(right);
right = SATnormalNode(right);
right = SATnodeID(right);
right = inverted ? -right : right;
j = SATnodeID(i);
fprintf(fout, "%ld %ld %ld 0\n", -left, -right, j);
fprintf(fout, "%ld %ld 0\n", left, -j);
fprintf(fout, "%ld %ld 0\n", right, -j);
}
}
Here is the call graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: satInterface.c,v 1.20 2009/04/11 18:26:37 fabio Exp $" [static] |
CFile***********************************************************************
FileName [satInterface.c]
PackageName [sat]
Synopsis [Routines for various decision heuristics.]
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 satInterface.c.
