diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-02 15:14:49 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-02 15:14:49 -0700 |
| commit | 9914c1686802ee507f52856943a22380c1b5d8c8 (patch) | |
| tree | faa1995e7d236681d15a204d9251ed243ab5d6ee /src/sat/bsat/satSolver2.h | |
| parent | 57b9a9fe130351f609bac0f63b57b7dbcbbc03c8 (diff) | |
| download | abc-9914c1686802ee507f52856943a22380c1b5d8c8.tar.gz abc-9914c1686802ee507f52856943a22380c1b5d8c8.tar.bz2 abc-9914c1686802ee507f52856943a22380c1b5d8c8.zip | |
Adding interpolant computation sat_solver2.
Diffstat (limited to 'src/sat/bsat/satSolver2.h')
| -rw-r--r-- | src/sat/bsat/satSolver2.h | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index d7d16d73..41dfc680 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -42,6 +42,7 @@ ABC_NAMESPACE_HEADER_START struct sat_solver2_t; typedef struct sat_solver2_t sat_solver2; +typedef struct Int2_Man_t_ Int2_Man_t; extern sat_solver2* sat_solver2_new(void); extern void sat_solver2_delete(sat_solver2* s); @@ -72,6 +73,14 @@ extern void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ); extern word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars ); extern void Sat_ProofCheck( sat_solver2 * s ); +// interpolation APIs +extern Int2_Man_t * Int2_ManStart( sat_solver2 * pSat, int * pGloVars, int nGloVars ); +extern void Int2_ManStop( Int2_Man_t * p ); +extern int Int2_ManChainStart( Int2_Man_t * p, clause * c ); +extern int Int2_ManChainResolve( Int2_Man_t * p, clause * c, int iLit, int varA ); +extern void * Int2_ManReadInterpolant( sat_solver2 * s ); + + //================================================================================================= // Solver representation: @@ -156,6 +165,8 @@ struct sat_solver2_t int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final) Prf_Man_t * pPrf2; // another proof manager double dPrfMemory; // memory used by the proof-logger + Int2_Man_t * pInt2; // interpolation manager + int tempInter; // temporary storage for the interpolant // statistics stats_t stats; |