#include "puresatInt.h"#include "sat.h"
Include dependency graph for puresatUtil.c:
Go to the source code of this file.
Functions | |
| PureSat_Manager_t * | PureSatManagerAlloc (void) |
| void | PureSatManagerFree (PureSat_Manager_t *pm) |
| PureSat_IncreSATManager_t * | PureSatIncreSATManagerAlloc (PureSat_Manager_t *pm) |
| void | PureSatIncreSATManagerFree (PureSat_Manager_t *pm, PureSat_IncreSATManager_t *pism) |
| void | PureSatBmcGetCoiForNtkNode (Ntk_Node_t *node, st_table *CoiTable, st_table *visited) |
| void | PureSatBmcGetCoiForLtlFormulaRecursive (Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable, st_table *visited) |
| DfsColor | PureSatNodeReadColor (Ntk_Node_t *node) |
| void | PureSatNodeSetColor (Ntk_Node_t *node, DfsColor color) |
| void | PureSatNodeRecursivelyComputeTransitiveFaninNodes_AllNodes (Ntk_Node_t *node, int *NumofSupports, boolean stopAtLatches) |
| int | PureSatNodeComputeCombinationalSupport_AllNodes (Ntk_Network_t *network, array_t *nodeArray, boolean stopAtLatches) |
| void | PureSatGenerateSupportTable (Ntk_Network_t *network, PureSat_Manager_t *pm) |
| void | PureSatBmcGetCoiForLtlFormula (Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable) |
| void | PureSatGetFormulaNodes (Ntk_Network_t *network, Ctlsp_Formula_t *F, array_t *formulaNodes) |
| void | PureSatGetFaninLatches (Ntk_Node_t *node, st_table *visited, st_table *vertexTable) |
| st_table * | PureSatCreateInitialAbstraction (Ntk_Network_t *network, Ctlsp_Formula_t *invFormula, int *Num, PureSat_Manager_t *pm) |
| void | PureSatRecursivelyComputeTableForLatch (Ntk_Network_t *network, st_table *Table, Ntk_Node_t *node) |
| void | PureSatComputeTableForLatch (Ntk_Network_t *network, st_table *Table, Ntk_Node_t *Latch) |
| void | PureSatGetCoiForVisibleArray_Ring (Ntk_Network_t *network, array_t *visibleArray, int position, st_table *ltlCoiTable) |
| int | NumInConeCompare (int *ptrX, int *ptrY) |
| int | NumInConeCompare_Ring (int *ptrX, int *ptrY) |
| void | PureSatRecursivelyComputeCorrelationforLatch (Ntk_Network_t *network, st_table *AbsTable, st_table *visited, Ntk_Node_t *node, int *count) |
| int | PureSatComputeCorrelationforLatch (Ntk_Network_t *network, st_table *AbsTable, Ntk_Node_t *Latch) |
| array_t * | PureSatGenerateRingFromAbs (Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *invisibleArray, int *NumInSecondLevel) |
| void | PureSatCleanSat (satManager_t *cm) |
| void | PureSatReadClauses (PureSat_IncreSATManager_t *pism, PureSat_Manager_t *pm) |
| array_t * | PureSatGetImmediateSupportLatches (Ntk_Network_t *network, int beginPosition, array_t *latchNameArray) |
| void | PureSatWriteClausesToFile (PureSat_IncreSATManager_t *pism, mAig_Manager_t *maigManager, char *coreFile) |
| void | PureSatWriteAllClausesToFile (PureSat_IncreSATManager_t *pism, char *coreFile) |
| array_t * | PureSatGetLatchFromTable (Ntk_Network_t *network, PureSat_Manager_t *pm, char *coreFile) |
| array_t * | PureSatRemove_char (array_t *array1, int i) |
| void | PureSatComputeNumGatesInAbsForNode (Ntk_Network_t *network, PureSat_Manager_t *pm, Ntk_Node_t *node, st_table *visited, int *ct, int *ct1) |
| void | PureSatComputeNumGatesInAbs (Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *invisibleArray) |
| void | PureSatComputeNumGatesInConeForNode (Ntk_Network_t *network, PureSat_Manager_t *pm, Ntk_Node_t *node, st_table *visited, int *ct) |
| void | PureSatComputeNumGatesInCone (Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *latchArray) |
| array_t * | PureSatGenerateRCArray_2 (Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *invisibleArray, int *NumInSecondLevel) |
Variables | |
| static array_t * | RCArray |
| static int | DfsLevel = 0 |
| static array_t * | NumInCone |
| static array_t * | NumInAbs |
| static array_t * | DfsArray |
Function Documentation
| int NumInConeCompare | ( | int * | ptrX, |
| int * | ptrY | ||
| ) |
Function********************************************************************
Synopsis [Compare function for quick sort]
Description [Compare function for quick sort]
SideEffects []
SeeAlso []
Definition at line 768 of file puresatUtil.c.
{
int a,b;
int c,d;
double e,f;
a = array_fetch(int,NumInCone,(int)*ptrX);
b = array_fetch(int,NumInCone,(int)*ptrY);
c = array_fetch(int,NumInAbs,(int)*ptrX);
d = array_fetch(int,NumInAbs,(int)*ptrY);
e = (double)c/(double)a;
f = (double)d/(double)b;
if(e > f)
return -1;
if( e < f)
return 1;
return 0;
}
| int NumInConeCompare_Ring | ( | int * | ptrX, |
| int * | ptrY | ||
| ) |
Function********************************************************************
Synopsis [Compare function for quick sort]
Description [Compare function for quick sort]
SideEffects []
SeeAlso []
Definition at line 801 of file puresatUtil.c.
{
int a,b;
double c,d;
double e,f;
a = array_fetch(int,DfsArray,(int)*ptrX);
b = array_fetch(int,DfsArray,(int)*ptrY);
c = array_fetch(double,RCArray,(int)*ptrX);
d = array_fetch(double,RCArray,(int)*ptrY);
e = (double)((a)*1000000)-c;
f = (double)((b)*1000000)-d;
if(e > f)
return 1;
if( e < f)
return -1;
return 0;
}
Here is the caller graph for this function:
| void PureSatBmcGetCoiForLtlFormula | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | formula, | ||
| st_table * | ltlCoiTable | ||
| ) |
Function********************************************************************
Synopsis [Compute the cone of influence for a ltl formula]
Description [Compute the cone of influence for a ltl formula]
SideEffects []
SeeAlso []
Definition at line 501 of file puresatUtil.c.
{
st_table *visited = st_init_table(st_ptrcmp, st_ptrhash);
PureSatBmcGetCoiForLtlFormulaRecursive(network, formula, ltlCoiTable, visited);
st_free_table(visited);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatBmcGetCoiForLtlFormulaRecursive | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | formula, | ||
| st_table * | ltlCoiTable, | ||
| st_table * | visited | ||
| ) |
Function********************************************************************
Synopsis [Get the cone of influence for a ltl formula]
Description [Get the cone of influence for a ltl formula]
SideEffects []
SeeAlso []
Definition at line 313 of file puresatUtil.c.
{
if (formula == NIL(Ctlsp_Formula_t)) {
return;
}
/* leaf node */
if (formula->type == Ctlsp_ID_c){
char *name = Ctlsp_FormulaReadVariableName(formula);
Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, name);
int tmp;
if (st_lookup_int(visited, node, &tmp)){
/* Node already visited */
return;
}
PureSatBmcGetCoiForNtkNode(node, ltlCoiTable, visited);
return;
}
PureSatBmcGetCoiForLtlFormulaRecursive(network, formula->left, ltlCoiTable, visited);
PureSatBmcGetCoiForLtlFormulaRecursive(network, formula->right, ltlCoiTable, visited);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatBmcGetCoiForNtkNode | ( | Ntk_Node_t * | node, |
| st_table * | CoiTable, | ||
| st_table * | visited | ||
| ) |
Function********************************************************************
Synopsis [Get the cone of influence for a network node]
Description [Get the cone of influence for a network node]
SideEffects []
SeeAlso []
Definition at line 258 of file puresatUtil.c.
{
int i, j;
Ntk_Node_t *faninNode;
if(node == NIL(Ntk_Node_t)){
return;
}
if(Ntk_NodeTestIsLatch(node)){
DfsLevel++;
if (st_lookup_int(CoiTable, node, &j)&&j<=DfsLevel){
DfsLevel--;
return;
}
}
if (st_lookup_int(visited, node, &j)&&j<=DfsLevel){
if(Ntk_NodeTestIsLatch(node))
DfsLevel--;
return;
}
st_insert(visited, node, (char *)(long)DfsLevel);
if (Ntk_NodeTestIsLatch(node)){
st_insert(CoiTable, node, (char *)(long)DfsLevel);
}
if(Ntk_NodeTestIsInput(node))
{
return;
}
Ntk_NodeForEachFanin(node, i, faninNode) {
PureSatBmcGetCoiForNtkNode(faninNode, CoiTable, visited);
}
if(Ntk_NodeTestIsLatch(node))
DfsLevel--;
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatCleanSat | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [Clean the SAT solver after a SAT solving procedure is done]
Description [Clean the SAT solver after a SAT solving procedure is done]
SideEffects []
SeeAlso []
Definition at line 1028 of file puresatUtil.c.
{
int i;
satVariable_t *var;
satLevel_t *d;
cm->nodesArraySize = satNodeSize;
sat_ArrayFree(cm->unitLits);
sat_ArrayFree(cm->pureLits);
cm->unitLits = sat_ArrayAlloc(16);
cm->pureLits = sat_ArrayAlloc(16);
memset(cm->each,0,sizeof(satStatistics_t));
cm->literals->last = cm->literals->begin+1;
cm->literals->initialSize = cm->literals->last;
cm->status = 0;
cm->currentVarPos = 0;
cm->currentTopConflict = 0;
cm->lowestBacktrackLevel = 0;
cm->implicatedSoFar = 0;
/*cm->decisionHead = ALLOC(satLevel_t, cm->decisionHeadSize);*/
memset(cm->decisionHead, 0, sizeof(satLevel_t) * cm->decisionHeadSize);
/* FREE(cm->variableArray);
cm->variableArray = 0;*/
if(cm->variableArray) {
for(i=0; i<=cm->initNumVariables; i++) {
var = &(cm->variableArray[i]);
if(var->wl[0]) {
sat_ArrayFree(var->wl[0]);
var->wl[0] = 0;
}
if(var->wl[1]) {
sat_ArrayFree(var->wl[1]);
var->wl[1] = 0;
}
}
free(cm->variableArray);
cm->variableArray = 0;
}
if(cm->decisionHead) {
for(i=0; i<cm->decisionHeadSize; i++) {
d = &(cm->decisionHead[i]);
if(d->implied)
sat_ArrayFree(d->implied);
if(d->satisfied)
sat_ArrayFree(d->satisfied);
}
free(cm->decisionHead);
cm->decisionHead = 0;
cm->decisionHeadSize = 0;
}
sat_FreeQueue(cm->queue);
cm->queue = 0;
sat_FreeQueue(cm->BDDQueue);
cm->BDDQueue = 0;
sat_FreeQueue(cm->unusedAigQueue);
cm->unusedAigQueue = 0;
sat_ArrayFree(cm->auxArray);
sat_ArrayFree(cm->nonobjUnitLitArray);
sat_ArrayFree(cm->objUnitLitArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int PureSatComputeCorrelationforLatch | ( | Ntk_Network_t * | network, |
| st_table * | AbsTable, | ||
| Ntk_Node_t * | Latch | ||
| ) |
Function********************************************************************
Synopsis [Compute the relative correlation of a latch. For more information of Relative Correlation, please check the BMC'03 and STTT'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", and " Abstraction in symbolic model checking using satisfiability as the only decision procedure"]
Description [Compute the relative correlation of a latch. For more information of Relative Correlation, please check the BMC'03 and STTT'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", and " Abstraction in symbolic model checking using satisfiability as the only decision procedure"]
SideEffects []
SeeAlso []
Definition at line 890 of file puresatUtil.c.
{
int count =0,i;
Ntk_Node_t * fanin;
st_table *visited = st_init_table(st_ptrcmp,st_ptrhash);
Ntk_NodeForEachFanin(Latch,i,fanin)
PureSatRecursivelyComputeCorrelationforLatch(network,AbsTable,visited,fanin,&count);
st_free_table(visited);
return count*10000;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatComputeNumGatesInAbs | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| array_t * | invisibleArray | ||
| ) |
Function********************************************************************
Synopsis [For nodes in one array: count number of gates and how many of them are already in abstraction]
Description []
SideEffects []
SeeAlso []
Definition at line 1503 of file puresatUtil.c.
{
int i,ct,ct1,j;
char * name;
Ntk_Node_t * node,*fanin;
st_table * visited;
arrayForEachItem(char*,invisibleArray,i,name){
node = Ntk_NetworkFindNodeByName(network,name);
ct = 0;
ct1 = 0;
visited = st_init_table(st_ptrcmp,st_ptrhash);
st_insert(visited,node,(char *)0);
ct1++;
Ntk_NodeForEachFanin(node,j,fanin){
if(!st_lookup(visited,(char *)fanin,NIL(char *))&&
!Ntk_NodeTestIsLatch(fanin))
PureSatComputeNumGatesInAbsForNode(network,pm,
fanin,visited,&ct,&ct1);
}
st_insert(pm->niaTable,name,(char*)(long)ct);
st_free_table(visited);
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatComputeNumGatesInAbsForNode | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| Ntk_Node_t * | node, | ||
| st_table * | visited, | ||
| int * | ct, | ||
| int * | ct1 | ||
| ) |
Function********************************************************************
Synopsis [For one node: count number of gates and how many of them are already in abstraction]
Description []
SideEffects []
SeeAlso []
Definition at line 1460 of file puresatUtil.c.
{
int i;
Ntk_Node_t *fanin;
st_insert(visited,node,(char *)0);
(*ct1)++;
if(st_lookup(pm->AbsTable,node,NIL(char*)))
(*ct)++;
if(Ntk_NodeTestIsCombInput(node))
return;
Ntk_NodeForEachFanin(node,i,fanin){
if(!st_lookup(visited,(char *)fanin,NIL(char *))&&
!Ntk_NodeTestIsLatch(fanin))
PureSatComputeNumGatesInAbsForNode(network,pm,fanin,visited,ct,ct1);
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatComputeNumGatesInCone | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| array_t * | latchArray | ||
| ) |
Function********************************************************************
Synopsis [For each node in one array: count how many nodes are in its cone]
Description []
SideEffects []
SeeAlso []
Definition at line 1588 of file puresatUtil.c.
{
int i,ct,j;
char * name;
Ntk_Node_t * node,* fanin;
st_table * visited;
arrayForEachItem(char*,latchArray,i,name){
node = Ntk_NetworkFindNodeByName(network,name);
ct = 0;
visited = st_init_table(st_ptrcmp,st_ptrhash);
st_insert(visited,node,(char *)0);
ct++;
Ntk_NodeForEachFanin(node,j,fanin){
if(!st_lookup(visited,(char *)fanin,NIL(char *))&&
!Ntk_NodeTestIsLatch(fanin))
PureSatComputeNumGatesInConeForNode(network,pm
,fanin,visited,&ct);
}
st_insert(pm->nicTable,name,(char*)(long)ct);
st_free_table(visited);
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatComputeNumGatesInConeForNode | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| Ntk_Node_t * | node, | ||
| st_table * | visited, | ||
| int * | ct | ||
| ) |
Function********************************************************************
Synopsis [For one node: count how many nodes are in its cone]
Description []
SideEffects []
SeeAlso []
Definition at line 1549 of file puresatUtil.c.
{
int i;
Ntk_Node_t *fanin;
st_insert(visited,node,(char *)0);
(*ct)++;
if(Ntk_NodeTestIsCombInput(node))
return;
Ntk_NodeForEachFanin(node,i,fanin){
if(!st_lookup(visited,(char *)fanin,NIL(char *))&&
!Ntk_NodeTestIsLatch(fanin))
PureSatComputeNumGatesInConeForNode(network,pm,fanin,visited,ct);
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatComputeTableForLatch | ( | Ntk_Network_t * | network, |
| st_table * | Table, | ||
| Ntk_Node_t * | Latch | ||
| ) |
Function********************************************************************
Synopsis [Get direct fan in gates of a node]
Description [Get direct fan in gates of a node]
SideEffects []
SeeAlso []
Definition at line 693 of file puresatUtil.c.
{
Ntk_Node_t * fanin;
int i;
if(!Ntk_NodeTestIsLatch(Latch))
{
char * name = Ntk_NodeReadName(Latch);
fprintf(vis_stdout,"%s is not a latch!\n",name);
exit (0);
}
if(!st_lookup(Table,Latch,NIL(char *)))
{
st_insert(Table,Latch, (char *)0);
Ntk_NodeForEachFanin(Latch,i,fanin)
PureSatRecursivelyComputeTableForLatch(network,Table,fanin);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| st_table* PureSatCreateInitialAbstraction | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | invFormula, | ||
| int * | Num, | ||
| PureSat_Manager_t * | pm | ||
| ) |
Function********************************************************************
Synopsis [Build a vertex table which stores all the latches in the beginning abstract model]
Description [The table contains only those immediate fanin latches of the given formula.]
SideEffects []
SeeAlso []
Definition at line 598 of file puresatUtil.c.
{
array_t *formulaNodes = array_alloc(Ntk_Node_t *, 0);
Ntk_Node_t *node;
int i;
st_table *vertexTable = st_init_table(strcmp, st_strhash);
st_table *visited = st_init_table(st_ptrcmp, st_ptrhash);
*Num=0;
PureSatGetFormulaNodes(network, invFormula, formulaNodes);
arrayForEachItem(Ntk_Node_t *, formulaNodes, i, node) {
PureSatGetFaninLatches(node, visited, vertexTable);
}
st_free_table(visited);
array_free(formulaNodes);
if (1) {
st_generator *stgen;
char *nodeNameString;
if(pm->verbosity>=1)
fprintf(vis_stdout, "\n Create_InitialAbstraction() =\n");
st_foreach_item(vertexTable, stgen, &nodeNameString, 0) {
if(pm->verbosity>=1)
fprintf(vis_stdout, "%s\n", nodeNameString);
(*Num)++;
}
if(pm->verbosity>=1){
fprintf(vis_stdout, "\n");
fflush(vis_stdout);
}
}
return vertexTable;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* PureSatGenerateRCArray_2 | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| array_t * | invisibleArray, | ||
| int * | NumInSecondLevel | ||
| ) |
Function********************************************************************
Synopsis [Generate latch candidate array based on BFS ring and RC information]
Description []
SideEffects []
SeeAlso []
Definition at line 1632 of file puresatUtil.c.
{
array_t * tmpRCArray = array_alloc(double,0);
array_t * tmpDfsArray = array_alloc(int,0);
array_t * arrayRC = array_alloc(char*,array_n(invisibleArray));
int i,j;
char * name;
if(pm->RefPredict)
pm->latchArray = array_alloc(char *,0);
PureSatComputeNumGatesInAbs(network,pm,invisibleArray);
for(i=0;i<array_n(invisibleArray);i++){
int nic,nia,dfs;
Ntk_Node_t *tmpnode;
int retVal;
name = array_fetch(char *,invisibleArray,i);
tmpnode = Ntk_NetworkFindNodeByName(network,name);
retVal = st_lookup(pm->node2dfsTable,name,&dfs);
assert(retVal);
array_insert_last(int,tmpDfsArray,dfs);
retVal = st_lookup(pm->nicTable,name,&nic);
assert(retVal);
retVal = st_lookup(pm->niaTable,name,&nia);
assert(retVal);
array_insert_last(double,tmpRCArray,
(double)nia/(double)nic);
}
DfsArray = tmpDfsArray;
RCArray = tmpRCArray;
*NumInSecondLevel = 0;
{
int tmpvalue;
double rcvalue;
int nn = array_n(invisibleArray);
int *tay=ALLOC(int,nn);
for(j=0;j<nn;j++)
tay[j]=j;
qsort((void *)tay, nn, sizeof(int),
(int (*)(const void *, const void *))NumInConeCompare_Ring);
for(i=0;i<nn;i++)
{
name = array_fetch(char *,invisibleArray,tay[i]);
array_insert(char *,arrayRC,i,name);
tmpvalue = array_fetch(int,tmpDfsArray,tay[i]);
if(tmpvalue == 2)
(*NumInSecondLevel)++;
rcvalue = array_fetch(double,tmpRCArray,tay[i]);
if(pm->verbosity>=1)
fprintf(vis_stdout,"arrayRC %s: %f-%f = %f\n",name,
(double)tmpvalue*1000000,rcvalue,(double)tmpvalue*1000000-rcvalue);
if(pm->RefPredict){
if(rcvalue>=0.87&&tmpvalue==2){
array_insert_last(char*,pm->latchArray,name);
if(pm->verbosity>=1)
fprintf(vis_stdout,"add %s into pm->latchArray\n",name);
}
}
}
FREE(tay);
}
array_free(DfsArray);
array_free(RCArray);
return arrayRC;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* PureSatGenerateRingFromAbs | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| array_t * | invisibleArray, | ||
| int * | NumInSecondLevel | ||
| ) |
Function********************************************************************
Synopsis [Generating the ring information needed for the computation of the relative correlation of a latch. For more information of Relative Correlation, please check the BMC'03 and STTT'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", and " Abstraction in symbolic model checking using satisfiability as the only decision procedure]
Description [Generating the ring information needed for the computation of the relative correlation of a latch. For more information of Relative Correlation, please check the BMC'03 and STTT'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", and " Abstraction in symbolic model checking using satisfiability as the only decision procedure"]
SideEffects []
SeeAlso []
Definition at line 925 of file puresatUtil.c.
{
st_table *CoiTable = pm->CoiTable;
st_table *supportTable = pm->supportTable;
st_table *AbsTable= pm->AbsTable;
array_t * arrayRC = array_alloc(char *,array_n(invisibleArray)),* NumInConeArray = array_alloc(int,0),* NumInAbsArray = array_alloc(int,0);
array_t * tmpNumInCone = array_alloc(int,0),* tmpNumInAbs = array_alloc(int,0);
array_t * tmpDfsArray = array_alloc(int,0), *tmpRCArray = array_alloc(double,0);
array_t * tmpDfsArray1 = array_alloc(int,0), *tmpRCArray1 = array_alloc(double,0);
int numincone,i,j,dfs;
char *name;
double d1;
(*NumInSecondLevel) = 0;
for(i=0;i<array_n(invisibleArray);i++)
{
int tmp;
Ntk_Node_t *tmpnode;
name = array_fetch(char *,invisibleArray,i);
tmpnode = Ntk_NetworkFindNodeByName(network,name);
tmp = PureSatComputeCorrelationforLatch(network,AbsTable,tmpnode);
tmp = tmp/10000;
if(!st_lookup_int(CoiTable,tmpnode,&dfs)){
fprintf(vis_stderr,"not in Coitable, Wrong");
exit(0);
}
if(!st_lookup_int(supportTable,tmpnode, &numincone)){
fprintf(vis_stderr,"not in supporttable, Wrong");
exit(0);
}
d1 = (double)tmp/(double)numincone;
array_insert_last(double,tmpRCArray,d1);
array_insert_last(int,tmpDfsArray,dfs);
}
DfsArray = tmpDfsArray;
RCArray = tmpRCArray;
{
int tmpvalue;
double dvalue;
int nn = array_n(invisibleArray);
int *tay=ALLOC(int,nn);
for(j=0;j<nn;j++)
tay[j]=j;
qsort((void *)tay, nn, sizeof(int),
(int (*)(const void *, const void *))NumInConeCompare_Ring);
for(i=0;i<nn;i++)
{
char *str=ALLOC(char,100);
name = array_fetch(char *,invisibleArray,tay[i]);
strcpy(str,name);
array_insert(char *,arrayRC,i,str);
tmpvalue = array_fetch(int,tmpDfsArray,tay[i]);
if(tmpvalue == 2)
(*NumInSecondLevel)++;
array_insert(int,tmpDfsArray1,i,tmpvalue);
dvalue = array_fetch(double,tmpRCArray,tay[i]);
array_insert(double,tmpRCArray1,i,dvalue);
if(pm->verbosity>=2){
int i1;
double d1,d2;
i1 = array_fetch(int,tmpDfsArray1,i)*1000000;
d1 = array_fetch(double,tmpRCArray1,i);
d2 = (double)array_fetch(int,tmpDfsArray1,i)*1000000 - d1;
if(pm->verbosity>=1)
fprintf(vis_stdout,"arrayRC %s: %d-%f = %f\n",name,i1,d1,d2);
/* fprintf(vis_stdout,"arrayRC %s: %d-%f = %f\n",name,array_fetch(int,tmpDfsArray1,i)*1000000,array_fetch(double,tmpRCArray1,i),
(double)array_fetch(int,tmpDfsArray1,i)*1000000-(double)array_fetch(double,tmpRCArray1,i));*/
}
}
FREE(tay);
}
array_free(NumInConeArray);
array_free(NumInAbsArray);
array_free(tmpNumInCone);
array_free(tmpNumInAbs);
array_free(tmpDfsArray);
array_free(tmpRCArray);
array_free(tmpDfsArray1);
array_free(tmpRCArray1);
return arrayRC;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatGenerateSupportTable | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm | ||
| ) |
Function********************************************************************
Synopsis [Build a support table,each value associated with a latch is the number of gates in its cone of influence ]
Description [Build a support table,each value associated with a latch is the number of gates in its cone of influence ]
SideEffects []
SeeAlso []
Definition at line 469 of file puresatUtil.c.
{
array_t *roots = array_alloc(Ntk_Node_t *,0); /*supports;*/
st_generator *stgen;
Ntk_Node_t *node,*DataNode=(Ntk_Node_t *)0;
int count, NumofSupports;
st_foreach_item_int(pm->CoiTable, stgen, &node, &count) {
if (Ntk_NodeTestIsLatch(node))
DataNode = Ntk_LatchReadDataInput(node);
array_insert(Ntk_Node_t *, roots, 0, DataNode);
NumofSupports = PureSatNodeComputeCombinationalSupport_AllNodes(network, roots,FALSE);
st_insert(pm->supportTable,node, (char *)(long)NumofSupports);
}
array_free(roots);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatGetCoiForVisibleArray_Ring | ( | Ntk_Network_t * | network, |
| array_t * | visibleArray, | ||
| int | position, | ||
| st_table * | ltlCoiTable | ||
| ) |
Function********************************************************************
Synopsis [Take latches in visibleArray as the first level compute the DFS level of each latch in ltlCoiTable]
Description [Take latches in visibleArray as the first level compute the DFS level of each latch in ltlCoiTable]
SideEffects []
SeeAlso []
Definition at line 731 of file puresatUtil.c.
{
int i;
char * name;
Ntk_Node_t * node;
st_table *visited = st_init_table(st_ptrcmp, st_ptrhash);
for(i=position;i<array_n(visibleArray);i++){
name = array_fetch(char *,visibleArray,i);
node = Ntk_NetworkFindNodeByName(network,name);
DfsLevel = 0;
PureSatBmcGetCoiForNtkNode(node,ltlCoiTable, visited);
}
st_free_table(visited);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatGetFaninLatches | ( | Ntk_Node_t * | node, |
| st_table * | visited, | ||
| st_table * | vertexTable | ||
| ) |
Function********************************************************************
Synopsis [Get direct fan in latches for a node]
Description [Get direct fan in latches for a node]
SideEffects []
SeeAlso []
Definition at line 564 of file puresatUtil.c.
{
if (st_is_member(visited, node))
return;
st_insert(visited, node, (char *)0);
if (Ntk_NodeTestIsLatch(node))
st_insert(vertexTable, Ntk_NodeReadName(node), (char *)0);
else {
int i;
Ntk_Node_t *fanin;
Ntk_NodeForEachFanin(node, i, fanin) {
PureSatGetFaninLatches(fanin, visited, vertexTable);
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatGetFormulaNodes | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | F, | ||
| array_t * | formulaNodes | ||
| ) |
Function********************************************************************
Synopsis []
Description [recursively compute the nodes in a ltl formula and put them in an array]
SideEffects []
SeeAlso []
Definition at line 528 of file puresatUtil.c.
{
if (F == NIL(Ctlsp_Formula_t))
return;
if (Ctlsp_FormulaReadType(F) == Ctlsp_ID_c) {
char *nodeNameString = Ctlsp_FormulaReadVariableName(F);
Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);
assert(node);
array_insert_last(Ntk_Node_t *, formulaNodes, node);
return;
}
PureSatGetFormulaNodes(network, Ctlsp_FormulaReadRightChild(F), formulaNodes);
PureSatGetFormulaNodes(network, Ctlsp_FormulaReadLeftChild(F), formulaNodes);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* PureSatGetImmediateSupportLatches | ( | Ntk_Network_t * | network, |
| int | beginPosition, | ||
| array_t * | latchNameArray | ||
| ) |
Function********************************************************************
Synopsis [Get immediate latch supports for latches in latchNameArray]
Description [Get immediate latch supports for latches in latchNameArray]
SideEffects []
SeeAlso []
Definition at line 1191 of file puresatUtil.c.
{
/* old support, form 0 to 'beginPosition'-1*/
array_t *dataInputs, *supports;
/* new support, from 'beginPosition' to array_n(latchNameArray)-1*/
array_t *dataInputs2, *supports2, *supportLatches2;
/* The result should be {new support}-{old support}*/
st_table *oldSupportTable;
Ntk_Node_t *latch, *dataInput;
int i;
char *latchName;
dataInputs = array_alloc(Ntk_Node_t *, 0);
dataInputs2 = array_alloc(Ntk_Node_t *, 0);
arrayForEachItem(char *, latchNameArray, i, latchName) {
latch = Ntk_NetworkFindNodeByName(network, latchName);
assert(latch);
assert(Ntk_NodeTestIsLatch(latch));
dataInput = Ntk_LatchReadDataInput(latch);
if (i < beginPosition)
array_insert_last(Ntk_Node_t *, dataInputs, dataInput);
else
array_insert_last(Ntk_Node_t *, dataInputs2, dataInput);
}
supports = Ntk_NodeComputeCombinationalSupport(network, dataInputs, 1);
supports2 = Ntk_NodeComputeCombinationalSupport(network, dataInputs2, 1);
array_free(dataInputs);
array_free(dataInputs2);
oldSupportTable = st_init_table(st_ptrcmp, st_ptrhash);
arrayForEachItem(Ntk_Node_t *, supports, i, latch) {
st_insert(oldSupportTable, latch, NIL(char));
}
array_free(supports);
supportLatches2 = array_alloc(char *, 0);
arrayForEachItem(Ntk_Node_t *, supports2, i, latch) {
if (Ntk_NodeTestIsLatch(latch) &&
!st_is_member(oldSupportTable,latch))
array_insert_last(char *, supportLatches2, Ntk_NodeReadName(latch));
}
array_free(supports2);
arrayForEachItem(char *, latchNameArray, i, latchName) {
if (i < beginPosition) continue;
latch = Ntk_NetworkFindNodeByName(network, latchName);
if (!st_is_member(oldSupportTable, latch))
array_insert_last(char *, supportLatches2, latchName);
}
st_free_table(oldSupportTable);
return supportLatches2;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* PureSatGetLatchFromTable | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| char * | coreFile | ||
| ) |
Function********************************************************************
Synopsis [Generate refinement latches from UNSAT proof]
Description [Generate refinement latches from UNSAT proof]
SideEffects []
SeeAlso []
Definition at line 1387 of file puresatUtil.c.
{
FILE *fp;
char buffer[1024],*nodeName;
int idx;
st_table * localTable = st_init_table(strcmp,st_strhash);
array_t * refinement = array_alloc(char *,0);
st_table *ClsidxToLatchTable = pm->ClsidxToLatchTable;
st_table *vertexTable = pm->vertexTable;
fp = fopen(coreFile,"r");
while(fgets(buffer,1024,fp)){
if(strncmp(buffer,"#clause index:",14)==0){
sscanf(buffer,"#clause index:%d\n",&idx);
if(st_lookup(ClsidxToLatchTable,(char *)(long)idx,&nodeName))
if(!st_lookup(vertexTable,nodeName,NIL(char *))&&!st_lookup(localTable,nodeName,NIL(char *)))
{
st_insert(localTable,nodeName,(char *)0);
array_insert_last(char *,refinement,nodeName);
}
}
}
st_free_table(localTable);
return refinement;
}
Here is the caller graph for this function:
| PureSat_IncreSATManager_t* PureSatIncreSATManagerAlloc | ( | PureSat_Manager_t * | pm | ) |
Function********************************************************************
Synopsis [Allocate a puresat incremental SAT manager]
Description [Allocate a puresat incremental SAT manager]
SideEffects []
SeeAlso []
Definition at line 184 of file puresatUtil.c.
{
PureSat_IncreSATManager_t * pism = ALLOC(PureSat_IncreSATManager_t,1);
pism->beginPosition = 0;
pism->Length = 0;
pism->oldLength = 0;
pism->propertyPos = 0;
memset(pism,0,sizeof(PureSat_IncreSATManager_t));
if(pm->sss){
pism->cnfClauses = BmcCnfClausesAlloc();
pism->cm = sat_InitManager(0);
pism->cm->comment = ALLOC(char, 2);
pism->cm->comment[0] = ' ';
pism->cm->comment[1] = '\0';
pism->cm->maxNodesArraySize = 1;
pism->cm->nodesArray = ALLOC(long, pism->cm->maxNodesArraySize );
pism->cm->nodesArraySize = satNodeSize;
pism->cm->stdErr = vis_stderr;
pism->cm->stdOut = vis_stdout;
pism->cm->unitLits = sat_ArrayAlloc(16);
pism->cm->pureLits = sat_ArrayAlloc(16);
pism->cm->each = sat_InitStatistics();
pism->cm->option = sat_InitOption();
pism->cm->option->ForceFinish = 1;
pism->cm->option->incTraceObjective = 1;
pism->cm->option->includeLevelZeroLiteral = 1;
pism->cm->option->minimizeConflictClause = 0;
pism->cm->option->SSS = 1;
}
return pism;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatIncreSATManagerFree | ( | PureSat_Manager_t * | pm, |
| PureSat_IncreSATManager_t * | pism | ||
| ) |
Function********************************************************************
Synopsis [Free a puresat incremental SAT manager]
Description [Free a puresat incremental SAT manager]
SideEffects []
SeeAlso []
Definition at line 230 of file puresatUtil.c.
{
if(pm->sss){
BmcCnfClausesFree(pism->cnfClauses);
FREE(pism->cm->nodesArray);
sat_ArrayFree(pism->cm->unitLits);
sat_ArrayFree(pism->cm->pureLits);
sat_FreeStatistics(pism->cm->each);
sat_FreeOption(pism->cm->option);
FREE(pism->cm);
}
FREE(pism);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| PureSat_Manager_t* PureSatManagerAlloc | ( | void | ) |
Function********************************************************************
Synopsis [Allocate a puresat manager]
Description [Allocate a puresat manager]
SideEffects []
SeeAlso []
Definition at line 123 of file puresatUtil.c.
{
PureSat_Manager_t * pm = ALLOC(PureSat_Manager_t,1);
memset(pm,0,sizeof(PureSat_Manager_t));
pm->incre = TRUE;
pm->ltlFileName = ALLOC(char,200);
pm->timeOutPeriod = 10000000;
pm->Arosat = TRUE;;
pm->CoreRefMin = TRUE;
pm->RefPredict = TRUE;
pm->Switch = TRUE;
return pm;
}
Here is the caller graph for this function:
| void PureSatManagerFree | ( | PureSat_Manager_t * | pm | ) |
Function********************************************************************
Synopsis [Free a puresat manager]
Description [Free a puresat manager]
SideEffects []
SeeAlso []
Definition at line 149 of file puresatUtil.c.
{
if(pm->latchToTableBaigNodes)
st_free_table(pm->latchToTableBaigNodes);
if(pm->ClsidxToLatchTable)
st_free_table(pm->ClsidxToLatchTable);
if(pm->CoiTable)
st_free_table(pm->CoiTable);
if(pm->AbsTable)
st_free_table(pm->AbsTable);
if(pm->vertexTable)
st_free_table(pm->vertexTable);
if(pm->SufAbsTable)
st_free_table(pm->SufAbsTable);;
if(pm->supportTable)
st_free_table(pm->supportTable);
if(pm->node2dfsTable)
st_free_table(pm->node2dfsTable);
if(pm->result!=NIL(array_t))
array_free(pm->result);
FREE(pm->ltlFileName);
FREE(pm);
}
Here is the caller graph for this function:
| int PureSatNodeComputeCombinationalSupport_AllNodes | ( | Ntk_Network_t * | network, |
| array_t * | nodeArray, | ||
| boolean | stopAtLatches | ||
| ) |
Function********************************************************************
Synopsis [Get the number of combination support of a node]
Description [Get the number of combination support of a node]
SideEffects []
SeeAlso []
Definition at line 432 of file puresatUtil.c.
{
lsGen gen;
int i, NumofSupports=0;
Ntk_Node_t *node;
Ntk_NetworkForEachNode( network, gen, node ) {
PureSatNodeSetColor( node, dfsWhite_c );
}
/* for each lacthes(node) in the nodeArray, compute the number of gates in
the cone of this latch, put the number in NumofSupports*/
arrayForEachItem( Ntk_Node_t *, nodeArray, i, node ) {
NumofSupports = 0;
PureSatNodeRecursivelyComputeTransitiveFaninNodes_AllNodes( node, &NumofSupports, stopAtLatches );
}
return NumofSupports;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| DfsColor PureSatNodeReadColor | ( | Ntk_Node_t * | node | ) |
Function********************************************************************
Synopsis [Get the color of a node]
Description [Get the color of a node]
SideEffects []
SeeAlso []
Definition at line 353 of file puresatUtil.c.
{
return ((DfsColor) (long) Ntk_NodeReadUndef(node));
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatNodeRecursivelyComputeTransitiveFaninNodes_AllNodes | ( | Ntk_Node_t * | node, |
| int * | NumofSupports, | ||
| boolean | stopAtLatches | ||
| ) |
Function********************************************************************
Synopsis [Recursively compute the transitive fan in nodes of a node]
Description [Recursively compute the transitive fan in nodes of a node]
SideEffects []
SeeAlso []
Definition at line 390 of file puresatUtil.c.
{
int i;
Ntk_Node_t * fanin;
/* test if we have already started processing this node */
if ( PureSatNodeReadColor( node ) == dfsBlack_c ) {
return;
}
PureSatNodeSetColor( node, dfsBlack_c );
/* if ( Ntk_NodeTestIsCombInput( node ) ) {
st_insert( resultTable, (char *) node, (char *) 0 );
}*/
(*NumofSupports)++;
if ( Ntk_NodeTestIsInput(node) || ((stopAtLatches == TRUE)&&(Ntk_NodeTestIsLatch(node))) ) {
return;
}
Ntk_NodeForEachFanin( node, i, fanin ) {
PureSatNodeRecursivelyComputeTransitiveFaninNodes_AllNodes( fanin, NumofSupports, stopAtLatches );
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatNodeSetColor | ( | Ntk_Node_t * | node, |
| DfsColor | color | ||
| ) |
Function********************************************************************
Synopsis [Set the color of a node]
Description [Set the color of a node]
SideEffects []
SeeAlso []
Definition at line 371 of file puresatUtil.c.
{
Ntk_NodeSetUndef(node, (void *) (long) color);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatReadClauses | ( | PureSat_IncreSATManager_t * | pism, |
| PureSat_Manager_t * | pm | ||
| ) |
Function********************************************************************
Synopsis [Read clauses from a puresat incremental SAT manager to the CirCUs SAT solver]
Description [Read clauses from a puresat incremental SAT manager to the CirCUs SAT solver]
SideEffects []
SeeAlso []
Definition at line 1106 of file puresatUtil.c.
{
int i,node,nVar = pism->cnfClauses->cnfGlobalIndex - 1;
satManager_t * cm = pism->cm;
satArray_t * clauseArray;
cm->option->verbose = pm->verbosity;
cm->initNumVariables = nVar;
cm->variableArray = ALLOC(satVariable_t, cm->initNumVariables+1);
memset(cm->variableArray, 0, sizeof(satVariable_t) *
(cm->initNumVariables+1));
if(cm->maxNodesArraySize <= (cm->initNumVariables+2)*satNodeSize){
cm->nodesArray = ALLOC(long, (cm->initNumVariables+2)*satNodeSize);
cm->maxNodesArraySize = (cm->initNumVariables+2)*satNodeSize;
}
if(pism->cm->option->coreGeneration){
pism->cm->dependenceTable = st_init_table(st_ptrcmp, st_ptrhash);
/*the tables stroes entry of (var_node_idx,cls_idx);*/
pism->cm->anteTable = st_init_table(st_numcmp, st_numhash);
}
sat_AllocLiteralsDB(cm);
for(i=1;i<=nVar;i++){
node = sat_CreateNode(cm,2,2);
SATflags(node) |= CoiMask;
SATvalue(node) = 2;
/*SATfanout(node) = 0;*/
cm->nodesArray[node+satFanout] = 0;
SATnFanout(node) = 0;
}
clauseArray = sat_ArrayAlloc(4096);
for(i=0; i<pism->cnfClauses->nextIndex;i++){
int k, cls_idx,v;
k = array_fetch(int,pism->cnfClauses->clauseArray,i);
if(k!=0){
int sign = 1;
if(k<0){
sign = 0;
k = -k;
}
v = k*satNodeSize + sign;
sat_ArrayInsert(clauseArray, v);
}
else{
if(clauseArray->num == 1) {
v = clauseArray->space[0];
sat_ArrayInsert(cm->unitLits, SATnot(v));
cls_idx = sat_AddUnitClause(cm, clauseArray);
if(pism->cm->option->coreGeneration){
v = SATnormalNode(v);
st_insert(pism->cm->anteTable,(char *)(long)v,(char *)(long)cls_idx);
}
}
else{
cls_idx = sat_AddClause(cm, clauseArray);
}
cm->initNumClauses++;
cm->initNumLiterals += clauseArray->num;
if(i>pism->propertyPos)
SATflags(cls_idx) |= ObjMask;
clauseArray->num = 0;
}
}
sat_ArrayFree(clauseArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatRecursivelyComputeCorrelationforLatch | ( | Ntk_Network_t * | network, |
| st_table * | AbsTable, | ||
| st_table * | visited, | ||
| Ntk_Node_t * | node, | ||
| int * | count | ||
| ) |
Function********************************************************************
Synopsis [Recursively compute the relative correlation of a latch. For more information of Relative Correlation, please check the BMC'03 and STTT'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", and " Abstraction in symbolic model checking using satisfiability as the only decision procedure"]
Description [Recursively compute the relative correlation of a latch. For more information of Relative Correlation, please check the BMC'03 and STTT'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", and " Abstraction in symbolic model checking using satisfiability as the only decision procedure"]
SideEffects []
SeeAlso []
Definition at line 841 of file puresatUtil.c.
{
Ntk_Node_t * fanin;
int i;
if(!st_lookup(visited,node,NIL(char *)))
{
st_insert(visited,node,(char *)0);
if(st_lookup(AbsTable,node,NIL(char *)))
{
(*count)++;
}
}
else
return;
if(Ntk_NodeTestIsCombInput(node))
return;
Ntk_NodeForEachFanin(node,i,fanin)
PureSatRecursivelyComputeCorrelationforLatch(network,AbsTable,visited,fanin,count);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatRecursivelyComputeTableForLatch | ( | Ntk_Network_t * | network, |
| st_table * | Table, | ||
| Ntk_Node_t * | node | ||
| ) |
Function********************************************************************
Synopsis [Recursively get direct fan in gates of a node]
Description [Recursively get direct fan in gates of a node]
SideEffects []
SeeAlso []
Definition at line 655 of file puresatUtil.c.
{
int i;
Ntk_Node_t * fanin;
//want input to be in the Table
if(Ntk_NodeTestIsLatch(node))
return;
if(!st_lookup(Table,node,NIL(char *)))
st_insert(Table,node, (char *)0);
else
return;
if ( Ntk_NodeTestIsCombInput(node)) {
return;
}
Ntk_NodeForEachFanin( node,i,fanin)
PureSatRecursivelyComputeTableForLatch(network,Table,fanin);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* PureSatRemove_char | ( | array_t * | array1, |
| int | i | ||
| ) |
Function********************************************************************
Synopsis [remove the ith member of a certain array]
Description [remove the ith member of a certain array]
SideEffects []
SeeAlso []
Definition at line 1430 of file puresatUtil.c.
{
int j;
char * str;
array_t * array2=array_alloc(char *,0);
assert(i<array_n(array1));
arrayForEachItem(char *,array1,j,str)
{
if(j!=i)
{
array_insert_last(char *,array2,str);
}
}
return array2;
}
Here is the caller graph for this function:
| void PureSatWriteAllClausesToFile | ( | PureSat_IncreSATManager_t * | pism, |
| char * | coreFile | ||
| ) |
Function********************************************************************
Synopsis [Dump out all the clauses, including conflict clauses, to a file]
Description [Dump out all the clauses, including conflict clauses, to a file]
SideEffects []
SeeAlso []
Definition at line 1310 of file puresatUtil.c.
{
satManager_t *cm = pism->cm;
char *tmpallcnfFile = BmcCreateTmpFile();
FILE *fp1 = fopen(coreFile,"r");
FILE *fp2 = fopen(tmpallcnfFile,"w");
char buffer[1024], buffer1[1024];
long *space;
int i, numOfConCls=0, numOfVar, sign,var;
satArray_t *saved = cm->savedConflictClauses;
for(i=0, space=saved->space; i<saved->num; i++,space++){
if(*space<0)
numOfConCls++;
}
if(numOfConCls%2!=0){
fprintf(vis_stdout,"should be times of 2\n");
exit(0);
}
numOfConCls/=2;
numOfConCls += cm->initNumClauses;
numOfVar = cm->initNumVariables;
i=0;
/*sprintf(buffer,"p cnf %d %d 0\n", numOfConCls, numOfVar);
fputs(buffer, fp2);*/
while(fgets(buffer,1024,fp1)){
if(strncmp(buffer,"c ",2)!=0){
if(strncmp(buffer,"p cnf ",6)==0){
sprintf(buffer1,"p cnf %d %d 0\n", numOfVar, numOfConCls);
fputs(buffer1, fp2);
}
else
fputs(buffer, fp2);
}
}
saved = cm->savedConflictClauses;
for(i=0, space=saved->space; i<saved->num; i++){
if(*space<0){
space++;
i++;
while(*space>0){
sign = !SATisInverted(*space);
var = SATnormalNode(*space);
if(sign == 0)
var = -var;
fprintf(fp2,"%d ",var);
space++;
i++;
}
fprintf(fp2,"0\n");
space++;
i++;
}
}
fclose(fp1);
fclose(fp2);
FREE(tmpallcnfFile);
}
Here is the call graph for this function:
| void PureSatWriteClausesToFile | ( | PureSat_IncreSATManager_t * | pism, |
| mAig_Manager_t * | maigManager, | ||
| char * | coreFile | ||
| ) |
Function********************************************************************
Synopsis [Dump out clauses to a file]
Description [Dump out clauses to a file]
SideEffects []
SeeAlso []
Definition at line 1261 of file puresatUtil.c.
{
BmcCnfClauses_t *cnfClauses = pism->cnfClauses;
st_generator *stGen;
char *name;
int cnfIndex, i, k;
FILE *cnfFile;
coreFile = BmcCreateTmpFile();
cnfFile = fopen(coreFile,"w");
fprintf(vis_stdout, "coreFile is %s\n", coreFile);
fprintf(vis_stdout,
"Number of Variables = %d Number of Clauses = %d\n",
cnfClauses->cnfGlobalIndex-1, cnfClauses->noOfClauses);
st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, &name, &cnfIndex) {
fprintf(cnfFile, "c %s %d\n",name, cnfIndex);
}
(void) fprintf(cnfFile, "p cnf %d %d\n", cnfClauses->cnfGlobalIndex-1,
cnfClauses->noOfClauses);
if (cnfClauses->clauseArray != NIL(array_t)) {
for (i = 0; i < cnfClauses->nextIndex; i++) {
k = array_fetch(int, cnfClauses->clauseArray, i);
(void) fprintf(cnfFile, "%d%c", k, (k == 0) ? '\n' : ' ');
}
}
fclose(cnfFile);
FREE(coreFile);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
array_t* DfsArray [static] |
Definition at line 107 of file puresatUtil.c.
int DfsLevel = 0 [static] |
AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [time out function]
Description [time out function]
SideEffects []
SeeAlso []
Definition at line 104 of file puresatUtil.c.
array_t* NumInAbs [static] |
Definition at line 106 of file puresatUtil.c.
array_t* NumInCone [static] |
Definition at line 105 of file puresatUtil.c.
array_t* RCArray [static] |
CFile***********************************************************************
FileName [puresatUtil.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.]
Definition at line 67 of file puresatUtil.c.
