(proof-new) Updates to skolem manager interface (#4664)

Adds a fix for mkPurifySkolem and introduces new interfaces in preparation for arithmetic operator elimination and term formula removal proofs.

1 files changed, 21 insertions, 3 deletions

diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 8dd3a3ef9..1e02d94f4 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -86,6 +86,12 @@ class SkolemManager
    * @param pg The proof generator for this skolem. If non-null, this proof
    * generator must respond to a call to getProofFor(exists v. pred) during
    * the lifetime of the current node manager.
+   * @param retWitness Whether we wish to return the witness term for the
+   * given Skolem, which notice is of the form (witness v. pred), where pred
+   * is in Skolem form. A typical use case of setting this flag to true
+   * is preprocessing passes that eliminate terms. Using a witness term
+   * instead of its corresponding Skolem indicates that the body of the witness
+   * term needs to be added as an assertion, e.g. by the term formula remover.
    * @return The skolem whose witness form is registered by this class.
    */
   Node mkSkolem(Node v,
@@ -93,7 +99,8 @@ class SkolemManager
                 const std::string& prefix,
                 const std::string& comment = "",
                 int flags = NodeManager::SKOLEM_DEFAULT,
-                ProofGenerator* pg = nullptr);
+                ProofGenerator* pg = nullptr,
+                bool retWitness = false);
   /**
    * Make skolemized form of existentially quantified formula q, and store its
    * Skolems into the argument skolems.
@@ -143,6 +150,12 @@ class SkolemManager
                       const std::string& comment = "",
                       int flags = NodeManager::SKOLEM_DEFAULT);
   /**
+   * Make Boolean term variable for term t. This is a special case of
+   * mkPurifySkolem above, where the returned term has kind
+   * BOOLEAN_TERM_VARIABLE.
+   */
+  Node mkBooleanTermVariable(Node t);
+  /**
    * Get proof generator for existentially quantified formula q. This returns
    * the proof generator that was provided in a call to mkSkolem above.
    */
@@ -153,13 +166,18 @@ class SkolemManager
    * where T is the type of t, and x is a variable unique to t,p.
    */
   Node mkExistential(Node t, Node p);
-  /** convert to witness form
+  /**
+   * Convert to witness form, where notice this recursively replaces *all*
+   * skolems in n by their corresponding witness term. This is intended to be
+   * used by the proof checker only.
    *
    * @param n The term or formula to convert to witness form described above
    * @return n in witness form.
    */
   static Node getWitnessForm(Node n);
-  /** convert to Skolem form
+  /**
+   * Convert to Skolem form, which recursively replaces all witness terms in n
+   * by their corresponding Skolems.
    *
    * @param n The term or formula to convert to Skolem form described above
    * @return n in Skolem form.