VIS

src/puresat/puresatIPUtil.c File Reference

#include "puresatInt.h"
Include dependency graph for puresatIPUtil.c:

Go to the source code of this file.

Functions

static int NodeIndexCompare (const void *x, const void *y)
static int StringCheckIsInteger (char *string, int *value)
RTnode_t RTCreateNode (RTManager_t *rm)
IP_Manager_t * IPManagerAlloc ()
void IPManagerFree (IP_Manager_t *ipm)
int PureSat_IdentifyConflict (satManager_t *cm, long left, bAigEdge_t right, bAigEdge_t node)
void PureSatBmcGetCoiForNtkNode_New (Ntk_Node_t *node, st_table *CoiTable, st_table *visited)
void PureSatBmcGetCoiForLtlFormulaRecursive_New (Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable, st_table *visited)
void PureSatBmcGetCoiForLtlFormula_New (Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable)
void PureSat_MarkTransitiveFaninForNode (satManager_t *cm, bAigEdge_t v, unsigned int mask)
void PureSat_MarkTransitiveFaninForArray (satManager_t *cm, satArray_t *arr, unsigned int mask)
void PureSat_MarkTransitiveFaninForNode2 (mAig_Manager_t *manager, bAigEdge_t v, unsigned int mask)
void PureSat_MarkTransitiveFaninForArray2 (mAig_Manager_t *manager, satArray_t *arr, unsigned int mask)
void PureSat_MarkTransitiveFaninForNode3 (mAig_Manager_t *manager, bAigEdge_t v, unsigned int mask)
void PureSat_MarkTransitiveFaninForArray3 (mAig_Manager_t *manager, satArray_t *arr, unsigned int mask)
void PureSat_MarkTransitiveFaninForNode4 (mAig_Manager_t *manager, bAigEdge_t v, unsigned int mask, int bound)
void PureSat_MarkTransitiveFaninForArray4 (mAig_Manager_t *manager, satArray_t *arr, unsigned int mask, int bound)
void PureSat_CleanMask (mAig_Manager_t *manager, unsigned int mask)
void PureSat_SetCOI (satManager_t *cm)
void PureSat_ResetCoi (satManager_t *cm)
void PureSatSetLatchCOI (Ntk_Network_t *network, PureSat_Manager_t *pm, satManager_t *cm, st_table *AbsTable, int from, int to)
void PureSatSetLatchCOI2 (Ntk_Network_t *network, PureSat_Manager_t *pm, satManager_t *cm, bAigEdge_t obj, int bound)
void PureSatSetCOI (Ntk_Network_t *network, PureSat_Manager_t *pm, satManager_t *cm, st_table *AbsTable, int from, int to, int bound)
void PureSatAbstractLatch (bAig_Manager_t *manager, bAigEdge_t v, st_table *tmpTable)
void PureSatKillPseudoGVNode (bAig_Manager_t *manager, bAigEdge_t v, st_table *tmpTable)
void PureSatKillPseudoGV (Ntk_Network_t *network, PureSat_Manager_t *pm, st_table *AbsTable, int from, int to)
int PureSat_CountNodesInCoi (satManager_t *cm)
void PureSat_Check (bAig_Manager_t *manager, bAigEdge_t v)
void PureSat_CheckFanoutFanin (bAig_Manager_t *manager)
void PureSat_ResetManager (mAig_Manager_t *manager, satManager_t *cm, int clean)
void PureSat_RestoreAigForDummyNode (mAig_Manager_t *manager, int oldPosition)
void PureSatProcessFanout (satManager_t *cm)
long PureSatRecoverFanoutNode (satManager_t *cm, bAigEdge_t v)
void PureSatRecoverISVNode (satManager_t *cm, bAigEdge_t v)
void PureSatRecoverFanout (satManager_t *cm, PureSat_Manager_t *pm)
void PureSatCheckCoiNode (bAig_Manager_t *manager, bAigEdge_t node)
void PureSatCheckCoi (bAig_Manager_t *manager)
void PureSatPreprocess (Ntk_Network_t *network, satManager_t *cm, PureSat_Manager_t *pm, st_table *vertexTable, int Length)
void PureSatPostprocess (bAig_Manager_t *manager, satManager_t *cm, PureSat_Manager_t *pm)
int PureSat_TestConvergeForIP (mAig_Manager_t *manager, PureSat_Manager_t *pm, satManager_t *cm, bAigEdge_t state1, bAigEdge_t state2)
int PureSat_TestConvergeForIP_AbRf (Ntk_Network_t *network, satManager_t *cm, PureSat_Manager_t *pm, array_t *CoiArray, bAigEdge_t state1, bAigEdge_t state2)
satManager_t * PureSat_SatManagerAlloc (bAig_Manager_t *manager, PureSat_Manager_t *pm, bAigEdge_t object, array_t *auxObjectArray)
satManager_t * PureSat_SatManagerAlloc_WOCOI (mAig_Manager_t *manager, PureSat_Manager_t *pm, bAigEdge_t object, array_t *auxObjectArray)
void PureSat_SatFreeManager (satManager_t *cm)
void PureSat_PrintAigStatus (mAig_Manager_t *manager)
void PureSat_MarkGlobalVar (bAig_Manager_t *manager, int length)
void PureSat_UnMarkGlobalVar (bAig_Manager_t *manager, int length)
void PureSat_MarkGlobalVar_AbRf (bAig_Manager_t *manager, int length)
void PuresatMarkVisibleVarWithVPGV (Ntk_Network_t *network, array_t *visibleArray, PureSat_Manager_t *pm, int from, int to)
void PuresatMarkVisibleVar (Ntk_Network_t *network, array_t *visibleArray, PureSat_Manager_t *pm, int from, int to)
bAigEdge_t PureSat_MapIPRecur (mAig_Manager_t *manager, bAigEdge_t node, st_table *tmpTable)
bAigEdge_t PureSat_MapIP (mAig_Manager_t *manager, bAigEdge_t node, int from, int to)
void PureSatProcessDummy (bAig_Manager_t *manager, satManager_t *cm, RTnode_t RTnode)
bAigEdge_t PureSat_FindNodeByName (bAig_Manager_t *manager, nameType_t *name, int bound)
bAigEdge_t PureSatCreatebAigOfPropFormula (Ntk_Network_t *network, bAig_Manager_t *manager, int bound, Ctlsp_Formula_t *ltl, int withInitialState)
void PureSatMarkObj (bAig_Manager_t *manager, long from, long to)
boolean PureSat_ConcretTest (Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *sufArray, bAigEdge_t property, array_t *previousResultArray, int Con, int satStat, int inc)
boolean PureSat_ConcretTest_Core (Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *sufArray, bAigEdge_t property, array_t *previousResultArray, st_table *junkTable)
void PureSatGenerateRingForNode (Ntk_Network_t *network, PureSat_Manager_t *pm, Ntk_Node_t *node1, array_t *ringArray, int *dfs)
array_t * PureSatGenerateRing (Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *coreArray, int *dfs)
void PureSatGenerateDfs (Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *vertexArray)
array_t * PureSatComputeOrder_2 (Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *vertexArray, array_t *invisibleArray, int *sccArray, int *NumInSecondLevel)
void PureSatAddIdenLatchToAbs (Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *nameArray)
void PureSatCreateInitAbsByAIG (bAig_Manager_t *manager, PureSat_Manager_t *pm, bAigEdge_t node, st_table *tmpTable)
void PureSat_GetLatchForNode (bAig_Manager_t *manager, PureSat_Manager_t *pm, bAigEdge_t node, array_t *nameArray, st_table *tmpTable, int cut)
st_table * PureSatGetAigCoi (Ntk_Network_t *network, PureSat_Manager_t *pm, bAigEdge_t property)
void PureSatPreProcLatch (Ntk_Network_t *network, PureSat_Manager_t *pm)
void PureSatGetIndenticalLatch (Ntk_Network_t *network, PureSat_Manager_t *pm)

Function Documentation

IP_Manager_t* IPManagerAlloc ( )

Function********************************************************************

Synopsis [Allocate an interpolation manager]

Description [Allocate an interpolation manager]

SideEffects []

SeeAlso []

Definition at line 227 of file puresatIPUtil.c.

{
  IP_Manager_t * ipm = ALLOC(IP_Manager_t, 1);
  memset(ipm,0,sizeof(IP_Manager_t));
  return ipm;
}

Here is the caller graph for this function:

void IPManagerFree ( IP_Manager_t *  ipm)

Function********************************************************************

Synopsis [Free an interpolation manager]

Description [Free an interpolation manager]

SideEffects []

SeeAlso []

Definition at line 248 of file puresatIPUtil.c.

{
  FREE(ipm);
}
static int NodeIndexCompare ( const void *  x,
const void *  y 
) [static]

CFile***********************************************************************

FileName [puresatIPUtil.c]

PackageName [puresat]

Synopsis [Abstraction refinement for large scale invariant checking.]

Description [This file contains the functions to check invariant properties by the PureSAT abstraction refinement algorithm, which is entirely based on SAT solver, the input of which could be either CNF or AIG. It has several parts:

Localization-reduction base Abstraction K-induction or interpolation to prove the truth of a property Bounded Model Checking to find bugs Incremental concretization based methods to verify abstract bugs Incremental SAT solver to improve efficiency UNSAT proof based method to obtain refinement AROSAT to bring in only necessary latches into unsat proofs Bridge abstraction to get compact coarse refinement Refinement minization to guarrantee minimal refinements Unsat proof-based refinement minimization to eliminate multiple candidate by on SAT test Refinement prediction to decrease the number of refinement iterations Dynamic switching to redistribute computional resources to improve efficiency

For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", " Abstraction in symbolic model checking using satisfiability as the only decision procedure", "Efficient computation of small abstraction refinements", and "Efficient abstraction refinement in interpolation-based unbounded model checking"]

Author [Bing Li]

Copyright [Copyright (c) 2004 The Regents of the Univ. of Colorado. All rights reserved.

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.]AutomaticStart AutomaticEnd Function********************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []Function********************************************************************

Synopsis [Comparison function for sorting]

Description [Comparison function for sorting]

SideEffects []

SeeAlso []

Definition at line 116 of file puresatIPUtil.c.

{
int n1, n2;

  n1 = *(int *)x;
  n2 = *(int *)y;
  return(n1 > n2);
}

Here is the caller graph for this function:

void PureSat_Check ( bAig_Manager_t *  manager,
bAigEdge_t  v 
)

Function********************************************************************

Synopsis [Sanity check for one node for abstraction processsing]

Description [Sanity check for one node for abstraction processsing]

SideEffects []

SeeAlso []

Definition at line 1128 of file puresatIPUtil.c.

{
  bAigEdge_t *fan,*fan1,nfan1;
  bAigEdge_t nfan,cur,child,tmpchild,v1,other,cur1;
  int size,i,j,find=0,inver,left,left1;

  nfan = nFanout(v);
  fan = (bAigEdge_t *)fanout(v);
  if(fan == 0){
    assert(nfan==0);
    return;
  }

  size = 0;

  for(i=0; fan[i]!=0; i++){
    size++;
    cur = fan[i];
    left = 1;
    inver = 0;
    if(SATisInverted(cur))
      left = 0;
    cur >>= 1;
    if(SATisInverted(cur))
      inver = 1;
    cur = SATnormalNode(cur);
    child = inver? SATnormalNode(v)+1:SATnormalNode(v);
    if(left)
      tmpchild = leftChild(cur);
    else
      tmpchild = rightChild(cur);
    assert(tmpchild == child);

    /*check the other child*/
    find = 0;
    other = left?rightChild(cur):leftChild(cur);
    assert(other!=bAig_NULL);
    v1 = SATnormalNode(other);
    nfan1 = nFanout(v1);
    fan1 = (bAigEdge_t *)fanout(v1);
    assert(nfan1!=0&&fan1!=0);
    for(j=0; fan1[j]!=0; j++){
      cur1 = fan1[j];
      left1 = 1;
      if(SATisInverted(cur1))
        left1 = 0;
      assert(j<nfan1);
      if((SATnormalNode(cur1>>1)==cur)&&(left1!=left)){
        find = 1;

        break;
      }
    }
    assert(find);
  }

  assert(nfan==size);
}

Here is the caller graph for this function:

void PureSat_CheckFanoutFanin ( bAig_Manager_t *  manager)

Function********************************************************************

Synopsis [Sanity check for abstraction processsing]

Description [Sanity check for abstraction processsing]

SideEffects []

SeeAlso []

Definition at line 1201 of file puresatIPUtil.c.

{
  bAigEdge_t  i,v;

  for(i=bAigNodeSize;i<manager->nodesArraySize;i+=bAigNodeSize){
    v = i;
    if((flags(v) & IsCNFMask))
      continue;
    PureSat_Check(manager,v);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSat_CleanMask ( mAig_Manager_t *  manager,
unsigned int  mask 
)

Function********************************************************************

Synopsis [clean a certain mask for all the aig nodes]

Description [clean a certain mask for all the aig nodes]

SideEffects []

SeeAlso []

Definition at line 688 of file puresatIPUtil.c.

{
  bAigEdge_t i;

  for(i=bAigNodeSize; i<manager->nodesArraySize;i+=bAigNodeSize)
    flags(i)&=mask;

}

Here is the caller graph for this function:

boolean PureSat_ConcretTest ( Ntk_Network_t *  network,
PureSat_Manager_t *  pm,
array_t *  sufArray,
bAigEdge_t  property,
array_t *  previousResultArray,
int  Con,
int  satStat,
int  inc 
)

Function********************************************************************

Synopsis [procedure of concretization]

Description []

SideEffects []

SeeAlso []

Definition at line 3027 of file puresatIPUtil.c.

{
  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  int status,i,nodes_in_coi=0;
  satManager_t *cm;
  char *name;
  double t1,t2;
  satArray_t *saved;
  st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash);
  bAigEdge_t from,*lp;

   arrayForEachItem(char *,sufArray,i,name){
    st_insert(SufAbsNameTable,name,(char*)0);
   }

   manager->assertArray = sat_ArrayAlloc(1);
  sat_ArrayInsert(manager->assertArray,manager->InitState);
  cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);

  cm->option->coreGeneration = 0;
  cm->option->RT = 0;
  cm->option->AbRf = 1;
  if(inc){
    cm->option->incTraceObjective = 1;
    cm->savedConflictClauses = pm->savedConCls;
    pm->savedConCls = 0;
  }
  t1 = util_cpu_ctime();
  PureSat_CleanMask(manager,ResetVisibleVarMask);
  PuresatMarkVisibleVar(network,sufArray,pm,0,pm->Length+1);
  if(!Con){
    from = manager->nodesArraySize;
    PureSatSetCOI(network,pm,cm,SufAbsNameTable,0,pm->Length,pm->Length);
    PureSatKillPseudoGV(network,pm,SufAbsNameTable,1,pm->Length);
    if(inc){
      PureSatMarkObj(manager,from,manager->nodesArraySize-bAigNodeSize);
    }
    PureSat_ResetManager(manager,cm,0);
    PureSatProcessFanout(cm);
  }
  else{
    sat_MarkTransitiveFaninForNode(cm,property,CoiMask);
    sat_MarkTransitiveFaninForNode(cm,manager->InitState,CoiMask);
    cm->option->AbRf = 0;
  }
  t2 = util_cpu_ctime();
  pm->tPro += t2-t1;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"process time:%g,total:%g\n",
           (double)((t2-t1)/1000.0),pm->tPro/1000);
  if(pm->verbosity>=1){
    nodes_in_coi = PureSat_CountNodesInCoi(cm);
    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
  }
  st_free_table(SufAbsNameTable);
  manager->assertArray2 = cm->assertArray2;
  sat_Main(cm);
  if(satStat)
    sat_ReportStatistics(cm,cm->each);
  cm->option->AbRf = 1;
  manager->NodesArray = cm->nodesArray;
  t1 = util_cpu_ctime();
  if(!Con){
    PureSatRecoverFanout(cm,pm);
    PureSat_RestoreAigForDummyNode(manager,pm->oldPos);
    PureSat_CleanMask(manager,ResetVisited3Mask);
  }
  /*record conflict*/
  if(inc && cm->savedConflictClauses ){
    if(!Con){
      int num=0;
      saved = cm->savedConflictClauses;
      pm->savedConCls = sat_ArrayAlloc(1);
      for(i=0, lp=saved->space; i<saved->num; i++, lp++){
        sat_ArrayInsert(pm->savedConCls,*lp);
        if(*lp<0)
          num++;
      }
      assert(num%2==0);
      if(pm->verbosity>=2)
        fprintf(vis_stdout,"record %d ConCls for incremental concretization\n",num/2);
    }
    else
      pm->savedConCls = 0;
    sat_ArrayFree(cm->savedConflictClauses);
    cm->savedConflictClauses = 0;
  }
  t2 = util_cpu_ctime();
  pm->tPro += t2-t1;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"process time:%g,total:%g\n",
           (double)((t2-t1)/1000.0),pm->tPro/1000);
  sat_ArrayFree(manager->assertArray);
  status = cm->status;
  cm->option->coreGeneration = 1;
  PureSat_SatFreeManager(cm);
  if(status == SAT_SAT){
    if(pm->verbosity>=1)
      fprintf(vis_stdout,"CEX exist\n");
    return FALSE; /* cex exists*/
  }
  else{
    if(pm->verbosity>=1)
      fprintf(vis_stdout,"no CEX\n");
    return TRUE;   /* no cex*/
  }

}

