Support for multiple (check-sat)
Closed this issue · 3 comments
Dear all,
Using the following code, Z3 first replies sat
and then it replies unsat
.
(set-logic QF_NRA)
(declare-fun x () Real)
(assert (> x 0.0))
(assert (< x 2.0))
(check-sat)
(assert (> x 5.0))
(check-sat)
(exit)
According to my understanding, the first check-sat
is based on just the first two assertions, and the second check-sat
also considers the third assertion. In the first case there is a solution (e.g. x == 1), but in the second case it becomes unsat.
You can also verify this online at:
http://rise4fun.com/z3
If I run the same code on dReal, it just says:
delta-sat with delta = 0.00100000000000000
One first thing I did not understand is: why is dReal giving just one reply, considering I asked to check satisfiability twice? (using two different check-sat
commands)
If I try to run it using the --model
option, it still says delta-sat
just once, but it provides two solutions. The output is below.
Solution:
x : [ ENTIRE ] = [0, 2]
Solution:
x : [ ENTIRE ] = [5, inf]
delta-sat with delta = 0.00100000000000000
You can also verify this online at:
http://dreal.github.io/try/
I also do not understand this reply. The first provided solution seems correct (it is compatible with the solution provided by Z3), but I think the second one is incorrect, and I think that after the first check-sat
is executed, the solver forgets about the two assertions before it, then when the second check-sat
is executed, the solver only considers the third assertion.
Am I wrong? May this be a bug? Probably multiple check-sat
commands are not supported? Is there a way to simulate the Z3 behavior, maybe using push
and pop
mechanisms?
Would the output be different if I use the dReal APIs instead? About this, how should I write the above problem using the dReal C++ APIs instead of writing it in SMT2 format?
My OS is Ubuntu 14.04 64bit and I installed the precompiled dReal binaries using apt-get
with the dReal repository.
Many thanks for all your work and support.
Hi @AndreaCallia, thanks for the report. The delta-sat
from the second check-sat
is a bug and I'm working on a fix. I'll also change it to have an output for each check-sat
command.
Many thanks for this fix @soonho-tri ...