diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-26 18:17:39 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-26 18:17:39 -0800 |
commit | fc4ab6bd39cfd4a83af8069902878c422e1e885e (patch) | |
tree | f69c22fb4064ab8f87b27cf1b776a386b417b1f8 /src/sat/bsat/satSolver2.h | |
parent | 0cfc97b9400f2d4ff814eb815a584bc6ffbfe1e6 (diff) | |
download | abc-fc4ab6bd39cfd4a83af8069902878c422e1e885e.tar.gz abc-fc4ab6bd39cfd4a83af8069902878c422e1e885e.tar.bz2 abc-fc4ab6bd39cfd4a83af8069902878c422e1e885e.zip |
Started experiments with a new solver.
Diffstat (limited to 'src/sat/bsat/satSolver2.h')
-rw-r--r-- | src/sat/bsat/satSolver2.h | 100 |
1 files changed, 45 insertions, 55 deletions
diff --git a/src/sat/bsat/satSolver2.h b/src/sat/bsat/satSolver2.h index dda7be7a..2725c92b 100644 --- a/src/sat/bsat/satSolver2.h +++ b/src/sat/bsat/satSolver2.h @@ -77,71 +77,61 @@ extern void * sat_solver2_store_release( sat_solver2 * s ); //struct clause_t; //typedef struct clause_t clause; +struct varinfo_t; +typedef struct varinfo_t varinfo; + struct sat_solver2_t { - int size; // nof variables - int cap; // size of varmaps - int qhead; // Head index of queue. - int qtail; // Tail index of queue. + int size; // nof variables + int cap; // size of varmaps + int qhead; // Head index of queue. + int qtail; // Tail index of queue. + + int root_level; // Level of first proper decision. + int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'. + int simpdb_props; // Number of propagations before next 'simplifyDB()'. + double random_seed; + double progress_estimate; + 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 // clauses - vecp clauses; // List of problem constraints. (contains: clause*) - vecp learnts; // List of learnt clauses. (contains: clause*) + int iLearnt; // the first learnt clause + int iLast; // the last learnt clause + veci* wlists; // watcher lists (for each literal) + cla* pWatches; // watcher lists (for each literal) - // activities -// double var_inc; // Amount to bump next variable with. -// double var_decay; // INVERSE decay factor for variable activity: stores 1/decay. - int var_inc; -// int var_decay; - -// float cla_inc; // Amount to bump next clause with. - int cla_inc; // Amount to bump next clause with. -// float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay. - - clause** pWatches; // watcher lists (for each literal) - vecp* wlists; // -// double* activity; // A heuristic measurement of the activity of a variable. - unsigned*activity; // A heuristic measurement of the activity of a variable. - lbool* assigns; // Current values of variables. - int* orderpos; // Index in variable order. - clause** reasons; // - int* levels; // - lit* trail; - char* polarity; - - clause* binary; // A temporary binary clause - lbool* tags; // - veci tagged; // (contains: var) - veci stack; // (contains: var) - - veci order; // Variable order. (heap) (contains: var) - veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) - 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. - - int root_level; // Level of first proper decision. - int simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'. - int simpdb_props; // Number of propagations before next 'simplifyDB()'. - double random_seed; - double progress_estimate; - int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything - - stats_t stats; + // clause memory + int * pMemArray; + int nMemAlloc; + int nMemSize; + // activities + 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. + + // internal state + varinfo * vi; // variable information + cla* reasons; + lit* trail; + int* orderpos; // Index in variable order. + + veci tagged; // (contains: var) + veci stack; // (contains: var) + veci order; // Variable order. (heap) (contains: var) + veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int) + veci temp_clause; // temporary storage for a CNF clause + 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. + // statistics + stats_t stats; ABC_INT64_T nConfLimit; // external limit on the number of conflicts ABC_INT64_T nInsLimit; // external limit on the number of implications int nRuntimeLimit; // external limit on runtime - // clause memory - int * pMemArray; - int nMemAlloc; - int nMemSize; - -// int fSkipSimplify; // set to one to skip simplification of the clause database - int fNotUseRandom; // do not allow random decisions with a fixed probability - - veci temp_clause; // temporary storage for a CNF clause }; static int sat_solver2_var_value( sat_solver2* s, int v ) |