diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-09 11:27:16 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-09 11:27:16 -0500 |
commit | 9662830ebf97954ebe14055eb4503beba134d3c3 (patch) | |
tree | ac521e6067bb0de85c683918e18d1dcb0dce1ace /src/api/python/cvc5.pxi | |
parent | 4d08fa6705aac1099fe73468d4ed6dd2d97771ba (diff) | |
parent | 0c982a7486ef9b6991589685f9091602e0cf5572 (diff) |
Merge branch 'master' into smtcompoptssmtcompopts
Diffstat (limited to 'src/api/python/cvc5.pxi')
-rw-r--r-- | src/api/python/cvc5.pxi | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 3339543f3..258005207 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -740,6 +740,21 @@ cdef class Solver: return term def mkReal(self, val, den=None): + ''' + Make a real number term. + + Really, makes a rational term. + + Can be used in various forms. + * Given a string "N/D" constructs the corresponding rational. + * Given a string "W.D" constructs the reduction of (W * P + D)/P, where + P is the appropriate power of 10. + * Given a float f, constructs the rational matching f's string + representation. This means that mkReal(0.3) gives 3/10 and not the + IEEE-754 approximation of 3/10. + * Given a string "W" or an integer, constructs that integer. + * Given two strings and/or integers N and D, constructs N/D. + ''' cdef Term term = Term(self) if den is None: term.cterm = self.csolver.mkReal(str(val).encode()) @@ -1766,12 +1781,14 @@ cdef class Term: return self.cterm.isRealValue() def getRealValue(self): - return float(Fraction(self.cterm.getRealValue().decode())) + '''Returns the value of a real term as a Fraction''' + return Fraction(self.cterm.getRealValue().decode()) def isBitVectorValue(self): return self.cterm.isBitVectorValue() def getBitVectorValue(self, base = 2): + '''Returns the value of a bit-vector term as a 0/1 string''' return self.cterm.getBitVectorValue(base).decode() def toPythonObj(self): |