Here is the call graph for this function:

Here is the caller graph for this function:

boolean PureSat_ConcretTest_Core ( Ntk_Network_t *  network,
PureSat_Manager_t *  pm,
array_t *  sufArray,
bAigEdge_t  property,
array_t *  previousResultArray,
st_table *  junkTable 
)

Function********************************************************************

Synopsis [Concretization procedure for unsat proof-based refinement minimization]

Description []

SideEffects []

SeeAlso []

Definition at line 3159 of file puresatIPUtil.c.

{
  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  int status,i,nodes_in_coi=0;
  satManager_t *cm;
  char *name;
  double t1,t2;
  st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash);
  array_t * tmpRef1;
  st_table *refTable = st_init_table(strcmp,st_strhash);

  arrayForEachItem(char *,sufArray,i,name){
    st_insert(SufAbsNameTable,name,(char*)0);
  }

  manager->assertArray = sat_ArrayAlloc(1);
  sat_ArrayInsert(manager->assertArray,manager->InitState);
  cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);
  cm->option->coreGeneration = 1;
  cm->option->AbRf = 1;
  cm->option->IP = 1;
  t1 = util_cpu_ctime();
  PureSat_CleanMask(manager,ResetVisibleVarMask);
  PuresatMarkVisibleVarWithVPGV(network,sufArray,pm,0,pm->Length+1);

    PureSatSetCOI(network,pm,cm,SufAbsNameTable,0,pm->Length,pm->Length);
    PureSatKillPseudoGV(network,pm,SufAbsNameTable,1,pm->Length);
    PureSat_ResetManager(manager,cm,0);
    PureSatProcessFanout(cm);

  t2 = util_cpu_ctime();
  pm->tPro += t2-t1;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"process time:%g,total:%g\n",
           (double)((t2-t1)/1000.0),pm->tPro/1000);
  if(pm->verbosity>=1){
    nodes_in_coi = PureSat_CountNodesInCoi(cm);
    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
  }
  manager->assertArray2 = cm->assertArray2;
  sat_Main(cm);
  manager->NodesArray = cm->nodesArray;
  t1 = util_cpu_ctime();
    PureSatRecoverFanout(cm,pm);
    PureSat_RestoreAigForDummyNode(manager,pm->oldPos);
    PureSat_CleanMask(manager,ResetVisited3Mask);
    if(cm->status==SAT_UNSAT){
      PureSatProcessDummy(manager,cm,cm->rm->root);
      ResetRTree(cm->rm);
    }
  t2 = util_cpu_ctime();
  pm->tPro += t2-t1;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"process time:%g,total:%g\n",
           (double)((t2-t1)/1000.0),pm->tPro/1000);

  if(cm->status==SAT_UNSAT){
    tmpRef1 = PureSat_GetSufAbsFromCore(network,cm,pm,property,SufAbsNameTable);

    arrayForEachItem(char*,tmpRef1,i,name)
      st_insert(refTable,name,(char*)0);

    arrayForEachItem(char*,sufArray,i,name){
      if(!st_lookup(refTable,name,NIL(char*))&&
         !st_lookup(pm->vertexTable,name,NIL(char*))){
        if(pm->verbosity>=2)
          fprintf(vis_stdout,"%s can be gotten rid of\n",name);
        st_insert(junkTable,name,(char*)0);
      }
    }
    array_free(tmpRef1);
  }

  st_free_table(SufAbsNameTable);
  st_free_table(refTable);
  RT_Free(cm->rm);
  sat_ArrayFree(manager->assertArray);
  status = cm->status;
  cm->option->coreGeneration = 1;
  PureSat_SatFreeManager(cm);
  if(status == SAT_SAT){
    if(pm->verbosity>=1)
      fprintf(vis_stdout,"CEX exist\n");
    return FALSE; // cex exists
  }
  else{
    if(pm->verbosity>=1)
      fprintf(vis_stdout,"no CEX\n");
    return TRUE;   // no cex
  }

}

Here is the call graph for this function:

Here is the caller graph for this function:

int PureSat_CountNodesInCoi ( satManager_t *  cm)

Function********************************************************************

Synopsis [Count number of nodes in COI]

Description [Count number of nodes in COI]

SideEffects []

SeeAlso []

Definition at line 1100 of file puresatIPUtil.c.

{
  int ct=0;
  bAigEdge_t i;

  for(i=satNodeSize;i<cm->nodesArraySize;i+=satNodeSize){
    if(SATflags(i) & CoiMask){
      ct++;

    }
  }
  /*fprintf(vis_stdout,"There are %d node in COI\n",ct);*/
  return ct;
}

Here is the caller graph for this function:

bAigEdge_t PureSat_FindNodeByName ( bAig_Manager_t *  manager,
nameType_t *  name,
int  bound 
)

Function********************************************************************

Synopsis [Find an aig node from its name]

Description []

SideEffects []

SeeAlso []

Definition at line 2815 of file puresatIPUtil.c.

