(proof-new) Simplifications to arithmetic operator elimination and preprocessing...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 3 Mar 2021 17:25:02 +0000 (11:25 -0600)
committerGitHub <noreply@github.com>
Wed, 3 Mar 2021 17:25:02 +0000 (17:25 +0000)
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.

src/theory/arith/operator_elim.cpp
src/theory/arith/operator_elim.h
src/theory/arith/theory_arith.cpp

index fbd1798cd813f8585a33d1242f99654af91a3f6d..e34c0110e3f5a62348d19b7f15d8d9710b561c8d 100644 (file)
@@ -52,86 +52,16 @@ TrustNode OperatorElim::eliminate(Node n, bool partialOnly)
   Node nn = eliminateOperators(n, tg, partialOnly);
   if (nn != n)
   {
-    // since elimination may introduce new operators to eliminate, we must
-    // recursively eliminate result
-    Node nnr = eliminateOperatorsRec(nn, tg, partialOnly);
-    return TrustNode::mkTrustRewrite(n, nnr, nullptr);
+    return TrustNode::mkTrustRewrite(n, nn, nullptr);
   }
   return TrustNode::null();
 }
 
-Node OperatorElim::eliminateOperatorsRec(Node n,
-                                         TConvProofGenerator* tg,
-                                         bool partialOnly)
-{
-  Trace("arith-elim") << "Begin elim: " << n << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
-  std::unordered_map<Node, Node, TNodeHashFunction> visited;
-  std::unordered_map<Node, Node, TNodeHashFunction>::iterator it;
-  std::vector<Node> visit;
-  Node cur;
-  visit.push_back(n);
-  do
-  {
-    cur = visit.back();
-    visit.pop_back();
-    it = visited.find(cur);
-    if (Theory::theoryOf(cur) != THEORY_ARITH)
-    {
-      visited[cur] = cur;
-    }
-    else if (it == visited.end())
-    {
-      visited[cur] = Node::null();
-      visit.push_back(cur);
-      for (const Node& cn : cur)
-      {
-        visit.push_back(cn);
-      }
-    }
-    else if (it->second.isNull())
-    {
-      Node ret = cur;
-      bool childChanged = false;
-      std::vector<Node> children;
-      if (cur.getMetaKind() == metakind::PARAMETERIZED)
-      {
-        children.push_back(cur.getOperator());
-      }
-      for (const Node& cn : cur)
-      {
-        it = visited.find(cn);
-        Assert(it != visited.end());
-        Assert(!it->second.isNull());
-        childChanged = childChanged || cn != it->second;
-        children.push_back(it->second);
-      }
-      if (childChanged)
-      {
-        ret = nm->mkNode(cur.getKind(), children);
-      }
-      Node retElim = eliminateOperators(ret, tg, partialOnly);
-      if (retElim != ret)
-      {
-        // recursively eliminate operators in result, since some eliminations
-        // are defined in terms of other non-standard operators.
-        ret = eliminateOperatorsRec(retElim, tg, partialOnly);
-      }
-      visited[cur] = ret;
-    }
-  } while (!visit.empty());
-  Assert(visited.find(n) != visited.end());
-  Assert(!visited.find(n)->second.isNull());
-  return visited[n];
-}
-
 Node OperatorElim::eliminateOperators(Node node,
                                       TConvProofGenerator* tg,
                                       bool partialOnly)
 {
   NodeManager* nm = NodeManager::currentNM();
-  SkolemManager* sm = nm->getSkolemManager();
-
   Kind k = node.getKind();
   switch (k)
   {
@@ -164,14 +94,8 @@ 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",
-                         NodeManager::SKOLEM_DEFAULT,
-                         this,
-                         true);
+        toIntSkolem = mkWitnessTerm(
+            v, lem, "toInt", "a conversion of a Real term to its Integer part");
         d_to_int_skolem[node[0]] = toIntSkolem;
       }
       else
@@ -271,13 +195,8 @@ 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",
-                              NodeManager::SKOLEM_DEFAULT,
-                              this,
-                              true);
+        intVar = mkWitnessTerm(
+            v, lem, "linearIntDiv", "the result of an intdiv-by-k term");
         d_int_div_skolem[rw] = intVar;
       }
       else
@@ -321,13 +240,8 @@ 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",
-                           NodeManager::SKOLEM_DEFAULT,
-                           this,
-                           true);
+        var = mkWitnessTerm(
+            v, lem, "nonlinearDiv", "the result of a non-linear div term");
         d_div_skolem[rw] = var;
       }
       else
@@ -404,6 +318,11 @@ Node OperatorElim::eliminateOperators(Node node,
     case ARCSECANT:
     case ARCCOTANGENT:
     {
+      if (partialOnly)
+      {
+        // not eliminating total operators
+        return node;
+      }
       checkNonLinearLogic(node);
       // eliminate inverse functions here
       std::map<Node, Node>::const_iterator it =
@@ -469,14 +388,11 @@ Node OperatorElim::eliminateOperators(Node node,
           lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
         }
         Assert(!lem.isNull());
-        Node ret = sm->mkSkolem(
+        Node ret = mkWitnessTerm(
             var,
             lem,
             "tfk",
-            "Skolem to eliminate a non-standard transcendental function",
-            NodeManager::SKOLEM_DEFAULT,
-            this,
-            true);
+            "Skolem to eliminate a non-standard transcendental function");
         Assert(ret.getKind() == WITNESS);
         d_nlin_inverse_skolem[node] = ret;
         return ret;
@@ -557,6 +473,18 @@ Node OperatorElim::getArithSkolemApp(Node n, ArithSkolemId asi)
   return skolem;
 }
 
+Node OperatorElim::mkWitnessTerm(Node v,
+                                 Node pred,
+                                 const std::string& prefix,
+                                 const std::string& comment)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
+  Node k = sm->mkSkolem(
+      v, pred, prefix, comment, NodeManager::SKOLEM_DEFAULT, this, true);
+  return k;
+}
+
 }  // namespace arith
 }  // namespace theory
 }  // namespace CVC4
index bca80ea4db95e3f8af5d68347c718f74b180839a..cf5b9248c92fb40bc158bce9f87128390c950589 100644 (file)
@@ -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
index 6de5c72213c7e4ea268ef1b30b3d7b43fb450764..9bca5e182a2fc29cb1f9c3c71bbdbd3fa6f2311e 100644 (file)
@@ -119,16 +119,6 @@ TrustNode TheoryArith::ppRewrite(TNode atom)
       Assert(atom[0].getType().isReal());
       Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1];
       Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1];
-      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;