search

epfl-lara / ScalaZ3

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

Could not find mkFPConst(String) for floats similar to mkRealCons(String) #75

Open AnishGG opened 4 years ago

AnishGG commented 4 years ago

Hello, Thank you for the awesome API.

I am completely new to z3 and I am trying to perform a constraint satisfying problem. This is what I want to achieve:

a * 2.5 < 5
1 < a < 3.5

But I am not able to find any way to represent a which should be a floating point number. Can someone help me here.

Also, are there any examples that I can refer to, for scalaZ3. Any help would be much appreciated!