diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.cc | 42 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 11 |
2 files changed, 28 insertions, 25 deletions
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index 698d2a776..9e50433ef 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -48,27 +48,27 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of //================================================================================================= // Constructor/Destructor: - -SimpSolver::SimpSolver(CVC4::context::Context* c) : - Solver(c) - , grow (opt_grow) - , clause_lim (opt_clause_lim) - , subsumption_lim (opt_subsumption_lim) - , simp_garbage_frac (opt_simp_garbage_frac) - , use_asymm (opt_use_asymm) - , use_rcheck (opt_use_rcheck) - , use_elim (opt_use_elim && - CVC4::options::bitblastMode() == CVC4::theory::bv::BITBLAST_MODE_EAGER && - !CVC4::options::produceModels()) - , merges (0) - , asymm_lits (0) - , eliminated_vars (0) - , elimorder (1) - , use_simplification (!PROOF_ON()) - , occurs (ClauseDeleted(ca)) - , elim_heap (ElimLt(n_occ)) - , bwdsub_assigns (0) - , n_touched (0) +SimpSolver::SimpSolver(CVC4::context::Context* c) + : Solver(c), + grow(opt_grow), + clause_lim(opt_clause_lim), + subsumption_lim(opt_subsumption_lim), + simp_garbage_frac(opt_simp_garbage_frac), + use_asymm(opt_use_asymm), + use_rcheck(opt_use_rcheck), + use_elim(opt_use_elim + && CVC4::options::bitblastMode() + == CVC4::options::BitblastMode::EAGER + && !CVC4::options::produceModels()), + merges(0), + asymm_lits(0), + eliminated_vars(0), + elimorder(1), + use_simplification(!PROOF_ON()), + occurs(ClauseDeleted(ca)), + elim_heap(ElimLt(n_occ)), + bwdsub_assigns(0), + n_touched(0) { vec<Lit> dummy(1,lit_Undef); diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 3cdd6b654..80d767b3d 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -106,15 +106,18 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory d_context = context; - if( options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL ) { + if (options::decisionMode() != options::DecisionMode::INTERNAL) + { Notice() << "minisat: Incremental solving is forced on (to avoid variable elimination)" << " unless using internal decision strategy." << std::endl; } // Create the solver - d_minisat = new Minisat::SimpSolver(theoryProxy, d_context, - options::incrementalSolving() || - options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL ); + d_minisat = new Minisat::SimpSolver( + theoryProxy, + d_context, + options::incrementalSolving() + || options::decisionMode() != options::DecisionMode::INTERNAL); d_statistics.init(d_minisat); } |