search

dreal / dreal2

Please check dreal4 instead.
https://github.com/dreal/dreal4
GNU General Public License v3.0
13 stars 15 forks source link

dReach "-e" flag #50

Closed shmarovfedor closed 10 years ago

shmarovfedor commented 10 years ago

The following model is SAT with -k 5:

#define a 20
#define b 30
[0, 130] x;
#define K 1.0
[0, 5] time;
[0, 1000] tau;

{ mode 1;
  invt:
        (x >= 18);
  flow:
        d/dt[x] = - x * K;
        d/dt[tau] = 10.0;
  jump:
        (x <= 18) ==> @2 (and (x' = x) (tau' = tau));
}
{ mode 2;
  invt:
        (x <= 22);
  flow:
        d/dt[x] = - K * (x - 30);
        d/dt[tau] = 10.0;
  jump:
        (x >= 22) ==> @1 (and (x' = x) (tau' = tau));
}
init:
@1      (and (x >= a) (x <= b) (tau = 0));

goal:
@2      (and (x >= 19.9) (x <= 20.1) (tau = 18));

But the model is UNSAT if I run it with -k 5 and -e flag

danbryce commented 10 years ago

Can you tell me the result with the alternative flags: “-r” or “-b” or “-d"?

On Jun 20, 2014, at 9:12 AM, shmarovfedor notifications@github.com wrote:

The following model is SAT with -k 5:

define a 20

define b 30

[0, 130] x;

define K 1.0

[0, 5] time; [0, 1000] tau;

{ mode 1; invt: (x >= 18); flow: d/dt[x] = - x * K; d/dt[tau] = 10.0; jump: (x <= 18) ==> @2 (and (x' = x) (tau' = tau)); } { mode 2; invt: (x <= 22); flow: d/dt[x] = - K * (x - 30); d/dt[tau] = 10.0; jump: (x >= 22) ==> @1 (and (x' = x) (tau' = tau)); } init: @1 (and (x >= a) (x <= b) (tau = 0));

goal: @2 (and (x >= 19.9) (x <= 20.1) (tau = 18));

But the model is UNSAT if I run it with -k 5 and -e flag

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

shmarovfedor commented 10 years ago

It is unsat for any of the flags

danbryce commented 10 years ago

That suggests there is a problem with the “all paths” encoding. Can you post the SMT2 file generated using the -d option?

On Jun 20, 2014, at 9:19 AM, shmarovfedor notifications@github.com wrote:

It is unsat for any of the flags

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

