diff options
Diffstat (limited to 'examples/api/python/floating_point.py')
-rw-r--r-- | examples/api/python/floating_point.py | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py index 5444a7df3..44a3d66d2 100644 --- a/examples/api/python/floating_point.py +++ b/examples/api/python/floating_point.py @@ -16,16 +16,16 @@ # Darulova. This requires building cvc5 with symfpu. ## -import pycvc4 -from pycvc4 import kinds +import pycvc5 +from pycvc5 import kinds if __name__ == "__main__": - slv = pycvc4.Solver() + slv = pycvc5.Solver() if not slv.supportsFloatingPoint(): - # CVC4 must be built with SymFPU to support the theory of + # cvc5 must be built with SymFPU to support the theory of # floating-point numbers - print("CVC4 was not built with floating-point support.") + print("cvc5 was not built with floating-point support.") exit() slv.setOption("produce-models", "true") @@ -35,7 +35,7 @@ if __name__ == "__main__": fp32 = slv.mkFloatingPointSort(8, 24) # the standard rounding mode - rm = slv.mkRoundingMode(pycvc4.RoundNearestTiesToEven) + rm = slv.mkRoundingMode(pycvc5.RoundNearestTiesToEven) # create a few single-precision variables x = slv.mkConst(fp32, 'x') @@ -49,7 +49,7 @@ if __name__ == "__main__": slv.assertFormula(slv.mkTerm(kinds.Not, commutative)) print("Checking floating-point commutativity") print("Expect SAT (property does not hold for NaN and Infinities).") - print("CVC4:", slv.checkSat()) + print("cvc5:", slv.checkSat()) print("Model for x:", slv.getValue(x)) print("Model for y:", slv.getValue(y)) @@ -61,7 +61,7 @@ if __name__ == "__main__": print("Checking floating-point commutativity assuming x and y are not NaN or Infinity") print("Expect UNSAT.") - print("CVC4:", slv.checkSat()) + print("cvc5:", slv.checkSat()) # check floating-point arithmetic is not associative slv.pop() @@ -84,7 +84,7 @@ if __name__ == "__main__": print("Checking floating-point associativity") print("Expect SAT.") - print("CVC4:", slv.checkSat()) + print("cvc5:", slv.checkSat()) print("Model for x:", slv.getValue(x)) print("Model for y:", slv.getValue(y)) print("Model for z:", slv.getValue(z)) |