From 61aa589c4a702ee378c5b3643f4a69373da2d360 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 5 Nov 2021 16:45:13 -0500 Subject: [PATCH] Eliminate a level of nesting of traversals in theory preprocessing (#7345) This simplifies the theory preprocessor so that it does not rely on the term formula removal to do a nested traversal. Instead, it only relies on its "runCurrent" method. Notice that this PR essentially replaces TheoryPreprocessor's theoryPreprocess method with TermFormulaRemoval's runInternal method, while adding the required call to rewriteWithProof and preprocessWithProof as post-rewrites. This is far simpler than the previous method, which invoked nested traversals using TermFormulaRemoval::run. There are two things that will be improved in follow up PRs: The initial full rewrite step in the theory preprocessor can be merged into the main traversal of theory preprocess (I believe this is why we are slower on nec benchmark than we were previously), We should eliminate the traversal methods from TermFormulaRemoval altogether, as they are now subsumed by the theory preprocessors main traversal. This will require refactoring how "early ITE removal" works, as this is the only user now of TermFormulaRemoval::run. Note we should probably performance test this change. This incidentally fixes #6973, as the previous theory preprocessing code was to blame for that issue. --- src/smt/term_formula_removal.cpp | 42 ++- src/smt/term_formula_removal.h | 19 +- src/theory/booleans/theory_bool.cpp | 13 - src/theory/theory_preprocessor.cpp | 335 +++++++++--------- src/theory/theory_preprocessor.h | 79 ++--- test/regress/CMakeLists.txt | 3 +- .../strings/issue6973-dup-lemma-conc.smt2 | 2 + 7 files changed, 251 insertions(+), 242 deletions(-) diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index c633ecb63..edf4e2761 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -24,6 +24,7 @@ #include "proof/conv_proof_generator.h" #include "proof/lazy_proof.h" #include "smt/env.h" +#include "smt/logic_exception.h" using namespace std; @@ -47,6 +48,12 @@ RemoveTermFormulas::RemoveTermFormulas(Env& env) TConvCachePolicy::NEVER, "RemoveTermFormulas::TConvProofGenerator", &d_rtfc)); + d_tpgi.reset( + new TConvProofGenerator(pnm, + nullptr, + TConvPolicy::ONCE, + TConvCachePolicy::NEVER, + "RemoveTermFormulas::TConvProofGenerator")); d_lp.reset(new LazyCDProof( pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof")); } @@ -158,7 +165,8 @@ Node RemoveTermFormulas::runInternal(TNode assertion, Debug("ite") << "removeITEs(" << node << ")" << " " << inQuant << " " << inTerm << std::endl; Assert(!inQuant); - Node currt = runCurrentInternal(node, inTerm, newLem); + Node currt = + runCurrentInternal(node, inTerm, newLem, nodeVal, d_tpg.get()); // if we replaced by a skolem, we do not recurse if (!currt.isNull()) { @@ -246,17 +254,21 @@ TrustNode RemoveTermFormulas::runCurrent(TNode node, bool inTerm, TrustNode& newLem) { - Node k = runCurrentInternal(node, inTerm, newLem); + // use the term conversion generator that is term context insensitive, with + // cval set to 0. + Node k = runCurrentInternal(node, inTerm, newLem, 0, d_tpgi.get()); if (!k.isNull()) { - return TrustNode::mkTrustRewrite(node, k, d_tpg.get()); + return TrustNode::mkTrustRewrite(node, k, d_tpgi.get()); } return TrustNode::null(); } Node RemoveTermFormulas::runCurrentInternal(TNode node, bool inTerm, - TrustNode& newLem) + TrustNode& newLem, + uint32_t cval, + TConvProofGenerator* pg) { NodeManager *nodeManager = NodeManager::currentNM(); @@ -269,6 +281,13 @@ Node RemoveTermFormulas::runCurrentInternal(TNode node, // in the "non-variable Boolean term within term" case below. if (node.getKind() == kind::ITE && !nodeType.isBoolean()) { + if (!nodeType.isFirstClass()) + { + std::stringstream ss; + ss << "ITE branches of type " << nodeType + << " are currently not supported." << std::endl; + throw LogicException(ss.str()); + } // Here, we eliminate the ITE if we are not Boolean and if we are // not in a quantified formula. This policy should be in sync with // the policy for when to apply theory preprocessing to terms, see PR @@ -457,20 +476,19 @@ Node RemoveTermFormulas::runCurrentInternal(TNode node, // since a formula-term may rewrite to the same skolem in multiple contexts. if (isProofEnabled()) { - uint32_t cval = RtfTermContext::getValue(false, inTerm); // justify the introduction of the skolem // ------------------- MACRO_SR_PRED_INTRO // t = witness x. x=t // The above step is trivial, since the skolems introduced above are // all purification skolems. We record this equality in the term // conversion proof generator. - d_tpg->addRewriteStep(node, - skolem, - PfRule::MACRO_SR_PRED_INTRO, - {}, - {node.eqNode(skolem)}, - true, - cval); + pg->addRewriteStep(node, + skolem, + PfRule::MACRO_SR_PRED_INTRO, + {}, + {node.eqNode(skolem)}, + true, + cval); } // if the skolem was introduced in this call diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 1942b0fdc..31f9bfc3d 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -174,6 +174,10 @@ class RemoveTermFormulas : protected EnvObj * A proof generator for the term conversion. */ std::unique_ptr d_tpg; + /** + * A proof generator for the term conversion, not text-context sensitive. + */ + std::unique_ptr d_tpgi; /** * A proof generator for skolems we introduce that are based on axioms that * this class is responsible for. @@ -204,8 +208,21 @@ class RemoveTermFormulas : protected EnvObj * * Otherwise, if t should not be replaced in the term context, this method * returns the null node. + * + * @param node The node under consideration + * @param inTerm Whether we are in a term context (see RtfTermContext) + * @param newLem The new lemma axiomatizing the return value + * @param cval The term context identifier to cache the proof in pg, if it + * exists + * @param pg The proof generator to store the proof step + * @return the skolem that node should be replaced with, if applicable, or + * the null node otherwise. */ - Node runCurrentInternal(TNode node, bool inTerm, TrustNode& newLem); + Node runCurrentInternal(TNode node, + bool inTerm, + TrustNode& newLem, + uint32_t cval, + TConvProofGenerator* pg); /** Is proof enabled? True if proofs are enabled in any mode. */ bool isProofEnabled() const; }; /* class RemoveTTE */ diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 1327d1131..3184a6242 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -19,7 +19,6 @@ #include #include "proof/proof_node_manager.h" -#include "smt/logic_exception.h" #include "smt_util/boolean_simplification.h" #include "theory/booleans/circuit_propagator.h" #include "theory/booleans/theory_bool_rewriter.h" @@ -71,18 +70,6 @@ Theory::PPAssertStatus TheoryBool::ppAssert( TrustNode TheoryBool::ppRewrite(TNode n, std::vector& lems) { - Trace("bool-ppr") << "TheoryBool::ppRewrite " << n << std::endl; - if (n.getKind() == ITE) - { - TypeNode tn = n.getType(); - if (!tn.isFirstClass()) - { - std::stringstream ss; - ss << "ITE branches of type " << tn << " are currently not supported." - << std::endl; - throw LogicException(ss.str()); - } - } return TrustNode::null(); } diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index ee1e35b77..e92722a2a 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -16,6 +16,7 @@ #include "theory/theory_preprocessor.h" #include "expr/skolem_manager.h" +#include "expr/term_context_stack.h" #include "proof/lazy_proof.h" #include "smt/logic_exception.h" #include "theory/logic_info.h" @@ -30,11 +31,9 @@ namespace theory { TheoryPreprocessor::TheoryPreprocessor(Env& env, TheoryEngine& engine) : EnvObj(env), d_engine(engine), - d_ppCache(userContext()), - d_rtfCache(userContext()), + d_cache(userContext()), d_tfr(env), d_tpg(nullptr), - d_tpgRtf(nullptr), d_tpgRew(nullptr), d_tspg(nullptr), d_lp(nullptr) @@ -50,13 +49,7 @@ TheoryPreprocessor::TheoryPreprocessor(Env& env, TheoryEngine& engine) TConvPolicy::FIXPOINT, TConvCachePolicy::NEVER, "TheoryPreprocessor::preprocess_rewrite", - &d_iqtc)); - d_tpgRtf.reset(new TConvProofGenerator(pnm, - u, - TConvPolicy::FIXPOINT, - TConvCachePolicy::NEVER, - "TheoryPreprocessor::rtf", - &d_iqtc)); + &d_rtfc)); d_tpgRew.reset(new TConvProofGenerator(pnm, u, TConvPolicy::ONCE, @@ -71,7 +64,7 @@ TheoryPreprocessor::TheoryPreprocessor(Env& env, TheoryEngine& engine) // removal+rewriting. std::vector ts; ts.push_back(d_tpgRew.get()); - ts.push_back(d_tpgRtf.get()); + ts.push_back(d_tpg.get()); d_tspg.reset(new TConvSeqProofGenerator( pnm, ts, userContext(), "TheoryPreprocessor::sequence")); } @@ -97,7 +90,7 @@ TrustNode TheoryPreprocessor::preprocessInternal( // An example of this is (forall ((x Int)) (and (tail L) (P x))) which // rewrites to (and (tail L) (forall ((x Int)) (P x))). The subterm (tail L) // must be preprocessed as a child here. - Node irNode = rewriteWithProof(node, d_tpgRew.get(), true); + Node irNode = rewriteWithProof(node, d_tpgRew.get(), true, 0); // run theory preprocessing TrustNode tpp = theoryPreprocess(irNode, newLemmas); @@ -223,188 +216,185 @@ RemoveTermFormulas& TheoryPreprocessor::getRemoveTermFormulas() return d_tfr; } -struct preprocess_stack_element -{ - TNode node; - bool children_added; - preprocess_stack_element(TNode n) : node(n), children_added(false) {} -}; - TrustNode TheoryPreprocessor::theoryPreprocess( TNode assertion, std::vector& newLemmas) { - Trace("theory::preprocess") - << "TheoryPreprocessor::theoryPreprocess(" << assertion << ")" << endl; - // spendResource(); - - // Do a topological sort of the subexpressions and substitute them - vector toVisit; - toVisit.push_back(assertion); - - while (!toVisit.empty()) + // Map from (term, term context identifier) to the term that it was + // theory-preprocessed to. This is used when the result of the current node + // should be set to the final result of converting its theory-preprocessed + // form. + std::unordered_map, + Node, + PairHashFunction>> + wasPreprocessed; + std::unordered_map< + std::pair, + Node, + PairHashFunction>>::iterator itw; + NodeManager* nm = NodeManager::currentNM(); + TCtxStack ctx(&d_rtfc); + std::vector processedChildren; + ctx.pushInitial(assertion); + processedChildren.push_back(false); + std::pair initial = ctx.getCurrent(); + std::pair curr; + Node node; + uint32_t nodeVal; + TppCache::const_iterator itc; + while (!ctx.empty()) { - // The current node we are processing - preprocess_stack_element& stackHead = toVisit.back(); - TNode current = stackHead.node; - - Trace("theory::preprocess-debug") - << "TheoryPreprocessor::theoryPreprocess processing " << current - << endl; - - // If node already in the cache we're done, pop from the stack - if (d_rtfCache.find(current) != d_rtfCache.end()) + curr = ctx.getCurrent(); + itc = d_cache.find(curr); + node = curr.first; + nodeVal = curr.second; + Trace("tpp-debug") << "Visit " << node << ", " << nodeVal << std::endl; + if (itc != d_cache.end()) { - toVisit.pop_back(); + Trace("tpp-debug") << "...already computed" << std::endl; + ctx.pop(); + processedChildren.pop_back(); + // already computed continue; } - - TheoryId tid = Theory::theoryOf(current); - - if (!logicInfo().isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER) - { - stringstream ss; - ss << "The logic was specified as " << logicInfo().getLogicString() - << ", which doesn't include " << tid - << ", but got a preprocessing-time fact for that theory." << endl - << "The fact:" << endl - << current; - throw LogicException(ss.str()); - } - // If this is an atom, we preprocess its terms with the theory ppRewriter - if (tid != THEORY_BOOL) + // if we have yet to process children + if (!processedChildren.back()) { - Node ppRewritten = ppTheoryRewrite(current, newLemmas); - Assert(rewrite(ppRewritten) == ppRewritten); - if (isProofEnabled() && ppRewritten != current) + // check if we should replace the current node by a Skolem + TrustNode newLem; + bool inQuant, inTerm; + RtfTermContext::getFlags(nodeVal, inQuant, inTerm); + Assert(!inQuant); + TrustNode currTrn = d_tfr.runCurrent(node, inTerm, newLem); + // if we replaced by a skolem, we do not recurse + if (!currTrn.isNull()) { - TrustNode trn = - TrustNode::mkTrustRewrite(current, ppRewritten, d_tpg.get()); - registerTrustedRewrite(trn, d_tpgRtf.get(), true); + Node ret = currTrn.getNode(); + // if this is the first time we've seen this term, we have a new lemma + // which we add to our vectors + if (!newLem.isNull()) + { + newLemmas.push_back(theory::SkolemLemma(newLem, ret)); + } + // register the rewrite into the proof generator + if (isProofEnabled()) + { + registerTrustedRewrite(currTrn, d_tpg.get(), true, nodeVal); + } + Trace("tpp-debug") << "...replace by skolem" << std::endl; + d_cache.insert(curr, ret); + continue; } - - // Term formula removal without fixed point. We do not need to do fixed - // point since newLemmas are theory-preprocessed until fixed point in - // preprocessInternal (at top-level, when procLemmas=true). - TrustNode ttfr = d_tfr.run(ppRewritten, newLemmas, false); - Node rtfNode = ppRewritten; - if (!ttfr.isNull()) + size_t nchild = node.getNumChildren(); + if (nchild > 0) { - rtfNode = ttfr.getNode(); - registerTrustedRewrite(ttfr, d_tpgRtf.get(), true); + if (node.isClosure()) + { + // currently, we never do any term formula removal in quantifier + // bodies + } + else + { + Trace("tpp-debug") << "...recurse to children" << std::endl; + // recurse if we have children + processedChildren[processedChildren.size() - 1] = true; + for (size_t i = 0; i < nchild; i++) + { + ctx.pushChild(node, nodeVal, i); + processedChildren.push_back(false); + } + continue; + } } - // Finish the conversion by rewriting. Notice that we must consider this a - // pre-rewrite since we do not recursively register the rewriting steps - // of subterms of rtfNode. For example, if this step rewrites - // (not A) ---> B, then if registered a pre-rewrite, it will apply when - // reconstructing proofs via d_tpgRtf. However, if it is a post-rewrite - // it will fail to apply if another call to this class registers A -> C, - // in which case (not C) will be returned instead of B (see issue 6754). - Node retNode = rewriteWithProof(rtfNode, d_tpgRtf.get(), true); - d_rtfCache[current] = retNode; + else + { + Trace("tpp-debug") << "...base case" << std::endl; + } + } + Trace("tpp-debug") << "...reconstruct" << std::endl; + // otherwise, we are now finished processing children, pop the current node + // and compute the result + ctx.pop(); + processedChildren.pop_back(); + // if this was preprocessed previously, we set our result to the final + // form of the preprocessed form of this. + itw = wasPreprocessed.find(curr); + if (itw != wasPreprocessed.end()) + { + // we preprocessed it to something else, carry that + std::pair key(itw->second, nodeVal); + itc = d_cache.find(key); + Assert(itc != d_cache.end()); + d_cache.insert(curr, itc->second); + wasPreprocessed.erase(curr); continue; } - - // Not yet substituted, so process - if (stackHead.children_added) + Node ret = node; + Node pret = node; + if (!node.isClosure() && node.getNumChildren() > 0) { - // Children have been processed, so substitute - NodeBuilder builder(current.getKind()); - if (current.getMetaKind() == kind::metakind::PARAMETERIZED) + // if we have not already computed the result + std::vector newChildren; + bool childChanged = false; + if (node.getMetaKind() == kind::metakind::PARAMETERIZED) { - builder << current.getOperator(); + newChildren.push_back(node.getOperator()); } - for (unsigned i = 0; i < current.getNumChildren(); ++i) + // reconstruct from the children + std::pair currChild; + for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; i++) { - Assert(d_rtfCache.find(current[i]) != d_rtfCache.end()); - builder << d_rtfCache[current[i]].get(); + // recompute the value of the child + uint32_t val = d_rtfc.computeValue(node, nodeVal, i); + currChild = std::pair(node[i], val); + itc = d_cache.find(currChild); + Assert(itc != d_cache.end()); + Node newChild = (*itc).second; + Assert(!newChild.isNull()); + childChanged |= (newChild != node[i]); + newChildren.push_back(newChild); } - // Mark the substitution and continue - Node result = builder; - // always rewrite here, since current may not be in rewritten form after - // reconstruction - result = rewriteWithProof(result, d_tpgRtf.get(), false); - Trace("theory::preprocess-debug") - << "TheoryPreprocessor::theoryPreprocess setting " << current - << " -> " << result << endl; - d_rtfCache[current] = result; - toVisit.pop_back(); - } - else - { - // Mark that we have added the children if any - if (current.getNumChildren() > 0) + // If changes, we reconstruct the node + if (childChanged) { - stackHead.children_added = true; - // We need to add the children - for (TNode::iterator child_it = current.begin(); - child_it != current.end(); - ++child_it) - { - TNode childNode = *child_it; - if (d_rtfCache.find(childNode) == d_rtfCache.end()) - { - toVisit.push_back(childNode); - } - } - } - else - { - // No children, so we're done - Trace("theory::preprocess-debug") - << "SubstitutionMap::internalSubstitute setting " << current - << " -> " << current << endl; - d_rtfCache[current] = current; - toVisit.pop_back(); + ret = nm->mkNode(node.getKind(), newChildren); } + // Finish the conversion by rewriting. Notice that we must consider this a + // pre-rewrite since we do not recursively register the rewriting steps + // of subterms of rtfNode. For example, if this step rewrites + // (not A) ---> B, then if registered a pre-rewrite, it will apply when + // reconstructing proofs via d_tpg. However, if it is a post-rewrite + // it will fail to apply if another call to this class registers A -> C, + // in which case (not C) will be returned instead of B (see issue 6754). + pret = rewriteWithProof(ret, d_tpg.get(), false, nodeVal); } - } - Assert(d_rtfCache.find(assertion) != d_rtfCache.end()); - // Return the substituted version - Node res = d_rtfCache[assertion]; - return TrustNode::mkTrustRewrite(assertion, res, d_tpg.get()); -} - -// Recursively traverse a term and call the theory rewriter on its sub-terms -Node TheoryPreprocessor::ppTheoryRewrite(TNode term, - std::vector& lems) -{ - NodeMap::iterator find = d_ppCache.find(term); - if (find != d_ppCache.end()) - { - return (*find).second; - } - if (term.getNumChildren() == 0) - { - return preprocessWithProof(term, lems); - } - // should be in rewritten form here - Assert(term == rewrite(term)); - Trace("theory-pp") << "ppTheoryRewrite { " << term << endl; - // do not rewrite inside quantifiers - Node newTerm = term; - if (!term.isClosure()) - { - NodeBuilder newNode(term.getKind()); - if (term.getMetaKind() == kind::metakind::PARAMETERIZED) + // if we did not rewrite above, we are ready to theory preprocess + if (pret == ret) { - newNode << term.getOperator(); + pret = preprocessWithProof(ret, newLemmas, nodeVal); } - for (const Node& nt : term) + // if we changed due to rewriting or preprocessing, we traverse again + if (pret != ret) { - newNode << ppTheoryRewrite(nt, lems); + // must restart + ctx.push(node, nodeVal); + processedChildren.push_back(true); + ctx.push(pret, nodeVal); + processedChildren.push_back(false); + wasPreprocessed[curr] = pret; + continue; } - newTerm = Node(newNode); - newTerm = rewriteWithProof(newTerm, d_tpg.get(), false); + // cache + d_cache.insert(curr, ret); } - newTerm = preprocessWithProof(newTerm, lems); - d_ppCache[term] = newTerm; - Trace("theory-pp") << "ppTheoryRewrite returning " << newTerm << "}" << endl; - return newTerm; + itc = d_cache.find(initial); + Assert(itc != d_cache.end()); + return TrustNode::mkTrustRewrite(assertion, (*itc).second, d_tpg.get()); } Node TheoryPreprocessor::rewriteWithProof(Node term, TConvProofGenerator* pg, - bool isPre) + bool isPre, + uint32_t tctx) { Node termr = rewrite(term); // store rewrite step if tracking proofs and it rewrites @@ -415,15 +405,15 @@ Node TheoryPreprocessor::rewriteWithProof(Node term, { Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (rewriting) " << term << " -> " << termr << std::endl; - // always use term context hash 0 (default) - pg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term}, isPre); + pg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term}, isPre, tctx); } } return termr; } Node TheoryPreprocessor::preprocessWithProof(Node term, - std::vector& lems) + std::vector& lems, + uint32_t tctx) { // Important that it is in rewritten form, to ensure that the rewrite steps // recorded in d_tpg are functional. In other words, there should not @@ -462,18 +452,18 @@ Node TheoryPreprocessor::preprocessWithProof(Node term, Assert(term != termr); if (isProofEnabled()) { - registerTrustedRewrite(trn, d_tpg.get(), false); + registerTrustedRewrite(trn, d_tpg.get(), false, tctx); } // Rewrite again here, which notice is a *pre* rewrite. - termr = rewriteWithProof(termr, d_tpg.get(), true); - return ppTheoryRewrite(termr, lems); + return rewriteWithProof(termr, d_tpg.get(), true, tctx); } bool TheoryPreprocessor::isProofEnabled() const { return d_tpg != nullptr; } void TheoryPreprocessor::registerTrustedRewrite(TrustNode trn, TConvProofGenerator* pg, - bool isPre) + bool isPre, + uint32_t tctx) { if (!isProofEnabled() || trn.isNull()) { @@ -491,7 +481,7 @@ void TheoryPreprocessor::registerTrustedRewrite(TrustNode trn, "TheoryPreprocessor::preprocessWithProof"); // always use term context hash 0 (default) pg->addRewriteStep( - term, termr, trn.getGenerator(), isPre, PfRule::ASSUME, true); + term, termr, trn.getGenerator(), isPre, PfRule::ASSUME, true, tctx); } else { @@ -503,7 +493,8 @@ void TheoryPreprocessor::registerTrustedRewrite(TrustNode trn, PfRule::THEORY_PREPROCESS, {}, {term.eqNode(termr)}, - isPre); + isPre, + tctx); } } diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h index e4bd5955a..382bcd2da 100644 --- a/src/theory/theory_preprocessor.h +++ b/src/theory/theory_preprocessor.h @@ -23,6 +23,7 @@ #include "context/cdhashmap.h" #include "context/context.h" #include "expr/node.h" +#include "expr/term_context.h" #include "proof/conv_proof_generator.h" #include "proof/conv_seq_proof_generator.h" #include "proof/lazy_proof.h" @@ -48,22 +49,13 @@ namespace theory { * [2] * TRAVERSE( * prerewrite: - * if theory atom { - * TRAVERSE( - * prerewrite: - * // nothing - * postrewrite: - * apply rewriter - * apply ppRewrite - * if changed - * apply rewriter - * REPEAT traversal - * ) - * apply term formula removal - * apply rewriter - * } - * postrewrite: // for Boolean connectives - * apply rewriter + * apply term formula removal to the current node + * postrewrite: + * apply rewriter + * apply ppRewrite + * if changed + * apply rewriter + * REPEAT traversal * ) * * Note that the rewriter must be applied beforehand, since the rewriter may @@ -134,33 +126,27 @@ class TheoryPreprocessor : protected EnvObj bool procLemmas); /** Reference to owning theory engine */ TheoryEngine& d_engine; - /** - * Cache for theory-preprocessing of theory atoms. The domain of this map - * are terms that appear within theory atoms given to this class. - */ - NodeMap d_ppCache; - /** - * Cache for theory-preprocessing + term formula removal of the Boolean - * structure of assertions. The domain of this map are the Boolean - * connectives and theory atoms given to this class. + + typedef context::CDInsertHashMap< + std::pair, + Node, + PairHashFunction>> + TppCache; + /** term formula removal cache + * + * This stores the results of theory preprocessing using the theoryPreprocess + * method, where the integer in the pair we hash on is the + * result of cacheVal of the rtf term context. */ - NodeMap d_rtfCache; + TppCache d_cache; /** The term formula remover */ RemoveTermFormulas d_tfr; - /** The term context, which computes hash values for term contexts. */ - InQuantTermContext d_iqtc; /** * A term conversion proof generator storing preprocessing and rewriting * steps, which is done until fixed point in the inner traversal of this * class for theory atoms in step [2] above. */ std::unique_ptr d_tpg; - /** - * A term conversion proof generator storing large steps from d_tpg (results - * of its fixed point) and term formula removal steps for the outer traversal - * of this class for theory atoms in step [2] above. - */ - std::unique_ptr d_tpgRtf; /** * A term conversion proof generator storing rewriting steps, which is used * for top-level rewriting before the preprocessing pass, step [1] above. @@ -175,27 +161,32 @@ class TheoryPreprocessor : protected EnvObj /** A lazy proof, for additional lemmas. */ std::unique_ptr d_lp; /** - * Helper for theoryPreprocess, which traverses the provided term and - * applies ppRewrite and rewriting until fixed point on term using - * the method preprocessWithProof helper below. + * The remove term formula context, which computes hash values for term + * contexts. */ - Node ppTheoryRewrite(TNode term, std::vector& lems); + RtfTermContext d_rtfc; /** * Rewrite with proof, which stores a REWRITE step in pg if necessary * and returns the rewritten form of term. * * @param term The term to rewrite * @param pg The proof generator to register to - * @param isPre whether the rewrite is a pre-rewrite. + * @param isPre Whether the rewrite is a pre-rewrite + * @param tctx The term context identifier we should store the proof in pg */ - Node rewriteWithProof(Node term, TConvProofGenerator* pg, bool isPre); + Node rewriteWithProof(Node term, + TConvProofGenerator* pg, + bool isPre, + uint32_t tctx); /** * Preprocess with proof, which calls the appropriate ppRewrite method, * stores the corresponding rewrite step in d_tpg if necessary and returns * the preprocessed and rewritten form of term. It should be the case that * term is already in rewritten form. */ - Node preprocessWithProof(Node term, std::vector& lems); + Node preprocessWithProof(Node term, + std::vector& lems, + uint32_t tctx); /** * Register rewrite trn based on trust node into term conversion generator * pg, which uses THEORY_PREPROCESS as a step if no proof generator is @@ -203,11 +194,13 @@ class TheoryPreprocessor : protected EnvObj * * @param trn The REWRITE trust node * @param pg The proof generator to register to - * @param isPre whether the rewrite is a pre-rewrite. + * @param isPre Whether the rewrite is a pre-rewrite + * @param tctx The term context identifier we should store the proof in pg */ void registerTrustedRewrite(TrustNode trn, TConvProofGenerator* pg, - bool isPre); + bool isPre, + uint32_t tctx); /** Proofs enabled */ bool isProofEnabled() const; }; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f322ffafc..b6ccbcc54 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2053,7 +2053,6 @@ set(regress_1_tests regress1/quantifiers/stream-x2014-09-18-unsat.smt2 regress1/quantifiers/sygus-infer-nested.smt2 regress1/quantifiers/sygus-inst-nia-psyco-060.smt2 - regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 regress1/quantifiers/symmetric_unsat_7.smt2 regress1/quantifiers/tpp-unit-fail-qbv.smt2 regress1/quantifiers/var-eq-trigger.smt2 @@ -2824,6 +2823,8 @@ set(regression_disabled_tests # ajreynol: different error messages on production and debug: regress1/quantifiers/subtype-param-unk.smt2 regress1/quantifiers/subtype-param.smt2 + # timeout after changes to theory preprocessing, note is non-linear and does not involve sygus-inst + regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2 ### regress1/rels/garbage_collect.cvc.smt2 regress1/sets/setofsets-disequal.smt2 diff --git a/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 b/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 index 4c6fe5c62..36162852f 100644 --- a/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 +++ b/test/regress/regress1/strings/issue6973-dup-lemma-conc.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --strings-exp +; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg (set-logic QF_SLIA) (set-info :status unsat) (declare-fun a () String) -- 2.30.2