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/cecInt.h | |
| 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/cecInt.h')
| -rw-r--r-- | src/proof/cec/cecInt.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/proof/cec/cecInt.h b/src/proof/cec/cecInt.h index 80663db9..f78e5f25 100644 --- a/src/proof/cec/cecInt.h +++ b/src/proof/cec/cecInt.h @@ -27,6 +27,7 @@ //////////////////////////////////////////////////////////////////////// #include "sat/bsat/satSolver.h" +#include "sat/glucose2/AbcGlucose2.h" #include "misc/bar/bar.h" #include "aig/gia/gia.h" #include "cec.h" @@ -80,7 +81,8 @@ struct Cec_ManSat_t_ Gia_Man_t * pAig; // the AIG whose outputs are considered Vec_Int_t * vStatus; // status for each output // SAT solving - sat_solver * pSat; // recyclable SAT solver + sat_solver * pSat; // recyclable SAT solver (MiniSAT) + bmcg2_sat_solver*pSat2; // recyclable SAT solver (Glucose) int nSatVars; // the counter of SAT variables int * pSatVars; // mapping of each node into its SAT var Vec_Ptr_t * vUsedNodes; // nodes whose SAT vars are assigned @@ -212,6 +214,8 @@ extern int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * p extern int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 ); extern void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 ); extern Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * p ); +/*=== cecSolveG.c ============================================================*/ +extern void CecG_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int f0Proved ); /*=== ceFraeep.c ============================================================*/ extern Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p ); extern int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew ); |