Sorry this is a basic question, I'm new to z3.
I wrote a program to find a real solution to a certain equation. Since it should be generated for every equation, I can't simplify the equation to much beforehand. But the program is really slow. It is a long equation, but I only have 4 unknown variables, so I wouldn't expect it to take this long (Similar equations (but shorter) had a much shorter runtime and where done in milliseconds). Did I somehow create a loop or is this equation really to complicated.
(declare-const l1 Real)
(declare-const l0 Real)
(declare-const sqrt0 Real)
(assert
(>= sqrt0 0)
)
(assert
(=
(^ sqrt0 2)
(+
(^ l0 2)
(^ l1 2)
)
)
)
(declare-const sqrt1 Real)
(assert
(>= sqrt1 0)
)
(assert
(=
(^ sqrt1 2)
(-
(^ sqrt0 2)
1)
)
)
(assert
(=
(+
(^
(- 0.625000 l0)
2)
(^
(- 0.414578 l1)
2)
)
(^
(+
(/ 1
(-
(* -2 sqrt0)
(* 2 sqrt1)
)
)
(+
(* 0.5 sqrt0)
(* 0.5 sqrt1)
)
)
2)
)
)
(assert
(=
(+
(^
(- 0.500000 l0)
2)
(^
(- 0.000000 l1)
2)
)
(^
(+
(/ 1
(-
(* -2 sqrt0)
(* 2 sqrt1)
)
)
(+
(* 0.5 sqrt0)
(* 0.5 sqrt1)
)
)
2)
)
)
)
(check-sat)
I tried using the FloatingPoint type with the built in fp.sqrt function, but it didn't make program any faster (Maybe I'm wrong but I also couldn't find a built square function for FLoatingPoint, so I used fp.mul). I hoped using the fp.sqrt function would help alot, as after is should only have two unknown constants.
Thanks in advance and sorry if this is a stupid question.
It's anybody's guess when a solver takes too long to answer: It could be stuck in some sort of a non-productive loop, or the problem can genuinely be too hard to solve. From this perspective, most solvers act as a block-box: Unless you're intimately familiar with their internals, it's hard to guess what might be going wrong.
If you do believe this should be "easy" to solve, you can file a ticket at: https://github.com/Z3Prover/z3/issues and have the developers take a look. I doubt this'll be very productive, but they might be able to trace the internals and at least tell if this is a genuine issue, or just simply too difficult.
The other option is to use dReal: http://dreal.github.io. Note that dReal is a delta-sat tool, i.e., the solutions are considered OK up to a certain numerical error bound, which can be specified by the user. Since the result doesn't have to be precise, it can run a lot faster and usually finds "acceptable" solutions. Of course, what acceptable means will depend on your particular problem domain, and you might have to tweak with parameters a bit. (For instance, you might have to assert some upper-lower bounds for l0 and l1, so you don't run into floating-point overflows. In dReal, "real" numbers are modeled by IEEE-double-precision-floating point values.)
So, I'd give dReal a try, and see if it works better for you. But keep in mind that the solutions will be within an error-bound, which might be just fine for your application.