Incorrect delta-sat witness

[shmarovfedor]

I think there was a similar issue before when you introduce a variable behaving as time. Here is the smt2 formula:

(set-logic QF_NRA_ODE)
(declare-fun b () Real)
(declare-fun b_0_0 () Real)
(declare-fun b_0_t () Real)
(assert (>= b_0_0  0))
(assert (>= b_0_t  0))
(assert (<= b_0_0  5e5))
(assert (<= b_0_t  5e5))
(declare-fun b_max () Real)
(declare-fun b_max_0_0 () Real)
(declare-fun b_max_0_t () Real)
(assert (>= b_max_0_0  0))
(assert (>= b_max_0_t  0))
(assert (<= b_max_0_0  5e5))
(assert (<= b_max_0_t  5e5))
(declare-fun p () Real)
(declare-fun p_0_0 () Real)
(declare-fun p_0_t () Real)
(assert (>= p_0_0 (- 1e6)))
(assert (>= p_0_t (- 1e6)))
(assert (<= p_0_0  4e6))
(assert (<= p_0_t  4e6))
(declare-fun s () Real)
(declare-fun s_0_0 () Real)
(declare-fun s_0_t () Real)
(assert (>= s_0_0  0))
(assert (>= s_0_t  0))
(assert (<= s_0_0  3e5))
(assert (<= s_0_t  3e5))
(declare-fun tau () Real)
(declare-fun tau_0_0 () Real)
(declare-fun tau_0_t () Real)
(assert (>= tau_0_0  0))
(assert (>= tau_0_t  0))
(assert (<= tau_0_0  3600))
(assert (<= tau_0_t  3600))
(declare-fun u_b () Real)
(declare-fun u_b_0_0 () Real)
(declare-fun u_b_0_t () Real)
(assert (>= u_b_0_0 (- 1.0)))
(assert (>= u_b_0_t (- 1.0)))
(assert (<= u_b_0_0  1.0))
(assert (<= u_b_0_t  1.0))
(declare-fun u_d () Real)
(declare-fun u_d_0_0 () Real)
(declare-fun u_d_0_t () Real)
(assert (>= u_d_0_0 (- 1.0)))
(assert (>= u_d_0_t (- 1.0)))
(assert (<= u_d_0_0  1.0))
(assert (<= u_d_0_t  1.0))
(declare-fun v () Real)
(declare-fun v_0_0 () Real)
(declare-fun v_0_t () Real)
(assert (>= v_0_0  0))
(assert (>= v_0_t  0))
(assert (<= v_0_0  2e5))
(assert (<= v_0_t  2e5))
(declare-fun time_0 () Real)
(assert (>= time_0  0))
(assert (<= time_0  3600))
(define-ode flow_1 ((= d/dt[b] (* 617 u_b))(= d/dt[b_max]  0)(= d/dt[p] (* 1.67e4 u_d))(= d/dt[s]  v)(= d/dt[tau]  1.0)(= d/dt[u_b]  0)(= d/dt[u_d]  0)(= d/dt[v] (*(/ 1 3.0e6)(-(-(/ p v)(+(+(+ 7.36e4(* 0 v))(* 101(^ v 2))) b))(* 9.81(sin 0)))))))
(assert (and 
(or ((and(= s_0_0 0)(= v_0_0 40)(= p_0_0 2e6)(= u_d_0_0(- 1))(= u_b_0_0 1)(= b_0_0 0)(= b_max_0_0 3.7e5)(= tau_0_0 0))))
(= [b_0_t b_max_0_t p_0_t s_0_t tau_0_t u_b_0_t u_d_0_t v_0_t ] (integral 0.0 time_0 [b_0_0 b_max_0_0 p_0_0 s_0_0 tau_0_0 u_b_0_0 u_d_0_0 v_0_0 ] flow_1))
(or ((and(= tau_0_t 60))))))
(check-sat)
(exit)

The result returned by dReal v3.16.12 (commit 5af96ed851a8):

delta-sat with the following box:
	b_0_0 : [0, 0];
	b_0_t : [0, 0.0009313225746154785];
	b_max_0_0 : [370000, 370000];
	b_max_0_t : [369999.9991804361, 370000.0001117587];
	p_0_0 : [2000000, 2000000];
	p_0_t : [-1000000, -999999.9994179234];
	s_0_0 : [0, 0];
	s_0_t : [0.0005587935447692871, 0.001117587089538574];
	tau_0_0 : [0, 0];
	tau_0_t : [60, 60];
	time_0 : [334.1148811626434, 334.1157394609451];
	u_b_0_0 : [1, 1];
	u_b_0_t : [0.9990234375, 1];
	u_d_0_0 : [-1, -1];
	u_d_0_t : [-1, -0.9990234375];
	v_0_0 : [40, 40];
	v_0_t : [0, 0.0007450580596923828]

I think that the result is correct but the witness is not as the differential equation for tau is d/dt[tau]=1.0.

[soonho-tri]

I'll check it soon.

[soonho-tri]

We know that tau_t == time_0 == 60.0 but apparently dReal doesn't see this relation in ODE solving.

Without this information, dReal tries to integrate until time = 3600 which will generate ODE exceptions. Over time, it branches on time (and on other dimensions as well). But all ODE pruning fails due to ODE exceptions. As a result, it ends up with a random box (whose size is smaller than delta) and reports it back to the user.

[soonho-tri]

Some observations:

1. I manually added a constraint (= time_0 tau_0_t) to the smt2 file and it gets me to the right solution. Inferring closed-form relational constraints between time variables and other variables should help.

2. I need to investigate why the branching on time_0 takes us to [334.1148811626434, 334.1157394609451] instead of a smaller one. I think we need to favor a smaller interval, at least for this special time variable for ODEs.