{

  bAigEdge_t node;

  if (!st_lookup(manager->SymbolTableArray[bound], name, &node)){
    node = bAig_NULL;
  }

  return bAig_GetCanonical(manager, node);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSat_GetLatchForNode ( bAig_Manager_t *  manager,
PureSat_Manager_t *  pm,
bAigEdge_t  node,
array_t *  nameArray,
st_table *  tmpTable,
int  cut 
)

Function********************************************************************

Synopsis [Get support latches for one aig node]

Description []

SideEffects []

SeeAlso []

Definition at line 3554 of file puresatIPUtil.c.

{
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  char * name;
  st_table * table;
  st_generator * stgen;

  if(node==bAig_NULL)
    return;

  node = bAig_NonInvertedEdge(node);

  if(flags(node)&VisitedMask)
    return;

  flags(node) |= VisitedMask;


  if(flags(node)&StateBitMask){
    if(!st_lookup(tf->MultiLatchTable,(char*)node,&table)){
      int retVal = st_lookup(tf->idx2name,(char*)node,&name);
      assert(retVal);
      if(!st_lookup(tmpTable,name,NIL(char*))){
        st_insert(tmpTable,name,(char*)0);
        array_insert_last(char *,nameArray,name);
        if(pm->verbosity>=2)
          fprintf(vis_stdout,"insert %s\n",name);
      }
    }
    else{
      st_foreach_item(table,stgen,&name,NIL(char*)){
        if(!st_lookup(tmpTable,name,NIL(char*))){
          st_insert(tmpTable,name,(char*)0);
          array_insert_last(char *,nameArray,name);
          if(pm->verbosity>=2)
            fprintf(vis_stdout,"insert %s\n",name);
        }
      }
    }
  }

  if(cut==2){
    if(flags(node)&Visited2Mask)
      return;
  }
  else{
    if(cut==1){
      if(flags(node)&Visited3Mask)
        return;
    }
    else{
      fprintf(vis_stdout,"wrong cut\n");
      exit(0);
    }
  }

  PureSat_GetLatchForNode(manager,pm,leftChild(node),nameArray,tmpTable,cut);
  PureSat_GetLatchForNode(manager,pm,rightChild(node),nameArray,tmpTable,cut);
}

Here is the caller graph for this function:

int PureSat_IdentifyConflict ( satManager_t *  cm,
long  left,
bAigEdge_t  right,
bAigEdge_t  node 
)

Function********************************************************************

Synopsis [Find the type of conflict, return the value to caller]

Description [

0 1 1 1 1 1 | | | | | | 20---33,49--- 9,13--- 17 --- 5 --- 1--- / \ / \ / \ / \ / \ / \ 1 1 X 0 0 X 1 0 0 1 0 0

Bing note: For case 1, maybe solving conflict with both childern is better, but in sat package, only conflict with left child is solved ]

SideEffects []

SeeAlso []

Definition at line 277 of file puresatIPUtil.c.

{
  int result; /*1:left 2:right 3:both*/
  int value = SATgetValue(left,right,node);
  switch(value){
  case 1:
  case 5:
  case 9:
  case 13:
    result = 1;
    break;
  case 17:
  case 33:
  case 49:
    result = 2;
    break;
  case 20:
    result = 3;
    break;
  default:
    fprintf(vis_stdout,"can't identify the conflict, exit\n");
    exit(0);
  }

  return result;
}

Here is the caller graph for this function:

bAigEdge_t PureSat_MapIP ( mAig_Manager_t *  manager,
bAigEdge_t  node,
int  from,
int  to 
)

Function********************************************************************

Synopsis [Maping interpolant from a timeframe to another timeframe]

Description []

SideEffects []

SeeAlso []

Definition at line 2688 of file puresatIPUtil.c.

{
  bAigTimeFrame_t *tf = manager->timeframeWOI;
  st_table *tmpTable = st_init_table(st_numcmp,st_numhash);
  bAigEdge_t * L1,*L0,result,v1,v0;
  int i;

  if(node==bAig_One||node==bAig_Zero)
    return node;

  L1 = tf->latchInputs[from];
  L0 = tf->latchInputs[to];
  for(i=0;i<tf->nLatches;i++){
   v1 = L1[i];
   v0 = L0[i];
   if(SATisInverted(v1)){
     v1 = SATnot(v1);
     v0 = SATnot(v0);
   }
   st_insert(tmpTable,(char*)v1,(char*)v0);

  }
  L1 = tf->blatchInputs[from];
  L0 = tf->blatchInputs[to];
  for(i=0;i<tf->nbLatches;i++){
    v1 = L1[i];
    v0 = L0[i];
    if(SATisInverted(v1)){
      v1 = SATnot(v1);
      v0 = SATnot(v0);
    }
    st_insert(tmpTable,(char*)v1,(char*)v0);

  }

  manager->class_ = to;
  result = PureSat_MapIPRecur(manager,node,tmpTable);

  st_free_table(tmpTable);

  return result;
}

Here is the call graph for this function:

Here is the caller graph for this function:

bAigEdge_t PureSat_MapIPRecur ( mAig_Manager_t *  manager,
bAigEdge_t  node,
st_table *  tmpTable 
)

Function********************************************************************

Synopsis [Recursively mapping interpolant from a timeframe to another timeframe]

Description []

SideEffects []

SeeAlso []

Definition at line 2639 of file puresatIPUtil.c.

{
  bAigEdge_t v,result,left,right;
  int isInverted;

#if DBG
  assert(node!=bAig_NULL);
#endif
  if(node == bAig_One || node == bAig_Zero){
    return node;
  }

  if(st_lookup(tmpTable,(char *)bAig_NonInvertedEdge(node),&v)){
    if(bAig_IsInverted(node))
      result = bAig_Not(v);
    else
      result = v;

    return result;
  }

  left = PureSat_MapIPRecur(manager,leftChild(node),tmpTable);
  right = PureSat_MapIPRecur(manager,rightChild(node),tmpTable);

  v = PureSat_And(manager,left,right);
  isInverted = bAig_IsInverted(node);
  result = isInverted ? bAig_Not(v) : v;
  st_insert(tmpTable,(char *)bAig_NonInvertedEdge(node),(char *)v);

  //fprintf(vis_stdout,"return %d->%d\n",node,result);
  return result;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSat_MarkGlobalVar ( bAig_Manager_t *  manager,
int  length 
)

Function********************************************************************

Synopsis [Mark global variables]

Description [Mark global variables]

SideEffects []

SeeAlso []

Definition at line 2347 of file puresatIPUtil.c.

{
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  bAigEdge_t * li,* bli,node;
  int i;

  li = tf->latchInputs[length];
  bli = tf->blatchInputs[length];

  for(i=0; i<tf->nLatches; i++){
    node = bAig_NonInvertedEdge(li[i]);
    manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask;
  }

  for(i=0; i<tf->nbLatches; i++){
    node = bAig_NonInvertedEdge(bli[i]);
    manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask;
  }
}

Here is the caller graph for this function:

void PureSat_MarkGlobalVar_AbRf ( bAig_Manager_t *  manager,
int  length 
)

Function********************************************************************

Synopsis [Makr global variable for abstraction refinement]

Description []

SideEffects []

SeeAlso []

Definition at line 2414 of file puresatIPUtil.c.

{
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  bAigEdge_t * li,* bli,node;
  int i;


  li = tf->latchInputs[length];
  bli = tf->blatchInputs[length];

  for(i=0; i<tf->nLatches; i++){
    node = bAig_NonInvertedEdge(li[i]);
    if(flags(node)&VisibleVarMask)
      manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask;
  }

  for(i=0; i<tf->nbLatches; i++){
    node = bAig_NonInvertedEdge(bli[i]);
    if(flags(node)&VisibleVarMask)
      manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask;
  }

}

Here is the caller graph for this function:

void PureSat_MarkTransitiveFaninForArray ( satManager_t *  cm,
satArray_t *  arr,
unsigned int  mask 
)

Function********************************************************************

Synopsis [Mark transitive fanin for an array of aig nodes]

Description [Mark transitive fanin for an array of aig nodes]

SideEffects []

SeeAlso []

Definition at line 465 of file puresatIPUtil.c.

{
  int  i, size;
  bAigEdge_t v;

  if(arr == 0)  return;
  size = arr->num;

  for(i=0; i<size; i++) {
    v = arr->space[i];
    PureSat_MarkTransitiveFaninForNode(cm, v, mask);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSat_MarkTransitiveFaninForArray2 ( mAig_Manager_t *  manager,
satArray_t *  arr,
unsigned int  mask 
)

Function********************************************************************

Synopsis [Mark transitive fanin for an array of aig nodes]

Description [Mark transitive fanin for an array of aig nodes]

SideEffects []

SeeAlso []

Definition at line 525 of file puresatIPUtil.c.

{
bAigEdge_t v;
int i, size;

  if(arr == 0)  return;
  size = arr->num;

  for(i=0; i<size; i++) {
    v = arr->space[i];
    PureSat_MarkTransitiveFaninForNode2(manager, v, mask);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSat_MarkTransitiveFaninForArray3 ( mAig_Manager_t *  manager,
satArray_t *  arr,
unsigned int  mask 
)

Function********************************************************************

Synopsis [Mark transitive fanin for an array of aig nodes]

Description [Mark transitive fanin for an array of aig nodes]

SideEffects []

SeeAlso []

Definition at line 585 of file puresatIPUtil.c.

{
bAigEdge_t v;
int i, size;

  if(arr == 0)  return;
  size = arr->num;

  for(i=0; i<size; i++) {
    v = arr->space[i];
    PureSat_MarkTransitiveFaninForNode3(manager, v, mask);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSat_MarkTransitiveFaninForArray4 ( mAig_Manager_t *  manager,
satArray_t *  arr,
unsigned int  mask,
int  bound 
)

Function********************************************************************

Synopsis [Mark transitive fanin for an array of aig nodes]

Description [Mark transitive fanin for an array of aig nodes]

SideEffects []

SeeAlso []

Definition at line 653 of file puresatIPUtil.c.

{
bAigEdge_t v;
int i, size;

  if(arr == 0)  return;
  size = arr->num;

  for(i=0; i<size; i++) {
    v = arr->space[i];

    v = SATnormalNode(v);
    PureSat_MarkTransitiveFaninForNode4(manager,v,mask,bound);

  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSat_MarkTransitiveFaninForNode ( satManager_t *  cm,
bAigEdge_t  v,
unsigned int  mask 
)

Function********************************************************************

Synopsis [Mark transitive fanin for an aig node]

Description [Mark transitive fanin for an aig node]

SideEffects []

SeeAlso []

Definition at line 434 of file puresatIPUtil.c.

{
  if(v == bAig_NULL)    return;

  v = SATnormalNode(v);

  if(SATflags(v) & mask)        return;

  SATflags(v) |= mask;
  if(SATflags(v) & Visited3Mask) return;

  PureSat_MarkTransitiveFaninForNode(cm, SATleftChild(v), mask);
  PureSat_MarkTransitiveFaninForNode(cm, SATrightChild(v), mask);
}

Here is the caller graph for this function:

void PureSat_MarkTransitiveFaninForNode2 ( mAig_Manager_t *  manager,
bAigEdge_t  v,
unsigned int  mask 
)

Function********************************************************************

Synopsis [Mark transitive fanin for an aig node]

Description [Mark transitive fanin for an aig node]

SideEffects []

SeeAlso []

Definition at line 494 of file puresatIPUtil.c.

{
  if(v == bAig_NULL)    return;

  v = SATnormalNode(v);

  if(flags(v) & mask)   return;

  flags(v) |= mask;
  if(flags(v) & Visited3Mask) return;

  PureSat_MarkTransitiveFaninForNode2(manager, leftChild(v), mask);
  PureSat_MarkTransitiveFaninForNode2(manager, rightChild(v), mask);
}

Here is the caller graph for this function:

void PureSat_MarkTransitiveFaninForNode3 ( mAig_Manager_t *  manager,
bAigEdge_t  v,
unsigned int  mask 
)

Function********************************************************************

Synopsis [Mark transitive fanin for an array of aig nodes]

Description [Mark transitive fanin for an array of aig nodes]

SideEffects []

SeeAlso []

Definition at line 556 of file puresatIPUtil.c.

{
  if(v == 2)    return;

  v = SATnormalNode(v);

  if(flags(v) & mask)   return;

  flags(v) |= mask;

  PureSat_MarkTransitiveFaninForNode3(manager, leftChild(v), mask);
  PureSat_MarkTransitiveFaninForNode3(manager, rightChild(v), mask);
}

Here is the caller graph for this function:

void PureSat_MarkTransitiveFaninForNode4 ( mAig_Manager_t *  manager,
bAigEdge_t  v,
unsigned int  mask,
int  bound 
)

Function********************************************************************

Synopsis [Mark transitive fanin for an array of aig nodes]

Description [Mark transitive fanin for an array of aig nodes]

SideEffects []

SeeAlso []

Definition at line 616 of file puresatIPUtil.c.

{
  if(v == bAig_NULL)    return;

  v = SATnormalNode(v);

  if(flags(v) & mask)   return;

  flags(v) |= mask;

  if((flags(v)&StateBitMask)&&
     !(flags(v)&VisibleVarMask)&&
     (bAig_Class(v)>0)){

    return;
  }

  PureSat_MarkTransitiveFaninForNode4(manager, leftChild(v), mask,bound);
  PureSat_MarkTransitiveFaninForNode4(manager, rightChild(v), mask,bound);
}

Here is the caller graph for this function:

void PureSat_PrintAigStatus ( mAig_Manager_t *  manager)

Function********************************************************************

Synopsis [Print the status of AIG]

Description [Print the status of AIG]

SideEffects []

SeeAlso []

Definition at line 2325 of file puresatIPUtil.c.

{
  (void) fprintf(vis_stdout,"Maximum number of nodes: %ld\n",
                 manager->maxNodesArraySize/bAigNodeSize);
  (void) fprintf(vis_stdout,"Current number of nodes: %ld\n",
                 manager->nodesArraySize/bAigNodeSize);
  fprintf(vis_stdout,"Current Max Node Index: %ld\n\n",
          manager->nodesArraySize);
}

Here is the caller graph for this function:

void PureSat_ResetCoi ( satManager_t *  cm)

Function********************************************************************

Synopsis [Reset COI mask for all nodes]

Description [Reset COI mask for all nodes]

SideEffects []

SeeAlso []

Definition at line 733 of file puresatIPUtil.c.

{
  bAigEdge_t i;
  for(i=satNodeSize;i<cm->nodesArraySize;i+=satNodeSize){
    if(SATflags(i) & CoiMask)
      SATflags(i) &= ResetCoiMask;
  }
}

Here is the caller graph for this function:

void PureSat_ResetManager ( mAig_Manager_t *  manager,
satManager_t *  cm,
int  clean 
)

Function********************************************************************

Synopsis [Reset a sat manager]

Description [Reset a sat manager]

SideEffects []

SeeAlso []

Definition at line 1227 of file puresatIPUtil.c.

{

  int i;
  satVariable_t var;
  satLevel_t *d;

  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;
    cm->currentDecision = 0;
  }

  if(cm->literals){
    sat_FreeLiteralsDB(cm->literals);
    cm->literals=0;
    sat_AllocLiteralsDB(cm);
  }
  if(cm->each){
    FREE(cm->each);
    cm->each = sat_InitStatistics();
  }

  if(cm->queue)         sat_FreeQueue(cm->queue);
  if(cm->BDDQueue)      sat_FreeQueue(cm->BDDQueue);
  if(cm->unusedAigQueue)sat_FreeQueue(cm->unusedAigQueue);
  cm->queue = 0;
  cm->BDDQueue = 0;
  cm->unusedAigQueue = 0;


  if(cm->nonobjUnitLitArray)   sat_ArrayFree(cm->nonobjUnitLitArray);
  if(cm->objUnitLitArray)      sat_ArrayFree(cm->objUnitLitArray);
  if(cm->orderedVariableArray) sat_ArrayFree(cm->orderedVariableArray);
  if(cm->dormantConflictArray) sat_ArrayFree(cm->dormantConflictArray);
  if(cm->shrinkArray)          sat_ArrayFree(cm->shrinkArray);

  cm->nonobjUnitLitArray = 0;
  cm->objUnitLitArray = 0;
  cm->orderedVariableArray = 0;
  cm->dormantConflictArray = 0;
  cm->shrinkArray = 0;

  /*change initNumVariable after cm->variableArray has been freed,
    otherwise, initNumVariable may change*/
  cm->nodesArray = manager->NodesArray;
  cm->nodesArraySize = manager->nodesArraySize;
  cm->initNodesArraySize = manager->nodesArraySize;
  cm->maxNodesArraySize = manager->maxNodesArraySize;
  cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize)-1;
  cm->initNumClauses = 0;
  cm->initNumLiterals = 0;

  cm->ipm = manager->ipm;
  cm->assertArray = manager->assertArray;
  cm->assertArray2 = manager->assertArray2;
  cm->InitState = manager->InitState;
  cm->CoiAssertArray = manager->CoiAssertArray;
  cm->EqArray = manager->EqArray;

  cm->currentVarPos = 0;
  cm->currentTopConflict = 0;
  cm->currentTopConflictCount = 0;
  cm->lowestBacktrackLevel = 0;
  cm->implicatedSoFar = 0;
  //cm->status = 0;

  if(clean){
    for(i=bAigNodeSize;i<cm->nodesArraySize;i+=bAigNodeSize)
      cm->nodesArray[i] = 2;
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSat_RestoreAigForDummyNode ( mAig_Manager_t *  manager,
int  oldPosition 
)

Function********************************************************************

Synopsis [Restore AIG to get rid of Dummy nodes]

Description [Restore AIG to get rid of Dummy nodes]

SideEffects []

SeeAlso []

Definition at line 1338 of file puresatIPUtil.c.

{

  bAigEdge_t  i;

  for(i=manager->nodesArraySize-bAigNodeSize;
      i>oldPosition;i=i-bAigNodeSize){
#if DBG
    assert(leftChild(i)==bAig_NULL&&
           rightChild(i)==bAig_NULL);
    assert(flags(i)&DummyMask);
#endif
    FREE(fanout(i));
  }

  manager->nodesArraySize = oldPosition+bAigNodeSize;

  return;

}

Here is the caller graph for this function:

void PureSat_SatFreeManager ( satManager_t *  cm)

Function********************************************************************

Synopsis [Free a PureSAT manager]

Description [Free a PureSAT manager]

SideEffects []

SeeAlso []

Definition at line 2221 of file puresatIPUtil.c.

{
satVariable_t var;
satLevel_t *d;
int i;


  if(cm->option->coreGeneration){
    st_free_table(cm->anteTable);
    st_free_table(cm->RTreeTable);

    cm->anteTable=0;
    cm->RTreeTable=0;
  }

  /*timeframe, timeframeWOI,HashTable can't be freed*/

  if(cm->option)        sat_FreeOption(cm->option);
  if(cm->total)         sat_FreeStatistics(cm->total);
  if(cm->each)          sat_FreeStatistics(cm->each);

  if(cm->literals)      sat_FreeLiteralsDB(cm->literals);

  cm->option=0;
  cm->total=0;
  cm->each=0;
  cm->literals=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;
  }

  if(cm->queue)         sat_FreeQueue(cm->queue);
  if(cm->BDDQueue)      sat_FreeQueue(cm->BDDQueue);
  if(cm->unusedAigQueue)sat_FreeQueue(cm->unusedAigQueue);
  cm->queue = 0;
  cm->BDDQueue = 0;
  cm->unusedAigQueue = 0;

  if(cm->auxObj)               sat_ArrayFree(cm->auxObj);
  if(cm->obj)                  sat_ArrayFree(cm->obj);
  if(cm->unitLits)             sat_ArrayFree(cm->unitLits);
  if(cm->pureLits)             sat_ArrayFree(cm->pureLits);
  if(cm->assertion)            sat_ArrayFree(cm->assertion);
  if(cm->auxArray)             sat_ArrayFree(cm->auxArray);
  if(cm->nonobjUnitLitArray)   sat_ArrayFree(cm->nonobjUnitLitArray);
  if(cm->objUnitLitArray)      sat_ArrayFree(cm->objUnitLitArray);
  if(cm->orderedVariableArray) sat_ArrayFree(cm->orderedVariableArray);
  if(cm->savedConflictClauses) sat_ArrayFree(cm->savedConflictClauses);

  cm->auxObj = 0;
  cm->obj = 0;
  cm->unitLits = 0;
  cm->pureLits = 0;
  cm->assertion = 0;
  cm->auxArray = 0;
  cm->nonobjUnitLitArray = 0;
  cm->objUnitLitArray = 0;
  cm->orderedVariableArray = 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->comment)       free(cm->comment);
  cm->comment=0;

  FREE(cm);
}

Here is the call graph for this function:

Here is the caller graph for this function:

satManager_t* PureSat_SatManagerAlloc ( bAig_Manager_t *  manager,
PureSat_Manager_t *  pm,
bAigEdge_t  object,
array_t *  auxObjectArray 
)

Function********************************************************************

Synopsis [Allocate a PureSAT Manager]

Description [Allocate a PureSAT Manager]

SideEffects []

SeeAlso []

Definition at line 1999 of file puresatIPUtil.c.

{
  satManager_t * cm;
  satOption_t *option;
  int i,size;
  bAigEdge_t tv;

  cm = ALLOC(satManager_t, 1);
  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)-1;
  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;

  cm->ipm = manager->ipm;
  cm->assertArray = manager->assertArray;
  cm->assertArray2 = manager->assertArray2;
  cm->InitState = manager->InitState;
  cm->CoiAssertArray = manager->CoiAssertArray;
  cm->EqArray = manager->EqArray;

  if(auxObjectArray) {
    cm->auxObj = sat_ArrayAlloc(auxObjectArray->num+1);
    size = auxObjectArray->num;
    for(i=0; i<size; i++) {
      tv = array_fetch(bAigEdge_t, auxObjectArray, i);
      if(tv == 1)       continue;
      else if(tv == 0) {
        cm->status = SAT_UNSAT;
        break;
      }
      sat_ArrayInsert(cm->auxObj, tv);
    }
  }
  if(object == 0)      cm->status = SAT_UNSAT;
  else if(object == 1) cm->status = SAT_SAT;


  if(cm->status == 0) {
    if(object!=-1){
      cm->obj = sat_ArrayAlloc(1);
      sat_ArrayInsert(cm->obj, object);
    }
    /* initialize option*/
    option = sat_InitOption();

    option->coreGeneration = 1;
    option->ForceFinish = 1;

    option->clauseDeletionHeuristic = 0;
    option->includeLevelZeroLiteral = 1;
    option->minimizeConflictClause = 0;
    option->IP = 1;
    option->RT = 1;
    option->verbose = pm->verbosity;

    cm->anteTable = st_init_table(st_numcmp,st_numhash);
    cm->RTreeTable = st_init_table(st_ptrcmp,st_ptrhash);

    cm->option = option;
    cm->each = sat_InitStatistics();

    BmcRestoreAssertion(manager,cm);

    /* value reset..*/
    sat_CleanDatabase(cm);

    /* set cone of influence*/
    sat_SetConeOfInfluence(cm);
    sat_AllocLiteralsDB(cm);
  }
  return cm;
}

Here is the call graph for this function:

Here is the caller graph for this function:

satManager_t* PureSat_SatManagerAlloc_WOCOI ( mAig_Manager_t *  manager,
PureSat_Manager_t *  pm,
bAigEdge_t  object,
array_t *  auxObjectArray 
)

Function********************************************************************

Synopsis [Allocate a PureSAT Manager without setting COI]

Description [Allocate a PureSAT Manager without setting COI]

SideEffects []

SeeAlso []

Definition at line 2111 of file puresatIPUtil.c.

{
  satManager_t * cm;
  satOption_t *option;
  int i,size;
  bAigEdge_t tv;

  cm = ALLOC(satManager_t, 1);
  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)-1;
  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;

  cm->ipm = manager->ipm;
  cm->assertArray = manager->assertArray;
  cm->assertArray2 = manager->assertArray2;
  cm->InitState = manager->InitState;
  cm->CoiAssertArray = manager->CoiAssertArray;
  cm->EqArray = manager->EqArray;

  if(auxObjectArray) {
    cm->auxObj = sat_ArrayAlloc(auxObjectArray->num+1);
    size = auxObjectArray->num;
    for(i=0; i<size; i++) {
      tv = array_fetch(bAigEdge_t, auxObjectArray, i);
      if(tv == 1)       continue;
      else if(tv == 0) {
        cm->status = SAT_UNSAT;
        break;
      }
      sat_ArrayInsert(cm->auxObj, tv);
    }
  }
  if(object == 0)      cm->status = SAT_UNSAT;
  else if(object == 1) cm->status = SAT_SAT;


  if(cm->status == 0) {
    if(object!=-1){
      cm->obj = sat_ArrayAlloc(1);
      sat_ArrayInsert(cm->obj, object);
    }

    option = sat_InitOption();
    option->ForceFinish = 1;

    option->coreGeneration = 1;
    option->clauseDeletionHeuristic = 0;
    option->includeLevelZeroLiteral = 1;
    option->minimizeConflictClause = 0;
    option->IP = 0;
    option->RT = 1;
    option->verbose = pm->verbosity;

    cm->anteTable = st_init_table(st_numcmp,st_numhash);
    cm->RTreeTable = st_init_table(st_ptrcmp,st_ptrhash);

    cm->option = option;
    cm->each = sat_InitStatistics();

    BmcRestoreAssertion(manager,cm);

    sat_CleanDatabase(cm);

    /* WOCOI: NO set cone of influence*/
    sat_AllocLiteralsDB(cm);
  }
  return cm;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSat_SetCOI ( satManager_t *  cm)

Function********************************************************************

Synopsis [Set COI mask for SAT solver]

Description [Set COI mask for SAT solver]

SideEffects []

SeeAlso []

Definition at line 711 of file puresatIPUtil.c.

{

  PureSat_MarkTransitiveFaninForArray(cm, cm->auxObj, CoiMask);
  PureSat_MarkTransitiveFaninForArray(cm, cm->obj, CoiMask);
  PureSat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);

}

Here is the call graph for this function:

int PureSat_TestConvergeForIP ( mAig_Manager_t *  manager,
PureSat_Manager_t *  pm,
satManager_t *  cm,
bAigEdge_t  state1,
bAigEdge_t  state2 
)

Function********************************************************************

Synopsis [Convergence test for flat interpolation algorithm]

Description [Convergence test for flat interpolation algorithm]

SideEffects []

SeeAlso []

Definition at line 1799 of file puresatIPUtil.c.

{
  satArray_t * tmp1,*tmp2,*tmp3, *tmp4,*tmp5, *tmp6, *tmp7;
  int status, nodes_in_coi = 0;

 if(state2 == bAig_Zero)
    return 1;
  if(state1 == bAig_One)
    return 1;
  if(state1 == bAig_Zero && state2 != bAig_Zero)
    return 0;
  if(state1 != bAig_One && state2 == bAig_One)
    return 0;

  if(pm->verbosity>=1)
    fprintf(vis_stdout,"Test convergence:\n");
  PureSat_ResetCoi(cm);
  if(pm->verbosity>=1){
    fprintf(vis_stdout,"after reset COI\n");
    nodes_in_coi = PureSat_CountNodesInCoi(cm);
    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
  }
  tmp1 = cm->obj;
  tmp2 = cm->auxObj;
  tmp3 = cm->assertion;
  tmp4 = cm->assertArray;
  //Bing:
  tmp5 = cm->unitLits;
  tmp6 = cm->pureLits;
  tmp7 = cm->nonobjUnitLitArray;
  cm->obj = 0;
  cm->auxObj = 0;
  cm->assertion = 0;
  //cm->assertArray2 = 0;
  cm->assertArray = sat_ArrayAlloc(1);
  sat_ArrayInsert(cm->assertArray,SATnot(state1));
  sat_ArrayInsert(cm->assertArray,state2);
  sat_SetConeOfInfluence(cm);
  if(pm->verbosity>=1){
    fprintf(vis_stdout,"after add new init states:\n");
    nodes_in_coi = PureSat_CountNodesInCoi(cm);
    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
  }
  cm->option->coreGeneration = 0;
  //cm->option->effIP = 0;
  cm->option->IP = 0;
  cm->status = 0;
  sat_Main(cm);
  if(manager->NodesArray!=cm->nodesArray)
    /*cm->nodesArray may be reallocated*/
    manager->NodesArray = cm->nodesArray;
  cm->obj = tmp1;
  cm->auxObj = tmp2;
  cm->assertion = tmp3;
  sat_ArrayFree(cm->assertArray);
  cm->assertArray = tmp4;

  cm->unitLits = tmp5;
  cm->pureLits = tmp6;
  cm->nonobjUnitLitArray = tmp7;

  cm->option->coreGeneration = 1;

  cm->option->IP = 1;
  status = cm->status;
#if DBG
  assert(cm->currentDecision>=-1);
#endif
  if(cm->currentDecision!=-1)
    sat_Backtrack(cm,-1);
  cm->status = 0;

  if(status == SAT_UNSAT)
    /*state2 contains state1, reach convergence*/
    return 1;
  else
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int PureSat_TestConvergeForIP_AbRf ( Ntk_Network_t *  network,
satManager_t *  cm,
PureSat_Manager_t *  pm,
array_t *  CoiArray,
bAigEdge_t  state1,
bAigEdge_t  state2 
)

Function********************************************************************

Synopsis [Convergence test for interpolation algorithm with abstraction refinement ]

Description [Convergence test for flat interpolation algorithmwith abstraction refinement ]

SideEffects []

SeeAlso []

Definition at line 1899 of file puresatIPUtil.c.

{
  satArray_t * tmp1,*tmp2,*tmp3, *tmp4,*tmp5, *tmp6, *tmp7;
  int status, nodes_in_coi = 0;
  mAig_Manager_t * manager;


  if(state2 == bAig_Zero)
    return 1;
  if(state1 == bAig_One)
    return 1;
  if(state1 == bAig_Zero && state2 != bAig_Zero)
    return 0;
  if(state1 != bAig_One && state2 == bAig_One)
    return 0;


  manager = Ntk_NetworkReadMAigManager(network);

  if(pm->verbosity>=1)
    fprintf(vis_stdout,"Test convergence:\n");
  PureSat_ResetCoi(cm);
  if(pm->verbosity>=1){
    fprintf(vis_stdout,"after reset COI\n");
    nodes_in_coi = PureSat_CountNodesInCoi(cm);
    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
  }
  tmp1 = cm->obj;
  tmp2 = cm->auxObj;
  tmp3 = cm->assertion;
  tmp4 = cm->assertArray;

  tmp5 = cm->unitLits;
  tmp6 = cm->pureLits;
  tmp7 = cm->nonobjUnitLitArray;
  cm->obj = 0;
  cm->auxObj = 0;
  cm->assertion = 0;
  cm->unitLits = 0;
  cm->pureLits = 0;
  cm->nonobjUnitLitArray = 0;
  cm->assertArray = sat_ArrayAlloc(1);
  sat_ArrayInsert(cm->assertArray,SATnot(state1));
  sat_ArrayInsert(cm->assertArray,state2);

  sat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);

  if(pm->verbosity>=1){
    fprintf(vis_stdout,"after add new init states:\n");
    nodes_in_coi = PureSat_CountNodesInCoi(cm);
    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
  }
  cm->option->coreGeneration = 0;
  cm->status = 0;
  cm->option->AbRf = 0;
  sat_Main(cm);
  cm->option->AbRf = 1;
  if(manager->NodesArray!=cm->nodesArray)
    /*cm->nodesArray may be reallocated*/
    manager->NodesArray = cm->nodesArray;
  sat_ArrayFree(cm->assertArray);
  manager->assertArray = tmp4;
  cm->obj = tmp1;
  cm->auxObj = tmp2;
  cm->assertion = tmp3;
  cm->assertArray = tmp4;

  cm->unitLits = tmp5;
  cm->pureLits = tmp6;
  cm->nonobjUnitLitArray = tmp7;
  cm->option->coreGeneration = 1;
  status = cm->status;
  if(cm->currentDecision!=-1)
    sat_Backtrack(cm,-1);
  cm->status = 0;

  if(status == SAT_UNSAT)
    /*state2 contains state1, reach convergence*/
    return 1;
  else
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSat_UnMarkGlobalVar ( bAig_Manager_t *  manager,
int  length 
)

Function********************************************************************

Synopsis [UnMark global variables]

Description [UnMark global variables]

SideEffects []

SeeAlso []

Definition at line 2380 of file puresatIPUtil.c.

{
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  bAigEdge_t * li,* bli,node;
  int i;

  li = tf->latchInputs[length];
  bli = tf->blatchInputs[length];

  for(i=0; i<tf->nLatches; i++){
    node = bAig_NonInvertedEdge(li[i]);
    manager->NodesArray[node+bAigFlags] &= ResetGlobalVarMask;
  }

  for(i=0; i<tf->nbLatches; i++){
    node = bAig_NonInvertedEdge(bli[i]);
    manager->NodesArray[node+bAigFlags] &= ResetGlobalVarMask;
  }
}

Here is the caller graph for this function:

void PureSatAbstractLatch ( bAig_Manager_t *  manager,
bAigEdge_t  v,
st_table *  tmpTable 
)

Function********************************************************************

Synopsis [Build abstraction from concrete model]

Description [Build abstraction from concrete model]

SideEffects []

SeeAlso []

Definition at line 894 of file puresatIPUtil.c.

{
  bAigEdge_t nv;

  /*fanin: set left and right to bAig_NULL*/
  nv = bAig_NonInvertedEdge(v);

  if(leftChild(nv)!=bAig_NULL){
    if(!(flags(leftChild(nv))&CoiMask))
      flags(leftChild(nv)) |= Visited3Mask;
    manager->NodesArray[nv+bAigLeft]=bAig_NULL;
  }

  if(rightChild(nv)!=bAig_NULL){
    if(!(flags(rightChild(nv))&CoiMask))
      flags(rightChild(nv)) |= Visited3Mask;
    manager->NodesArray[nv+bAigRight]=bAig_NULL;
  }

}

Here is the caller graph for this function:

void PureSatAddIdenLatchToAbs ( Ntk_Network_t *  network,
PureSat_Manager_t *  pm,
array_t *  nameArray 
)

Function********************************************************************

Synopsis [Some latches have the same aig node, add them all to abstractions once one is added. ]

Description []

SideEffects []

SeeAlso []

Definition at line 3441 of file puresatIPUtil.c.

{
  int i;
  st_generator * stgen;
  st_table* table;
  char *name,*name1;
  st_table *table1 = st_init_table(st_ptrcmp,st_ptrhash);
  array_t * tmpArray = array_alloc(char*,0);

  st_foreach_item(pm->vertexTable,stgen,&name,NIL(char*))
    st_insert(table1,name,(char*)0);
  arrayForEachItem(char*,nameArray,i,name)
    st_insert(table1,name,(char*)0);

  arrayForEachItem(char*,nameArray,i,name){

    if(st_lookup(pm->IdenLatchTable,name,&table)){
      st_foreach_item(table,stgen,&name1,NIL(char*)){
        if(!st_lookup(table1,name1,NIL(char*))){
          st_insert(table1,name1,(char*)0);
          array_insert_last(char*,tmpArray,name1);
        }
      }
    }
  }

  arrayForEachItem(char*,tmpArray,i,name){
    array_insert_last(char*,nameArray,name);
    if(pm->verbosity>=2)
      fprintf(vis_stdout,"add %s to refineArray\n",name);
  }

  array_free(tmpArray);
  st_free_table(table1);
}

Here is the caller graph for this function:

void PureSatBmcGetCoiForLtlFormula_New ( Ntk_Network_t *  network,
Ctlsp_Formula_t *  formula,
st_table *  ltlCoiTable 
)

Function********************************************************************

Synopsis [Get COI nodes for a LTL formula]

Description [Get COI nodes for a LTL formula]

SideEffects []

SeeAlso []

Definition at line 408 of file puresatIPUtil.c.

{
  st_table *visited = st_init_table(st_ptrcmp, st_ptrhash);

  PureSatBmcGetCoiForLtlFormulaRecursive_New(network, formula, ltlCoiTable, visited);
  st_free_table(visited);
  return;
} /* BmcGetCoiForLtlFormula() */

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatBmcGetCoiForLtlFormulaRecursive_New ( Ntk_Network_t *  network,
Ctlsp_Formula_t *  formula,
st_table *  ltlCoiTable,
st_table *  visited 
)

Function********************************************************************

Synopsis [Recursively get COI nodes for a LTL formula]

Description [Recursively get COI nodes for a LTL formula]

SideEffects []

SeeAlso []

Definition at line 367 of file puresatIPUtil.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, (char *) node, &tmp)){
      /* Node already visited */
      return;
    }
    PureSatBmcGetCoiForNtkNode_New(node, ltlCoiTable, visited);
    return;
  }
  PureSatBmcGetCoiForLtlFormulaRecursive_New(network, formula->left,  ltlCoiTable, visited);
  PureSatBmcGetCoiForLtlFormulaRecursive_New(network, formula->right, ltlCoiTable, visited);

  return;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatBmcGetCoiForNtkNode_New ( Ntk_Node_t *  node,
st_table *  CoiTable,
st_table *  visited 
)

Function********************************************************************

Synopsis [Get COI for a network node]

Description [Get COI for a network node]

SideEffects []

SeeAlso []

Definition at line 322 of file puresatIPUtil.c.

{
  int        i;
  Ntk_Node_t *faninNode;

  if(node == NIL(Ntk_Node_t)){
    return;
  }


  if (st_lookup_int(visited, (char *) node, NIL(int))){
    return;
  }
  st_insert(visited, (char *) node, (char *) 0);

  if(Ntk_NodeTestIsInput(node))
    return;

  if (Ntk_NodeTestIsLatch(node)){
    st_insert(CoiTable, (char *) node, (char *)0);
  }

  Ntk_NodeForEachFanin(node, i, faninNode) {
    PureSatBmcGetCoiForNtkNode_New(faninNode, CoiTable, visited);
  }

  return;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatCheckCoi ( bAig_Manager_t *  manager)

Function********************************************************************

Synopsis [sanity check for abstraction processing]

Description [sanity check for abstraction processing]

SideEffects []

SeeAlso []

Definition at line 1718 of file puresatIPUtil.c.

{
  long i;
  for(i=bAigNodeSize;i<manager->nodesArraySize;i+=bAigNodeSize){
    if(flags(i) & IsCNFMask)
      continue;
    if(!(flags(i) & CoiMask))
      continue;
    PureSatCheckCoiNode(manager,i);
  }

}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatCheckCoiNode ( bAig_Manager_t *  manager,
bAigEdge_t  node 
)

Function********************************************************************

Synopsis [sanity check for one node for abstraction processing]

Description [sanity check for one node for abstraction processing]

SideEffects []

SeeAlso []

Definition at line 1671 of file puresatIPUtil.c.

{
  int i;
  long *fan;
  long  nfan,child, cur;
  int left,inv;

  nfan = nFanout(node);
  fan = (bAigEdge_t*)fanout(node);
  if(fan==0) return;
  /*check child*/
  assert((leftChild(node)==bAig_NULL)||
   (flags(leftChild(node))&CoiMask));
  assert((rightChild(node)==bAig_NULL)||
   (flags(rightChild(node))&CoiMask));
  if((leftChild(node)==bAig_NULL)||(rightChild(node)==bAig_NULL))
    assert((leftChild(node)==bAig_NULL)&&(rightChild(node)==bAig_NULL));
  /*check fanout*/
  for(i=0; i<nfan; i++){
    cur = fan[i]>>1;
    assert(flags(cur)&CoiMask);
    left=SATisInverted(fan[i])?0:1;
    inv=SATisInverted(cur)?1:0;
    child = inv?SATnormalNode(node)+1:SATnormalNode(node);
    if(left){
     assert(child==leftChild(cur));
    }
    else{
      assert(child==rightChild(cur));
    }
  }

}

Here is the caller graph for this function:

array_t* PureSatComputeOrder_2 ( Ntk_Network_t *  network,
PureSat_Manager_t *  pm,
array_t *  vertexArray,
array_t *  invisibleArray,
int *  sccArray,
int *  NumInSecondLevel 
)

Function********************************************************************

Synopsis [Sort latch candidate based on BFS ring and RC information]

Description []

SideEffects []

SeeAlso []

Definition at line 3409 of file puresatIPUtil.c.

{

  array_t * RCArray;

  PureSatGenerateDfs(network,pm,vertexArray);
  RCArray = PureSatGenerateRCArray_2(network,pm,invisibleArray,
                                   NumInSecondLevel);

  return RCArray;
}

Here is the call graph for this function:

Here is the caller graph for this function:

bAigEdge_t PureSatCreatebAigOfPropFormula ( Ntk_Network_t *  network,
bAig_Manager_t *  manager,
int  bound,
Ctlsp_Formula_t *  ltl,
int  withInitialState 
)

Function********************************************************************

Synopsis [Create Aig for a ltl formula]

Description []

SideEffects []

SeeAlso []

Definition at line 2844 of file puresatIPUtil.c.

{
  int index;
  bAigEdge_t result, left, right, *li;
  bAigTimeFrame_t *timeframe;

  if (ltl == NIL(Ctlsp_Formula_t))      return bAig_NULL;
  if (ltl->type == Ctlsp_TRUE_c)        return bAig_One;
  if (ltl->type == Ctlsp_FALSE_c)       return bAig_Zero;

  assert(Ctlsp_isPropositionalFormula(ltl));

  if(withInitialState) timeframe = manager->timeframe;
  else                 timeframe = manager->timeframeWOI;

  if (ltl->type == Ctlsp_ID_c){
      char *nodeNameString  = Ctlsp_FormulaReadVariableName(ltl);
      char *nodeValueString = Ctlsp_FormulaReadValueName(ltl);
      Ntk_Node_t *node      = Ntk_NetworkFindNodeByName(network, nodeNameString);

      Var_Variable_t *nodeVar;
      int             nodeValue;

      MvfAig_Function_t  *tmpMvfAig;
      st_table           *nodeToMvfAigTable; /* maps each node to its mvfAig */

      if (node == NIL(Ntk_Node_t)) {
        char   *nameKey;
        char   tmpName[100];

        sprintf(tmpName, "%s_%d", nodeNameString, bound);
        nameKey = util_strsav(tmpName);

        result  = PureSat_FindNodeByName(manager, nameKey,bound);
        if(result == bAig_NULL){
           result = PureSat_CreateVarNode(manager, nameKey);
        } else {

          FREE(nameKey);
        }
        return result;
      }

      nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
      assert(nodeToMvfAigTable != NIL(st_table));

      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 ) {
          (void) fprintf(vis_stderr, "Value specified in RHS is not in domain of variable\n");
          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
          return bAig_NULL;
        }
      }
      else {
        int check;
         check = StringCheckIsInteger(nodeValueString, &nodeValue);
         if( check == 0 ) {
          (void) fprintf(vis_stderr,"Illegal value in the RHS\n");
          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
          return bAig_NULL;
         }
         if( check == 1 ) {
          (void) fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
          (void) fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
          return bAig_NULL;
         }
         if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
          (void) fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
          return bAig_NULL;

         }
      }
      result = MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue);
      result = bAig_GetCanonical(manager, result);
      if(st_lookup(timeframe->li2index, (char *)result, &index)) {
        li = timeframe->latchInputs[bound];
        result = bAig_GetCanonical(manager, li[index]);
      }
      else if(st_lookup(timeframe->o2index, (char *)result, &index)) {
        li = timeframe->outputs[bound];
        result = bAig_GetCanonical(manager, li[index]);

      }
      else if(st_lookup(timeframe->i2index, (char *)result, &index)) {
        li = timeframe->internals[bound];
        result = bAig_GetCanonical(manager, li[index]);

      }
      return result;
  }

  left = PureSatCreatebAigOfPropFormula(network, manager, bound, ltl->left, withInitialState);
  if (left == bAig_NULL){
    return bAig_NULL;
  }
  right = PureSatCreatebAigOfPropFormula(network, manager, bound, ltl->right, withInitialState);
  if (right == bAig_NULL && ltl->type ==Ctlsp_NOT_c ){
    return bAig_Not(left);
  }
  else if(right == bAig_NULL) {
    return bAig_NULL;
  }

  switch(ltl->type) {

    case Ctlsp_OR_c:
      result = PureSat_Or(manager, left, right);
      break;
    case Ctlsp_AND_c:
      result = PureSat_And(manager, left, right);
      break;
    case Ctlsp_THEN_c:
      result = PureSat_Then(manager, left, right);
      break;
    case Ctlsp_EQ_c:
      result = PureSat_Eq(manager, left, right);
      break;
    case Ctlsp_XOR_c:
      result = PureSat_Xor(manager, left, right);
      break;
    default:
      fail("Unexpected type");
  }
  return result;
} /* BmcCirCUsCreatebAigOfPropFormula */

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatCreateInitAbsByAIG ( bAig_Manager_t *  manager,
PureSat_Manager_t *  pm,
bAigEdge_t  node,
st_table *  tmpTable 
)

Function********************************************************************

Synopsis [Create initial abstraction from aig]

Description []

SideEffects []

SeeAlso []

Definition at line 3492 of file puresatIPUtil.c.

{
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  char * name;
  st_table * table;
  st_generator * stgen;

  if(node==bAig_NULL)
    return;

  node = bAig_NonInvertedEdge(node);

  if(flags(node)&VisitedMask)
    return;

  flags(node) |= VisitedMask;


  if(flags(node)&StateBitMask){
    if(!st_lookup(tf->MultiLatchTable,(char*)node,&table)){
      int retVal = st_lookup(tf->idx2name,(char*)node,&name);
      assert(retVal);
      if(!st_lookup(tmpTable,name,NIL(char*))){
        st_insert(tmpTable,name,(char*)0);

      }
    }
    else{
      st_foreach_item(table,stgen,&name,NIL(char*)){
        if(!st_lookup(tmpTable,name,NIL(char*))){
          st_insert(tmpTable,name,(char*)0);

        }
      }
    }
  }

  if(flags(node)&StateBitMask)
    return;

  PureSatCreateInitAbsByAIG(manager,pm,leftChild(node),tmpTable);
  PureSatCreateInitAbsByAIG(manager,pm,rightChild(node),tmpTable);
}

Here is the caller graph for this function:

void PureSatGenerateDfs ( Ntk_Network_t *  network,
PureSat_Manager_t *  pm,
array_t *  vertexArray 
)

Function********************************************************************

Synopsis [Generate the ring information for the whole circuit]

Description []

SideEffects []

SeeAlso []

Definition at line 3344 of file puresatIPUtil.c.

{

  int dfs = 1,i,ct=0;
  char *name;
  Ntk_Node_t *node;
  array_t * ringArray = array_alloc(char *,0);
  array_t * coreArray;
  lsGen gen;
  st_generator * stgen;

  Ntk_NetworkForEachNode( network, gen, node ) {
    PureSatNodeSetColor( node, dfsWhite_c );
  }

  arrayForEachItem(char *,vertexArray,i,name){
    st_insert(pm->node2dfsTable,name,(char*)(long)dfs);
    node = Ntk_NetworkFindNodeByName(network,name);
    PureSatNodeSetColor(node,dfsBlack_c);
    ct++;
  }

  coreArray = array_dup(vertexArray);

  while(coreArray->num>0){
    dfs++;
    ringArray = PureSatGenerateRing(network,pm,coreArray,
                                    &dfs);
    arrayForEachItem(char*,ringArray,i,name){
      st_insert(pm->node2dfsTable,name,(char*)(long)dfs);

      ct++;
    }
    array_free(coreArray);
    coreArray = ringArray;
  }

  st_foreach_item(pm->CoiTable,stgen,&node,NIL(char*)){
    name = Ntk_NodeReadName(node);
    if(!st_lookup(pm->node2dfsTable,name,NIL(char*))){
      st_insert(pm->node2dfsTable,name,(char*)LARGEDFS);
      if(pm->verbosity>=2)
        fprintf(vis_stdout,"%s LARGEDFS is inserted into node2dfsTable\n",name);
    }
  }

  return;

}

Here is the call graph for this function:

Here is the caller graph for this function:

array_t* PureSatGenerateRing ( Ntk_Network_t *  network,
PureSat_Manager_t *  pm,
array_t *  coreArray,
int *  dfs 
)

Function********************************************************************

Synopsis [Generate BFS ring for one array]

Description []

SideEffects []

SeeAlso []

Definition at line 3311 of file puresatIPUtil.c.

{
  array_t * ringArray = array_alloc(char *,0);
  int i,j;
  char *name;
  Ntk_Node_t *node1,*node;

  arrayForEachItem(char *,coreArray,i,name){
    node1 = Ntk_NetworkFindNodeByName(network,name);
    Ntk_NodeForEachFanin(node1,j,node){
      PureSatGenerateRingForNode(network,pm,node,
                                 ringArray,dfs);
    }
  }
  return ringArray;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatGenerateRingForNode ( Ntk_Network_t *  network,
PureSat_Manager_t *  pm,
Ntk_Node_t *  node1,
array_t *  ringArray,
int *  dfs 
)

Function********************************************************************

Synopsis [Generate BFS ring for a network node]

Description []

SideEffects []

SeeAlso []

Definition at line 3271 of file puresatIPUtil.c.

{
  Ntk_Node_t *node;
  char *name;
  int i;

  if(PureSatNodeReadColor(node1) == dfsBlack_c)
    return;
  PureSatNodeSetColor(node1,dfsBlack_c);
  if(Ntk_NodeTestIsLatch(node1)){
    name = Ntk_NodeReadName(node1);
    st_insert(pm->node2dfsTable,name,(char*)(long)(*dfs));
    array_insert_last(char *,ringArray,name);
    return;
  }

  Ntk_NodeForEachFanin(node1,i,node){
    PureSatGenerateRingForNode(network,pm,node,ringArray,
                               dfs);
  }
  return;
}

Here is the call graph for this function:

Here is the caller graph for this function:

st_table* PureSatGetAigCoi ( Ntk_Network_t *  network,
PureSat_Manager_t *  pm,
bAigEdge_t  property 
)

Function********************************************************************

Synopsis [Get COI reduction based on aig, not ntk]

Description []

SideEffects []

SeeAlso []

Definition at line 3632 of file puresatIPUtil.c.

{
  bAig_Manager_t *manager;
  st_table * node2MvfAigTable,*tmpTable;
  array_t * nameArray,*nameArray1;
  bAigTimeFrame_t *tf;
  char * name;
  Ntk_Node_t *latch;
  MvfAig_Function_t *mvfAig;
  mAigMvar_t lmVar;
  mAigBvar_t bVar;
  array_t *bVarList,*mVarList;
  int i,j,lmAigId;
  long index,index1;
  bAigEdge_t v, *li, *bli;

  manager = Ntk_NetworkReadMAigManager(network);
  if (manager == NIL(mAig_Manager_t)) {
    (void) fprintf(vis_stdout,
                   "** bmc error: run build_partition_maigs command first\n");
    exit(0);;
  }
  node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
                                    MVFAIG_NETWORK_APPL_KEY);
  tf = manager->timeframeWOI;

  bVarList = mAigReadBinVarList(manager);
  mVarList = mAigReadMulVarList(manager);

  assert(manager->timeframeWOI->currentTimeframe>=2);
  PureSat_CleanMask(manager,ResetVisitedMask);
  PureSat_CleanMask(manager,ResetVisited2Mask);
  PureSat_CleanMask(manager,ResetVisited3Mask);
  li = tf->latchInputs[1];
  for(i=0;i<tf->nLatches;i++)
    flags(li[i])|=Visited3Mask;
  li = tf->blatchInputs[1];
  for(i=0;i<tf->nbLatches;i++)
    flags(li[i])|=Visited3Mask;
  li = tf->latchInputs[2];
  for(i=0;i<tf->nLatches;i++)
    flags(li[i])|=Visited2Mask;
  li = tf->blatchInputs[2];
  for(i=0;i<tf->nbLatches;i++)
    flags(li[i])|=Visited2Mask;

  nameArray = array_alloc(char *,0);
  tmpTable = st_init_table(st_ptrcmp,st_ptrhash);
  PureSat_GetLatchForNode(manager,pm,property,nameArray,tmpTable,2);
  PureSat_CleanMask(manager,ResetVisitedMask);


  li = tf->latchInputs[2];
  bli = tf->blatchInputs[2];
  while(nameArray->num>0){
    nameArray1 = nameArray;
    nameArray = array_alloc(char *,0);
    arrayForEachItem(char*,nameArray1,i,name){
      latch = Ntk_NetworkFindNodeByName(network,name);
      st_lookup(node2MvfAigTable,latch,&mvfAig);
      for(j=0;j<mvfAig->num;j++){
        int retVal;
        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
        if(v==bAig_Zero||v==bAig_One)
          continue;
        retVal = st_lookup(tf->li2index,(char*)v,&index);
        assert(retVal);
        if(li[index]==bAig_Zero||li[index]==bAig_One)
          continue;
        PureSat_GetLatchForNode(manager,pm,li[index],nameArray,tmpTable,1);
      }


      lmAigId = Ntk_NodeReadMAigId(latch);
      lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
      for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
        int retVal;
        bVar = array_fetch(mAigBvar_t,bVarList,index1);
        if(bVar.node==bAig_Zero||bVar.node==bAig_One)
          continue;
        retVal = st_lookup(tf->bli2index,(char*)bVar.node,&index);
        assert(retVal);
        if(bli[index]==bAig_Zero||bli[index]==bAig_One)
          continue;
        PureSat_GetLatchForNode(manager,pm,bli[index],nameArray,tmpTable,1);
      }
    }

    array_free(nameArray1);
  }

  array_free(nameArray);
  PureSat_CleanMask(manager,ResetVisitedMask);
  PureSat_CleanMask(manager,ResetVisited2Mask);
  PureSat_CleanMask(manager,ResetVisited3Mask);

  return tmpTable;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatGetIndenticalLatch ( Ntk_Network_t *  network,
PureSat_Manager_t *  pm 
)

Function********************************************************************

Synopsis [Generate identical latch clusters]

Description []

SideEffects []

SeeAlso []

Definition at line 3825 of file puresatIPUtil.c.

{
  bAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  bAigEdge_t *li=tf->latchInputs[2],*bli = tf->blatchInputs[2];
  int i;
  bAigEdge_t v;
  st_table *table;
  st_generator *stgen,*stgen1;
  char *name,*name1;
  st_table *table2,*table1=st_init_table(st_ptrcmp,st_ptrhash);

  pm->IdenLatchTable = st_init_table(st_ptrcmp,st_ptrhash);

  for(i=0;i<tf->nLatches;i++){
    v=bAig_NonInvertedEdge(li[i]);
    if(!st_lookup(table1,(char*)v,NIL(char*))){
      if(st_lookup(tf->MultiLatchTable,(char*)v,&table)){
        int init=0;
        st_foreach_item(table,stgen,&name,NIL(char*)){
          if(!st_lookup(pm->IdenLatchTable,name,&table2)){
            st_insert(pm->IdenLatchTable,name,table);
            if(pm->verbosity>=2)
              fprintf(vis_stdout,"%s and ",name);
            init = 1;
          }
          /*insert everything in table 2 into table
          name is already in another group, put everything of current group
          into that group*/
          else{
            st_foreach_item(table,stgen1,&name1,NIL(char*)){
              st_insert(table2,name1,(char*)0);
              st_insert(pm->IdenLatchTable,name1,table2);
              if(pm->verbosity>=2)
                fprintf(vis_stdout,"%s and ",name1);
            }
            if(pm->verbosity>=2)
              fprintf(vis_stdout,"are the same\n");
            break;
          }
        }
        if(init){
          if(pm->verbosity>=2)
            fprintf(vis_stdout,"are the same\n");
        }
      }
      st_insert(table1,(char*)v,(char*)0);
    }
  }


  for(i=0;i<tf->nbLatches;i++){
    v=bAig_NonInvertedEdge(bli[i]);
    if(!st_lookup(table1,(char*)v,NIL(char*))){
      if(st_lookup(tf->MultiLatchTable,(char*)v,&table)){
        int init=0;
        st_foreach_item(table,stgen,&name,NIL(char*)){

          if(!st_lookup(pm->IdenLatchTable,name,table2)){
            st_insert(pm->IdenLatchTable,name,table);
            if(pm->verbosity>=2)
              fprintf(vis_stdout,"%s and ",name);
            init = 1;
          }
          /*insert everything in table 2 into table
          name is already in another group, put everything of current group
          into that group*/
          else{
            st_foreach_item(table,stgen1,&name1,NIL(char*)){

              st_insert(table2,name1,(char*)0);
              st_insert(pm->IdenLatchTable,name1,table2);
              if(pm->verbosity>=2)
                fprintf(vis_stdout,"%s and ",name1);
            }
            if(pm->verbosity>=2)
              fprintf(vis_stdout,"are the same\n");
            break;
          }
        }
        if(init){
          if(pm->verbosity>=2)
            fprintf(vis_stdout,"are the same\n");
        }
      }
      st_insert(table1,(char*)v,(char*)0);
    }
  }

  st_free_table(table1);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatKillPseudoGV ( Ntk_Network_t *  network,
PureSat_Manager_t *  pm,
st_table *  AbsTable,
int  from,
int  to 
)

Function********************************************************************

Synopsis [Kill all pseudo global variables for interpolation computation]

Description [Kill all pseudo global variables for interpolation computation]

SideEffects []

SeeAlso []

Definition at line 1013 of file puresatIPUtil.c.

{
  bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  bAigTimeFrame_t *tf = manager->timeframeWOI;
  array_t *bVarList,*mVarList;
  bAigEdge_t * li, *bli,node;
  int i,j;
  st_table * tmpTable, *DoneTable;


  pm->oldPos = manager->nodesArraySize-bAigNodeSize;

  bVarList = mAigReadBinVarList(manager);
  mVarList = mAigReadMulVarList(manager);

  if(from < 1)
    from = 1;

  if(to>pm->Length)
    to=pm->Length;

  li = tf->latchInputs[1];
  bli = tf->blatchInputs[1];
  for(j=0;j<tf->nLatches;j++)
    flags(li[j])&=ResetPGVMask;
  for(j=0;j<tf->nbLatches;j++)
    flags(bli[j])&=ResetPGVMask;

  for(i=from;i<=to;i++){
    li = tf->latchInputs[i];
    bli = tf->blatchInputs[i];
    manager->class_ = i;
    tmpTable = st_init_table(st_numcmp,st_numhash);
    DoneTable = st_init_table(st_numcmp,st_numhash);

    for(j=0; j<tf->nLatches; j++){
      node = bAig_NonInvertedEdge(li[j]);
      if(st_lookup(DoneTable,(char*)node,NIL(char*)))
        continue;
      st_insert(DoneTable,(char*)node,(char*)0);
      if((flags(node)&StateBitMask)&&
         !(flags(node)&VisibleVarMask)&&
         (flags(node)&CoiMask)){
        if(i==1)
          PureSatKillPseudoGVNode(manager,node,tmpTable);
        else
          PureSatAbstractLatch(manager,node,tmpTable);
      }
    }

    for(j=0; j<tf->nbLatches; j++){
      node = bAig_NonInvertedEdge(bli[j]);
      if(st_lookup(DoneTable,(char*)node,NIL(char*)))
        continue;
      st_insert(DoneTable,(char*)node,(char*)0);
      if((flags(node)&StateBitMask)&&
         !(flags(node)&VisibleVarMask)&&
         (flags(node)&CoiMask)){
        if(i==1)
          PureSatKillPseudoGVNode(manager,node,tmpTable);
        else
          PureSatAbstractLatch(manager,node,tmpTable);
      }
    }
    st_free_table(tmpTable);
    st_free_table(DoneTable);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatKillPseudoGVNode ( bAig_Manager_t *  manager,
bAigEdge_t  v,
st_table *  tmpTable 
)

Function********************************************************************

Synopsis [Kill all pseudo global variables for one node for interpolation computation]

Description [Kill all pseudo global variables for one node for interpolation computation]

SideEffects []

SeeAlso []

Definition at line 929 of file puresatIPUtil.c.

{
  long size = nFanout(v),i,inv=0;
  bAigEdge_t v1,v2,nv;
  bAigEdge_t  * fan = (bAigEdge_t *)fanout(v),left;

  /*fanin: set left and right to bAig_NULL*/
  nv = bAig_NonInvertedEdge(v);
  flags(nv) |= PGVMask;

  if(leftChild(nv)!=bAig_NULL){
    if(!(flags(leftChild(nv))&CoiMask))
      flags(leftChild(nv)) |= Visited3Mask;
    manager->NodesArray[nv+bAigLeft]=bAig_NULL;
  }

  if(rightChild(nv)!=bAig_NULL){
    if(!(flags(rightChild(nv))&CoiMask))
      flags(rightChild(nv)) |= Visited3Mask;
    manager->NodesArray[nv+bAigRight]=bAig_NULL;
  }


  manager->class_ = 2;

  /*fanout: connection to vars in next tf is disconnected, and a new pseudo var
    is created, and used as a replacement*/
  for(i=0;i<size;i++){
    v1 = bAig_NonInvertedEdge(fan[i]>>1);
    if(!(flags(v1)&CoiMask))
      continue;
    if(bAig_Class(v1)>1){
      /*igonre invSV since its left and right will be processed to 2*/
      if(!(flags(v1)&VisibleVarMask)&&(flags(v1)&StateBitMask))
        continue;
      /*if nonSV, create new Node as replacement*/
      if(!st_lookup(tmpTable,(char*)nv,&v2)){
        v2 = bAig_CreateNode(manager,bAig_NULL, bAig_NULL);

        flags(v2) |= DummyMask;
        st_insert(tmpTable,(char*)nv,(char*)v2);
      }

      left = 1;
      if(bAig_IsInverted(fan[i]))
        left = 0;
      inv = bAig_IsInverted(fan[i]>>1)?1:0;
      v2 = inv ? bAig_Not(v2) : v2;
      if(left){
#if DBG
        assert(manager->NodesArray[v1+bAigLeft] != v2);
#endif
        manager->NodesArray[v1+bAigLeft] = v2;
        PureSat_connectOutput(manager, v2, v1,0);
        flags(v2) |= CoiMask;
      }
      else{
#if DBG
        assert(manager->NodesArray[v1+bAigRight] != v2);
#endif
        manager->NodesArray[v1+bAigRight] = v2;
        PureSat_connectOutput(manager, v2, v1,1);
        flags(v2) |= CoiMask;
      }
    }
  }

}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatMarkObj ( bAig_Manager_t *  manager,
long  from,
long  to 
)

Function********************************************************************

Synopsis [Mark all node between from and to with obj mask]

Description []

SideEffects []

SeeAlso []

Definition at line 3002 of file puresatIPUtil.c.

{
  long v;

  for(v=from;v<=to;v+=bAigNodeSize)
    flags(v)|=ObjMask;
}

Here is the caller graph for this function:

void PuresatMarkVisibleVar ( Ntk_Network_t *  network,
array_t *  visibleArray,
PureSat_Manager_t *  pm,
int  from,
int  to 
)

Function********************************************************************

Synopsis [Mark visible latch variables]

Description []

SideEffects []

SeeAlso []

Definition at line 2555 of file puresatIPUtil.c.

{

  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
                                                         MVFAIG_NETWORK_APPL_KEY);
  MvfAig_Function_t *mvfAig;
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  mAigMvar_t lmVar;
  mAigBvar_t bVar;
  array_t *bVarList,*mVarList;
  int i,j,k,lmAigId,index,index1;
  char * name;
  Ntk_Node_t * latch;
  bAigEdge_t node,v, *li, *bli;

  bVarList = mAigReadBinVarList(manager);
  mVarList = mAigReadMulVarList(manager);


  if(from<0)
    from=0;
  if(to>pm->Length+1)
    to=pm->Length+1;

  for(i=from;i<=to;i++){
    li = tf->latchInputs[i];
    bli = tf->blatchInputs[i];
    arrayForEachItem(char *,visibleArray,k,name){
      latch = Ntk_NetworkFindNodeByName(network,name);
      st_lookup(node2MvfAigTable,latch,&mvfAig);
      /*multi val var*/
      for(j=0;j<mvfAig->num;j++){
        int retVal;
        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
        if(v==bAig_Zero||v==bAig_One)
          continue;
        retVal = st_lookup(tf->li2index,(char*)v,&index);
        assert(retVal);
        if(li[index]==bAig_Zero||li[index]==bAig_One)
          continue;
        node = bAig_NonInvertedEdge(li[index]);
        manager->NodesArray[node+bAigFlags] |= VisibleVarMask;
      }

      /*binary var*/
      lmAigId = Ntk_NodeReadMAigId(latch);
      lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
      for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
        int retVal;
        bVar = array_fetch(mAigBvar_t,bVarList,index1);
        if(bVar.node==bAig_Zero||bVar.node==bAig_One)
          continue;
        retVal = st_lookup(tf->bli2index,(char*)bVar.node,&index);
        assert(retVal);
        if(bli[index]==bAig_Zero||bli[index]==bAig_One)
          continue;
        node = bAig_NonInvertedEdge(bli[index]);
        manager->NodesArray[node+bAigFlags] |= VisibleVarMask;
      }
    }// arrayForEachItem(char *,visibleArray,k,name)
  }

  return;

}

Here is the call graph for this function:

Here is the caller graph for this function:

void PuresatMarkVisibleVarWithVPGV ( Ntk_Network_t *  network,
array_t *  visibleArray,
PureSat_Manager_t *  pm,
int  from,
int  to 
)

Function********************************************************************

Synopsis [Mark visible variable and also mark visible pseudo global variable]

Description []

SideEffects []

SeeAlso []

Definition at line 2452 of file puresatIPUtil.c.

{

  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
                                                         MVFAIG_NETWORK_APPL_KEY);
  MvfAig_Function_t *mvfAig;
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  mAigMvar_t lmVar;
  mAigBvar_t bVar;
  array_t *bVarList,*mVarList;
  int i,j,k,lmAigId,index,index1;
  char * name;
  Ntk_Node_t * latch;
  bAigEdge_t node,v, *li, *bli;

  bVarList = mAigReadBinVarList(manager);
  mVarList = mAigReadMulVarList(manager);

  /*Although some SV in tf 0 are not marked as visiblevar,
    //they actually visible since all SV of tf 0 are visible*/
  if(from<0)
    from=0;
  if(to>pm->Length+1)
    to=pm->Length+1;

  /*clean VPGV mask*/
  li = tf->latchInputs[1];
  bli = tf->blatchInputs[1];
  for(j=0;j<tf->nLatches;j++)
    flags(li[j])&=ResetVPGVMask;
  for(j=0;j<tf->nbLatches;j++)
    flags(bli[j])&=ResetVPGVMask;

  for(i=from;i<=to;i++){
    li = tf->latchInputs[i];
    bli = tf->blatchInputs[i];
    arrayForEachItem(char *,visibleArray,k,name){
      int retVal;
      latch = Ntk_NetworkFindNodeByName(network,name);
      st_lookup(node2MvfAigTable,latch,&mvfAig);
      for(j=0;j<mvfAig->num;j++){
        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
        if(v==bAig_Zero||v==bAig_One)
          continue;
        retVal = st_lookup(tf->li2index,(char*)v,&index);
        assert(retVal);
        if(li[index]==bAig_Zero||li[index]==bAig_One)
          continue;
        node = bAig_NonInvertedEdge(li[index]);
        manager->NodesArray[node+bAigFlags] |= VisibleVarMask;
        /*marking PGV*/
        if(i==1){
          if(!st_lookup(pm->vertexTable,name,NIL(char*))){
            flags(node) |= VPGVMask;

          }
        }
      }


      lmAigId = Ntk_NodeReadMAigId(latch);
      lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
      for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
        int retVal;
        bVar = array_fetch(mAigBvar_t,bVarList,index1);
        if(bVar.node==bAig_Zero||bVar.node==bAig_One)
          continue;
        retVal = st_lookup(tf->bli2index,(char*)bVar.node,&index);
        assert(retVal);
        if(bli[index]==bAig_Zero||bli[index]==bAig_One)
          continue;
        node = bAig_NonInvertedEdge(bli[index]);
        manager->NodesArray[node+bAigFlags] |= VisibleVarMask;
        /*marking PGV*/
        if(i==1){
          if(!st_lookup(pm->vertexTable,name,NIL(char*)))
            flags(node) |= VPGVMask;
        }
      }
    }
  }
  return;

}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatPostprocess ( bAig_Manager_t *  manager,
satManager_t *  cm,
PureSat_Manager_t *  pm 
)

