search

dreal / dreal3

There is a new version of dReal, available at https://github.com/dreal/dreal4
GNU General Public License v3.0
48 stars 36 forks source link

dReal v3.16.06 gives only upper bound when finding a model of "x > 0" #259

Closed nikosarechiga closed 8 years ago

nikosarechiga commented 8 years ago

Correct output is [0, +INFTY], but dReal returns [ +INFTY]. Added the smt2 and smt2.model files in a zip, because apparently github doesn't like smt2/smt2.model files.

badquery.zip

soonhokong commented 8 years ago

Further discussion revealed that it's due to the way we print out intervals with infinity. See the code in the filib++ that we're depending on.

We agree to change the code so that we have [+INFTY, +INFTY] for +oo and [-INFTY, -INFTY] for -oo.

soonhokong commented 8 years ago

Now it outputs:

Solution:
x : [ ENTIRE ] = [+INFTY, +INFTY]
delta-sat with delta = 0.00100000000000000
soonhokong commented 8 years ago

You need to do make update_pkgs. I also picked up new commits for the new version of IBEX. I'll run regression tests and release a new version.

nikosarechiga commented 8 years ago

main concern is with the model file--what will the model file show?

soonhokong commented 8 years ago

@narechiga, it's the same [+INFTY, +INFTY]:

delta-sat with the following box:
    x : [+INFTY, +INFTY]
soonhokong commented 8 years ago

Closed by https://github.com/dreal-deps/filibxx/commit/614c01ba587ddff84b9fc144064cbf453398a668.