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.

6 files changed, 55 insertions, 8 deletions

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
@@ -427,6 +427,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;
   std::vector<Node> newSkolems;
   theory::TrustNode tpn =
@@ -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,6 +135,9 @@ 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
@@ -142,6 +145,22 @@ public:
   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
    * be in either phase; that is, if "lit" is a SAT literal, this function returns