From 564234963dd7e76c8d9b88ef941a6683694e5b53 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 8 Dec 2017 10:14:31 -0600 Subject: [PATCH] Make collect model info return a Bool (#1421) --- src/theory/arith/theory_arith.cpp | 6 +- src/theory/arith/theory_arith.h | 2 +- src/theory/arith/theory_arith_private.cpp | 9 ++- src/theory/arith/theory_arith_private.h | 2 +- src/theory/arrays/theory_arrays.cpp | 16 ++-- src/theory/arrays/theory_arrays.h | 9 +-- src/theory/bv/bitblaster_template.h | 4 +- src/theory/bv/bv_eager_solver.cpp | 5 +- src/theory/bv/bv_eager_solver.h | 2 +- src/theory/bv/bv_quick_check.cpp | 5 +- src/theory/bv/bv_quick_check.h | 2 +- src/theory/bv/bv_subtheory.h | 2 +- src/theory/bv/bv_subtheory_algebraic.cpp | 10 ++- src/theory/bv/bv_subtheory_algebraic.h | 4 +- src/theory/bv/bv_subtheory_bitblast.cpp | 3 +- src/theory/bv/bv_subtheory_bitblast.h | 2 +- src/theory/bv/bv_subtheory_core.cpp | 16 +++- src/theory/bv/bv_subtheory_core.h | 2 +- src/theory/bv/bv_subtheory_inequality.cpp | 10 ++- src/theory/bv/bv_subtheory_inequality.h | 2 +- src/theory/bv/eager_bitblaster.cpp | 9 ++- src/theory/bv/lazy_bitblaster.cpp | 9 ++- src/theory/bv/theory_bv.cpp | 13 ++-- src/theory/bv/theory_bv.h | 2 +- src/theory/datatypes/theory_datatypes.cpp | 23 ++++-- src/theory/datatypes/theory_datatypes.h | 2 +- src/theory/fp/theory_fp.cpp | 10 ++- src/theory/fp/theory_fp.h | 2 +- src/theory/quantifiers/theory_quantifiers.cpp | 14 +++- src/theory/quantifiers/theory_quantifiers.h | 2 +- src/theory/quantifiers_engine.cpp | 34 ++++---- src/theory/sep/theory_sep.cpp | 6 +- src/theory/sep/theory_sep.h | 11 ++- src/theory/sets/theory_sets.cpp | 5 +- src/theory/sets/theory_sets.h | 2 +- src/theory/sets/theory_sets_private.cpp | 19 +++-- src/theory/sets/theory_sets_private.h | 2 +- src/theory/strings/theory_strings.cpp | 24 ++++-- src/theory/strings/theory_strings.h | 8 +- src/theory/theory.h | 6 +- src/theory/theory_engine.cpp | 43 +++++++---- src/theory/theory_engine.h | 2 +- src/theory/theory_model.cpp | 59 +++++++++----- src/theory/theory_model.h | 77 ++++++++++++++----- src/theory/theory_model_builder.cpp | 7 +- src/theory/theory_model_builder.h | 3 +- src/theory/uf/theory_uf.cpp | 14 +++- src/theory/uf/theory_uf.h | 2 +- 48 files changed, 347 insertions(+), 176 deletions(-) diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 985799e88..e354305d7 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -106,9 +106,9 @@ bool TheoryArith::isExtfReduced( int effort, Node n, Node on, std::vector< Node void TheoryArith::propagate(Effort e) { d_internal->propagate(e); } - -void TheoryArith::collectModelInfo( TheoryModel* m ){ - d_internal->collectModelInfo(m); +bool TheoryArith::collectModelInfo(TheoryModel* m) +{ + return d_internal->collectModelInfo(m); } void TheoryArith::notifyRestart(){ diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index e1226279a..1c10bde0d 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -61,7 +61,7 @@ public: bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ); bool isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp ); - void collectModelInfo( TheoryModel* m ); + bool collectModelInfo(TheoryModel* m) override; void shutdown(){ } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index c9a220566..8313abd68 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4252,7 +4252,8 @@ Rational TheoryArithPrivate::deltaValueForTotalOrder() const{ return belowMin; } -void TheoryArithPrivate::collectModelInfo( TheoryModel* m ){ +bool TheoryArithPrivate::collectModelInfo(TheoryModel* m) +{ AlwaysAssert(d_qflraStatus == Result::SAT); //AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints"); @@ -4288,7 +4289,10 @@ void TheoryArithPrivate::collectModelInfo( TheoryModel* m ){ Node qNode = mkRationalNode(qmodel); Debug("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl; - m->assertEquality(term, qNode, true); + if (!m->assertEquality(term, qNode, true)) + { + return false; + } }else{ Debug("arith::collectModelInfo") << "Skipping m->assertEquality(" << term << ", true)" << endl; @@ -4301,6 +4305,7 @@ void TheoryArithPrivate::collectModelInfo( TheoryModel* m ){ // m->assertEqualityEngine(&ee); Debug("arith::collectModelInfo") << "collectModelInfo() end " << endl; + return true; } bool TheoryArithPrivate::safeToReset() const { diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index b2471c5e8..08b884a03 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -444,7 +444,7 @@ public: Rational deltaValueForTotalOrder() const; - void collectModelInfo( TheoryModel* m ); + bool collectModelInfo(TheoryModel* m); void shutdown(){ } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index af417f740..508c9d8ff 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1038,8 +1038,7 @@ void TheoryArrays::computeCareGraph() // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// - -void TheoryArrays::collectModelInfo( TheoryModel* m ) +bool TheoryArrays::collectModelInfo(TheoryModel* m) { set termSet; @@ -1140,7 +1139,10 @@ void TheoryArrays::collectModelInfo( TheoryModel* m ) } while (changed); // Send the equality engine information to the model - m->assertEqualityEngine(&d_equalityEngine, &termSet); + if (!m->assertEqualityEngine(&d_equalityEngine, &termSet)) + { + return false; + } // Build a list of all the relevant reads, indexed by the store representative std::map > selects; @@ -1215,11 +1217,15 @@ void TheoryArrays::collectModelInfo( TheoryModel* m ) for (unsigned j = 0; j < reads.size(); ++j) { rep = nm->mkNode(kind::STORE, rep, reads[j][1], reads[j]); } - m->assertEquality(n, rep, true); + if (!m->assertEquality(n, rep, true)) + { + return false; + } if (!n.isConst()) { - m->assertRepresentative(rep); + m->assertSkeleton(rep); } } + return true; } ///////////////////////////////////////////////////////////////////////////// diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 08d1618c2..24c286e92 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -248,12 +248,11 @@ class TheoryArrays : public Theory { private: public: + bool collectModelInfo(TheoryModel* m) override; - void collectModelInfo(TheoryModel* m); - - ///////////////////////////////////////////////////////////////////////////// - // NOTIFICATIONS - ///////////////////////////////////////////////////////////////////////////// + ///////////////////////////////////////////////////////////////////////////// + // NOTIFICATIONS + ///////////////////////////////////////////////////////////////////////////// private: public: 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& 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::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& 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 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& 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& 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 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& 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& 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 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& 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 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"); } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 674e0d6b3..c17c022a1 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1490,7 +1490,8 @@ void TheoryDatatypes::computeCareGraph(){ Trace("dt-cg-summary") << "...done, # pairs = " << n_pairs << std::endl; } -void TheoryDatatypes::collectModelInfo( TheoryModel* m ){ +bool TheoryDatatypes::collectModelInfo(TheoryModel* m) +{ Trace("dt-cmi") << "Datatypes : Collect model info " << d_equalityEngine.consistent() << std::endl; Trace("dt-model") << std::endl; printModelDebug( "dt-model" ); @@ -1502,7 +1503,10 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m ){ getRelevantTerms(termSet); //combine the equality engine - m->assertEqualityEngine( &d_equalityEngine, &termSet ); + if (!m->assertEqualityEngine(&d_equalityEngine, &termSet)) + { + return false; + } //get all constructors eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine ); @@ -1579,7 +1583,10 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m ){ } if( !neqc.isNull() ){ Trace("dt-cmi") << "Assign : " << neqc << std::endl; - m->assertEquality( eqc, neqc, true ); + if (!m->assertEquality(eqc, neqc, true)) + { + return false; + } eqc_cons[ eqc ] = neqc; } if( addCons ){ @@ -1598,14 +1605,18 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m ){ std::map< Node, int > vmap; Node v = getCodatatypesValue( it->first, eqc_cons, vmap, 0 ); Trace("dt-cmi") << " EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << ", const = " << v.isConst() << std::endl; - m->assertEquality( eqc, v, true ); - m->assertRepresentative( v ); + if (!m->assertEquality(eqc, v, true)) + { + return false; + } + m->assertSkeleton(v); } }else{ Trace("dt-cmi") << "Datatypes : assert representative " << it->second << " for " << it->first << std::endl; - m->assertRepresentative( it->second ); + m->assertSkeleton(it->second); } } + return true; } diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 3c0a7c7cf..b3d88bb1c 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -264,7 +264,7 @@ public: void presolve(); void addSharedTerm(TNode t); EqualityStatus getEqualityStatus(TNode a, TNode b); - void collectModelInfo( TheoryModel* m ); + bool collectModelInfo(TheoryModel* m) override; void shutdown() { } std::string identify() const { return std::string("TheoryDatatypes"); } /** equality engine */ diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 276edfc0a..5be4a4601 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -578,7 +578,8 @@ Node TheoryFp::getModelValue(TNode var) { return d_conv.getValue(d_valuation, var); } -void TheoryFp::collectModelInfo(TheoryModel *m) { +bool TheoryFp::collectModelInfo(TheoryModel *m) +{ std::set relevantTerms; Trace("fp-collectModelInfo") @@ -632,10 +633,13 @@ void TheoryFp::collectModelInfo(TheoryModel *m) { << "TheoryFp::collectModelInfo(): relevantVariable " << node << std::endl; - m->assertEquality(node, d_conv.getValue(d_valuation, node), true); + if (!m->assertEquality(node, d_conv.getValue(d_valuation, node), true)) + { + return false; + } } - return; + return true; } bool TheoryFp::NotifyClass::eqNotifyTriggerEquality(TNode equality, diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 5205f5e23..614cbff46 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -46,7 +46,7 @@ class TheoryFp : public Theory { void check(Effort); Node getModelValue(TNode var); - void collectModelInfo(TheoryModel* m); + bool collectModelInfo(TheoryModel* m) override; std::string identify() const { return "THEORY_FP"; } diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 66e05b1cd..a278274c3 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -120,16 +120,24 @@ void TheoryQuantifiers::computeCareGraph() { //do nothing } -void TheoryQuantifiers::collectModelInfo(TheoryModel* m) { +bool TheoryQuantifiers::collectModelInfo(TheoryModel* m) +{ for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { if((*i).assertion.getKind() == kind::NOT) { Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl; - m->assertPredicate((*i).assertion[0], false); + if (!m->assertPredicate((*i).assertion[0], false)) + { + return false; + } } else { Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl; - m->assertPredicate(*i, true); + if (!m->assertPredicate(*i, true)) + { + return false; + } } } + return true; } void TheoryQuantifiers::check(Effort e) { diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 9c621dbd6..295a39464 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -56,7 +56,7 @@ public: void check(Effort e); Node getNextDecisionRequest( unsigned& priority ); Node getValue(TNode n); - void collectModelInfo( TheoryModel* m ); + bool collectModelInfo(TheoryModel* m) override; void shutdown() { } std::string identify() const { return std::string("TheoryQuantifiers"); } void setUserAttribute(const std::string& attr, Node n, std::vector node_values, std::string str_value); diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 59a85de1f..34dde7fc8 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -562,14 +562,22 @@ void QuantifiersEngine::check( Theory::Effort e ){ static_cast(qef); d_curr_effort_level = quant_e; //build the model if any module requested it - if( needsModelE==quant_e && !d_model->isBuilt() ){ - // theory engine's model builder is quantifier engine's builder if it has one - Assert( !d_builder || d_builder==d_te->getModelBuilder() ); - Trace("quant-engine-debug") << "Build model..." << std::endl; - if( !d_te->getModelBuilder()->buildModel( d_model ) ){ - //we are done if model building was unsuccessful - Trace("quant-engine-debug") << "...added lemmas." << std::endl; - flushLemmas(); + if (needsModelE == quant_e) + { + if (!d_model->isBuilt()) + { + // theory engine's model builder is quantifier engine's builder if it + // has one + Assert(!d_builder || d_builder == d_te->getModelBuilder()); + Trace("quant-engine-debug") << "Build model..." << std::endl; + if (!d_te->getModelBuilder()->buildModel(d_model)) + { + flushLemmas(); + } + } + if (!d_model->isBuiltSuccess()) + { + break; } } if( !d_hasAddedLemma ){ @@ -690,16 +698,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ //SAT case if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){ - if( options::produceModels() ){ - if( d_model->isBuilt() ){ - Trace("quant-engine-debug") << "Already built model using model builder, finish..." << std::endl; - }else{ - //use default model builder when no module built the model - Trace("quant-engine-debug") << "Build the default model..." << std::endl; - d_te->getModelBuilder()->buildModel( d_model ); - Trace("quant-engine-debug") << "Done building the model." << std::endl; - } - } if( setIncomplete ){ Trace("quant-engine") << "Set incomplete flag." << std::endl; getOutputChannel().setIncomplete(); diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 71cde2841..0107b80c8 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -200,15 +200,15 @@ void TheorySep::computeCareGraph() { // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// - -void TheorySep::collectModelInfo( TheoryModel* m ){ +bool TheorySep::collectModelInfo(TheoryModel* m) +{ set termSet; // Compute terms appearing in assertions and shared terms computeRelevantTerms(termSet); // Send the equality engine information to the model - m->assertEqualityEngine( &d_equalityEngine, &termSet ); + return m->assertEqualityEngine(&d_equalityEngine, &termSet); } void TheorySep::postProcessModel( TheoryModel* m ){ diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 591a495d0..65f076631 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -109,13 +109,12 @@ class TheorySep : public Theory { ///////////////////////////////////////////////////////////////////////////// public: + bool collectModelInfo(TheoryModel* m) override; + void postProcessModel(TheoryModel* m); - void collectModelInfo(TheoryModel* m); - void postProcessModel(TheoryModel* m); - - ///////////////////////////////////////////////////////////////////////////// - // NOTIFICATIONS - ///////////////////////////////////////////////////////////////////////////// + ///////////////////////////////////////////////////////////////////////////// + // NOTIFICATIONS + ///////////////////////////////////////////////////////////////////////////// private: public: diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 263d61934..9fcf3c089 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -50,8 +50,9 @@ bool TheorySets::needsCheckLastEffort() { return d_internal->needsCheckLastEffort(); } -void TheorySets::collectModelInfo(TheoryModel* m) { - d_internal->collectModelInfo(m); +bool TheorySets::collectModelInfo(TheoryModel* m) +{ + return d_internal->collectModelInfo(m); } void TheorySets::computeCareGraph() { diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 3ecd404bb..1f0fbdd1f 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -52,7 +52,7 @@ public: bool needsCheckLastEffort(); - void collectModelInfo(TheoryModel* m); + bool collectModelInfo(TheoryModel* m) override; void computeCareGraph(); diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 3013711eb..6bafbb0de 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1911,16 +1911,19 @@ EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) { /******************** Model generation ********************/ /******************** Model generation ********************/ - -void TheorySetsPrivate::collectModelInfo(TheoryModel* m) { +bool TheorySetsPrivate::collectModelInfo(TheoryModel* m) +{ Trace("sets-model") << "Set collect model info" << std::endl; set termSet; // Compute terms appearing in assertions and shared terms d_external.computeRelevantTerms(termSet); // Assert equalities and disequalities to the model - m->assertEqualityEngine(&d_equalityEngine,&termSet); - + if (!m->assertEqualityEngine(&d_equalityEngine, &termSet)) + { + return false; + } + std::map< Node, Node > mvals; for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){ Node eqc = d_set_eqc[i]; @@ -1970,10 +1973,14 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m) { rep = Rewriter::rewrite( rep ); Trace("sets-model") << "* Assign representative of " << eqc << " to " << rep << std::endl; mvals[eqc] = rep; - m->assertEquality( eqc, rep, true ); - m->assertRepresentative( rep ); + if (!m->assertEquality(eqc, rep, true)) + { + return false; + } + m->assertSkeleton(rep); } } + return true; } /********************** Helper functions ***************************/ diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 175e82bb8..bd63ff43d 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -178,7 +178,7 @@ public: bool needsCheckLastEffort(); - void collectModelInfo(TheoryModel* m); + bool collectModelInfo(TheoryModel* m); void computeCareGraph(); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 9b259bf97..e6b8807e9 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -447,8 +447,8 @@ void TheoryStrings::presolve() { // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// - -void TheoryStrings::collectModelInfo( TheoryModel* m ) { +bool TheoryStrings::collectModelInfo(TheoryModel* m) +{ Trace("strings-model") << "TheoryStrings : Collect model info" << std::endl; Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl; @@ -458,9 +458,12 @@ void TheoryStrings::collectModelInfo( TheoryModel* m ) { // Compute terms appearing in assertions and shared terms //computeRelevantTerms(termSet); //m->assertEqualityEngine( &d_equalityEngine, &termSet ); - - m->assertEqualityEngine( &d_equalityEngine ); - + + if (!m->assertEqualityEngine(&d_equalityEngine)) + { + return false; + } + // Generate model std::vector< Node > nodes; getEquivalenceClasses( nodes ); @@ -554,7 +557,10 @@ void TheoryStrings::collectModelInfo( TheoryModel* m ) { ++sel; Trace("strings-model") << "*** Assigned constant " << c << " for " << pure_eq[j] << std::endl; processed[pure_eq[j]] = c; - m->assertEquality( pure_eq[j], c, true ); + if (!m->assertEquality(pure_eq[j], c, true)) + { + return false; + } } } } @@ -583,11 +589,15 @@ void TheoryStrings::collectModelInfo( TheoryModel* m ) { Assert( cc.getKind()==kind::CONST_STRING ); Trace("strings-model") << "*** Determined constant " << cc << " for " << nodes[i] << std::endl; processed[nodes[i]] = cc; - m->assertEquality( nodes[i], cc, true ); + if (!m->assertEquality(nodes[i], cc, true)) + { + return false; + } } } //Trace("strings-model") << "String Model : Assigned." << std::endl; Trace("strings-model") << "String Model : Finished." << std::endl; + return true; } ///////////////////////////////////////////////////////////////////////////// diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 39ab70e2f..70706bbd4 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -214,11 +214,11 @@ private: // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// public: - void collectModelInfo(TheoryModel* m); + bool collectModelInfo(TheoryModel* m) override; - ///////////////////////////////////////////////////////////////////////////// - // NOTIFICATIONS - ///////////////////////////////////////////////////////////////////////////// + ///////////////////////////////////////////////////////////////////////////// + // NOTIFICATIONS + ///////////////////////////////////////////////////////////////////////////// public: void presolve(); void shutdown() { } diff --git a/src/theory/theory.h b/src/theory/theory.h index 0f820ac8e..204c514a9 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -512,9 +512,11 @@ public: * Get all relevant information in this theory regarding the current * model. This should be called after a call to check( FULL_EFFORT ) * for all theories with no conflicts and no lemmas added. + * + * This method returns true if and only if the equality engine of m is + * consistent as a result of this call. */ - virtual void collectModelInfo( TheoryModel* m ){ } - + virtual bool collectModelInfo(TheoryModel* m) { return true; } /** if theories want to do something with model after building, do it here */ virtual void postProcessModel( TheoryModel* m ){ } /** diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 944185b31..4e2062c43 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -605,8 +605,6 @@ void TheoryEngine::check(Theory::Effort effort) { if( theory->needsCheckLastEffort() ){ if( !d_curr_model->isBuilt() ){ if( !d_curr_model_builder->buildModel(d_curr_model) ){ - //model building should fail only if the model builder adds lemmas - Assert( needCheck() ); break; } } @@ -617,10 +615,14 @@ void TheoryEngine::check(Theory::Effort effort) { } if( ! d_inConflict && ! needCheck() ){ if(d_logicInfo.isQuantified()) { - // quantifiers engine must pass effort last call check + // quantifiers engine must check at last call effort d_quantEngine->check(Theory::EFFORT_LAST_CALL); - // if returning incomplete or SAT, we have ensured that d_curr_model has been built - } else if(options::produceModels() && !d_curr_model->isBuilt()) { + } + } + if (!d_inConflict && !needCheck()) + { + if (options::produceModels() && !d_curr_model->isBuilt()) + { // must build model at this point d_curr_model_builder->buildModel(d_curr_model); } @@ -631,14 +633,21 @@ void TheoryEngine::check(Theory::Effort effort) { Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl; if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) { - //we will answer SAT + // case where we are about to answer SAT if( d_masterEqualityEngine != NULL ){ AlwaysAssert(d_masterEqualityEngine->consistent()); } - if( options::produceModels() ){ - d_curr_model_builder->debugCheckModel(d_curr_model); - // Do post-processing of model from the theories (used for THEORY_SEP to construct heap model) - postProcessModel(d_curr_model); + if (d_curr_model->isBuilt()) + { + // model construction should always succeed unless lemmas were added + AlwaysAssert(d_curr_model->isBuiltSuccess()); + if (options::produceModels()) + { + d_curr_model_builder->debugCheckModel(d_curr_model); + // Do post-processing of model from the theories (used for THEORY_SEP + // to construct heap model) + postProcessModel(d_curr_model); + } } } } catch(const theory::Interrupted&) { @@ -846,7 +855,8 @@ bool TheoryEngine::properExplanation(TNode node, TNode expl) const { return true; } -void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){ +bool TheoryEngine::collectModelInfo(theory::TheoryModel* m) +{ //have shared term engine collectModelInfo // d_sharedTerms.collectModelInfo( m ); // Consult each active theory to get all relevant information @@ -854,7 +864,10 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){ for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) { if(d_logicInfo.isTheoryEnabled(theoryId)) { Trace("model-builder") << " CollectModelInfo on theory: " << theoryId << endl; - d_theoryTable[theoryId]->collectModelInfo( m ); + if (!d_theoryTable[theoryId]->collectModelInfo(m)) + { + return false; + } } } // Get the Boolean variables @@ -870,8 +883,12 @@ void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){ value = false; } Trace("model-builder-assertions") << "(assert" << (value ? " " : " (not ") << var << (value ? ");" : "));") << endl; - m->assertPredicate(var, value); + if (!m->assertPredicate(var, value)) + { + return false; + } } + return true; } void TheoryEngine::postProcessModel( theory::TheoryModel* m ){ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 179530240..f380e86aa 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -707,7 +707,7 @@ public: /** * collect model info */ - void collectModelInfo( theory::TheoryModel* m ); + bool collectModelInfo(theory::TheoryModel* m); /** post process model */ void postProcessModel( theory::TheoryModel* m ); diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 02dd92ad7..5555e29e2 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -25,8 +25,13 @@ using namespace CVC4::context; namespace CVC4 { namespace theory { -TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncModels) : - d_substitutions(c, false), d_modelBuilt(false), d_enableFuncModels(enableFuncModels) +TheoryModel::TheoryModel(context::Context* c, + std::string name, + bool enableFuncModels) + : d_substitutions(c, false), + d_modelBuilt(false), + d_modelBuiltSuccess(false), + d_enableFuncModels(enableFuncModels) { d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); @@ -53,6 +58,7 @@ TheoryModel::~TheoryModel() throw() { void TheoryModel::reset(){ d_modelBuilt = false; + d_modelBuiltSuccess = false; d_modelCache.clear(); d_comment_str.clear(); d_sep_heap = Node::null(); @@ -333,20 +339,24 @@ void TheoryModel::addTermInternal(TNode n) } /** assert equality */ -void TheoryModel::assertEquality(TNode a, TNode b, bool polarity ){ +bool TheoryModel::assertEquality(TNode a, TNode b, bool polarity) +{ + Assert(d_equalityEngine->consistent()); if (a == b && polarity) { - return; + return true; } Trace("model-builder-assertions") << "(assert " << (polarity ? "(= " : "(not (= ") << a << " " << b << (polarity ? "));" : ")));") << endl; d_equalityEngine->assertEquality( a.eqNode(b), polarity, Node::null() ); - Assert(d_equalityEngine->consistent()); + return d_equalityEngine->consistent(); } /** assert predicate */ -void TheoryModel::assertPredicate(TNode a, bool polarity ){ +bool TheoryModel::assertPredicate(TNode a, bool polarity) +{ + Assert(d_equalityEngine->consistent()); if ((a == d_true && polarity) || (a == d_false && (!polarity))) { - return; + return true; } if (a.getKind() == EQUAL) { Trace("model-builder-assertions") << "(assert " << (polarity ? " " : "(not ") << a << (polarity ? ");" : "));") << endl; @@ -354,13 +364,15 @@ void TheoryModel::assertPredicate(TNode a, bool polarity ){ } else { Trace("model-builder-assertions") << "(assert " << (polarity ? "" : "(not ") << a << (polarity ? ");" : "));") << endl; d_equalityEngine->assertPredicate( a, polarity, Node::null() ); - Assert(d_equalityEngine->consistent()); } + return d_equalityEngine->consistent(); } /** assert equality engine */ -void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set* termSet) +bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, + set* termSet) { + Assert(d_equalityEngine->consistent()); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); for (; !eqcs_i.isFinished(); ++eqcs_i) { Node eqc = (*eqcs_i); @@ -384,11 +396,12 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set* continue; } if (predicate) { - if (predTrue) { - assertPredicate(*eqc_i, true); - } - else if (predFalse) { - assertPredicate(*eqc_i, false); + if (predTrue || predFalse) + { + if (!assertPredicate(*eqc_i, predTrue)) + { + return false; + } } else { if (first) { @@ -398,7 +411,10 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set* else { Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << rep << "));" << endl; d_equalityEngine->mergePredicates(*eqc_i, rep, Node::null()); - Assert(d_equalityEngine->consistent()); + if (!d_equalityEngine->consistent()) + { + return false; + } } } } else { @@ -413,17 +429,22 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set* first = false; } else { - assertEquality(*eqc_i, rep, true); + if (!assertEquality(*eqc_i, rep, true)) + { + return false; + } } } } } + return true; } -void TheoryModel::assertRepresentative(TNode n ) +void TheoryModel::assertSkeleton(TNode n) { - Trace("model-builder-reps") << "Assert rep : " << n << std::endl; - Trace("model-builder-reps") << "Rep eqc is : " << getRepresentative( n ) << std::endl; + Trace("model-builder-reps") << "Assert skeleton : " << n << std::endl; + Trace("model-builder-reps") << "...rep eqc is : " << getRepresentative(n) + << std::endl; d_reps[ n ] = n; } diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 600f511c8..ab844c6ec 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -55,19 +55,25 @@ namespace theory { * * These calls may modify the model object using the interface * functions below, including: - * - assertEquality, assertPredicate, assertRepresentative, + * - assertEquality, assertPredicate, assertSkeleton, * assertEqualityEngine. * - assignFunctionDefinition * - * During and after this building process, these calls may use - * interface functions below to guide the model construction: + * This class provides several interface functions: * - hasTerm, getRepresentative, areEqual, areDisequal * - getEqualityEngine * - getRepSet * - hasAssignedFunctionDefinition, getFunctionsToAssign + * - getValue * - * After this building process, the function getValue can be - * used to query the value of nodes. + * The above functions can be used for a model m after it has been + * successfully built, i.e. when m->isBuiltSuccess() returns true. + * + * Additionally, all of the above functions, with the exception of getValue, + * can be used during step (5) of TheoryEngineModelBuilder::buildModel, as + * documented in theory_model_builder.h. In particular, we make calls to the + * above functions such as getRepresentative() when assigning total + * interpretations for uninterpreted functions. */ class TheoryModel : public Model { @@ -80,7 +86,7 @@ public: virtual void reset(); /** is built * - * Have we (attempted to) build this model since the last + * Have we attempted to build this model since the last * call to reset? Notice for model building techniques * that are not guaranteed to succeed (such as * when quantified formulas are enabled), a true return @@ -88,22 +94,51 @@ public: * current assertions. */ bool isBuilt() { return d_modelBuilt; } + /** is built success + * + * Was this model successfully built since the last call to reset? + */ + bool isBuiltSuccess() { return d_modelBuiltSuccess; } //---------------------------- for building the model /** Adds a substitution from x to t. */ void addSubstitution(TNode x, TNode t, bool invalidateCache = true); - /** assert equality holds in the model */ - void assertEquality(TNode a, TNode b, bool polarity); - /** assert predicate holds in the model */ - void assertPredicate(TNode a, bool polarity); - /** assert all equalities/predicates in equality engine hold in the model */ - void assertEqualityEngine(const eq::EqualityEngine* ee, std::set* termSet = NULL); - /** assert representative - * This function tells the model that n should be the representative of its equivalence class. - * It should be called during model generation, before final representatives are chosen. In the - * case of TheoryEngineModelBuilder, it should be called during Theory's collectModelInfo( ... ) - * functions. - */ - void assertRepresentative(TNode n); + /** assert equality holds in the model + * + * This method returns true if and only if the equality engine of this model + * is consistent after asserting the equality to this model. + */ + bool assertEquality(TNode a, TNode b, bool polarity); + /** assert predicate holds in the model + * + * This method returns true if and only if the equality engine of this model + * is consistent after asserting the predicate to this model. + */ + bool assertPredicate(TNode a, bool polarity); + /** assert all equalities/predicates in equality engine hold in the model + * + * This method returns true if and only if the equality engine of this model + * is consistent after asserting the equality engine to this model. + */ + bool assertEqualityEngine(const eq::EqualityEngine* ee, + std::set* termSet = NULL); + /** assert skeleton + * + * This method gives a "skeleton" for the model value of the equivalence + * class containing n. This should be an application of interpreted function + * (e.g. datatype constructor, array store, set union chain). The subterms of + * this term that are variables or terms that belong to other theories will + * be filled in with model values. + * + * For example, if we call assertSkeleton on (C x y) where C is a datatype + * constructor and x and y are variables, then the equivalence class of + * (C x y) will be interpreted in m as (C x^m y^m) where + * x^m = m->getValue( x ) and y^m = m->getValue( y ). + * + * It should be called during model generation, before final representatives + * are chosen. In the case of TheoryEngineModelBuilder, it should be called + * during Theory's collectModelInfo( ... ) functions. + */ + void assertSkeleton(TNode n); //---------------------------- end building the model // ------------------- general equality queries @@ -171,8 +206,10 @@ public: protected: /** substitution map for this model */ SubstitutionMap d_substitutions; - /** whether this model has been built */ + /** whether we have tried to build this model in the current context */ bool d_modelBuilt; + /** whether this model has been built successfully */ + bool d_modelBuiltSuccess; /** special local context for our equalityEngine so we can clear it * independently of search context */ context::Context* d_eeContext; diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index ac12b37e3..e88d1e3be 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -286,11 +286,15 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) // mark as built tm->d_modelBuilt = true; + tm->d_modelBuiltSuccess = false; // Collect model info from the theories Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl; - d_te->collectModelInfo(tm); + if (!d_te->collectModelInfo(tm)) + { + return false; + } // model-builder specific initialization if (!preProcessBuildModel(tm)) @@ -799,6 +803,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) } else { + tm->d_modelBuiltSuccess = true; return true; } } diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index c24d50cbf..bb74569b7 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -58,7 +58,8 @@ class TheoryEngineModelBuilder : public ModelBuilder * (4) assign constants to all equivalence classes * of m's equality engine, through alternating * iterations of evaluation and enumeration, - * (5) builder-specific post-processing. + * (5) builder-specific processing, which includes assigning total + * interpretations to uninterpreted functions. * * This function returns false if any of the above * steps results in a lemma sent on an output channel. diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index f97a4b639..38ddb1246 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -330,14 +330,18 @@ Node TheoryUF::explain(TNode literal, eq::EqProof* pf) { return mkAnd(assumptions); } -void TheoryUF::collectModelInfo( TheoryModel* m ){ +bool TheoryUF::collectModelInfo(TheoryModel* m) +{ Debug("uf") << "UF : collectModelInfo " << std::endl; set termSet; // Compute terms appearing in assertions and shared terms computeRelevantTerms(termSet); - m->assertEqualityEngine( &d_equalityEngine, &termSet ); + if (!m->assertEqualityEngine(&d_equalityEngine, &termSet)) + { + return false; + } if( options::ufHo() ){ for( std::set::iterator it = termSet.begin(); it != termSet.end(); ++it ){ @@ -345,12 +349,16 @@ void TheoryUF::collectModelInfo( TheoryModel* m ){ if( n.getKind()==kind::APPLY_UF ){ // for model-building with ufHo, we require that APPLY_UF is always expanded to HO_APPLY Node hn = TheoryUfRewriter::getHoApplyForApplyUf( n ); - m->assertEquality( n, hn, true ); + if (!m->assertEquality(n, hn, true)) + { + return false; + } } } } Debug("uf") << "UF : finish collectModelInfo " << std::endl; + return true; } void TheoryUF::presolve() { diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 0665b8272..269aa63db 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -242,7 +242,7 @@ public: void preRegisterTerm(TNode term); Node explain(TNode n); - void collectModelInfo( TheoryModel* m ); + bool collectModelInfo(TheoryModel* m) override; void ppStaticLearn(TNode in, NodeBuilder<>& learned); void presolve(); -- 2.30.2