Function********************************************************************

Synopsis [Recovery step after SAT solving]

Description [Recovery step after SAT solving]

SideEffects []

SeeAlso []

Definition at line 1774 of file puresatIPUtil.c.

{

  PureSatRecoverFanout(cm,pm);
  PureSat_RestoreAigForDummyNode(manager,pm->oldPos);
  PureSat_CleanMask(manager,ResetVisited3Mask);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatPreprocess ( Ntk_Network_t *  network,
satManager_t *  cm,
PureSat_Manager_t *  pm,
st_table *  vertexTable,
int  Length 
)

Function********************************************************************

Synopsis [Preprocess to form SAT instances]

Description [Preprocess to form SAT instances]

SideEffects []

SeeAlso []

Definition at line 1744 of file puresatIPUtil.c.

{
  bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);

  PureSatSetCOI(network,pm,cm,vertexTable,0, Length,Length);
  /*for interpolation*/
  PureSatKillPseudoGV(network,pm,vertexTable,1,Length);
  PureSat_ResetManager(manager,cm,0);
  /*for abstraction*/
  PureSatProcessFanout(cm);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatPreProcLatch ( Ntk_Network_t *  network,
PureSat_Manager_t *  pm 
)

Function********************************************************************

Synopsis [There are some latches whose DI is empty, put them into abstraction will not add any burden to model checker]

Description []

SideEffects []

SeeAlso []

Definition at line 3748 of file puresatIPUtil.c.

{
  st_generator * stgen;
  bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
                                                         MVFAIG_NETWORK_APPL_KEY);
  bAigTimeFrame_t * tf = manager->timeframeWOI;
  mAigMvar_t lmVar;
  mAigBvar_t bVar;
  array_t *bVarList,*mVarList;
  int j,lmAigId,id,index1;
  char * name;
  Ntk_Node_t * latch;
  bAigEdge_t v, **li, **bli;
  MvfAig_Function_t *mvfAig;

  bVarList = mAigReadBinVarList(manager);
  mVarList = mAigReadMulVarList(manager);
  li = tf->latchInputs;
  bli = tf->blatchInputs;

  st_foreach_item(pm->CoiTable,stgen,&latch,NIL(char*)){
    int checkbin=1;
    st_lookup(node2MvfAigTable,latch,&mvfAig);
    for(j=0;j<mvfAig->num;j++){
      int retVal;
      v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
      if(v==bAig_Zero||v==bAig_One)
        continue;
      retVal = st_lookup(tf->li2index,(char*)v,&id);
      assert(retVal);
      if(li[0][id]==li[1][id]&&li[1][id]==li[2][id]){
        name = Ntk_NodeReadName(latch);
        st_insert(pm->vertexTable,name,(char*)0);
        if(pm->verbosity>=2)
          fprintf(vis_stdout,"preproc: add %s to abs\n",name);
        checkbin = 0;
        break;
      }
    }
    if(checkbin){
      lmAigId = Ntk_NodeReadMAigId(latch);
      lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
      for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
        int retVal;
        bVar = array_fetch(mAigBvar_t,bVarList,index1);
        if(bVar.node==bAig_Zero||bVar.node==bAig_One)
          continue;
        retVal = st_lookup(tf->bli2index,(char*)bVar.node,&id);
        assert(retVal);
        if(bli[0][id]==bli[1][id]&&bli[1][id]==bli[2][id]){
          name = Ntk_NodeReadName(latch);
          st_insert(pm->vertexTable,name,(char*)0);
          if(pm->verbosity>=2)
            fprintf(vis_stdout,"preproc BINARY: add %s to abs\n",name);
          break;
        }
      }
    }
  }

}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatProcessDummy ( bAig_Manager_t *  manager,
satManager_t *  cm,
RTnode_t  RTnode 
)

