diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2016-01-01 12:30:04 -0800 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2016-01-01 12:30:04 -0800 |
| commit | 541c88a37f0880d7ea42a1aaa3a8688fc86ac811 (patch) | |
| tree | d472c4ce579a1a52cb55d33fa1c7f45ec93455fd | |
| parent | 395e05c2c443845c71dd1fdbb3eae26a68f15520 (diff) | |
Added propagation rule for array ext lemmas to aid proofs
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 25 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine_types.h | 1 |
2 files changed, 20 insertions, 6 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index e4ad0e4a2..2863fad8a 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1293,9 +1293,14 @@ void TheoryArrays::check(Effort e) { Node ak = nm->mkNode(kind::SELECT, fact[0][0], k); Node bk = nm->mkNode(kind::SELECT, fact[0][1], k); - Node eq = d_valuation.ensureLiteral(ak.eqNode(bk)); - Assert(eq.getKind() == kind::EQUAL); + Node eq = ak.eqNode(bk); Node lemma = fact[0].orNode(eq.notNode()); + if (options::arraysPropagate() > 0 && d_equalityEngine.hasTerm(ak) && d_equalityEngine.hasTerm(bk)) { + // Propagate witness disequality - might produce a conflict + d_permRef.push_back(lemma); + d_equalityEngine.assertEquality(eq, false, lemma, eq::MERGED_ARRAYS_EXT); + ++d_numProp; + } Trace("arrays-lem")<<"Arrays::addExtLemma " << lemma <<"\n"; d_out->lemma(lemma); ++d_numExt; @@ -1424,11 +1429,19 @@ Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions, bool invert, unsigned } } else if (t.getKind() == kind::OR) { - // Expand explanation resulting from propagating a ROW lemma + // Expand explanation resulting from propagating a ROW or EXT lemma if ((explained.find(t) == explained.end())) { - Assert(t[1].getKind() == kind::EQUAL); - d_equalityEngine.explainEquality(t[1][0], t[1][1], false, conjunctions); - explained.insert(t); + if (t[1].getKind() == kind::EQUAL) { + // ROW lemma + d_equalityEngine.explainEquality(t[1][0], t[1][1], false, conjunctions); + explained.insert(t); + } else { + // EXT lemma + Assert(t[1].getKind() == kind::NOT && t[1][0].getKind() == kind::EQUAL); + Assert(t[0].getKind() == kind::EQUAL); + all.insert(t[0].notNode()); + explained.insert(t); + } } } else { diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h index d91d5e4f2..fb1e73575 100644 --- a/src/theory/uf/equality_engine_types.h +++ b/src/theory/uf/equality_engine_types.h @@ -74,6 +74,7 @@ enum MergeReasonType { /** Theory specific proof rules */ MERGED_ARRAYS_ROW, MERGED_ARRAYS_ROW1, + MERGED_ARRAYS_EXT }; inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { |