diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-12-16 22:04:06 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-12-16 22:04:06 -0800 |
| commit | 73dcdab6d836440ae5edf6fd23f9a409f9e519c2 (patch) | |
| tree | 753131e555387b725ab39167446e744d0c6abcfd /src/proof/cec/cecCore.c | |
| parent | 8066fdbcb53f0e9ea617f24de1a73bc9f0cb69f6 (diff) | |
| download | abc-73dcdab6d836440ae5edf6fd23f9a409f9e519c2.tar.gz abc-73dcdab6d836440ae5edf6fd23f9a409f9e519c2.tar.bz2 abc-73dcdab6d836440ae5edf6fd23f9a409f9e519c2.zip | |
Adding solver type in &sat.
Diffstat (limited to 'src/proof/cec/cecCore.c')
| -rw-r--r-- | src/proof/cec/cecCore.c | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c index 4e8e5497..f94bd27f 100644 --- a/src/proof/cec/cecCore.c +++ b/src/proof/cec/cecCore.c @@ -45,6 +45,7 @@ ABC_NAMESPACE_IMPL_START void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ) { memset( p, 0, sizeof(Cec_ParSat_t) ); + p->SolverType = -1; // SAT solver type p->nBTLimit = 100; // conflict limit at a node p->nSatVarMax = 2000; // the max number of SAT variables p->nCallsRecycle = 200; // calls to perform before recycling SAT solver @@ -237,7 +238,10 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars, int f0Pro Gia_Man_t * pNew; Cec_ManPat_t * pPat; pPat = Cec_ManPatStart(); - Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL, f0Proved ); + if ( pPars->SolverType == -1 ) + Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL, f0Proved ); + else + CecG_ManSatSolve( pPat, pAig, pPars, f0Proved ); // pNew = Gia_ManDupDfsSkip( pAig ); pNew = Gia_ManCleanup( pAig ); Cec_ManPatStop( pPat ); |