diff options
-rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.cpp | 13 | ||||
-rw-r--r-- | src/theory/bv/bitblast/lazy_bitblaster.h | 6 | ||||
-rw-r--r-- | src/theory/bv/bv_quick_check.cpp | 5 | ||||
-rw-r--r-- | src/theory/bv/bv_quick_check.h | 3 | ||||
-rw-r--r-- | src/theory/bv/bv_solver.h | 12 | ||||
-rw-r--r-- | src/theory/bv/bv_solver_lazy.cpp | 12 | ||||
-rw-r--r-- | src/theory/bv/bv_solver_lazy.h | 10 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory.h | 4 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 13 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.h | 3 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.cpp | 10 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.h | 3 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 33 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.h | 6 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.cpp | 5 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.h | 3 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 14 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 4 |
18 files changed, 74 insertions, 85 deletions
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 3e32b4cc3..1813784d7 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -530,12 +530,9 @@ Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) { return utils::mkConst(bits.size(), value); } -bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) +bool TLazyBitblaster::collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) { - std::set<Node> termSet; - const std::set<Kind>& irrKinds = m->getIrrelevantKinds(); - d_bv->computeAssertedTerms(termSet, irrKinds, true); - for (std::set<Node>::const_iterator it = termSet.begin(); it != termSet.end(); ++it) { TNode var = *it; // not actually a leaf of the bit-vector theory @@ -549,9 +546,9 @@ bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) Node const_value = getModelFromSatSolver(var, true); Assert(const_value.isNull() || const_value.isConst()); if(const_value != Node()) { - Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= " - << var << " " - << const_value << "))\n"; + Debug("bitvector-model") + << "TLazyBitblaster::collectModelValues (assert (= " << var << " " + << const_value << "))\n"; if (!m->assertEquality(var, const_value, true)) { return false; diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h index e53f1697d..66cd6cc23 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.h +++ b/src/theory/bv/bitblast/lazy_bitblaster.h @@ -72,10 +72,10 @@ class TLazyBitblaster : public TBitblaster<Node> * Adds a constant value for each bit-blasted variable in the model. * * @param m the model - * @param fullModel whether to create a "full model," i.e., add - * constants to equivalence classes that don't already have them + * @param termSet the set of relevant terms */ - bool collectModelInfo(TheoryModel* m, bool fullModel); + bool collectModelValues(TheoryModel* m, + const std::set<Node>& termSet); typedef TNodeSet::const_iterator vars_iterator; vars_iterator beginVars() { return d_variables.begin(); } diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp index f8e30247f..10fc8c4b7 100644 --- a/src/theory/bv/bv_quick_check.cpp +++ b/src/theory/bv/bv_quick_check.cpp @@ -140,9 +140,10 @@ void BVQuickCheck::popToZero() { } } -bool BVQuickCheck::collectModelInfo(theory::TheoryModel* model, bool fullModel) +bool BVQuickCheck::collectModelValues(theory::TheoryModel* model, + const std::set<Node>& termSet) { - return d_bitblaster->collectModelInfo(model, fullModel); + return d_bitblaster->collectModelValues(model, termSet); } BVQuickCheck::~BVQuickCheck() { diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index c1d9e333e..95e1eb600 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -98,7 +98,8 @@ class BVQuickCheck * @return */ uint64_t computeAtomWeight(TNode atom, NodeSet& seen); - bool collectModelInfo(theory::TheoryModel* model, bool fullModel); + bool collectModelValues(theory::TheoryModel* model, + const std::set<Node>& termSet); typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator vars_iterator; diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h index fef95ceef..f8d6467aa 100644 --- a/src/theory/bv/bv_solver.h +++ b/src/theory/bv/bv_solver.h @@ -77,13 +77,11 @@ class BVSolver Unimplemented() << "BVSolver propagated a node but doesn't implement the " "BVSolver::explain() interface!"; return TrustNode::null(); - }; + } - /** - * This is temporary only and will be deprecated soon in favor of - * Theory::collectModelValues. - */ - virtual bool collectModelInfo(TheoryModel* m) = 0; + /** Collect model values in m based on the relevant terms given by termSet */ + virtual bool collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) = 0; virtual std::string identify() const = 0; @@ -96,7 +94,7 @@ class BVSolver virtual void presolve(){}; - virtual void notifySharedTerm(TNode t) = 0; + virtual void notifySharedTerm(TNode t) {} virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp index ad673b402..c0f34c132 100644 --- a/src/theory/bv/bv_solver_lazy.cpp +++ b/src/theory/bv/bv_solver_lazy.cpp @@ -368,7 +368,8 @@ bool BVSolverLazy::needsCheckLastEffort() return false; } -bool BVSolverLazy::collectModelInfo(TheoryModel* m) +bool BVSolverLazy::collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) { Assert(!inConflict()); if (options::bitblastMode() == options::BitblastMode::EAGER) @@ -382,7 +383,7 @@ bool BVSolverLazy::collectModelInfo(TheoryModel* m) { if (d_subtheories[i]->isComplete()) { - return d_subtheories[i]->collectModelInfo(m, true); + return d_subtheories[i]->collectModelValues(m, termSet); } } return true; @@ -719,13 +720,6 @@ void BVSolverLazy::notifySharedTerm(TNode t) Debug("bitvector::sharing") << indent() << "BVSolverLazy::notifySharedTerm(" << t << ")" << std::endl; d_sharedTermsSet.insert(t); - if (options::bitvectorEqualitySolver()) - { - for (unsigned i = 0; i < d_subtheories.size(); ++i) - { - d_subtheories[i]->addSharedTerm(t); - } - } } EqualityStatus BVSolverLazy::getEqualityStatus(TNode a, TNode b) diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h index 81f40340e..e7033275f 100644 --- a/src/theory/bv/bv_solver_lazy.h +++ b/src/theory/bv/bv_solver_lazy.h @@ -87,7 +87,8 @@ class BVSolverLazy : public BVSolver TrustNode explain(TNode n) override; - bool collectModelInfo(TheoryModel* m) override; + bool collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) override; std::string identify() const override { return std::string("BVSolverLazy"); } @@ -208,13 +209,6 @@ class BVSolverLazy : public BVSolver void checkForLemma(TNode node); - void computeAssertedTerms(std::set<Node>& termSet, - const std::set<Kind>& irrKinds, - bool includeShared) const - { - return d_bv.computeAssertedTerms(termSet, irrKinds, includeShared); - } - size_t numAssertions() { return d_bv.numAssertions(); } theory::Assertion get() { return d_bv.get(); } diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 1244ae828..37474bfec 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -74,11 +74,11 @@ class SubtheorySolver { virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0; virtual void preRegister(TNode node) {} virtual void propagate(Theory::Effort e) {} - virtual bool collectModelInfo(TheoryModel* m, bool fullModel) = 0; + virtual bool collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) = 0; virtual Node getModelValue(TNode var) = 0; virtual bool isComplete() = 0; virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0; - virtual void addSharedTerm(TNode node) {} bool done() { return d_assertionQueue.size() == d_assertionIndex; } TNode get() { Assert(!done()); diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 49043b445..e900566f9 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -472,7 +472,8 @@ bool AlgebraicSolver::quickCheck(std::vector<Node>& facts) { return false; } -void AlgebraicSolver::setConflict(TNode conflict) { +void AlgebraicSolver::setConflict(TNode conflict) +{ Node final_conflict = conflict; if (options::bitvectorQuickXplain() && conflict.getKind() == kind::AND && @@ -711,13 +712,11 @@ EqualityStatus AlgebraicSolver::getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; } -bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) +bool AlgebraicSolver::collectModelValues(TheoryModel* model, + const std::set<Node>& termSet) { - Debug("bitvector-model") << "AlgebraicSolver::collectModelInfo\n"; + Debug("bitvector-model") << "AlgebraicSolver::collectModelValues\n"; AlwaysAssert(!d_quickSolver->inConflict()); - set<Node> termSet; - const std::set<Kind>& irrKinds = model->getIrrelevantKinds(); - d_bv->computeAssertedTerms(termSet, irrKinds, true); // collect relevant terms that the bv theory abstracts to variables // (variables and parametric terms such as select apply_uf) @@ -748,7 +747,7 @@ bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) for (NodeSet::const_iterator it = leaf_vars.begin(); it != leaf_vars.end(); ++it) { TNode var = *it; Node value = d_quickSolver->getVarValue(var, true); - Assert(!value.isNull() || !fullModel); + Assert(!value.isNull()); // may be a shared term that did not appear in the current assertions // AJR: need to check whether already in map for cases where collectModelInfo is called multiple times in the same context diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h index a5d7b2db3..92cfac71e 100644 --- a/src/theory/bv/bv_subtheory_algebraic.h +++ b/src/theory/bv/bv_subtheory_algebraic.h @@ -236,7 +236,8 @@ class AlgebraicSolver : public SubtheorySolver Unreachable() << "AlgebraicSolver does not propagate.\n"; } EqualityStatus getEqualityStatus(TNode a, TNode b) override; - bool collectModelInfo(TheoryModel* m, bool fullModel) override; + bool collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) override; Node getModelValue(TNode node) override; bool isComplete() override; void assertFact(TNode fact) override; diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 93ac87abe..47ab5cec5 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -248,9 +248,10 @@ EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) { return d_bitblaster->getEqualityStatus(a, b); } -bool BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) +bool BitblastSolver::collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) { - return d_bitblaster->collectModelInfo(m, fullModel); + return d_bitblaster->collectModelValues(m, termSet); } Node BitblastSolver::getModelValue(TNode node) @@ -263,9 +264,8 @@ Node BitblastSolver::getModelValue(TNode node) return val; } - - -void BitblastSolver::setConflict(TNode conflict) { +void BitblastSolver::setConflict(TNode conflict) +{ Node final_conflict = conflict; if (options::bitvectorQuickXplain() && conflict.getKind() == kind::AND) { diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h index 0832b6772..0f43b4f30 100644 --- a/src/theory/bv/bv_subtheory_bitblast.h +++ b/src/theory/bv/bv_subtheory_bitblast.h @@ -72,7 +72,8 @@ class BitblastSolver : public SubtheorySolver bool check(Theory::Effort e) override; void explain(TNode literal, std::vector<TNode>& assumptions) override; EqualityStatus getEqualityStatus(TNode a, TNode b) override; - bool collectModelInfo(TheoryModel* m, bool fullModel) override; + bool collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) override; Node getModelValue(TNode node) override; bool isComplete() override { return true; } void bitblastQueue(); diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 5bb6a45e4..162c2d31d 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -347,7 +347,10 @@ void CoreSolver::buildModel() bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) { // Notify the equality engine - if (!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; @@ -370,7 +373,8 @@ bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) { } // checking for a conflict - if (d_bv->inConflict()) { + if (d_bv->inConflict()) + { return false; } return true; @@ -412,29 +416,23 @@ bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) { return utils::isEqualityTerm(term, seen); } -bool CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel) +bool CoreSolver::collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) { if (Debug.isOn("bitvector-model")) { context::CDQueue<Node>::const_iterator it = d_assertionQueue.begin(); for (; it!= d_assertionQueue.end(); ++it) { - Debug("bitvector-model") << "CoreSolver::collectModelInfo (assert " - << *it << ")\n"; + Debug("bitvector-model") + << "CoreSolver::collectModelValues (assert " << *it << ")\n"; } } - set<Node> termSet; - const std::set<Kind>& irrKinds = m->getIrrelevantKinds(); - d_bv->computeAssertedTerms(termSet, irrKinds, true); - if (!m->assertEqualityEngine(d_equalityEngine, &termSet)) - { - return false; - } if (isComplete()) { - Debug("bitvector-model") << "CoreSolver::collectModelInfo complete."; + Debug("bitvector-model") << "CoreSolver::collectModelValues complete."; for (ModelValue::const_iterator it = d_modelValues.begin(); it != d_modelValues.end(); ++it) { Node a = it->first; Node b = it->second; - Debug("bitvector-model") << "CoreSolver::collectModelInfo modelValues " - << a << " => " << b <<")\n"; + Debug("bitvector-model") << "CoreSolver::collectModelValues modelValues " + << a << " => " << b << ")\n"; if (!m->assertEquality(a, b, true)) { return false; @@ -462,11 +460,6 @@ Node CoreSolver::getModelValue(TNode var) { return result; } -void CoreSolver::addSharedTerm(TNode t) -{ - d_equalityEngine->addTriggerTerm(t, THEORY_BV); -} - EqualityStatus CoreSolver::getEqualityStatus(TNode a, TNode b) { if (d_equalityEngine->areEqual(a, b)) diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h index 876daeabe..7bc5337c4 100644 --- a/src/theory/bv/bv_subtheory_core.h +++ b/src/theory/bv/bv_subtheory_core.h @@ -110,8 +110,6 @@ class CoreSolver : public SubtheorySolver { ModelValue d_modelValues; void buildModel(); bool assertFactToEqualityEngine(TNode fact, TNode reason); - bool decomposeFact(TNode fact); - Node getBaseDecomposition(TNode a); bool isCompleteForTerm(TNode term, TNodeBoolMap& seen); Statistics d_statistics; @@ -154,9 +152,9 @@ class CoreSolver : public SubtheorySolver { void preRegister(TNode node) override; bool check(Theory::Effort e) override; void explain(TNode literal, std::vector<TNode>& assumptions) override; - bool collectModelInfo(TheoryModel* m, bool fullModel) override; + bool collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) override; Node getModelValue(TNode var) override; - void addSharedTerm(TNode t) override; EqualityStatus getEqualityStatus(TNode a, TNode b) override; bool hasTerm(TNode node) const; void addTermToEqualityEngine(TNode node); diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index ffc354d8d..80a603ef0 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -189,9 +189,10 @@ void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) { } void InequalitySolver::propagate(Theory::Effort e) { Assert(false); } -bool InequalitySolver::collectModelInfo(TheoryModel* m, bool fullModel) +bool InequalitySolver::collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) { - Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n"; + Debug("bitvector-model") << "InequalitySolver::collectModelValues \n"; std::vector<Node> model; d_inequalityGraph.getAllValuesInModel(model); for (unsigned i = 0; i < model.size(); ++i) { diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index 05c9c3d60..ba0275fa6 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -79,7 +79,8 @@ class InequalitySolver : public SubtheorySolver void propagate(Theory::Effort e) override; void explain(TNode literal, std::vector<TNode>& assumptions) override; bool isComplete() override { return d_isComplete; } - bool collectModelInfo(TheoryModel* m, bool fullModel) override; + bool collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) override; Node getModelValue(TNode var) override; EqualityStatus getEqualityStatus(TNode a, TNode b) override; void assertFact(TNode fact) override; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 6f25d0843..fb7395a28 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -164,9 +164,9 @@ bool TheoryBV::needsCheckLastEffort() return d_internal->needsCheckLastEffort(); } -bool TheoryBV::collectModelInfo(TheoryModel* m) +bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet) { - return d_internal->collectModelInfo(m); + return d_internal->collectModelValues(m, termSet); } void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); } @@ -183,7 +183,15 @@ void TheoryBV::presolve() { d_internal->presolve(); } TrustNode TheoryBV::explain(TNode node) { return d_internal->explain(node); } -void TheoryBV::notifySharedTerm(TNode t) { d_internal->notifySharedTerm(t); }; +void TheoryBV::notifySharedTerm(TNode t) +{ + d_internal->notifySharedTerm(t); + // temporary, will be built into Theory::addSharedTerm + if (d_equalityEngine != nullptr) + { + d_equalityEngine->addTriggerTerm(t, THEORY_BV); + } +} void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index d33ea1337..cff16bec0 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -71,7 +71,9 @@ class TheoryBV : public Theory TrustNode explain(TNode n) override; - bool collectModelInfo(TheoryModel* m) override; + /** Collect model values in m based on the relevant terms given by termSet */ + bool collectModelValues(TheoryModel* m, + const std::set<Node>& termSet) override; std::string identify() const override { return std::string("TheoryBV"); } |