shmarovfedor commented 10 years ago 
(set-logic QF_NRA_ODE)
(declare-fun x () Real)
(declare-fun tau () 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 x_3_0 () Real)
(declare-fun x_3_t () Real)
(declare-fun x_4_0 () Real)
(declare-fun x_4_t () Real)
(declare-fun x_5_0 () Real)
(declare-fun x_5_t () Real)
(declare-fun tau_0_0 () Real)
(declare-fun tau_0_t () Real)
(declare-fun tau_1_0 () Real)
(declare-fun tau_1_t () Real)
(declare-fun tau_2_0 () Real)
(declare-fun tau_2_t () Real)
(declare-fun tau_3_0 () Real)
(declare-fun tau_3_t () Real)
(declare-fun tau_4_0 () Real)
(declare-fun tau_4_t () Real)
(declare-fun tau_5_0 () Real)
(declare-fun tau_5_t () Real)
(declare-fun time_0 () Real)
(declare-fun time_1 () Real)
(declare-fun time_2 () Real)
(declare-fun time_3 () Real)
(declare-fun time_4 () Real)
(declare-fun time_5 () Real)
(declare-fun mode_0 () Real)
(declare-fun mode_1 () Real)
(declare-fun mode_2 () Real)
(declare-fun mode_3 () Real)
(declare-fun mode_4 () Real)
(declare-fun mode_5 () Real)
(define-ode flow_1 ((= d/dt[x] (* (- 0 x) 1)) (= d/dt[tau] 10)))
(define-ode flow_2 ((= d/dt[x] (* -1 (- x 30))) (= d/dt[tau] 10)))
(assert (<= 0 x_0_0))
(assert (<= x_0_0 130))
(assert (<= 0 x_0_t))
(assert (<= x_0_t 130))
(assert (<= 0 x_1_0))
(assert (<= x_1_0 130))
(assert (<= 0 x_1_t))
(assert (<= x_1_t 130))
(assert (<= 0 x_2_0))
(assert (<= x_2_0 130))
(assert (<= 0 x_2_t))
(assert (<= x_2_t 130))
(assert (<= 0 x_3_0))
(assert (<= x_3_0 130))
(assert (<= 0 x_3_t))
(assert (<= x_3_t 130))
(assert (<= 0 x_4_0))
(assert (<= x_4_t 130))
(assert (<= 0 x_5_0))
(assert (<= x_5_0 130))
(assert (<= 0 x_5_t))
(assert (<= x_5_t 130))
(assert (<= 0 tau_0_0))
(assert (<= tau_0_0 1000))
(assert (<= 0 tau_0_t))
(assert (<= tau_0_t 1000))
(assert (<= 0 tau_1_0))
(assert (<= tau_1_0 1000))
(assert (<= 0 tau_1_t))
(assert (<= tau_1_t 1000))
(assert (<= 0 tau_2_0))
(assert (<= tau_2_0 1000))
(assert (<= 0 tau_2_t))
(assert (<= tau_2_t 1000))
(assert (<= 0 tau_3_0))
(assert (<= tau_3_0 1000))
(assert (<= 0 tau_3_t))
(assert (<= tau_3_t 1000))
(assert (<= 0 tau_4_0))
(assert (<= tau_4_0 1000))
(assert (<= 0 tau_4_t))
(assert (<= tau_4_t 1000))
(assert (<= 0 tau_5_0))
(assert (<= tau_5_0 1000))
(assert (<= 0 tau_5_t))
(assert (<= tau_5_t 1000))
(assert (<= 0 time_0))
(assert (<= time_0 5))
(assert (<= 0 time_1))
(assert (<= time_1 5))
(assert (<= 0 time_2))
(assert (<= time_2 5))
(assert (<= 0 time_3))
(assert (<= time_3 5))
(assert (<= 0 time_4))
(assert (<= time_4 5))
(assert (<= 0 time_5))
(assert (<= time_5 5))
(assert (<= 1 mode_0))
(assert (<= mode_0 2))
(assert (<= 1 mode_1))
(assert (<= mode_1 2))
(assert (<= 1 mode_2))
(assert (<= mode_2 2))
(assert (<= 1 mode_3))
(assert (<= mode_3 2))
(assert (<= 1 mode_4))
(assert (<= mode_4 2))
(assert (<= 1 mode_5))
(assert (<= mode_5 2))
(assert (and (or (and (= [x_5_t tau_5_t] (integral 0. time_5 [x_5_0 tau_5_0] flow_2)) (= mode_5 2) (forall_t 2 [0 time_5] (<= x_5_t 22)) (<= x_5_t 22) (<= x_5_0 22)) (and (= [x_5_t tau_5_t] (integral 0. time_5 [x_5_0 tau_5_0] flow_1)) (= mode_5 1) (forall_t 1 [0 time_5] (>= x_5_t 18)) (>= x_5_t 18) (>= x_5_0 18))) (or (and (= [x_4_t tau_4_t] (integral 0. time_4 [x_4_0 tau_4_0] flow_2)) (= mode_4 2) (forall_t 2 [0 time_4] (<= x_4_t 22)) (<= x_4_t 22) (<= x_4_0 22) (= mode_5 1) (>= x_4_t 22) (= tau_5_0 tau_4_t) (= x_5_0 x_4_t)) (and (= [x_4_t tau_4_t] (integral 0. time_4 [x_4_0 tau_4_0] flow_1)) (= mode_4 1) (forall_t 1 [0 time_4] (>= x_4_t 18)) (>= x_4_t 18) (>= x_4_0 18) (= mode_5 2) (<= x_4_t 18) (= tau_5_0 tau_4_t) (= x_5_0 x_4_t))) (or (and (= [x_3_t tau_3_t] (integral 0. time_3 [x_3_0 tau_3_0] flow_2)) (= mode_3 2) (forall_t 2 [0 time_3] (<= x_3_t 22)) (<= x_3_t 22) (<= x_3_0 22) (= mode_4 1) (>= x_3_t 22) (= tau_4_0 tau_3_t) (= x_4_0 x_3_t)) (and (= [x_3_t tau_3_t] (integral 0. time_3 [x_3_0 tau_3_0] flow_1)) (= mode_3 1) (forall_t 1 [0 time_3] (>= x_3_t 18)) (>= x_3_t 18) (>= x_3_0 18) (= mode_4 2) (<= x_3_t 18) (= tau_4_0 tau_3_t) (= x_4_0 x_3_t))) (or (and (= [x_2_t tau_2_t] (integral 0. time_2 [x_2_0 tau_2_0] flow_2)) (= mode_2 2) (forall_t 2 [0 time_2] (<= x_2_t 22)) (<= x_2_t 22) (<= x_2_0 22) (= mode_3 1) (>= x_2_t 22) (= tau_3_0 tau_2_t) (= x_3_0 x_2_t)) (and (= [x_2_t tau_2_t] (integral 0. time_2 [x_2_0 tau_2_0] flow_1)) (= mode_2 1) (forall_t 1 [0 time_2] (>= x_2_t 18)) (>= x_2_t 18) (>= x_2_0 18) (= mode_3 2) (<= x_2_t 18) (= tau_3_0 tau_2_t) (= x_3_0 x_2_t))) (or (and (= [x_1_t tau_1_t] (integral 0. time_1 [x_1_0 tau_1_0] flow_2)) (= mode_1 2) (forall_t 2 [0 time_1] (<= x_1_t 22)) (<= x_1_t 22) (<= x_1_0 22) (= mode_2 1) (>= x_1_t 22) (= tau_2_0 tau_1_t) (= x_2_0 x_1_t)) (and (= [x_1_t tau_1_t] (integral 0. time_1 [x_1_0 tau_1_0] flow_1)) (= mode_1 1) (forall_t 1 [0 time_1] (>= x_1_t 18)) (>= x_1_t 18) (>= x_1_0 18) (= mode_2 2) (<= x_1_t 18) (= tau_2_0 tau_1_t) (= x_2_0 x_1_t))) (or (and (= [x_0_t tau_0_t] (integral 0. time_0 [x_0_0 tau_0_0] flow_2)) (= mode_0 2) (forall_t 2 [0 time_0] (<= x_0_t 22)) (<= x_0_t 22) (<= x_0_0 22) (= mode_1 1) (>= x_0_t 22) (= tau_1_0 tau_0_t) (= x_1_0 x_0_t)) (and (= [x_0_t tau_0_t] (integral 0. time_0 [x_0_0 tau_0_0] flow_1)) (= mode_0 1) (forall_t 1 [0 time_0] (>= x_0_t 18)) (>= x_0_t 18) (>= x_0_0 18) (= mode_1 2) (<= x_0_t 18) (= tau_1_0 tau_0_t) (= x_1_0 x_0_t))) (and (= tau_0_0 0) (<= x_0_0 30) (>= x_0_0 20)) (= mode_0 1) (= mode_5 2) (= tau_5_t 18) (<= x_5_t 20.1) (>= x_5_t 19.9)))
(check-sat)
(exit)
danbryce commented 10 years ago

I created a simpler version of this problem (k = 2) with the drh:

define a 20

define b 30

[0, 130] x;

define K 1.0

[0, 5] time; [0, 1000] tau;

{ mode 1; invt: (x >= 18); flow: d/dt[x] = - x * K; d/dt[tau] = 10.0; jump: (x <= 18) ==> @2 (and (x' = x) (tau' = tau)); } { mode 2; invt: (x <= 22); flow: d/dt[x] = - K * (x - 30); d/dt[tau] = 10.0; jump: (x >= 22) ==> @1 (and (x' = x) (tau' = tau)); } init: @1 (and (x >= a) (x <= b) (tau = 0));

goal: @1 (and (x = 22) );

With the -d flag, I get an unsat result because (I think) the explanation generated by the ICP solver is incorrect. The search gets to a point where it asserts:

x_0_t <= 18 x_0_t >= 18 x_0_t >= 22

This is going to be unsat, and it is properly detected as such. However the explanation drops the "x_0_t >= 22” literal, which is the cause of the conflict. Among other literals it says:

x_0_t <= 18 x_0_t >= 18

are the literals to blame. Unfortunately, these are required by the SAT solution. Soonho?

The SMT2 is:

(set-logic QF_NRA_ODE) (declare-fun x () Real) (declare-fun tau () 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 tau_0_0 () Real) (declare-fun tau_0_t () Real) (declare-fun tau_1_0 () Real) (declare-fun tau_1_t () Real) (declare-fun tau_2_0 () Real) (declare-fun tau_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]( %28- 0 x%29 1)) (= d/dt[tau] 10))) (define-ode flow_2 ((= d/dt[x]( -1 %28- x 30%29)) (= d/dt[tau] 10))) (assert (<= 0 x_0_0)) (assert (<= x_0_0 130)) (assert (<= 0 x_0_t)) (assert (<= x_0_t 130)) (assert (<= 0 x_1_0)) (assert (<= x_1_0 130)) (assert (<= 0 x_1_t)) (assert (<= x_1_t 130)) (assert (<= 0 x_2_0)) (assert (<= x_2_0 130)) (assert (<= 0 x_2_t)) (assert (<= x_2_t 130)) (assert (<= 0 tau_0_0)) (assert (<= tau_0_0 1000)) (assert (<= 0 tau_0_t)) (assert (<= tau_0_t 1000)) (assert (<= 0 tau_1_0)) (assert (<= tau_1_0 1000)) (assert (<= 0 tau_1_t)) (assert (<= tau_1_t 1000)) (assert (<= 0 tau_2_0)) (assert (<= tau_2_0 1000)) (assert (<= 0 tau_2_t)) (assert (<= tau_2_t 1000)) (assert (<= 0 time_0)) (assert (<= time_0 5)) (assert (<= 0 time_1)) (assert (<= time_1 5)) (assert (<= 0 time_2)) (assert (<= time_2 5)) (assert (<= 1 mode_0)) (assert (<= mode_0 2)) (assert (<= 1 mode_1)) (assert (<= mode_1 2)) (assert (<= 1 mode_2)) (assert (<= mode_2 2)) (assert

(and (or (and (= [x_2_t tau_2_t](integral 0. time_2 [x_2_0 tau_2_0] flow_2)) (forall_t 2 [0 time_2](= x_2_t 22)) (<= x_2_t 22) (<= x_2_0 22)) (and (= [x_2_t tau_2_t](integral 0. time_2 [x_2_0 tau_2_0] flow_1)) (= mode_2 1) (forall_t 1 [0 time_2](>= x_2_t 18)) (>= x_2_t 18) (>= x_2_0 18)))

(or (and (= [x_1_t tau_1_t](integral 0. time_1 [x_1_0 tau_1_0] flow_2)) (= mode_1 2) (forall_t 2 [0 time_1](= x_1_t 22)) (<= x_1_t 22) (<= x_1_0 22) (= mode_2 1) (>= x_1_t 22) (= tau_2_0 tau_1_t) (= x_2_0 x_1_t)) (and (= [x_1_t tau_1_t](integral 0. time_1 [x_1_0 tau_1_0] flow_1)) (forall_t 1 [0 time_1](>= x_1_t 18)) (>= x_1_t 18) (>= x_1_0 18) (<= x_1_t 18) (= tau_2_0 tau_1_t) (= x_2_0 x_1_t)))

(or (and (= [x_0_t tau_0_t](integral 0. time_0 [x_0_0 tau_0_0] flow_2)) (forall_t 2 [0 time_0](= x_0_t 22)) (<= x_0_t 22) (<= x_0_0 22) (>= x_0_t 22) (= tau_1_0 tau_0_t) (= x_1_0 x_0_t)) (and (= [x_0_t tau_0_t](integral 0. time_0 [x_0_0 tau_0_0] flow_1)) (= mode_0 1) (forall_t 1 [0 time_0](>= x_0_t 18)) (>= x_0_t 18) (>= x_0_0 18) (= mode_1 2) (<= x_0_t 18) (= tau_1_0 tau_0_t) (= x_1_0 x_0_t)))

(and (= tau_0_0 0) (<= x_0_0 30) (>= x_0_0 20)) (= mode_0 1) (= mode_2 1) (= x_2_t 22))) (check-sat) (exit)

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

