Wrong unsat

[scungao]

This formula should be sat. New version returns unsat. Old version is correct.

(set-logic QF_NRA)
(declare-fun xd () Real)
(declare-fun theta () Real)
(declare-fun thetad () Real)
(declare-fun u () Real)
(assert (<= xd 10))
(assert (>= xd -10))
(assert (<= theta 4))
(assert (>= theta -4))
(assert (<= thetad 10))
(assert (>= thetad -10))
(assert (<= u 10))
(assert (>= u -10))
(assert (and (and (= thetad 0) (and (= xd 0) (= (/ (+ (+ (* (* (* 1.0 1.0) (sin theta)) (^ thetad 2)) (* 1.0 (* 9.8 (* (cos theta) (sin theta))))) u) (+ (* 1.0 (^ (sin theta) 2)) 2.0)) 0))) (= (/ (+ (+ (* (* (* (* 1.0 1.0) (sin theta)) (cos theta)) (^ thetad 2)) (* (* (+ 1.0 2.0) 9.8) (sin theta))) (* (cos theta) u)) (* (- 0 1.0) (+ (* 1.0 (^ (sin theta) 2)) 2.0))) 0)))
(check-sat)
(exit)

[soonhokong]

FYI, this is a bug of dReal, not IBEX. Let me revisit this after finishing up forall_t.

[scungao]

Great :)

On Jan 28, 2015, at 13:08, Soonho Kong notifications@github.com wrote:

FYI, this is a bug of dReal, not IBEX. Let me revisit this after finishing up forall_t.

—
Reply to this email directly or view it on GitHub.

[soonhokong]

Solution:
theta : [-4, 4] = [3.14159, 3.14159]
thetad : [-10, 10] = [0, 0]
u : [-10, 10] = [-1.65661e-29, 1.59744e-29]
xd : [-10, 10] = [-0, 0]
sat

[soonhokong]

It kept haunting me so I spent a little more time on it to fix.

When we convert an Enode expression x^y to ibex function, we encoded x^y as pow(x,y). FYI, in IBEX, it is represented as exp(x*log(y)) and they don't really have a representation for x^y. f213d38 is to handle x^2 as sqr(x) instead of pow(x,y). This solves the problem somehow.

[scungao]

You mean exp(y*log(x)) right?
The solution is right - btw it's a stationary point of an inverted pendulum. :)

[soonhokong]

You mean exp(y*log(x)) right?

Yes.

[scungao]

Btw let Zenna know about the new version with this problem fixed.

On Jan 28, 2015, at 14:20, Soonho Kong notifications@github.com wrote:

You mean exp(y*log(x)) right?

Yes.

—
Reply to this email directly or view it on GitHub.

[soonhokong]

@zenna, could you check out the latest source code, recompile, and test this as @scungao suggested? If you still need a pre-compiled binary, please let me know. I'll get some sleep but will be back in 4 - 5 hours from now.

[zenna]

Thanks @soonhokong and @scungao, yes it builds. Sleep for more than four hours at a time!

However, the following are both (wrongly) unsat

(set-logic QF_NRA)
(declare-fun omega0 () Real)
(assert (>= omega0 0.3999996185302735))
(assert (<= omega0 0.39999985694885254))
(assert (not (> (+ (* (- 1 0) omega0) 0) 0.4)))
(check-sat)
(exit)

(set-logic QF_NRA)
(declare-fun omega0 () Real)
(assert (>= omega0 0.3999996185302735))
(assert (<= omega0 0.39999985694885254))
(assert (> (+ (* (- 1 0) omega0) 0) 0.4))
(check-sat)
(exit)

Also the following problem causes dReal to segfault

(set-logic QF_NRA)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(assert (>= x1 0))
(assert (<= x1 1))
(assert (not (= (- x1 x1) 0)))
(check-sat)
(exit)

[zenna]

And the old version answers this particular problem correctly.

[scungao]

The problem with rebuild? @soonhokong

@zenna Were you building from a fresh clone of the source or updating a previous one? In the latter case, rm -rf the build directory and build again. I had a similar problem when seeing some seg faults.

On Jan 30, 2015, at 16:57, Zenna Tavares notifications@github.com wrote:

Thanks @soonhokong and @scungao, yes it builds. Sleep for more than four hours at a time!

However, the following are both (wrongly) unsat

(set-logic QF_NRA)
(declare-fun omega0 () Real)
(assert (>= omega0 0.3999996185302735))
(assert (<= omega0 0.39999985694885254))
(assert (not (> (+ (* (- 1 0) omega0) 0) 0.4)))
(check-sat)
(exit)
(set-logic QF_NRA)
(declare-fun omega0 () Real)
(assert (>= omega0 0.3999996185302735))
(assert (<= omega0 0.39999985694885254))
(assert (> (+ (* (- 1 0) omega0) 0) 0.4))
(check-sat)
(exit)
Also the following problem causes dReal to segfault

(set-logic QF_NRA)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(assert (>= x1 0))
(assert (<= x1 1))
(assert (not (= (- x1 x1) 0)))
(check-sat)
(exit)
—
Reply to this email directly or view it on GitHub.

[zenna]

@scungao I did a build from scratch. Do you get the same result on this example?

[zenna]

@scungao I didn't do a fresh clone, but that shouldn't make a difference. I'll do it anyway. But from what I have seen it does look a lot faster.

[soonhokong]

@zenna, I can reproduce the two wrongly UNSATs and one segmentation fault problem. Let me open two separate issues for them.

[soonhokong]

#12 and #13