diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-04-11 22:12:18 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-04-11 22:12:18 -0700 |
| commit | b1eaf714f2a23eaee74efcafff9a40dd017bb00b (patch) | |
| tree | a3700bc7c5e73b6872f304ebfac4c7708c6ba94c /src/proof/cec | |
| parent | 79584f5e201e7388e30df39e6f8fc9b50f34b834 (diff) | |
| download | abc-b1eaf714f2a23eaee74efcafff9a40dd017bb00b.tar.gz abc-b1eaf714f2a23eaee74efcafff9a40dd017bb00b.tar.bz2 abc-b1eaf714f2a23eaee74efcafff9a40dd017bb00b.zip | |
Experiments with SAT sweeping.
Diffstat (limited to 'src/proof/cec')
| -rw-r--r-- | src/proof/cec/cec.h | 1 | ||||
| -rw-r--r-- | src/proof/cec/cecCore.c | 1 | ||||
| -rw-r--r-- | src/proof/cec/cecSat.c | 7 |
3 files changed, 8 insertions, 1 deletions
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index e8b243d3..cb4ff27f 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -108,6 +108,7 @@ struct Cec_ParFra_t_ int fColorDiff; // miter with separate outputs int fSatSweeping; // enable SAT sweeping int fRunCSat; // enable another solver + int fUseCones; // use cones int fUseOrigIds; // enable recording of original IDs int fVeryVerbose; // verbose stats int fVerbose; // verbose stats diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c index ed5c4ab7..ccc5a8e6 100644 --- a/src/proof/cec/cecCore.c +++ b/src/proof/cec/cecCore.c @@ -138,6 +138,7 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p ) p->fDualOut = 0; // miter with separate outputs p->fColorDiff = 0; // miter with separate outputs p->fSatSweeping = 0; // enable SAT sweeping + p->fUseCones = 0; // use cones p->fVeryVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats p->iOutFail = -1; // the failed output diff --git a/src/proof/cec/cecSat.c b/src/proof/cec/cecSat.c index fc53d503..c32ed7f9 100644 --- a/src/proof/cec/cecSat.c +++ b/src/proof/cec/cecSat.c @@ -101,7 +101,7 @@ void Cec2_SetDefaultParams( Cec2_Par_t * p ) p->nItersMax = 10; // max number of iterations p->nConfLimit = 1000; // conflict limit at a node p->fIsMiter = 0; // this is a miter - p->fUseCones = 0; // use logic cones + p->fUseCones = 1; // use logic cones p->fVeryVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats } @@ -968,7 +968,11 @@ int Cec2_ManPerformSweeping( Gia_Man_t * p, Cec2_Par_t * pPars, Gia_Man_t ** ppN continue; } if ( Cec2_ManSweepNode(pMan, i) ) + { + if ( Gia_ObjProved(p, i) ) + pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase ); continue; + } pObj->Value = ~0; Vec_IntPushThree( pMan->vCexTriples, Gia_ObjId(p, pRepr), i, Abc_Var2Lit(p->iPatsPi, pObj->fPhase ^ pRepr->fPhase) ); fDisproved = 1; @@ -1011,6 +1015,7 @@ Gia_Man_t * Cec2_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars0 ) // pPars->nSimRounds = pPars0->nRounds; // simulation rounds // pPars->nItersMax = pPars0->nItersMax; // max number of iterations pPars->nConfLimit = pPars0->nBTLimit; // conflict limit at a node + pPars->fUseCones = pPars0->fUseCones; pPars->fVerbose = pPars0->fVerbose; // Gia_ManComputeGiaEquivs( p, 100000, 0 ); // Gia_ManEquivPrintClasses( p, 1, 0 ); |