sine model for benchmarks

[shmarovfedor]

This is the model which was very slow in the previous version of dReal. Now it is significantly faster but there are a lot of division by 0 exceptions

(set-logic QF_NRA_ODE)
(declare-fun y () Real)
(declare-fun y_0 () Real)
(declare-fun 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] (* (/ 1 k) (cos (/ t k))))))
(assert (>= y_0 -2))
(assert (<= y_0 2))
(assert (>= y_1 -2))
(assert (<= 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_1 k_1 t_1] (integral 0. time_0 [y_0 k_0 t_0] flow_1))
(= k_0 k_1)
(= t_0 0)
(>= y_0 -1e-05)
(<= y_0 1e-05)
(= t_1 1)
(or
(< y_1 0.47)
(> y_1 0.49)
)
)
)
(check-sat)
(exit)

[soonhokong]

It's because the domain of k includes 0. When I changed the domain of k to 0.00001 <= k <= 4, it stops generating exceptions while it took about 6 min to terminate.

[shmarovfedor]

Thank you, Soonho. Could you please add this example to the benchmarks?

[soonhokong]

Sure, I will do it. How did the previous version work with the example?

• Did it generate div-by-zero exceptions when the domain of k includes zero? I think I did some modification of CAPD-3.0 to ignore certain div-by-zero and continue to proceed. It might affect the behavior.
• How was the performance? Was it also take about 6 min or more/less?

[shmarovfedor]

In the previous version it was still generating division by 0.

The previous version was much slower on this example

[soonhokong]

I see. I think that makes sense.

FYI, I have some cases where CAPD3 still outperforms CAPD4. I think they change the algorithm for making ODE steps and sometimes CAPD4 picks up very tiny ODE steps which causes slow performance in ODE solving.

One idea is to run both of them in parallel and takes the one first to come and interrupts the other one. I'm working on this direction.

[shmarovfedor]

Great. Could you also please check another ticket I created today?

[soonhokong]

Sure, I'm on it now.

[scungao]

Email CAPD about this?

On Thu, Dec 18, 2014 at 11:22 AM, Soonho Kong notifications@github.com wrote:

I see. I think that makes sense.

FYI, I have some cases where CAPD3 still outperforms CAPD4. I think they change the algorithm for making ODE steps and sometimes CAPD4 picks up very tiny ODE steps which causes slow performance in ODE solving.

One idea is to run both of them in parallel and takes the one first to come and interrupts the other one. I'm working on this direction.

— Reply to this email directly or view it on GitHub https://github.com/dreal/dreal/issues/63#issuecomment-67511467.