Z3 为涉及整数除法的简单查询返回未知数答案

【问题标题】：Z3 returning unknown for a simple query involving integer divisionZ3 为涉及整数除法的简单查询返回未知数
【发布时间】：2016-02-10 22:43:08
【问题描述】：

这是一个涉及整数除法（即非线性运算）的简单 Z3 查询：

(declare-const a01 Int)
(declare-const a02 Int)
(assert(or (= (/ a01 a02) 2) (= (/ a02 a01) 2)))
(assert( > a01 0))
(assert( > a02 0))
(check-sat)

Z3 在尝试解决此查询时返回 uknown for。我知道非线性整数算术是不可判定的，但我仍然希望 Z3 在实践中不会那么脆弱。

如果我遗漏了一些我可以为 Z3 设置的明显参数以帮助它解决此类查询，请告诉我。我正在使用 Z3 4.4.1，我也在rise4fun 上尝试了该版本。谢谢！

【问题讨论】：

标签： z3

【解决方案1】：

使用div 而不是/。

(declare-const a01 Int)
(declare-const a02 Int)
(assert(or (= (div a01 a02) 2) (= (div a02 a01) 2)))
(assert( > a01 0))
(assert( > a02 0))
(check-sat)

【讨论】：