From: Andrew Reynolds Date: Wed, 30 Oct 2019 00:42:50 +0000 (-0500) Subject: Split some generic utilities from the non-linear extension (#3419) X-Git-Tag: cvc5-1.0.0~3869 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8dda9531995953c3cec094339002f2ee7cadae08;p=cvc5.git Split some generic utilities from the non-linear extension (#3419) * Split arith util * Cleaner * cpp * Format * Minor --- 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(); + + 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 #include #include #include @@ -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 b) and (a b), then (a 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 b) and (b c) then (a 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 b, a b, we know a 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 b, b c, we know a 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 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(); - - 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