我最近开始使用 Z3，但目前对带有子逗号值的实数进行错误计算时遇到了问题。我使用 SMT2 在文本文件中定义问题并将其提供给 Z3（4.3 版）。
我使用非线性算法来解决调度问题，如果任务执行时间、周期等是自然数，例如 1.0、2.0，则该问题可以很好地解决。而例如 0.3 或 0.2 不会返回正确的结果。好像会有转换错误。对于不同的子逗号值，可以重现该问题。当前的解决方法是将常量乘以 10^x 以消除所有子逗号值，然后问题就解决了。
我可能会为以下代码产生错误：（它返回的 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)
该代码计算两个相互通信的周期性任务 t1 和 t2 的可行开始时间。受定义的截止日期约束并防止两个任务相交。s_t1 和 s_t2 分别代表 t1 和 t2 的开始时间， w_t1_t2 是等待时间， t_f1 代表从 t1 开始到 t2 完成的截止时间。周期为 5.0，deadline 为 6.0，t1 和 t2 的执行时间分别为 0.2 和 0.3，这里得到的结果是：s_t1=0.3，s_t2=0（相当于一个 5.0 作为它的周期性执行）和 w_t1_t2=5.0。但是，手动计算 w_t1_t2 会导致： w_t1_t2= s_t2 + period -(s_t2 + execution_time_t1)=0.0 +5.0 -(0.3+0.2)=4.5
相反，如果将 0.2 和 0.3 替换为 0.1 和 2.0，则结果是正确的。
我错过了什么吗？你对如何解决这个问题有什么建议吗？
谢谢你和最好的问候，弗洛里安