search

epfl-lara / ScalaZ3

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

Missing support for Real sort. #4

Closed msama closed 12 years ago

msama commented 12 years ago

There is no support for Real, or at least the z3 api for real is not accessibile from the wrapper.

dipakc commented 12 years ago

I also need Real support. I can define a integer literal using z3.mkInt("5", z3.mkIntSort()). However, if I want to define a real literal (eg 5.5), I couldn't find z3.mkReal API. ( Note that there is mkRealSort API in the interface but I couldn't find any way to to create real literals)

msama commented 12 years ago

Z3 let you define real as fraction. http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaca5f639e917eb848b6289fb9add5744d

In my fork I added z3.mkReal(numerator, denominator) as in the Z3 API. https://github.com/msama/ScalaZ3

dipakc commented 12 years ago

thanks msama.

psuter commented 12 years ago

Sorry, I had close to no time to work on ScalaZ3 recently. @msama, since you seem to have worked on this could you perhaps prepare a pull request? That would be great.

msama commented 12 years ago

Yes sure!

psuter commented 12 years ago

Thanks! Just merged it.