From c323481d737d82b4b4b2906afec3200fe223707f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 28 Jul 2020 16:02:41 -0500 Subject: [PATCH] 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 --- src/options/arrays_options.toml | 8 -- src/smt/set_defaults.cpp | 1 - src/theory/arrays/theory_arrays.cpp | 122 ++-------------------------- src/theory/arrays/theory_arrays.h | 1 - 4 files changed, 9 insertions(+), 123 deletions(-) diff --git a/src/options/arrays_options.toml b/src/options/arrays_options.toml index 389bb6e4c..309370163 100644 --- a/src/options/arrays_options.toml +++ b/src/options/arrays_options.toml @@ -10,14 +10,6 @@ header = "options/arrays_options.h" default = "true" help = "turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper)" -[[option]] - name = "arraysLazyRIntro1" - category = "regular" - long = "arrays-lazy-rintro1" - type = "bool" - default = "true" - help = "turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination)" - [[option]] name = "arraysWeakEquivalence" category = "regular" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 8f6ab6c18..fa96d522c 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1317,7 +1317,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) || options::checkModels()) { options::arraysOptimizeLinear.set(false); - options::arraysLazyRIntro1.set(false); } if (options::proof()) 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& 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& assumptions, bool checkLoop = false, TNode a = TNode(), TNode b = TNode()); void mergeArrays(TNode a, TNode b); -- 2.30.2