diff options
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): |