diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /src/theory/arrays | |
parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) |
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 17 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 8 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 8 |
3 files changed, 15 insertions, 18 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 7946fea59..f9b97d524 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -247,16 +247,14 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck for (j = leftWrites - 1; j > i; --j) { index_j = write_j[1]; if (!ppCheck || !ppDisequal(index_i, index_j)) { - Node hyp2(index_i.getType() == nm->booleanType()? - index_i.iffNode(index_j) : index_i.eqNode(index_j)); + Node hyp2(index_i.eqNode(index_j)); hyp << hyp2.notNode(); } write_j = write_j[0]; } Node r1 = nm->mkNode(kind::SELECT, e1, index_i); - conc = (r1.getType() == nm->booleanType())? - r1.iffNode(write_i[2]) : r1.eqNode(write_i[2]); + conc = r1.eqNode(write_i[2]); if (hyp.getNumChildren() != 0) { if (hyp.getNumChildren() == 1) { conc = hyp.getChild(0).impNode(conc); @@ -356,8 +354,7 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs case kind::NOT: { d_ppFacts.push_back(in); - Assert(in[0].getKind() == kind::EQUAL || - in[0].getKind() == kind::IFF ); + Assert(in[0].getKind() == kind::EQUAL ); Node a = in[0][0]; Node b = in[0][1]; d_ppEqualityEngine.assertEquality(in[0], false, in); @@ -403,7 +400,7 @@ void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions, eq::E TNode atom = polarity ? literal : literal[0]; //eq::EqProof * eqp = new eq::EqProof; // eq::EqProof * eqp = NULL; - if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { + if (atom.getKind() == kind::EQUAL) { d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, proof); } else { d_equalityEngine.explainPredicate(atom, polarity, assumptions, proof); @@ -2235,11 +2232,7 @@ void TheoryArrays::conflict(TNode a, TNode b) { Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl; eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL; - if (a.getKind() == kind::CONST_BOOLEAN) { - d_conflictNode = explain(a.iffNode(b), proof); - } else { - d_conflictNode = explain(a.eqNode(b), proof); - } + d_conflictNode = explain(a.eqNode(b), proof); if (!d_inCheckModel) { ProofArray* proof_array = NULL; diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 77c5928f0..a1d275364 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -296,7 +296,13 @@ class TheoryArrays : public Theory { } bool eqNotifyTriggerPredicate(TNode predicate, bool value) { - Unreachable(); + Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; + // Just forward to arrays + if (value) { + return d_arrays.propagate(predicate); + } else { + return d_arrays.propagate(predicate.notNode()); + } } bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 2726f386b..e63c224a0 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -33,7 +33,7 @@ void setMostFrequentValue(TNode store, TNode value); void setMostFrequentValueCount(TNode store, uint64_t count); static inline Node mkEqNode(Node a, Node b) { - return a.getType().isBoolean() ? a.iffNode(b) : a.eqNode(b); + return a.eqNode(b); } class TheoryArraysRewriter { @@ -377,8 +377,7 @@ public: } break; } - case kind::EQUAL: - case kind::IFF: { + case kind::EQUAL:{ if(node[0] == node[1]) { Trace("arrays-postrewrite") << "Arrays::postRewrite returning true" << std::endl; return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); @@ -483,8 +482,7 @@ public: } break; } - case kind::EQUAL: - case kind::IFF: { + case kind::EQUAL:{ if(node[0] == node[1]) { Trace("arrays-prerewrite") << "Arrays::preRewrite returning true" << std::endl; return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); |