(set-logic QF_NRA_ODE) (declare-fun x () Real) (declare-fun tau () 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 x_3_0 () Real) (declare-fun x_3_t () Real) (declare-fun x_4_0 () Real) (declare-fun x_4_t () Real) (declare-fun x_5_0 () Real) (declare-fun x_5_t () Real) (declare-fun tau_0_0 () Real) (declare-fun tau_0_t () Real) (declare-fun tau_1_0 () Real) (declare-fun tau_1_t () Real) (declare-fun tau_2_0 () Real) (declare-fun tau_2_t () Real) (declare-fun tau_3_0 () Real) (declare-fun tau_3_t () Real) (declare-fun tau_4_0 () Real) (declare-fun tau_4_t () Real) (declare-fun tau_5_0 () Real) (declare-fun tau_5_t () Real) (declare-fun time_0 () Real) (declare-fun time_1 () Real) (declare-fun time_2 () Real) (declare-fun time_3 () Real) (declare-fun time_4 () Real) (declare-fun time_5 () Real) (declare-fun mode_0 () Real) (declare-fun mode_1 () Real) (declare-fun mode_2 () Real) (declare-fun mode_3 () Real) (declare-fun mode_4 () Real) (declare-fun mode_5 () Real) (define-ode flow_1 ((= d/dt[x]( %28- 0 x%29 1)) (= d/dt[tau] 10))) (define-ode flow_2 ((= d/dt[x]( -1 %28- x 30%29)) (= d/dt[tau] 10))) (assert (<= 0 x_0_0)) (assert (<= x_0_0 130)) (assert (<= 0 x_0_t)) (assert (<= x_0_t 130)) (assert (<= 0 x_1_0)) (assert (<= x_1_0 130)) (assert (<= 0 x_1_t)) (assert (<= x_1_t 130)) (assert (<= 0 x_2_0)) (assert (<= x_2_0 130)) (assert (<= 0 x_2_t)) (assert (<= x_2_t 130)) (assert (<= 0 x_3_0)) (assert (<= x_3_0 130)) (assert (<= 0 x_3_t)) (assert (<= x_3_t 130)) (assert (<= 0 x_4_0)) (assert (<= x_4_t 130)) (assert (<= 0 x_5_0)) (assert (<= x_5_0 130)) (assert (<= 0 x_5_t)) (assert (<= x_5_t 130)) (assert (<= 0 tau_0_0)) (assert (<= tau_0_0 1000)) (assert (<= 0 tau_0_t)) (assert (<= tau_0_t 1000)) (assert (<= 0 tau_1_0)) (assert (<= tau_1_0 1000)) (assert (<= 0 tau_1_t)) (assert (<= tau_1_t 1000)) (assert (<= 0 tau_2_0)) (assert (<= tau_2_0 1000)) (assert (<= 0 tau_2_t)) (assert (<= tau_2_t 1000)) (assert (<= 0 tau_3_0)) (assert (<= tau_3_0 1000)) (assert (<= 0 tau_3_t)) (assert (<= tau_3_t 1000)) (assert (<= 0 tau_4_0)) (assert (<= tau_4_0 1000)) (assert (<= 0 tau_4_t)) (assert (<= tau_4_t 1000)) (assert (<= 0 tau_5_0)) (assert (<= tau_5_0 1000)) (assert (<= 0 tau_5_t)) (assert (<= tau_5_t 1000)) (assert (<= 0 time_0)) (assert (<= time_0 5)) (assert (<= 0 time_1)) (assert (<= time_1 5)) (assert (<= 0 time_2)) (assert (<= time_2 5)) (assert (<= 0 time_3)) (assert (<= time_3 5)) (assert (<= 0 time_4)) (assert (<= time_4 5)) (assert (<= 0 time_5)) (assert (<= time_5 5)) (assert (<= 1 mode_0)) (assert (<= mode_0 2)) (assert (<= 1 mode_1)) (assert (<= mode_1 2)) (assert (<= 1 mode_2)) (assert (<= mode_2 2)) (assert (<= 1 mode_3)) (assert (<= mode_3 2)) (assert (<= 1 mode_4)) (assert (<= mode_4 2)) (assert (<= 1 mode_5)) (assert (<= mode_5 2)) (assert (and (or (and (= [x_5_t tau_5_t](integral 0. time_5 [x_5_0 tau_5_0] flow_2)) (= mode_5 2) (forall_t 2 [0 time_5](= x_5_t 22)) (<= x_5_t 22) (<= x_5_0 22)) (and (= [x_5_t tau_5_t](integral 0. time_5 [x_5_0 tau_5_0] flow_1)) (= mode_5 1) (forall_t 1 [0 time_5](>= x_5_t 18)) (>= x_5_t 18) (>= x_5_0 18))) (or (and (= [x_4_t tau_4_t](integral 0. time_4 [x_4_0 tau_4_0] flow_2)) (= mode_4 2) (forall_t 2 [0 time_4](= x_4_t 22)) (<= x_4_t 22) (<= x_4_0 22) (= mode_5 1) (>= x_4_t 22) (= tau_5_0 tau_4_t) (= x_5_0 x_4_t)) (and (= [x_4_t tau_4_t](integral 0. time_4 [x_4_0 tau_4_0] flow_1)) (= mode_4 1) (forall_t 1 [0 time_4](>= x_4_t 18)) (>= x_4_t 18) (>= x_4_0 18) (= mode_5 2) (<= x_4_t 18) (= tau_5_0 tau_4_t) (= x_5_0 x_4_t))) (or (and (= [x_3_t tau_3_t](integral 0. time_3 [x_3_0 tau_3_0] flow_2)) (= mode_3 2) (forall_t 2 [0 time_3](= x_3_t 22)) (<= x_3_t 22) (<= x_3_0 22) (= mode_4 1) (>= x_3_t 22) (= tau_4_0 tau_3_t) (= x_4_0 x_3_t)) (and (= [x_3_t tau_3_t](integral 0. time_3 [x_3_0 tau_3_0] flow_1)) (= mode_3 1) (forall_t 1 [0 time_3](>= x_3_t 18)) (>= x_3_t 18) (>= x_3_0 18) (= mode_4 2) (<= x_3_t 18) (= tau_4_0 tau_3_t) (= x_4_0 x_3_t))) (or (and (= [x_2_t tau_2_t](integral 0. time_2 [x_2_0 tau_2_0] flow_2)) (= mode_2 2) (forall_t 2 [0 time_2](= x_2_t 22)) (<= x_2_t 22) (<= x_2_0 22) (= mode_3 1) (>= x_2_t 22) (= tau_3_0 tau_2_t) (= x_3_0 x_2_t)) (and (= [x_2_t tau_2_t](integral 0. time_2 [x_2_0 tau_2_0] flow_1)) (= mode_2 1) (forall_t 1 [0 time_2](>= x_2_t 18)) (>= x_2_t 18) (>= x_2_0 18) (= mode_3 2) (<= x_2_t 18) (= tau_3_0 tau_2_t) (= x_3_0 x_2_t))) (or (and (= [x_1_t tau_1_t](integral 0. time_1 [x_1_0 tau_1_0] flow_2)) (= mode_1 2) (forall_t 2 [0 time_1](= x_1_t 22)) (<= x_1_t 22) (<= x_1_0 22) (= mode_2 1) (>= x_1_t 22) (= tau_2_0 tau_1_t) (= x_2_0 x_1_t)) (and (= [x_1_t tau_1_t](integral 0. time_1 [x_1_0 tau_1_0] flow_1)) (= mo de_1 1) (forall_t 1 [0 time_1](>= x_1_t 18)) (>= x_1_t 18) (>= x_1_0 18) (= mode_2 2) (<= x_1_t 18) (= tau_2_0 tau_1_t) (= x_2_0 x_1_t))) (or (and (= [x_0_t tau_0_t](integral 0. time_0 [x_0_0 tau_0_0] flow_2)) (= mode_0 2) (forall_t 2 [0 time_0](= x_0_t 22)) (<= x_0_t 22) (<= x_0_0 22) (= mode_1 1) (>= x_0_t 22) (= tau_1_0 tau_0_t) (= x_1_0 x_0_t)) (and (= [x_0_t tau_0_t](integral 0. time_0 [x_0_0 tau_0_0] flow_1)) (= mode_0 1) (forall_t 1 [0 time_0](>= x_0_t 18)) (>= x_0_t 18) (>= x_0_0 18) (= mode_1 2) (<= x_0_t 18) (= tau_1_0 tau_0_t) (= x_1_0 x_0_t))) (and (= tau_0_0 0) (<= x_0_0 30) (>= x_0_0 20)) (= mode_0 1) (= mode_5 2) (= tau_5_t 18) (<= x_5_t 20.1) (>= x_5_t 19.9))) (check-sat) (exit)

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