Function********************************************************************

Synopsis [process dummy nodes]

Description [In UNSAT core, there may be dummy nodes, but in manager, they don't exist any more. This funct is to mark them]

SideEffects []

SeeAlso []

Definition at line 2748 of file puresatIPUtil.c.

{
  int i;
  bAigEdge_t *lp,node;
  RTManager_t *rm = cm->rm;

  if(RT_flag(RTnode)&RT_VisitedMask){
    return;
  }
  RT_flag(RTnode) |= RT_VisitedMask;

  if(RT_pivot(RTnode)==0){ /*leaf*/
#if DBG
    assert(RT_oriClsIdx(RTnode)==0);
#endif
    if(RT_oriClsIdx(RTnode))
      lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode));
    else

      lp = RT_formula(RTnode) + cm->rm->fArray;
    for(i=0;i<RT_fSize(RTnode);i++,lp++){
      assert(*lp>0);/* not processed yet*/
      if(RT_oriClsIdx(RTnode))/*is CNF*/
        node = SATgetNode(*lp);
      else /*is AIG*/
        node = *lp;
      node = SATnormalNode(node);
      if(node>=manager->nodesArraySize){
#if DBG
        assert(flags(node)&DummyMask);
#endif
        *lp = DUMMY;
      }
    }
  } /*leaf*/

  /*not leaf*/
  else{
    if(RT_pivot(RTnode)>=manager->nodesArraySize){
      int class_ = bAig_Class(RT_pivot(RTnode));
      RT_pivot(RTnode) = DUMMY+class_;
    }
    PureSatProcessDummy(manager,cm,RT_left(RTnode));
    PureSatProcessDummy(manager,cm,RT_right(RTnode));
  }

  return ;

}

