summaryrefslogtreecommitdiff
path: root/src/theory/bv
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv')
-rw-r--r--src/theory/bv/bitblaster_template.h4
-rw-r--r--src/theory/bv/bv_eager_solver.cpp5
-rw-r--r--src/theory/bv/bv_eager_solver.h2
-rw-r--r--src/theory/bv/bv_quick_check.cpp5
-rw-r--r--src/theory/bv/bv_quick_check.h2
-rw-r--r--src/theory/bv/bv_subtheory.h2
-rw-r--r--src/theory/bv/bv_subtheory_algebraic.cpp10
-rw-r--r--src/theory/bv/bv_subtheory_algebraic.h4
-rw-r--r--src/theory/bv/bv_subtheory_bitblast.cpp3
-rw-r--r--src/theory/bv/bv_subtheory_bitblast.h2
-rw-r--r--src/theory/bv/bv_subtheory_core.cpp16
-rw-r--r--src/theory/bv/bv_subtheory_core.h2
-rw-r--r--src/theory/bv/bv_subtheory_inequality.cpp10
-rw-r--r--src/theory/bv/bv_subtheory_inequality.h2
-rw-r--r--src/theory/bv/eager_bitblaster.cpp9
-rw-r--r--src/theory/bv/lazy_bitblaster.cpp9
-rw-r--r--src/theory/bv/theory_bv.cpp13
-rw-r--r--src/theory/bv/theory_bv.h2
18 files changed, 67 insertions, 35 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 565c454e3..0e7614221 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -207,7 +207,7 @@ public:
* @param fullModel whether to create a "full model," i.e., add
* constants to equivalence classes that don't already have them
*/
- void collectModelInfo(TheoryModel* m, bool fullModel);
+ bool collectModelInfo(TheoryModel* m, bool fullModel);
void setProofLog( BitVectorProof * bvp );
typedef TNodeSet::const_iterator vars_iterator;
@@ -292,7 +292,7 @@ public:
bool assertToSat(TNode node, bool propagate = true);
bool solve();
- void collectModelInfo(TheoryModel* m, bool fullModel);
+ bool collectModelInfo(TheoryModel* m, bool fullModel);
void setProofLog( BitVectorProof * bvp );
};
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 50070b29a..01282880c 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -123,9 +123,10 @@ bool EagerBitblastSolver::hasAssertions(const std::vector<TNode>& formulas) {
return true;
}
-void EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
+{
AlwaysAssert(!d_useAig && d_bitblaster);
- d_bitblaster->collectModelInfo(m, fullModel);
+ return d_bitblaster->collectModelInfo(m, fullModel);
}
void EagerBitblastSolver::setProofLog(BitVectorProof* bvp) { d_bvp = bvp; }
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index d259d49e6..856de530d 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -47,7 +47,7 @@ class EagerBitblastSolver {
void turnOffAig();
bool isInitialized();
void initialize();
- void collectModelInfo(theory::TheoryModel* m, bool fullModel);
+ bool collectModelInfo(theory::TheoryModel* m, bool fullModel);
void setProofLog(BitVectorProof* bvp);
private:
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index b347ddccf..a3442e4c6 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -136,8 +136,9 @@ void BVQuickCheck::popToZero() {
}
}
-void BVQuickCheck::collectModelInfo(theory::TheoryModel* model, bool fullModel) {
- d_bitblaster->collectModelInfo(model, fullModel);
+bool BVQuickCheck::collectModelInfo(theory::TheoryModel* model, bool fullModel)
+{
+ return d_bitblaster->collectModelInfo(model, fullModel);
}
BVQuickCheck::~BVQuickCheck() {
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index c5fe63ad6..d163bf7f9 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -97,7 +97,7 @@ public:
* @return
*/
uint64_t computeAtomWeight(TNode atom, NodeSet& seen);
- void collectModelInfo(theory::TheoryModel* model, bool fullModel);
+ bool collectModelInfo(theory::TheoryModel* model, bool fullModel);
typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator vars_iterator;
vars_iterator beginVars();
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 454f89b6c..63dd53407 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -75,7 +75,7 @@ class SubtheorySolver {
virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
virtual void preRegister(TNode node) {}
virtual void propagate(Theory::Effort e) {}
- virtual void collectModelInfo(TheoryModel* m, bool fullModel) = 0;
+ virtual bool collectModelInfo(TheoryModel* m, bool fullModel) = 0;
virtual Node getModelValue(TNode var) = 0;
virtual bool isComplete() = 0;
virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0;
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index c5313b9e7..a6e3153cb 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -676,7 +676,8 @@ void AlgebraicSolver::assertFact(TNode fact) {
EqualityStatus AlgebraicSolver::getEqualityStatus(TNode a, TNode b) {
return EQUALITY_UNKNOWN;
}
-void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) {
+bool AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel)
+{
Debug("bitvector-model") << "AlgebraicSolver::collectModelInfo\n";
AlwaysAssert (!d_quickSolver->inConflict());
set<Node> termSet;
@@ -729,9 +730,12 @@ void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) {
Debug("bitvector-model") << "AlgebraicSolver: " << variables[i] << " => " << subst << "\n";
// Doesn't have to be constant as it may be irrelevant
Assert (subst.getKind() == kind::CONST_BITVECTOR);
- model->assertEquality(variables[i], subst, true);
+ if (!model->assertEquality(variables[i], subst, true))
+ {
+ return false;
+ }
}
-
+ return true;
}
Node AlgebraicSolver::getModelValue(TNode node) {
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index 4b4103e44..0534c0f17 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -227,8 +227,8 @@ public:
void preRegister(TNode node) {}
bool check(Theory::Effort e);
void explain(TNode literal, std::vector<TNode>& assumptions) {Unreachable("AlgebraicSolver does not propagate.\n");}
- EqualityStatus getEqualityStatus(TNode a, TNode b);
- void collectModelInfo(TheoryModel* m, bool fullModel);
+ EqualityStatus getEqualityStatus(TNode a, TNode b);
+ bool collectModelInfo(TheoryModel* m, bool fullModel);
Node getModelValue(TNode node);
bool isComplete();
virtual void assertFact(TNode fact);
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 77e596d1f..b9467c168 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -234,7 +234,8 @@ EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) {
return d_bitblaster->getEqualityStatus(a, b);
}
-void BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
+{
return d_bitblaster->collectModelInfo(m, fullModel);
}
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 4bbe4327e..5927feddc 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -69,7 +69,7 @@ public:
bool check(Theory::Effort e);
void explain(TNode literal, std::vector<TNode>& assumptions);
EqualityStatus getEqualityStatus(TNode a, TNode b);
- void collectModelInfo(TheoryModel* m, bool fullModel);
+ bool collectModelInfo(TheoryModel* m, bool fullModel);
Node getModelValue(TNode node);
bool isComplete() { return true; }
void bitblastQueue();
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 54f454dca..8ef2b471f 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -396,7 +396,8 @@ bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) {
return utils::isEqualityTerm(term, seen);
}
-void CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel)
+{
if (d_useSlicer) {
Unreachable();
}
@@ -409,17 +410,24 @@ void CoreSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
}
set<Node> termSet;
d_bv->computeRelevantTerms(termSet);
- m->assertEqualityEngine(&d_equalityEngine, &termSet);
+ if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
+ {
+ return false;
+ }
if (isComplete()) {
Debug("bitvector-model") << "CoreSolver::collectModelInfo 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";
- m->assertEquality(a, b, true);
+ << a << " => " << b <<")\n";
+ if (!m->assertEquality(a, b, true))
+ {
+ return false;
+ }
}
}
+ return true;
}
Node CoreSolver::getModelValue(TNode var) {
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index b416e019d..6cc6253ff 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -105,7 +105,7 @@ public:
void preRegister(TNode node);
bool check(Theory::Effort e);
void explain(TNode literal, std::vector<TNode>& assumptions);
- void collectModelInfo(TheoryModel* m, bool fullModel);
+ bool collectModelInfo(TheoryModel* m, bool fullModel);
Node getModelValue(TNode var);
void addSharedTerm(TNode t) {
d_equalityEngine.addTriggerTerm(t, THEORY_BV);
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index d662f056b..d828cc892 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -182,15 +182,19 @@ void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
void InequalitySolver::propagate(Theory::Effort e) {
Assert (false);
}
-
-void InequalitySolver::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool InequalitySolver::collectModelInfo(TheoryModel* m, bool fullModel)
+{
Debug("bitvector-model") << "InequalitySolver::collectModelInfo \n";
std::vector<Node> model;
d_inequalityGraph.getAllValuesInModel(model);
for (unsigned i = 0; i < model.size(); ++i) {
Assert (model[i].getKind() == kind::EQUAL);
- m->assertEquality(model[i][0], model[i][1], true);
+ if (!m->assertEquality(model[i][0], model[i][1], true))
+ {
+ return false;
+ }
}
+ return true;
}
Node InequalitySolver::getModelValue(TNode var) {
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 1123d15ae..be0492125 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -69,7 +69,7 @@ public:
void propagate(Theory::Effort e);
void explain(TNode literal, std::vector<TNode>& assumptions);
bool isComplete() { return d_isComplete; }
- void collectModelInfo(TheoryModel* m, bool fullModel);
+ bool collectModelInfo(TheoryModel* m, bool fullModel);
Node getModelValue(TNode var);
EqualityStatus getEqualityStatus(TNode a, TNode b);
void assertFact(TNode fact);
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 29f6e7800..e2bfec893 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -219,7 +219,8 @@ Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
return utils::mkConst(BitVector(bits.size(), value));
}
-void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
+{
TNodeSet::iterator it = d_variables.begin();
for (; it != d_variables.end(); ++it) {
TNode var = *it;
@@ -234,10 +235,14 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
Debug("bitvector-model")
<< "EagerBitblaster::collectModelInfo (assert (= " << var << " "
<< const_value << "))\n";
- m->assertEquality(var, const_value, true);
+ if (!m->assertEquality(var, const_value, true))
+ {
+ return false;
+ }
}
}
}
+ return true;
}
void EagerBitblaster::setProofLog(BitVectorProof* bvp) {
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 32aff1fb0..7976097e1 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -484,7 +484,8 @@ Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
return utils::mkConst(BitVector(bits.size(), value));
}
-void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
+bool TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel)
+{
std::set<Node> termSet;
d_bv->computeRelevantTerms(termSet);
@@ -504,9 +505,13 @@ void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
<< var << " "
<< const_value << "))\n";
- m->assertEquality(var, const_value, true);
+ if (!m->assertEquality(var, const_value, true))
+ {
+ return false;
+ }
}
}
+ return true;
}
void TLazyBitblaster::setProofLog( BitVectorProof * bvp ){
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index e03cecdd9..cb214217c 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -576,18 +576,21 @@ bool TheoryBV::doExtfReductions( std::vector< Node >& terms ) {
bool TheoryBV::needsCheckLastEffort() {
return d_needsLastCallCheck;
}
-
-void TheoryBV::collectModelInfo( TheoryModel* m ){
+bool TheoryBV::collectModelInfo(TheoryModel* m)
+{
Assert(!inConflict());
if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
- d_eagerSolver->collectModelInfo(m, true);
+ if (!d_eagerSolver->collectModelInfo(m, true))
+ {
+ return false;
+ }
}
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
if (d_subtheories[i]->isComplete()) {
- d_subtheories[i]->collectModelInfo(m, true);
- return;
+ return d_subtheories[i]->collectModelInfo(m, true);
}
}
+ return true;
}
Node TheoryBV::getModelValue(TNode var) {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index c21938aa7..a425cbdc8 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -80,7 +80,7 @@ public:
Node explain(TNode n);
- void collectModelInfo( TheoryModel* m );
+ bool collectModelInfo(TheoryModel* m) override;
std::string identify() const { return std::string("TheoryBV"); }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback