Split some generic utilities from the non-linear extension (#3419)

* Split arith util

* Cleaner

* cpp

* Format

* Minor

5 files changed, 224 insertions, 190 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index b6b4acffb..dd2b7eaea 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -268,6 +268,7 @@ libcvc4_add_sources(
   theory/arith/arith_rewriter.h
   theory/arith/arith_static_learner.cpp
   theory/arith/arith_static_learner.h
+  theory/arith/arith_utilities.cpp
   theory/arith/arith_utilities.h
   theory/arith/arithvar.cpp
   theory/arith/arithvar.h
diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp
new file mode 100644
index 000000000..3d3078d99
--- /dev/null
+++ b/src/theory/arith/arith_utilities.cpp
@@ -0,0 +1,196 @@
+/*********************                                                        */
+/*! \file arith_utilities.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of common functions for dealing with nodes.
+ **/
+
+#include "arith_utilities.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+Kind joinKinds(Kind k1, Kind k2)
+{
+  if (k2 < k1)
+  {
+    return joinKinds(k2, k1);
+  }
+  else if (k1 == k2)
+  {
+    return k1;
+  }
+  Assert(isRelationOperator(k1));
+  Assert(isRelationOperator(k2));
+  if (k1 == EQUAL)
+  {
+    if (k2 == LEQ || k2 == GEQ)
+    {
+      return k1;
+    }
+  }
+  else if (k1 == LT)
+  {
+    if (k2 == LEQ)
+    {
+      return k1;
+    }
+  }
+  else if (k1 == LEQ)
+  {
+    if (k2 == GEQ)
+    {
+      return EQUAL;
+    }
+  }
+  else if (k1 == GT)
+  {
+    if (k2 == GEQ)
+    {
+      return k1;
+    }
+  }
+  return UNDEFINED_KIND;
+}
+
+Kind transKinds(Kind k1, Kind k2)
+{
+  if (k2 < k1)
+  {
+    return transKinds(k2, k1);
+  }
+  else if (k1 == k2)
+  {
+    return k1;
+  }
+  Assert(isRelationOperator(k1));
+  Assert(isRelationOperator(k2));
+  if (k1 == EQUAL)
+  {
+    return k2;
+  }
+  else if (k1 == LT)
+  {
+    if (k2 == LEQ)
+    {
+      return k1;
+    }
+  }
+  else if (k1 == GT)
+  {
+    if (k2 == GEQ)
+    {
+      return k1;
+    }
+  }
+  return UNDEFINED_KIND;
+}
+
+bool isTranscendentalKind(Kind k)
+{
+  // many operators are eliminated during rewriting
+  Assert(k != TANGENT && k != COSINE && k != COSECANT
+         && k != SECANT && k != COTANGENT);
+  return k == EXPONENTIAL || k == SINE || k == PI;
+}
+
+Node getApproximateConstant(Node c, bool isLower, unsigned prec)
+{
+  Assert(c.isConst());
+  Rational cr = c.getConst<Rational>();
+
+  unsigned lower = 0;
+  unsigned upper = pow(10, prec);
+
+  Rational den = Rational(upper);
+  if (cr.getDenominator() < den.getNumerator())
+  {
+    // denominator is not more than precision, we return it
+    return c;
+  }
+
+  int csign = cr.sgn();
+  Assert(csign != 0);
+  if (csign == -1)
+  {
+    cr = -cr;
+  }
+  Rational one = Rational(1);
+  Rational ten = Rational(10);
+  Rational pow_ten = Rational(1);
+  // inefficient for large numbers
+  while (cr >= one)
+  {
+    cr = cr / ten;
+    pow_ten = pow_ten * ten;
+  }
+  Rational allow_err = one / den;
+
+  // now do binary search
+  Rational two = Rational(2);
+  NodeManager* nm = NodeManager::currentNM();
+  Node cret;
+  do
+  {
+    unsigned curr = (lower + upper) / 2;
+    Rational curr_r = Rational(curr) / den;
+    Rational err = cr - curr_r;
+    int esign = err.sgn();
+    if (err.abs() <= allow_err)
+    {
+      if (esign == 1 && !isLower)
+      {
+        curr_r = Rational(curr + 1) / den;
+      }
+      else if (esign == -1 && isLower)
+      {
+        curr_r = Rational(curr - 1) / den;
+      }
+      curr_r = curr_r * pow_ten;
+      cret = nm->mkConst(csign == 1 ? curr_r : -curr_r);
+    }
+    else
+    {
+      Assert(esign != 0);
+      // update lower/upper
+      if (esign == -1)
+      {
+        upper = curr;
+      }
+      else if (esign == 1)
+      {
+        lower = curr;
+      }
+    }
+  } while (cret.isNull());
+  return cret;
+}
+
+void printRationalApprox(const char* c, Node cr, unsigned prec)
+{
+  Assert(cr.isConst());
+  Node ca = getApproximateConstant(cr, true, prec);
+  if (ca != cr)
+  {
+    Trace(c) << "(+ ";
+  }
+  Trace(c) << ca;
+  if (ca != cr)
+  {
+    Trace(c) << " [0,10^" << prec << "])";
+  }
+}
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index c8e92dfd3..4588a5848 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -9,9 +9,7 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Arith utilities are common inline functions for dealing with nodes.
- **
- ** Arith utilities are common functions for dealing with nodes.
+ ** \brief Common functions for dealing with nodes.
  **/
 
 #include "cvc4_private.h"
@@ -19,6 +17,7 @@
 #ifndef CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 #define CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 
+#include <math.h>
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>
@@ -302,6 +301,31 @@ inline Node mkPi()
   return NodeManager::currentNM()->mkNullaryOperator(
       NodeManager::currentNM()->realType(), kind::PI);
 }
+/** Join kinds, where k1 and k2 are arithmetic relations returns an
+ * arithmetic relation ret such that
+ * if (a <k1> b) and (a <k2> b), then (a <ret> b).
+ */
+Kind joinKinds(Kind k1, Kind k2);
+
+/** Transitive kinds, where k1 and k2 are arithmetic relations returns an
+ * arithmetic relation ret such that
+ * if (a <k1> b) and (b <k2> c) then (a <ret> c).
+ */
+Kind transKinds(Kind k1, Kind k2);
+
+/** Is k a transcendental function kind? */
+bool isTranscendentalKind(Kind k);
+/**
+ * Get a lower/upper approximation of the constant r within the given
+ * level of precision. In other words, this returns a constant c' such that
+ *   c' <= c <= c' + 1/(10^prec) if isLower is true, or
+ *   c' + 1/(10^prec) <= c <= c' if isLower is false.
+ * where c' is a rational of the form n/d for some n and d <= 10^prec.
+ */
+Node getApproximateConstant(Node c, bool isLower, unsigned prec);
+
+/** print rational approximation of cr with precision prec on trace c */
+void printRationalApprox(const char* c, Node cr, unsigned prec = 5);
 
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 4dfda79b7..4747727c8 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -553,85 +553,6 @@ Node NonlinearExtension::mkBounded( Node l, Node a, Node u ) {
       NodeManager::currentNM()->mkNode(LEQ, a, u));
 }
 
