diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-29 19:42:50 -0500 |
---|---|---|
committer | Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> | 2019-10-29 17:42:50 -0700 |
commit | 8dda9531995953c3cec094339002f2ee7cadae08 (patch) | |
tree | a3c4b194878133a1c46de15c15c6d4e420fe6bad /src/theory/arith/arith_utilities.h | |
parent | d6a8803054c0c5731a6c4111d8d00c18e2953032 (diff) |
Split some generic utilities from the non-linear extension (#3419)
* Split arith util
* Cleaner
* cpp
* Format
* Minor
Diffstat (limited to 'src/theory/arith/arith_utilities.h')
-rw-r--r-- | src/theory/arith/arith_utilities.h | 30 |
1 files changed, 27 insertions, 3 deletions
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 */ |