(proof-new) Arithmetic operator elim proof producing (#4783)

This updates the interface for arithmetic operator elimination for the new proof format.

The actual proof production of the operator elimination class (providing proofs for 
introduced witness terms) will be done in a separate PR.

This also changes the witness terms introduced by this class so their body is in 
Skolem form, which simplifies term formula removal.

Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>

5 files changed, 122 insertions, 80 deletions

diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index 593fbd584..938fe0a47 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -27,7 +27,10 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-OperatorElim::OperatorElim(const LogicInfo& info) : d_info(info) {}
+OperatorElim::OperatorElim(ProofNodeManager* pnm, const LogicInfo& info)
+    : EagerProofGenerator(pnm), d_info(info)
+{
+}
 
 void OperatorElim::checkNonLinearLogic(Node term)
 {
@@ -43,7 +46,21 @@ void OperatorElim::checkNonLinearLogic(Node term)
   }
 }
 
-Node OperatorElim::eliminateOperatorsRec(Node n)
+TrustNode OperatorElim::eliminate(Node n)
+{
+  TConvProofGenerator* tg = nullptr;
+  Node nn = eliminateOperators(n, tg);
+  if (nn != n)
+  {
+    // since elimination may introduce new operators to eliminate, we must
+    // recursively eliminate result
+    Node nnr = eliminateOperatorsRec(nn, tg);
+    return TrustNode::mkTrustRewrite(n, nnr, nullptr);
+  }
+  return TrustNode::null();
+}
+
+Node OperatorElim::eliminateOperatorsRec(Node n, TConvProofGenerator* tg)
 {
   Trace("arith-elim") << "Begin elim: " << n << std::endl;
   NodeManager* nm = NodeManager::currentNM();
@@ -91,12 +108,12 @@ Node OperatorElim::eliminateOperatorsRec(Node n)
       {
         ret = nm->mkNode(cur.getKind(), children);
       }
-      Node retElim = eliminateOperators(ret);
+      Node retElim = eliminateOperators(ret, tg);
       if (retElim != ret)
       {
         // recursively eliminate operators in result, since some eliminations
         // are defined in terms of other non-standard operators.
-        ret = eliminateOperatorsRec(retElim);
+        ret = eliminateOperatorsRec(retElim, tg);
       }
       visited[cur] = ret;
     }
@@ -106,7 +123,7 @@ Node OperatorElim::eliminateOperatorsRec(Node n)
   return visited[n];
 }
 
-Node OperatorElim::eliminateOperators(Node node)
+Node OperatorElim::eliminateOperators(Node node, TConvProofGenerator* tg)
 {
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();
@@ -138,9 +155,14 @@ Node OperatorElim::eliminateOperators(Node node)
         Node zero = mkRationalNode(0);
         Node diff = nm->mkNode(MINUS, node[0], v);
         Node lem = mkInRange(diff, zero, one);
-        toIntSkolem = sm->mkSkolem(
-            v, lem, "toInt", "a conversion of a Real term to its Integer part");
-        toIntSkolem = SkolemManager::getWitnessForm(toIntSkolem);
+        toIntSkolem =
+            sm->mkSkolem(v,
+                         lem,
+                         "toInt",
+                         "a conversion of a Real term to its Integer part",
+                         NodeManager::SKOLEM_DEFAULT,
+                         this,
+                         true);
         d_to_int_skolem[node[0]] = toIntSkolem;
       }
       else
@@ -235,9 +257,13 @@ Node OperatorElim::eliminateOperators(Node node)
                               nm->mkNode(
                                   PLUS, v, nm->mkConst(Rational(-1))))))));
         }
-        intVar = sm->mkSkolem(
-            v, lem, "linearIntDiv", "the result of an intdiv-by-k term");
-        intVar = SkolemManager::getWitnessForm(intVar);
+        intVar = sm->mkSkolem(v,
+                              lem,
+                              "linearIntDiv",
+                              "the result of an intdiv-by-k term",
+                              NodeManager::SKOLEM_DEFAULT,
+                              this,
+                              true);
         d_int_div_skolem[rw] = intVar;
       }
       else
@@ -276,9 +302,13 @@ Node OperatorElim::eliminateOperators(Node node)
         Node lem = nm->mkNode(IMPLIES,
                               den.eqNode(nm->mkConst(Rational(0))).negate(),
                               nm->mkNode(MULT, den, v).eqNode(num));
-        var = sm->mkSkolem(
-            v, lem, "nonlinearDiv", "the result of a non-linear div term");
-        var = SkolemManager::getWitnessForm(var);
+        var = sm->mkSkolem(v,
+                           lem,
+                           "nonlinearDiv",
+                           "the result of a non-linear div term",
+                           NodeManager::SKOLEM_DEFAULT,
+                           this,
+                           true);
         d_div_skolem[rw] = var;
       }
       else
@@ -424,8 +454,11 @@ Node OperatorElim::eliminateOperators(Node node)
             var,
             lem,
             "tfk",
