From: Andrew Reynolds Date: Sun, 24 Jan 2021 17:42:08 +0000 (-0600) Subject: Add interface for getting preprocessed term (#5798) X-Git-Tag: cvc5-1.0.0~2366 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1d49bcb407777cf177620dac4d8e4df82f5e1122;p=cvc5.git Add interface for getting preprocessed term (#5798) Several places, e.g. in quantifiers, requiring knowing what the theory-preprocessed form of a node is. This is required for an improvement to our E-matching algorithm, which requires knowing what the preprocessed form of ground subterms of triggers are. Note that I'm not 100% happy with adding a new interface to Valuation, but at the moment I don't see a better way of doing this. On the positive side, this interface will make a few other things (e.g. the return value of OutputChannel::lemma) obsolete. --- diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 384734100..2fa62d9f6 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -425,6 +425,16 @@ void PropEngine::getBooleanVariables(std::vector& outputVariables) const } Node PropEngine::ensureLiteral(TNode n) +{ + // must preprocess + Node preprocessed = getPreprocessedTerm(n); + Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed + << std::endl; + d_cnfStream->ensureLiteral(preprocessed); + return preprocessed; +} + +Node PropEngine::getPreprocessedTerm(TNode n) { // must preprocess std::vector newLemmas; @@ -434,14 +444,9 @@ Node PropEngine::ensureLiteral(TNode n) // send lemmas corresponding to the skolems introduced by preprocessing n for (const theory::TrustNode& tnl : newLemmas) { - Trace("ensureLiteral") << " lemma: " << tnl.getNode() << std::endl; assertLemma(tnl, theory::LemmaProperty::NONE); } - Node preprocessed = tpn.isNull() ? Node(n) : tpn.getNode(); - Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed - << std::endl; - d_cnfStream->ensureLiteral(preprocessed); - return preprocessed; + return tpn.isNull() ? Node(n) : tpn.getNode(); } void PropEngine::push() diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 453c1c2af..8086a427e 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -190,6 +190,12 @@ class PropEngine * via getSatValue(). */ Node ensureLiteral(TNode n); + /** + * This returns the theory-preprocessed form of term n. This rewrites and + * preprocesses n, which notice may involve adding clauses to the SAT solver + * if preprocessing n involves introducing new skolems. + */ + Node getPreprocessedTerm(TNode n); /** * Push the context level. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 5206ed7ae..27ae0018e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1174,6 +1174,11 @@ Node TheoryEngine::ensureLiteral(TNode n) { return d_propEngine->ensureLiteral(rewritten); } +Node TheoryEngine::getPreprocessedTerm(TNode n) +{ + Node rewritten = Rewriter::rewrite(n); + return d_propEngine->getPreprocessedTerm(rewritten); +} void TheoryEngine::printInstantiations( std::ostream& out ) { if( d_quantEngine ){ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 41f8372a9..df57d9903 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -654,10 +654,16 @@ class TheoryEngine { /** * Takes a literal and returns an equivalent literal that is guaranteed to be * a SAT literal. This rewrites and preprocesses n, which notice may involve - * sending lemmas if preprocessing n involves introducing new skolems. + * adding clauses to the SAT solver if preprocessing n involves introducing + * new skolems. */ Node ensureLiteral(TNode n); - + /** + * This returns the theory-preprocessed form of term n. This rewrites and + * preprocesses n, which notice may involve adding clauses to the SAT solver + * if preprocessing n involves introducing new skolems. + */ + Node getPreprocessedTerm(TNode n); /** * Print all instantiations made by the quantifiers module. */ diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index ad6ee9fdf..b8ee5d41c 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -159,6 +159,12 @@ Node Valuation::ensureLiteral(TNode n) { return d_engine->ensureLiteral(n); } +Node Valuation::getPreprocessedTerm(TNode n) +{ + Assert(d_engine != nullptr); + return d_engine->getPreprocessedTerm(n); +} + bool Valuation::isDecision(Node lit) const { Assert(d_engine != nullptr); return d_engine->getPropEngine()->isDecision(lit); diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 01b33eb99..065556872 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -135,12 +135,31 @@ public: * that is definitionally equal to it. The result of this function * is a Node that can be queried via getSatValue(). * + * Note that this call may add lemmas to the SAT solver corresponding to the + * definition of subterms eliminated by preprocessing. + * * @return the actual node that's been "literalized," which may * differ from the input due to theory-rewriting and preprocessing, * as well as CNF conversion */ Node ensureLiteral(TNode n) CVC4_WARN_UNUSED_RESULT; + /** + * This returns the theory-preprocessed form of term n. The theory + * preprocessed form of a term t is one returned by + * TheoryPreprocess::preprocess (see theory/theory_preprocess.h). In + * particular, the returned term has syntax sugar symbols eliminated + * (e.g. div, mod, partial datatype selectors), has term formulas (e.g. ITE + * terms eliminated) and has been rewritten. + * + * Note that this call may add lemmas to the SAT solver corresponding to the + * definition of subterms eliminated by preprocessing. + * + * @param n The node to preprocess + * @return The preprocessed form of n + */ + Node getPreprocessedTerm(TNode n); + /** * Returns whether the given lit (which must be a SAT literal) is a decision * literal or not. Throws an exception if lit is not a SAT literal. "lit" may