From 3544ad31b067fe6c54fcd34c058646852ef8d605 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Sat, 10 Nov 2012 20:15:24 +0000 Subject: [PATCH] Fixed missing \ in uflra/Makefile.ma Fixed another model bug and added previously failing fuzz testcase --- src/theory/arrays/theory_arrays.cpp | 91 ++++++++++++---- src/theory/arrays/theory_arrays.h | 6 ++ src/theory/model.cpp | 3 +- test/regress/regress0/aufbv/Makefile.am | 1 + test/regress/regress0/aufbv/fuzz11.smt | 131 ++++++++++++++++++++++++ test/regress/regress0/uflra/Makefile.am | 3 +- 6 files changed, 210 insertions(+), 25 deletions(-) create mode 100644 test/regress/regress0/aufbv/fuzz11.smt diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 4931a18f0..b9f027afa 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -79,6 +79,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC d_sharedOther(c), d_sharedTerms(c, false), d_reads(c), + d_readsInternal(c), d_decisionRequests(c), d_permRef(c) { @@ -362,7 +363,7 @@ void TheoryArrays::explain(TNode literal, std::vector& assumptions) { * Note: completeness depends on having pre-register called on all the input * terms before starting to instantiate lemmas. */ -void TheoryArrays::preRegisterTerm(TNode node) +void TheoryArrays::preRegisterTermInternal(TNode node, bool internalAssert) { if (d_conflict) { return; @@ -398,7 +399,7 @@ void TheoryArrays::preRegisterTerm(TNode node) Assert(s.getKind()==kind::STORE); Node ni = nm->mkNode(kind::SELECT, s, s[1]); if (ni != node) { - preRegisterTerm(ni); + preRegisterTermInternal(ni); } d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true); Assert(++it == stores->end()); @@ -421,6 +422,9 @@ void TheoryArrays::preRegisterTerm(TNode node) Assert(d_equalityEngine.getRepresentative(store) == store); d_infoMap.addIndex(store, node[1]); + if (internalAssert) { + d_readsInternal.push_back(node); + } d_reads.push_back(node); Assert((d_isPreRegistered.insert(node), true)); checkRowForIndex(node[1], store); @@ -441,7 +445,7 @@ void TheoryArrays::preRegisterTerm(TNode node) NodeManager* nm = NodeManager::currentNM(); Node ni = nm->mkNode(kind::SELECT, node, i); if (!d_equalityEngine.hasTerm(ni)) { - preRegisterTerm(ni); + preRegisterTermInternal(ni); } // Apply RIntro1 Rule @@ -471,6 +475,12 @@ void TheoryArrays::preRegisterTerm(TNode node) } +void TheoryArrays::preRegisterTerm(TNode node) +{ + preRegisterTermInternal(node, false); +} + + void TheoryArrays::propagate(Effort e) { // direct propagation now @@ -638,13 +648,49 @@ void TheoryArrays::computeCareGraph() // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// + +void TheoryArrays::collectReads(TNode n, set& readSet, set& cache) +{ + if (cache.find(n) != cache.end()) { + return; + } + if (n.getKind() == kind::SELECT) { + readSet.insert(n); + } + for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) { + collectReads(*child_it, readSet, cache); + } + cache.insert(n); +} + + void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){ m->assertEqualityEngine( &d_equalityEngine ); std::map > selects; - std::vector arrays; - // Go through all equivalence classes + set readSet; + set cache; + // Collect all selects appearing in assertions + context::CDList::const_iterator assert_it = facts_begin(), assert_it_end = facts_end(); + for (; assert_it != assert_it_end; ++assert_it) { + collectReads(*assert_it, readSet, cache); + } + + // Add selects that are shared terms + context::CDList::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end(); + for (; shared_it != shared_it_end; ++ shared_it) { + collectReads(*shared_it, readSet, cache); + } + + // Add selects that were generated internally + unsigned size = d_readsInternal.size(); + for (unsigned i = 0; i < size; ++i) { + readSet.insert(d_readsInternal[i]); + } + + // Go through all equivalence classes and collect relevant arrays and reads + std::vector arrays; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); bool isArray, computeRep; while( !eqcs_i.isFinished() ){ @@ -659,8 +705,9 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){ arrays.push_back(eqc); computeRep = true; } - // If this term is a select, record that the EC rep of its store parameter is being read from using this term - if (n.getKind()==kind::SELECT) { + // If this term is a select, and it appears in an assertion or was generated internally, + // record that the EC rep of its store parameter is being read from using this term + if (n.getKind() == kind::SELECT && readSet.find(n) != readSet.end()) { selects[d_equalityEngine.getRepresentative(n[0])].push_back(n); } ++eqc_i; @@ -966,7 +1013,7 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b) NodeManager* nm = NodeManager::currentNM(); d_infoMap.setRIntro1Applied(s); Node ni = nm->mkNode(kind::SELECT, s, s[1]); - preRegisterTerm(ni); + preRegisterTermInternal(ni); d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true); } } @@ -1202,10 +1249,10 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) Node reason = nm->mkNode(kind::OR, aj_eq_bj, i_eq_j); d_permRef.push_back(reason); if (!ajExists) { - preRegisterTerm(aj); + preRegisterTermInternal(aj); } if (!bjExists) { - preRegisterTerm(bj); + preRegisterTermInternal(bj); } d_equalityEngine.assertEquality(aj_eq_bj, true, reason); ++d_numProp; @@ -1244,20 +1291,20 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) Node aj2 = Rewriter::rewrite(aj); if (aj != aj2) { if (!ajExists) { - preRegisterTerm(aj); + preRegisterTermInternal(aj); } if (!d_equalityEngine.hasTerm(aj2)) { - preRegisterTerm(aj2); + preRegisterTermInternal(aj2); } d_equalityEngine.assertEquality(aj.eqNode(aj2), true, d_true); } Node bj2 = Rewriter::rewrite(bj); if (bj != bj2) { if (!bjExists) { - preRegisterTerm(bj); + preRegisterTermInternal(bj); } if (!d_equalityEngine.hasTerm(bj2)) { - preRegisterTerm(bj2); + preRegisterTermInternal(bj2); } d_equalityEngine.assertEquality(bj.eqNode(bj2), true, d_true); } @@ -1270,10 +1317,10 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) Node eq1_r = Rewriter::rewrite(eq1); if (eq1_r == d_true) { if (!d_equalityEngine.hasTerm(aj2)) { - preRegisterTerm(aj2); + preRegisterTermInternal(aj2); } if (!d_equalityEngine.hasTerm(bj2)) { - preRegisterTerm(bj2); + preRegisterTermInternal(bj2); } d_equalityEngine.assertEquality(eq1, true, d_true); return; @@ -1344,20 +1391,20 @@ void TheoryArrays::dischargeLemmas() Node aj2 = Rewriter::rewrite(aj); if (aj != aj2) { if (!ajExists) { - preRegisterTerm(aj); + preRegisterTermInternal(aj); } if (!d_equalityEngine.hasTerm(aj2)) { - preRegisterTerm(aj2); + preRegisterTermInternal(aj2); } d_equalityEngine.assertEquality(aj.eqNode(aj2), true, d_true); } Node bj2 = Rewriter::rewrite(bj); if (bj != bj2) { if (!bjExists) { - preRegisterTerm(bj); + preRegisterTermInternal(bj); } if (!d_equalityEngine.hasTerm(bj2)) { - preRegisterTerm(bj2); + preRegisterTermInternal(bj2); } d_equalityEngine.assertEquality(bj.eqNode(bj2), true, d_true); } @@ -1370,10 +1417,10 @@ void TheoryArrays::dischargeLemmas() Node eq1_r = Rewriter::rewrite(eq1); if (eq1_r == d_true) { if (!d_equalityEngine.hasTerm(aj2)) { - preRegisterTerm(aj2); + preRegisterTermInternal(aj2); } if (!d_equalityEngine.hasTerm(bj2)) { - preRegisterTerm(bj2); + preRegisterTermInternal(bj2); } d_equalityEngine.assertEquality(eq1, true, d_true); continue; diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 92e04ed24..8358fe6c9 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -177,6 +177,9 @@ class TheoryArrays : public Theory { /** For debugging only- checks invariants about when things are preregistered*/ context::CDHashSet d_isPreRegistered; + /** Helper for preRegisterTerm, also used internally */ + void preRegisterTermInternal(TNode n, bool internalAssert = true); + public: void preRegisterTerm(TNode n); @@ -215,6 +218,8 @@ class TheoryArrays : public Theory { ///////////////////////////////////////////////////////////////////////////// private: + /** Helper function for collectModelInfo */ + void collectReads(TNode n, std::set& readSet, std::set& cache); public: void collectModelInfo( TheoryModel* m, bool fullModel ); @@ -331,6 +336,7 @@ class TheoryArrays : public Theory { context::CDHashSet d_sharedOther; context::CDO d_sharedTerms; context::CDList d_reads; + context::CDList d_readsInternal; std::hash_map d_diseqCache; // The decision requests we have for the core diff --git a/src/theory/model.cpp b/src/theory/model.cpp index e79c2c479..6363cfb27 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -365,8 +365,7 @@ bool TheoryEngineModelBuilder::isAssignable(TNode n) void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cache) { - NodeSet::iterator it = cache.find(n); - if (it != cache.end()) { + if (cache.find(n) != cache.end()) { return; } if (isAssignable(n)) { diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index 5e8f9ee5c..38c8cf924 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -42,6 +42,7 @@ TESTS = \ fuzz08.smt \ fuzz09.smt \ fuzz10.smt \ + fuzz11.smt \ fifo32bc06k08.delta01.smt \ rewrite_bug.smt diff --git a/test/regress/regress0/aufbv/fuzz11.smt b/test/regress/regress0/aufbv/fuzz11.smt new file mode 100644 index 000000000..4e0056470 --- /dev/null +++ b/test/regress/regress0/aufbv/fuzz11.smt @@ -0,0 +1,131 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:status sat +:extrafuns ((v0 BitVec[11])) +:extrafuns ((v1 BitVec[2])) +:extrafuns ((v2 BitVec[9])) +:extrafuns ((a3 Array[9:10])) +:extrafuns ((a4 Array[9:14])) +:extrafuns ((a5 Array[13:4])) +:formula +(let (?e6 bv28452[16]) +(let (?e7 (bvnand ?e6 (zero_extend[7] v2))) +(let (?e8 (bvurem (sign_extend[7] v1) v2)) +(let (?e9 (ite (bvult (zero_extend[7] v2) ?e7) bv1[1] bv0[1])) +(let (?e10 (bvmul (sign_extend[14] v1) ?e6)) +(let (?e11 (bvcomp v0 (sign_extend[2] v2))) +(let (?e12 (select a3 (extract[8:0] v0))) +(let (?e13 (select a4 (extract[9:1] ?e12))) +(let (?e14 (select a3 (extract[11:3] ?e10))) +(let (?e15 (select a4 (extract[8:0] ?e12))) +(let (?e16 (bvmul v0 v0)) +(let (?e17 (ite (bvsge ?e14 (zero_extend[8] v1)) bv1[1] bv0[1])) +(let (?e18 (bvsmod (zero_extend[6] ?e14) ?e10)) +(let (?e19 (repeat[1] ?e15)) +(let (?e20 (bvurem (sign_extend[12] v1) ?e19)) +(let (?e21 (bvnand (sign_extend[6] ?e12) ?e7)) +(let (?e22 (ite (bvslt (sign_extend[2] ?e20) ?e18) bv1[1] bv0[1])) +(let (?e23 (ite (bvult (sign_extend[9] ?e11) ?e12) bv1[1] bv0[1])) +(let (?e24 (ite (bvuge (zero_extend[1] ?e9) v1) bv1[1] bv0[1])) +(let (?e25 (ite (distinct ?e6 (sign_extend[2] ?e15)) bv1[1] bv0[1])) +(let (?e26 (ite (bvult ?e13 (zero_extend[3] v0)) bv1[1] bv0[1])) +(let (?e27 (bvand ?e8 (zero_extend[8] ?e9))) +(let (?e28 (bvxor (sign_extend[2] v2) v0)) +(flet ($e29 (bvuge (zero_extend[2] ?e19) ?e10)) +(flet ($e30 (bvult ?e10 (sign_extend[2] ?e20))) +(flet ($e31 (bvuge ?e23 ?e24)) +(flet ($e32 (bvule (sign_extend[15] ?e23) ?e6)) +(flet ($e33 (bvsge (zero_extend[6] ?e12) ?e10)) +(flet ($e34 (bvule ?e9 ?e9)) +(flet ($e35 (bvugt ?e15 (sign_extend[13] ?e23))) +(flet ($e36 (bvsge ?e8 (zero_extend[8] ?e17))) +(flet ($e37 (bvule ?e20 (zero_extend[3] v0))) +(flet ($e38 (bvsle ?e15 (zero_extend[5] ?e8))) +(flet ($e39 (bvuge ?e17 ?e11)) +(flet ($e40 (bvuge ?e26 ?e26)) +(flet ($e41 (bvslt (sign_extend[10] ?e23) v0)) +(flet ($e42 (bvule (sign_extend[2] ?e13) ?e7)) +(flet ($e43 (bvugt ?e25 ?e26)) +(flet ($e44 (= (sign_extend[12] v1) ?e15)) +(flet ($e45 (distinct (zero_extend[13] ?e26) ?e13)) +(flet ($e46 (bvsge ?e26 ?e24)) +(flet ($e47 (bvsgt ?e7 ?e18)) +(flet ($e48 (bvugt (zero_extend[3] v0) ?e19)) +(flet ($e49 (bvslt ?e18 (zero_extend[15] ?e17))) +(flet ($e50 (bvuge ?e14 (sign_extend[9] ?e25))) +(flet ($e51 (distinct (sign_extend[15] ?e23) ?e6)) +(flet ($e52 (= ?e8 (sign_extend[8] ?e25))) +(flet ($e53 (bvule ?e14 ?e12)) +(flet ($e54 (bvsle (sign_extend[8] ?e25) ?e8)) +(flet ($e55 (bvuge (sign_extend[14] v1) ?e6)) +(flet ($e56 (= (zero_extend[2] ?e13) ?e7)) +(flet ($e57 (bvult ?e20 (sign_extend[3] ?e28))) +(flet ($e58 (= (sign_extend[1] ?e22) v1)) +(flet ($e59 (bvslt ?e6 (sign_extend[15] ?e23))) +(flet ($e60 (bvuge ?e22 ?e17)) +(flet ($e61 (bvsle (sign_extend[2] v2) v0)) +(flet ($e62 (bvsge (sign_extend[13] ?e11) ?e13)) +(flet ($e63 (bvugt (sign_extend[15] ?e11) ?e7)) +(flet ($e64 (distinct ?e27 (zero_extend[8] ?e17))) +(flet ($e65 (bvult (zero_extend[1] ?e9) v1)) +(flet ($e66 (bvslt ?e26 ?e22)) +(flet ($e67 (= ?e12 (sign_extend[9] ?e25))) +(flet ($e68 (bvugt (sign_extend[3] ?e16) ?e13)) +(flet ($e69 (bvsgt (sign_extend[8] ?e9) ?e27)) +(flet ($e70 (bvsgt (zero_extend[15] ?e11) ?e21)) +(flet ($e71 (iff $e36 $e60)) +(flet ($e72 (iff $e59 $e35)) +(flet ($e73 (and $e70 $e66)) +(flet ($e74 (or $e69 $e57)) +(flet ($e75 (if_then_else $e62 $e64 $e47)) +(flet ($e76 (if_then_else $e56 $e52 $e73)) +(flet ($e77 (and $e58 $e49)) +(flet ($e78 (xor $e72 $e30)) +(flet ($e79 (not $e54)) +(flet ($e80 (iff $e45 $e34)) +(flet ($e81 (iff $e38 $e37)) +(flet ($e82 (or $e40 $e74)) +(flet ($e83 (not $e42)) +(flet ($e84 (and $e29 $e77)) +(flet ($e85 (if_then_else $e41 $e76 $e48)) +(flet ($e86 (iff $e53 $e44)) +(flet ($e87 (if_then_else $e82 $e46 $e50)) +(flet ($e88 (or $e78 $e79)) +(flet ($e89 (and $e87 $e88)) +(flet ($e90 (not $e51)) +(flet ($e91 (xor $e65 $e84)) +(flet ($e92 (or $e75 $e31)) +(flet ($e93 (not $e68)) +(flet ($e94 (or $e67 $e67)) +(flet ($e95 (or $e85 $e89)) +(flet ($e96 (if_then_else $e61 $e32 $e83)) +(flet ($e97 (or $e71 $e71)) +(flet ($e98 (not $e94)) +(flet ($e99 (if_then_else $e97 $e33 $e98)) +(flet ($e100 (implies $e43 $e43)) +(flet ($e101 (implies $e91 $e100)) +(flet ($e102 (and $e101 $e90)) +(flet ($e103 (or $e39 $e95)) +(flet ($e104 (if_then_else $e86 $e99 $e80)) +(flet ($e105 (iff $e102 $e96)) +(flet ($e106 (or $e63 $e63)) +(flet ($e107 (iff $e103 $e103)) +(flet ($e108 (implies $e93 $e55)) +(flet ($e109 (implies $e105 $e81)) +(flet ($e110 (if_then_else $e104 $e104 $e109)) +(flet ($e111 (and $e107 $e110)) +(flet ($e112 (if_then_else $e108 $e106 $e106)) +(flet ($e113 (or $e92 $e92)) +(flet ($e114 (not $e113)) +(flet ($e115 (iff $e114 $e114)) +(flet ($e116 (iff $e115 $e111)) +(flet ($e117 (and $e112 $e112)) +(flet ($e118 (not $e116)) +(flet ($e119 (implies $e117 $e118)) +(flet ($e120 (and $e119 (not (= v2 bv0[9])))) +(flet ($e121 (and $e120 (not (= ?e19 bv0[14])))) +(flet ($e122 (and $e121 (not (= ?e10 bv0[16])))) +(flet ($e123 (and $e122 (not (= ?e10 (bvnot bv0[16]))))) +$e123 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index f4797a287..86a1a9431 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -34,9 +34,10 @@ SMT_TESTS = \ incorrect2.smt \ incorrect1.smt \ incorrect1.delta01.smt \ - incorrect1.delta02.smt + incorrect1.delta02.smt \ error1.smt \ neq-deltacomp.smt + # Regression tests for SMT2 inputs SMT2_TESTS = -- 2.30.2