diff options
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/bitblaster_template.h | 4 | ||||
-rw-r--r-- | src/theory/bv/bv_eager_solver.cpp | 5 | ||||
-rw-r--r-- | src/theory/bv/bv_eager_solver.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_quick_check.cpp | 5 | ||||
-rw-r--r-- | src/theory/bv/bv_quick_check.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 10 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.h | 4 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.cpp | 3 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_bitblast.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.cpp | 16 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_core.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.cpp | 10 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.h | 2 | ||||
-rw-r--r-- | src/theory/bv/eager_bitblaster.cpp | 9 | ||||
-rw-r--r-- | src/theory/bv/lazy_bitblaster.cpp | 9 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 13 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 2 |
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"); } |