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
--- /dev/null
+/********************* */
+/*! \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
** 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"
#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>
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 */
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;
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,
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
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
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;
* 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
projects / cvc5.git / commitdiff