summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/bv/bitblast/lazy_bitblaster.cpp13
-rw-r--r--src/theory/bv/bitblast/lazy_bitblaster.h6
-rw-r--r--src/theory/bv/bv_quick_check.cpp5
-rw-r--r--src/theory/bv/bv_quick_check.h3
-rw-r--r--src/theory/bv/bv_solver.h12
-rw-r--r--src/theory/bv/bv_solver_lazy.cpp12
-rw-r--r--src/theory/bv/bv_solver_lazy.h10
-rw-r--r--src/theory/bv/bv_subtheory.h4
-rw-r--r--src/theory/bv/bv_subtheory_algebraic.cpp13
-rw-r--r--src/theory/bv/bv_subtheory_algebraic.h3
-rw-r--r--src/theory/bv/bv_subtheory_bitblast.cpp10
-rw-r--r--src/theory/bv/bv_subtheory_bitblast.h3
-rw-r--r--src/theory/bv/bv_subtheory_core.cpp33
-rw-r--r--src/theory/bv/bv_subtheory_core.h6
-rw-r--r--src/theory/bv/bv_subtheory_inequality.cpp5
-rw-r--r--src/theory/bv/bv_subtheory_inequality.h3
-rw-r--r--src/theory/bv/theory_bv.cpp14
-rw-r--r--src/theory/bv/theory_bv.h4
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"); }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback