#include "baig.h"#include "baigInt.h"#include "ntk.h"#include "bmc.h"#include "sat.h"
Include dependency graph for baigAllSat.c:
Go to the source code of this file.
Functions | |
| static int | nodenameCompare (const void *node1, const void *node2) |
| static int | levelCompare (const void *node1, const void *node2) |
| static int | indexCompare (const void *node1, const void *node2) |
| static int | StringCheckIsInteger (char *string, int *value) |
| bAigTransition_t * | bAigCreateTransitionRelation (Ntk_Network_t *network, mAig_Manager_t *manager) |
| bAigEdge_t | bAig_CreatebAigForInvariant (Ntk_Network_t *network, bAig_Manager_t *manager, Ctlsp_Formula_t *inv) |
| int | bAigCheckInvariantWithAG (bAigTransition_t *t, bAigEdge_t objective) |
| void | bAigReduceBlockingClauseWithUnsatCore (bAigTransition_t *t) |
| int | bAigInclusionTestOnInitialStates (bAigTransition_t *t) |
| satArray_t * | bAigCreateCNFInstanceForInclusionTestOnInitialStates (bAigTransition_t *t) |
| void | bAig_CreateCNFFromAIG (bAig_Manager_t *manager, satArray_t *rootArray, satArray_t *cnfArray) |
| void | bAig_ComputeAX (bAigTransition_t *t) |
| void | bAigSolveAllSatWithLifting (bAigTransition_t *t) |
| void | bAigBlockingClauseAnalysisBasedOnLifting (bAigTransition_t *t, satManager_t *allsat) |
| int | bAigCheckExistenceOfUIP (satManager_t *cm, satArray_t *clauseArray, int mLevel, bAigEdge_t *fdaLit, int *bLevel) |
| void | bAigMinimizationBasedOnLifting (bAigTransition_t *t, bAigEdge_t obj, satArray_t *orderArray) |
| void | bAigMinimizationBasedOnLiftingAllAtOnce (bAigTransition_t *t, bAigEdge_t obj, satArray_t *orderArray) |
| void | bAigSolverForLifting (satManager_t *cm, int tLevel) |
| void | bAigCollectAntecdentOfObjective (bAigTransition_t *t, satManager_t *cm, bAigEdge_t obj, satArray_t *clauseArray) |
| void | bAigCollectAntecdentOfObjectiveAux (satManager_t *cm, bAigEdge_t v) |
| void | bAigCreateSatManagerForLiftingUnconstrained (bAigTransition_t *t) |
| void | bAigCreateSatManagerForLifting (bAigTransition_t *t) |
| void | bAigPreProcessingForLiftingInstance (bAigTransition_t *t, satManager_t *cm) |
| void | bAig_PostProcessForAX (bAigTransition_t *t, satManager_t *cm) |
| void | bAigMarkConeOfInfluenceForAX (bAigTransition_t *t, satManager_t *cm) |
| satManager_t * | bAigCirCUsInterfaceForAX (bAigTransition_t *t) |
| bAigEdge_t | bAigBuildObjectiveFromFrontierSet (bAigTransition_t *t) |
| bAigEdge_t | bAigBuildComplementedObjectiveWithCNF (bAigTransition_t *t, satManager_t *cm, satArray_t *narr, satArray_t *carr) |
| void | bAigCleanUpDataFromPreviousExecution (bAigTransition_t *t) |
| void | bAigPrintTransitionInfo (bAigTransition_t *t) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: baigAllSat.c,v 1.4 2009/04/11 02:40:01 fabio Exp $" |
| static satManager_t * | SATcm |
Function Documentation
| void bAig_ComputeAX | ( | bAigTransition_t * | t | ) |
Function********************************************************************
Synopsis [Compute AX based on SAT.]
Description [Compute AX based on SAT.]
SideEffects []
SeeAlso []
Copy to transition so that they can be used for next iteration
Definition at line 855 of file baigAllSat.c.
{
satManager_t *cm;
long btime, etime;
btime = util_cpu_time();
cm = t->allsat;
sat_PreProcessingForMixed(cm);
if(cm->status == 0) {
if(t->constrain)
bAigCreateSatManagerForLifting(t);
else
bAigCreateSatManagerForLiftingUnconstrained(t);
bAigSolveAllSatWithLifting(t);
if(t->iteration > 0 && t->reductionUsingUnsat)
bAigReduceBlockingClauseWithUnsatCore(t);
}
sat_PostProcessing(cm);
t->reached = cm->reached;
t->frontier = cm->frontier;
cm->reached = 0;
cm->frontier = 0;
etime = util_cpu_time();
cm->each->satTime = (double)(etime - btime) / 1000.0 ;
fflush(vis_stdout);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t bAig_CreatebAigForInvariant | ( | Ntk_Network_t * | network, |
| bAig_Manager_t * | manager, | ||
| Ctlsp_Formula_t * | inv | ||
| ) |
Function********************************************************************
Synopsis [Create AIG for invariant property.]
Description [Create AIG for invariant property.]
SideEffects []
SeeAlso []
Definition at line 226 of file baigAllSat.c.
{
bAigEdge_t result, left, right;
st_table *nodeToMvfAigTable;
int nodeValue;
int check;
char *nodeNameString;
char *nodeValueString;
Ntk_Node_t *node;
Var_Variable_t *nodeVar;
MvfAig_Function_t *tmpMvfAig;
if (inv == NIL(Ctlsp_Formula_t)) return mAig_NULL;
if (inv->type == Ctlsp_TRUE_c) return mAig_One;
if (inv->type == Ctlsp_FALSE_c) return mAig_Zero;
assert(Ctlsp_isPropositionalFormula(inv));
if (inv->type == Ctlsp_ID_c){
nodeNameString = Ctlsp_FormulaReadVariableName(inv);
nodeValueString = Ctlsp_FormulaReadValueName(inv);
node = Ntk_NetworkFindNodeByName(network, nodeNameString);
if (node == NIL(Ntk_Node_t)) {
fprintf(vis_stderr, "sat_inv error: Could not find node corresponding to the name\t %s\n", nodeNameString);
return mAig_NULL;
}
nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
if (nodeToMvfAigTable == NIL(st_table)){
fprintf(vis_stderr,
"sat_inv error: please run build_partiton_maigs first");
return mAig_NULL;
}
tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
if (tmpMvfAig == NIL(MvfAig_Function_t)){
tmpMvfAig = Bmc_NodeBuildMVF(network, node);
array_free(tmpMvfAig);
tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
}
nodeVar = Ntk_NodeReadVariable(node);
if (Var_VariableTestIsSymbolic(nodeVar)) {
nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
if ( nodeValue == -1 ) {
fprintf(vis_stderr,
"Value specified in RHS is not in domain of variable\n");
fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
return mAig_NULL;
}
}
else {
check = StringCheckIsInteger(nodeValueString, &nodeValue);
if( check == 0 ) {
fprintf(vis_stderr,"Illegal value in the RHS\n");
fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
return mAig_NULL;
}
if( check == 1 ) {
fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
return mAig_NULL;
}
if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
return mAig_NULL;
}
}
result = bAig_GetCanonical(manager,
MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue));
return result;
}
left = bAig_CreatebAigForInvariant(network, manager, inv->left);
if (left == mAig_NULL){
return mAig_NULL;
}
right = bAig_CreatebAigForInvariant(network, manager, inv->right);
if (right == mAig_NULL && inv->type ==Ctlsp_NOT_c ){
return mAig_Not(left);
}
else if(right == mAig_NULL) {
return mAig_NULL;
}
switch(inv->type) {
case Ctlsp_OR_c:
result = mAig_Or(manager, left, right);
break;
case Ctlsp_AND_c:
result = mAig_And(manager, left, right);
break;
case Ctlsp_THEN_c:
result = mAig_Then(manager, left, right);
break;
case Ctlsp_EQ_c:
result = mAig_Eq(manager, left, right);
break;
case Ctlsp_XOR_c:
result = mAig_Xor(manager, left, right);
break;
default:
fail("Unexpected LTL type");
}
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAig_CreateCNFFromAIG | ( | bAig_Manager_t * | manager, |
| satArray_t * | rootArray, | ||
| satArray_t * | cnfArray | ||
| ) |
Function********************************************************************
Synopsis [Create instance for AIG]
Description [Create instance for AIG]
SideEffects []
SeeAlso []
create CNF for this AIG
Definition at line 798 of file baigAllSat.c.
{
int i;
bAigEdge_t v, left, right;
for(i=0; i<rootArray->num; i++) {
v = rootArray->space[i];
bAig_SetMaskTransitiveFanin(manager, v, VisitedMask);
}
for(v=bAigFirstNodeIndex ; v<manager->nodesArraySize; v+=bAigNodeSize){
if(flags(v) & IsCNFMask)
continue;
if(flags(v) & VisitedMask) {
left = leftChild(v);
if(left == 2)
continue;
right = rightChild(v);
sat_ArrayInsert(cnfArray, SATnot(left));
sat_ArrayInsert(cnfArray, SATnot(right));
sat_ArrayInsert(cnfArray, (v));
sat_ArrayInsert(cnfArray, -1);
sat_ArrayInsert(cnfArray, (left));
sat_ArrayInsert(cnfArray, SATnot(v));
sat_ArrayInsert(cnfArray, -1);
sat_ArrayInsert(cnfArray, (right));
sat_ArrayInsert(cnfArray, SATnot(v));
sat_ArrayInsert(cnfArray, -1);
}
}
for(i=0; i<rootArray->num; i++) {
v = rootArray->space[i];
bAig_ResetMaskTransitiveFanin(manager, v, VisitedMask, ResetVisitedMask);
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAig_PostProcessForAX | ( | bAigTransition_t * | t, |
| satManager_t * | cm | ||
| ) |
Function********************************************************************
Synopsis [Post processing after computing AX.]
Description [Free sat manager...]
SideEffects []
SeeAlso []
reset objective for next iteration
Definition at line 2264 of file baigAllSat.c.
{
bAig_Manager_t *manager;
manager = t->manager;
if(cm->maxNodesArraySize > manager->maxNodesArraySize) {
manager->maxNodesArraySize = cm->maxNodesArraySize;
manager->nameList = REALLOC(char *, manager->nameList , manager->maxNodesArraySize/bAigNodeSize);
manager->bddIdArray = REALLOC(int , manager->bddIdArray , manager->maxNodesArraySize/bAigNodeSize);
manager->bddArray = REALLOC(bdd_t *, manager->bddArray , manager->maxNodesArraySize/bAigNodeSize);
}
manager->maxNodesArraySize = cm->maxNodesArraySize;
manager->NodesArray = cm->nodesArray;
manager->literals = cm->literals;
cm->literals->last = cm->literals->initialSize;
cm->nodesArray = 0;
cm->literals = 0;
cm->HashTable = 0;
sat_FreeManager(cm);
t->objective = 0;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAigBlockingClauseAnalysisBasedOnLifting | ( | bAigTransition_t * | t, |
| satManager_t * | allsat | ||
| ) |
Function********************************************************************
Synopsis [Apply minimization based on lifting and create blocking clause.]
Description [Apply minimization based on lifting and create blocking clause.]
SideEffects []
SeeAlso []
cm is lifting instance from now on
Propagate primary input variable first, since they can be freely qunatified
Propagate current state variable to apply greedy minization. Save candidates variable for lifting to clauseArray
exceptional case
If a current state variable is implied by other state variable sasignments then it is part of candidate variable
the objective is satified with primary input only
the objective is satified with primary input only
bAigMinimizationBasedOnLifting(t, t->objective, clauseArray);
the objective is satified with primary input only
fprintf(stdout, "ERROR : This might be the bug after lifting\n");
operation on all sat instance
Definition at line 979 of file baigAllSat.c.
{
satManager_t *cm;
satLevel_t *d;
satArray_t *clauseArray;
bAigEdge_t v, obj, blocked, fdaLit;
int objInverted, inverted;
int i, satisfied;
int value, tvalue;
int mLevel, bLevel;
cm = allsat;
for(i=0; i<t->nInputs; i++) {
v = t->inputs[i];
t->vinputs[i] = SATvalue(v);
}
SATcm = allsat;
qsort(t->tstates, t->nLatches, sizeof(bAigEdge_t), levelCompare);
for(i=0; i<t->nLatches; i++) {
v = t->tstates[i];
t->vtstates[i] = SATvalue(v);
}
cm = t->lifting;
obj = (bAigEdge_t )cm->obj->space[0];
objInverted = SATisInverted(obj);
obj = SATnormalNode(obj);
d = sat_AllocLevel(cm);
satisfied = 0;
clauseArray = sat_ArrayAlloc(256);
clauseArray->num = 0;
for(i=0; i<t->nInputs; i++) {
if(satisfied) break;
v = t->inputs[i];
if(!(SATflags(v) & CoiMask)) continue;
value = t->vinputs[i];
if(value > 1) continue;
tvalue = SATvalue(v);
if(tvalue < 2) continue;
SATvalue(v) = value;
SATmakeImplied(v, d);
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
sat_ImplicationMain(cm, d);
value = SATvalue(obj);
if(value < 2) satisfied = 1;
}
if(satisfied == 0) {
d = sat_AllocLevel(cm);
for(i=0; i<t->nLatches; i++) {
if(satisfied) break;
v = t->tstates[i];
if(!(SATflags(v) & CoiMask)) continue;
value = t->vtstates[i];
if(value > 1) continue;
tvalue = SATvalue(v);
sat_ArrayInsert(clauseArray, v^(!value));
if(tvalue > 1) {
SATvalue(v) = value;
SATmakeImplied(v, d);
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
sat_ImplicationMain(cm, d);
value = SATvalue(obj);
if(value < 2) satisfied = 1;
}
}
}
value = SATvalue(obj);
if(value > 1) {
fprintf(stdout, "ERROR : Can't justify objective %ld\n", t->objective);
exit(0);
}
if(clauseArray->num == 0) {
sat_Backtrack(cm, 0);
cm->currentDecision--;
sat_Backtrack(allsat, 0);
allsat->currentDecision--;
return;
}
bAigCollectAntecdentOfObjective(t, cm, t->objective, clauseArray);
if(clauseArray->num == 0) {
fprintf(stdout, "ERROR : This might be the bug after greedy heuristic\n");
sat_Backtrack(cm, 0);
cm->currentDecision--;
return;
}
sat_Backtrack(cm, 0);
d = SATgetDecision(cm->currentDecision);
sat_Undo(cm, d);
cm->currentDecision--;
if(t->disableLifting == 0)
bAigMinimizationBasedOnLiftingAllAtOnce(t, t->objective, clauseArray);
if(clauseArray->num == 0) {
if(cm->currentDecision >= 0) {
sat_Backtrack(cm, 0);
cm->currentDecision--;
}
sat_Backtrack(allsat, 0);
allsat->currentDecision--;
return;
}
cm = t->allsat;
mLevel = 0;
for(i=0; i<clauseArray->num; i++) {
v = clauseArray->space[i];
v = SATnormalNode(v);
if(mLevel < SATlevel(v))
mLevel = SATlevel(v);
}
blocked = sat_AddBlockingClause(cm, clauseArray);
SATflags(blocked) |= IsFrontierMask;
if(t->verbose > 3)
sat_PrintNode(cm, blocked);
sat_Backtrack(cm, mLevel);
d = SATgetDecision(cm->currentDecision);
if(t->verbose > 3) {
qsort(clauseArray->space, clauseArray->num, sizeof(long), indexCompare);
for(i=0; i<clauseArray->num; i++) {
fprintf(stdout, "%ld ", clauseArray->space[i]);
}
fprintf(stdout, "\n");
}
if(bAigCheckExistenceOfUIP(cm, clauseArray, mLevel, &fdaLit, &bLevel)) {
sat_Backtrack(cm, bLevel);
if(SATlevel(fdaLit) == 0) {
sat_Backtrack(cm, 0);
cm->currentDecision = -1;
sat_ArrayFree(clauseArray);
return;
}
d = SATgetDecision(cm->currentDecision);
inverted = SATisInverted(fdaLit);
fdaLit = SATnormalNode(fdaLit);
SATante(fdaLit) = blocked;
SATvalue(fdaLit) = inverted;
SATmakeImplied(fdaLit, d);
if((SATflags(fdaLit) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, fdaLit);
SATflags(fdaLit) |= InQueueMask;
}
}
else {
d->conflict = blocked;
sat_ConflictAnalysisWithBlockingClause(cm, d);
}
sat_ArrayFree(clauseArray);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t bAigBuildComplementedObjectiveWithCNF | ( | bAigTransition_t * | t, |
| satManager_t * | cm, | ||
| satArray_t * | narr, | ||
| satArray_t * | carr | ||
| ) |
0 or -1 is seperator between clauses
skip
trivially satisfied
seperator
0 or -1 is seperator between clauses
seperator
Definition at line 2616 of file baigAllSat.c.
{
satArray_t *clause;
satArray_t *andArr, *orArr;
satArray_t *fandArr;
satArray_t *fArr, *arr;
satArray_t *frontier;
int i, j, nCls, removeFlag;
int inverted;
long *space, index;
bAigEdge_t v, tv, out, objective;
bAigEdge_t obj1, obj2;
andArr = sat_ArrayAlloc(1024);
fandArr = sat_ArrayAlloc(1024);
clause = sat_ArrayAlloc(1024);
if(t->coiStates == 0)
t->coiStates = ALLOC(bAigEdge_t, sizeof(bAigEdge_t) * t->csize);
memset(t->coiStates, 0, sizeof(bAigEdge_t)*t->csize);
if(t->tVariables) t->tVariables->num = 0;
else t->tVariables = sat_ArrayAlloc(1024);
fArr = sat_ArrayAlloc(1024);
orArr =sat_ArrayAlloc(1024);
sat_ArrayInsert(fArr, 0);
nCls = 0;
frontier = narr;
if(frontier) {
for(i=0, space=frontier->space; i<frontier->num; i++, space++) {
if(*space <= 0) {
space++;
i++;
if(i >= frontier->num) {
break;
}
removeFlag = 0;
fandArr->num = 0;
andArr->num = 0;
while(*space > 0) {
sat_ArrayInsert(fandArr, *space);
i++;
space++;
}
i--;
space--;
removeFlag = 0;
for(j=0; j<fandArr->num; j++) {
v = fandArr->space[j];
inverted = SATisInverted(v);
tv = SATnormalNode(v);
index = SATnodeID(tv);
if(index > t->csize) {
fprintf(stdout, "ERROR : %ld is not current state variable\n", tv);
exit(0);
}
v = t->c2n[index];
v = v ^ (inverted);
if(t->verbose > 4)
fprintf(stdout, "%ld(%ld) ",fandArr->space[j], v);
if(v == 0) {
andArr->space[j] = 0;
}
else if(v == 1)
removeFlag = 1;
else {
sat_ArrayInsert(andArr, v);
t->coiStates[index] = 1;
}
}
if(t->verbose > 4)
fprintf(stdout, "\n");
if(removeFlag)
continue;
if(t->verbose > 4) {
fprintf(stdout, "%ld-> ", andArr->num);
for(j=0; j<andArr->num; j++) {
v = andArr->space[j];
fprintf(stdout, "%ld ", v);
}
fprintf(stdout, "\n");
}
out = sat_CreateNode(cm, 2, 2);
sat_ArrayInsert(orArr, out);
sat_ArrayInsert(t->tVariables, out);
for(j=0; j<andArr->num; j++) {
v = andArr->space[j];
sat_ArrayInsert(fArr, SATnot(v));
sat_ArrayInsert(fArr, SATnot(out));
sat_ArrayInsert(fArr, -1);
nCls++;
}
for(j=0; j<andArr->num; j++) {
v = andArr->space[j];
sat_ArrayInsert(fArr, v);
}
sat_ArrayInsert(fArr, out);
sat_ArrayInsert(fArr, -1);
nCls++;
}
}
}
obj1 = sat_CreateNode(cm, 2, 2);
for(i=0; i<orArr->num; i++) {
v = orArr->space[i];
sat_ArrayInsert(fArr, SATnot(v));
sat_ArrayInsert(fArr, obj1);
sat_ArrayInsert(fArr, -1);
nCls++;
}
for(i=0; i<orArr->num; i++) {
v = orArr->space[i];
sat_ArrayInsert(fArr, v);
}
sat_ArrayInsert(fArr, SATnot(obj1));
sat_ArrayInsert(fArr, -1);
nCls++;
#if 1
frontier = carr;
if(frontier) {
for(i=0, space=frontier->space; i<frontier->num; i++, space++) {
if(*space <= 0) {
space++;
i++;
if(i >= frontier->num) {
break;
}
fandArr->num = 0;
andArr->num = 0;
while(*space > 0) {
sat_ArrayInsert(fandArr, *space);
i++;
space++;
}
i--;
space--;
if(t->verbose > 4) {
fprintf(stdout, "%ld-> ", andArr->num);
for(j=0; j<andArr->num; j++) {
v = andArr->space[j];
fprintf(stdout, "%ld ", v);
}
fprintf(stdout, "\n");
}
out = sat_CreateNode(cm, 2, 2);
sat_ArrayInsert(orArr, out);
sat_ArrayInsert(t->tVariables, out);
for(j=0; j<andArr->num; j++) {
v = andArr->space[j];
sat_ArrayInsert(fArr, SATnot(v));
sat_ArrayInsert(fArr, SATnot(out));
sat_ArrayInsert(fArr, -1);
nCls++;
}
for(j=0; j<andArr->num; j++) {
v = andArr->space[j];
sat_ArrayInsert(fArr, v);
}
sat_ArrayInsert(fArr, out);
sat_ArrayInsert(fArr, -1);
nCls++;
}
}
}
obj2 = sat_CreateNode(cm, 2, 2);
for(i=0; i<orArr->num; i++) {
v = orArr->space[i];
sat_ArrayInsert(fArr, SATnot(v));
sat_ArrayInsert(fArr, obj2);
sat_ArrayInsert(fArr, -1);
nCls++;
}
for(i=0; i<orArr->num; i++) {
v = orArr->space[i];
sat_ArrayInsert(fArr, v);
}
sat_ArrayInsert(fArr, SATnot(obj2));
sat_ArrayInsert(fArr, -1);
nCls++;
#endif
sat_ArrayInsert(t->tVariables, obj1);
sat_ArrayInsert(t->tVariables, obj2);
objective = sat_CreateNode(cm, 2, 2);
sat_ArrayInsert(fArr, SATnot(obj1));
sat_ArrayInsert(fArr, SATnot(obj2));
sat_ArrayInsert(fArr, objective);
sat_ArrayInsert(fArr, -1);
sat_ArrayInsert(fArr, (obj1));
sat_ArrayInsert(fArr, SATnot(objective));
sat_ArrayInsert(fArr, -1);
sat_ArrayInsert(fArr, (obj2));
sat_ArrayInsert(fArr, SATnot(objective));
sat_ArrayInsert(fArr, -1);
if(orArr->num == 0) {
fArr->num = 0;
}
if(t->verbose > 0) {
fprintf(vis_stdout, "** SAT_INV : %ld number of frontier blocking clauses are processed\n", orArr->num);
fprintf(vis_stdout, "** SAT_INV : %d number of clauses are added to build objective\n", nCls);
}
sat_ArrayFree(andArr);
sat_ArrayFree(fandArr);
sat_ArrayFree(clause);
cm->initNumVariables = cm->nodesArraySize;
if(cm->variableArray == 0) {
cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
memset(cm->variableArray, 0,
sizeof(satVariable_t) * (cm->initNumVariables+1));
}
sat_RestoreClauses(cm, fArr);
sat_CleanDatabase(cm);
if(t->allsat->assertion) t->lifting->assertion = sat_ArrayDuplicate(t->allsat->assertion);
if(t->allsat->auxObj) t->lifting->auxObj = sat_ArrayDuplicate(t->allsat->auxObj);
sat_MarkTransitiveFaninForNode(cm, objective, CoiMask);
for(i=0; i<t->csize; i++) {
if(t->coiStates[i]) {
sat_MarkTransitiveFaninForNode(cm, SATnormalNode(t->c2n[i]), CoiMask);
}
}
if(t->tVariables) {
arr = t->tVariables;
for(i=0; i<arr->num; i++) {
v = arr->space[i];
SATflags(v) |= CoiMask;
}
}
if(t->auxObj) {
arr = t->auxObj;
for(i=0; i<arr->num; i++) {
v = arr->space[i];
sat_MarkTransitiveFaninForNode(cm, v, CoiMask);
}
}
return(objective);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t bAigBuildObjectiveFromFrontierSet | ( | bAigTransition_t * | t | ) |
Function********************************************************************
Synopsis [Build new objective from frontier set by complementing blocking cluases]
Description [Build new objective from frontier set by complementing blocking cluases, the frontier array of bAigTransition_t save the blocking clause as clause form. The structure of frontier array is as follows. clause seperator, literals in clause, clause seperator, ..., clause seperator ]
SideEffects []
SeeAlso []
0 or -1 is seperator between clauses
skip
trivially satisfied
seperator
Definition at line 2432 of file baigAllSat.c.
{
mAig_Manager_t *manager;
satArray_t *frontier;
satArray_t *clause;
satArray_t *andArr, *orArr;
satArray_t *fandArr;
satArray_t *fArr;
int i, j, nCls, removeFlag;
int inverted;
long *space, index;
bAigEdge_t v, tv, out, objective;
manager = t->manager;
andArr = sat_ArrayAlloc(1024);
fandArr = sat_ArrayAlloc(1024);
clause = sat_ArrayAlloc(1024);
if(t->coiStates == 0)
t->coiStates = ALLOC(bAigEdge_t, sizeof(bAigEdge_t) * t->csize);
memset(t->coiStates, 0, sizeof(bAigEdge_t)*t->csize);
if(t->tVariables) t->tVariables->num = 0;
else t->tVariables = sat_ArrayAlloc(1024);
fArr = sat_ArrayAlloc(1024);
orArr = t->tVariables;
nCls = 0;
frontier = t->frontier;
sat_ArrayInsert(fArr, 0);
for(i=0, space=frontier->space; i<frontier->num; i++, space++) {
if(*space <= 0) {
space++;
i++;
if(i >= frontier->num) {
break;
}
removeFlag = 0;
fandArr->num = 0;
andArr->num = 0;
while(*space > 0) {
#if 0
v = *space;
inverted = SATisInverted(v);
tv = SATnormalNode(v);
index = SATnodeID(tv);
if(index > t->csize) {
fprintf(stdout, "ERROR : %ld is not current state variable\n", tv);
exit(0);
}
v = t->c2n[index];
v = v ^ (inverted);
if(v == 0) {
}
else if(v == 1)
removeFlag = 1;
else if(removeFlag == 0) {
sat_ArrayInsert(andArr, v);
t->coiStates[index] = 1;
}
#endif
sat_ArrayInsert(fandArr, *space);
i++;
space++;
}
i--;
space--;
removeFlag = 0;
for(j=0; j<fandArr->num; j++) {
v = fandArr->space[j];
inverted = SATisInverted(v);
tv = SATnormalNode(v);
index = SATnodeID(tv);
if(index > t->csize) {
fprintf(stdout, "ERROR : %ld is not current state variable\n", tv);
exit(0);
}
v = t->c2n[index];
v = v ^ (inverted);
if(t->verbose > 4)
fprintf(stdout, "%ld(%ld) ",fandArr->space[j], v);
if(v == 0) {
andArr->space[j] = 0;
}
else if(v == 1)
removeFlag = 1;
else {
sat_ArrayInsert(andArr, v);
t->coiStates[index] = 1;
}
}
if(t->verbose > 4)
fprintf(stdout, "\n");
if(removeFlag)
continue;
if(t->verbose > 4) {
fprintf(stdout, "%ld-> ", andArr->num);
for(j=0; j<andArr->num; j++) {
v = andArr->space[j];
fprintf(stdout, "%ld ", v);
}
fprintf(stdout, "\n");
}
out = bAig_CreateNode(manager, 2, 2);
sat_ArrayInsert(orArr, out);
for(j=0; j<andArr->num; j++) {
v = andArr->space[j];
sat_ArrayInsert(fArr, SATnot(v));
sat_ArrayInsert(fArr, SATnot(out));
sat_ArrayInsert(fArr, -1);
nCls++;
}
for(j=0; j<andArr->num; j++) {
v = andArr->space[j];
sat_ArrayInsert(fArr, v);
}
sat_ArrayInsert(fArr, out);
sat_ArrayInsert(fArr, -1);
nCls++;
}
}
objective = bAig_CreateNode(manager, 2, 2);
for(i=0; i<orArr->num; i++) {
v = orArr->space[i];
sat_ArrayInsert(fArr, SATnot(v));
sat_ArrayInsert(fArr, objective);
sat_ArrayInsert(fArr, -1);
nCls++;
}
for(i=0; i<orArr->num; i++) {
v = orArr->space[i];
sat_ArrayInsert(fArr, v);
}
sat_ArrayInsert(fArr, SATnot(objective));
sat_ArrayInsert(fArr, -1);
nCls++;
if(orArr->num == 0) {
fArr->num = 0;
}
if(t->verbose > 0) {
fprintf(vis_stdout, "** SAT_INV : %ld number of frontier blocking clauses are processed\n", orArr->num);
fprintf(vis_stdout, "** SAT_INV : %d number of clauses are added to build objective\n", nCls);
}
sat_ArrayFree(andArr);
sat_ArrayFree(fandArr);
sat_ArrayFree(clause);
t->originalFrontier = frontier;
t->frontier = fArr;
t->objective = objective;
if(t->objArr == 0)
t->objArr = sat_ArrayAlloc(t->nLatches);
t->objArr->num = 0;
for(i=0; i<t->csize; i++) {
if(t->coiStates[i]) {
sat_ArrayInsert(t->objArr, SATnormalNode(t->c2n[i]));
}
}
return(objective);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int bAigCheckExistenceOfUIP | ( | satManager_t * | cm, |
| satArray_t * | clauseArray, | ||
| int | mLevel, | ||
| bAigEdge_t * | fdaLit, | ||
| int * | bLevel | ||
| ) |
Function********************************************************************
Synopsis [Apply minization based on checking antecedent of objective.]
Description [Apply minization based on checking antecedent of objective.]
SideEffects []
SeeAlso []
Definition at line 1203 of file baigAllSat.c.
{
int i, nLit, level;
int uipFlag;
bAigEdge_t v, ante;
nLit = 0;
*bLevel = 0;
*fdaLit = 0;
uipFlag = 0;
for(i=0; i<clauseArray->num; i++) {
v = clauseArray->space[i];
v = SATnormalNode(v);
level = SATlevel(v);
if(level == mLevel) {
nLit++;
if(nLit > 1)
break;
ante = SATante(v);
if(ante == 0) {
uipFlag = 1;
*fdaLit = clauseArray->space[i];
}
}
else if(*bLevel < level)
*bLevel = level;
}
if(nLit > 1)
uipFlag = 0;
if(uipFlag) return(1);
else return(0);
}
Here is the caller graph for this function:
| int bAigCheckInvariantWithAG | ( | bAigTransition_t * | t, |
| bAigEdge_t | objective | ||
| ) |
Function********************************************************************
Synopsis [Compute AG.]
Description [Compute AG.]
SideEffects []
SeeAlso []
This is for applying SAT-based AX operation
This function do nothing in the first iteration, since no frontier is provided at first. Instead of frontier, we have complemented objective at first
property passed
propoerty failed
reched to convergenece
property passed
Definition at line 352 of file baigAllSat.c.
{
int included, returnFlag;
bAig_Manager_t *manager;
satManager_t *cm;
long frontierNodesBegin;
manager = t->manager;
bAigCleanUpDataFromPreviousExecution(t);
objective = bAig_Not(objective);
t->objective = objective;
returnFlag = 0;
while(1) {
if(t->verbose > 1)
fprintf(vis_stdout, "** SAT_INV : %d'th pre-image is being computed\n", t->iteration+1);
frontierNodesBegin = manager->nodesArraySize;
if(t->iteration > 0) {
bAigBuildObjectiveFromFrontierSet(t);
if(t->frontier->num <= 1) {
returnFlag = 1;
break;
}
}
cm = bAigCirCUsInterfaceForAX(t);
cm->frontierNodesBegin = frontierNodesBegin;
t->allsat = cm;
sat_CleanDatabase(cm);
bAigMarkConeOfInfluenceForAX(t, cm);
fflush(vis_stdout);
bAig_ComputeAX(t);
if(t->verbose > 1) {
sat_ReportStatistics(cm, cm->each);
}
included = bAigInclusionTestOnInitialStates(t);
if(included == 0) {
returnFlag = 2;
}
if(t->frontier->num <= 1) {
returnFlag = 1;
}
bAig_PostProcessForAX(t, cm);
t->manager->nodesArraySize = frontierNodesBegin;
t->allsat = 0;
if(t->lifting) {
sat_FreeManager(t->lifting);
t->lifting = 0;
}
if(t->originalFrontier) {
sat_ArrayFree(t->originalFrontier);
t->originalFrontier = 0;
}
if(returnFlag) {
break;
}
t->iteration++;
}
if(t->verbose > 0) {
fprintf(vis_stdout, "** SAT_INV : Total %d pre-image is computed\n", t->iteration+1);
}
sat_ArrayFree(t->frontier);
t->frontier = 0;
sat_ArrayFree(t->reached);
t->reached = 0;
fflush(vis_stdout);
return(returnFlag);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| satManager_t* bAigCirCUsInterfaceForAX | ( | bAigTransition_t * | t | ) |
Function********************************************************************
Synopsis [Make interface for CirCUs to compute AX.]
Description [Make interface for CirCUs to compute AX.]
SideEffects []
SeeAlso []
Copy to reachable states and frontier to satManager so that they can be used to build current instance.
Definition at line 2349 of file baigAllSat.c.
{
satManager_t *cm;
bAig_Manager_t *manager;
satOption_t *option;
int i;
bAigEdge_t v;
manager = t->manager;
cm = sat_InitManager(0);
memset(cm, 0, sizeof(satManager_t));
cm->nodesArraySize = manager->nodesArraySize;
cm->initNodesArraySize = manager->nodesArraySize;
cm->maxNodesArraySize = manager->maxNodesArraySize;
cm->nodesArray = manager->NodesArray;
cm->HashTable = manager->HashTable;
cm->literals = manager->literals;
cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize);
cm->initNumClauses = 0;
cm->initNumLiterals = 0;
cm->comment = ALLOC(char, 2);
cm->comment[0] = ' ';
cm->comment[1] = '\0';
cm->stdErr = vis_stderr;
cm->stdOut = vis_stdout;
cm->status = 0;
cm->orderedVariableArray = 0;
cm->unitLits = sat_ArrayAlloc(16);
cm->pureLits = sat_ArrayAlloc(16);
cm->option = 0;
cm->each = 0;
cm->decisionHead = 0;
cm->variableArray = 0;
cm->queue = 0;
cm->BDDQueue = 0;
cm->unusedAigQueue = 0;
option = sat_InitOption();
cm->option = option;
option->verbose = 0;
cm->each = sat_InitStatistics();
sat_AllocLiteralsDB(cm);
cm->obj = sat_ArrayAlloc(1);
sat_ArrayInsert(cm->obj, t->objective);
if(t->auxObj && t->auxObj->num) {
cm->auxObj = sat_ArrayAlloc(t->auxObj->num);
for(i=0; i<t->auxObj->num; i++) {
v = t->auxObj->space[i];
sat_ArrayInsert(cm->auxObj, v);
}
}
cm->option->allSatMode = 1;
cm->reached = t->reached;
cm->frontier = t->frontier;
t->reached = 0;
t->frontier = 0;
return(cm);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAigCleanUpDataFromPreviousExecution | ( | bAigTransition_t * | t | ) |
Function********************************************************************
Synopsis [Function to clean data of bAigTransition_t generated from previous execution]
Description [Function to clean data of bAigTransition_t generated from previous execution]
SideEffects []
SeeAlso []
Definition at line 2908 of file baigAllSat.c.
{
if(t->frontier) {
sat_ArrayFree(t->frontier);
t->frontier = 0;
}
if(t->reached) {
sat_ArrayFree(t->reached);
t->reached = 0;
}
t->objective = 0;
t->iteration = 0;
t->nBlocked = 0;
t->sum = 0;
t->avgLits = 0;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAigCollectAntecdentOfObjective | ( | bAigTransition_t * | t, |
| satManager_t * | cm, | ||
| bAigEdge_t | obj, | ||
| satArray_t * | clauseArray | ||
| ) |
Function********************************************************************
Synopsis [Apply minization based on checking antecedent of objective.]
Description [Apply minization based on checking antecedent of objective.]
SideEffects []
SeeAlso []
We don't need to reset visited flags, since they will be reset by backtracking
Definition at line 1705 of file baigAllSat.c.
{
int i, value;
bAigEdge_t v;
bAigCollectAntecdentOfObjectiveAux(cm, obj);
clauseArray->num = 0;
for(i=0; i<t->nLatches; i++) {
v = t->tstates[i];
if(SATflags(v) & VisitedMask) {
value = t->vtstates[i];
sat_ArrayInsert(clauseArray, v^(!value));
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAigCollectAntecdentOfObjectiveAux | ( | satManager_t * | cm, |
| bAigEdge_t | v | ||
| ) |
Function********************************************************************
Synopsis [Apply minization based on checking antecedent of objective.]
Description [Apply minization based on checking antecedent of objective.]
SideEffects []
SeeAlso []
Definition at line 1742 of file baigAllSat.c.
{
int i, size, completeness;
int value, inverted;
bAigEdge_t ante, nv, *plit;
if(v == 2)
return;
v = SATnormalNode(v);
if(SATflags(v) & VisitedMask)
return;
SATflags(v) |= VisitedMask;
ante = SATante(v);
if(ante == 0)
return;
if(SATflags(ante) & IsCNFMask) {
size = SATnumLits(ante);
completeness = 1;
for(i=0, plit=(bAigEdge_t*)SATfirstLit(ante); i<size; i++, plit++) {
nv = SATgetNode(*plit);
inverted = SATisInverted(nv);
nv = SATnormalNode(nv);
value = SATvalue(nv) ^ inverted;
if(v == nv) {
if(value == 0) completeness = 0;
}
else {
if(value == 1) completeness = 0;
}
}
if(completeness == 0) {
fprintf(stdout, "ERROR : incomplete implication graph\n");
}
for(i=0, plit=(bAigEdge_t*)SATfirstLit(ante); i<size; i++, plit++) {
nv = SATgetNode(*plit);
nv = SATnormalNode(nv);
if(SATflags(nv) & VisitedMask)
continue;
bAigCollectAntecdentOfObjectiveAux(cm, nv);
}
}
else {
bAigCollectAntecdentOfObjectiveAux(cm, ante);
ante = SATante2(v);
if(ante)
bAigCollectAntecdentOfObjectiveAux(cm, ante);
}
}
Here is the caller graph for this function:
| satArray_t* bAigCreateCNFInstanceForInclusionTestOnInitialStates | ( | bAigTransition_t * | t | ) |
Function********************************************************************
Synopsis [Create instance for initial states inclusion test]
Description [Create instance for initial states inclusion test]
SideEffects []
SeeAlso []
0 or -1 is seperator between clauses
seperator
assert objective
Collect AIG for CNF translation
connect AIG root and current state variable with equivalence relation
Definition at line 635 of file baigAllSat.c.
{
satArray_t *cnfArray, *frontier;
satArray_t *andArr, *orArr, *fandArr, *clause;
satArray_t *rootArray;
bAigEdge_t v, cv, out, objective;
bAigEdge_t maxIndex;
long *space;
int i, j;
int nCls;
maxIndex = 0;
for(i=0; i<t->nLatches; i++) {
v = t->cstates[i];
if(maxIndex < v) maxIndex = v;
}
maxIndex += bAigNodeSize;
cnfArray = sat_ArrayAlloc(2048);
andArr = sat_ArrayAlloc(1024);
orArr = sat_ArrayAlloc(1024);
fandArr = sat_ArrayAlloc(1024);
clause = sat_ArrayAlloc(1024);
nCls = 0;
frontier = t->frontier;
sat_ArrayInsert(cnfArray, 0);
for(i=0, space=frontier->space; i<frontier->num; i++, space++) {
if(*space <= 0) {
space++;
i++;
if(i >= frontier->num) {
break;
}
fandArr->num = 0;
andArr->num = 0;
while(*space > 0) {
sat_ArrayInsert(fandArr, *space);
i++;
space++;
}
i--;
space--;
for(j=0; j<fandArr->num; j++) {
v = fandArr->space[j];
sat_ArrayInsert(andArr, v);
}
out = maxIndex;
maxIndex += bAigNodeSize;
sat_ArrayInsert(orArr, out);
for(j=0; j<andArr->num; j++) {
v = andArr->space[j];
sat_ArrayInsert(cnfArray, SATnot(v));
sat_ArrayInsert(cnfArray, SATnot(out));
sat_ArrayInsert(cnfArray, -1);
nCls++;
}
for(j=0; j<andArr->num; j++) {
v = andArr->space[j];
sat_ArrayInsert(cnfArray, v);
}
sat_ArrayInsert(cnfArray, out);
sat_ArrayInsert(cnfArray, -1);
nCls++;
}
}
objective = maxIndex;
maxIndex += bAigNodeSize;
for(i=0; i<orArr->num; i++) {
v = orArr->space[i];
sat_ArrayInsert(cnfArray, SATnot(v));
sat_ArrayInsert(cnfArray, objective);
sat_ArrayInsert(cnfArray, -1);
nCls++;
}
for(i=0; i<orArr->num; i++) {
v = orArr->space[i];
sat_ArrayInsert(cnfArray, v);
}
sat_ArrayInsert(cnfArray, SATnot(objective));
sat_ArrayInsert(cnfArray, -1);
nCls++;
sat_ArrayInsert(cnfArray, objective);
sat_ArrayInsert(cnfArray, -1);
nCls++;
sat_ArrayFree(andArr);
sat_ArrayFree(orArr);
sat_ArrayFree(fandArr);
sat_ArrayFree(clause);
rootArray = sat_ArrayAlloc(t->nLatches);
for(i=0; i<t->nLatches; i++) {
v = t->initials[i];
if(v>1)
sat_ArrayInsert(rootArray, v);
}
if(t->allsat->maxNodesArraySize > t->manager->maxNodesArraySize) {
t->manager->maxNodesArraySize = t->allsat->maxNodesArraySize;
t->manager->nameList = REALLOC(char *, t->manager->nameList , t->manager->maxNodesArraySize/bAigNodeSize);
t->manager->bddIdArray = REALLOC(int , t->manager->bddIdArray , t->manager->maxNodesArraySize/bAigNodeSize);
t->manager->bddArray = REALLOC(bdd_t *, t->manager->bddArray , t->manager->maxNodesArraySize/bAigNodeSize);
}
t->manager->maxNodesArraySize = t->allsat->maxNodesArraySize;
t->manager->NodesArray = t->allsat->nodesArray;
bAig_CreateCNFFromAIG(t->manager, rootArray, cnfArray);
sat_ArrayFree(rootArray);
for(i=0; i<t->nLatches; i++) {
v = t->initials[i];
cv = t->cstates[i];
if(v == 0) {
sat_ArrayInsert(cnfArray, SATnot(cv));
sat_ArrayInsert(cnfArray, -1);
}
else if(v == 1) {
sat_ArrayInsert(cnfArray, cv);
sat_ArrayInsert(cnfArray, -1);
}
else {
sat_ArrayInsert(cnfArray, SATnot(v));
sat_ArrayInsert(cnfArray, (cv));
sat_ArrayInsert(cnfArray, -1);
sat_ArrayInsert(cnfArray, (v));
sat_ArrayInsert(cnfArray, SATnot(cv));
sat_ArrayInsert(cnfArray, -1);
}
}
return(cnfArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAigCreateSatManagerForLifting | ( | bAigTransition_t * | t | ) |
Function********************************************************************
Synopsis [Create SAT manager for lifting.]
Description [Create SAT manager for lifting.]
SideEffects []
SeeAlso []
to add blocking clause to lifting instance, modify lastLit
if(allsat->nodesArraySize != allsat->frontierNodesEnd){ v = allsat->frontierNodesEnd-satNodeSize; lastLit = SATfirstLit(v); lastLit += SATnumLits(v); lastLit++; } lifting->nodesArraySize = allsat->frontierNodesEnd;
To copy circuit, frontier, and all blocking clauses lifting->nodesArraySize = allsat->nodesArraySize;
To copy circuit structure
We save the frontier SAT first in allsat instance and blocking clauses geenrated from previous runs.
there are clauses for objective
there is no extra logic for objective
this is important because of incrementality
To apply greedy minimization, the objective is not asserted The complemented objective will be asserted during lifting process
Definition at line 1938 of file baigAllSat.c.
{
satManager_t *lifting, *allsat, *cm;
bAigEdge_t *lastLit, v;
satOption_t *option;
satLiteralDB_t *literals;
int size, dir;
int nCls, nLits, index;
long *space;
allsat = t->allsat;
lifting = sat_InitManager(0);
t->lifting = lifting;
cm = allsat;
lastLit = 0;
if(t->constrain) {
if(allsat->nodesArraySize != allsat->frontierNodesEnd){
v = allsat->nodesArraySize-satNodeSize;
lastLit = (bAigEdge_t *) SATfirstLit(v);
lastLit += SATnumLits(v);
lastLit++;
}
lifting->nodesArraySize = allsat->nodesArraySize;
}
else {
lifting->nodesArraySize = allsat->frontierNodesBegin;
}
lifting->initNodesArraySize = lifting->nodesArraySize;
lifting->maxNodesArraySize = lifting->nodesArraySize * 2;
lifting->nodesArray = ALLOC(long, lifting->maxNodesArraySize);
memcpy(lifting->nodesArray, allsat->nodesArray, sizeof(long) * lifting->nodesArraySize);
lifting->HashTable = ALLOC(long, bAig_HashTableSize);
memcpy(lifting->HashTable, allsat->HashTable, sizeof(long)*bAig_HashTableSize);
literals = ALLOC(satLiteralDB_t, 1);
lifting->literals = literals;
if(lastLit > 0) {
size = lastLit - allsat->literals->begin;
}
else {
size = 0;
}
if(size > 1) {
literals->begin = ALLOC(long, size*4);
literals->end = literals->begin + size*4;
memcpy(literals->begin, allsat->literals->begin, sizeof(long)*size);
literals->last = literals->begin + size;
literals->initialSize = literals->begin+size-1;
}
else {
size = 1024 * 1024;
literals->begin = ALLOC(long, size);
*(literals->begin) = 0;
literals->last = literals->begin + 1;
literals->end = literals->begin + size;
literals->initialSize = literals->last;
}
lifting->initNumVariables = allsat->initNumVariables;
lifting->initNumClauses = allsat->initNumClauses;
lifting->initNumLiterals = allsat->initNumLiterals;
lifting->comment = ALLOC(char, 2);
lifting->comment[0] = ' ';
lifting->comment[1] = '\0';
lifting->stdErr = allsat->stdErr;
lifting->stdOut = allsat->stdOut;
lifting->status = 0;
lifting->orderedVariableArray = 0;
lifting->unitLits = sat_ArrayAlloc(16);
lifting->pureLits = sat_ArrayAlloc(16);
lifting->option = 0;
lifting->each = 0;
lifting->decisionHead = 0;
lifting->variableArray = 0;
lifting->queue = 0;
lifting->BDDQueue = 0;
lifting->unusedAigQueue = 0;
option = sat_InitOption();
lifting->option = option;
option->verbose = 0;
option->decisionHeuristic = 0;
option->decisionHeuristic |= DVH_DECISION;
lifting->each = sat_InitStatistics();
sat_CleanDatabase(lifting);
if(lifting->variableArray == 0) {
lifting->variableArray = ALLOC(satVariable_t, lifting->initNumVariables+1);
memset(lifting->variableArray, 0,
sizeof(satVariable_t) * (lifting->initNumVariables+1));
}
cm = lifting;
nCls = nLits = 0;
for(space = literals->begin; space < literals->last; space++) {
if(*space < 0) {
v = -(*space);
space++;
SATfirstLit(v) = (long) space;
index = 0;
while(1) {
if(*space < 0) break;
dir = SATgetDir(*space);
nLits++;
if(dir == -2){
space++;
index++;
continue;
}
SATunsetWL(space);
sat_AddWL(cm, v, index, dir);
space++;
index++;
}
nCls++;
}
}
lifting->initNumClauses = nCls;
lifting->initNumLiterals = nLits;
if(allsat->assertion) lifting->assertion = sat_ArrayDuplicate(allsat->assertion);
if(allsat->auxObj) lifting->auxObj = sat_ArrayDuplicate(allsat->auxObj);
bAigMarkConeOfInfluenceForAX(t, lifting);
bAigPreProcessingForLiftingInstance(t, lifting) ;
/*
* reset score of PI
* Since the scores of PI and current state variables are high than
* other variables because of blocking clauses that forwarded from
* prevous image step.
for(i=0; i<t->nInputs; i++) {
v = t->inputs[i];
var = lifting->variableArray[SATnodeID(v)];
var.scores[0] = 0;
var.scores[1] = 0;
}
for(i=0; i<t->nLatches; i++) {
v = t->cstates[i];
var = lifting->variableArray[SATnodeID(v)];
var.scores[0] = 0;
var.scores[1] = 0;
}
**/
if(lifting->obj) sat_ArrayFree(lifting->obj);
lifting->obj = sat_ArrayDuplicate(allsat->obj);
lifting->currentDecision = -1;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAigCreateSatManagerForLiftingUnconstrained | ( | bAigTransition_t * | t | ) |
Function********************************************************************
Synopsis [Create SAT manager for lifting.]
Description [Create SAT manager for lifting.]
SideEffects []
SeeAlso []
to add blocking clause to lifting instance, modify lastLit
To copy circuit structure
allocate literal pool
this is important because of incrementality
To apply greedy minimization, the objective is not asserted The complemented objective will be asserted during lifting process
Definition at line 1810 of file baigAllSat.c.
{
satManager_t *lifting, *allsat, *cm;
bAigEdge_t *lastLit;
satOption_t *option;
satLiteralDB_t *literals;
long objective;
allsat = t->allsat;
lifting = sat_InitManager(0);
t->lifting = lifting;
cm = allsat;
lastLit = 0;
lifting->nodesArraySize = allsat->frontierNodesBegin;
lifting->initNodesArraySize = lifting->nodesArraySize;
lifting->maxNodesArraySize = lifting->nodesArraySize * 2;
lifting->nodesArray = ALLOC(long, lifting->maxNodesArraySize);
memcpy(lifting->nodesArray, allsat->nodesArray, sizeof(long) * lifting->nodesArraySize);
lifting->HashTable = ALLOC(long, bAig_HashTableSize);
memcpy(lifting->HashTable, allsat->HashTable, sizeof(long)*bAig_HashTableSize);
sat_AllocLiteralsDB(lifting);
literals = lifting->literals;
lifting->comment = ALLOC(char, 2);
lifting->comment[0] = ' ';
lifting->comment[1] = '\0';
lifting->stdErr = allsat->stdErr;
lifting->stdOut = allsat->stdOut;
lifting->status = 0;
lifting->orderedVariableArray = 0;
lifting->unitLits = sat_ArrayAlloc(16);
lifting->pureLits = sat_ArrayAlloc(16);
lifting->option = 0;
lifting->each = 0;
lifting->decisionHead = 0;
lifting->variableArray = 0;
lifting->queue = 0;
lifting->BDDQueue = 0;
lifting->unusedAigQueue = 0;
option = sat_InitOption();
lifting->option = option;
option->verbose = 0;
option->decisionHeuristic = 0;
option->decisionHeuristic |= DVH_DECISION;
lifting->each = sat_InitStatistics();
if(t->originalFrontier || t->allsat->reached) {
objective = bAigBuildComplementedObjectiveWithCNF(
t, lifting, t->originalFrontier, t->allsat->reached);
objective = SATnot(objective);
}
else {
lifting->initNumVariables = lifting->nodesArraySize;
if(lifting->variableArray == 0) {
lifting->variableArray = ALLOC(satVariable_t, lifting->initNumVariables+1);
memset(lifting->variableArray, 0,
sizeof(satVariable_t) * (lifting->initNumVariables+1));
}
sat_CleanDatabase(lifting);
if(t->allsat->assertion) t->lifting->assertion = sat_ArrayDuplicate(t->allsat->assertion);
if(t->allsat->auxObj) t->lifting->auxObj = sat_ArrayDuplicate(t->allsat->auxObj);
objective = allsat->obj->space[0];
sat_MarkTransitiveFaninForNode(lifting, objective, CoiMask);
}
sat_PreProcessingForMixedNoCompact(lifting);
if(lifting->obj) sat_ArrayFree(lifting->obj);
lifting->obj = sat_ArrayAlloc(1);
sat_ArrayInsert(lifting->obj, (objective));
/*
* reset score of PI
* Since the scores of PI and current state variables are high than
* other variables because of blocking clauses that forwarded from
* prevous image step.
for(i=0; i<t->nInputs; i++) {
v = t->inputs[i];
var = lifting->variableArray[SATnodeID(v)];
var.scores[0] = 0;
var.scores[1] = 0;
}
for(i=0; i<t->nLatches; i++) {
v = t->cstates[i];
var = lifting->variableArray[SATnodeID(v)];
var.scores[0] = 0;
var.scores[1] = 0;
}
**/
lifting->currentDecision = -1;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigTransition_t* bAigCreateTransitionRelation | ( | Ntk_Network_t * | network, |
| mAig_Manager_t * | manager | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Create data structure for transition relation.]
Description [Create data structure for transition relation.]
SideEffects []
SeeAlso []
Definition at line 62 of file baigAllSat.c.
{
bAigTransition_t *t;
array_t *bVarList, *mVarList;
array_t *latcharr;
Ntk_Node_t *node, *dataInput;
mAigMvar_t mVar;
mAigBvar_t bVar;
st_table *node2MvfAigTable;
lsGen gen;
int nLatches, nInputs;
int i, j, index, index1;
int mAigId, maxCS;
bAigEdge_t v;
bAigEdge_t *cstates, *nstates, *inputs;
t = ALLOC(bAigTransition_t, 1);
memset(t, 0, sizeof(bAigTransition_t));
t->network = network;
t->manager = manager;
bVarList = mAigReadBinVarList(manager);
mVarList = mAigReadMulVarList(manager);
latcharr = array_alloc(Ntk_Node_t *, 16);
nLatches = 0;
Ntk_NetworkForEachLatch(network, gen, node) {
mAigId = Ntk_NodeReadMAigId(node);
mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
nLatches += mVar.encodeLength;
array_insert_last(Ntk_Node_t *, latcharr, node);
}
t->nLatches = nLatches;
node2MvfAigTable =
(st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
array_sort(latcharr, nodenameCompare);
cstates = ALLOC(bAigEdge_t, nLatches);
nstates = ALLOC(bAigEdge_t, nLatches);
t->tstates = ALLOC(bAigEdge_t, nLatches);
t->initials = ALLOC(bAigEdge_t, nLatches);
nLatches = 0;
maxCS = 0;
for(j=0; j<array_n(latcharr); j++) {
node = array_fetch(Ntk_Node_t *, latcharr, j);
mAigId = Ntk_NodeReadMAigId(node);
mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
index = nLatches;
for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
bVar = array_fetch(mAigBvar_t, bVarList, index1++);
v = bVar.node;
cstates[index++] = v;
if(maxCS < v)
maxCS = v;
}
dataInput = Ntk_LatchReadDataInput(node);
mAigId = Ntk_NodeReadMAigId(dataInput);
mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
index = nLatches;
for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
bVar = array_fetch(mAigBvar_t, bVarList, index1++);
v = bVar.node;
v = bAig_GetCanonical(manager, v);
nstates[index++] = v;
}
dataInput = Ntk_LatchReadInitialInput(node);
mAigId = Ntk_NodeReadMAigId(dataInput);
mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
index = nLatches;
for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
bVar = array_fetch(mAigBvar_t, bVarList, index1++);
v = bVar.node;
v = bAig_GetCanonical(manager, v);
t->initials[index++] = v;
}
nLatches = index;
}
nInputs = 0;
Ntk_NetworkForEachPrimaryInput(network, gen, node) {
mAigId = Ntk_NodeReadMAigId(node);
mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
nInputs += mVar.encodeLength;
}
Ntk_NetworkForEachPseudoInput(network, gen, node) {
mAigId = Ntk_NodeReadMAigId(node);
mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
nInputs += mVar.encodeLength;
}
t->nInputs = nInputs;
inputs = ALLOC(bAigEdge_t, nInputs);
nInputs = 0;
Ntk_NetworkForEachPrimaryInput(network, gen, node) {
mAigId = Ntk_NodeReadMAigId(node);
mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
bVar = array_fetch(mAigBvar_t, bVarList, index1++);
v = bVar.node;
inputs[nInputs++] = v;
}
}
Ntk_NetworkForEachPseudoInput(network, gen, node) {
mAigId = Ntk_NodeReadMAigId(node);
mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
bVar = array_fetch(mAigBvar_t, bVarList, index1++);
v = bVar.node;
inputs[nInputs++] = v;
}
}
t->cstates = cstates;
t->nstates = nstates;
t->inputs = inputs;
maxCS /= bAigNodeSize;
maxCS++;
t->csize = maxCS;
t->cobj = ALLOC(bAigEdge_t, maxCS);
memset(t->cobj, 0, sizeof(bAigEdge_t)*maxCS);
t->c2n = ALLOC(bAigEdge_t, maxCS);
memset(t->c2n, 0, sizeof(bAigEdge_t)*maxCS);
nLatches = t->nLatches;
for(i=0; i<nLatches; i++) {
v = t->cstates[i];
t->c2n[SATnodeID(v)] = t->nstates[i];
}
memcpy(t->tstates, cstates, sizeof(bAigEdge_t)*t->nLatches);
t->vinputs = ALLOC(int, t->nInputs);
memset(t->vinputs, 0, sizeof(int)*t->nInputs);
t->vtstates = ALLOC(int, t->nLatches);
memset(t->vtstates, 0, sizeof(int)*t->nLatches);
t->avgLits = 0;
t->sum = 0;
t->interval = 10;
t->period = 100;
array_free(latcharr);
return(t);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int bAigInclusionTestOnInitialStates | ( | bAigTransition_t * | t | ) |
Function********************************************************************
Synopsis [Check if the initial states are included in conjunction of block clauses.]
Description [Check if the initial states are included in conjunction of block clauses. It is done by checking satisfiability of formula (I B). If it is unsatisfiable then all the initial states are included in B.]
SideEffects []
SeeAlso []
Definition at line 598 of file baigAllSat.c.
{
satArray_t *cnfArray;
satOption_t *option;
char filename[1024];
int flag;
if(t->inclusionInitial == 0) return(1);
cnfArray = bAigCreateCNFInstanceForInclusionTestOnInitialStates(t);
option = sat_InitOption();
if(t->verbose > 2) {
sprintf(filename, "init%d.cnf", t->iteration);
sat_WriteCNFFromArray(cnfArray, filename);
}
flag = sat_CNFMainWithArray(option, cnfArray, 0, 0, 0);
sat_ArrayFree(cnfArray);
if(flag == SAT_UNSAT) return(1);
else return(0);
return(1);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAigMarkConeOfInfluenceForAX | ( | bAigTransition_t * | t, |
| satManager_t * | cm | ||
| ) |
Function********************************************************************
Synopsis [Mark cone of influence for AX.]
Description [Mark cone of influence for objective and intermediate variable that are created for complement frontier.]
SideEffects []
SeeAlso []
Definition at line 2303 of file baigAllSat.c.
{
satArray_t *arr;
int i;
bAigEdge_t v;
sat_MarkTransitiveFaninForNode(cm, t->objective, CoiMask);
if(t->tVariables) {
arr = t->tVariables;
for(i=0; i<arr->num; i++) {
v = arr->space[i];
SATflags(v) |= CoiMask;
}
}
if(t->auxObj) {
arr = t->auxObj;
for(i=0; i<arr->num; i++) {
v = arr->space[i];
sat_MarkTransitiveFaninForNode(cm, v, CoiMask);
}
}
if(t->objArr) {
arr = t->objArr;
for(i=0; i<arr->num; i++) {
v = arr->space[i];
sat_MarkTransitiveFaninForNode(cm, v, CoiMask);
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAigMinimizationBasedOnLifting | ( | bAigTransition_t * | t, |
| bAigEdge_t | obj, | ||
| satArray_t * | orderArray | ||
| ) |
Function********************************************************************
Synopsis [Apply minization based on checking antecedent of objective.]
Description [Apply minization based on checking antecedent of objective.]
SideEffects []
SeeAlso []
This is for incremental SAT to identified objective dependent conflict clauses
Make level 0 implication 1. Primary input since they are not the target of lifting 2. Unit and pure literals.. 3. Complemented objective
Apply lifting
check liftability of i'th variable on order array
implied by other decisions
check liftability of i'th variable on order array
to identify previous decision
implied by other decisions
decision variable
assign complemented value
the variable can be lifted
the variable can be lifted
the variable can be lifted
the variable can be lifted
Need further decision
There is a case that the implication queue is not empty
Forward clauses from lifting process to allsat process
Need to review this code
To check if the clause is safe to add allsat instance
Definition at line 1256 of file baigAllSat.c.
{
satManager_t *allsat, *cm;
satLevel_t *d;
satArray_t *tmpArray;
satArray_t *notLiftableArray;
bAigEdge_t v, tv, *plit;
bAigEdge_t lastNode, lastLit, ante;
int inverted, inserted;
int tvalue, value, bLevel;
int i, j, size;
cm = t->lifting;
allsat = t->allsat;
cm->option->includeLevelZeroLiteral = 1;
lastLit = cm->literals->last-cm->literals->begin;
lastNode = cm->nodesArraySize;
d = sat_AllocLevel(cm);
for(i=0; i<t->nInputs; i++) {
v = t->inputs[i];
if(!(SATflags(v) & CoiMask)) continue;
value = t->vinputs[i];
SATvalue(v) = value;
SATmakeImplied(v, d);
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
}
sat_ImplyArray(cm, d, cm->assertion);
sat_ImplyArray(cm, d, cm->unitLits);
sat_ImplyArray(cm, d, cm->pureLits);
sat_ImplyArray(cm, d, cm->auxObj);
sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
value = SATisInverted(obj);
v = SATnormalNode(obj);
SATvalue(v) = value;
SATmakeImplied(v, d);
if((SATflags(v) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
}
sat_ImplicationMain(cm, d);
for(i=0; i<orderArray->num; i++) {
cm->status = 0;
tv = orderArray->space[i];
v = SATnormalNode(tv);
value = SATvalue(v);
if(value < 2) {
continue;
}
value = !SATisInverted(tv);
SATvalue(v) = value;
d = sat_AllocLevel(cm);
SATmakeImplied(v, d);
if((SATflags(v) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
}
sat_ImplicationMain(cm, d);
}
notLiftableArray = sat_ArrayAlloc(orderArray->num);
for(i=orderArray->num-1; i>=0; i--) {
while(1) {
if(i<0) break;
tv = orderArray->space[i];
v = SATnormalNode(tv);
value = SATvalue(v);
ante = SATante(v);
if(ante) {
tvalue = !SATisInverted(tv);
if(tvalue == value)
sat_ArrayInsert(notLiftableArray, tv);
i--;
continue;
}
else {
sat_Backtrack(cm, SATlevel(v)-1);
break;
}
}
if(i<0) break;
bLevel = cm->currentDecision;
tv = orderArray->space[i];
value = SATisInverted(tv);
SATvalue(v) = value;
d = sat_AllocLevel(cm);
SATmakeImplied(v, d);
if((SATflags(v) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
}
sat_ImplicationMain(cm, d);
if(d->conflict) {
sat_Backtrack(cm, bLevel);
continue;
}
for(j=0; j<notLiftableArray->num; j++) {
v = notLiftableArray->space[j];
value = !SATisInverted(v);
v = SATnormalNode(v);
tvalue = SATvalue(v);
if(tvalue < 2 && tvalue != value) {
sat_Backtrack(cm, bLevel);
d->conflict = v;
continue;
}
SATvalue(v) = value;
SATmakeImplied(v, d);
if((SATflags(v) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
}
sat_ImplicationMain(cm, d);
if(d->conflict) {
break;
}
}
if(d->conflict) {
sat_Backtrack(cm, bLevel);
continue;
}
bAigSolverForLifting(cm, cm->currentDecision);
sat_CleanImplicationQueue(cm);
if(cm->status == SAT_SAT) {
sat_ArrayInsert(notLiftableArray, tv);
}
sat_Backtrack(cm, bLevel);
}
memcpy(orderArray->space, notLiftableArray->space, sizeof(long)*notLiftableArray->num);
orderArray->num = notLiftableArray->num;
sat_ArrayFree(notLiftableArray);
sat_Backtrack(cm, 0);
d = SATgetDecision(cm->currentDecision);
sat_Undo(cm, d);
cm->currentDecision--;
cm->status = 0;
tmpArray = sat_ArrayAlloc(64);
for(i=lastNode; i<cm->nodesArraySize; i+=satNodeSize) {
size = SATnumLits(i);
plit = (long*)SATfirstLit(i);
inserted = 0;
tmpArray->num = 0;
for(j=0; j<size; j++, plit++) {
v = SATgetNode(*plit);
inverted = SATisInverted(v);
v = SATnormalNode(v);
value = (allsat->nodesArray[v+satValue]) ;
value = value ^ inverted;
if(value > 0)
inserted = 1;
sat_ArrayInsert(tmpArray, v^(!inverted));
}
if(inserted)
sat_AddConflictClause(allsat, tmpArray, 0);
}
sat_ArrayFree(tmpArray);
return;
}
Here is the call graph for this function:
| void bAigMinimizationBasedOnLiftingAllAtOnce | ( | bAigTransition_t * | t, |
| bAigEdge_t | obj, | ||
| satArray_t * | orderArray | ||
| ) |
Function********************************************************************
Synopsis [Apply minization based on checking antecedent of objective.]
Description [Apply minization based on checking antecedent of objective.]
SideEffects []
SeeAlso []
This is for incremental SAT to identified objective dependent conflict clauses
Make level 0 implication 1. Primary input since they are not the target of lifting 2. Unit and pure literals.. 3. Complemented objective
Apply lifting
check liftability of i'th variable on order array
Need further decision
There is a case that the implication queue is not empty
Definition at line 1470 of file baigAllSat.c.
{
satManager_t *allsat, *cm;
satLevel_t *d;
satArray_t *implied;
satArray_t *notLiftableArray;
bAigEdge_t v, tv;
bAigEdge_t lastNode, lastLit;
long *space;
int value;
int i, j, size, num;
cm = t->lifting;
allsat = t->allsat;
cm->option->includeLevelZeroLiteral = 1;
lastLit = cm->literals->last-cm->literals->begin;
lastNode = cm->nodesArraySize;
d = sat_AllocLevel(cm);
for(i=0; i<t->nInputs; i++) {
v = t->inputs[i];
if(!(SATflags(v) & CoiMask)) continue;
value = t->vinputs[i];
SATvalue(v) = value;
SATmakeImplied(v, d);
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
}
sat_ImplyArray(cm, d, cm->assertion);
sat_ImplyArray(cm, d, cm->unitLits);
sat_ImplyArray(cm, d, cm->pureLits);
sat_ImplyArray(cm, d, cm->auxObj);
sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
value = SATisInverted(obj);
v = SATnormalNode(obj);
SATvalue(v) = value;
SATmakeImplied(v, d);
if((SATflags(v) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
}
sat_ImplicationMain(cm, d);
num = d->implied->num;
notLiftableArray = sat_ArrayAlloc(orderArray->num);
for(i=0; i<orderArray->num; i++) {
cm->status = 0;
d->conflict = 0;
tv = orderArray->space[i];
v = SATnormalNode(tv);
value = SATisInverted(tv);
SATvalue(v) = value;
SATmakeImplied(v, d);
if((SATflags(v) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
}
for(j=i+1; j<orderArray->num; j++) {
v = orderArray->space[j];
value = !SATisInverted(v);
v = SATnormalNode(v);
SATvalue(v) = value;
SATmakeImplied(v, d);
if((SATflags(v) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
}
}
for(j=0; j<notLiftableArray->num; j++) {
v = notLiftableArray->space[j];
value = !SATisInverted(v);
v = SATnormalNode(v);
SATvalue(v) = value;
SATmakeImplied(v, d);
if((SATflags(v) & InQueueMask) == 0) {
sat_Enqueue(cm->queue, v);
SATflags(v) |= InQueueMask;
}
}
sat_ImplicationMain(cm, d);
if(d->conflict == 0) {
bAigSolverForLifting(cm, 0);
sat_CleanImplicationQueue(cm);
}
else {
cm->status = SAT_UNSAT;
}
if(cm->status == SAT_SAT) {
sat_ArrayInsert(notLiftableArray, tv);
sat_Backtrack(cm, 0);
}
d = SATgetDecision(0);
implied = d->implied;
space = implied->space;
size = implied->num;
for(j=num; j<size; j++) {
v = space[j];
SATvalue(v) = 2;
SATflags(v) &= ResetNewVisitedObjInQueueMask;
SATante(v) = 0;
SATante2(v) = 0;
SATlevel(v) = -1;
}
implied->num = num;
cm->currentDecision = 0;
}
memcpy(orderArray->space, notLiftableArray->space, sizeof(long)*notLiftableArray->num);
orderArray->num = notLiftableArray->num;
sat_ArrayFree(notLiftableArray);
d = SATgetDecision(0);
sat_Undo(cm, d);
cm->status = 0;
cm->currentDecision = -1;
#if 0
tmpArray = sat_ArrayAlloc(64);
for(i=lastNode; i<cm->nodesArraySize; i+=satNodeSize) {
size = SATnumLits(i);
plit = (long*)SATfirstLit(i);
inserted = 0;
tmpArray->num = 0;
for(j=0; j<size; j++, plit++) {
tv = SATgetNode(*plit);
inverted = SATisInverted(tv);
v = SATnormalNode(tv);
value = (allsat->nodesArray[v+satValue]) ;
value = value ^ inverted;
if(value > 0)
inserted = 1;
sat_ArrayInsert(tmpArray, SATnot(tv));
}
if(inserted)
sat_AddConflictClause(allsat, tmpArray, 0);
}
sat_ArrayFree(tmpArray);
#endif
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAigPreProcessingForLiftingInstance | ( | bAigTransition_t * | t, |
| satManager_t * | cm | ||
| ) |
Function********************************************************************
Synopsis [ Pre-processing to run CirCUs with AIG and CNF]
Description [ Pre-processing to run CirCUs with AIG and CNF]
SideEffects [ One has to run sat_PostProcessing for AllSat enumeration after running CirCUs]
SeeAlso [ sat_PostProcessing ]
create implication queue
create variable array : one can reduce size of variable array using mapping. for fanout free internal node....
compact fanout of AIG node sat_CompactFanout(cm);
Initial score
create decision stack
to avoid purify warning
incremental SAT....
Level 0 decision....
There is a case that circuit consists of single objective node
Definition at line 2140 of file baigAllSat.c.
{
satLevel_t *d;
int i;
long v;
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));
}
if(cm->auxArray == 0)
cm->auxArray = sat_ArrayAlloc(1024);
if(cm->nonobjUnitLitArray == 0)
cm->nonobjUnitLitArray = sat_ArrayAlloc(128);
if(cm->objUnitLitArray == 0)
cm->objUnitLitArray = sat_ArrayAlloc(128);
cm->initNodesArraySize = cm->nodesArraySize;
cm->beginConflict = cm->nodesArraySize;
if(cm->option->allSatMode) {
sat_RestoreFrontierClauses(cm);
sat_RestoreBlockingClauses(cm);
}
sat_InitScoreForMixed(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;
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;
for(i=0; i<cm->pureLits->num; i++) {
v = cm->pureLits->space[i];
if(v == t->objective) {
for(;i<cm->pureLits->num; i++) {
cm->pureLits->space[i] = cm->pureLits->space[i+1];
}
cm->pureLits->num--;
break;
}
}
sat_ImplyArray(cm, d, cm->assertion);
sat_ImplyArray(cm, d, cm->unitLits);
sat_ImplyArray(cm, d, cm->pureLits);
sat_ImplyArray(cm, d, cm->auxObj);
sat_ImplyArray(cm, d, cm->nonobjUnitLitArray);
sat_ImplyArray(cm, d, cm->obj);
sat_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 bAigPrintTransitionInfo | ( | bAigTransition_t * | t | ) |
Function********************************************************************
Synopsis [Function to print information of bAigTransition_t]
Description [Function to print information of bAigTransition_t]
SideEffects []
SeeAlso []
Definition at line 2938 of file baigAllSat.c.
{
int i;
fprintf(vis_stdout, "Transition relation information in terms of AIG\n");
fprintf(vis_stdout, "objective : %ld\n", t->objective);
fprintf(vis_stdout, "number of primary inputs : %d\n", t->nInputs);
fprintf(vis_stdout, "number of states variables : %d\n", t->nLatches);
fprintf(vis_stdout, "primary inputs :");
for(i=0; i<t->nInputs; i++) {
fprintf(vis_stdout, "%5ld ", t->inputs[i]);
if((i+1)%10 == 0 && i > 0)
fprintf(vis_stdout, "\n ");
}
fprintf(vis_stdout, "\n");
fprintf(vis_stdout, "state variables :");
for(i=0; i<t->nLatches; i++) {
fprintf(vis_stdout, "%5ld(%5ld):%5ld ",
t->cstates[i], t->initials[i], t->nstates[i]);
if((i+1)%3 == 0 && i > 0)
fprintf(vis_stdout, "\n ");
}
fprintf(vis_stdout, "\n");
}
Here is the caller graph for this function:
| void bAigReduceBlockingClauseWithUnsatCore | ( | bAigTransition_t * | t | ) |
Function********************************************************************
Synopsis [Reduce the number of blocking clauses based on UNSAT core generation.]
Description [Reduce the number of blocking clauses based on UNSAT core generation.]
SideEffects []
SeeAlso []
Collect CNF from frontier of previous run
Collect transition function(AIG) for CNF translation
Collect all previous blocking clauses
add objecitve into CNF instance
else { fprintf(stdout, "ERROR : the clause %ld should be in the mapping table\n", v); }
Definition at line 463 of file baigAllSat.c.
{
satArray_t *cnfArray;
satArray_t *coreArray;
satArray_t *rootArray;
satOption_t *option;
satManager_t *cm;
st_table *mappedTable;
char filename[1024];
int flag, i, size;
bAigEdge_t v, nv, *plit;
cnfArray = sat_ArrayAlloc(1024);
mappedTable = st_init_table(st_numcmp, st_numhash);
sat_ArrayInsert(cnfArray, 0);
cm = t->allsat;
for(v = cm->frontierNodesBegin; v<cm->frontierNodesEnd; v+= satNodeSize) {
if(!(SATflags(v) & IsCNFMask)) continue;
size = SATnumLits(v);
plit = (long*)SATfirstLit(v);
for(i=0; i<size; i++, plit++) {
nv = SATgetNode(*plit);
sat_ArrayInsert(cnfArray, nv);
nv = SATnormalNode(nv);
SATflags(nv) |= VisitedMask;
}
sat_ArrayInsert(cnfArray, 0);
}
rootArray = sat_ArrayAlloc(t->nLatches);
for(i=0; i<t->nLatches; i++) {
v = t->nstates[i];
v = SATnormalNode(v);
if(v>1 && (SATflags(v) & VisitedMask))
sat_ArrayInsert(rootArray, v);
}
for(i=0; i<rootArray->num; i++) {
v = rootArray->space[i];
SATflags(v) &= ResetVisitedMask;
}
if(cm->maxNodesArraySize > t->manager->maxNodesArraySize) {
t->manager->maxNodesArraySize = cm->maxNodesArraySize;
t->manager->nameList = REALLOC(char *, t->manager->nameList , t->manager->maxNodesArraySize/bAigNodeSize);
t->manager->bddIdArray = REALLOC(int , t->manager->bddIdArray , t->manager->maxNodesArraySize/bAigNodeSize);
t->manager->bddArray = REALLOC(bdd_t *, t->manager->bddArray , t->manager->maxNodesArraySize/bAigNodeSize);
}
t->manager->maxNodesArraySize = cm->maxNodesArraySize;
t->manager->NodesArray = cm->nodesArray;
bAig_CreateCNFFromAIG(t->manager, rootArray, cnfArray);
sat_ArrayFree(rootArray);
for(v = cm->frontierNodesEnd; v<cm->nodesArraySize; v+= satNodeSize) {
if(!(SATflags(v) & IsCNFMask)) continue;
if(!(SATflags(v) & IsBlockingMask)) continue;
size = SATnumLits(v);
plit = (long*)SATfirstLit(v);
for(i=0; i<size; i++, plit++) {
nv = SATgetNode(*plit);
sat_ArrayInsert(cnfArray, nv);
}
sat_ArrayInsert(cnfArray, -v);
}
sat_ArrayInsert(cnfArray, t->objective);
sat_ArrayInsert(cnfArray, 0);
option = sat_InitOption();
if(t->verbose > 2) {
sprintf(filename, "core%d.cnf", t->iteration);
sat_WriteCNFFromArray(cnfArray, filename);
}
coreArray = sat_ArrayAlloc(1024);
flag = sat_CNFMainWithArray(option, cnfArray, 1, coreArray, mappedTable);
if(flag == SAT_SAT) {
sprintf(filename, "core%d.cnf", t->iteration);
fprintf(stdout, "ERROR : this instance %s should be UNSAT\n", filename);
sat_WriteCNFFromArray(cnfArray, filename);
}
for(i=0; i<coreArray->num; i++) {
v = coreArray->space[i];
if(st_lookup(mappedTable, (char *)v, &nv)) {
/* If a clause is blocking clause then it is in the table **/
SATflags(nv) |= InCoreMask;
}
}
for(v=satNodeSize; v<cm->nodesArraySize; v+=satNodeSize) {
if(!(SATflags(v) & IsCNFMask))
continue;
if(!(SATflags(v) & IsBlockingMask))
continue;
if(!(SATflags(v) & IsFrontierMask))
continue;
if((SATflags(v) & InCoreMask))
continue;
SATresetInUse(v);
if(t->verbose > 4) {
fprintf(vis_stdout, "NOTICE : deleted blocking clause\n");
sat_PrintNode(cm, v);
}
}
st_free_table(mappedTable);
sat_ArrayFree(cnfArray);
sat_ArrayFree(coreArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAigSolveAllSatWithLifting | ( | bAigTransition_t * | t | ) |
Function********************************************************************
Synopsis [Enumerate solution with lifting.]
Description [Enumerate solution with lifting.]
SideEffects []
SeeAlso []
option->decisionHeuristic = 0; option->decisionHeuristic |= DVH_DECISION;
Definition at line 905 of file baigAllSat.c.
{
satManager_t *cm;
satLevel_t *d;
satOption_t *option;
int level;
cm = t->allsat;
d = SATgetDecision(0);
cm->implicatedSoFar = d->implied->num;
cm->currentTopConflict = 0;
option = cm->option;
if(cm->status == SAT_UNSAT) {
sat_Undo(cm, SATgetDecision(0));
return;
}
while(1) {
sat_PeriodicFunctions(cm);
d = sat_MakeDecision(cm);
if(d == 0) {
bAigBlockingClauseAnalysisBasedOnLifting(t, cm);
if(cm->currentDecision == -1) {
sat_Undo(cm, SATgetDecision(0));
cm->status = SAT_UNSAT;
return;
}
d = SATgetDecision(cm->currentDecision);
}
while(1) {
sat_ImplicationMain(cm, d);
if(d->conflict == 0)
break;
level = sat_ConflictAnalysis(cm, d);
if(cm->currentDecision == -1) {
sat_Undo(cm, SATgetDecision(0));
cm->status = SAT_UNSAT;
return;
}
d = SATgetDecision(cm->currentDecision);
}
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAigSolverForLifting | ( | satManager_t * | cm, |
| int | tLevel | ||
| ) |
Function********************************************************************
Synopsis [SAT solver for lifting .]
Description [SAT solver for lifting. ]
SideEffects []
SeeAlso []
Definition at line 1658 of file baigAllSat.c.
{
satLevel_t *d;
int level;
d = SATgetDecision(0);
cm->implicatedSoFar = d->implied->num;
while(1) {
d = sat_MakeDecision(cm);
if(d == 0) {
cm->status = SAT_SAT;
return;
}
while(1) {
sat_ImplicationMain(cm, d);
if(d->conflict == 0)
break;
level = sat_ConflictAnalysisForLifting(cm, d);
if(cm->currentDecision <= -1) {
cm->status = SAT_UNSAT;
return;
}
d = SATgetDecision(cm->currentDecision);
}
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int indexCompare | ( | const void * | node1, |
| const void * | node2 | ||
| ) | [static] |
Function********************************************************************
Synopsis [Function to check the index ]
Description [Function to check the index ]
SideEffects []
SeeAlso []
Definition at line 3059 of file baigAllSat.c.
{
bAigEdge_t v1, v2;
v1 = *(bAigEdge_t *)(node1);
v2 = *(bAigEdge_t *)(node2);
return(v1 > v2);
}
Here is the caller graph for this function:
| static int levelCompare | ( | const void * | node1, |
| const void * | node2 | ||
| ) | [static] |
Function********************************************************************
Synopsis [Function to check the deicison level of variable ]
Description [Function to check the deicison level of variable ]
SideEffects []
SeeAlso []
Definition at line 3032 of file baigAllSat.c.
{
bAigEdge_t v1, v2;
int l1, l2;
v1 = *(bAigEdge_t *)(node1);
v2 = *(bAigEdge_t *)(node2);
l1 = SATcm->variableArray[SATnodeID(v1)].level;
l2 = SATcm->variableArray[SATnodeID(v2)].level;
if(l1 == l2) return(v1 > v2);
return (l1 > l2);
}
Here is the caller graph for this function:
| static int nodenameCompare | ( | const void * | node1, |
| const void * | node2 | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Function to arrange node to the alphabetic order ]
Description [Function to arrange node to the alphabetic order ]
SideEffects []
SeeAlso []
Definition at line 2977 of file baigAllSat.c.
{
Ntk_Node_t *v1, *v2;
char *name1, *name2;
v1 = *(Ntk_Node_t **)(node1);
v2 = *(Ntk_Node_t **)(node2);
name1 = Ntk_NodeReadName(v1);
name2 = Ntk_NodeReadName(v2);
return (strcmp(name1, name2));
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int StringCheckIsInteger | ( | char * | string, |
| int * | value | ||
| ) | [static] |
Function********************************************************************
Synopsis [Function to check if given string is integer]
Description [Function to check if given string is integer]
SideEffects []
SeeAlso []
Definition at line 3004 of file baigAllSat.c.
{
char *ptr;
long l;
l = strtol (string, &ptr, 0) ;
if(*ptr != '\0')
return 0;
if ((l > MAXINT) || (l < -1 - MAXINT))
return 1 ;
*value = (int) l;
return 2 ;
}
Here is the caller graph for this function:
Variable Documentation
satManager_t* SATcm [static] |
Definition at line 26 of file baigAllSat.c.
char rcsid [] UNUSED = "$Id: baigAllSat.c,v 1.4 2009/04/11 02:40:01 fabio Exp $" [static] |
CFile***********************************************************************
FileName [baigAllSat.c]
PackageName [baig]
Synopsis [Routines to check sat-based invariant checking.]
Author [HoonSang Jin]
Copyright [ This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
Definition at line 25 of file baigAllSat.c.