-            "Skolem to eliminate a non-standard transcendental function");
-        ret = SkolemManager::getWitnessForm(ret);
+            "Skolem to eliminate a non-standard transcendental function",
+            NodeManager::SKOLEM_DEFAULT,
+            this,
+            true);
+        Assert(ret.getKind() == WITNESS);
         d_nlin_inverse_skolem[node] = ret;
         return ret;
       }
@@ -438,6 +471,8 @@ Node OperatorElim::eliminateOperators(Node node)
   return node;
 }
 
+Node OperatorElim::getAxiomFor(Node n) { return Node::null(); }
+
 Node OperatorElim::getArithSkolem(ArithSkolemId asi)
 {
   std::map<ArithSkolemId, Node>::iterator it = d_arith_skolem.find(asi);
diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h
index 2cdf9bc49..4646a6f13 100644
--- a/src/theory/arith/operator_elim.h
+++ b/src/theory/arith/operator_elim.h
@@ -17,43 +17,32 @@
 #include <map>
 
 #include "expr/node.h"
+#include "expr/term_conversion_proof_generator.h"
+#include "theory/eager_proof_generator.h"
 #include "theory/logic_info.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
-class OperatorElim
+class OperatorElim : public EagerProofGenerator
 {
  public:
-  OperatorElim(const LogicInfo& info);
+  OperatorElim(ProofNodeManager* pnm, const LogicInfo& info);
   ~OperatorElim() {}
+  /** Eliminate operators in this term.
+    *
+    * Eliminate operators in term n. If n has top symbol that is not a core
+    * one (including division, int division, mod, to_int, is_int, syntactic sugar
+    * transcendental functions), then we replace it by a form that eliminates
+    * that operator. This may involve the introduction of witness terms.
+    */
+  TrustNode eliminate(Node n);
   /**
-   * Eliminate operators in term n. If n has top symbol that is not a core
-   * one (including division, int division, mod, to_int, is_int, syntactic sugar
-   * transcendental functions), then we replace it by a form that eliminates
-   * that operator. This may involve the introduction of witness terms.
-   *
-   * One exception to the above rule is that we may leave certain applications
-   * like (/ 4 1) unchanged, since replacing this by 4 changes its type from
-   * real to int. This is important for some subtyping issues during
-   * expandDefinition. Moreover, applications like this can be eliminated
-   * trivially later by rewriting.
-   *
-   * This method is called both during expandDefinition and during ppRewrite.
-   *
-   * @param n The node to eliminate operators from.
-   * @return The (single step) eliminated form of n.
+   * Get axiom for term n. This returns the axiom that this class uses to
+   * eliminate the term n, which is determined by its top-most symbol.
    */
-  Node eliminateOperators(Node n);
-  /**
-   * 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);
+  static Node getAxiomFor(Node n);
 
  private:
   /** Logic info of the owner of this class */
@@ -95,6 +84,32 @@ class OperatorElim
    * function-ness of e.g. division by zero is ignored.
    */
   std::map<ArithSkolemId, Node> d_arith_skolem;
+  /**
+   * Eliminate operators in term n. If n has top symbol that is not a core
+   * one (including division, int division, mod, to_int, is_int, syntactic sugar
+   * transcendental functions), then we replace it by a form that eliminates
+   * that operator. This may involve the introduction of witness terms.
+   *
+   * One exception to the above rule is that we may leave certain applications
+   * like (/ 4 1) unchanged, since replacing this by 4 changes its type from
+   * real to int. This is important for some subtyping issues during
+   * expandDefinition. Moreover, applications like this can be eliminated
+   * trivially later by rewriting.
+   *
+   * This method is called both during expandDefinition and during ppRewrite.
+   *
+   * @param n The node to eliminate operators from.
+   * @return The (single step) eliminated form of n.
+   */
+  Node eliminateOperators(Node n, TConvProofGenerator* tg);
+  /**
+   * 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);
   /** get arithmetic skolem
    *
    * Returns the Skolem in the above map for the given id, creating it if it
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index fcbfd1baf..52321ffd4 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -39,7 +39,7 @@ TheoryArith::TheoryArith(context::Context* c,
                          ProofNodeManager* pnm)
     : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, pnm),
       d_internal(
-          new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)),
+          new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)),
       d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
       d_proofRecorder(nullptr)
 {
@@ -78,8 +78,7 @@ void TheoryArith::finishInit()
 
 TrustNode TheoryArith::expandDefinition(Node node)
 {
-  Node expNode = d_internal->expandDefinition(node);
-  return TrustNode::mkTrustRewrite(node, expNode, nullptr);
+  return d_internal->expandDefinition(node);
 }
 
 void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -93,12 +92,7 @@ void TheoryArith::addSharedTerm(TNode n){
 TrustNode TheoryArith::ppRewrite(TNode atom)
 {
   CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true);
-  Node ret = d_internal->ppRewrite(atom);
-  if (ret != atom)
-  {
-    return TrustNode::mkTrustRewrite(atom, ret, nullptr);
-  }
-  return TrustNode::null();
+  return d_internal->ppRewrite(atom);
 }
 
 Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index cdf3c16c7..6f47ffb0e 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -87,7 +87,8 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
                                        context::UserContext* u,
                                        OutputChannel& out,
                                        Valuation valuation,
-                                       const LogicInfo& logicInfo)
+                                       const LogicInfo& logicInfo,
+                                       ProofNodeManager* pnm)
     : d_containing(containing),
       d_nlIncomplete(false),
       d_rowTracking(),
@@ -156,7 +157,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
       d_solveIntMaybeHelp(0u),
       d_solveIntAttempts(0u),
       d_statistics(),
-      d_opElim(logicInfo)
+      d_opElim(pnm, logicInfo)
 {
   // only need to create if non-linear logic
   if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
@@ -1078,26 +1079,21 @@ Node TheoryArithPrivate::getModelValue(TNode term) {
   }
 }
 
-Node TheoryArithPrivate::ppRewriteTerms(TNode n) {
+TrustNode TheoryArithPrivate::ppRewriteTerms(TNode n)
+{
   if(Theory::theoryOf(n) != THEORY_ARITH) {
-    return n;
+    return TrustNode::null();
   }
   // Eliminate operators recursively. Notice we must do this here since other
   // theories may generate lemmas that involve non-standard operators. For
   // example, quantifier instantiation may use TO_INTEGER terms; SyGuS may
   // introduce non-standard arithmetic terms appearing in grammars.
   // call eliminate operators
-  Node nn = d_opElim.eliminateOperators(n);
-  if (nn != n)
-  {
-    // since elimination may introduce new operators to eliminate, we must
-    // recursively eliminate result
-    return d_opElim.eliminateOperatorsRec(nn);
-  }
-  return n;
+  return d_opElim.eliminate(n);
 }
 
-Node TheoryArithPrivate::ppRewrite(TNode atom) {
+TrustNode TheoryArithPrivate::ppRewrite(TNode atom)
+{
   Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
 
   if (options::arithRewriteEq())
@@ -1106,13 +1102,21 @@ Node TheoryArithPrivate::ppRewrite(TNode atom) {
     {
       Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
       Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
-      leq = ppRewriteTerms(leq);
-      geq = ppRewriteTerms(geq);
+      TrustNode tleq = ppRewriteTerms(leq);
+      TrustNode tgeq = ppRewriteTerms(geq);
+      if (!tleq.isNull())
+      {
+        leq = tleq.getNode();
+      }
+      if (!tgeq.isNull())
+      {
+        geq = tgeq.getNode();
+      }
       Node rewritten = Rewriter::rewrite(leq.andNode(geq));
       Debug("arith::preprocess")
           << "arith::preprocess() : returning " << rewritten << endl;
       // don't need to rewrite terms since rewritten is not a non-standard op
-      return rewritten;
+      return TrustNode::mkTrustRewrite(atom, rewritten, nullptr);
     }
   }
   return ppRewriteTerms(atom);
@@ -4812,17 +4816,10 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{
   return d_rowTracking[ridx];
 }
 
-Node TheoryArithPrivate::expandDefinition(Node node)
+TrustNode TheoryArithPrivate::expandDefinition(Node node)
 {
   // call eliminate operators
-  Node nn = d_opElim.eliminateOperators(node);
-  if (nn != node)
-  {
-    // since elimination may introduce new operators to eliminate, we must
-    // recursively eliminate result
-    return d_opElim.eliminateOperatorsRec(nn);
-  }
-  return node;
+  return d_opElim.eliminate(node);
 }
 
 std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 867029e3c..42ec7f47b 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -415,7 +415,7 @@ private:
   Node axiomIteForTotalIntDivision(Node int_div_like);
 
   // handle linear /, div, mod, and also is_int, to_int
-  Node ppRewriteTerms(TNode atom);
+  TrustNode ppRewriteTerms(TNode atom);
 
  public:
   TheoryArithPrivate(TheoryArith& containing,
@@ -423,7 +423,8 @@ private:
                      context::UserContext* u,
                      OutputChannel& out,
                      Valuation valuation,
-                     const LogicInfo& logicInfo);
+                     const LogicInfo& logicInfo,
+                     ProofNodeManager* pnm);
   ~TheoryArithPrivate();
 
   TheoryRewriter* getTheoryRewriter() { return &d_rewriter; }
@@ -432,7 +433,7 @@ private:
    * Does non-context dependent setup for a node connected to a theory.
    */
   void preRegisterTerm(TNode n);
-  Node expandDefinition(Node node);
+  TrustNode expandDefinition(Node node);
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
 
@@ -452,7 +453,7 @@ private:
   void presolve();
   void notifyRestart();
   Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
-  Node ppRewrite(TNode atom);
+  TrustNode ppRewrite(TNode atom);
   void ppStaticLearn(TNode in, NodeBuilder<>& learned);
 
   std::string identify() const { return std::string("TheoryArith"); }