summaryrefslogtreecommitdiff
path: root/src/prop/bvminisat
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2019-12-17 13:43:44 -0800
committerGitHub <noreply@github.com>2019-12-17 13:43:44 -0800
commite9499c41f405df8b42fd9ae10004b1b91a869106 (patch)
treefa1475f43a3e61b8f6ffdcb903b65919eba28661 /src/prop/bvminisat
parent9b2914ed9f7b14ecf535ffe9e1328d0fa042e072 (diff)
Generate code for options with modes. (#3561)
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
Diffstat (limited to 'src/prop/bvminisat')
-rw-r--r--src/prop/bvminisat/simp/SimpSolver.cc42
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback