From 56013a80a76b0d46f6f8497d7570e51877dbf99d Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Wed, 14 Nov 2012 21:54:25 +0000 Subject: [PATCH] bug fixes to models, array rewriter with previously failing testcases --- src/theory/arrays/theory_arrays.cpp | 107 +++++---- src/theory/arrays/theory_arrays.h | 10 +- src/theory/arrays/theory_arrays_rewriter.h | 10 +- src/theory/model.cpp | 12 +- src/theory/model.h | 2 +- test/regress/regress0/aufbv/Makefile.am | 1 + test/regress/regress0/aufbv/fuzz13.smt | 90 ++++++++ test/regress/regress0/auflia/Makefile.am | 5 +- test/regress/regress0/auflia/fuzz02.smt | 244 +++++++++++++++++++++ test/regress/regress0/auflia/fuzz03.smt | 15 ++ test/regress/regress0/auflia/fuzz04.smt | 15 ++ 11 files changed, 452 insertions(+), 59 deletions(-) create mode 100644 test/regress/regress0/aufbv/fuzz13.smt create mode 100644 test/regress/regress0/auflia/fuzz02.smt create mode 100644 test/regress/regress0/auflia/fuzz03.smt create mode 100644 test/regress/regress0/auflia/fuzz04.smt diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 342e67654..3a109b51a 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -423,7 +423,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node, bool internalAssert) Assert(d_equalityEngine.getRepresentative(store) == store); d_infoMap.addIndex(store, node[1]); if (internalAssert) { - d_readsInternal.push_back(node); + d_readsInternal.insert(node); } d_reads.push_back(node); Assert((d_isPreRegistered.insert(node), true)); @@ -445,7 +445,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node, bool internalAssert) NodeManager* nm = NodeManager::currentNM(); Node ni = nm->mkNode(kind::SELECT, node, i); if (!d_equalityEngine.hasTerm(ni)) { - preRegisterTermInternal(ni); + preRegisterTermInternal(ni, false); } // Apply RIntro1 Rule @@ -649,81 +649,80 @@ void TheoryArrays::computeCareGraph() ///////////////////////////////////////////////////////////////////////////// -void TheoryArrays::collectReads(TNode n, set& readSet, set& cache) +void TheoryArrays::collectTerms(TNode n, set& termSet) { - if (cache.find(n) != cache.end()) { + if (termSet.find(n) != termSet.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); + termSet.insert(n); + if (n.getType().isBoolean() || !isLeaf(n)) { + for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) { + collectTerms(*child_it, termSet); + } } - cache.insert(n); } -void TheoryArrays::collectArrays(TNode n, set& arraySet, set& cache) +void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ) { - if (cache.find(n) != cache.end()) { - return; - } - if (n.getType().isArray()) { - arraySet.insert(n); - } - for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) { - collectArrays(*child_it, arraySet, cache); - } - cache.insert(n); -} + set termSet; + set cache; - -void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){ - m->assertEqualityEngine( &d_equalityEngine ); - - std::map > selects; - - set readSet, arraySet; - set readCache, arrayCache; - // Collect all arrays and selects appearing in assertions + // Collect all terms 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, readCache); - collectArrays(*assert_it, arraySet, arrayCache); + collectTerms(*assert_it, termSet); } - // Add arrays and selects that are shared terms + // Add terms 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, readCache); - collectArrays(*shared_it, arraySet, arrayCache); + for (; shared_it != shared_it_end; ++shared_it) { + collectTerms(*shared_it, termSet); } // Add selects that were generated internally - unsigned size = d_readsInternal.size(); - for (unsigned i = 0; i < size; ++i) { - readSet.insert(d_readsInternal[i]); + context::CDHashSet::iterator internal_it = d_readsInternal.begin(), internal_it_end = d_readsInternal.end(); + for (; internal_it != internal_it_end; ++internal_it) { + termSet.insert(*internal_it); } // Go through all equivalence classes and collect relevant arrays and reads std::vector arrays; + std::map > selects; + bool computeRep, isArray; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - bool computeRep; while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); + isArray = eqc.getType().isArray(); computeRep = false; eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ){ Node n = *eqc_i; // If this EC is an array type and it contains something other than STORE nodes, we have to compute a representative explicitly - if (!computeRep && n.getKind() != kind::STORE && arraySet.find(n) != arraySet.end()) { - arrays.push_back(eqc); - computeRep = true; + if (isArray && termSet.find(n) != termSet.end()) { + if (n.getKind() == kind::STORE) { + // Make sure RIntro1 reads are included + termSet.insert(NodeManager::currentNM()->mkNode(kind::SELECT, n, n[1])); + } + else if (!computeRep) { + arrays.push_back(eqc); + computeRep = true; + } } - // If this term is a select, and it appears in an assertion or was generated internally, + ++eqc_i; + } + ++eqcs_i; + } + + eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs_i.isFinished() ){ + Node eqc = (*eqcs_i); + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + Node n = *eqc_i; + // If this term is a select, and it appears in an assertion or was derived from one, // 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()) { + if (n.getKind() == kind::SELECT && termSet.find(n) != termSet.end()) { selects[d_equalityEngine.getRepresentative(n[0])].push_back(n); } ++eqc_i; @@ -731,6 +730,8 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){ ++eqcs_i; } + m->assertEqualityEngine(&d_equalityEngine, &termSet); + NodeManager* nm = NodeManager::currentNM(); Node rep; map defValues; @@ -1259,6 +1260,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) Node i_eq_j = i.eqNode(j); Node reason = nm->mkNode(kind::OR, aj_eq_bj, i_eq_j); d_permRef.push_back(reason); + d_readsInternal.insert(aj); + d_readsInternal.insert(bj); if (!ajExists) { preRegisterTermInternal(aj); } @@ -1301,6 +1304,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) // Make sure that any terms introduced by rewriting are appropriately stored in the equality database Node aj2 = Rewriter::rewrite(aj); if (aj != aj2) { + d_readsInternal.insert(aj); + d_readsInternal.insert(aj2); if (!ajExists) { preRegisterTermInternal(aj); } @@ -1311,6 +1316,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) } Node bj2 = Rewriter::rewrite(bj); if (bj != bj2) { + d_readsInternal.insert(bj); + d_readsInternal.insert(bj2); if (!bjExists) { preRegisterTermInternal(bj); } @@ -1327,6 +1334,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) Node eq1 = aj2.eqNode(bj2); Node eq1_r = Rewriter::rewrite(eq1); if (eq1_r == d_true) { + d_readsInternal.insert(aj2); + d_readsInternal.insert(bj2); if (!d_equalityEngine.hasTerm(aj2)) { preRegisterTermInternal(aj2); } @@ -1401,6 +1410,8 @@ void TheoryArrays::dischargeLemmas() // Make sure that any terms introduced by rewriting are appropriately stored in the equality database Node aj2 = Rewriter::rewrite(aj); if (aj != aj2) { + d_readsInternal.insert(aj); + d_readsInternal.insert(aj2); if (!ajExists) { preRegisterTermInternal(aj); } @@ -1411,6 +1422,8 @@ void TheoryArrays::dischargeLemmas() } Node bj2 = Rewriter::rewrite(bj); if (bj != bj2) { + d_readsInternal.insert(bj); + d_readsInternal.insert(bj2); if (!bjExists) { preRegisterTermInternal(bj); } @@ -1427,6 +1440,8 @@ void TheoryArrays::dischargeLemmas() Node eq1 = aj2.eqNode(bj2); Node eq1_r = Rewriter::rewrite(eq1); if (eq1_r == d_true) { + d_readsInternal.insert(aj2); + d_readsInternal.insert(bj2); if (!d_equalityEngine.hasTerm(aj2)) { preRegisterTermInternal(aj2); } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index a47c8440e..9bf1201f3 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -218,12 +218,12 @@ class TheoryArrays : public Theory { ///////////////////////////////////////////////////////////////////////////// private: - /** Helper functions for collectModelInfo */ - void collectReads(TNode n, std::set& readSet, std::set& cache); - void collectArrays(TNode n, std::set& arraySet, std::set& cache); + /** Helper function for collectModelInfo */ + void collectTerms(TNode n, std::set& termSet); + public: - void collectModelInfo( TheoryModel* m, bool fullModel ); + void collectModelInfo(TheoryModel* m, bool fullModel); ///////////////////////////////////////////////////////////////////////////// // NOTIFICATIONS @@ -337,7 +337,7 @@ class TheoryArrays : public Theory { context::CDHashSet d_sharedOther; context::CDO d_sharedTerms; context::CDList d_reads; - context::CDList d_readsInternal; + context::CDHashSet d_readsInternal; std::hash_map d_diseqCache; // The decision requests we have for the core diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 62782f90e..da479616d 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -306,7 +306,15 @@ public: NodeManager* nm = NodeManager::currentNM(); if (val) { // store(store(a,i,v),i,w) = store(a,i,w) - Node result = nm->mkNode(kind::STORE, store[0], index, value); + Node result; + if (value.getKind() == kind::SELECT && + value[0] == store[0] && + value[1] == index) { + result = store[0]; + } + else { + result = nm->mkNode(kind::STORE, store[0], index, value); + } Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << result << std::endl; return RewriteResponse(REWRITE_DONE, result); } diff --git a/src/theory/model.cpp b/src/theory/model.cpp index a01844f77..0e1d90a74 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -246,9 +246,10 @@ void TheoryModel::assertPredicate( Node a, bool polarity ){ } /** assert equality engine */ -void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){ +void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set* termSet) +{ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); - while( !eqcs_i.isFinished() ){ + for (; !eqcs_i.isFinished(); ++eqcs_i) { Node eqc = (*eqcs_i); bool predicate = false; bool predTrue = false; @@ -259,7 +260,10 @@ void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){ predFalse = ee->areEqual(eqc, d_false); } eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee); - while(!eqc_i.isFinished()) { + for (; !eqc_i.isFinished(); ++eqc_i) { + if (termSet != NULL && termSet->find(*eqc_i) == termSet->end()) { + continue; + } if (predicate) { if (predTrue) { assertPredicate(*eqc_i, true); @@ -275,9 +279,7 @@ void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){ } else { assertEquality(*eqc_i, eqc, true); } - ++eqc_i; } - ++eqcs_i; } } diff --git a/src/theory/model.h b/src/theory/model.h index 5b691d4d9..d17192281 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -92,7 +92,7 @@ public: /** assert predicate holds in the model */ void assertPredicate( Node a, bool polarity ); /** assert all equalities/predicates in equality engine hold in the model */ - void assertEqualityEngine( const eq::EqualityEngine* ee ); + void assertEqualityEngine(const eq::EqualityEngine* ee, std::set* termSet = NULL); /** assert representative * This function tells the model that n should be the representative of its equivalence class. * It should be called during model generation, before final representatives are chosen. In the diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index 1a698b180..c67ce5b00 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -44,6 +44,7 @@ TESTS = \ fuzz10.smt \ fuzz11.smt \ fuzz12.smt \ + fuzz13.smt \ fifo32bc06k08.delta01.smt \ rewrite_bug.smt \ array_rewrite_bug.smt diff --git a/test/regress/regress0/aufbv/fuzz13.smt b/test/regress/regress0/aufbv/fuzz13.smt new file mode 100644 index 000000000..d8c0b8480 --- /dev/null +++ b/test/regress/regress0/aufbv/fuzz13.smt @@ -0,0 +1,90 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:status sat +:extrafuns ((v0 BitVec[9])) +:extrafuns ((v1 BitVec[14])) +:extrafuns ((a2 Array[2:5])) +:extrafuns ((a3 Array[8:5])) +:formula +(let (?e4 bv712[10]) +(let (?e5 (ite (bvslt ?e4 ?e4) bv1[1] bv0[1])) +(let (?e6 (ite (= bv1[1] (extract[2:2] v1)) (sign_extend[5] v0) v1)) +(let (?e7 (store a2 (sign_extend[1] ?e5) (extract[12:8] ?e6))) +(let (?e8 (store ?e7 (zero_extend[1] ?e5) (extract[6:2] v1))) +(let (?e9 (select ?e8 (extract[12:11] v1))) +(let (?e10 (select a2 (extract[2:1] ?e4))) +(let (?e11 (store ?e8 (zero_extend[1] ?e5) ?e10)) +(let (?e12 (select ?e11 (extract[1:0] ?e10))) +(let (?e13 (select a2 (extract[3:2] ?e9))) +(let (?e14 (ite (bvsge (zero_extend[4] ?e10) v0) bv1[1] bv0[1])) +(let (?e15 (bvnand ?e4 (zero_extend[5] ?e13))) +(let (?e16 (ite (bvule ?e12 ?e12) bv1[1] bv0[1])) +(let (?e17 (extract[0:0] ?e5)) +(let (?e18 (zero_extend[0] ?e6)) +(let (?e19 (bvsdiv (zero_extend[9] ?e12) v1)) +(let (?e20 (bvsdiv (zero_extend[9] ?e9) ?e6)) +(flet ($e21 (bvugt v1 (zero_extend[9] ?e12))) +(flet ($e22 (bvuge ?e9 (sign_extend[4] ?e14))) +(flet ($e23 (bvslt ?e6 (sign_extend[9] ?e10))) +(flet ($e24 (bvugt ?e19 v1)) +(flet ($e25 (bvult (sign_extend[4] ?e12) v0)) +(flet ($e26 (= (sign_extend[4] ?e15) v1)) +(flet ($e27 (= ?e19 (sign_extend[9] ?e12))) +(flet ($e28 (bvsge (zero_extend[9] ?e9) ?e6)) +(flet ($e29 (bvuge ?e13 (zero_extend[4] ?e5))) +(flet ($e30 (distinct (zero_extend[4] ?e14) ?e9)) +(flet ($e31 (bvsle (zero_extend[4] ?e14) ?e12)) +(flet ($e32 (bvslt ?e10 ?e12)) +(flet ($e33 (distinct ?e6 ?e18)) +(flet ($e34 (bvsge (sign_extend[4] ?e12) v0)) +(flet ($e35 (bvsge ?e6 (zero_extend[5] v0))) +(flet ($e36 (distinct v0 (sign_extend[4] ?e13))) +(flet ($e37 (= ?e18 (sign_extend[5] v0))) +(flet ($e38 (bvugt ?e16 ?e5)) +(flet ($e39 (bvslt ?e9 (sign_extend[4] ?e16))) +(flet ($e40 (distinct (zero_extend[9] ?e13) ?e19)) +(flet ($e41 (bvsle ?e19 (zero_extend[13] ?e5))) +(flet ($e42 (bvslt (zero_extend[4] ?e12) v0)) +(flet ($e43 (bvugt ?e14 ?e17)) +(flet ($e44 (bvsle (sign_extend[4] ?e14) ?e13)) +(flet ($e45 (bvugt (zero_extend[4] ?e14) ?e12)) +(flet ($e46 (bvsge ?e19 ?e6)) +(flet ($e47 (bvsle ?e10 (zero_extend[4] ?e14))) +(flet ($e48 (bvsle ?e20 (zero_extend[4] ?e4))) +(flet ($e49 (and $e22 $e30)) +(flet ($e50 (or $e38 $e29)) +(flet ($e51 (xor $e41 $e34)) +(flet ($e52 (iff $e21 $e48)) +(flet ($e53 (iff $e46 $e23)) +(flet ($e54 (iff $e33 $e44)) +(flet ($e55 (and $e24 $e43)) +(flet ($e56 (implies $e32 $e31)) +(flet ($e57 (or $e56 $e47)) +(flet ($e58 (xor $e50 $e40)) +(flet ($e59 (or $e57 $e45)) +(flet ($e60 (iff $e42 $e59)) +(flet ($e61 (or $e35 $e36)) +(flet ($e62 (if_then_else $e51 $e60 $e25)) +(flet ($e63 (or $e55 $e54)) +(flet ($e64 (xor $e53 $e39)) +(flet ($e65 (and $e63 $e63)) +(flet ($e66 (or $e61 $e28)) +(flet ($e67 (and $e27 $e27)) +(flet ($e68 (or $e26 $e26)) +(flet ($e69 (or $e65 $e49)) +(flet ($e70 (xor $e58 $e62)) +(flet ($e71 (implies $e68 $e37)) +(flet ($e72 (if_then_else $e52 $e52 $e70)) +(flet ($e73 (implies $e66 $e67)) +(flet ($e74 (xor $e64 $e71)) +(flet ($e75 (and $e73 $e73)) +(flet ($e76 (implies $e72 $e69)) +(flet ($e77 (xor $e76 $e75)) +(flet ($e78 (iff $e77 $e74)) +(flet ($e79 (and $e78 (not (= v1 bv0[14])))) +(flet ($e80 (and $e79 (not (= v1 (bvnot bv0[14]))))) +(flet ($e81 (and $e80 (not (= ?e6 bv0[14])))) +(flet ($e82 (and $e81 (not (= ?e6 (bvnot bv0[14]))))) +$e82 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am index 362209579..ed810eaeb 100644 --- a/test/regress/regress0/auflia/Makefile.am +++ b/test/regress/regress0/auflia/Makefile.am @@ -15,7 +15,10 @@ endif TESTS = \ bug330.smt2 \ bug336.smt2 \ - fuzz01.delta01.smt + fuzz01.delta01.smt \ + fuzz02.smt \ + fuzz03.smt \ + fuzz04.smt EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/auflia/fuzz02.smt b/test/regress/regress0/auflia/fuzz02.smt new file mode 100644 index 000000000..7f34226e7 --- /dev/null +++ b/test/regress/regress0/auflia/fuzz02.smt @@ -0,0 +1,244 @@ +(benchmark fuzzsmt +:logic QF_AUFLIA +:status sat +:extrafuns ((f0 Int Int)) +:extrafuns ((f1 Array Array)) +:extrapreds ((p0 Int Int Int)) +:extrapreds ((p1 Array Array Array)) +:extrafuns ((v0 Int)) +:extrafuns ((v1 Int)) +:extrafuns ((v2 Array)) +:extrafuns ((v3 Array)) +:formula +(let (?e4 1) +(let (?e5 (+ v0 v0)) +(let (?e6 (f0 v0)) +(let (?e7 (ite (p0 ?e6 v1 ?e5) 1 0)) +(let (?e8 (* v0 ?e4)) +(let (?e9 (select v3 ?e6)) +(let (?e10 (select v3 ?e5)) +(let (?e11 (f1 v3)) +(let (?e12 (f1 ?e11)) +(let (?e13 (f1 ?e12)) +(let (?e14 (f1 v2)) +(flet ($e15 (p1 v3 v3 v3)) +(flet ($e16 (p1 ?e11 ?e11 ?e13)) +(flet ($e17 (p1 ?e14 ?e13 ?e12)) +(flet ($e18 (p1 v2 v3 ?e11)) +(flet ($e19 (p0 v1 ?e9 v0)) +(flet ($e20 (p0 ?e8 v1 ?e7)) +(flet ($e21 (> v0 ?e6)) +(flet ($e22 (< ?e5 ?e10)) +(let (?e23 (ite $e20 ?e12 ?e12)) +(let (?e24 (ite $e21 ?e23 v3)) +(let (?e25 (ite $e22 ?e13 ?e12)) +(let (?e26 (ite $e18 v2 ?e24)) +(let (?e27 (ite $e15 ?e11 ?e26)) +(let (?e28 (ite $e22 ?e14 ?e26)) +(let (?e29 (ite $e16 ?e13 ?e23)) +(let (?e30 (ite $e17 ?e11 ?e28)) +(let (?e31 (ite $e19 ?e13 ?e11)) +(let (?e32 (ite $e21 v0 ?e7)) +(let (?e33 (ite $e20 ?e8 v1)) +(let (?e34 (ite $e20 ?e32 ?e32)) +(let (?e35 (ite $e16 v1 ?e8)) +(let (?e36 (ite $e17 ?e6 ?e7)) +(let (?e37 (ite $e19 ?e32 ?e7)) +(let (?e38 (ite $e21 ?e9 ?e8)) +(let (?e39 (ite $e15 ?e10 ?e37)) +(let (?e40 (ite $e19 ?e7 ?e6)) +(let (?e41 (ite $e22 ?e5 ?e8)) +(let (?e42 (ite $e18 ?e32 ?e8)) +(let (?e43 (select ?e13 ?e35)) +(let (?e44 (select ?e26 ?e37)) +(let (?e45 (f1 ?e26)) +(let (?e46 (f1 ?e12)) +(let (?e47 (f1 ?e25)) +(let (?e48 (f1 ?e25)) +(let (?e49 (f1 ?e24)) +(let (?e50 (f1 ?e14)) +(let (?e51 (f1 ?e23)) +(let (?e52 (f1 ?e27)) +(let (?e53 (f1 ?e30)) +(let (?e54 (f1 ?e29)) +(let (?e55 (f1 ?e31)) +(let (?e56 (f1 v3)) +(let (?e57 (f1 ?e50)) +(let (?e58 (f1 ?e13)) +(let (?e59 (f1 ?e11)) +(let (?e60 (f1 ?e12)) +(let (?e61 (f1 ?e28)) +(let (?e62 (f1 ?e49)) +(let (?e63 (f1 v2)) +(let (?e64 (f0 ?e36)) +(let (?e65 (+ v0 ?e36)) +(let (?e66 (- v1 ?e35)) +(let (?e67 (f0 ?e65)) +(let (?e68 (f0 ?e32)) +(let (?e69 (f0 ?e6)) +(let (?e70 (- ?e35 ?e68)) +(let (?e71 (* ?e4 ?e40)) +(let (?e72 (~ ?e42)) +(let (?e73 (- ?e38 ?e37)) +(let (?e74 (~ ?e39)) +(let (?e75 (ite (p0 ?e64 ?e34 ?e70) 1 0)) +(let (?e76 (- ?e10 ?e5)) +(let (?e77 (* ?e41 ?e4)) +(let (?e78 (ite (p0 ?e73 ?e7 ?e34) 1 0)) +(let (?e79 (~ ?e10)) +(let (?e80 (- ?e42 ?e64)) +(let (?e81 (* ?e10 (~ ?e4))) +(let (?e82 (+ ?e9 ?e69)) +(let (?e83 (- ?e34 ?e39)) +(let (?e84 (~ ?e33)) +(let (?e85 (+ ?e43 ?e33)) +(let (?e86 (- ?e37 ?e37)) +(let (?e87 (ite (p0 ?e5 ?e64 ?e83) 1 0)) +(let (?e88 (f0 ?e74)) +(let (?e89 (ite (p0 ?e88 ?e9 ?e73) 1 0)) +(let (?e90 (+ ?e88 ?e80)) +(let (?e91 (- ?e8 ?e8)) +(let (?e92 (~ ?e44)) +(flet ($e93 (p1 ?e52 ?e59 ?e30)) +(flet ($e94 (p1 ?e61 ?e29 ?e46)) +(flet ($e95 (p1 ?e51 ?e50 ?e63)) +(flet ($e96 (p1 ?e13 ?e63 ?e23)) +(flet ($e97 (p1 ?e57 ?e25 ?e57)) +(flet ($e98 (p1 v2 ?e58 ?e31)) +(flet ($e99 (p1 ?e14 ?e28 ?e14)) +(flet ($e100 (p1 ?e62 ?e57 ?e30)) +(flet ($e101 (p1 ?e53 ?e12 ?e62)) +(flet ($e102 (p1 ?e49 ?e12 ?e52)) +(flet ($e103 (p1 ?e46 ?e49 ?e14)) +(flet ($e104 (p1 ?e57 v2 ?e31)) +(flet ($e105 (p1 ?e24 ?e55 ?e14)) +(flet ($e106 (p1 ?e53 ?e59 ?e30)) +(flet ($e107 (p1 v3 ?e11 ?e30)) +(flet ($e108 (p1 ?e56 ?e59 ?e60)) +(flet ($e109 (p1 ?e62 ?e23 ?e55)) +(flet ($e110 (p1 ?e29 ?e59 ?e51)) +(flet ($e111 (p1 ?e30 ?e28 ?e59)) +(flet ($e112 (p1 v2 ?e54 ?e13)) +(flet ($e113 (p1 ?e14 ?e50 ?e48)) +(flet ($e114 (p1 ?e26 ?e60 ?e30)) +(flet ($e115 (p1 ?e27 ?e12 ?e47)) +(flet ($e116 (p1 ?e45 ?e53 ?e62)) +(flet ($e117 (<= ?e91 ?e85)) +(flet ($e118 (>= ?e40 ?e89)) +(flet ($e119 (distinct ?e76 ?e77)) +(flet ($e120 (>= ?e91 ?e5)) +(flet ($e121 (= ?e84 ?e68)) +(flet ($e122 (p0 ?e41 v1 ?e36)) +(flet ($e123 (= ?e77 ?e69)) +(flet ($e124 (> ?e38 ?e10)) +(flet ($e125 (p0 v1 ?e77 ?e5)) +(flet ($e126 (= ?e64 ?e41)) +(flet ($e127 (>= ?e81 ?e40)) +(flet ($e128 (< ?e67 ?e39)) +(flet ($e129 (distinct ?e78 ?e65)) +(flet ($e130 (<= ?e34 ?e33)) +(flet ($e131 (<= ?e72 ?e76)) +(flet ($e132 (> ?e87 ?e88)) +(flet ($e133 (>= ?e92 ?e8)) +(flet ($e134 (>= ?e86 ?e36)) +(flet ($e135 (> ?e32 ?e33)) +(flet ($e136 (distinct ?e90 ?e6)) +(flet ($e137 (< ?e88 ?e35)) +(flet ($e138 (p0 ?e9 ?e38 ?e78)) +(flet ($e139 (> ?e80 ?e32)) +(flet ($e140 (p0 ?e79 ?e91 ?e88)) +(flet ($e141 (p0 ?e75 ?e10 ?e74)) +(flet ($e142 (>= ?e34 ?e39)) +(flet ($e143 (p0 ?e66 ?e67 ?e66)) +(flet ($e144 (= ?e90 ?e39)) +(flet ($e145 (< ?e37 ?e79)) +(flet ($e146 (distinct ?e44 ?e78)) +(flet ($e147 (< ?e83 v0)) +(flet ($e148 (>= ?e7 ?e69)) +(flet ($e149 (>= ?e73 ?e10)) +(flet ($e150 (p0 ?e71 ?e90 ?e65)) +(flet ($e151 (p0 ?e36 ?e33 ?e33)) +(flet ($e152 (> ?e82 ?e80)) +(flet ($e153 (distinct ?e79 ?e10)) +(flet ($e154 (p0 ?e42 ?e64 v0)) +(flet ($e155 (< ?e70 ?e86)) +(flet ($e156 (<= ?e43 ?e7)) +(flet ($e157 (or $e16 $e139)) +(flet ($e158 (if_then_else $e103 $e93 $e141)) +(flet ($e159 (not $e132)) +(flet ($e160 (or $e111 $e100)) +(flet ($e161 (iff $e160 $e134)) +(flet ($e162 (and $e19 $e133)) +(flet ($e163 (and $e146 $e128)) +(flet ($e164 (and $e157 $e156)) +(flet ($e165 (xor $e140 $e155)) +(flet ($e166 (implies $e113 $e153)) +(flet ($e167 (iff $e164 $e102)) +(flet ($e168 (implies $e121 $e116)) +(flet ($e169 (if_then_else $e142 $e119 $e104)) +(flet ($e170 (implies $e129 $e99)) +(flet ($e171 (or $e135 $e161)) +(flet ($e172 (or $e126 $e15)) +(flet ($e173 (implies $e158 $e137)) +(flet ($e174 (iff $e166 $e117)) +(flet ($e175 (iff $e105 $e174)) +(flet ($e176 (not $e125)) +(flet ($e177 (iff $e120 $e171)) +(flet ($e178 (xor $e168 $e149)) +(flet ($e179 (and $e96 $e96)) +(flet ($e180 (and $e130 $e143)) +(flet ($e181 (and $e108 $e20)) +(flet ($e182 (if_then_else $e173 $e159 $e167)) +(flet ($e183 (xor $e118 $e107)) +(flet ($e184 (implies $e98 $e169)) +(flet ($e185 (and $e177 $e136)) +(flet ($e186 (not $e185)) +(flet ($e187 (and $e170 $e138)) +(flet ($e188 (iff $e109 $e147)) +(flet ($e189 (or $e188 $e145)) +(flet ($e190 (implies $e152 $e94)) +(flet ($e191 (if_then_else $e97 $e181 $e163)) +(flet ($e192 (iff $e115 $e190)) +(flet ($e193 (if_then_else $e183 $e172 $e17)) +(flet ($e194 (not $e127)) +(flet ($e195 (iff $e179 $e101)) +(flet ($e196 (iff $e186 $e154)) +(flet ($e197 (if_then_else $e178 $e176 $e150)) +(flet ($e198 (xor $e122 $e124)) +(flet ($e199 (not $e182)) +(flet ($e200 (and $e112 $e197)) +(flet ($e201 (iff $e151 $e184)) +(flet ($e202 (or $e106 $e192)) +(flet ($e203 (iff $e162 $e95)) +(flet ($e204 (and $e199 $e199)) +(flet ($e205 (if_then_else $e131 $e187 $e131)) +(flet ($e206 (xor $e144 $e201)) +(flet ($e207 (and $e18 $e202)) +(flet ($e208 (and $e193 $e22)) +(flet ($e209 (or $e123 $e203)) +(flet ($e210 (not $e196)) +(flet ($e211 (and $e209 $e200)) +(flet ($e212 (xor $e208 $e114)) +(flet ($e213 (xor $e212 $e175)) +(flet ($e214 (and $e148 $e206)) +(flet ($e215 (or $e198 $e210)) +(flet ($e216 (or $e213 $e215)) +(flet ($e217 (xor $e189 $e194)) +(flet ($e218 (and $e214 $e204)) +(flet ($e219 (and $e211 $e21)) +(flet ($e220 (and $e165 $e191)) +(flet ($e221 (xor $e180 $e180)) +(flet ($e222 (and $e218 $e205)) +(flet ($e223 (iff $e195 $e219)) +(flet ($e224 (not $e221)) +(flet ($e225 (iff $e222 $e220)) +(flet ($e226 (implies $e225 $e223)) +(flet ($e227 (not $e207)) +(flet ($e228 (if_then_else $e226 $e226 $e216)) +(flet ($e229 (iff $e217 $e110)) +(flet ($e230 (not $e229)) +(flet ($e231 (if_then_else $e224 $e230 $e227)) +(flet ($e232 (or $e231 $e228)) +$e232 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + diff --git a/test/regress/regress0/auflia/fuzz03.smt b/test/regress/regress0/auflia/fuzz03.smt new file mode 100644 index 000000000..151250a1f --- /dev/null +++ b/test/regress/regress0/auflia/fuzz03.smt @@ -0,0 +1,15 @@ +(benchmark fuzzsmt +:logic QF_AUFLIA +:extrapreds ((p1 Array Array Array)) +:extrafuns ((v1 Array)) +:extrafuns ((f1 Array Array Array Array)) +:status sat +:formula +(let (?n1 0) +(let (?n2 (store v1 ?n1 ?n1)) +(let (?n3 (f1 v1 v1 ?n2)) +(let (?n4 (f1 v1 ?n2 v1)) +(let (?n5 (f1 v1 ?n4 ?n2)) +(flet ($n6 (p1 ?n3 ?n5 v1)) +$n6 +))))))) diff --git a/test/regress/regress0/auflia/fuzz04.smt b/test/regress/regress0/auflia/fuzz04.smt new file mode 100644 index 000000000..7523aae28 --- /dev/null +++ b/test/regress/regress0/auflia/fuzz04.smt @@ -0,0 +1,15 @@ +(benchmark fuzzsmt +:logic QF_AUFLIA +:extrapreds ((p1 Array Array)) +:extrafuns ((f1 Array Array Array Array)) +:extrafuns ((v3 Array)) +:status sat +:formula +(let (?n1 (f1 v3 v3 v3)) +(let (?n2 0) +(let (?n3 (store v3 ?n2 ?n2)) +(let (?n4 (f1 v3 v3 ?n3)) +(let (?n5 (f1 v3 ?n4 v3)) +(flet ($n6 (p1 ?n1 ?n5)) +$n6 +))))))) -- 2.30.2