From: Clark Barrett Date: Thu, 29 Nov 2012 14:28:28 +0000 (+0000) Subject: Fix for nasty corner case found by fuzzer... X-Git-Tag: cvc5-1.0.0~7532 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=09df42818dcbcd4c44d8daf777dec62eb1f9d2a7;p=cvc5.git Fix for nasty corner case found by fuzzer... --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8330b2a20..25a066e4a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -307,6 +307,11 @@ private: */ void removeITEs(); + /** + * Helper function to fix up assertion list to restore invariants needed after ite removal + */ + void collectSkolems(TNode n, set& skolemSet, hash_map& cache); + /** * Helper function to fix up assertion list to restore invariants needed after ite removal */ @@ -2000,6 +2005,32 @@ Result SmtEngine::quickCheck() { } +void SmtEnginePrivate::collectSkolems(TNode n, set& skolemSet, hash_map& cache) +{ + hash_map::iterator it; + it = cache.find(n); + if (it != cache.end()) { + return; + } + + size_t sz = n.getNumChildren(); + if (sz == 0) { + IteSkolemMap::iterator it = d_iteSkolemMap.find(n); + if (it != d_iteSkolemMap.end()) { + skolemSet.insert(n); + } + cache[n] = true; + return; + } + + size_t k = 0; + for (; k < sz; ++k) { + collectSkolems(n[k], skolemSet, cache); + } + cache[n] = true; +} + + bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map& cache) { hash_map::iterator it; @@ -2157,7 +2188,7 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("pre-simplify", d_assertionsToPreprocess); Chat() << "simplifying assertions..." << endl; bool noConflict = simplifyAssertions(); - dumpAssertions("post-simplify", d_assertionsToPreprocess); + dumpAssertions("post-simplify", d_assertionsToCheck); dumpAssertions("pre-static-learning", d_assertionsToCheck); if(options::doStaticLearning()) { @@ -2189,7 +2220,21 @@ void SmtEnginePrivate::processAssertions() { // 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: + // For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk. + + // cache for expression traversal + hash_map cache; + + // First, find all skolems that appear in the substitution map - their associated iteExpr will need + // to be moved to the main assertion set + set skolemSet; + SubstitutionMap::iterator pos = d_topLevelSubstitutions.begin(); + for (; pos != d_topLevelSubstitutions.end(); ++pos) { + collectSkolems((*pos).first, skolemSet, cache); + collectSkolems((*pos).second, skolemSet, cache); + } + + // 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 @@ -2199,18 +2244,20 @@ void SmtEnginePrivate::processAssertions() { builder << d_assertionsToCheck[d_realAssertionsEnd - 1]; vector toErase; for (; it != iend; ++it) { - 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; + if (skolemSet.find((*it).first) == skolemSet.end()) { + 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) { + cache.clear(); + 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