diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-08-19 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-08-19 08:01:00 -0700 |
| commit | c8a25de8e411409b60f3677f70eab0860070b462 (patch) | |
| tree | 1f5f57c35a3aab5563879ca31119316ac3bcf207 /src/aig/fra/fraSat.c | |
| parent | 3244fa2f327af3342194cbe74ec07fe198191837 (diff) | |
| download | abc-c8a25de8e411409b60f3677f70eab0860070b462.tar.gz abc-c8a25de8e411409b60f3677f70eab0860070b462.tar.bz2 abc-c8a25de8e411409b60f3677f70eab0860070b462.zip | |
Version abc70819
Diffstat (limited to 'src/aig/fra/fraSat.c')
| -rw-r--r-- | src/aig/fra/fraSat.c | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c index 417163d5..bc8ef08a 100644 --- a/src/aig/fra/fraSat.c +++ b/src/aig/fra/fraSat.c @@ -77,7 +77,7 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) } // if the nodes do not have SAT variables, allocate them - Fra_NodeAddToSolver( p, pOld, pNew ); + Fra_CnfNodeAddToSolver( p, pOld, pNew ); if ( p->pSat->qtail != p->pSat->qhead ) { @@ -113,7 +113,7 @@ p->timeSatUnsat += clock() - clk; else if ( RetValue1 == l_True ) { p->timeSatSat += clock() - clk; - Fra_SavePattern( p ); + Fra_SmlSavePattern( p ); p->nSatCallsSat++; return 0; } @@ -156,7 +156,7 @@ p->timeSatUnsat += clock() - clk; else if ( RetValue1 == l_True ) { p->timeSatSat += clock() - clk; - Fra_SavePattern( p ); + Fra_SmlSavePattern( p ); p->nSatCallsSat++; return 0; } @@ -234,7 +234,7 @@ int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fCom } // if the nodes do not have SAT variables, allocate them - Fra_NodeAddToSolver( p, pOld, pNew ); + Fra_CnfNodeAddToSolver( p, pOld, pNew ); if ( p->pSat->qtail != p->pSat->qhead ) { @@ -272,7 +272,7 @@ p->timeSatUnsat += clock() - clk; else if ( RetValue1 == l_True ) { p->timeSatSat += clock() - clk; - Fra_SavePattern( p ); + Fra_SmlSavePattern( p ); p->nSatCallsSat++; return 0; } @@ -320,7 +320,7 @@ int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ) } // if the nodes do not have SAT variables, allocate them - Fra_NodeAddToSolver( p, NULL, pNew ); + Fra_CnfNodeAddToSolver( p, NULL, pNew ); // prepare variable activity if ( p->pPars->fConeBias ) @@ -346,7 +346,7 @@ p->timeSatUnsat += clock() - clk; { p->timeSatSat += clock() - clk; if ( p->pPatWords ) - Fra_SavePattern( p ); + Fra_SmlSavePattern( p ); p->nSatCallsSat++; return 0; } |