From db35c4be8bd37746e1c27e446291c82556df1d05 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Fri, 16 Nov 2012 20:14:07 +0000 Subject: [PATCH] Fix for bug451 --- src/smt/smt_engine.cpp | 78 +++++++++++++++++++++++-- test/regress/regress0/aufbv/Makefile.am | 1 + test/regress/regress0/aufbv/bug451.smt | 67 +++++++++++++++++++++ 3 files changed, 141 insertions(+), 5 deletions(-) create mode 100644 test/regress/regress0/aufbv/bug451.smt diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 425892583..6058c66d7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -296,6 +296,12 @@ private: */ void removeITEs(); + /** + * Helper function to fix up assertion list to restore invariants needed after ite removal + */ + bool checkForBadSkolems(TNode n, TNode skolem, hash_map& cache); + + // Simplify ITE structure void simpITE(); @@ -1974,6 +1980,41 @@ Result SmtEngine::quickCheck() { return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK); } + +bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map& cache) +{ + hash_map::iterator it; + it = cache.find(n); + if (it != cache.end()) { + return (*it).second; + } + + size_t sz = n.getNumChildren(); + if (sz == 0) { + IteSkolemMap::iterator it = d_iteSkolemMap.find(n); + bool bad = false; + if (it != d_iteSkolemMap.end()) { + if (!((*it).first < n)) { + bad = true; + } + } + cache[n] = bad; + return bad; + } + + size_t k = 0; + for (; k < sz; ++k) { + if (checkForBadSkolems(n[k], skolem, cache)) { + cache[n] = true; + return true; + } + } + + cache[n] = false; + return false; +} + + void SmtEnginePrivate::processAssertions() { Assert(d_smt.d_fullyInited); Assert(d_smt.d_pendingPops == 0); @@ -2105,19 +2146,43 @@ void SmtEnginePrivate::processAssertions() { Chat() << "simplifying assertions..." << endl; noConflict &= simplifyAssertions(); if (noConflict) { - // Some skolem variables may have been solved for - which is a good thing - - // but it means we have to move those ITE's back to the main set of assertions + // Need to fix up assertion list to maintain invariants: + // Let Sk be the set of Skolem variables introduced by ITE's. Let <_sk be the order in which these variables were introduced + // during ite removal. + // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk. We need to ensure: + // 1. iteExpr has the form (ite cond (sk = t) (sk = e)) + // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk + // If either of these is violated, we must add iteExpr as a proper assertion IteSkolemMap::iterator it = d_iteSkolemMap.begin(); IteSkolemMap::iterator iend = d_iteSkolemMap.end(); NodeBuilder<> builder(kind::AND); builder << d_assertionsToCheck[d_realAssertionsEnd - 1]; + vector toErase; for (; it != iend; ++it) { - if (d_topLevelSubstitutions.hasSubstitution((*it).first)) { - builder << d_assertionsToCheck[(*it).second]; - d_assertionsToCheck[(*it).second] = NodeManager::currentNM()->mkConst(true); + TNode iteExpr = d_assertionsToCheck[(*it).second]; + if (iteExpr.getKind() == kind::ITE && + iteExpr[1].getKind() == kind::EQUAL && + iteExpr[1][0] == (*it).first && + iteExpr[2].getKind() == kind::EQUAL && + iteExpr[2][0] == (*it).first) { + hash_map cache; + bool bad = checkForBadSkolems(iteExpr[0], (*it).first, cache); + bad = bad || checkForBadSkolems(iteExpr[1][1], (*it).first, cache); + bad = bad || checkForBadSkolems(iteExpr[2][1], (*it).first, cache); + if (!bad) { + continue; + } } + // Move this iteExpr into the main assertions + builder << d_assertionsToCheck[(*it).second]; + d_assertionsToCheck[(*it).second] = NodeManager::currentNM()->mkConst(true); + toErase.push_back((*it).first); } if(builder.getNumChildren() > 1) { + while (!toErase.empty()) { + d_iteSkolemMap.erase(toErase.back()); + toErase.pop_back(); + } d_assertionsToCheck[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder)); } @@ -2244,6 +2309,9 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc // Add the formula if(!e.isNull()) { d_problemExtended = true; + if(d_assertionList != NULL) { + d_assertionList->push_back(e); + } d_private->addFormula(e.getNode()); } diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index aadaf39e7..564f5cd56 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -19,6 +19,7 @@ TESTS = \ bug338.smt2 \ bug347.smt \ bug348.smt \ + bug451.smt \ try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt \ try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.delta01.smt \ diseqprop.01.smt \ diff --git a/test/regress/regress0/aufbv/bug451.smt b/test/regress/regress0/aufbv/bug451.smt new file mode 100644 index 000000000..a3e0454ab --- /dev/null +++ b/test/regress/regress0/aufbv/bug451.smt @@ -0,0 +1,67 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:status unsat +:extrafuns ((v0 BitVec[15])) +:extrafuns ((a1 Array[9:14])) +:formula +(let (?e2 bv37005[16]) +(let (?e3 bv1274[11]) +(let (?e4 (ite (bvugt v0 (zero_extend[4] ?e3)) bv1[1] bv0[1])) +(let (?e5 (ite (= ?e2 ?e2) bv1[1] bv0[1])) +(let (?e6 (store a1 (extract[8:0] v0) (zero_extend[13] ?e4))) +(let (?e7 (store ?e6 (extract[14:6] v0) (extract[14:1] ?e2))) +(let (?e8 (store ?e6 (extract[8:0] ?e3) (extract[15:2] ?e2))) +(let (?e9 (select a1 (extract[8:0] v0))) +(let (?e10 (store ?e7 (extract[9:1] ?e9) (zero_extend[13] ?e5))) +(let (?e11 (store ?e7 (extract[9:1] ?e9) (zero_extend[3] ?e3))) +(let (?e12 (bvxor ?e2 ?e2)) +(let (?e13 (bvmul (zero_extend[15] ?e5) ?e2)) +(let (?e14 (ite (bvuge ?e13 (sign_extend[1] v0)) bv1[1] bv0[1])) +(let (?e15 (ite (= (sign_extend[14] ?e4) v0) bv1[1] bv0[1])) +(let (?e16 (bvashr ?e3 (sign_extend[10] ?e14))) +(let (?e17 (bvnand ?e9 (sign_extend[3] ?e16))) +(flet ($e18 (bvsgt ?e2 (sign_extend[15] ?e5))) +(flet ($e19 (distinct (sign_extend[2] ?e17) ?e12)) +(flet ($e20 (bvult ?e17 ?e17)) +(flet ($e21 (bvsge ?e16 (zero_extend[10] ?e14))) +(flet ($e22 (bvsge v0 (zero_extend[4] ?e16))) +(flet ($e23 (bvuge (zero_extend[14] ?e4) v0)) +(flet ($e24 (bvsle (sign_extend[2] ?e17) ?e12)) +(flet ($e25 (= ?e13 (zero_extend[2] ?e17))) +(flet ($e26 (bvsgt v0 (sign_extend[14] ?e5))) +(flet ($e27 (distinct ?e13 ?e13)) +(flet ($e28 (bvule ?e13 (zero_extend[5] ?e16))) +(flet ($e29 (bvule ?e17 ?e17)) +(flet ($e30 (bvsle ?e13 (sign_extend[15] ?e4))) +(flet ($e31 (bvsge ?e2 (sign_extend[5] ?e3))) +(flet ($e32 (bvule ?e13 (sign_extend[5] ?e3))) +(flet ($e33 (bvule ?e13 (zero_extend[2] ?e17))) +(flet ($e34 (= (sign_extend[14] ?e14) v0)) +(flet ($e35 (bvsgt ?e3 (zero_extend[10] ?e15))) +(flet ($e36 (bvuge ?e9 (sign_extend[13] ?e15))) +(flet ($e37 (not $e20)) +(flet ($e38 (and $e30 $e22)) +(flet ($e39 (not $e33)) +(flet ($e40 (xor $e28 $e36)) +(flet ($e41 (implies $e37 $e37)) +(flet ($e42 (xor $e40 $e18)) +(flet ($e43 (or $e25 $e38)) +(flet ($e44 (iff $e43 $e23)) +(flet ($e45 (if_then_else $e27 $e32 $e34)) +(flet ($e46 (or $e24 $e19)) +(flet ($e47 (iff $e46 $e21)) +(flet ($e48 (or $e44 $e41)) +(flet ($e49 (iff $e39 $e26)) +(flet ($e50 (implies $e49 $e48)) +(flet ($e51 (or $e42 $e42)) +(flet ($e52 (xor $e35 $e31)) +(flet ($e53 (iff $e47 $e52)) +(flet ($e54 (implies $e53 $e29)) +(flet ($e55 (if_then_else $e51 $e50 $e51)) +(flet ($e56 (and $e55 $e54)) +(flet ($e57 (xor $e56 $e56)) +(flet ($e58 (not $e57)) +(flet ($e59 (and $e58 $e45)) +$e59 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + -- 2.30.2