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.

1 files changed, 8 insertions, 2 deletions

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.
    */