variables with underscores in ODEs

[shmarovfedor]

Apparently, dReal does not allow using variables with underscores in ODEs. Example of the model:

(set-logic QF_NRA_ODE)
(declare-fun y_y () Real)
(declare-fun y_y_0 () Real)
(declare-fun y_y_1 () Real)
(declare-fun k () Real)
(declare-fun k_0 () Real)
(declare-fun k_1 () Real)
(declare-fun t () Real)
(declare-fun t_0 () Real)
(declare-fun t_1 () Real)
(declare-fun time_0 () Real)
(define-ode flow_1 ((= d/dt[k] 0.0)(= d/dt[t] 1.0)(= d/dt[y_y] (* (/ 1 k) (cos (/ t k))))))
(assert (>= y_y_0 -2))
(assert (<= y_y_0 2))
(assert (>= y_y_1 -2))
(assert (<= y_y_1 2))
(assert (>= k_0 0))
(assert (<= k_0 4))
(assert (>= k_1 0))
(assert (<= k_1 4))
(assert (>= time_0 0))
(assert (<= time_0 1))
(assert (>= t_0 0))
(assert (<= t_0 1))
(assert (>= t_1 0))
(assert (<= t_1 1))
(assert 
(and 
(= [y_y_1 k_1 t_1] (integral 0. time_0 [y_y_0 k_0 t_0] flow_1))
(= k_0 k_1)
(= t_0 0)
(>= y_y_0 -1e-05)
(<= y_y_0 1e-05)
(= t_1 1)
(or
(< y_y_1 0.47)
(> y_y_1 0.49)
)
)
)
(check-sat)
(exit)

Error message:

y is not found in flow_map.
Segmentation fault (core dumped)

Is it possible to enable using variables with underscores? It is very important for us because in the biological models we use for parameter synthesis they appear quite frequently.

[soonhokong]

We have a variable convention for ODE variables. For instance, let's say that you have a system variable y_y in a flow, and you have a time variable time_0 in the integral constraint:

• Using the variable time_0 indicates that the integral constraint is in step 0.
• As a result, we expect you use the variable y_y_0_0 and y_y_0_t. Here, the convention is <system_variable_name>_<step>_<0|t>

I understand that the current convention can be seen artificial. I'll relax the condition in the next version.

For your original SMT2 formula, you can rename variables and get the following SMT2 formula:

(set-logic QF_NRA_ODE)
(declare-fun y_y () Real)
(declare-fun y_y_0_0 () Real)
(declare-fun y_y_0_t () Real)
(declare-fun k () Real)
(declare-fun k_0_0 () Real)
(declare-fun k_0_t () Real)
(declare-fun t () Real)
(declare-fun t_0_0 () Real)
(declare-fun t_0_t () Real)
(declare-fun time_0 () Real)
(define-ode flow_1
  ((= d/dt[k] 0.0)
   (= d/dt[t] 1.0)
   (= d/dt[y_y] (* (/ 1 k) (cos (/ t k))))))
(assert (>= y_y_0_0 -2))
(assert (<= y_y_0_0 2))
(assert (>= y_y_0_t -2))
(assert (<= y_y_0_t 2))
(assert (>= k_0_0 0))
(assert (<= k_0_0 4))
(assert (>= k_0_t 0))
(assert (<= k_0_t 4))
(assert (>= time_0 0))
(assert (<= time_0 1))
(assert (>= t_0_0 0))
(assert (<= t_0_0 1))
(assert (>= t_0_t 0))
(assert (<= t_0_t 1))
(assert
 (and
  (= [y_y_0_t k_0_t t_0_t] (integral 0. time_0 [y_y_0_0 k_0_0 t_0_0] flow_1))
  (= k_0_0 k_0_t)
  (= t_0_0 0)
  (>= y_y_0_0 -1e-05)
  (<= y_y_0_0 1e-05)
  (= t_0_t 1)
  (or
   (< y_y_0_t 0.47)
   (> y_y_0_t 0.49)
   )
  )
 )
(check-sat)
(exit)

Please try to run this example, and let me know if you have a problem.

[shmarovfedor]

Thanks, Soonho. It works!!! I will be following this encoding now