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/arrays | |
parent | 805d4b7483e51a9b4d24058d493f85700a87f099 (diff) |
Make collect model info return a Bool (#1421)
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 16 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 9 |
2 files changed, 15 insertions, 10 deletions
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<Node> 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<Node, std::vector<Node> > 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: |