diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-06-21 22:29:01 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-06-21 22:29:01 -0700 |
| commit | 252a8fb4323fed6eb621a4f88a06abfc39307b76 (patch) | |
| tree | 1858636286f1c657c2fd03ec4c788db8602d1489 /src/util | |
| parent | be33ac9656bf7feafa3715d6623749f6afd962b5 (diff) | |
Add floating-point support in the Java API (#3063)
This commit adds support for the theory of floating-point numbers in the
Java API. Previously, floating-point related classes were missing in the
JAR. The commit also provides an example that showcases how to work with
the theory of floating-point numbers through the API.
Diffstat (limited to 'src/util')
| -rw-r--r-- | src/util/floatingpoint.i | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/util/floatingpoint.i b/src/util/floatingpoint.i index c66cc311d..7a57de057 100644 --- a/src/util/floatingpoint.i +++ b/src/util/floatingpoint.i @@ -2,4 +2,17 @@ #include "util/floatingpoint.h" %} +// Ignore the methods related to FloatingPointLiteral (otherwise we have to +// wrap those classes as well) +%ignore CVC4::FloatingPointLiteral; +%ignore CVC4::FloatingPoint::FloatingPoint (const FloatingPointSize &oldt, const FloatingPointLiteral &oldfpl); +%ignore CVC4::FloatingPoint::getLiteral () const; + +// Ignore the partial methods (otherwise we have to provide a template +// instantiation for std::pair<FloatingPoint, bool> which is quite ugly) +%ignore CVC4::FloatingPoint::max(const FloatingPoint &arg) const; +%ignore CVC4::FloatingPoint::min(const FloatingPoint &arg) const; +%ignore CVC4::FloatingPoint::convertToRational() const; +%ignore CVC4::FloatingPoint::convertToBV(BitVectorSize width, const RoundingMode &rm, bool signedBV) const; + %include "util/floatingpoint.h" |