summaryrefslogtreecommitdiff
path: root/src/theory/arrays/theory_arrays.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
-rw-r--r--src/theory/arrays/theory_arrays.cpp137
1 files changed, 44 insertions, 93 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 80bcb47dd..1dd74f060 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -23,17 +23,13 @@
#include <map>
#include "theory/rewriter.h"
#include "expr/command.h"
-#include "theory/uf/equality_engine_impl.h"
-
using namespace std;
-
namespace CVC4 {
namespace theory {
namespace arrays {
-
// These are the options that produce the best empirical results on QF_AX benchmarks.
// eagerLemmas = true
// eagerIndexSplitting = false
@@ -58,14 +54,12 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0),
d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0),
d_checkTimer("theory::arrays::checkTime"),
- d_ppNotify(),
- d_ppEqualityEngine(d_ppNotify, u, "theory::arrays::TheoryArraysPP"),
+ d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP"),
d_ppFacts(u),
// d_ppCache(u),
d_literalsToPropagate(c),
d_literalsToPropagateIndex(c, 0),
- d_mayEqualNotify(),
- d_mayEqualEqualityEngine(d_mayEqualNotify, c, "theory::arrays::TheoryArraysMayEqual"),
+ d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual"),
d_notify(*this),
d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays"),
d_conflict(c, false),
@@ -91,14 +85,6 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
- d_ppEqualityEngine.addTerm(d_true);
- d_ppEqualityEngine.addTerm(d_false);
- d_ppEqualityEngine.addTriggerEquality(d_true, d_false, d_false);
-
- d_equalityEngine.addTerm(d_true);
- d_equalityEngine.addTerm(d_false);
- d_equalityEngine.addTriggerEquality(d_true, d_false, d_false);
-
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::SELECT);
if (d_ccStore) {
@@ -281,7 +267,7 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs
case kind::EQUAL:
{
d_ppFacts.push_back(in);
- d_ppEqualityEngine.addEquality(in[0], in[1], in);
+ d_ppEqualityEngine.assertEquality(in, true, in);
if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
outSubstitutions.addSubstitution(in[0], in[1]);
return PP_ASSERT_STATUS_SOLVED;
@@ -299,7 +285,7 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs
in[0].getKind() == kind::IFF );
Node a = in[0][0];
Node b = in[0][1];
- d_ppEqualityEngine.addDisequality(a, b, in);
+ d_ppEqualityEngine.assertEquality(in[0], false, in);
break;
}
default:
@@ -335,10 +321,8 @@ bool TheoryArrays::propagate(TNode literal)
Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
std::vector<TNode> assumptions;
Node negatedLiteral;
- if (normalized != d_false) {
- negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
- assumptions.push_back(negatedLiteral);
- }
+ negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+ assumptions.push_back(negatedLiteral);
explain(literal, assumptions);
d_conflictNode = mkAnd(assumptions);
d_conflict = true;
@@ -357,67 +341,40 @@ bool TheoryArrays::propagate(TNode literal)
void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) {
- TNode lhs, rhs;
- switch (literal.getKind()) {
- case kind::EQUAL:
- lhs = literal[0];
- rhs = literal[1];
- break;
- case kind::SELECT:
- lhs = literal;
- rhs = d_true;
- break;
- case kind::NOT:
- if (literal[0].getKind() == kind::EQUAL) {
- // Disequalities
- d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions);
- return;
- } else {
- // Predicates
- lhs = literal[0];
- rhs = d_false;
- break;
- }
- case kind::CONST_BOOLEAN:
- // we get to explain true = false, since we set false to be the trigger of this
- lhs = d_true;
- rhs = d_false;
- break;
- default:
- Unreachable();
+ // Do the work
+ bool polarity = literal.getKind() != kind::NOT;
+ TNode atom = polarity ? literal : literal[0];
+ if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+ d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+ } else {
+ d_equalityEngine.explainPredicate(atom, polarity, assumptions);
}
- d_equalityEngine.explainEquality(lhs, rhs, assumptions);
}
- /**
- * Stores in d_infoMap the following information for each term a of type array:
- *
- * - all i, such that there exists a term a[i] or a = store(b i v)
- * (i.e. all indices it is being read atl; store(b i v) is implicitly read at
- * position i due to the implicit axiom store(b i v)[i] = v )
- *
- * - all the stores a is congruent to (this information is context dependent)
- *
- * - all store terms of the form store (a i v) (i.e. in which a appears
- * directly; this is invariant because no new store terms are created)
- *
- * Note: completeness depends on having pre-register called on all the input
- * terms before starting to instantiate lemmas.
- */
+/**
+ * Stores in d_infoMap the following information for each term a of type array:
+ *
+ * - all i, such that there exists a term a[i] or a = store(b i v)
+ * (i.e. all indices it is being read atl; store(b i v) is implicitly read at
+ * position i due to the implicit axiom store(b i v)[i] = v )
+ *
+ * - all the stores a is congruent to (this information is context dependent)
+ *
+ * - all store terms of the form store (a i v) (i.e. in which a appears
+ * directly; this is invariant because no new store terms are created)
+ *
+ * Note: completeness depends on having pre-register called on all the input
+ * terms before starting to instantiate lemmas.
+ */
void TheoryArrays::preRegisterTerm(TNode node)
{
Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl;
switch (node.getKind()) {
case kind::EQUAL:
- // Add the terms
- // d_equalityEngine.addTerm(node[0]);
- // d_equalityEngine.addTerm(node[1]);
- d_equalityEngine.addTerm(node);
// Add the trigger for equality
- d_equalityEngine.addTriggerEquality(node[0], node[1], node);
- d_equalityEngine.addTriggerDisequality(node[0], node[1], node.notNode());
+ d_equalityEngine.addTriggerEquality(node);
break;
case kind::SELECT: {
// Reads
@@ -438,7 +395,7 @@ void TheoryArrays::preRegisterTerm(TNode node)
Assert(!d_equalityEngine.hasTerm(ni));
preRegisterTerm(ni);
}
- d_equalityEngine.addEquality(ni, s[2], d_true);
+ d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true);
Assert(++it == stores->end());
}
}
@@ -447,8 +404,7 @@ void TheoryArrays::preRegisterTerm(TNode node)
// TODO: remove this or keep it if we allow Boolean elements in arrays.
if (node.getType().isBoolean()) {
// Get triggered for both equal and dis-equal
- d_equalityEngine.addTriggerEquality(node, d_true, node);
- d_equalityEngine.addTriggerEquality(node, d_false, node.notNode());
+ d_equalityEngine.addTriggerPredicate(node);
}
d_infoMap.addIndex(node[0], node[1]);
@@ -463,7 +419,7 @@ void TheoryArrays::preRegisterTerm(TNode node)
// TNode i = node[1];
// TNode v = node[2];
- d_mayEqualEqualityEngine.addEquality(node, a, d_true);
+ d_mayEqualEqualityEngine.assertEquality(node.eqNode(a), true, d_true);
// NodeManager* nm = NodeManager::currentNM();
// Node ni = nm->mkNode(kind::SELECT, node, i);
@@ -508,10 +464,8 @@ void TheoryArrays::propagate(Effort e)
Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl;
Node negatedLiteral;
std::vector<TNode> assumptions;
- if (normalized != d_false) {
- negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
- assumptions.push_back(negatedLiteral);
- }
+ negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+ assumptions.push_back(negatedLiteral);
explain(literal, assumptions);
d_conflictNode = mkAnd(assumptions);
d_conflict = true;
@@ -727,17 +681,17 @@ void TheoryArrays::check(Effort e) {
// Do the work
switch (fact.getKind()) {
case kind::EQUAL:
- d_equalityEngine.addEquality(fact[0], fact[1], fact);
+ d_equalityEngine.assertEquality(fact, true, fact);
break;
case kind::SELECT:
- d_equalityEngine.addPredicate(fact, true, fact);
+ d_equalityEngine.assertPredicate(fact, true, fact);
break;
case kind::NOT:
if (fact[0].getKind() == kind::SELECT) {
- d_equalityEngine.addPredicate(fact[0], false, fact);
+ d_equalityEngine.assertPredicate(fact[0], false, fact);
} else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1])) {
// Assert the dis-equality
- d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact);
+ d_equalityEngine.assertEquality(fact[0], false, fact);
// Apply ArrDiseq Rule if diseq is between arrays
if(fact[0][0].getType().isArray()) {
@@ -764,7 +718,7 @@ void TheoryArrays::check(Effort e) {
if (!d_equalityEngine.hasTerm(bk)) {
preRegisterTerm(bk);
}
- d_equalityEngine.addDisequality(ak, bk, fact);
+ d_equalityEngine.assertEquality(ak.eqNode(bk), false, fact);
Trace("arrays-lem")<<"Arrays::addExtLemma "<< ak << " /= " << bk <<"\n";
++d_numExt;
}
@@ -807,14 +761,11 @@ Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions)
for (; i < conjunctions.size(); ++i) {
t = conjunctions[i];
- // Remove true node - represents axiomatically true assertion
- if (t == d_true) continue;
-
// Expand explanation resulting from propagating a ROW lemma
if (t.getKind() == kind::OR) {
if ((explained.find(t) == explained.end())) {
Assert(t[1].getKind() == kind::EQUAL);
- d_equalityEngine.explainDisequality(t[1][0], t[1][1], conjunctions);
+ d_equalityEngine.explainEquality(t[1][0], t[1][1], false, conjunctions);
explained.insert(t);
}
continue;
@@ -949,7 +900,7 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b)
Node ni = nm->mkNode(kind::SELECT, s, s[1]);
Assert(!d_equalityEngine.hasTerm(ni));
preRegisterTerm(ni);
- d_equalityEngine.addEquality(ni, s[2], d_true);
+ d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true);
}
}
@@ -1004,7 +955,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
}
}
- d_mayEqualEqualityEngine.addEquality(a, b, d_true);
+ d_mayEqualEqualityEngine.assertEquality(a.eqNode(b), true, d_true);
checkRowLemmas(a,b);
checkRowLemmas(b,a);
@@ -1186,7 +1137,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
if (!bjExists) {
preRegisterTerm(bj);
}
- d_equalityEngine.addEquality(aj, bj, reason);
+ d_equalityEngine.assertEquality(aj.eqNode(bj), true, reason);
++d_numProp;
return;
}
@@ -1194,7 +1145,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n";
Node reason = nm->mkNode(kind::OR, i.eqNode(j), aj.eqNode(bj));
d_permRef.push_back(reason);
- d_equalityEngine.addEquality(i, j, reason);
+ d_equalityEngine.assertEquality(i.eqNode(j), true, reason);
++d_numProp;
return;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback