diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-12-04 16:10:11 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-12-04 16:10:11 -0800 |
commit | 09d3e1ff77e656976268fa27b6045ff6f284fd3b (patch) | |
tree | 8fd52c0920fe3a46f7599fdee2b745d24b94320d /src/sat/bsat/satSolver2.h | |
parent | a7031bb3f76385b014af0e329e5313b531cf2d72 (diff) | |
download | abc-09d3e1ff77e656976268fa27b6045ff6f284fd3b.tar.gz abc-09d3e1ff77e656976268fa27b6045ff6f284fd3b.tar.bz2 abc-09d3e1ff77e656976268fa27b6045ff6f284fd3b.zip |
Proof-logging in the updated solver.
Diffstat (limited to 'src/sat/bsat/satSolver2.h')
-rw-r--r-- | src/sat/bsat/satSolver2.h | 31 |
1 files changed, 21 insertions, 10 deletions
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index a5ed85b3..937972a6 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -32,7 +32,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA ABC_NAMESPACE_HEADER_START - +//#define USE_FLOAT_ACTIVITY //================================================================================================= // Public interface: @@ -70,9 +70,6 @@ extern void * sat_solver2_store_release( sat_solver2 * s ); //================================================================================================= // Solver representation: -//struct clause_t; -//typedef struct clause_t clause; - struct varinfo_t; typedef struct varinfo_t varinfo; @@ -91,21 +88,26 @@ struct sat_solver2_t int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything int fNotUseRandom; // do not allow random decisions with a fixed probability // int fSkipSimplify; // set to one to skip simplification of the clause database + int fProofLogging; // enable proof-logging // clauses + veci clauses; // clause memory + veci* wlists; // watcher lists (for each literal) int iLearnt; // the first learnt clause int iLast; // the last learnt clause - veci* wlists; // watcher lists (for each literal) - - // clause memory - int * pMemArray; - int nMemAlloc; - int nMemSize; // activities +#ifdef USE_FLOAT_ACTIVITY + double var_inc; // Amount to bump next variable with. + double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. + float cla_inc; // Amount to bump next clause with. + float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. + double* activity; // A heuristic measurement of the activity of a variable. +#else int var_inc; // Amount to bump next variable with. int cla_inc; // Amount to bump next clause with. unsigned* activity; // A heuristic measurement of the activity of a variable. +#endif veci claActs; // clause activities veci claProofs; // clause proofs @@ -123,6 +125,15 @@ struct sat_solver2_t veci model; // If problem is solved, this vector contains the model (contains: lbool). veci conf_final; // If problem is unsatisfiable (possibly under assumptions), // this vector represent the final conflict clause expressed in the assumptions. + veci mark_levels; // temporary storage for labeled levels + veci min_lit_order; // ordering of removable literals + veci min_step_order;// ordering of resolution steps + + // proof logging + veci proof_clas; // sequence of proof clauses + veci proof_vars; // sequence of proof variables + int iStartChain; // beginning of the chain + // statistics stats_t stats; ABC_INT64_T nConfLimit; // external limit on the number of conflicts |