diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-01-21 08:01:00 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-01-21 08:01:00 -0800 |
| commit | 2167d6c148191f7aa65381bb0618b64050bf4de3 (patch) | |
| tree | 345f5cc859142b50f01d261073688e880e61b631 /src/aig/ivy | |
| parent | 76bcf6b25411e1b0d73e5dff6c8fd3e2f4bab9e1 (diff) | |
| download | abc-2167d6c148191f7aa65381bb0618b64050bf4de3.tar.gz abc-2167d6c148191f7aa65381bb0618b64050bf4de3.tar.bz2 abc-2167d6c148191f7aa65381bb0618b64050bf4de3.zip | |
Version abc70121
Diffstat (limited to 'src/aig/ivy')
| -rw-r--r-- | src/aig/ivy/ivyCut.c | 2 | ||||
| -rw-r--r-- | src/aig/ivy/ivyFraig.c | 15 |
2 files changed, 15 insertions, 2 deletions
diff --git a/src/aig/ivy/ivyCut.c b/src/aig/ivy/ivyCut.c index d918c96c..e257d8a6 100644 --- a/src/aig/ivy/ivyCut.c +++ b/src/aig/ivy/ivyCut.c @@ -930,6 +930,8 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves */ iLeaf0 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin0(pLeaf)) ); iLeaf1 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin1(pLeaf)) ); +// if ( iLeaf0 == iLeaf1 ) // strange situation observed on Jan 18, 2007 +// continue; if ( !Ivy_NodeCutPrescreen( pCut, iLeaf0, iLeaf1 ) ) continue; if ( iLeaf0 > iLeaf1 ) diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c index ce21c269..e9a65881 100644 --- a/src/aig/ivy/ivyFraig.c +++ b/src/aig/ivy/ivyFraig.c @@ -252,7 +252,7 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars ) Prove_Params_t * pParams = pPars; Ivy_FraigParams_t Params, * pIvyParams = &Params; Ivy_Man_t * pManAig, * pManTemp; - int RetValue, nIter, Counter, clk, timeStart = clock(); + int RetValue, nIter, clk, timeStart = clock();//, Counter; sint64 nSatConfs, nSatInspects; // start the network and parameters @@ -314,12 +314,14 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars ) // try rewriting if ( pParams->fUseRewriting ) - { + { // bug in Ivy_NodeFindCutsAll() when leaves are identical! +/* clk = clock(); Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter)); pManAig = Ivy_ManRwsat( pManAig, 0 ); RetValue = Ivy_FraigMiterStatus( pManAig ); Ivy_FraigMiterPrint( pManAig, "Rewriting ", clk, pParams->fVerbose ); +*/ } if ( RetValue >= 0 ) break; @@ -368,6 +370,15 @@ int Ivy_FraigProve( Ivy_Man_t ** ppManAig, void * pPars ) s_nInsLimitGlobal = 0; RetValue = Ivy_FraigMiterStatus( pManAig ); Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose ); + // make sure that the sover never returns "undecided" when infinite resource limits are set + if( RetValue == -1 && pParams->nTotalInspectLimit == 0 && + pParams->nTotalBacktrackLimit == 0 ) + { + extern void Prove_ParamsPrint( Prove_Params_t * pParams ); + Prove_ParamsPrint( pParams ); + printf("ERROR: ABC has returned \"undecided\" in spite of no limits...\n"); + exit(1); + } } // assign the model if it was proved by rewriting (const 1 miter) |