dreal/dreal3

Inconsistent behavior while using negation in forall_t

Opened this issue · 5 comments

Nikh13 commented

Hi,

I am currently formalizing a simple system with ODEs in SMT2 and using dReal to solve it. I wanted to apply the invariant not (x<3 & y>1) to a particular mode using the forall_t logic.

Case 1: The invariant is satisfied
(assert (forall_t 1 [0 duration_0_] (not (and (> y_0_t 1)(< x_0_t 3)))))

Case2: The invariant is unsatisfiable
(assert (forall_t 1 [0 duration_0_] (not (and (< x_0_t 3)(> y_0_t 1)))))

As you can see both statements are exactly the same except that I have changed the order of the conjunctive terms, but give different results. In a couple of other cases as well, using negation with the forall_t statement seemed to be giving inconsistent as well as unexpected results. Just needed to know if I am missing something or if there is a fix for this.

Thanks.

scungao commented

Thanks @Nikh13 for the report. This is pretty weird. We'll look into it soon.

soonho-tri commented

Hi @Nikh13 , could you send me the full smt2 file so that I can reproduce it locally?

Nikh13 commented

Hi Soonho,

I have attached the file and commented the rules that are producing this behaviour. Please do let me know if you need anything else.

Thanks,
Nikhil

car-turning-HA-2step.smt2.zip

soonho-tri commented

@Nikh13 , thank you. I've found two problems in the file:

  1. We have a special convention for the time variables. They should be of the form <alpha_numeric_name>_<int>, and the current time variables duration_0_ doesn't fit in this pattern. There is actually an exception thrown but for now it occurs only in debug mode. I'll change it to be more explicit.
  2. Our ODE solver doesn't support tan function. In dReach, we convert any tan(expr) into sin(expr) / cos(expr). Since you're formulating smt2 file directly, you need to do this step manually for now.
Nikh13 commented

Hi @soonho-tri,

Thank you for the prompt response.

I fixed the file based on the problems you found with it but I still seem to be getting the same behavior. I have attached the updated file.

car-turning-HA-2step.smt2.zip

I also wanted to verify the exact working of the forall_t rule.

  • The forall_t rule is applied only when the integral construct for the same mode is also triggered.

  • The initial values used in the forall_t rule are obtained from the initial values from the integral construct for the same mode.

Is this correct?