Here is the caller graph for this function:

void PureSatProcessFanout ( satManager_t *  cm)

Function********************************************************************

Synopsis [Process fanout nodes to generate abstraction]

Description [Process fanout nodes to generate abstraction]

SideEffects []

SeeAlso []

Definition at line 1374 of file puresatIPUtil.c.

{

long bufSize, bufIndex;
bAigEdge_t *buf,left,right,*fan,v,cur;
int i, j;
long size, tsize;

int InvStateVar,l;


  bufSize = 1024;
  bufIndex = 0;
  buf = malloc(sizeof(bAigEdge_t) * bufSize);
  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    v = i;

    if(!(SATflags(v) & CoiMask))
      continue;

    InvStateVar = 0;
    if((SATflags(v)&StateBitMask)&&
       !(SATflags(v)&VisibleVarMask))
      InvStateVar = 1;

    size = SATnFanout(v);
    if(size >= bufSize) {
      bufSize <<= 1;
      if(size >= bufSize)
        bufSize = size + 1;
      buf = realloc(buf, sizeof(bAigEdge_t) * bufSize);
    }

    bufIndex = 0;
    for(j=0, fan = SATfanout(v); j<size; j++) {
      cur = fan[j];
      cur >>= 1;
      cur = SATnormalNode(cur);
      /*Not in COI , pass */
      if(!(SATflags(cur) & CoiMask))
        continue;
      /*cur is invisible var*/
      left = SATleftChild(cur);
      right = SATrightChild(cur);
      if(left==bAig_NULL||right==bAig_NULL){
#if DBG

        assert(left==bAig_NULL&&right==bAig_NULL);
        assert((SATflags(cur)&StateBitMask)&&
               !(SATflags(cur)&VisibleVarMask));
#endif
        continue;
      }
      /*v itself is InvStateVar and cur is not InvSV*/

      if(SATflags(v)&PGVMask){

         if(SATclass(cur)>=2){
          l = SATisInverted(fan[j]) ? 0 : 1;
          if(l){
#if DBG
            bAigEdge_t v1 = SATnormalNode(SATleftChild(cur));
            assert(v1!=v);
            assert(SATflags(v1)&DummyMask);
#endif
          }
          else{
#if DBG
            bAigEdge_t v1 = SATnormalNode(SATrightChild(cur));
            assert(v1!=v);
            assert(SATflags(v1)&DummyMask);
#endif
          }
          continue;
        }
      }
      buf[bufIndex++] = fan[j];
    }

    if(bufIndex > 0) {
      tsize = bufIndex;
      for(j=0, fan=SATfanout(v); j<size; j++) {
        cur = fan[j];
        cur >>= 1;
        cur = SATnormalNode(cur);
        if(!(SATflags(cur) & CoiMask))  {
          buf[bufIndex++] = fan[j];
          continue;
        }

        left = SATleftChild(cur);
        right = SATrightChild(cur);

        if(left==bAig_NULL||right==bAig_NULL){
          buf[bufIndex++] = fan[j];
          continue;
        }


        if(SATflags(v)&PGVMask){
          if(SATclass(cur)>=2){
            buf[bufIndex++] = fan[j];
            continue;
          }
        }

      }/*for(j=0, fan=SATfanout(v); j<size; j++) {*/
      buf[bufIndex] = 0;
      memcpy(fan, buf, sizeof(bAigEdge_t)*(size+1));
      SATnFanout(v) = tsize;
    }
    else
      SATnFanout(v) = 0;
  }

  free(buf);

  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
    v = i;
    if(!(SATflags(v) & CoiMask))
      continue;
    fan = SATfanout(v);
    size = SATnFanout(v);
    qsort(fan, size, sizeof(bAigEdge_t), NodeIndexCompare);
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatRecoverFanout ( satManager_t *  cm,
PureSat_Manager_t *  pm 
)