soonhokong commented 10 years ago

I think the ICP detects a conflict from x_0_0 variable, not from x_0_t variable in this case. It assigns [20, 30] to x_0_0, and then check constraints. When it meets (<= 18 x_0_0) which is unfeasible with the value [20, 30], ICP solver generates an explanation.

danbryce commented 10 years ago

If you look at the attached .output file, you’ll see that the theory literals are consistent up until the point we add the (x >= 22) literal. The explanation does not include this literal.

Thanks, Dan

On Jun 20, 2014, at 2:51 PM, Soonho Kong notifications@github.com wrote:

I think the ICP detects a conflict from x_0_0 variable, not from x_0_t variable in this case. It assigns [20, 30] to x_0_0, and then check constraints. When it meets (<= 18 x_0_0) which is unfeasible with the value [20, 30], ICP solver generates an explanation.

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

soonhokong commented 10 years ago

@danbryce, thanks. I found a horrible bug that I've been hunting for a week. I'm fixing it now.

soonhokong commented 10 years ago

Now both of @shmarovfedor and @danbryce 's examples are SAT with -d, -e, and -r options.

danbryce commented 10 years ago

Thanks!

Dan

On Jun 24, 2014, at 2:55 PM, Soonho Kong notifications@github.com wrote:

Now both of @shmarovfedor and @danbryce 's examples are SAT with -d, -e, and -r options.

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