From cd33db0a13ef195995885c4c42031386b2261ac4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 16 Dec 2020 16:35:59 -0600 Subject: [PATCH] Simplify preprocessing (#5647) This simplifies preprocessing so that the only call to theory-preprocess and ite-removal is at the very end. (One exception is early-theory-pp which is used by default in combination with ite-simp to maintain the performance on QF_LIA/nec). This is in preparation for making theory preprocessing happen lazily, post-CNF conversion. @HanielB has done SMT-LIB performance runs, see below. --- src/options/smt_options.toml | 8 + .../passes/unconstrained_simplifier.cpp | 2 + src/smt/process_assertions.cpp | 172 +----------------- src/smt/process_assertions.h | 16 -- src/smt/set_defaults.cpp | 12 ++ test/regress/regress0/unconstrained/4481.smt2 | 3 +- 6 files changed, 31 insertions(+), 182 deletions(-) diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 08d53855c..b01b7780f 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -361,6 +361,14 @@ header = "options/smt_options.h" default = "false" help = "enables compressing ites after ite simplification" +[[option]] + name = "earlyIteRemoval" + category = "experimental" + long = "early-ite-removal" + type = "bool" + default = "false" + help = "remove ITEs early in preprocessing" + [[option]] name = "unconstrainedSimp" category = "regular" diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 51434e369..6ebf1b8c8 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -358,6 +358,8 @@ void UnconstrainedSimplifier::processUnconstrained() case kind::BITVECTOR_SHL: case kind::BITVECTOR_LSHR: case kind::BITVECTOR_ASHR: + case kind::BITVECTOR_UDIV: + case kind::BITVECTOR_UREM: case kind::BITVECTOR_UDIV_TOTAL: case kind::BITVECTOR_UREM_TOTAL: case kind::BITVECTOR_SDIV: diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index c2374c6ff..77c7d450e 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -203,10 +203,6 @@ bool ProcessAssertions::apply(Assertions& as) if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF) { d_passes["bv-to-int"]->apply(&assertions); - // after running bv-to-int, we need to immediately run - // theory-preprocess and ite-removal so that newlly created - // terms and assertions are normalized (e.g., div is expanded). - d_passes["theory-preprocess"]->apply(&assertions); } // Since this pass is not robust for the information tracking necessary for @@ -290,6 +286,7 @@ bool ProcessAssertions::apply(Assertions& as) } Debug("smt") << " assertions : " << assertions.size() << endl; + if (options::earlyIteRemoval()) { d_smtStats.d_numAssertionsPre += assertions.size(); d_passes["ite-removal"]->apply(&assertions); @@ -309,84 +306,6 @@ bool ProcessAssertions::apply(Assertions& as) Chat() << "re-simplifying assertions..." << endl; ScopeCounter depth(d_simplifyAssertionsDepth); noConflict &= simplifyAssertions(assertions); - if (noConflict) - { - // 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. - - // cache for expression traversal - unordered_map cache; - - IteSkolemMap& iskMap = assertions.getIteSkolemMap(); - // 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& top_level_substs = - d_preprocessingPassContext->getTopLevelSubstitutions().get(); - SubstitutionMap::iterator pos = top_level_substs.begin(); - for (; pos != top_level_substs.end(); ++pos) - { - collectSkolems(iskMap, (*pos).first, skolemSet, cache); - collectSkolems(iskMap, (*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 - IteSkolemMap::iterator it = iskMap.begin(); - IteSkolemMap::iterator iend = iskMap.end(); - std::vector newConj; - vector toErase; - for (; it != iend; ++it) - { - if (skolemSet.find((*it).first) == skolemSet.end()) - { - TNode iteExpr = assertions[(*it).second]; - if (iteExpr.getKind() == ITE && iteExpr[1].getKind() == EQUAL - && iteExpr[1][0] == (*it).first && iteExpr[2].getKind() == EQUAL - && iteExpr[2][0] == (*it).first) - { - cache.clear(); - bool bad = - checkForBadSkolems(iskMap, iteExpr[0], (*it).first, cache); - bad = bad - || checkForBadSkolems( - iskMap, iteExpr[1][1], (*it).first, cache); - bad = bad - || checkForBadSkolems( - iskMap, iteExpr[2][1], (*it).first, cache); - if (!bad) - { - continue; - } - } - } - // Move this iteExpr into the main assertions - newConj.push_back(assertions[(*it).second]); - assertions.replace((*it).second, d_true); - toErase.push_back((*it).first); - } - if (!newConj.empty()) - { - while (!toErase.empty()) - { - iskMap.erase(toErase.back()); - toErase.pop_back(); - } - size_t index = assertions.getRealAssertionsEnd() - 1; - Node newAssertion = NodeManager::currentNM()->mkAnd(newConj); - assertions.conjoin(index, newAssertion); - } - // TODO(b/1256): For some reason this is needed for some benchmarks, such - // as - // QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2 - d_passes["ite-removal"]->apply(&assertions); - d_passes["apply-substs"]->apply(&assertions); - } Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-repeat-simplify" << endl; @@ -407,12 +326,19 @@ bool ProcessAssertions::apply(Assertions& as) << endl; Debug("smt") << " assertions : " << assertions.size() << endl; + // ensure rewritten + d_passes["rewrite"]->apply(&assertions); + // apply theory preprocess d_passes["theory-preprocess"]->apply(&assertions); // Must remove ITEs again since theory preprocessing may introduce them. // Notice that we alternatively could ensure that the theory-preprocess // pass above calls TheoryPreprocess::preprocess instead of // TheoryPreprocess::theoryPreprocess, as the former also does ITE removal. d_passes["ite-removal"]->apply(&assertions); + // This is needed because when solving incrementally, removeITEs may + // introduce skolems that were solved for earlier and thus appear in the + // substitution map. + d_passes["apply-substs"]->apply(&assertions); if (options::bitblastMode() == options::BitblastMode::EAGER) { @@ -470,13 +396,6 @@ bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions) Debug("smt") << " assertions : " << assertions.size() << endl; - // Theory preprocessing - bool doEarlyTheoryPp = !options::arithRewriteEq(); - if (doEarlyTheoryPp) - { - d_passes["theory-preprocess"]->apply(&assertions); - } - // ITE simplification if (options::doITESimp() && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat())) @@ -542,80 +461,5 @@ void ProcessAssertions::dumpAssertions(const char* key, } } -void ProcessAssertions::collectSkolems( - IteSkolemMap& iskMap, - TNode n, - set& skolemSet, - unordered_map& cache) -{ - unordered_map::iterator it; - it = cache.find(n); - if (it != cache.end()) - { - return; - } - - size_t sz = n.getNumChildren(); - if (sz == 0) - { - if (iskMap.find(n) != iskMap.end()) - { - skolemSet.insert(n); - } - cache[n] = true; - return; - } - - size_t k = 0; - for (; k < sz; ++k) - { - collectSkolems(iskMap, n[k], skolemSet, cache); - } - cache[n] = true; -} - -bool ProcessAssertions::checkForBadSkolems( - IteSkolemMap& iskMap, - TNode n, - TNode skolem, - unordered_map& cache) -{ - unordered_map::iterator it; - it = cache.find(n); - if (it != cache.end()) - { - return (*it).second; - } - - size_t sz = n.getNumChildren(); - if (sz == 0) - { - IteSkolemMap::iterator iit = iskMap.find(n); - bool bad = false; - if (iit != iskMap.end()) - { - if (!((*iit).first < n)) - { - bad = true; - } - } - cache[n] = bad; - return bad; - } - - size_t k = 0; - for (; k < sz; ++k) - { - if (checkForBadSkolems(iskMap, n[k], skolem, cache)) - { - cache[n] = true; - return true; - } - } - - cache[n] = false; - return false; -} - } // namespace smt } // namespace CVC4 diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index 072603e7d..ca834459d 100644 --- a/src/smt/process_assertions.h +++ b/src/smt/process_assertions.h @@ -118,22 +118,6 @@ class ProcessAssertions */ void dumpAssertions(const char* key, const preprocessing::AssertionPipeline& assertionList); - /** - * Helper function to fix up assertion list to restore invariants needed after - * ite removal. - */ - void collectSkolems(IteSkolemMap& iskMap, - TNode n, - set& skolemSet, - NodeToBoolHashMap& cache); - /** - * Helper function to fix up assertion list to restore invariants needed after - * ite removal. - */ - bool checkForBadSkolems(IteSkolemMap& iskMap, - TNode n, - TNode skolem, - NodeToBoolHashMap& cache); }; } // namespace smt diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index c8aecf288..bbbe73cb1 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -210,6 +210,18 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } + // --ite-simp is an experimental option designed for QF_LIA/nec. This + // technique is experimental. This benchmark set also requires removing ITEs + // during preprocessing, before repeating simplification. Hence, we enable + // this by default. + if (options::doITESimp()) + { + if (!options::earlyIteRemoval.wasSetByUser()) + { + options::earlyIteRemoval.set(true); + } + } + // Set default options associated with strings-exp. We also set these options // if we are using eager string preprocessing, which may introduce quantified // formulas at preprocess time. diff --git a/test/regress/regress0/unconstrained/4481.smt2 b/test/regress/regress0/unconstrained/4481.smt2 index 19179f4d7..028607093 100644 --- a/test/regress/regress0/unconstrained/4481.smt2 +++ b/test/regress/regress0/unconstrained/4481.smt2 @@ -1,6 +1,5 @@ ; COMMAND-LINE: --unconstrained-simp -; EXPECT: (error "Cannot use unconstrained simplification in this logic, due to (possibly internally introduced) quantified formula.") -; EXIT: 1 +; EXPECT: unsat (set-logic ALL) (set-info :status unsat) (declare-fun a () Int) -- 2.30.2