diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-12-17 13:43:44 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-12-17 13:43:44 -0800 |
commit | e9499c41f405df8b42fd9ae10004b1b91a869106 (patch) | |
tree | fa1475f43a3e61b8f6ffdcb903b65919eba28661 /src/theory/bv | |
parent | 9b2914ed9f7b14ecf535ffe9e1328d0fa042e072 (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/theory/bv')
-rw-r--r-- | src/theory/bv/abstraction.cpp | 5 | ||||
-rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.cpp | 8 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/slicer.cpp | 12 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 35 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.cpp | 3 |
7 files changed, 40 insertions, 27 deletions
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index d9de9731a..d3aeb5c37 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -88,7 +88,7 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, } // if we are using the eager solver reverse the abstraction - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + if (options::bitblastMode() == options::BitblastMode::EAGER) { if (d_funcToSignature.size() == 0) { @@ -1081,7 +1081,8 @@ bool AbstractionModule::isLemmaAtom(TNode node) const { } void AbstractionModule::addInputAtom(TNode atom) { - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY) { + if (options::bitblastMode() == options::BitblastMode::LAZY) + { d_inputAtoms.insert(atom); } } diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 9d43355cc..cd906769d 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -42,7 +42,7 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c) prop::SatSolver *solver = nullptr; switch (options::bvSatSolver()) { - case SAT_SOLVER_MINISAT: + case options::SatSolverMode::MINISAT: { prop::BVSatSolverInterface* minisat = prop::SatSolverFactory::createMinisat( @@ -52,11 +52,11 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c) solver = minisat; break; } - case SAT_SOLVER_CADICAL: + case options::SatSolverMode::CADICAL: solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(), "EagerBitblaster"); break; - case SAT_SOLVER_CRYPTOMINISAT: + case options::SatSolverMode::CRYPTOMINISAT: solver = prop::SatSolverFactory::createCryptoMinisat( smtStatisticsRegistry(), "EagerBitblaster"); break; @@ -120,7 +120,7 @@ void EagerBitblaster::bbAtom(TNode node) Node atom_definition = NodeManager::currentNM()->mkNode(kind::EQUAL, node, atom_bb); - AlwaysAssert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); + AlwaysAssert(options::bitblastMode() == options::BitblastMode::EAGER); storeBBAtom(node, atom_bb); d_cnfStream->convertAndAssert( atom_definition, false, false, RULE_INVALID, TNode::null()); diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 6f8804042..14753deec 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -253,7 +253,7 @@ AlgebraicSolver::~AlgebraicSolver() {} bool AlgebraicSolver::check(Theory::Effort e) { - Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); + Assert(options::bitblastMode() == options::BitblastMode::LAZY); if (!Theory::fullEffort(e)) { return true; } if (!useHeuristic()) { return true; } diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 94dfdee14..25fe7002e 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -120,7 +120,7 @@ void BitblastSolver::bitblastQueue() { bool BitblastSolver::check(Theory::Effort e) { Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n"; - Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); + Assert(options::bitblastMode() == options::BitblastMode::LAZY); ++(d_statistics.d_numCallstoCheck); diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index 0ffd58d5a..e1732625e 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -536,10 +536,14 @@ bool Slicer::isCoreTerm(TNode node) { if (d_coreTermCache.find(node) == d_coreTermCache.end()) { Kind kind = node.getKind(); bool not_core; - if (options::bitvectorEqualitySlicer() != BITVECTOR_SLICER_OFF) { - not_core = (kind != kind::BITVECTOR_EXTRACT && kind != kind::BITVECTOR_CONCAT); - } else { - not_core = true; + if (options::bitvectorEqualitySlicer() != options::BvSlicerMode::OFF) + { + not_core = + (kind != kind::BITVECTOR_EXTRACT && kind != kind::BITVECTOR_CONCAT); + } + else + { + not_core = true; } if (not_core && kind != kind::EQUAL && diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 23ffabcd1..afd99647b 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -77,7 +77,8 @@ TheoryBV::TheoryBV(context::Context* c, setupExtTheory(); getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT); getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR); - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + if (options::bitblastMode() == options::BitblastMode::EAGER) + { d_eagerSolver.reset(new EagerBitblastSolver(c, this)); return; } @@ -112,7 +113,8 @@ TheoryBV::TheoryBV(context::Context* c, TheoryBV::~TheoryBV() {} void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) { - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + if (options::bitblastMode() == options::BitblastMode::EAGER) + { return; } if (options::bitvectorEqualitySolver()) { @@ -237,7 +239,7 @@ void TheoryBV::preRegisterTerm(TNode node) { d_calledPreregister = true; Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl; - if (options::bitblastMode() == BITBLAST_MODE_EAGER) + if (options::bitblastMode() == options::BitblastMode::EAGER) { // the aig bit-blaster option is set heuristically // if bv abstraction is used @@ -325,7 +327,8 @@ void TheoryBV::check(Effort e) // we may be getting new assertions so the model cache may not be sound d_invalidateModelCache.set(true); // if we are using the eager solver - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + if (options::bitblastMode() == options::BitblastMode::EAGER) + { // this can only happen on an empty benchmark if (!d_eagerSolver->isInitialized()) { d_eagerSolver->initialize(); @@ -354,7 +357,6 @@ void TheoryBV::check(Effort e) return; } - if (Theory::fullEffort(e)) { ++(d_statistics.d_numCallsToCheckFullEffort); } else { @@ -521,7 +523,8 @@ bool TheoryBV::needsCheckLastEffort() { bool TheoryBV::collectModelInfo(TheoryModel* m) { Assert(!inConflict()); - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + if (options::bitblastMode() == options::BitblastMode::EAGER) + { if (!d_eagerSolver->collectModelInfo(m, true)) { return false; @@ -547,7 +550,8 @@ Node TheoryBV::getModelValue(TNode var) { void TheoryBV::propagate(Effort e) { Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl; - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { + if (options::bitblastMode() == options::BitblastMode::EAGER) + { return; } @@ -910,9 +914,9 @@ void TheoryBV::addSharedTerm(TNode t) { EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b) { - if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) + if (options::bitblastMode() == options::BitblastMode::EAGER) return EQUALITY_UNKNOWN; - Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY); + Assert(options::bitblastMode() == options::BitblastMode::LAZY); for (unsigned i = 0; i < d_subtheories.size(); ++i) { EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b); if (status != EQUALITY_UNKNOWN) { @@ -975,9 +979,9 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) { bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) { bool changed = d_abstractionModule->applyAbstraction(assertions, new_assertions); - if (changed && - options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && - options::bitvectorAig()) { + if (changed && options::bitblastMode() == options::BitblastMode::EAGER + && options::bitvectorAig()) + { // disable AIG mode AlwaysAssert(!d_eagerSolver->isInitialized()); d_eagerSolver->turnOffAig(); @@ -988,9 +992,12 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector void TheoryBV::setProofLog(proof::BitVectorProof* bvp) { - if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){ + if (options::bitblastMode() == options::BitblastMode::EAGER) + { d_eagerSolver->setProofLog(bvp); - }else{ + } + else + { for( unsigned i=0; i< d_subtheories.size(); i++ ){ d_subtheories[i]->setProofLog( bvp ); } diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index c0df9f35c..765541150 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -18,6 +18,7 @@ #include <vector> +#include "options/theory_options.h" #include "theory/theory.h" namespace CVC4 { @@ -156,7 +157,7 @@ static bool isCoreEqTerm(bool iseq, TNode term, TNodeBoolMap& cache) continue; } - if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, n) + if (theory::Theory::theoryOf(options::TheoryOfMode::THEORY_OF_TERM_BASED, n) == theory::THEORY_BV) { Kind k = n.getKind(); |