search

epfl-lara / ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver
Apache License 2.0
122 stars 34 forks source link

add support for mkNumeral in Z3Wrapper and Z3Contex, and everything Real related #13

Closed remi-delmas-3000 closed 5 years ago

remi-delmas-3000 commented 11 years ago

Add a method mkNumeral(String, Sort) in the Z3Context to be able to create arbitrary precision integers and real numbers based on their string representation (reals are written as rational fractions with arbitrary precision integers as numerators and denominators). Current state of the Z3Context only allows Int constants and and fractions of integers for Real constants.

Also, add support for get methods for numeral values of Real sort, especially those which return string representations.

romac commented 6 years ago

I think we can close this as support was added in ca62ad2d.