Incorrect smt2 encoding using "-e" flag for "-k=0"

[shmarovfedor]

This is an example where using -e with -k=0 I get incorrect smt2 encoding (but, with -d and -r it works fine). I suspect that the only problem is that the integral is missing in smt2.

The drh model:

#define a 0
#define b 20
[0.7854] alpha;
[9.8] g;
[0, 100] Sy;
[0, 1000] Sx;
[0, 15] t;
[0, 15] time;
[-100, 100] v0;

{ mode 1;

  flow:
        d/dt[Sx] = v0 * cos(alpha);
        d/dt[Sy] = v0 * sin(alpha) - g * t;
        d/dt[t] = 1.0;
        d/dt[v0] = 0.0;
  jump:
        (and (t >= 0.0001) (Sy = 0)) ==> @1 (and (Sx' = Sx) (Sy' = 0) (t' = 0) (v0' = 0.9 * v0));
}

init:
@1    (and (Sx = 0) (Sy = 0) (t = 0) (v0 <= b) (v0 >= a));

goal:
@1    (and (Sx >= 100.0) (Sy >= 0));

The smt2 file:

(set-logic QF_NRA_ODE)
(declare-fun v0 () Real)
(declare-fun t () Real)
(declare-fun Sy () Real)
(declare-fun Sx () Real)
(declare-fun v0_0_0 () Real)
(declare-fun v0_0_t () Real)
(declare-fun t_0_0 () Real)
(declare-fun t_0_t () Real)
(declare-fun Sy_0_0 () Real)
(declare-fun Sy_0_t () Real)
(declare-fun Sx_0_0 () Real)
(declare-fun Sx_0_t () Real)
(declare-fun time_0 () Real)
(declare-fun mode_0 () Real)
(define-ode flow_0_1 ((= d/dt[Sx] (* v0 (cos 0.7854))) (= d/dt[Sy] (- (* v0 (sin 0.7854)) (* 9.8 t))) (= d/dt[t] 1) (= d/dt[v0] 0)))
(assert (<= -100 v0_0_0))
(assert (<= v0_0_0 100))
(assert (<= -100 v0_0_t))
(assert (<= v0_0_t 100))
(assert (<= 0 t_0_0))
(assert (<= t_0_0 15))
(assert (<= 0 t_0_t))
(assert (<= t_0_t 15))
(assert (<= 0 Sy_0_0))
(assert (<= Sy_0_0 100))
(assert (<= 0 Sy_0_t))
(assert (<= Sy_0_t 100))
(assert (<= 0 Sx_0_0))
(assert (<= Sx_0_0 1000))
(assert (<= 0 Sx_0_t))
(assert (<= Sx_0_t 1000))
(assert (<= 0 time_0))
(assert (<= time_0 15))
(assert (<= 1 mode_0))
(assert (<= mode_0 1))
(assert (and (= mode_0 1) (and (>= v0_0_0 0) (<= v0_0_0 20) (= t_0_0 0) (= Sy_0_0 0) (= Sx_0_0 0)) (= mode_0 1) (= mode_0 1) (>= Sy_0_t 0) (>= Sx_0_t 100)))
(check-sat)
(exit)

[danbryce]

Fixed in pull request 52.

On Jun 25, 2014, at 7:20 AM, shmarovfedor notifications@github.com wrote:

This is an example where using -e with -k=0 I get incorrect smt2 encoding (but, with -d and -r it works fine). I suspect that the only problem is that the integral is missing in smt2.

The drh model:

define a 0

define b 20

[0.7854] alpha; [9.8] g; [0, 100] Sy; [0, 1000] Sx; [0, 15] t; [0, 15] time; [-100, 100] v0;

{ mode 1;

flow: d/dt[Sx] = v0 * cos(alpha); d/dt[Sy] = v0 * sin(alpha) - g * t; d/dt[t] = 1.0; d/dt[v0] = 0.0; jump: (and (t >= 0.0001) (Sy = 0)) ==> @1 (and (Sx' = Sx) (Sy' = 0) (t' = 0) (v0' = 0.9 * v0)); }

init: @1 (and (Sx = 0) (Sy = 0) (t = 0) (v0 <= b) (v0 >= a));

goal: @1 (and (Sx >= 100.0) (Sy >= 0));

The smt2 file:

(set-logic QF_NRA_ODE) (declare-fun v0 () Real) (declare-fun t () Real) (declare-fun Sy () Real) (declare-fun Sx () Real) (declare-fun v0_0_0 () Real) (declare-fun v0_0_t () Real) (declare-fun t_0_0 () Real) (declare-fun t_0_t () Real) (declare-fun Sy_0_0 () Real) (declare-fun Sy_0_t () Real) (declare-fun Sx_0_0 () Real) (declare-fun Sx_0_t () Real) (declare-fun time_0 () Real) (declare-fun mode_0 () Real) (define-ode flow_0_1 ((= d/dt[Sx]( v0 %28cos 0.7854%29)) (= d/dt[Sy](- %28 v0 %28sin 0.7854%29%29 %28* 9.8 t%29)) (= d/dt[t] 1) (= d/dt[v0] 0))) (assert (<= -100 v0_0_0)) (assert (<= v0_0_0 100)) (assert (<= -100 v0_0_t)) (assert (<= v0_0_t 100)) (assert (<= 0 t_0_0)) (assert (<= t_0_0 15)) (assert (<= 0 t_0_t)) (assert (<= t_0_t 15)) (assert (<= 0 Sy_0_0)) (assert (<= Sy_0_0 100)) (assert (<= 0 Sy_0_t)) (assert (<= Sy_0_t 100)) (assert (<= 0 Sx_0_0)) (assert (<= Sx_0_0 1000)) (assert (<= 0 Sx_0_t)) (assert (<= Sx_0_t 1000)) (assert (<= 0 time_0)) (assert (<= time_0 15)) (assert (<= 1 mode_0)) (assert (<= mode_0 1)) (assert (and (= mode_0 1) (and (>= v0_0_0 0) (<= v0_0_0 20) (= t_0_0 0) (= Sy_0_0 0) (= Sx_0_0 0)) (= mode_0 1) (= mode_0 1) (>= Sy_0_t 0) (>= Sx_0_t 100))) (check-sat) (exit)

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