diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-28 16:02:41 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-28 16:02:41 -0500 |
commit | c323481d737d82b4b4b2906afec3200fe223707f (patch) | |
tree | 636834eedc604f26799a7d54c69550e416c291f8 /src/theory/arrays | |
parent | e8bbee7afb039834955aee96d181b499550a28fe (diff) |
Remove arrays lazy rintro option (#4806)
This option has model soundness issues (#4771) and moreover is overall worse performance on SMT-LIB {QF_ABV QF_ABVFP QF_ABVFPLRA QF_ALIA QF_ANIA QF_AUFBV QF_AUFLIA QF_AUFNIA QF_AX}:
Configuration #unsat time #sat time #solved #total
CVC4-072720_def 9428 9405.46 24932 16631.6 34360 35399
CVC4-072720_nalr1 9446 9536.41 24924 16146.3 34370 35399
where def = default, nalr1 = --no-arrays-lazy-rintro1.
Fixes #4771.
FYI @barrettcw
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 122 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 1 |
2 files changed, 9 insertions, 114 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index f008dc2a1..27e49d2ce 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -54,7 +54,6 @@ const bool d_solveWrite2 = false; // These are now options //const bool d_propagateLemmas = true; //bool d_useNonLinearOpt = true; - //bool d_lazyRIntro1 = true; //bool d_eagerIndexSplitting = false; TheoryArrays::TheoryArrays(context::Context* c, @@ -697,26 +696,6 @@ void TheoryArrays::preRegisterTermInternal(TNode node) } Assert((d_isPreRegistered.insert(node), true)); - if (options::arraysLazyRIntro1() && !options::arraysWeakEquivalence()) { - // Apply RIntro1 rule to any stores equal to store if not done already - const CTNodeList* stores = d_infoMap.getStores(store); - CTNodeList::const_iterator it = stores->begin(); - if (it != stores->end()) { - NodeManager* nm = NodeManager::currentNM(); - TNode s = *it; - if (!d_infoMap.rIntro1Applied(s)) { - d_infoMap.setRIntro1Applied(s); - Assert(s.getKind() == kind::STORE); - Node ni = nm->mkNode(kind::SELECT, s, s[1]); - if (ni != node) { - preRegisterTermInternal(ni); - } - d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, d_reasonRow1); - Assert(++it == stores->end()); - } - } - } - Assert(d_equalityEngine.getRepresentative(store) == store); d_infoMap.addIndex(store, node[1]); @@ -772,19 +751,17 @@ void TheoryArrays::preRegisterTermInternal(TNode node) Assert(d_mayEqualEqualityEngine.consistent()); } - if (!options::arraysLazyRIntro1() || options::arraysWeakEquivalence()) { - TNode i = node[1]; - TNode v = node[2]; - NodeManager* nm = NodeManager::currentNM(); - Node ni = nm->mkNode(kind::SELECT, node, i); - if (!d_equalityEngine.hasTerm(ni)) { - preRegisterTermInternal(ni); - } - - // Apply RIntro1 Rule - d_equalityEngine.assertEquality(ni.eqNode(v), true, d_true, d_reasonRow1); + TNode i = node[1]; + TNode v = node[2]; + NodeManager* nm = NodeManager::currentNM(); + Node ni = nm->mkNode(kind::SELECT, node, i); + if (!d_equalityEngine.hasTerm(ni)) { + preRegisterTermInternal(ni); } + // Apply RIntro1 Rule + d_equalityEngine.assertEquality(ni.eqNode(v), true, d_true, d_reasonRow1); + d_infoMap.addStore(node, node); d_infoMap.addInStore(a, node); d_infoMap.setModelRep(node, node); @@ -1662,82 +1639,6 @@ void TheoryArrays::setNonLinear(TNode a) } -/***** - * When two array equivalence classes are merged, we may need to apply RIntro1 to a store in one of the EC's - * Here, we check the stores in a to see if any need RIntro1 applied - * We apply RIntro1 whenever: - * (a) a store becomes equal to another store - * (b) a store becomes equal to any term t such that read(t,i) exists - * (c) a store becomes equal to the root array of the store (i.e. store(store(...store(a,i,v)...)) = a) - */ -void TheoryArrays::checkRIntro1(TNode a, TNode b) -{ - const CTNodeList* astores = d_infoMap.getStores(a); - // Apply RIntro1 if applicable - CTNodeList::const_iterator it = astores->begin(); - - if (it == astores->end()) { - // No stores in this equivalence class - return - return; - } - - ++it; - if (it != astores->end()) { - // More than one store: should have already been applied - Assert(d_infoMap.rIntro1Applied(*it)); - Assert(d_infoMap.rIntro1Applied(*(--it))); - return; - } - - // Exactly one store - see if we need to apply RIntro1 - --it; - TNode s = *it; - Assert(s.getKind() == kind::STORE); - if (d_infoMap.rIntro1Applied(s)) { - // RIntro1 already applied to s - return; - } - - // Should be no reads from this EC - Assert(d_infoMap.getIndices(a)->begin() == d_infoMap.getIndices(a)->end()); - - bool apply = false; - if (d_infoMap.getStores(b)->size() > 0) { - // Case (a): two stores become equal - apply = true; - } - else { - const CTNodeList* i_b = d_infoMap.getIndices(b); - if (i_b->begin() != i_b->end()) { - // Case (b): there are reads from b - apply = true; - } - else { - // Get root array of s - TNode e1 = s[0]; - while (e1.getKind() == kind::STORE) { - e1 = e1[0]; - } - Assert(d_equalityEngine.hasTerm(e1)); - Assert(d_equalityEngine.hasTerm(b)); - if (d_equalityEngine.areEqual(e1, b)) { - apply = true; - } - } - } - - if (apply) { - NodeManager* nm = NodeManager::currentNM(); - d_infoMap.setRIntro1Applied(s); - Node ni = nm->mkNode(kind::SELECT, s, s[1]); - preRegisterTermInternal(ni); - d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, d_reasonRow1); - } -} - - - - void TheoryArrays::mergeArrays(TNode a, TNode b) { // Note: a is the new representative @@ -1760,11 +1661,6 @@ void TheoryArrays::mergeArrays(TNode a, TNode b) Assert(d_equalityEngine.getRepresentative(b) == a); Trace("arrays-merge") << spaces(getSatContext()->getLevel()) << "Arrays::merge: (" << a << ", " << b << ")\n"; - if (options::arraysLazyRIntro1() && !options::arraysWeakEquivalence()) { - checkRIntro1(a, b); - checkRIntro1(b, a); - } - if (options::arraysOptimizeLinear() && !options::arraysWeakEquivalence()) { bool aNL = d_infoMap.isNonLinear(a); bool bNL = d_infoMap.isNonLinear(b); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index a4416ab8c..54acf21a5 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -446,7 +446,6 @@ class TheoryArrays : public Theory { Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true); Node mkAnd(std::vector<TNode>& conjunctions, bool invert = false, unsigned startIndex = 0); void setNonLinear(TNode a); - void checkRIntro1(TNode a, TNode b); Node removeRepLoops(TNode a, TNode rep); Node expandStores(TNode s, std::vector<TNode>& assumptions, bool checkLoop = false, TNode a = TNode(), TNode b = TNode()); void mergeArrays(TNode a, TNode b); |