Incorrect result when not using --path in bouncing_ball_with_drag.drh

[danbryce]

mbp-db-2:bouncing_ball danbryce$ time dReach -k 2 bouncing_ball_with_drag.drh 
dReal Options:
SMT: bouncing_ball_with_drag_2_0.smt2, PATH : [1,2,1]
sat
sat -- [1,2,1]

real    0m0.908s
user    0m0.236s
sys 0m0.156s
mbp-db-2:bouncing_ball danbryce$ ../../../bin/bmc -k 2 bouncing_ball_with_drag.preprocessed.drh > bouncing_ball_with_drag.smt2
mbp-db-2:bouncing_ball danbryce$ time  ../../../bin/solver  bouncing_ball_with_drag.smt2 
unsat

real    0m26.670s
user    0m26.356s
sys 0m0.294s

I played with the SMT file (which encodes all paths) to see why it is unsat. The encoding includes a disjunction at each time step that allows choice between the jump source and destination. I found that removing disjuncts for time 0 and time 2, plus the invariant for time 1 "(forall_t 1.000000 [0.000000 time_1](= v_1_t 0.000000))" allows the SMT to be sat. I'm not sure why this is the case.

[danbryce]

I removed as much garbage as possible. This should be SAT but is UNSAT.

Remove (and (forall_t 1.000000 [0.000000 time_1] (<= v_1_t 0.000000))) to make it SAT. If we call this literal B, then the clause (or A B) is unsat, while the clause (A) is sat. Whether or not B is true, the clause (or A B) should be sat because A is sat.

(set-logic QF_NRA_ODE)
(declare-fun x () Real)
(declare-fun v () Real)
(declare-fun x_0_0 () Real)
(declare-fun x_0_t () Real)
(declare-fun x_1_0 () Real)
(declare-fun x_1_t () Real)
(declare-fun x_2_0 () Real)
(declare-fun x_2_t () Real)
(declare-fun v_0_0 () Real)
(declare-fun v_0_t () Real)
(declare-fun v_1_0 () Real)
(declare-fun v_1_t () Real)
(declare-fun v_2_0 () Real)
(declare-fun v_2_t () Real)
(declare-fun time_0 () Real)
(declare-fun time_1 () Real)
(declare-fun time_2 () Real)
(declare-fun mode_0 () Real)
(declare-fun mode_1 () Real)
(declare-fun mode_2 () Real)
(define-ode flow_1 ((= d/dt[x] v) (= d/dt[v] (+ (- 0.000000 9.800000) (* -0.450000 (^ v 1.000000))))))
(define-ode flow_2 ((= d/dt[x] v) (= d/dt[v] (+ (- 0.000000 9.800000) (* -0.450000 (^ v 1.000000))))))
(assert (<= 0.000000 x_0_0))
(assert (<= x_0_0 15.000000))
(assert (<= 0.000000 x_0_t))
(assert (<= x_0_t 15.000000))
(assert (<= 0.000000 x_1_0))
(assert (<= x_1_0 15.000000))
(assert (<= 0.000000 x_1_t))
(assert (<= x_1_t 15.000000))
(assert (<= 0.000000 x_2_0))
(assert (<= x_2_0 15.000000))
(assert (<= 0.000000 x_2_t))
(assert (<= x_2_t 15.000000))
(assert (<= -18.000000 v_0_0))
(assert (<= v_0_0 18.000000))
(assert (<= -18.000000 v_0_t))
(assert (<= v_0_t 18.000000))
(assert (<= -18.000000 v_1_0))
(assert (<= v_1_0 18.000000))
(assert (<= -18.000000 v_1_t))
(assert (<= v_1_t 18.000000))
(assert (<= -18.000000 v_2_0))
(assert (<= v_2_0 18.000000))
(assert (<= -18.000000 v_2_t))
(assert (<= v_2_t 18.000000))
(assert (<= 0.000000 time_0))
(assert (<= time_0 3.000000))
(assert (<= 0.000000 time_1))
(assert (<= time_1 3.000000))
(assert (<= 0.000000 time_2))
(assert (<= time_2 3.000000))
(assert (<= 1.000000 mode_0))
(assert (<= mode_0 2.000000))
(assert (<= 1.000000 mode_1))
(assert (<= mode_1 2.000000))
(assert (<= 1.000000 mode_2))
(assert (<= mode_2 2.000000))
(assert (and 

(or  
(and (= [x_2_t v_2_t] (integral 0. time_2 [x_2_0 v_2_0] flow_1)) (= mode_2 1.000000) (forall_t 1.000000 [0.000000 time_2] (<= v_2_t 0.000000)) (<= v_2_t 0.000000) (<= v_2_0 0.000000) (forall_t 1.000000 [0.000000 time_2] (>= x_2_t 0.000000)) (>= x_2_t 0.000000) (>= x_2_0 0.000000))
) 

(or 
(and (= [x_1_t v_1_t] (integral 0. time_1 [x_1_0 v_1_0] flow_2)) (= mode_1 2.000000) (forall_t 2.000000 [0.000000 time_1] (>= v_1_t 0.000000)) (>= v_1_t 0.000000) (>= v_1_0 0.000000) (forall_t 2.000000 [0.000000 time_1] (>= x_1_t 0.000000)) (>= x_1_t 0.000000) (>= x_1_0 0.000000) (= mode_2 1.000000) (= v_1_t 0.000000) (= v_2_0 v_1_t) (= x_2_0 x_1_t)) 
(and   (forall_t 1.000000 [0.000000 time_1] (<= v_1_t 0.000000)))
) 

(or  
(and (= [x_0_t v_0_t] (integral 0. time_0 [x_0_0 v_0_0] flow_1)) (= mode_0 1.000000) (forall_t 1.000000 [0.000000 time_0] (<= v_0_t 0.000000)) (<= v_0_t 0.000000) (<= v_0_0 0.000000) (forall_t 1.000000 [0.000000 time_0] (>= x_0_t 0.000000)) (>= x_0_t 0.000000) (>= x_0_0 0.000000) (= mode_1 2.000000) (= x_0_t 0.000000) (= v_1_0 (* -0.900000 v_0_t)) (= x_1_0 x_0_t))
) 

(and (= v_0_0 0.000000) (<= x_0_0 11.000000) (>= x_0_0 10.000000)) (= mode_0 1.000000) (= mode_2 1.000000) (>= v_2_t -18.000000) (>= x_2_t 0.350000)))
(check-sat)
(exit)

[danbryce]

Fixed in https://github.com/danbryce/dReal/commit/1e0b173dfd4bcc84b14b636f1fd0e09d1112dbc7

[soonhokong]

Thanks @danbryce!! But, is it really all that fix the problem? It's shocking to know that l->getPolarity().toInt() is not ``l->getPolarity().toInt() == 1 Anyway, I'll merge this to the repo, soon.

[danbryce]

I was surprised too. It was succeeding with value -1.

Dan

On Apr 23, 2014, at 4:14 PM, Soonho Kong notifications@github.com wrote:

Thanks @danbryce!! But, is it really all that fix the problem? It's shocking to know that l->getPolarity().toInt() is not ``l->getPolarity().toInt() == 1 Anyway, I'll merge this to the repo, soon.

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

[soonhokong]

I see. Any non-zero values are considered to be true in C/C++.

Thanks again for the fix!!

[soonhokong]

Merged 4c30145b0dfd07b98a385b1f215fe51121d66dfc.