Function********************************************************************

Synopsis [Recover fanout of nodes]

Description [Recover fanout of nodes]

SideEffects []

SeeAlso []

Definition at line 1635 of file puresatIPUtil.c.

{
  bAigEdge_t i, v;

  /*dummy node can't be recovered*/
  for(i=satNodeSize; i<=pm->oldPos; i+=satNodeSize) {
    v = i;
    if(SATflags(v) & IsCNFMask)
      continue;

    if((SATflags(v)&CoiMask)){
       SATnFanout(v) = PureSatRecoverFanoutNode(cm, v);
       continue;
    }
    /*for some node not in coi, but a child of one coi(ISV) node*/
    if(SATflags(v)&Visited3Mask){
      PureSatRecoverISVNode(cm,v);
      continue;
    }
  }

}

Here is the call graph for this function:

Here is the caller graph for this function:

long PureSatRecoverFanoutNode ( satManager_t *  cm,
bAigEdge_t  v 
)

Function********************************************************************

Synopsis [Recover from abstractions]

Description [Recover from abstractions]

SideEffects []

SeeAlso []

Definition at line 1512 of file puresatIPUtil.c.

{
  bAigEdge_t *fan,nfan,child,cur;
  long i;
  int left,inver;
  int InvStateVar = 0;

  if(!(SATflags(v)&VisibleVarMask)&&(SATflags(v)&StateBitMask))
    InvStateVar = 1;

  nfan = SATnFanout(v);

  fan = SATfanout(v);
  if(fan == 0)  return(0);

  /*recover left and right children for latch nodes*/

  for(i=nfan; fan[i]!=0; i++){
    cur = fan[i];
    if(!(SATflags(SATnormalNode(cur>>1))&CoiMask))
      continue;
    /*cur is InvSV*/
    if((SATleftChild(SATnormalNode(cur>>1))==bAig_NULL)||
       (SATrightChild(SATnormalNode(cur>>1))==bAig_NULL)){
#if DBG
      assert((SATflags(SATnormalNode(cur>>1))&StateBitMask)&&
             !(SATflags(SATnormalNode(cur>>1))&VisibleVarMask));
#endif
      left = 1;
      inver = 0;
      if(SATisInverted(cur))
        left = 0;
      cur >>= 1;
      if(SATisInverted(cur))
        inver = 1;
      cur = SATnormalNode(cur);
      child = inver? SATnormalNode(v)+1:SATnormalNode(v);
      if(left)
        SATleftChild(cur)=child;
      else
        SATrightChild(cur)=child;
      continue;
    }

    /*v is InvSV, cur is not InvSV*/

    if(SATflags(v)&PGVMask){

      if(SATclass(SATnormalNode(cur>>1))>=2){
        left = 1;
        inver = 0;
        if(SATisInverted(cur))
          left = 0;
        cur >>= 1;
        if(SATisInverted(cur))
          inver = 1;
        cur = SATnormalNode(cur);
        child = inver? SATnormalNode(v)+1:SATnormalNode(v);
        if(left)
          SATleftChild(cur)=child;
        else
          SATrightChild(cur)=child;
      }
    }
  }
  //recover all fanout
  return(i);
}

