diff options
| author | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-04-26 12:55:13 -0400 |
|---|---|---|
| committer | Dejan Jovanović <dejan@cs.nyu.edu> | 2013-05-02 14:47:20 -0400 |
| commit | fb05d8411fdf905550d0bfdef56f4a4c3ed6a8ef (patch) | |
| tree | ecdcda2fc6c9a2e11e8029333e7ca7998cd69d82 /src/theory/arrays | |
| parent | a5d1513db484457ac64a96711088aca1460af62e (diff) | |
* splitLemma to request atoms
* normalizing in bv before bitblasting
Diffstat (limited to 'src/theory/arrays')
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 801893107..9f7419b87 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -588,7 +588,10 @@ void TheoryArrays::computeCareGraph() } } } - if (options::arraysModelBased()) return; + if (options::arraysModelBased()) { + checkModel(EFFORT_COMBINATION); + return; + } if (d_sharedTerms) { vector< pair<TNode, TNode> > currentPairs; @@ -1009,7 +1012,7 @@ void TheoryArrays::checkModel(Effort e) Assert(d_skolemAssertions.empty()); Assert(d_lemmas.empty()); - if (fullEffort(e)) { + if (combination(e)) { // Add constraints for shared terms context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end(), shared_it2; Node modelVal, modelVal2, d; @@ -1294,7 +1297,7 @@ void TheoryArrays::checkModel(Effort e) d_skolemIndex = 0; while (!d_lemmas.empty()) { Debug("arrays-model-based") << "Sending lemma: " << d_lemmas.back() << endl; - d_out->lemma(d_lemmas.back()); + d_out->splitLemma(d_lemmas.back()); #ifdef CVC4_ASSERTIONS Assert(d_lemmasSaved.find(d_lemmas.back()) == d_lemmasSaved.end()); d_lemmasSaved.insert(d_lemmas.back()); @@ -1633,9 +1636,14 @@ bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain, return true; } } - getSatContext()->push(); Node d = node.eqNode(val); - d_decisions.push_back(invert ? d.notNode() : d); + Node r = Rewriter::rewrite(d); + if (r.isConst()) { + d_equalityEngine.assertEquality(d, r == d_true, d_true); + return ((r == d_true) == (!invert)); + } + getSatContext()->push(); + d_decisions.push_back(invert ? d.negate() : d); d_equalityEngine.assertEquality(d, !invert, d_decisions.back()); Debug("arrays-model-based") << "Asserting " << d_decisions.back() << " with explanation " << d_decisions.back() << endl; ++d_numSetModelValSplits; |