diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-11-06 16:43:32 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-11-06 16:43:32 -0800 |
| commit | 716969190a4d6d944cfa24a085c9e7069d868dab (patch) | |
| tree | 1a0a95bd9dfc505341c367752658c732900e55de /src/sat/glucose/AbcGlucose.h | |
| parent | 94a575a5b3113d714b96ba3711124c5780151bee (diff) | |
| download | abc-716969190a4d6d944cfa24a085c9e7069d868dab.tar.gz abc-716969190a4d6d944cfa24a085c9e7069d868dab.tar.bz2 abc-716969190a4d6d944cfa24a085c9e7069d868dab.zip | |
Profiling quantification and other changes.
Diffstat (limited to 'src/sat/glucose/AbcGlucose.h')
| -rw-r--r-- | src/sat/glucose/AbcGlucose.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h index e2c05e1b..1bf29aed 100644 --- a/src/sat/glucose/AbcGlucose.h +++ b/src/sat/glucose/AbcGlucose.h @@ -93,8 +93,9 @@ extern int bmcg_sat_solver_learntnum( bmcg_sat_solver* s ); extern int bmcg_sat_solver_conflictnum( bmcg_sat_solver* s ); extern int bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int nlits, int pivot ); extern int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl ); -extern int bmcg_sat_solver_quantify( bmcg_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData ); +extern int bmcg_sat_solver_quantify( bmcg_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits ); extern int bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv ); +extern Vec_Str_t * bmcg_sat_solver_sop( Gia_Man_t * p, int CubeLimit ); extern void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars ); extern int Glucose_SolveAig( Gia_Man_t * p, Glucose_Pars * pPars ); |