(proof-new) Simplifications to arithmetic operator elimination and preprocessing (#6040)

Due to refactoring in theory preprocessor, which does fixed point preprocessing on created lemmas, several things can be simplified in arithmetic operator elimination.

This is required for further simplification to witness forms in the internal proof calculus.

1 files changed, 8 insertions, 8 deletions

diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h
index bca80ea4d..cf5b9248c 100644
--- a/src/theory/arith/operator_elim.h
+++ b/src/theory/arith/operator_elim.h
@@ -102,20 +102,20 @@ class OperatorElim : public EagerProofGenerator
    * @return The (single step) eliminated form of n.
    */
   Node eliminateOperators(Node n, TConvProofGenerator* tg, bool partialOnly);
-  /**
-   * Recursively ensure that n has no non-standard operators. This applies
-   * the above method on all subterms of n.
-   *
-   * @param n The node to eliminate operators from.
-   * @return The eliminated form of n.
-   */
-  Node eliminateOperatorsRec(Node n, TConvProofGenerator* tg, bool partialOnly);
   /** get arithmetic skolem
    *
    * Returns the Skolem in the above map for the given id, creating it if it
    * does not already exist.
    */
   Node getArithSkolem(ArithSkolemId asi);
+  /**
+   * Make the witness term, which creates a witness term based on the skolem
+   * manager with this class as a proof generator.
+   */
+  Node mkWitnessTerm(Node v,
+                     Node pred,
+                     const std::string& prefix,
+                     const std::string& comment);
   /** get arithmetic skolem application
    *
    * By default, this returns the term f( n ), where f is the Skolem function