#include "puresatInt.h"
Include dependency graph for puresatArosat.c:
Go to the source code of this file.
Typedefs | |
| typedef int(* | ASIMPLY_FN )(satManager_t *cm, satLevel_t *d, long v, long left, long right) |
Functions | |
| static int | ScoreCompare (const void *node1, const void *node2) |
| int | AS_ImplyStop (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | AS_ImplySplit (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | AS_ImplyConflict (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | AS_ImplyLeftForward (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | AS_ImplyRightForward (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | AS_ImplyForwardOne (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | AS_ImplyPropRight (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | AS_ImplyPropRightOne (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | AS_ImplyPropLeft (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | AS_ImplyPropLeftOne (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| int | AS_ImplyPropLeftRight (satManager_t *cm, satLevel_t *d, long v, long left, long right) |
| void | AS_Undo (satManager_t *cm, satLevel_t *d) |
| void | AS_ImplyCNF (satManager_t *cm, satLevel_t *d, long v, satArray_t *wl) |
| int | AS_ImplyNode (satManager_t *cm, satLevel_t *d, long v) |
| void | AS_ImplicationMain (satManager_t *cm, satLevel_t *d) |
| void | AS_ImplyArray (satManager_t *cm, satLevel_t *d, satArray_t *arr) |
| void | AS_PreProcessing (satManager_t *cm) |
| void | AS_Backtrack (satManager_t *cm, int level) |
| void | AS_UpdateScore (satManager_t *cm) |
| void | AS_PeriodicFunctions (satManager_t *cm) |
| satLevel_t * | AS_MakeDecision (satManager_t *cm) |
| void | AS_FindUIP (satManager_t *cm, satArray_t *clauseArray, satLevel_t *d, int *objectFlag, int *bLevel, long *fdaLit) |
| int | AS_ConflictAnalysis (satManager_t *cm, satLevel_t *d) |
| void | AS_Solve (satManager_t *cm) |
| void | AS_Main (satManager_t *cm) |
| void | PureSatCreateOneLayer (Ntk_Network_t *network, PureSat_Manager_t *pm, satManager_t *cm, array_t *latchArray, int layer) |
| void | PureSatCreateLayer (Ntk_Network_t *network, PureSat_Manager_t *pm, satManager_t *cm, array_t *absModel, array_t *sufArray) |
Variables | |
| ASIMPLY_FN | ASImplicationFN [64] |
Typedef Documentation
| typedef int(* ASIMPLY_FN)(satManager_t *cm, satLevel_t *d, long v, long left, long right) |
AutomaticEnd
Definition at line 124 of file puresatArosat.c.
Function Documentation
| void AS_Backtrack | ( | satManager_t * | cm, |
| int | level | ||
| ) |
Function********************************************************************
Synopsis [backtrack procedure for arosat]
Description []
SideEffects []
SeeAlso []
Definition at line 1281 of file puresatArosat.c.
{
satLevel_t *d;
d = SATgetDecision(cm->currentDecision);
while(1) {
if(d->level <= level)
break;
AS_Undo(cm, d);
cm->currentDecision--;
if(cm->currentDecision == -1)
break;
d = SATgetDecision(cm->currentDecision);
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int AS_ConflictAnalysis | ( | satManager_t * | cm, |
| satLevel_t * | d | ||
| ) |
Function********************************************************************
Synopsis [Conflict analysis procedure]
Description []
SideEffects []
SeeAlso []
Bing : UNSAT core generation
Definition at line 1766 of file puresatArosat.c.
{
satStatistics_t *stats;
satOption_t *option;
satArray_t *clauseArray;
int objectFlag;
int bLevel;
long fdaLit, learned, conflicting;
int inverted;
RTManager_t * rm = cm->rm;
conflicting = d->conflict;
if(d->level == 0) {
if(cm->option->coreGeneration)
sat_ConflictAnalysisForCoreGen(cm, d);
cm->currentDecision--;
return (-1);
}
stats = cm->each;
option = cm->option;
stats->nBacktracks++;
clauseArray = cm->auxArray;
bLevel = 0;
fdaLit = -1;
clauseArray->num = 0;
/* Find Unique Implication Point */
AS_FindUIP(cm, clauseArray, d, &objectFlag, &bLevel, &fdaLit);
stats->nNonchonologicalBacktracks += (d->level - bLevel);
if(clauseArray->num == 0) {
sat_PrintImplicationGraph(cm, d);
sat_PrintNode(cm, conflicting);
}
/* If we could find UIP then it is critical error...
* at lease the decision node has to be detected as UIP.
*/
if(fdaLit == -1) {
fprintf(vis_stdout, "%s ERROR : Illegal unit literal\n", cm->comment);
fflush(vis_stdout);
sat_PrintNode(cm, conflicting);
sat_PrintImplicationGraph(cm, d);
sat_PrintDotForConflict(cm, d, conflicting, 0);
exit(0);
}
if(bLevel && cm->lowestBacktrackLevel > bLevel)
cm->lowestBacktrackLevel = bLevel;
inverted = SATisInverted(fdaLit);
fdaLit = SATnormalNode(fdaLit);
if(option->verbose > 2) {
if(option->verbose > 4)
sat_PrintNode(cm, conflicting);
fprintf(vis_stdout, "conflict at %3d on %6ld bLevel %d UnitLit ",
d->level, conflicting, bLevel);
sat_PrintNodeAlone(cm, fdaLit);
fprintf(vis_stdout, "\n");
}
d->conflict = 0;
/* unit literal conflict clause */
if(clauseArray->num == 1) {
learned = sat_AddUnitConflictClause(cm, clauseArray, objectFlag);
stats->nUnitConflictCl++;
cm->currentTopConflict = cm->literals->last-1;
cm->currentTopConflictCount = 0;
AS_Backtrack(cm, 0);
d = SATgetDecision(cm->currentDecision);
cm->implicatedSoFar -= d->implied->num;
SATante(fdaLit) = 0;
if(!(SATflags(SATnormalNode(fdaLit))&AssignedMask)){
satVariable_t *var = SATgetVariable(fdaLit);
int dfs = var->scores[0]/SCOREUNIT;
#if DBG
assert(dfs==cm->LatchLevel);
#endif
SATflags(SATnormalNode(fdaLit))|=AssignedMask;
cm->assignedArray[dfs]++;
if(cm->assignedArray[dfs]==cm->numArray[dfs])
sat_ASmergeLevel(cm);
}
SATvalue(fdaLit) = inverted;
SATmakeImplied(fdaLit, d);
if((SATflags(fdaLit) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, fdaLit);
SATflags(fdaLit) |= InQueueMask;
}
clauseArray->num = 0;
if(option->incTraceObjective && objectFlag == 0)
sat_ArrayInsert(cm->nonobjUnitLitArray, SATnot(fdaLit));
if(option->incDistill && objectFlag)
sat_ArrayInsert(cm->objUnitLitArray, SATnot(fdaLit));
if(objectFlag)
SATflags(fdaLit) |= ObjMask;
/* Bing: UNSAT core generation */
if(cm->option->coreGeneration){
st_insert(cm->anteTable,(char*)SATnormalNode(fdaLit),(char*)learned);
st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
RT_oriClsIdx(rm->root) = learned;
}
return(bLevel);
}
/* add conflict learned clause */
learned = sat_AddConflictClause(cm, clauseArray, objectFlag);
cm->currentTopConflict = cm->literals->last-1;
cm->currentTopConflictCount = 0;
/* Bing: UNSAT core generation */
if(cm->option->coreGeneration){
st_insert(cm->RTreeTable, (char *)learned, (char *)rm->root);
RT_oriClsIdx(rm->root) = learned;
}
if(option->verbose > 2) {
sat_PrintNode(cm, learned);
fflush(vis_stdout);
}
/* apply Deepest Variable Hike decision heuristic */
if(option->decisionHeuristic & DVH_DECISION)
sat_UpdateDVH(cm, d, clauseArray, bLevel, fdaLit);
/* Backtrack and failure driven assertion */
AS_Backtrack(cm, bLevel);
d = SATgetDecision(bLevel);
cm->implicatedSoFar -= d->implied->num;
if(!(SATflags(SATnormalNode(fdaLit))&AssignedMask)){
satVariable_t *var = SATgetVariable(fdaLit);
int dfs = var->scores[0]/SCOREUNIT;
#if DBG
assert(dfs==cm->LatchLevel);
#endif
SATflags(SATnormalNode(fdaLit))|=AssignedMask;
cm->assignedArray[dfs]++;
if(cm->assignedArray[dfs]==cm->numArray[dfs])
sat_ASmergeLevel(cm);
}
SATante(fdaLit) = learned;
SATvalue(fdaLit) = inverted;
SATmakeImplied(fdaLit, d);
if((SATflags(fdaLit) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, fdaLit);
SATflags(fdaLit) |= InQueueMask;
}
clauseArray->num = 0;
if(objectFlag)
SATflags(fdaLit) |= ObjMask;
return(bLevel);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void AS_FindUIP | ( | satManager_t * | cm, |
| satArray_t * | clauseArray, | ||
| satLevel_t * | d, | ||
| int * | objectFlag, | ||
| int * | bLevel, | ||
| long * | fdaLit | ||
| ) |
Function********************************************************************
Synopsis [Find UIP for generating conflict clauses]
Description []
SideEffects []
SeeAlso []
Definition at line 1540 of file puresatArosat.c.
{
long conflicting;
int nMarked, value;
int first, i,j;
long *space, v,left,right,inverted,result,*tmp;
satArray_t *implied;
satOption_t *option;
RTnode_t tmprt;
int size = 0;
long *lp, *tmpIP,ante,ante2,node;
RTManager_t * rm = cm->rm;
conflicting = d->conflict;
nMarked = 0;
option = cm->option;
if(option->incTraceObjective) *objectFlag = 0;
else *objectFlag = ObjMask;
(*objectFlag) |= (SATflags(conflicting) & ObjMask);
/* find seed from conflicting clause to find unique implication point.
* */
clauseArray->num = 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;
}
}
/*CNF but not conflict*/
else{
rm->root = RTCreateNode(rm);
RT_oriClsIdx(rm->root) = conflicting;
size = SATnumLits(conflicting);
RT_fSize(rm->root) = size;
}
}
/*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);
}
}
for(i=implied->num-1; i>=0; i--, space--) {
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;
}
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;
}
}
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++;
}
}
/*generate p1 and p2*/
lp = tmp;
sat_BuildRT(cm,tmprt,lp,tmpIP,size,1);
FREE(tmp);
}
/* left is CNF*/
else{
RT_oriClsIdx(tmprt) = ante;
//generate p1 and p2 for left
lp = (long*)SATfirstLit(ante);
size = SATnumLits(ante);
RT_fSize(tmprt) = size;
}
} /*else{ if not conflict CNF*/
}/*if(cm->option->coreGeneration){*/
sat_MarkNodeInImpliedNode(
cm, d, v, &nMarked, objectFlag, bLevel, clauseArray);
/*Bing:Important for EffIP*/
first = 0;
}
/* first = 0;*/
}
/* Minimize conflict clause */
if(option->minimizeConflictClause)
sat_MinimizeConflictClause(cm, clauseArray);
else
sat_ResetFlagForClauseArray(cm, clauseArray);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void AS_ImplicationMain | ( | satManager_t * | cm, |
| satLevel_t * | d | ||
| ) |
Function********************************************************************
Synopsis [The main procedure of implication propogation]
Description []
SideEffects []
SeeAlso []
Definition at line 1038 of file puresatArosat.c.
{
satQueue_t *Q, *BDDQ;
long v;
Q = cm->queue;
BDDQ = cm->BDDQueue;
while(1) {
v = sat_Dequeue(Q);
while(v && d->conflict == 0) {
AS_ImplyNode(cm, d, v);
SATflags(v) &= ResetInQueueMask;
v = sat_Dequeue(Q);
}
if(d->conflict)
break;
if(cm->option->BDDImplication) {
v = sat_Dequeue(Q);
while(v && d->conflict == 0) {
sat_ImplyBDD(cm, d, v);
SATflags(v) &= ResetInQueueMask;
v = sat_Dequeue(Q);
}
}
if(Q->size == 0 && BDDQ->size == 0)
break;
}
sat_CleanImplicationQueue(cm);
cm->implicatedSoFar += d->implied->num;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void AS_ImplyArray | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| satArray_t * | arr | ||
| ) |
Function********************************************************************
Synopsis [Implication for assertation in one array]
Description []
SideEffects []
SeeAlso []
Definition at line 1092 of file puresatArosat.c.
{
int i, size;
long v;
int inverted, value;
satQueue_t *Q;
satVariable_t *var;
int dfs;
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;
}
}
var = SATgetVariable(v);
dfs = var->scores[0]/SCOREUNIT;
if(dfs==cm->LatchLevel){
if(!(SATflags(SATnormalNode(v))&AssignedMask)){
SATflags(SATnormalNode(v))|=AssignedMask;
cm->assignedArray[dfs]++;
#if DBG
assert(cm->assignedArray[dfs]<=cm->numArray[dfs]);
#endif
if(cm->assignedArray[dfs]==cm->numArray[dfs])
sat_ASmergeLevel(cm);
}
}
SATvalue(v) = value;
SATmakeImplied(v, d);
if(cm->option->coreGeneration){
st_insert(cm->anteTable,(char *)SATnormalNode(v),(char *)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 AS_ImplyCNF | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| satArray_t * | wl | ||
| ) |
Function********************************************************************
Synopsis [implication for cnf]
Description []
SideEffects []
SeeAlso []
conflict happens
implication
to identify the objective dependent clause for incremental SAT
move watched literal
Definition at line 804 of file puresatArosat.c.
{
int size, i, j;
long *space;
long lit, *plit, *tplit;
int dir;
long nv, tv, *oplit, *wlit;
int isInverted, value;
int tsize, inverted;
long cur, clit;
satStatistics_t *stats;
satOption_t *option;
satQueue_t *Q;
satVariable_t *var;
long tmpv;
size = wl->num;
space = wl->space;
Q = cm->queue;
stats = cm->each;
option = cm->option;
nv = 0;
wlit = 0;
for(i=0; i<size; i++) {
plit = (long*)space[i];
if(plit == 0 || *plit == 0) {
size--;
space[i] = space[size];
i--;
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);
tmpv = tv;
isInverted = SATisInverted(tv);
tv = SATnormalNode(tv);
value = SATvalue(tv) ^ isInverted;
if(value == 0) {
d->conflict = nv;
wl->num = size;
return;
}
else if(value > 1) {
if(sat_ASImp(cm,d,tmpv,!isInverted))
break;
SATvalue(tv) = !isInverted;
SATmakeImplied(tv, d);
SATante(tv) = nv;
if((SATflags(tv) & InQueueMask) == 0) {
sat_Enqueue(Q, tv);
SATflags(tv) |= InQueueMask;
}
stats->nCNFImplications++;
if(option->incTraceObjective == 1) {
tsize = SATnumLits(nv);
for(j=0, tplit=(long*)SATfirstLit(nv); j<tsize; j++, tplit++) {
cur = SATgetNode(*tplit);
cur = SATnormalNode(cur);
if(SATflags(cur) & ObjMask) {
SATflags(tv) |= ObjMask;
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;
if(value == 1) {
break;
}
continue;
}
if(value == 0)
continue;
SATunsetWL(plit);
size--;
space[i] = space[size];
i--;
var = SATgetVariable(tv);
SATsetWL(oplit, dir);
inverted = !inverted;
if(var->wl[inverted]) {
sat_ArrayInsert(var->wl[inverted], (long)oplit);
}
else {
var->wl[inverted] = sat_ArrayAlloc(4);
sat_ArrayInsert(var->wl[inverted], (long)oplit);
}
break;
}
}
wl->num = size;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int AS_ImplyConflict | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [The conflict happens.]
Description [The conflict happens when 0 1 1 1 1 | | | | | --- --- --- --- --- / \ / \ / \ / \ / \ 1 1 X 0 0 X 1 0 0 1 ]
SideEffects []
SeeAlso []
Definition at line 277 of file puresatArosat.c.
{
if(left != 2) {
d->conflict = SATnormalNode(v);
}
return(0);
}
| int AS_ImplyForwardOne | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [A value implied to output due to both child.]
Description [A value implied to output due to both child X | --- / \ 1 1 ]
SideEffects []
SeeAlso []
Definition at line 400 of file puresatArosat.c.
{
if(sat_ASImp(cm,d,v,1))
return(0);
v = SATnormalNode(v);
left = SATnormalNode(left);
right = SATnormalNode(right);
SATvalue(v) = 1;
SATmakeImplied(v, d);
SATante(v) = right;
SATante2(v) = left;
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
SATflags(v) |= (SATflags(right) & ObjMask);
SATflags(v) |= (SATflags(left) & ObjMask);
cm->each->nAigImplications++;
return(0);
}
Here is the call graph for this function:
| int AS_ImplyLeftForward | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [A value implied to output due to left child.]
Description [A value implied to output due to left child X X | | --- --- / \ / \ 0 1 0 X ]
SideEffects []
SeeAlso []
Definition at line 309 of file puresatArosat.c.
{
if(sat_ASImp(cm,d,v,0))
return(0);
v = SATnormalNode(v);
left = SATnormalNode(left);
SATvalue(v) = 0;
SATmakeImplied(v, d);
SATante(v) = left;
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
SATflags(v) |= (SATflags(left) & ObjMask);
cm->each->nAigImplications++;
return(0);
}
Here is the call graph for this function:
| int AS_ImplyNode | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v | ||
| ) |
Function********************************************************************
Synopsis [implication for aig node and cnf ]
Description []
SideEffects []
SeeAlso []
implcation on CNF
implication on AIG
Definition at line 960 of file puresatArosat.c.
{
long *fan, cur;
int value;
int i, size;
long left, right;
satVariable_t *var;
satArray_t *wlArray;
value = SATvalue(v) ^ 1;
var = SATgetVariable(v);
wlArray = var->wl[value];
if(wlArray && wlArray->size) {
AS_ImplyCNF(cm, d, v, wlArray);
}
if(d->conflict)
return(0);
fan = (long *)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);
value = SATgetValue(left, right, cur);
#if DBG
assert(SATflags(SATnormalNode(left))&CoiMask);
assert(SATflags(SATnormalNode(right))&CoiMask);
#endif
(ASImplicationFN[value])(cm, d, cur, left, right);
if(d->conflict)
return(0);
}
left = SATleftChild(v);
right = SATrightChild(v);
value = SATgetValue(left, right, v);
#if DBG
assert(left==bAig_NULL||SATflags(SATnormalNode(left))&CoiMask);
assert(right==bAig_NULL||SATflags(SATnormalNode(right))&CoiMask);
#endif
(ASImplicationFN[value])(cm, d, v, left, right);
if(d->conflict)
return(0);
return(1);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int AS_ImplyPropLeft | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [A value implied to left child due to both output and right.]
Description [A value implied to left child due to both output and right 0 | --- / \ X 1 ]
SideEffects []
SeeAlso []
Definition at line 553 of file puresatArosat.c.
{
int isInverted;
if(sat_ASImp(cm,d,left,SATisInverted(left)))
return(0);
isInverted = SATisInverted(left);
v = SATnormalNode(v);
left = SATnormalNode(left);
right = SATnormalNode(right);
SATmakeImplied(left, d);
SATante(left) = v;
SATante2(left) = right;
SATvalue(left) = isInverted;
sat_Enqueue(cm->queue, left);
SATflags(left) |= InQueueMask;
SATflags(left) |= (SATflags(v) & ObjMask);
SATflags(left) |= (SATflags(right) & ObjMask);
cm->each->nAigImplications++;
return(0);
}
Here is the call graph for this function:
| int AS_ImplyPropLeftOne | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [A value implied to left child due to both output and right.]
Description [A value implied to left child due to both output and right 1 | --- / \ X 1 ]
SideEffects []
SeeAlso []
Definition at line 608 of file puresatArosat.c.
{
int isInverted;
if(sat_ASImp(cm,d,left,!SATisInverted(left)))
return(0);
isInverted = SATisInverted(left);
v = SATnormalNode(v);
left = SATnormalNode(left);
right = SATnormalNode(right);
SATmakeImplied(left, d);
SATante(left) = v;
SATvalue(left) = !isInverted;
sat_Enqueue(cm->queue, left);
SATflags(left) |= InQueueMask;
SATflags(left) |= (SATflags(v) & ObjMask);
cm->each->nAigImplications++;
return(0);
}
Here is the call graph for this function:
| int AS_ImplyPropLeftRight | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [A value implied to left and right child due to output.]
Description [A value implied to left and right child due to output 1 | --- / \ X X ]
SideEffects []
SeeAlso []
Definition at line 661 of file puresatArosat.c.
{
int isLeftInverted;
int isRightInverted;
int lImp=1,rImp=1;
if(left == right) return 1;
if(sat_ASImp(cm,d,left,!SATisInverted(left)))
lImp = 0;
if(sat_ASImp(cm,d,right,!SATisInverted(right)))
rImp = 0;
isLeftInverted = SATisInverted(left);
isRightInverted = SATisInverted(right);
v = SATnormalNode(v);
left = SATnormalNode(left);
right = SATnormalNode(right);
if(lImp){
SATmakeImplied(left, d);
SATante(left) = v;
SATvalue(left) = !isLeftInverted;
sat_Enqueue(cm->queue, left);
SATflags(left) |= InQueueMask;
SATflags(left) |= (SATflags(v) & ObjMask);
cm->each->nAigImplications ++;
}
if(rImp){
SATmakeImplied(right, d);
SATante(right) = v;
SATvalue(right) = !isRightInverted;
sat_Enqueue(cm->queue, right);
SATflags(right) |= InQueueMask;
SATflags(right) |= (SATflags(v) & ObjMask);
cm->each->nAigImplications ++;
}
return(0);
}
Here is the call graph for this function:
| int AS_ImplyPropRight | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [A value implied to right child due to both output and left.]
Description [A value implied to right child due to both output and left 0 | --- / \ 1 X ]
SideEffects []
SeeAlso []
Definition at line 448 of file puresatArosat.c.
{
int isInverted;
isInverted = SATisInverted(right);
if(sat_ASImp(cm,d,right, isInverted))
return(0);
v = SATnormalNode(v);
left = SATnormalNode(left);
right = SATnormalNode(right);
SATmakeImplied(right, d);
SATvalue(right) = isInverted;
SATante(right) = left;
SATante2(right) = v;
sat_Enqueue(cm->queue, right);
SATflags(right) |= InQueueMask;
SATflags(right) |= (SATflags(left) & ObjMask);
SATflags(right) |= (SATflags(v) & ObjMask);
cm->each->nAigImplications++;
return(0);
}
Here is the call graph for this function:
| int AS_ImplyPropRightOne | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [A value implied to right child due to both output and left.]
Description [A value implied to right child due to both output and left 1 | --- / \ 1 X ]
SideEffects []
SeeAlso []
Definition at line 501 of file puresatArosat.c.
{
int isInverted;
if(sat_ASImp(cm,d,right,!SATisInverted(right)))
return(0);
isInverted = SATisInverted(right);
v = SATnormalNode(v);
left = SATnormalNode(left);
right = SATnormalNode(right);
SATmakeImplied(right, d);
SATante(right) = v;
SATvalue(right) = !isInverted;
sat_Enqueue(cm->queue, right);
SATflags(right) |= InQueueMask;
SATflags(right) |= (SATflags(v) & ObjMask);
cm->each->nAigImplications++;
return(0);
}
Here is the call graph for this function:
| int AS_ImplyRightForward | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [A value implied to output due to right child.]
Description [A value implied to output due to right child X X | | --- --- / \ / \ 1 0 X 0 ]
SideEffects []
SeeAlso []
Definition at line 354 of file puresatArosat.c.
{
if(sat_ASImp(cm,d,v,0))
return(0);
v = SATnormalNode(v);
right = SATnormalNode(right);
SATvalue(v) = 0;
SATmakeImplied(v, d);
SATante(v) = right;
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
SATflags(v) |= (SATflags(right) & ObjMask);
cm->each->nAigImplications++;
return(0);
}
Here is the call graph for this function:
| int AS_ImplySplit | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [No further implcation when this function is called.]
Description [No further implcation when this function is called. and need split on output. 0 | --- / \ X X ]
SideEffects []
SeeAlso []
Definition at line 249 of file puresatArosat.c.
{
return(0);
}
| int AS_ImplyStop | ( | satManager_t * | cm, |
| satLevel_t * | d, | ||
| long | v, | ||
| long | left, | ||
| long | right | ||
| ) |
Function********************************************************************
Synopsis [No further implcation when this function is called.]
Description [No further implcation when this function is called. 0 0 0 1 | | | | --- --- --- --- / \ / \ / \ / \ 0 X X 0 0 0 1 1 ]
SideEffects []
SeeAlso []
Definition at line 220 of file puresatArosat.c.
{
return(0);
}
| void AS_Main | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [The main procedure of AROSAT solver]
Description []
SideEffects []
SeeAlso []
Bing: UNSAT core generation
Definition at line 2063 of file puresatArosat.c.
{
long btime, etime;
btime = util_cpu_time();
AS_PreProcessing(cm);
if(cm->status == 0)
AS_Solve(cm);
if(cm->option->coreGeneration && cm->status == SAT_UNSAT){
sat_GenerateCore_All(cm);
}
sat_PostProcessing(cm);
etime = util_cpu_time();
cm->each->satTime = (double)(etime - btime) / 1000.0 ;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| satLevel_t* AS_MakeDecision | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [Decision procedure]
Description []
SideEffects []
SeeAlso []
Definition at line 1465 of file puresatArosat.c.
{
satLevel_t *d;
int value;
long v;
satStatistics_t *stats;
d = SATgetDecision(cm->currentDecision);
if(cm->queue->size)
return(d);
d = sat_AllocLevel(cm);
v = 0;
v = sat_DecisionBasedOnBDD(cm, d);
if(v == 0)
v = sat_DecisionBasedOnScore(cm, d);
if(v == 0)
return(0);
sat_ASDec(cm,d,v);
stats = cm->each;
stats->nDecisions++;
value = !(SATisInverted(v));
v = SATnormalNode(v);
d->decisionNode = v;
if((SATgetVariable(v)->RecVal)!=0){
if(SATgetVariable(v)->RecVal==-1)
value=0;
else{
#if DBG
assert(SATgetVariable(v)->RecVal==1);
#endif
value=1;
}
}
SATvalue(v) = value;
SATmakeImplied(v, d);
#if DBG
assert(SATflags(v)&CoiMask);
#endif
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
return(d);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void AS_PeriodicFunctions | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [Periodically executed operations]
Description []
SideEffects []
SeeAlso []
Definition at line 1415 of file puresatArosat.c.
{
satStatistics_t *stats;
satOption_t *option;
int nDecisions;
int gap;
stats = cm->each;
option = cm->option;
nDecisions = stats->nDecisions-stats->nShrinkDecisions;
if(nDecisions && !(nDecisions % option->decisionAgeInterval)) {
if(option->decisionAgeRestart) {
gap = stats->nConflictCl-stats->nOldConflictCl;
if(gap > option->decisionAgeInterval>>2) {
AS_UpdateScore(cm);
AS_Backtrack(cm, cm->lowestBacktrackLevel);
cm->currentTopConflict = cm->literals->last-1;
cm->currentTopConflictCount = 0;
cm->lowestBacktrackLevel = MAXINT;
}
stats->nOldConflictCl = stats->nConflictCl;
}
else {
AS_UpdateScore(cm);
}
}
if(stats->nBacktracks > option->nextClauseDeletion) {
option->nextClauseDeletion += option->clauseDeletionInterval;
sat_ClauseDeletion(cm);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void AS_PreProcessing | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [Preprocessing step for AROSAT]
Description []
SideEffects []
SeeAlso []
create implication queue
create variable array : one can reduce size of variable array using mapping. for fanout free internal node....
create decision stack
to avoid purify warning
incremental SAT....
Level 0 decision....
Definition at line 1170 of file puresatArosat.c.
{
satLevel_t *d;
cm->queue = sat_CreateQueue(1024);
cm->BDDQueue = sat_CreateQueue(1024);
cm->unusedAigQueue = sat_CreateQueue(1024);
if(cm->variableArray == 0) {
cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
memset(cm->variableArray, 0,
sizeof(satVariable_t) * (cm->initNumVariables+1));
}
cm->auxArray = sat_ArrayAlloc(1024);
cm->nonobjUnitLitArray = sat_ArrayAlloc(128);
cm->objUnitLitArray = sat_ArrayAlloc(128);
if(cm->option->AbRf == 0)
sat_CompactFanout(cm);
/*assign initial layer score to variables*/
sat_InitLayerScore(cm);
if(cm->decisionHeadSize == 0) {
cm->decisionHeadSize = 32;
cm->decisionHead = ALLOC(satLevel_t, cm->decisionHeadSize);
memset(cm->decisionHead, 0, sizeof(satLevel_t) * cm->decisionHeadSize);
}
cm->currentDecision = -1;
SATvalue(2) = 2;
SATflags(0) = 0;
cm->initNodesArraySize = cm->nodesArraySize;
cm->beginConflict = cm->nodesArraySize;
if(cm->option->incTraceObjective) {
sat_RestoreForwardedClauses(cm, 0);
}
else if(cm->option->incAll) {
sat_RestoreForwardedClauses(cm, 1);
}
if(cm->option->incTraceObjective) {
sat_MarkObjectiveFlagToArray(cm, cm->obj);
sat_MarkObjectiveFlagToArray(cm, cm->objCNF);
}
d = sat_AllocLevel(cm);
sat_ApplyForcedAssignmentMain(cm, d);
if(cm->status == SAT_UNSAT)
return;
if(cm->option->coreGeneration){
cm->rm = ALLOC(RTManager_t, 1);
memset(cm->rm,0,sizeof(RTManager_t));
}
AS_ImplyArray(cm, d, cm->auxObj);
AS_ImplyArray(cm, d, cm->obj);
AS_ImplyArray(cm,d,cm->assertArray);
AS_ImplicationMain(cm, d);
if(d->conflict) {
cm->status = SAT_UNSAT;
}
if(cm->status == 0) {
if(cm->option->incDistill) {
sat_IncrementalUsingDistill(cm);
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void AS_Solve | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [Main solving procedure]
Description []
SideEffects []
SeeAlso []
Definition at line 1973 of file puresatArosat.c.
{
satLevel_t *d;
satOption_t *option;
satVariable_t *var;
int level;
d = SATgetDecision(0);
cm->implicatedSoFar = d->implied->num;
cm->currentTopConflict = 0;
option = cm->option;
if(option->BDDMonolithic) {
sat_TryToBuildMonolithicBDD(cm);
}
if(cm->status == SAT_UNSAT) {
AS_Undo(cm, SATgetDecision(0));
return;
}
while(1) {
AS_PeriodicFunctions(cm);
if(cm->currentDecision == 0)
sat_BuildLevelZeroHyperImplicationGraph(cm);
d = AS_MakeDecision(cm);
if(d == 0) {
cm->status = SAT_SAT;
return;
}
while(1) {
AS_ImplicationMain(cm, d);
if(d->conflict == 0) {
if(cm->option->verbose > 2) {
var = SATgetVariable(d->decisionNode);
fprintf(vis_stdout, "decision at %3d on %6ld <- %ld score(%d %d) %d %ld implied %.3f %%\n",
d->level, d->decisionNode, SATvalue(d->decisionNode),
var->scores[0], var->scores[1],
cm->each->nDecisions, d->implied->num,
(double)cm->implicatedSoFar/(double)cm->initNumVariables * 100);
fflush(vis_stdout);
}
break;
}
if(cm->option->verbose > 2) {
var = SATgetVariable(d->decisionNode);
fprintf(vis_stdout, "decision at %3d on %6ld <- %ld score(%d %d) %d %ld implied %.3f %% Conflict\n",
d->level, d->decisionNode, SATvalue(d->decisionNode),
var->scores[0], var->scores[1],
cm->each->nDecisions, d->implied->num,
(double)cm->implicatedSoFar/(double)cm->initNumVariables * 100);
fflush(vis_stdout);
}
level = AS_ConflictAnalysis(cm, d);
if(cm->currentDecision == -1) {
if(cm->option->incDistill) {
sat_BuildTrieForDistill(cm);
}
AS_Undo(cm, SATgetDecision(0));
cm->status = SAT_UNSAT;
return;
}
d = SATgetDecision(cm->currentDecision);
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void AS_Undo | ( | satManager_t * | cm, |
| satLevel_t * | d | ||
| ) |
Function********************************************************************
Synopsis [erase previous assignments by arosat]
Description []
SideEffects []
SeeAlso []
Definition at line 725 of file puresatArosat.c.
{
satArray_t *implied, *satisfied;
int size, i;
long *space, v;
satVariable_t *var;
int dfs;
implied = d->implied;
space = implied->space;
size = implied->num;
for(i=0; i<size; i++, space++) {
v = *space;
SATvalue(v) = 2;
SATflags(v) &= ResetNewVisitedObjInQueueMask;
SATante(v) = 0;
SATante2(v) = 0;
SATlevel(v) = -1;
if(SATflags(SATnormalNode(v))&AssignedMask){
SATflags(SATnormalNode(v))&=ResetAssignedMask;
var=SATgetVariable(v);
dfs = var->scores[0]/SCOREUNIT;
cm->assignedArray[dfs]--;
#if DBG
assert(cm->assignedArray[dfs]>=0);
#endif
}
}
cm->implicatedSoFar -= size;
if(d->satisfied) {
satisfied = d->implied;
space = satisfied->space;
size = satisfied->num;
for(i=0; i<size; i++, space++) {
v = *space;
SATflags(v) &= ResetBDDSatisfiedMask;
}
d->satisfied->num = 0;
}
if(d->level > 0) {
if((cm->decisionHead[d->level-1]).currentVarPos < cm->currentVarPos)
cm->currentVarPos = (cm->decisionHead[d->level-1]).currentVarPos;
}
else
cm->currentVarPos = d->currentVarPos;
d->implied->num = 0;
d->currentVarPos = 0;
d->conflict = 0;
}
Here is the caller graph for this function:
| void AS_UpdateScore | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [procedure for updating score]
Description []
SideEffects []
SeeAlso []
Definition at line 1317 of file puresatArosat.c.
{
satArray_t *one, *tmp;
satArray_t *ordered;
satVariable_t *var;
int size, i;
long v;
int value;
int baseScore,realScore,newNum;
ordered = cm->orderedVariableArray;
one = sat_ArrayAlloc(ordered->num);
tmp = sat_ArrayAlloc(ordered->num);
size = ordered->num;
for(i=0; i<size; i++) {
v = ordered->space[i];
if(SATvalue(v) < 2 && SATlevel(v) == 0)
continue;
var = SATgetVariable(v);
baseScore =(var->scores[0]/SCOREUNIT)*SCOREUNIT;
realScore = var->scores[0]%SCOREUNIT;
newNum = var->litsCount[0] - var->lastLitsCount[0];
var->scores[0] = baseScore + (realScore>>1) + newNum;
baseScore =(var->scores[1]/SCOREUNIT)*SCOREUNIT;
realScore = var->scores[1]%SCOREUNIT;
newNum = var->litsCount[1] - var->lastLitsCount[1];
var->scores[1] = baseScore + (realScore>>1) + newNum;
var->lastLitsCount[0] = var->litsCount[0];
var->lastLitsCount[1] = var->litsCount[1];
if((var->scores[0] + var->scores[1]) < 1) {
sat_ArrayInsert(one, v);
}
else {
value = (var->scores[0] > var->scores[1]) ? var->scores[0] : var->scores[1];
sat_ArrayInsert(tmp, v);
sat_ArrayInsert(tmp, value);
}
}
qsort(tmp->space, (tmp->num)>>1, sizeof(long)*2, ScoreCompare);
ordered->num = 0;
size = tmp->num;
for(i=0; i<size; i++) {
v = tmp->space[i];
sat_ArrayInsert(ordered, v);
var = SATgetVariable(v);
var->pos = (i>>1);
i++;
}
size = one->num;
for(i=0; i<size; i++) {
v = one->space[i];
var = SATgetVariable(v);
var->pos = ordered->num;
sat_ArrayInsert(ordered, v);
}
sat_ArrayFree(one);
sat_ArrayFree(tmp);
cm->orderedVariableArray = ordered;
cm->currentVarPos = 0;
for(i=1; i<cm->currentDecision; i++) {
cm->decisionHead[i].currentVarPos = 0;
}
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 PureSatCreateLayer | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| satManager_t * | cm, | ||
| array_t * | absModel, | ||
| array_t * | sufArray | ||
| ) |
Function********************************************************************
Synopsis [Create all the layers]
Description []
SideEffects []
SeeAlso []
Definition at line 2183 of file puresatArosat.c.
{
int layer;
char* name;
int i,j,threshold;
array_t *tmpArray;
if(sufArray->num<4)
layer = 1;
else if(sufArray->num<6)
layer = 2;
else if(sufArray->num<10)
layer = 3;
else if(sufArray->num<20)
layer = 5;
else if(sufArray->num<50)
layer = 8;
else
layer = 10;
threshold = sufArray->num/layer;
layer = array_n(sufArray)/threshold;
layer = sufArray->num%threshold?layer+1:layer;
cm->LatchLevel = layer;
cm->OriLevel = layer;
cm->layerTable = st_init_table(st_ptrcmp,st_ptrhash);
layer = layer+1;
for(i=0;i<array_n(sufArray);i=i+threshold){
if(i==0)
tmpArray = array_dup(absModel);
else
tmpArray = array_alloc(char*,0);
layer = layer-1;
for(j=0;j<threshold;j++){
if(i+j>=array_n(sufArray))
break;
name = array_fetch(char*,sufArray,i+j);
array_insert_last(char*,tmpArray,name);
}
PureSatCreateOneLayer(network,pm,cm,tmpArray,layer);
array_free(tmpArray);
}
assert(layer==1);
cm->assignedArray = ALLOC(int,cm->LatchLevel+1);
cm->numArray = ALLOC(int,cm->LatchLevel+1);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatCreateOneLayer | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| satManager_t * | cm, | ||
| array_t * | latchArray, | ||
| int | layer | ||
| ) |
Function********************************************************************
Synopsis [Create one layer for AROSAT]
Description []
SideEffects []
SeeAlso []
Definition at line 2100 of file puresatArosat.c.
{
mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
MVFAIG_NETWORK_APPL_KEY);
MvfAig_Function_t *mvfAig;
bAigTimeFrame_t * tf = manager->timeframeWOI;
mAigMvar_t lmVar;
mAigBvar_t bVar;
array_t *bVarList,*mVarList;
int i,j,k,lmAigId,index,index1;
char * name;
Ntk_Node_t * latch;
bAigEdge_t node,v, *li, *bli;
st_table *table = st_init_table(st_numcmp,st_numhash);
bVarList = mAigReadBinVarList(manager);
mVarList = mAigReadMulVarList(manager);
arrayForEachItem(char*,latchArray,i,name){
latch = Ntk_NetworkFindNodeByName(network,name);
st_lookup(node2MvfAigTable,latch,&mvfAig);
for(j=0;j<mvfAig->num;j++){
int retVal;
v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
if(v==bAig_Zero||v==bAig_One)
continue;
retVal = st_lookup(tf->li2index,(char *)v,&index);
assert(retVal);
for(k=1;k<=pm->Length;k++){
li = tf->latchInputs[k];
if(li[index]==bAig_Zero||li[index]==bAig_One)
continue;
node = bAig_NonInvertedEdge(li[index]);
st_insert(table,(char*)node,(char*)(long)layer);
}
}
lmAigId = Ntk_NodeReadMAigId(latch);
lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
int retVal;
bVar = array_fetch(mAigBvar_t,bVarList,index1);
if(bVar.node==bAig_Zero||bVar.node==bAig_One)
continue;
retVal = st_lookup(tf->bli2index,(char *)bVar.node,&index);
assert(retVal);
for(k=1;k<=pm->Length;k++){
bli = tf->blatchInputs[k];
if(bli[index]==bAig_Zero||bli[index]==bAig_One)
continue;
node = bAig_NonInvertedEdge(bli[index]);
st_insert(table,(char*)node,(char*)(long)layer);
}
}
}
st_insert(cm->layerTable,table,(char*)(long)layer);
}
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] |
CFile***********************************************************************
FileName [puresatArosat.c]
PackageName [puresat]
Synopsis [Abstraction refinement for large scale invariant checking.]
Description [This file contains the functions to check invariant properties by the PureSAT abstraction refinement algorithm, which is entirely based on SAT solver, the input of which could be either CNF or AIG. It has several parts:
Localization-reduction base Abstraction K-induction or interpolation to prove the truth of a property Bounded Model Checking to find bugs Incremental concretization based methods to verify abstract bugs Incremental SAT solver to improve efficiency UNSAT proof based method to obtain refinement AROSAT to bring in only necessary latches into unsat proofs Bridge abstraction to get compact coarse refinement Refinement minization to guarrantee minimal refinements Unsat proof-based refinement minimization to eliminate multiple candidate by on SAT test Refinement prediction to decrease the number of refinement iterations Dynamic switching to redistribute computional resources to improve efficiency
For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", " Abstraction in symbolic model checking using satisfiability as the only decision procedure", "Efficient computation of small abstraction refinements", and "Efficient abstraction refinement in interpolation-based unbounded model checking"]
Author [Bing Li]
Copyright [Copyright (c) 2004 The Regents of the Univ. of Colorado. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.]AutomaticStart Function********************************************************************
Synopsis [comparing score for sorting]
Description []
SideEffects []
SeeAlso []
Definition at line 92 of file puresatArosat.c.
{
int v1;
int v2;
int s1, s2;
v1 = *(int *)(node1);
v2 = *(int *)(node2);
s1 = *((int *)(node1) + 1);
s2 = *((int *)(node2) + 1);
if(s1 == s2) {
return(v1 > v2);
}
return(s1 < s2);
}
Here is the caller graph for this function:
Variable Documentation
Definition at line 127 of file puresatArosat.c.