Here is the caller graph for this function:

void PureSatRecoverISVNode ( satManager_t *  cm,
bAigEdge_t  v 
)

Function********************************************************************

Synopsis [Recover invisible state variable node]

Description [Recover invisible state variable node]

SideEffects []

SeeAlso []

Definition at line 1594 of file puresatIPUtil.c.

{

  bAigEdge_t size = SATnFanout(v),cur,node,child;
  bAigEdge_t  * fan = SATfanout(v);
  int inv,i,left;

  for(i=0;i<size;i++){
    cur = fan[i]>>1;
    node = SATnormalNode(cur);
    /*not in coi*/
    if(!(SATflags(node)&CoiMask))
      continue;
    /*not invisible var*/
    if(!((SATflags(node)&StateBitMask)&&
         !(SATflags(node)&VisibleVarMask)))
      continue;

    left=SATisInverted(fan[i])?0:1;
    inv=SATisInverted(cur)?1:0;
    child = inv?SATnormalNode(v)+1:SATnormalNode(v);
    if(left)
      SATleftChild(node) = child;
    else
      SATrightChild(node) = child;
  }
}

Here is the caller graph for this function:

void PureSatSetCOI ( Ntk_Network_t *  network,
PureSat_Manager_t *  pm,
satManager_t *  cm,
st_table *  AbsTable,
int  from,
int  to,
int  bound 
)

Function********************************************************************

Synopsis [Set COI for form the SAT problem]

Description [Set COI for form the SAT problem]

SideEffects []

SeeAlso []

Definition at line 859 of file puresatIPUtil.c.

{
  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  bAigEdge_t property;

  if(cm->obj->num>0){
    property = cm->obj->space[0];
    PureSatSetLatchCOI2(network,pm,cm,property,bound);
  }
  else{
    PureSatSetLatchCOI(network,pm,cm,AbsTable,from,to);
    PureSat_CleanMask(manager,ResetVisited3Mask);
  }


}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatSetLatchCOI ( Ntk_Network_t *  network,
PureSat_Manager_t *  pm,
satManager_t *  cm,
st_table *  AbsTable,
int  from,
int  to 
)

Function********************************************************************

Synopsis [Set COI for latch nodes]

Description [Set COI for latch nodes]

SideEffects []

SeeAlso []

Definition at line 754 of file puresatIPUtil.c.

{

  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);

  bAigTimeFrame_t *tf = manager->timeframeWOI;
  int i,j;
  bAigEdge_t *L0,*L1,*bL0,*bL1;
  satArray_t * assert;
  int nLatches = tf->nLatches, nbLatches = tf->nbLatches;

  if(from>=to) return;

  PureSat_ResetCoi(cm);

  assert = sat_ArrayAlloc(1);
  sat_ArrayInsert(assert,manager->InitState);
  PureSat_MarkTransitiveFaninForArray3(manager,assert,CoiMask);
  sat_ArrayFree(assert);

  for(i=from; i<to; i++){
    assert = sat_ArrayAlloc(1);

    L0 = tf->latchInputs[i];
    L1 = tf->latchInputs[i+1];
    bL0 = tf->blatchInputs[i];
    bL1 = tf->blatchInputs[i+1];

    for(j=0;j<nLatches;j++){
      if(L1[j]!=bAig_One&&L1[j]!=bAig_Zero){
        if(flags(L1[j])&VisibleVarMask)
          sat_ArrayInsert(assert,L1[j]);
      }
      if(L0[j]!=bAig_One&&L0[j]!=bAig_Zero&&
         !(flags(L0[j])&VisibleVarMask))
        flags(L0[j]) |= Visited3Mask;
    }

    for(j=0;j<nbLatches;j++){
      if(bL1[j]!=bAig_One&&bL1[j]!=bAig_Zero){
        if(flags(bL1[j])&VisibleVarMask)
          sat_ArrayInsert(assert,bL1[j]);
      }
      if(bL0[j]!=bAig_One&&bL0[j]!=bAig_Zero&&
         !(flags(bL0[j])&VisibleVarMask))
        flags(bL0[j]) |= Visited3Mask;
    }

    PureSat_MarkTransitiveFaninForArray2(manager,assert,CoiMask);
    sat_ArrayFree(assert);
  }

}

Here is the call graph for this function:

Here is the caller graph for this function:

void PureSatSetLatchCOI2 ( Ntk_Network_t *  network,
PureSat_Manager_t *  pm,
satManager_t *  cm,
bAigEdge_t  obj,
int  bound 
)

Function********************************************************************

Synopsis [Set COI for latch nodes]

Description [Set COI for latch nodes]

SideEffects []

SeeAlso []

Definition at line 827 of file puresatIPUtil.c.

{

  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  satArray_t * assert;

  PureSat_ResetCoi(cm);

  assert = sat_ArrayAlloc(1);
  sat_ArrayInsert(assert,obj);
  PureSat_MarkTransitiveFaninForArray4(manager,assert,CoiMask,bound);
  PureSat_MarkTransitiveFaninForArray4(manager,cm->assertArray,CoiMask,bound);
  sat_ArrayFree(assert);

}

Here is the call graph for this function:

Here is the caller graph for this function:

RTnode_t RTCreateNode ( RTManager_t *  rm)

AutomaticEnd Function********************************************************************

Synopsis [Create a node for resolution tree]

Description [Create a node for resolution tree]

SideEffects []

SeeAlso []

Definition at line 173 of file puresatIPUtil.c.

{
  RTnode_t node;

  if(rm->nArray==0){
    rm->nArray = ALLOC(long, RTnodeSize*RT_BLOCK);
    rm->maxSize = RTnodeSize*RT_BLOCK;
    rm->aSize = 0;
  }

  if(rm->maxSize<=rm->aSize+RTnodeSize){
    rm->nArray = REALLOC(long, rm->nArray,rm->maxSize+RTnodeSize*RT_BLOCK);
    if(rm->nArray == 0){
      fprintf(vis_stdout,"memout when alloc %ld bytes\n",
             (rm->maxSize+RTnodeSize*RT_BLOCK)*4);
      exit(0);
    }
    rm->maxSize = rm->maxSize+RTnodeSize*1000;
  }
  rm->aSize += RTnodeSize;
  node = rm->aSize;

  RT_fSize(node) = 0;
  RT_formula(node) = 0;
  RT_oriClsIdx(node) = 0;
  RT_pivot(node) = 0;
  RT_flag(node) = 0;
  RT_IPnode(node) = -1;
  RT_left(node) = 0;
  RT_right(node) = 0;

  if(rm->fArray==0){
    rm->fArray = ALLOC(long,FORMULA_BLOCK);

    rm->cpos = 0;
    rm->maxpos = FORMULA_BLOCK;
  }

  return node;
}

Here is the caller graph for this function:

static int StringCheckIsInteger ( char *  string,
int *  value 
) [static]

Function********************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 138 of file puresatIPUtil.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: