diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-11 12:45:46 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-11 12:45:46 -0700 |
| commit | b9ee5d8564025acfbeb632cf3c28ecb8d61a7aa4 (patch) | |
| tree | 9e5e3e6aebf36d28cf3c7726ac7f5f7bcdd8a843 /src/sat/bsat/satSolver.h | |
| parent | 5f3ba152e5729824f78fd03e3d164de81a452d22 (diff) | |
| download | abc-b9ee5d8564025acfbeb632cf3c28ecb8d61a7aa4.tar.gz abc-b9ee5d8564025acfbeb632cf3c28ecb8d61a7aa4.tar.bz2 abc-b9ee5d8564025acfbeb632cf3c28ecb8d61a7aa4.zip | |
Improvements in the proof-logging SAT solver.
Diffstat (limited to 'src/sat/bsat/satSolver.h')
| -rw-r--r-- | src/sat/bsat/satSolver.h | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index 8998b78c..520e8284 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -28,8 +28,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <string.h> #include <assert.h> -#include "satClause.h" #include "satVec.h" +#include "satClause.h" #include "misc/vec/vecSet.h" ABC_NAMESPACE_HEADER_START @@ -98,6 +98,8 @@ struct sat_solver_t int hLearnts; // the first learnt clause int hBinary; // the special binary clause clause * binary; + veci* wlists; // watcher lists + veci act_clas; // contain clause activities // activities #ifdef USE_FLOAT_ACTIVITY @@ -112,7 +114,6 @@ struct sat_solver_t unsigned* activity; // A heuristic measurement of the activity of a variable. #endif - veci* wlists; // // varinfo * vi; // variable information int* levels; // char* assigns; // Current values of variables. @@ -141,13 +142,11 @@ struct sat_solver_t int fVerbose; stats_t stats; + int nLearntMax; // max number of learned clauses int nLearntStart; // starting learned clause limit int nLearntDelta; // delta of learned clause limit int nLearntRatio; // ratio percentage of learned clauses - int nLearntMax; // max number of learned clauses int nDBreduces; // number of DB reductions -// veci learned; // contain learnt clause handles - veci act_clas; // contain clause activities ABC_INT64_T nConfLimit; // external limit on the number of conflicts ABC_INT64_T nInsLimit; // external limit on the number of implications |