diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-08 10:14:31 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-12-08 10:14:31 -0600 |
commit | 564234963dd7e76c8d9b88ef941a6683694e5b53 (patch) | |
tree | 313e46520c07d1536fffbad4b7080937cfc09aae /src/theory/theory_model.cpp | |
parent | 805d4b7483e51a9b4d24058d493f85700a87f099 (diff) |
Make collect model info return a Bool (#1421)
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 59 |
1 files changed, 40 insertions, 19 deletions
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<Node>* termSet) +bool TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, + set<Node>* 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<Node>* 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<Node>* 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<Node>* 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; } |