#include "satInt.h"#include "puresatInt.h"
Include dependency graph for satCore.c:
Go to the source code of this file.
Defines | |
| #define | CONFLICT 1 |
| #define | NO_CONFLICT 2 |
Functions | |
| static int | ScoreCompare (const void *node1, const void *node2) |
| void | sat_PrintClauseLits (satManager_t *cm, long concl) |
| void | sat_PrintClauseLitsForCore (satManager_t *cm, long concl, FILE *fp) |
| void | sat_GenerateCoreRecur (satManager_t *cm, long concl, FILE *fp, int *count) |
| void | sat_GetDependence (satManager_t *cm, long concl, satArray_t *dep) |
| void | sat_GenerateCore (satManager_t *cm) |
| void | sat_ImplyArrayWithAnte (satManager_t *cm, satLevel_t *d, satArray_t *arr) |
| void | sat_ImplyUnitPureLitsWithAnte (satManager_t *cm, satLevel_t *d) |
| void | sat_BuildRT (satManager_t *cm, RTnode_t root, long *lp, long *tmpIP, int size, boolean NotCNF) |
| bAigEdge_t | sat_GenerateFwdIP (bAig_Manager_t *manager, satManager_t *cm, RTnode_t RTnode, int cut) |
| bAigEdge_t | sat_GenerateBwdIP (bAig_Manager_t *manager, satManager_t *cm, RTnode_t RTnode, int cut) |
| void | ResetRTree (RTManager_t *rm) |
| void | RT_Free (RTManager_t *rm) |
| void | sat_MarkLayerProperty (satManager_t *cm, long v, int layer) |
| void | sat_MarkLayer (satManager_t *cm, long v, int layer) |
| void | sat_MarkLayerInitState (satManager_t *cm, long v, int layer) |
| void | sat_MarkLayerLatch (satManager_t *cm, long v, int layer) |
| void | sat_InitLayerScore (satManager_t *cm) |
| void | sat_GenerateCore_All (satManager_t *cm) |
| void | sat_ASmergeLevel (satManager_t *cm) |
| int | sat_CE_CNF (satManager_t *cm, satLevel_t *d, int v, satArray_t *wl) |
| int | sat_CE (satManager_t *cm, satLevel_t *d, long v, int dfs, int value) |
| int | sat_ASDec (satManager_t *cm, satLevel_t *d, long v) |
| int | sat_ASImp (satManager_t *cm, satLevel_t *d, long v, int value) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: satCore.c,v 1.20 2009/04/12 00:14:11 fabio Exp $" |
Define Documentation
Function Documentation
| void ResetRTree | ( | RTManager_t * | rm | ) |
Function********************************************************************
Synopsis [ Reset resolution tree]
Description []
SideEffects []
SeeAlso []
Definition at line 795 of file satCore.c.
{
int i;
for(i=RTnodeSize;i<=rm->aSize;i+=RTnodeSize){
RT_IPnode(i) = -1;
RT_flag(i) &= RT_ResetVisitedMask;
}
return;
}
Here is the caller graph for this function:
| void RT_Free | ( | RTManager_t * | rm | ) |
| int sat_ASDec | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v | ||
| ) |
Function********************************************************************
Synopsis [Decision procedure for Arosat]
Description []
SideEffects []
SeeAlso []
Definition at line 1739 of file satCore.c.
{
int dfs;
int *numArray,*assignedArray;
satVariable_t *var=SATgetVariable(v);
assignedArray = cm->assignedArray;
numArray = cm->numArray;
v = SATnormalNode(v);
dfs = var->scores[0]/SCOREUNIT;
#if DBG
assert(dfs==cm->LatchLevel);
assert(!(SATflags(SATnormalNode(v)) & InQueueMask));
assert(SATvalue(SATnormalNode(v))==2);
#endif
if(!(SATflags(SATnormalNode(v))&AssignedMask)){
SATflags(SATnormalNode(v))|=AssignedMask;
assignedArray[dfs]++;
/* if(dfs==cm->OriLevel)
// fprintf(vis_stdout,"Assign Level %d: %d dfs=%d assArray[%d]=%d\n",
// d->level,v,dfs,dfs,cm->assignedArray[dfs]);*/
if(cm->assignedArray[dfs]==cm->numArray[dfs])
sat_ASmergeLevel(cm);
/*fprintf(vis_stdout,"Decisionlevel:%d: %d dfs=%d,assArray[%d]=%d, numArray[%d]=%d\n",
// d->level,v,dfs,dfs,assignedArray[dfs],dfs,numArray[dfs]);*/
}
return 0;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int sat_ASImp | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| int | value | ||
| ) |
Function********************************************************************
Synopsis [Implication procedure for Arosat]
Description []
SideEffects []
SeeAlso []
Definition at line 1786 of file satCore.c.
{
int dfs;
long tmpv;
int *numArray,*assignedArray;
satVariable_t *var=SATgetVariable(v);
assignedArray = cm->assignedArray;
numArray = cm->numArray;
v = SATnormalNode(v);
#if DBG
assert(SATvalue(v)==2);
#endif
dfs = var->scores[0]/SCOREUNIT;
if(dfs==cm->LatchLevel){
if(!(SATflags(SATnormalNode(v))&AssignedMask)){
SATflags(SATnormalNode(v))|=AssignedMask;
assignedArray[dfs]++;
#if DBG
assert(assignedArray[dfs]<=numArray[dfs]);
#endif
if(cm->assignedArray[dfs]==cm->numArray[dfs])
sat_ASmergeLevel(cm);
}
return 0;
}
else{
/*if conflict enforcing*/
if(sat_CE(cm,d,v,dfs,value)){
if(!(SATflags(SATnormalNode(v))&AssignedMask)){
SATflags(SATnormalNode(v))|=AssignedMask;
assignedArray[dfs]++;
#if DBG
assert(assignedArray[dfs]<=numArray[dfs]);
#endif
}
return 0;
}
/*else implication is prohibited*/
else{
#if DBG
assert(value==0||value==1);
#endif
if(value==0)
tmpv = -1;
else
tmpv = 1;
SATgetVariable(v)->RecVal = tmpv;
return 1;
}
}
return 0;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_ASmergeLevel | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [Merge level for Arosat]
Description []
SideEffects []
SeeAlso []
Definition at line 1503 of file satCore.c.
{
int base;
long v;
satVariable_t *var;
int *assignedArray = cm->assignedArray;
int * numArray = cm->numArray,level=0;
if(cm->option->verbose >= 2)
fprintf(vis_stdout,"MERGE LEVEL\n");
while(cm->LatchLevel>0){
if(cm->option->verbose >= 2)
fprintf(vis_stdout,"Merge level %d and %d\n",cm->LatchLevel, cm->LatchLevel-1);
level++;
cm->LatchLevel--;
if(cm->numArray[cm->LatchLevel]>0)
break;
}
if(cm->option->verbose >= 2)
fprintf(vis_stdout,"After Merge,Latch level:%d\n",cm->LatchLevel);
#if DBG
assert(cm->LatchLevel>0);
#endif
for(v=satNodeSize;v<cm->initNodesArraySize;v+=satNodeSize){
if(!SATflags(v)&CoiMask)
continue;
var = SATgetVariable(v);
base = var->scores[0]/SCOREUNIT;
if(base==cm->LatchLevel+level){
var->scores[0] = cm->LatchLevel*SCOREUNIT + var->scores[0]%SCOREUNIT;
var->scores[1] = cm->LatchLevel*SCOREUNIT + var->scores[1]%SCOREUNIT;
}
}
assignedArray[cm->LatchLevel]+=assignedArray[cm->LatchLevel+level];
numArray[cm->LatchLevel]+=numArray[cm->LatchLevel+level];
}
Here is the caller graph for this function:
| void sat_BuildRT | ( | satManager_t * | cm, |
| RTnode_t | root, | ||
| long * | lp, | ||
| long * | tmpIP, | ||
| int | size, | ||
| boolean | NotCNF | ||
| ) |
Function********************************************************************
Synopsis [Build an node for resolution tree]
Description [tmpIP, lp,size must be prepared Get formula for leaf nodes]
SideEffects []
SeeAlso []
Definition at line 466 of file satCore.c.
{
int i;
long tmpnode;
RTManager_t *rm = cm->rm;
RT_formula(root) = rm->cpos;
RT_fSize(root) = size;
if(rm->maxpos<=rm->cpos+size+1){
rm->fArray = REALLOC(long,rm->fArray,rm->maxpos+FORMULA_BLOCK);
rm->maxpos = rm->maxpos+FORMULA_BLOCK;
}
for(i=0;i<size;i++,lp++){
if(NotCNF)
tmpnode = *lp;
else
tmpnode = SATgetNode(*lp);
rm->fArray[rm->cpos] = tmpnode;
rm->cpos++;
}
}
Here is the caller graph for this function:
| int sat_CE | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| int | dfs, | ||
| int | value | ||
| ) |
Function********************************************************************
Synopsis [Conflict enforcing]
Description []
SideEffects []
SeeAlso []
Definition at line 1653 of file satCore.c.
{
long value1,*fan;
long cur, i, size;
long left, right;
satVariable_t *var;
satArray_t *wlArray;
long enforce=0;
v = SATnormalNode(v);
var = SATgetVariable(v);
wlArray = var->wl[value^1];
/*need recovery*/
SATvalue(v) = value;
/* implcation on CNF*/
if(wlArray && wlArray->size) {
if(sat_CE_CNF(cm, d, v, wlArray)==CONFLICT){
enforce = 1;
}
}
/*need recovery*/
SATvalue(v) = value;
if(enforce==0){
/* implication on AIG*/
fan = SATfanout(v);
size = SATnFanout(v);
for(i=0; i<size; i++, fan++) {
cur = *fan;
cur = cur >> 1;
cur = SATnormalNode(cur);
left = SATleftChild(cur);
right = SATrightChild(cur);
value1 = SATgetValue(left, right, cur);
if(value1==1||value1==5||value1==9||value1==13||value1==17
||value1==20||value1==33||value1==49){
/*fprintf(vis_stdout,"AIG Output enforce\n");*/
enforce=1;
break;
}
}
}
if(enforce==0){
left = SATleftChild(v);
right = SATrightChild(v);
if(left!=2&&right!=2){
value1 = SATgetValue(left, right, v);
if(value1==1||value1==5||value1==9||value1==13||value1==17
||value1==20||value1==33||value1==49){
/*fprintf(vis_stdout,"AIG Children enforce\n");*/
enforce=1;
}
}
}
SATvalue(v)=2;
return enforce;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int sat_CE_CNF | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| int | v, | ||
| satArray_t * | wl | ||
| ) |
Function********************************************************************
Synopsis [CNF based conflict enforcing]
Description []
SideEffects []
SeeAlso []
Definition at line 1554 of file satCore.c.
{
long size, i, *space;
long lit, *plit, dir;
long nv, tv, *oplit, *wlit;
int isInverted, value;
long inverted, clit;
satStatistics_t *stats;
satOption_t *option;
satQueue_t *Q;
size = wl->num;
space = wl->space;
Q = cm->queue;
stats = cm->each;
option = cm->option;
for(i=0; i<size; i++) {
plit = (long*)space[i];
if(plit == 0 || *plit == 0) {
continue;
}
lit = *plit;
dir = SATgetDir(lit);
oplit = plit;
while(1) {
oplit += dir;
if(*oplit <=0) {
if(dir == 1) nv =- (*oplit);
if(dir == SATgetDir(lit)) {
oplit = plit;
dir = -dir;
continue;
}
tv = SATgetNode(*wlit);
isInverted = SATisInverted(tv);
tv = SATnormalNode(tv);
value = SATvalue(tv) ^ isInverted;
if(value == 0) { /* conflict happens*/
return CONFLICT;
}
else if(value > 1) { /* implication*/
/*implication can only be made on the other wl*/
break;
}
break;
}
clit = *oplit;
tv = SATgetNode(clit);
inverted = SATisInverted(tv);
tv = SATnormalNode(tv);
value = SATvalue(tv) ^ inverted;
if(SATisWL(clit)) { /* found other watched literal*/
wlit = oplit;
/*a little diff from zchaff, if otherwl==1, break*/
if(value == 1) {
break;
}
/*since it is otherwl, it can't be zero. Here it is unknow*/
continue;
}
if(value == 0)
continue;
/*now it is 1 or unknow*/
break;
}/*while(1)*/
}/*for*/
return NO_CONFLICT;
}
Here is the caller graph for this function:
| bAigEdge_t sat_GenerateBwdIP | ( | bAig_Manager_t * | manager, |
| satManager_t * | cm, | ||
| RTnode_t | RTnode, | ||
| int | cut | ||
| ) |
Function********************************************************************
Synopsis [Generate interpolation backwardly]
Description []
SideEffects []
SeeAlso []
Definition at line 663 of file satCore.c.
{
int i;
long node,node1, left, right, result, *lp, *lp1;
int IPTrue=0, local=1, allGV=1;
RTManager_t * rm = cm->rm;
manager->class_ = cut;
if(RT_flag(RTnode)&RT_VisitedMask){
#if DBG
assert(RT_IPnode(RTnode)!=-1);
#endif
return RT_IPnode(RTnode);
}
#if DBG
assert(RT_IPnode(RTnode)==-1);
#endif
RT_flag(RTnode) |= RT_VisitedMask;
if(RT_pivot(RTnode)==0){ /*leaf*/
#if DBG
assert(RT_left(RTnode)==RT_NULL&&RT_right(RTnode)==RT_NULL);
assert(RT_oriClsIdx(RTnode)==0);
#endif
result = bAig_Zero;
if(RT_oriClsIdx(RTnode))
lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode));
else
lp = RT_formula(RTnode) + cm->rm->fArray;
lp1 = lp;
for(i=0;i<RT_fSize(RTnode);i++,lp++){
if(*lp == DUMMY)
continue;
else{
assert(*lp>0);
}
if(RT_oriClsIdx(RTnode))/*is CNF*/
node = SATgetNode(*lp);
else /*is AIG*/
node = *lp;
node = SATnormalNode(node);
if(SATflags(node)&IsGlobalVarMask)
continue;
else
allGV = 0;
if(SATclass(node)<=cut){
IPTrue = 1;
break;
}
}
if(IPTrue||allGV){
RT_IPnode(RTnode) = bAig_One;
return bAig_One;
}
lp = lp1;
for(i=0;i<RT_fSize(RTnode);i++,lp++){
if(RT_oriClsIdx(RTnode))/*is CNF*/
node = SATgetNode(*lp);
else /*is AIG*/
node = *lp;
node1 = SATnormalNode(node);
if(SATflags(node1)&IsGlobalVarMask){
result = PureSat_Or(manager,result,node);
cm->nodesArray = manager->NodesArray;
}
}
RT_IPnode(RTnode) = result;
return result;
} /*leaf*/
/*not leaf*/
else{
#if DBG
assert(RT_left(RTnode)!=RT_NULL&&RT_right(RTnode)!=RT_NULL);
#endif
left = sat_GenerateBwdIP(manager,cm,RT_left(RTnode),cut);
right = sat_GenerateBwdIP(manager,cm,RT_right(RTnode),cut);
if(RT_pivot(RTnode)<0){
int class_;
class_ = RT_pivot(RTnode)-DUMMY;
#if DBG
assert(class_>0);
#endif
if(class_<=cut)
local=0;
}
else{
node = SATnormalNode(RT_pivot(RTnode));
if((SATflags(node)&IsGlobalVarMask)||
(SATclass(node)<=cut))
local = 0;
}
if(local==0){
result = PureSat_And(manager,left,right);
}
else{
result = PureSat_Or(manager,left,right);
}
}/* else{ not leaf*/
cm->nodesArray = manager->NodesArray;
RT_IPnode(RTnode) = result;
return result;
}
Here is the call graph for this function:
| void sat_GenerateCore | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [Conflict Core Generation]
Description [Conflict Core Generation]
SideEffects [ ]
SeeAlso [ ]
sat_ArrayInsert(unitArray, tmp);
Last Conflict Cls
sat_ArrayInsert(arr,cl);
is CONFLICT
not CONFLICT
fclose(fp);
Definition at line 241 of file satCore.c.
{
int j, tmp,value;
long *lit, node, concl, i;
satArray_t * dep;
FILE *fp = cm->fp;
int count, inverted;
st_generator *stGen;
satArray_t* tmpdep = sat_ArrayAlloc(1);
satLevel_t * d;
cm->status = 0;
count = 0;
d = SATgetDecision(0);
for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize){
node = i;
if((SATflags(node)&IsCNFMask)&&(SATnumLits(node)==1)){
lit = (long*)SATfirstLit(node);
tmp = SATgetNode(*lit);
inverted = SATisInverted(tmp);
tmp = SATnormalNode(tmp);
value = !inverted;
if(SATvalue(tmp) < 2) {
if(SATvalue(tmp) == value) continue;
else {
cm->status = SAT_UNSAT;
d->conflict = node;
break;
}
}
SATvalue(tmp) = !inverted;
SATmakeImplied(tmp, d);
SATante(tmp) = node;
if((SATflags(tmp) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, tmp);
SATflags(tmp) |= InQueueMask;
}
}
}
sat_ImplicationMain(cm, d);
if(d->conflict == 0) {
fprintf(vis_stderr,"There should be a conflict\n");
exit(0);
}
concl = d->conflict;
sat_ArrayInsert(tmpdep,concl);
SATflags(concl)|=NewMask;
if(!(SATflags(concl)&IsConflictMask)){
count++;
sat_PrintClauseLitsForCore(cm,concl,fp);
}
sat_GetDependence(cm, concl, tmpdep);
for(i=satNodeSize;i<cm->nodesArraySize;i+=satNodeSize){
SATflags(i)&=ResetNewMask;
}
for(i=0;i<tmpdep->num;i++){
concl = tmpdep->space[i];
if(!(SATflags(concl)&NewMask)){
SATflags(concl)|=NewMask;
if((SATflags(concl)&IsConflictMask)){
if(!st_lookup(cm->dependenceTable,(char *)concl,&dep)){
fprintf(cm->stdOut,"%ld is conflict but not in depe table\n",concl);
exit(0);
}
else{
for(j=0;j<dep->num; j++){
tmp = dep->space[j];
sat_GenerateCoreRecur(cm, tmp, fp, &count);
}
}
}
else{
count++;
sat_PrintClauseLitsForCore(cm,concl,fp);
}
}
}
cm->numOfClsInCore = count;
for(i=satNodeSize;i<cm->nodesArraySize;i+=satNodeSize){
SATflags(i)&=ResetNewMask;
}
st_foreach_item(cm->dependenceTable, stGen,&node, &dep)
sat_ArrayFree(dep);
sat_ArrayFree(tmpdep);
sat_Undo(cm,d);
st_free_table(cm->dependenceTable);
st_free_table(cm->anteTable);
cm->status = SAT_UNSAT;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_GenerateCore_All | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [Generate unsat proof in the form of resolution graph]
Description []
SideEffects []
SeeAlso []
Definition at line 1222 of file satCore.c.
{
int i,j,value;
long *lit, ante, node, tmp1;
int count, inverted;
satLevel_t * d;
satArray_t *clauseArray = sat_ArrayAlloc(1);
int objectFlag;
long conflicting, ante2;
int nMarked,first;
long v,left,right,result,*lp,*tmpIP;
long *space,*tmp;
satArray_t *implied;
RTnode_t tmprt;
int size = 0, *bLevel;
long *fdaLit=ALLOC(long,1);
boolean endnow;
RTManager_t * rm = cm->rm;
cm->status = 0;
count = 0;
d = SATgetDecision(0);
sat_ImplyArrayWithAnte(cm,d,cm->obj);
sat_ImplyArrayWithAnte(cm,d,cm->auxObj);
sat_ImplyArrayWithAnte(cm,d,cm->assertArray);
if(cm->status==0){
for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize){
node = i;
if((SATflags(node)&IsCNFMask)&&(SATnumLits(node)==1)){
lit = (long*)SATfirstLit(node);
tmp1 = SATgetNode(*lit);
inverted = SATisInverted(tmp1);
tmp1 = SATnormalNode(tmp1);
value = !inverted;
if(SATvalue(tmp1) < 2) {
if(SATvalue(tmp1) == value) continue;
else {
cm->status = SAT_UNSAT;
d->conflict = node;
break;
}
}
SATvalue(tmp1) = !inverted;
SATmakeImplied(tmp1, d);
SATante(tmp1) = node;
if((SATflags(tmp1) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, tmp1);
SATflags(tmp1) |= InQueueMask;
}
}
}
}
if(cm->status==0){
sat_ImplicationMain(cm, d);
}
if(d->conflict == 0) {
fprintf(vis_stderr,"There should be a conflict\n");
exit(0);
}
conflicting = d->conflict;
nMarked = 0;
sat_MarkNodeInConflict(
cm, d, &nMarked, &objectFlag, bLevel, clauseArray);
/* Traverse implication graph backward*/
first = 1;
implied = d->implied;
space = implied->space+implied->num-1;
if(cm->option->coreGeneration){
/*if last conflict is CNF*/
if(SATflags(conflicting)&IsCNFMask){
/*is conflict CNF*/
if(SATflags(conflicting)&IsConflictMask){
if(!st_lookup(cm->RTreeTable,(char*)conflicting,&tmprt)){
fprintf(vis_stderr,"RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
exit(0);
}
else{
rm->root = tmprt;
#if PR
fprintf(vis_stdout,"Get formula for CONFLICT CLAUSE:%d\n",ante);
#endif
}
}
/*CNF but not conflict*/
else{
rm->root = RTCreateNode(rm);
size = SATnumLits(conflicting);
RT_fSize(rm->root) = size;
lp = (long*)SATfirstLit(conflicting);
sat_BuildRT(cm,rm->root, lp, tmpIP,size,0);
}
}
/*if last conflict is AIG*/
else{
rm->root = RTCreateNode(rm);
node = SATnormalNode(conflicting);
left = SATleftChild(node);
right = SATrightChild(node);
result = PureSat_IdentifyConflict(cm,left,right,conflicting);
inverted = SATisInverted(left);
left = SATnormalNode(left);
left = inverted ? SATnot(left) : left;
inverted = SATisInverted(right);
right = SATnormalNode(right);
right = inverted ? SATnot(right) : right;
j = node;
if(result == 1){
tmp = ALLOC(long,3);
tmp[0] = left;
tmp[1] = SATnot(j);
size = 2;
}
else if(result == 2){
tmp = ALLOC(long,3);
tmp[0] = right;
tmp[1] = SATnot(j);
size = 2;
}
else if(result == 3){
tmp = ALLOC(long,4);
tmp[0] = SATnot(left);
tmp[1] = SATnot(right);
tmp[2] = j;
size = 3;
}
else{
fprintf(vis_stderr,"wrong returned result value, exit\n");
exit(0);
}
lp = tmp;
sat_BuildRT(cm,rm->root, lp, tmpIP,size,1);
FREE(tmp);
}
}
endnow = FALSE;
for(i=implied->num-1; i>=0; i--, space--) {
if(endnow)
break;
v = *space;
if(SATflags(v) & VisitedMask) {
SATflags(v) &= ResetVisitedMask;
--nMarked;
if(nMarked == 0 && (!first || i==0)) {
/*value = SATvalue(v);*/
*fdaLit = v^(!value);
sat_ArrayInsert(clauseArray, *fdaLit);
/*break;*/
endnow = TRUE;
}
if(cm->option->coreGeneration){
ante = SATante(v);
if(ante==0){
if(!(st_lookup(cm->anteTable, (char *)SATnormalNode(v),&ante))){
fprintf(vis_stderr,"ante = 0 and is not in anteTable %ld\n",v);
exit(0);
}
}
/*build non-leaf node*/
tmprt = RTCreateNode(rm);
RT_pivot(tmprt) = SATnormalNode(v);
RT_right(tmprt) = rm->root;
rm->root = tmprt;
if((SATflags(ante)&IsConflictMask)&&(SATflags(ante)&IsCNFMask)){
if(!st_lookup(cm->RTreeTable,(char*)ante,&tmprt)){
fprintf(vis_stderr,"RTree node of conflict cnf %ld is not in RTreeTable\n",ante);
exit(0);
}
else{
RT_left(rm->root) = tmprt;
#if PR
fprintf(vis_stdout,"Get formula for CONFLICT CLAUSE:%d\n",ante);
#endif
}
}
else{ /* if not conflict CNF*/
/*left*/
tmprt = RTCreateNode(rm);
RT_left(rm->root) = tmprt;
/*left is AIG*/
if(!(SATflags(ante) & IsCNFMask)){
/*generate formula for left*/
tmp = ALLOC(long,3);
value = SATvalue(v);
node = SATnormalNode(v);
node = value==1?node:SATnot(node);
tmp[0] = node;
size = 1;
if(ante != SATnormalNode(v)){
value = SATvalue(ante);
node = SATnormalNode(ante);
node = value==1?SATnot(node):node;
tmp[1] = node;
size++;
ante2 = SATante2(v);
if(ante2){
value = SATvalue(ante2);
node = SATnormalNode(ante2);
node = value==1?SATnot(node):node;
tmp[2] = node;
size++;
}
}
lp = tmp;
sat_BuildRT(cm,tmprt,lp,tmpIP,size,1);
FREE(tmp);
}
/* left is CNF*/
else{
lp = (long*)SATfirstLit(ante);
size = SATnumLits(ante);
RT_fSize(tmprt) = size;
sat_BuildRT(cm,tmprt, lp, tmpIP,size,0);
}
} /*else{ // if not conflict CNF*/
}/*if(cm->option->coreGeneration){*/
sat_MarkNodeInImpliedNode(
cm, d, v, &nMarked, &objectFlag, bLevel, clauseArray);
}/*if(SATflags(v) & VisitedMask) {*/
first = 0;
}/*for(i=implied->num-1; i>=*/
if(cm->option->verbose >= 2)
fprintf(vis_stdout,"total # of RTree node:%ld\n",rm->aSize/RTnodeSize);
sat_ArrayFree(clauseArray);
FREE(fdaLit);
if(cm->option->arosat)
AS_Undo(cm,d);
else
sat_Undo(cm,d);
cm->status = SAT_UNSAT;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_GenerateCoreRecur | ( | satManager_t * | cm, |
| long | concl, | ||
| FILE * | fp, | ||
| int * | count | ||
| ) |
Function********************************************************************
Synopsis [Recursively generate the UNSAT core]
Description [Recursively generate the UNSAT core]
SideEffects [ ]
SeeAlso [ ]
Not Conflict
is CONFLICT
if(!(SATflags(concl)&NewMask)){
Definition at line 158 of file satCore.c.
{
int j;
long tmp;
satArray_t * dep;
if(!(SATflags(concl)&NewMask)){
SATflags(concl)|=NewMask;
if(!(SATflags(concl)& IsConflictMask)){
(*count)++;
sat_PrintClauseLitsForCore(cm,concl,fp);
}
else{
if(!st_lookup(cm->dependenceTable,(char *)concl, &dep)){
fprintf(cm->stdOut,"%ld is not in depe table\n",concl);
exit(0);
}
else{
for(j=0;j<dep->num; j++){
tmp = dep->space[j];
sat_GenerateCoreRecur(cm, tmp, fp, count);
}
}
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t sat_GenerateFwdIP | ( | bAig_Manager_t * | manager, |
| satManager_t * | cm, | ||
| RTnode_t | RTnode, | ||
| int | cut | ||
| ) |
Function********************************************************************
Synopsis [Generate interpolation forwardly]
Description []
SideEffects []
SeeAlso []
Definition at line 510 of file satCore.c.
{
int i;
long node, node1, left, right, result, *lp, *lp1;
int IPTrue=0, local=1, first=0, second=0, allDummy=1;
RTManager_t * rm = cm->rm;
manager->class_ = cut;
if(RT_flag(RTnode)&RT_VisitedMask){
#if DBG
assert(RT_IPnode(RTnode)!=-1);
#endif
return RT_IPnode(RTnode);
}
#if DBG
assert(RT_IPnode(RTnode)==-1);
#endif
RT_flag(RTnode) |= RT_VisitedMask;
if(RT_pivot(RTnode)==0){ /*leaf*/
#if DBG
assert(RT_left(RTnode)==RT_NULL&&RT_right(RTnode)==RT_NULL);
#endif
#if DBG
assert(RT_oriClsIdx(RTnode)==0);
#endif
if(RT_oriClsIdx(RTnode))
lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode));
else
lp = RT_formula(RTnode) + cm->rm->fArray;
lp1 = lp;
for(i=0;i<RT_fSize(RTnode);i++,lp++){
if(*lp == DUMMY)
continue;
else{
allDummy = 0;
#if DBG
assert(*lp>0);
#endif
}
if(RT_oriClsIdx(RTnode))/*is CNF*/
node = SATgetNode(*lp);
else /*is AIG*/
node = *lp;
node = SATnormalNode(node);
if(SATflags(node)&IsGlobalVarMask)
continue;
if(SATclass(node)>cut){
IPTrue = 1;
#if DBG
second = 1;
#else
break;
#endif
}
#if DBG
else{
first = 1;
}
#endif
}
#if DBG
assert(!allDummy);
assert(!(first&&second));
#endif
if(IPTrue){
RT_IPnode(RTnode) = bAig_One;
return bAig_One;
}
lp = lp1;
result = bAig_Zero;
for(i=0;i<RT_fSize(RTnode);i++,lp++){
if(RT_oriClsIdx(RTnode))/*is CNF*/
node = SATgetNode(*lp);
else /*is AIG*/
node = *lp;
node1 = SATnormalNode(node);
if(flags(node1)&IsGlobalVarMask){
result = PureSat_Or(manager,result,node);
cm->nodesArray = manager->NodesArray;
}
}
RT_IPnode(RTnode) = result;
return result;
} /*leaf*/
/*not leaf*/
else{
#if DBG
assert(RT_left(RTnode)!=RT_NULL&&RT_right(RTnode)!=RT_NULL);
#endif
left = sat_GenerateFwdIP(manager,cm,RT_left(RTnode),cut);
right = sat_GenerateFwdIP(manager,cm,RT_right(RTnode),cut);
if(RT_pivot(RTnode)<0){
int class_;
class_ = RT_pivot(RTnode)-DUMMY;
#if DBG
assert(class_>0);
#endif
if(class_>cut)
local=0;
}
else{
node = SATnormalNode(RT_pivot(RTnode));
if((SATflags(node)&IsGlobalVarMask)||
(SATclass(node)>cut))
local = 0;
}
if(local==0){
result = PureSat_And(manager,left,right);
}
else{
result = PureSat_Or(manager,left,right);
}
}/* else{ not leaf*/
cm->nodesArray = manager->NodesArray;
RT_IPnode(RTnode) = result;
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_GetDependence | ( | satManager_t * | cm, |
| long | concl, | ||
| satArray_t * | dep | ||
| ) |
Function********************************************************************
Synopsis [Generate dependence clauses for the conflict]
Description [Generate dependence clauses for the conflict]
SideEffects [ ]
SeeAlso [ ]
Definition at line 205 of file satCore.c.
{
long node, *lit, ante;
int i;
for(i=0, lit = (long*)SATfirstLit(concl); i<SATnumLits(concl);i++, lit++){
node = SATgetNode(*lit);
node = SATnormalNode(node);
ante = SATante(node);
if(ante==0){
if(!st_lookup(cm->anteTable, (char *)node, &ante)){
fprintf(vis_stdout,"ante = 0 and is not in anteTable %ld\n",node);
exit(0);
}
}
if(!(SATflags(ante)&NewMask)){
SATflags(ante)|=NewMask;
sat_ArrayInsert(dep,ante);
sat_GetDependence(cm,ante,dep);
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_ImplyArrayWithAnte | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| satArray_t * | arr | ||
| ) |
Function********************************************************************
Synopsis [Implication propogation from assertations in an array ]
Description [This funct is only for AIG assertation]
SideEffects []
SeeAlso []
Definition at line 356 of file satCore.c.
{
int i, size;
bAigEdge_t v;
int inverted, value;
satQueue_t *Q;
if(arr == 0) return;
if(cm->status)return;
size = arr->num;
Q = cm->queue;
for(i=0; i<size; i++) {
v = arr->space[i];
inverted = SATisInverted(v);
v = SATnormalNode(v);
value = !inverted;
if(SATvalue(v) < 2) {
if(SATvalue(v) == value) continue;
else {
cm->status = SAT_UNSAT;
d->conflict = v;
return;
}
}
SATvalue(v) = value;
SATmakeImplied(v, d);
SATante(v) = SATnormalNode(v);
if((SATflags(v) & InQueueMask) == 0) {
sat_Enqueue(Q, v);
SATflags(v) |= InQueueMask;
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_ImplyUnitPureLitsWithAnte | ( | satManager_t * | cm, |
| satLevel_t * | d | ||
| ) |
Function********************************************************************
Synopsis [Force implication to pure and unit literals and set antecedence of them]
Description [Force implication to pure and unit literals and set antecedence of them]
SideEffects [ ]
SeeAlso [ ]
Definition at line 412 of file satCore.c.
{
int tmp, inverted;
long node, *lit, i;
for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize){
node = i;
if((SATflags(node)&IsCNFMask)&&(SATnumLits(node)==1)){
int value;
lit = (long*)SATfirstLit(node);
tmp = SATgetNode(*lit);
inverted = SATisInverted(tmp);
tmp = SATnormalNode(tmp);
value = !inverted;
if(SATvalue(tmp) < 2) {
if(SATvalue(tmp) == value) continue;
else {
cm->status = SAT_UNSAT;
d->conflict = node;
break;
}
}
SATvalue(tmp) = !inverted;
SATmakeImplied(tmp, d);
SATante(tmp) = node;
if((SATflags(tmp) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, tmp);
SATflags(tmp) |= InQueueMask;
}
}
}
if(cm->status == SAT_UNSAT)
return;
sat_ImplyArray(cm, d, cm->pureLits);
}
Here is the call graph for this function:
| void sat_InitLayerScore | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [layer score initialization]
Description []
SideEffects []
SeeAlso []
Definition at line 1018 of file satCore.c.
{
int i,j,k,layer;
long v;
st_table *table;
st_generator * stgen, *stgen1;
satVariable_t *var;
int objExist;
int inverted;
long *plit, nv;
int size;
int count0, count1;
satArray_t *ordered, *newOrdered;
array_t * layerArray = array_alloc(st_table *,cm->LatchLevel+1);
for(k=1;k<=cm->LatchLevel;k++){
cm->assignedArray[k]=0;
cm->numArray[k]=0;
}
cm->currentLevel = cm->LatchLevel;
for(i=satNodeSize;i<cm->nodesArraySize;i+=satNodeSize){
SATflags(i)&=ResetVisited2Mask;
}
sat_MarkLayerInitState(cm,cm->InitState,cm->LatchLevel);
sat_MarkLayerProperty(cm,cm->property,cm->LatchLevel);
st_foreach_item(cm->layerTable,stgen,&table,&layer)
array_insert(st_table *,layerArray,layer,table);
for(i=cm->LatchLevel;i>=1;i--){
table = array_fetch(st_table*,layerArray,i);
st_foreach_item(table,stgen1,&v,NIL(char*)){
sat_MarkLayerLatch(cm,v,i);
}
}
array_free(layerArray);
for(i=bAigNodeSize;i<cm->nodesArraySize;i+=bAigNodeSize){
if(SATflags(i)&Visited2Mask){
int layer;
SATflags(i)&=ResetVisited2Mask;
var = SATgetVariable(i);
#if DBG
assert(var->scores[0]%SCOREUNIT==0);
#endif
layer = var->scores[0]/SCOREUNIT;
cm->numArray[layer]++;
}
}
if(cm->option->verbose >= 2){
for(i=1;i<=cm->LatchLevel;i++){
fprintf(vis_stdout,"Level %d:%d\n",i,cm->numArray[i]);
}
}
ordered = cm->orderedVariableArray;
if(ordered == 0)
ordered = sat_ArrayAlloc(cm->initNumVariables);
else
ordered->num = 0;
cm->orderedVariableArray = ordered;
objExist = 0;
for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
v = i;
if((SATflags(v) & IsBDDMask)) {
continue;
}
if((SATflags(v) & IsCNFMask)) {
size = SATnumLits(v);
plit = (long*)SATfirstLit(v);
for(j=0; j<size; j++, plit++) {
nv = SATgetNode(*plit);
inverted = !(SATisInverted(nv));
nv = SATnormalNode(nv);
var = SATgetVariable(nv);
var->litsCount[inverted]++;
}
continue;
}
if(!(SATflags(v) & CoiMask)) continue;
if(!(SATflags(v) & VisitedMask) && objExist) continue;
if(SATvalue(v) != 2 && SATlevel(v) == 0) continue;
count0 = count1 = SATnFanout(v);
if(count0 == 0 && SATleftChild(v) == 2 && SATrightChild(v) == 2) {
count0 = 0;
count1 = 0;
}
else if(SATleftChild(v) != 2) {
count0 += 2;
count1++;
}
else {
count0 += 3;
count1 += 3;
}
var = SATgetVariable(v);
var->litsCount[0] += count0;
var->litsCount[1] += count1;
sat_ArrayInsert(ordered, v);
}
for(i=0; i<cm->unitLits->num; i++) {
v = cm->unitLits->space[i];
v = SATnormalNode(v);
SATflags(v) |= NewMask;
}
if(cm->assertion) {
for(i=0; i<cm->assertion->num; i++) {
v = cm->assertion->space[i];
v = SATnormalNode(v);
SATflags(v) |= NewMask;
}
}
newOrdered = sat_ArrayAlloc((ordered->num) * 2);
size = ordered->num;
for(i=0; i<size; i++) {
v = ordered->space[i];
var = SATgetVariable(v);
var->lastLitsCount[0] = var->litsCount[0];
var->lastLitsCount[1] = var->litsCount[1];
var->scores[0] += var->lastLitsCount[0];
var->scores[1] += var->lastLitsCount[1];
if(SATflags(v) & NewMask);
else if(var->scores[0] == 0 && var->scores[1] == 0 && !(SATflags(v) & NewMask)) {
sat_ArrayInsert(cm->pureLits, (v));
}
else if(var->scores[0] == 0 && !(SATflags(v) & NewMask)) {
sat_ArrayInsert(cm->pureLits, (v));
}
else if(var->scores[1] == 0 && !(SATflags(v) & NewMask)) {
sat_ArrayInsert(cm->pureLits, SATnot(v));
}
else {
sat_ArrayInsert(newOrdered, v);
sat_ArrayInsert(newOrdered, (var->scores[0] > var->scores[1]) ? var->scores[0] : var->scores[1]);
}
}
for(i=0; i<cm->unitLits->num; i++) {
v = cm->unitLits->space[i];
v = SATnormalNode(v);
SATflags(v) &= ResetNewMask;
}
if(cm->assertion) {
for(i=0; i<cm->assertion->num; i++) {
v = cm->assertion->space[i];
v = SATnormalNode(v);
SATflags(v) &= ResetNewMask;
}
}
cm->orderedVariableArray = ordered;
size = newOrdered->num;
qsort(newOrdered->space, size>>1, sizeof(long)*2, ScoreCompare);
cm->currentVarPos = 0;
ordered->num = 0;
for(i=0; i<size; i++) {
v = newOrdered->space[i];
var = SATgetVariable(v);
var->pos = (i>>1);
sat_ArrayInsert(ordered, v);
i++;
}
sat_ArrayFree(newOrdered);
if(cm->option->verbose > 3)
sat_PrintScore(cm);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_MarkLayer | ( | satManager_t * | cm, |
| long | v, | ||
| int | layer | ||
| ) |
Function********************************************************************
Synopsis [Mark nodes in layers associated normal visible latches]
Description []
SideEffects []
SeeAlso []
Definition at line 885 of file satCore.c.
{
satVariable_t *var = SATgetVariable(v);
if((v==bAig_NULL))
return;
if(!(SATflags(v)&CoiMask)){
return;
}
/*already assigned score*/
if(SATflags(v)&Visited2Mask){
return;
}
var->scores[0] = SCOREUNIT*layer;
var->scores[1] = SCOREUNIT*layer;
SATflags(v) |= Visited2Mask;
if((SATflags(v)&StateBitMask)){
return;
}
sat_MarkLayer(cm,SATleftChild(v),layer);
sat_MarkLayer(cm,SATrightChild(v),layer);
}
Here is the caller graph for this function:
| void sat_MarkLayerInitState | ( | satManager_t * | cm, |
| long | v, | ||
| int | layer | ||
| ) |
Function********************************************************************
Synopsis [Mark nodes in layers associated with initial states]
Description []
SideEffects []
SeeAlso []
Definition at line 933 of file satCore.c.
{
satVariable_t *var = SATgetVariable(v);
if((v==bAig_NULL))
return;
if(!(SATflags(v)&CoiMask)){
return;
}
/*already assigned score*/
if(SATflags(v)&Visited2Mask){
return;
}
var->scores[0] = SCOREUNIT*layer;
var->scores[1] = SCOREUNIT*layer;
SATflags(v) |= Visited2Mask;
/*if((SATflags(v)&StateBitMask)){
fprintf(vis_stderr,"%d ISV return\n",SATnormalNode(v));
return;
}*/
sat_MarkLayerInitState(cm,SATleftChild(v),layer);
sat_MarkLayerInitState(cm,SATrightChild(v),layer);
}
Here is the caller graph for this function:
| void sat_MarkLayerLatch | ( | satManager_t * | cm, |
| long | v, | ||
| int | layer | ||
| ) |
Function********************************************************************
Synopsis [Mark nodes in layers of a certain latch aig nodes]
Description []
SideEffects []
SeeAlso []
Definition at line 980 of file satCore.c.
{
satVariable_t *var = SATgetVariable(v);
if((v==bAig_NULL))
return;
if(!(SATflags(v)&CoiMask)){
return;
}
/*not assigned score yet*/
if(!(SATflags(v)&Visited2Mask)){
var->scores[0] = SCOREUNIT*layer;
var->scores[1] = SCOREUNIT*layer;
SATflags(v) |= Visited2Mask;
}
sat_MarkLayer(cm,SATleftChild(v),layer);
sat_MarkLayer(cm,SATrightChild(v),layer);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void sat_MarkLayerProperty | ( | satManager_t * | cm, |
| long | v, | ||
| int | layer | ||
| ) |
Function********************************************************************
Synopsis [Mark nodes in layer associated with property]
Description []
SideEffects []
SeeAlso []
Definition at line 837 of file satCore.c.
{
satVariable_t *var = SATgetVariable(v);
if((v==bAig_NULL))
return;
if(!(SATflags(v)&CoiMask)){
return;
}
/*already assigned score*/
if(SATflags(v)&Visited2Mask){
return;
}
var->scores[0] = SCOREUNIT*layer;
var->scores[1] = SCOREUNIT*layer;
SATflags(v) |= Visited2Mask;
if((SATflags(v)&StateBitMask)&&
(SATclass(v)<=cm->Length)){
return;
}
sat_MarkLayerProperty(cm,SATleftChild(v),layer);
sat_MarkLayerProperty(cm,SATrightChild(v),layer);
}
Here is the caller graph for this function:
| void sat_PrintClauseLits | ( | satManager_t * | cm, |
| long | concl | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Print literals of given clauses]
Description [Print literals of given clauses]
SideEffects [ ]
SeeAlso [ ]
Definition at line 79 of file satCore.c.
{
long i, node, var_idx,*lit;
for(i=0, lit = (long*)SATfirstLit(concl); i<SATnumLits(concl);i++, lit++){
node = SATgetNode(*lit);
var_idx = SATnodeID(node);
if(SATisInverted(node))
fprintf(vis_stdout,"%ld ", -var_idx);
else
fprintf(vis_stdout,"%ld ",var_idx);
}
fprintf(vis_stdout,"0\n");
}
| void sat_PrintClauseLitsForCore | ( | satManager_t * | cm, |
| long | concl, | ||
| FILE * | fp | ||
| ) |
Function********************************************************************
Synopsis [Print literals of given clauses to a certain file for UNSAT core generation]
Description [Print literals of given clauses to a certain file for UNSAT core generation]
SideEffects [ ]
SeeAlso [ ]
cls_idx -= cm->numOfVar * satNodeSize;
cls idx starts from 0
Definition at line 111 of file satCore.c.
{
long i, node, var_idx,*lit, cls_idx;
lit = (long*)SATfirstLit(concl);
cls_idx = -(*(lit-1));
if(fp) {
cls_idx -= cm->initNumVariables * satNodeSize;
cls_idx = cls_idx/satNodeSize - 1;
fprintf(fp,"#clause index:%ld\n",cls_idx);
for(i=0, lit = (long*)SATfirstLit(concl); i<SATnumLits(concl);i++, lit++){
node = SATgetNode(*lit);
var_idx = SATnodeID(node);
if(SATisInverted(node))
fprintf(fp, "%ld ", -var_idx);
else
fprintf(fp, "%ld ",var_idx);
}
fprintf(fp, "0\n");
}
else {
if(cm->clauseIndexInCore == 0)
cm->clauseIndexInCore = sat_ArrayAlloc(1024);
sat_ArrayInsert(cm->clauseIndexInCore, cls_idx);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int ScoreCompare | ( | const void * | node1, |
| const void * | node2 | ||
| ) | [static] |
Variable Documentation
char rcsid [] UNUSED = "$Id: satCore.c,v 1.20 2009/04/12 00:14:11 fabio Exp $" [static] |
CFile***********************************************************************
FileName [satCore.c]
PackageName [sat]
Synopsis [Routines for UNSAT core generation,both CNF-based and Aig-based UNSAT core generetions are available]
Author [Bing Li]
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.]
