Incorrect calculations in Z3 for sub comma values of Real numbers

Question

I recently started using Z3 and currently have issues with incorrect calculations for Real numbers with sub comma values. I use SMT2 to define the problem in a text file and feed it to Z3 (version 4.3).

I use non-linear arithmetic for solving a scheduling problem which solves well if the task execution time, period, etc. are in natural numbers e.g., 1.0, 2.0. While for instance 0.3 or 0.2 would not return a correct result. It seems as if there would be a conversion error. The problem can be reproduced for different sub comma values. Current work around is to multiply the constants by 10^x to eliminate all sub comma values and then the problem solves fine.

I could produce the error for the following code: (It returns an incorrect value for w_t1_t2)

(set-option :produce-models true)
(declare-const s_t2 Real)
(declare-const s_t1 Real)
(declare-const w_t1_t2 Real)
(declare-const t_f1 Real)
(assert (<= 0 s_t2 5.0))
(assert (<= 0 s_t1 5.0))
(assert (xor (<= (+ (+ 0.0 s_t2) 0.3) (+ 0.0 s_t1)) (<= (+ (+ 0.0 s_t1) 0.2) (+ 0.0 s_t2))))
(assert (xor (<= (+ (+ 0.0 s_t2) 0.3) (+ 5.0 s_t1)) (<= (+ (+ 5.0 s_t1) 0.2) (+ 0.0 s_t2))))
(assert (xor (<= (+ (+ 5.0 s_t2) 0.3) (+ 0.0 s_t1)) (<= (+ (+ 0.0 s_t1) 0.2) (+ 5.0 s_t2))))
(assert (xor (<= (+ (+ 5.0 s_t2) 0.3) (+ 5.0 s_t1)) (<= (+ (+ 5.0 s_t1) 0.2) (+ 5.0 s_t2))))
(assert (<= 0 w_t1_t2 5.0))
(assert (xor (= w_t1_t2 (- s_t2 (mod (+ s_t1 0.2) 5.0))) (= w_t1_t2 (- (+ s_t2 5.0) (mod (+ s_t1 0.2) 5.0)))))
(assert (<= (+ 0.3 0.2) t_f1 6.0))
(assert (>= t_f1 (+ (+ 0.3 0.2) (+ w_t1_t2))))
(check-sat)
(get-value ( s_t2 s_t1 w_t1_t2 t_f1))
(exit)

The code calculates feasible start times for two periodic tasks t1 and t2 communicating with each other. Constrained by a defined deadline and preventing that both tasks intersect. s_t1 and s_t2 stand for the start times of t1 and t2 respectively, w_t1_t2 is the waiting time and t_f1 stands for the deadline from the start of t1 till the completion of t2. With a period of 5.0, a deadline of 6.0 and execution time of 0.2 and 0.3 for t1 and t2 respectively, the result obtained here is: s_t1=0.3, s_t2=0 (equalling a 5.0 as its periodically executed) and w_t1_t2=5.0. However, calculating w_t1_t2 by hand leads to: w_t1_t2= s_t2 + period -(s_t2 + execution_time_t1)=0.0 +5.0 -(0.3+0.2)=4.5

If in contrast 0.2 and 0.3 would be replaced by 0.1 and 2.0 the result is correct.

Am I missing something? Do you have any suggestions on how to solve this problem?

Thank you and best regards, Florian

Answer 1

The equation:

 (= w_t1_t2 (- (+ s_t2 5.0) (mod (+ s_t1 0.2) 5.0)))

is satisfied. You are using the operator "mod", which is defined for integers. Z3 inserts coercions from Reals to integers such that (+ s_t1 0.2) is the floor.