From 99d5e608b1e1a7541406e86d16b8e3bf6e7e8f0a Mon Sep 17 00:00:00 2001 From: lianah Date: Tue, 14 May 2013 16:28:12 -0400 Subject: [PATCH] added some extra options to the bit-vector theory --- src/theory/bv/bv_subtheory.h | 3 -- src/theory/bv/bv_subtheory_bitblast.cpp | 3 +- src/theory/bv/bv_subtheory_bitblast.h | 1 + src/theory/bv/bv_subtheory_core.cpp | 69 ++++++++++++------------- src/theory/bv/options | 6 +++ src/theory/bv/theory_bv.cpp | 11 ++-- 6 files changed, 47 insertions(+), 46 deletions(-) diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 8374a3f75..1c6920236 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -55,9 +55,6 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) { } -const bool d_useEqualityEngine = true; -const bool d_useSatPropagation = true; - // forward declaration class TheoryBV; diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 2308f36a3..244d87233 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -34,7 +34,8 @@ BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv) d_bitblaster(new Bitblaster(c, bv)), d_bitblastQueue(c), d_statistics(), - d_validModelCache(c, true) + d_validModelCache(c, true), + d_useSatPropagation(options::bvPropagate()) {} BitblastSolver::~BitblastSolver() { diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 819b3d62c..315254c8e 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -47,6 +47,7 @@ class BitblastSolver : public SubtheorySolver { context::CDO d_validModelCache; Node getModelValueRec(TNode node); + bool d_useSatPropagation; public: BitblastSolver(context::Context* c, TheoryBV* bv); ~BitblastSolver(); diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index c0546f892..f7209d326 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -37,40 +37,38 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv) d_isCoreTheory(c, true), d_reasons(c) { - if (d_useEqualityEngine) { - // The kinds we are treating as function application in congruence - d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP); - d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true); - d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true); - d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT); - // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE); - } + // The kinds we are treating as function application in congruence + d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true); + d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT); + // d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE); } CoreSolver::~CoreSolver() { @@ -81,9 +79,6 @@ void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) { } void CoreSolver::preRegister(TNode node) { - if (!d_useEqualityEngine) - return; - if (node.getKind() == kind::EQUAL) { d_equalityEngine.addTriggerEquality(node); if (options::bitvectorCoreSolver()) { @@ -291,7 +286,7 @@ void CoreSolver::buildModel() { bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) { // Notify the equality engine - if (d_useEqualityEngine && !d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) { + if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) { Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl; // Debug("bv-slicer-eq") << " reason=" << reason << endl; bool negated = fact.getKind() == kind::NOT; diff --git a/src/theory/bv/options b/src/theory/bv/options index 7b87baa21..077299d1f 100644 --- a/src/theory/bv/options +++ b/src/theory/bv/options @@ -22,5 +22,11 @@ option bitvectorCoreSolver --bv-core-solver bool option bvToBool --bv-to-bool bool lift bit-vectors of size 1 to booleans when possible + +option bvPropagate --bv-propagate bool :default true + use bit-vector propagation in the bit-blaster + +option bvEquality --bv-eq bool :default true + use the equality engine for the bit-vector theory endmodule diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 4803fd62e..224359952 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -49,10 +49,11 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& d_literalsToPropagateIndex(c, 0), d_propagatedBy(c) { - SubtheorySolver* core_solver = new CoreSolver(c, this); - d_subtheories.push_back(core_solver); - d_subtheoryMap[SUB_CORE] = core_solver; - + if (options::bvEquality()) { + SubtheorySolver* core_solver = new CoreSolver(c, this); + d_subtheories.push_back(core_solver); + d_subtheoryMap[SUB_CORE] = core_solver; + } if (options::bitvectorInequalitySolver()) { SubtheorySolver* ineq_solver = new InequalitySolver(c, this); d_subtheories.push_back(ineq_solver); @@ -366,7 +367,7 @@ Node TheoryBV::explain(TNode node) { void TheoryBV::addSharedTerm(TNode t) { Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl; d_sharedTermsSet.insert(t); - if (!options::bitvectorEagerBitblast() && d_useEqualityEngine) { + if (!options::bitvectorEagerBitblast() && options::bvEquality()) { for (unsigned i = 0; i < d_subtheories.size(); ++i) { d_subtheories[i]->addSharedTerm(t); } -- 2.30.2