From 7d298cf9abe3cb09c897eafe6fab5ef636be4c27 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 14 May 2012 19:33:15 +0000 Subject: [PATCH] Fixed assertion failures in array theory This fixes bugs 335 and 333. --- src/theory/arrays/theory_arrays.cpp | 80 ++++++++++++++++--- src/theory/arrays/theory_arrays.h | 3 + test/regress/regress0/arrays/Makefile.am | 1 + .../arrays/swap_t1_np_nf_ai_00005_007.cvc.smt | 23 ++++++ 4 files changed, 97 insertions(+), 10 deletions(-) create mode 100644 test/regress/regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index f073e67d7..3c48c7907 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -59,6 +59,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC // d_ppCache(u), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), + d_isPreRegistered(c), d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual"), d_notify(*this), d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays"), @@ -370,15 +371,18 @@ void TheoryArrays::explain(TNode literal, std::vector& assumptions) { void TheoryArrays::preRegisterTerm(TNode node) { Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl; - switch (node.getKind()) { case kind::EQUAL: // Add the trigger for equality d_equalityEngine.addTriggerEquality(node); break; case kind::SELECT: { + // Invariant: array terms should be preregistered before being added to the equality engine + if (d_equalityEngine.hasTerm(node)) { + Assert(d_isPreRegistered.find(node) != d_isPreRegistered.end()); + return; + } // Reads - d_equalityEngine.addTerm(node); TNode store = d_equalityEngine.getRepresentative(node[0]); // Apply RIntro1 rule to any stores equal to store if not done already @@ -392,7 +396,6 @@ void TheoryArrays::preRegisterTerm(TNode node) Assert(s.getKind()==kind::STORE); Node ni = nm->mkNode(kind::SELECT, s, s[1]); if (ni != node) { - Assert(!d_equalityEngine.hasTerm(ni)); preRegisterTerm(ni); } d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true); @@ -400,6 +403,7 @@ void TheoryArrays::preRegisterTerm(TNode node) } } + d_equalityEngine.addTerm(node); // Maybe it's a predicate // TODO: remove this or keep it if we allow Boolean elements in arrays. if (node.getType().isBoolean()) { @@ -408,11 +412,14 @@ void TheoryArrays::preRegisterTerm(TNode node) } d_infoMap.addIndex(node[0], node[1]); - checkRowForIndex(node[1], store); d_reads.push_back(node); + Assert((d_isPreRegistered.insert(node), true)); + checkRowForIndex(node[1], store); break; } case kind::STORE: { + // Invariant: array terms should be preregistered before being added to the equality engine + Assert(!d_equalityEngine.hasTerm(node)); d_equalityEngine.addTriggerTerm(node); TNode a = node[0]; @@ -440,12 +447,15 @@ void TheoryArrays::preRegisterTerm(TNode node) // Variables etc if (node.getType().isArray()) { d_equalityEngine.addTriggerTerm(node); + Assert(d_equalityEngine.getSize(node) == 1); } else { d_equalityEngine.addTerm(node); } break; } + // Invariant: preregistered terms are exactly the terms in the equality engine + Assert(d_equalityEngine.hasTerm(node)); } @@ -898,7 +908,6 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b) NodeManager* nm = NodeManager::currentNM(); d_infoMap.setRIntro1Applied(s); Node ni = nm->mkNode(kind::SELECT, s, s[1]); - Assert(!d_equalityEngine.hasTerm(ni)); preRegisterTerm(ni); d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true); } @@ -1173,24 +1182,54 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) if (d_eagerLemmas || bothExist) { - Assert(aj == Rewriter::rewrite(aj)); - Assert(bj == Rewriter::rewrite(bj)); + // Make sure that any terms introduced by rewriting are appropriately stored in the equality database + Node aj2 = Rewriter::rewrite(aj); + if (aj != aj2) { + if (!ajExists) { + preRegisterTerm(aj); + } + if (!d_equalityEngine.hasTerm(aj2)) { + preRegisterTerm(aj2); + } + d_equalityEngine.assertEquality(aj.eqNode(aj2), true, d_true); + } + Node bj2 = Rewriter::rewrite(bj); + if (bj != bj2) { + if (!bjExists) { + preRegisterTerm(bj); + } + if (!d_equalityEngine.hasTerm(bj2)) { + preRegisterTerm(bj2); + } + d_equalityEngine.assertEquality(bj.eqNode(bj2), true, d_true); + } + if (aj2 == bj2) { + return; + } // construct lemma - Node eq1 = aj.eqNode(bj); + Node eq1 = aj2.eqNode(bj2); Node eq1_r = Rewriter::rewrite(eq1); if (eq1_r == d_true) { + if (!d_equalityEngine.hasTerm(aj2)) { + preRegisterTerm(aj2); + } + if (!d_equalityEngine.hasTerm(bj2)) { + preRegisterTerm(bj2); + } d_equalityEngine.assertEquality(eq1, true, d_true); return; } Node eq2 = i.eqNode(j); Node eq2_r = Rewriter::rewrite(eq2); - if (eq2 == d_true) { + if (eq2_r == d_true) { d_equalityEngine.assertEquality(eq2, true, d_true); return; } + Node lemma = nm->mkNode(kind::OR, eq2_r, eq1_r); + Trace("arrays-lem")<<"Arrays::addRowLemma adding "<lemma(lemma); @@ -1221,22 +1260,37 @@ void TheoryArrays::dischargeLemmas() NodeManager* nm = NodeManager::currentNM(); Node aj = nm->mkNode(kind::SELECT, a, j); Node bj = nm->mkNode(kind::SELECT, b, j); + bool ajExists = d_equalityEngine.hasTerm(aj); + bool bjExists = d_equalityEngine.hasTerm(bj); // Check for redundant lemma // TODO: more checks possible (i.e. check d_RowAlreadyAdded in context) if (d_equalityEngine.areEqual(i,j) || d_equalityEngine.areEqual(a,b) || - (d_equalityEngine.hasTerm(aj) && d_equalityEngine.hasTerm(bj) && d_equalityEngine.areEqual(aj,bj))) { + (ajExists && bjExists && d_equalityEngine.areEqual(aj,bj))) { d_RowQueue.push(l); continue; } + // Make sure that any terms introduced by rewriting are appropriately stored in the equality database Node aj2 = Rewriter::rewrite(aj); if (aj != aj2) { + if (!ajExists) { + preRegisterTerm(aj); + } + if (!d_equalityEngine.hasTerm(aj2)) { + preRegisterTerm(aj2); + } d_equalityEngine.assertEquality(aj.eqNode(aj2), true, d_true); } Node bj2 = Rewriter::rewrite(bj); if (bj != bj2) { + if (!bjExists) { + preRegisterTerm(bj); + } + if (!d_equalityEngine.hasTerm(bj2)) { + preRegisterTerm(bj2); + } d_equalityEngine.assertEquality(bj.eqNode(bj2), true, d_true); } if (aj2 == bj2) { @@ -1248,6 +1302,12 @@ void TheoryArrays::dischargeLemmas() Node eq1 = aj2.eqNode(bj2); Node eq1_r = Rewriter::rewrite(eq1); if (eq1_r == d_true) { + if (!d_equalityEngine.hasTerm(aj2)) { + preRegisterTerm(aj2); + } + if (!d_equalityEngine.hasTerm(bj2)) { + preRegisterTerm(bj2); + } d_equalityEngine.assertEquality(eq1, true, d_true); d_RowQueue.push(l); continue; diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 88986ee7a..146a2145b 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -165,6 +165,9 @@ class TheoryArrays : public Theory { /** Explain why this literal is true by adding assumptions */ void explain(TNode literal, std::vector& assumptions); + /** For debugging only- checks invariants about when things are preregistered*/ + context::CDHashSet d_isPreRegistered; + public: void preRegisterTerm(TNode n); diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index fcbeb208e..452663456 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -27,6 +27,7 @@ TESTS = \ incorrect9.smt \ incorrect10.smt \ incorrect11.smt \ + swap_t1_np_nf_ai_00005_007.cvc.smt \ x2.smt \ x3.smt diff --git a/test/regress/regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt b/test/regress/regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt new file mode 100644 index 000000000..af609c86f --- /dev/null +++ b/test/regress/regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt @@ -0,0 +1,23 @@ +(benchmark swap + :source { +Benchmarks used in the followin paper: +Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure +Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. +PDPAR'05 +http://www.ai.dist.unige.it/pdpar05/ + + +} + :status unsat +:difficulty { 0 } +:category { crafted } + :logic QF_AX + :extrafuns ((a1 Array)) + :extrafuns ((i0 Index)) + :extrafuns ((i1 Index)) + :extrafuns ((i2 Index)) + :extrafuns ((i3 Index)) + :extrafuns ((i4 Index)) + :formula +(let (?cvc_4 (select a1 i4)) (let (?cvc_5 (select a1 i2)) (let (?cvc_0 (store (store a1 i4 ?cvc_5) i2 ?cvc_4)) (let (?cvc_1 (store (store ?cvc_0 i0 (select ?cvc_0 i3)) i3 (select ?cvc_0 i0))) (let (?cvc_2 (store (store ?cvc_1 i2 (select ?cvc_1 i1)) i1 (select ?cvc_1 i2))) (let (?cvc_3 (store (store ?cvc_2 i4 (select ?cvc_2 i3)) i3 (select ?cvc_2 i4))) (let (?cvc_6 (store (store a1 i2 ?cvc_4) i4 ?cvc_5)) (let (?cvc_7 (store (store ?cvc_6 i0 (select ?cvc_6 i3)) i3 (select ?cvc_6 i0))) (let (?cvc_8 (store (store ?cvc_7 i1 (select ?cvc_7 i2)) i2 (select ?cvc_7 i1))) (let (?cvc_9 (store (store ?cvc_8 i3 (select ?cvc_8 i4)) i4 (select ?cvc_8 i3))) (not (= (store (store ?cvc_3 i3 (select ?cvc_3 i2)) i2 (select ?cvc_3 i3)) (store (store ?cvc_9 i2 (select ?cvc_9 i3)) i3 (select ?cvc_9 i2)))))))))))))) +) -- 2.30.2