VIS
|
00001 00019 #include "satInt.h" 00020 00021 static char rcsid[] UNUSED = "$Id: satInterface.c,v 1.20 2009/04/11 18:26:37 fabio Exp $"; 00022 00023 /*---------------------------------------------------------------------------*/ 00024 /* Constant declarations */ 00025 /*---------------------------------------------------------------------------*/ 00026 00029 /*---------------------------------------------------------------------------*/ 00030 /* Static function prototypes */ 00031 /*---------------------------------------------------------------------------*/ 00032 00033 00037 /*---------------------------------------------------------------------------*/ 00038 /* Definition of exported functions */ 00039 /*---------------------------------------------------------------------------*/ 00051 void sat_SetOptionForUP(satManager_t * cm) 00052 { 00053 cm->option->includeLevelZeroLiteral = 1; 00054 cm->option->minimizeConflictClause = 0; 00055 cm->option->clauseDeletionHeuristic = 0; 00056 cm->dependenceTable = st_init_table(st_ptrcmp, st_ptrhash); 00057 cm->anteTable = st_init_table(st_numcmp, st_numhash); 00058 cm->fp = fopen(cm->option->unsatCoreFileName, "w"); 00059 } 00060 00072 int 00073 sat_ReadCNF(satManager_t *cm, char *filename) 00074 { 00075 FILE *fin; 00076 satArray_t *clauseArray; 00077 char line[16384], word[1024], *lp; 00078 int nVar, nCl, nArg; 00079 int i, id, sign; 00080 long v; 00081 int begin; 00082 long cls_idx; 00083 00084 if(!(fin = fopen(filename, "r"))) { 00085 fprintf(cm->stdOut, "%s ERROR : Can't open CNF file %s\n", 00086 cm->comment, filename); 00087 return(0); 00088 } 00089 00090 //Bing: for unsat core 00091 if(cm->option->coreGeneration) 00092 sat_SetOptionForUP(cm); 00093 00094 begin = 0; 00095 clauseArray = sat_ArrayAlloc(1024); 00096 while(fgets(line, 16384, fin)) { 00097 lp = sat_RemoveSpace(line); 00098 if(lp[0] == '\n') continue; 00099 if(lp[0] == '#') continue; 00100 if(lp[0] == 'c') continue; 00101 if(lp[0] == 'p') { 00102 nArg = sscanf(line, "p cnf %d %d", &nVar, &nCl); 00103 if(nArg < 2) { 00104 fprintf(cm->stdErr, "ERROR : Unable to read the number of variables and clauses from CNF file %s\n", filename); 00105 fclose(fin); 00106 sat_ArrayFree(clauseArray); 00107 return(0); 00108 } 00109 begin = 1; 00110 00111 for(i=1; i<=nVar; i++) { 00112 v = sat_CreateNode(cm, 2, 2); 00113 SATflags(v) |= CoiMask; 00114 SATvalue(v) = 2; 00115 } 00116 00117 cm->initNumVariables = nVar; 00118 cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1); 00119 memset(cm->variableArray, 0, sizeof(satVariable_t) * (cm->initNumVariables+1)); 00120 continue; 00121 } 00122 else if(begin == 0) continue; 00123 00124 clauseArray->num = 0; 00125 while(1) { 00126 lp = sat_RemoveSpace(lp); 00127 lp = sat_CopyWord(lp, word); 00128 00129 if(strlen(word)) { 00130 id = atoi(word); 00131 sign = 1; 00132 00133 if(id != 0) { 00134 if(id < 0) { 00135 id = -id; 00136 sign = 0; 00137 } 00138 sat_ArrayInsert(clauseArray, (id*satNodeSize + sign)); 00139 } 00140 else { 00141 if(clauseArray->num == 1) { 00142 v = clauseArray->space[0]; 00143 sat_ArrayInsert(cm->unitLits, SATnot(v)); 00144 cm->initNumClauses++; 00145 cm->initNumLiterals += clauseArray->num; 00146 //Bing: for unsat core 00147 if(cm->option->coreGeneration){ 00148 cls_idx = sat_AddUnitClause(cm, clauseArray); 00149 if(cm->option->coreGeneration){ 00150 v = SATnormalNode(v); 00151 st_insert(cm->anteTable,(char *)v,(char *)cls_idx); 00152 } 00153 } 00154 } 00155 else { 00156 sat_AddClause(cm, clauseArray); 00157 cm->initNumClauses++; 00158 cm->initNumLiterals += clauseArray->num; 00159 } 00160 break; 00161 } 00162 } 00163 } 00164 } 00165 if(cm->initNumClauses == 0) { 00166 fprintf(cm->stdOut, "%s ERROR : CNF is not valid\n", cm->comment); 00167 return(0); 00168 } 00169 00170 if(cm->initNumClauses != nCl) { 00171 fprintf(cm->stdOut, "%s WARNING : wrong number of clauses\n", cm->comment); 00172 } 00173 00174 fclose(fin); 00175 sat_ArrayFree(clauseArray); 00176 00177 return(1); 00178 } 00179 00191 int 00192 sat_ReadCNFFromArray( 00193 satManager_t *cm, 00194 satArray_t *cnfArray, 00195 st_table *mappedTable) 00196 { 00197 satArray_t *clauseArray; 00198 int nVar, nCl; 00199 int i; 00200 long tv, v, c, *space; 00201 00202 if(cnfArray == 0) { 00203 fprintf(cm->stdOut, "%s ERROR : Can't find CNF array \n", cm->comment); 00204 return(0); 00205 } 00206 00207 nVar = 0; 00208 nCl = 0; 00209 for(i=1; i<cnfArray->num; i++) { 00210 v = cnfArray->space[i]; 00211 if(v <= 0) nCl++; 00212 else { 00213 v = SATnormalNode(v); 00214 if(v > nVar) nVar = v; 00215 } 00216 } 00217 nVar = nVar / satNodeSize; 00218 for(i=1; i<=nVar; i++) { 00219 v = sat_CreateNode(cm, 2, 2); 00220 SATflags(v) |= CoiMask; 00221 SATvalue(v) = 2; 00222 } 00223 00224 cm->initNumVariables = nVar; 00225 cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1); 00226 memset(cm->variableArray, 0, sizeof(satVariable_t) * (cm->initNumVariables+1)); 00227 00228 clauseArray = sat_ArrayAlloc(1024); 00229 for(i=0, space=cnfArray->space; i<cnfArray->num; i++, space++){ 00230 if(*space <= 0) { 00231 space++; 00232 i++; 00233 if(i>=cnfArray->num) 00234 break; 00235 clauseArray->num = 0; 00236 while(*space > 0) { 00237 v = (*space); 00238 sat_ArrayInsert(clauseArray, SATnot(v)); 00239 i++; 00240 space++; 00241 } 00242 00246 tv = *space; 00247 00248 if(clauseArray->num > 1) 00249 c = sat_AddClause(cm, clauseArray); 00250 else { 00251 c = sat_AddUnitClause(cm, clauseArray); 00252 if(cm->option->coreGeneration) { 00253 st_insert(cm->anteTable,(char *)(long)(SATnormalNode(v)),(char *)(long)c); 00254 } 00255 } 00256 if(clauseArray->num == 1) 00257 sat_ArrayInsert(cm->unitLits, (v)); 00258 00259 if(tv < -1) { /* this is blocking clause */ 00260 st_insert(mappedTable, (char *)c, (char *)(-tv)); 00261 } 00262 00263 cm->initNumClauses++; 00264 cm->initNumLiterals += clauseArray->num; 00265 i--; 00266 space--; 00267 } 00268 } 00269 sat_ArrayFree(clauseArray); 00270 00271 00272 return(1); 00273 } 00274 00286 int 00287 sat_WriteCNFFromArray(satArray_t *cnfArray, char *filename) 00288 { 00289 FILE *fin; 00290 int nVar, nCl; 00291 int i ; 00292 long v, *space; 00293 00294 if(cnfArray == 0) { 00295 fprintf(stdout, "ERROR : Can't find CNF array \n"); 00296 return(0); 00297 } 00298 00299 if(!(fin=fopen(filename, "w"))) { 00300 fprintf(stdout, "ERROR : Can't find file %s\n", filename); 00301 return(0); 00302 } 00303 00304 nVar = 0; 00305 nCl = 0; 00306 for(i=1; i<cnfArray->num; i++) { 00307 v = cnfArray->space[i]; 00308 if(v <= 0) nCl++; 00309 else { 00310 v = SATnormalNode(v); 00311 if(v > nVar) nVar = v; 00312 } 00313 } 00314 nVar = nVar / satNodeSize; 00315 00316 fprintf(fin, "p cnf %d %d\n", nVar, nCl); 00317 00318 for(i=0, space=cnfArray->space; i<cnfArray->num; i++, space++){ 00319 if(*space <= 0) { 00320 space++; 00321 i++; 00322 if(i>=cnfArray->num) 00323 break; 00324 00325 while(*space > 0) { 00326 v = (*space); 00327 if(SATisInverted(v)) v = -(SATnodeID(v)); 00328 else v = SATnodeID(v); 00329 fprintf(fin, "%ld ", v); 00330 i++; 00331 space++; 00332 } 00333 fprintf(fin, "0\n"); 00334 00335 i--; 00336 space--; 00337 } 00338 } 00339 fclose(fin); 00340 00341 return(1); 00342 } 00354 char * 00355 sat_CopyWord(char *lp, char *word) 00356 { 00357 char *wp; 00358 00359 for(wp = word; ; lp++, wp++) { 00360 if((*lp == ' ') || (*lp == '\t') || (*lp == '\n')) break; 00361 *wp = *lp; 00362 } 00363 *wp = '\0'; 00364 return(lp); 00365 } 00366 00378 char * 00379 sat_RemoveSpace(char *line) 00380 { 00381 int i; 00382 00383 for(i=0; ; i++) { 00384 if(line[i] == ' ') continue; 00385 else if(line[i] == '\t') continue; 00386 return(&(line[i])); 00387 } 00388 } 00389 00390 00405 void 00406 sat_WriteCNFWithPartialAssignment(satManager_t *cm, char *filename) 00407 { 00408 int nVars, nCls, j; 00409 int size, satisfied; 00410 int inverted, value; 00411 long *plit, v, tv, tsize, i; 00412 FILE *fout; 00413 00414 nVars = 0; 00415 nCls = 0; 00416 tsize = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict; 00417 for(i=satNodeSize; i<tsize; i+=satNodeSize) { 00418 if(SATleftChild(i) == 2 && SATrightChild(i) == 2) continue; 00419 if(!(SATflags(i) & IsCNFMask)) { 00420 if(!(SATflags(i) & CoiMask)) continue; 00421 fprintf(cm->stdOut, "Warning : current implementation can't take care of AIG node\n"); 00422 continue; 00423 } 00424 if(SATreadInUse(i) == 0) continue; 00425 00426 size = SATnumLits(i); 00427 satisfied = 0; 00428 plit = (long *)SATfirstLit(i); 00429 for(j=0; j<size; j++, plit++) { 00430 v = SATgetNode(*plit); 00431 inverted = SATisInverted(v); 00432 v = SATnormalNode(v); 00433 value = SATvalue(v) ^ inverted; 00434 if(value == 1) { 00435 satisfied = 1; 00436 break; 00437 } 00438 if(v > nVars) nVars = v; 00439 } 00440 if(satisfied) continue; 00441 00442 nCls++; 00443 } 00444 nVars /= satNodeSize; 00445 00446 if(!(fout = fopen(filename, "w"))) { 00447 fprintf(cm->stdOut, "%s ERROR : Can't open file %s\n", 00448 cm->comment, filename); 00449 exit(0); 00450 } 00451 00452 fprintf(fout, "p cnf %d %d\n", nVars, nCls); 00453 tsize = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict; 00454 for(i=satNodeSize; i<tsize; i+=satNodeSize) { 00455 if(SATleftChild(i) == 2 && SATrightChild(i) == 2) continue; 00456 if(!(SATflags(i) & IsCNFMask)) { 00457 if(!(SATflags(i) & CoiMask)) continue; 00458 continue; 00459 } 00460 if(SATreadInUse(i) == 0) continue; 00461 00462 satisfied = 0; 00463 size = SATnumLits(i); 00464 plit = (long *)SATfirstLit(i); 00465 for(j=0; j<size; j++, plit++) { 00466 v = SATgetNode(*plit); 00467 inverted = SATisInverted(v); 00468 v = SATnormalNode(v); 00469 value = SATvalue(v) ^ inverted; 00470 if(value == 1) { 00471 satisfied = 1; 00472 break; 00473 } 00474 } 00475 if(satisfied) continue; 00476 00477 plit = (long *)SATfirstLit(i); 00478 for(j=0; j<size; j++, plit++) { 00479 v = SATgetNode(*plit); 00480 inverted = SATisInverted(v); 00481 v = SATnormalNode(v); 00482 value = SATvalue(v) ^ inverted; 00483 if(value < 2) { 00484 continue; 00485 } 00486 tv = SATnodeID(v); 00487 fprintf(fout, "%ld ", inverted ? -tv : tv); 00488 } 00489 fprintf(fout, "0\n"); 00490 } 00491 fclose(fout); 00492 } 00504 void 00505 sat_WriteCNF(satManager_t *cm, char *filename) 00506 { 00507 FILE *fout; 00508 long i, tv, *plit, size, j; 00509 int csize, inverted; 00510 int nVar, nCl; 00511 long left, right; 00512 00513 if(!(fout = fopen(filename, "w"))) { 00514 fprintf(cm->stdOut, "%s ERROR : Can't open file %s\n", 00515 cm->comment, filename); 00516 exit(0); 00517 } 00518 00519 nVar = cm->initNumVariables; 00520 nCl = 0; 00521 size = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict; 00522 for(i=satNodeSize; i<size; i+=satNodeSize) { 00523 if(SATleftChild(i) == 2 && SATrightChild(i) == 2) continue; 00524 if(SATflags(i) & IsCNFMask) { 00525 if(SATreadInUse(i) == 0) continue; 00526 nCl++; 00527 continue; 00528 } 00529 if(!(SATflags(i) & CoiMask)) continue; 00530 nCl += 3; 00531 } 00532 sat_CountUnitLiteralClauses(cm, cm->assertion, &nCl); 00533 sat_CountUnitLiteralClauses(cm, cm->unitLits, &nCl); 00534 sat_CountUnitLiteralClauses(cm, cm->auxObj, &nCl); 00535 sat_CountUnitLiteralClauses(cm, cm->obj, &nCl); 00536 00537 fprintf(fout, "p cnf %d %d\n", nVar, nCl); 00538 00539 sat_PrintUnitLiteralClauses(cm, cm->assertion, fout); 00540 sat_PrintUnitLiteralClauses(cm, cm->unitLits, fout); 00541 sat_PrintUnitLiteralClauses(cm, cm->auxObj, fout); 00542 sat_PrintUnitLiteralClauses(cm, cm->obj, fout); 00543 00544 size = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict; 00545 for(i=satNodeSize; i<size; i+=satNodeSize) { 00546 if(SATleftChild(i) == 2 && SATrightChild(i) == 2) continue; 00547 if(SATflags(i) & IsCNFMask) { 00548 csize = SATnumLits(i); 00549 plit = (long*)SATfirstLit(i); 00550 for(j=0; j<csize; j++, plit++) { 00551 tv = SATgetNode(*plit); 00552 inverted = SATisInverted(tv); 00553 tv = SATnormalNode(tv); 00554 tv = SATnodeID(tv); 00555 fprintf(fout, "%ld ", inverted ? -tv : tv); 00556 } 00557 fprintf(fout, "0\n"); 00558 continue; 00559 } 00560 if(!(SATflags(i) & CoiMask)) continue; 00561 00562 00563 left = SATleftChild(i); 00564 inverted = SATisInverted(left); 00565 left = SATnormalNode(left); 00566 left = SATnodeID(left); 00567 left = inverted ? -left : left; 00568 00569 right = SATrightChild(i); 00570 inverted = SATisInverted(right); 00571 right = SATnormalNode(right); 00572 right = SATnodeID(right); 00573 right = inverted ? -right : right; 00574 00575 j = SATnodeID(i); 00576 00577 fprintf(fout, "%ld %ld %ld 0\n", -left, -right, j); 00578 fprintf(fout, "%ld %ld 0\n", left, -j); 00579 fprintf(fout, "%ld %ld 0\n", right, -j); 00580 } 00581 00582 fclose(fout); 00583 } 00584 00596 void 00597 sat_WriteCNFWithPointer(satManager_t *cm, FILE *fout) 00598 { 00599 long i, j, size, tv, *plit; 00600 int csize, inverted; 00601 int nVar, nCl; 00602 long left, right; 00603 00604 nVar = cm->initNumVariables; 00605 nCl = 0; 00606 size = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict; 00607 for(i=satNodeSize; i<size; i+=satNodeSize) { 00608 if(SATleftChild(i) == 2 && SATrightChild(i) == 2) continue; 00609 if(SATflags(i) & IsCNFMask) { 00610 if(SATreadInUse(i) == 0) continue; 00611 nCl++; 00612 continue; 00613 } 00614 if(!(SATflags(i) & CoiMask)) continue; 00615 nCl += 3; 00616 } 00617 sat_CountUnitLiteralClauses(cm, cm->assertion, &nCl); 00618 sat_CountUnitLiteralClauses(cm, cm->unitLits, &nCl); 00619 sat_CountUnitLiteralClauses(cm, cm->auxObj, &nCl); 00620 sat_CountUnitLiteralClauses(cm, cm->obj, &nCl); 00621 00622 fprintf(fout, "p cnf %d %d\n", nVar, nCl); 00623 00624 sat_PrintUnitLiteralClauses(cm, cm->assertion, fout); 00625 sat_PrintUnitLiteralClauses(cm, cm->unitLits, fout); 00626 sat_PrintUnitLiteralClauses(cm, cm->auxObj, fout); 00627 sat_PrintUnitLiteralClauses(cm, cm->obj, fout); 00628 00629 size = (cm->beginConflict == 0) ? cm->nodesArraySize : cm->beginConflict; 00630 for(i=satNodeSize; i<size; i+=satNodeSize) { 00631 if(SATleftChild(i) == 2 && SATrightChild(i) == 2) continue; 00632 if(SATflags(i) & IsCNFMask) { 00633 csize = SATnumLits(i); 00634 plit = (long*)SATfirstLit(i); 00635 for(j=0; j<csize; j++, plit++) { 00636 tv = SATgetNode(*plit); 00637 inverted = SATisInverted(tv); 00638 tv = SATnormalNode(tv); 00639 tv = SATnodeID(tv); 00640 fprintf(fout, "%ld ", inverted ? -tv : tv); 00641 } 00642 fprintf(fout, "0\n"); 00643 continue; 00644 } 00645 if(!(SATflags(i) & CoiMask)) continue; 00646 00647 00648 left = SATleftChild(i); 00649 inverted = SATisInverted(left); 00650 left = SATnormalNode(left); 00651 left = SATnodeID(left); 00652 left = inverted ? -left : left; 00653 00654 right = SATrightChild(i); 00655 inverted = SATisInverted(right); 00656 right = SATnormalNode(right); 00657 right = SATnodeID(right); 00658 right = inverted ? -right : right; 00659 00660 j = SATnodeID(i); 00661 00662 fprintf(fout, "%ld %ld %ld 0\n", -left, -right, j); 00663 fprintf(fout, "%ld %ld 0\n", left, -j); 00664 fprintf(fout, "%ld %ld 0\n", right, -j); 00665 } 00666 00667 } 00679 void 00680 sat_CountUnitLiteralClauses( 00681 satManager_t *cm, 00682 satArray_t *arr, 00683 int *nCl) 00684 { 00685 int i, count; 00686 long v; 00687 00688 if(arr == 0) return; 00689 count = 0; 00690 for(i=0; i<arr->num; i++) { 00691 v = arr->space[i]; 00692 if(v == 1) count++; 00693 } 00694 00695 *nCl += arr->num - count; 00696 } 00697 00709 void 00710 sat_PrintUnitLiteralClauses( 00711 satManager_t *cm, 00712 satArray_t *arr, 00713 FILE *fout) 00714 { 00715 int i, inverted; 00716 long v; 00717 00718 if(arr == 0) return; 00719 for(i=0; i<arr->num; i++) { 00720 v = arr->space[i]; 00721 if(v == 1) continue; 00722 inverted = SATisInverted(v); 00723 v = SATnormalNode(v); 00724 v = SATnodeID(v); 00725 fprintf(fout, "%ld 0\n", inverted ? -v : v); 00726 } 00727 }