-// by a <k1> b, a <k2> b, we know a <ret> b
-Kind NonlinearExtension::joinKinds(Kind k1, Kind k2) {
-  if (k2 < k1) {
-    return joinKinds(k2, k1);
-  } else if (k1 == k2) {
-    return k1;
-  } else {
-    Assert(k1 == EQUAL || k1 == LT || k1 == LEQ || k1 == GT || k1 == GEQ);
-    Assert(k2 == EQUAL || k2 == LT || k2 == LEQ || k2 == GT || k2 == GEQ);
-    if (k1 == EQUAL)
-    {
-      if (k2 == LEQ || k2 == GEQ)
-      {
-        return k1;
-      }
-    }
-    else if (k1 == LT)
-    {
-      if (k2 == LEQ)
-      {
-        return k1;
-      }
-    }
-    else if (k1 == LEQ)
-    {
-      if (k2 == GEQ)
-      {
-        return EQUAL;
-      }
-    }
-    else if (k1 == GT)
-    {
-      if (k2 == GEQ)
-      {
-        return k1;
-      }
-    }
-    return UNDEFINED_KIND;
-  }
-}
-
-// by a <k1> b, b <k2> c, we know a <ret> c
-Kind NonlinearExtension::transKinds(Kind k1, Kind k2) {
-  if (k2 < k1) {
-    return transKinds(k2, k1);
-  } else if (k1 == k2) {
-    return k1;
-  } else {
-    Assert(k1 == EQUAL || k1 == LT || k1 == LEQ || k1 == GT || k1 == GEQ);
-    Assert(k2 == EQUAL || k2 == LT || k2 == LEQ || k2 == GT || k2 == GEQ);
-    if (k1 == EQUAL)
-    {
-      return k2;
-    }
-    else if (k1 == LT)
-    {
-      if (k2 == LEQ)
-      {
-        return k1;
-      }
-    }
-    else if (k1 == GT)
-    {
-      if (k2 == GEQ)
-      {
-        return k1;
-      }
-    }
-    return UNDEFINED_KIND;
-  }
-}
-
-bool NonlinearExtension::isTranscendentalKind(Kind k) {
-  // many operators are eliminated during rewriting
-  Assert(k != TANGENT && k != COSINE && k != COSECANT && k != SECANT
-         && k != COTANGENT);
-  return k == EXPONENTIAL || k == SINE || k == PI;
-}
- 
 Node NonlinearExtension::mkMonomialRemFactor(
     Node n, const NodeMultiset& n_exp_rem) const {
   std::vector<Node> children;
@@ -2675,84 +2596,6 @@ void NonlinearExtension::getCurrentPiBounds( std::vector< Node >& lemmas ) {
   lemmas.push_back( pi_lem );
 }
 
-Node NonlinearExtension::getApproximateConstant(Node c,
-                                                bool isLower,
-                                                unsigned prec) const
-{
-  Assert(c.isConst());
-  Rational cr = c.getConst<Rational>();
-
-  unsigned lower = 0;
-  unsigned upper = pow(10, prec);
-
-  Rational den = Rational(upper);
-  if (cr.getDenominator() < den.getNumerator())
-  {
-    // denominator is not more than precision, we return it
-    return c;
-  }
-
-  int csign = cr.sgn();
-  Assert(csign != 0);
-  if (csign == -1)
-  {
-    cr = -cr;
-  }
-  Rational one = Rational(1);
-  Rational ten = Rational(10);
-  Rational pow_ten = Rational(1);
-  // inefficient for large numbers
-  while (cr >= one)
-  {
-    cr = cr / ten;
-    pow_ten = pow_ten * ten;
-  }
-  Rational allow_err = one / den;
-
-  Trace("nl-ext-approx") << "Compute approximation for " << c << ", precision "
-                         << prec << "..." << std::endl;
-  // now do binary search
-  Rational two = Rational(2);
-  NodeManager * nm = NodeManager::currentNM();
-  Node cret;
-  do
-  {
-    unsigned curr = (lower + upper) / 2;
-    Rational curr_r = Rational(curr) / den;
-    Rational err = cr - curr_r;
-    int esign = err.sgn();
-    if (err.abs() <= allow_err)
-    {
-      if (esign == 1 && !isLower)
-      {
-        curr_r = Rational(curr + 1) / den;
-      }
-      else if (esign == -1 && isLower)
-      {
-        curr_r = Rational(curr - 1) / den;
-      }
-      curr_r = curr_r * pow_ten;
-      cret = nm->mkConst(csign == 1 ? curr_r : -curr_r);
-    }
-    else
-    {
-      Assert(esign != 0);
-      // update lower/upper
-      if (esign == -1)
-      {
-        upper = curr;
-      }
-      else if (esign == 1)
-      {
-        lower = curr;
-      }
-    }
-  } while (cret.isNull());
-  Trace("nl-ext-approx") << "Approximation for " << c << " for precision "
-                         << prec << " is " << cret << std::endl;
-  return cret;
-}
-
 bool NonlinearExtension::getApproximateSqrt(Node c,
                                             Node& l,
                                             Node& u,
@@ -2798,23 +2641,6 @@ bool NonlinearExtension::getApproximateSqrt(Node c,
   return true;
 }
 
-void NonlinearExtension::printRationalApprox(const char* c,
-                                             Node cr,
-                                             unsigned prec) const
-{
-  Assert(cr.isConst());
-  Node ca = getApproximateConstant(cr, true, prec);
-  if (ca != cr)
-  {
-    Trace(c) << "(+ ";
-  }
-  Trace(c) << ca;
-  if (ca != cr)
-  {
-    Trace(c) << " [0,10^" << prec << "])";
-  }
-}
-
 void NonlinearExtension::printModelValue(const char* c,
                                          Node n,
                                          unsigned prec) const
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index 7452e322b..7bed514cd 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -195,9 +195,6 @@ class NonlinearExtension {
   static Node mkAbs(Node a);
   static Node mkValidPhase(Node a, Node pi);
   static Node mkBounded( Node l, Node a, Node u );
-  static Kind joinKinds(Kind k1, Kind k2);
-  static Kind transKinds(Kind k1, Kind k2);
-  static bool isTranscendentalKind(Kind k);
   Node mkMonomialRemFactor(Node n, const NodeMultiset& n_exp_rem) const;
   //---------------------------------------end term utilities
 
@@ -558,8 +555,6 @@ class NonlinearExtension {
 
   void mkPi();
   void getCurrentPiBounds( std::vector< Node >& lemmas );
-  /** print rational approximation */
-  void printRationalApprox(const char* c, Node cr, unsigned prec = 5) const;
   /** print model value */
   void printModelValue(const char* c, Node n, unsigned prec = 5) const;
 
@@ -691,14 +686,6 @@ class NonlinearExtension {
    * to a non-variable.
    */
   bool isRefineableTfFun(Node tf);
-  /**
-   * Get a lower/upper approximation of the constant r within the given
-   * level of precision. In other words, this returns a constant c' such that
-   *   c' <= c <= c' + 1/(10^prec) if isLower is true, or
-   *   c' + 1/(10^prec) <= c <= c' if isLower is false.
-   * where c' is a rational of the form n/d for some n and d <= 10^prec.
-   */
-  Node getApproximateConstant(Node c, bool isLower, unsigned prec) const;
   /** get approximate sqrt
    *
    * This approximates the square root of positive constant c. If this method