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 384734100a7b1bfd744228e42284ac6fb48f6d19..2fa62d9f68e996ded2daaac0ad0649694a2be705 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -425,6 +425,16 @@ void PropEngine::getBooleanVariables(std::vector<TNode>& 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<theory::TrustNode> 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 453c1c2af83febdd1183374d8963215176693927..8086a427e3673a687571e8e2b2101ec7ba0ba8c8 100644 (file)
--- 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 5206ed7aee6e00611b3191f72b1282c06b73e604..27ae0018e8907f960ce4bfd6987437bfc2a184cc 100644 (file)
--- 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 41f8372a9363ab865bc29d536d2906d45e23396b..df57d9903b6e2dd60a4989cd38c9634bf551a67f 100644 (file)
--- 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 ad6ee9fdf79abedd222f201309f129187b414ebb..b8ee5d41c1830c9427d0e9c5f371f276146b3a8b 100644 (file)
--- 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 01b33eb99da51298bdd6d6fc2c7607c2d5ebece4..06555687222dffb0af0475c1f4e69d1134037fca 100644 (file)
--- 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