diff options
Diffstat (limited to 'src/prop/bvminisat/simp/SimpSolver.cc')
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.cc | 42 |
1 files changed, 21 insertions, 21 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); |