Z3中的量词

Question

基本上，我想让Z3给我一个值大于10的任意整数。所以我写了下面的语句:

(declare-const x (Int))
(assert (forall ((i Int)) (> i 10)))
(check-sat)
(get-value(x))

我如何将此量词应用于我的模型?我知道你可以写(assert (> x 10))来实现这个，但是我的意思是我想要一个量词在我的模型中每次我声明一个整型常数它的值保证大于10，这样我就不必为我声明的每一个整型常数插入语句(assert (> x 10))。如果我必须使用宏来防止重复代码，那么量词的实际用途是什么?

Answer 1

您需要单独约束您声明的每个int。x > 10是正确的方法。

您可以使用宏或任何其他编码技术。在SMT求解器中，所有这些都扩展为规则约束。对运行时没有影响。

forall ((i Int)) (> i 10))表示"是否所有的整数都大于10?"，为假。

量词不会对您声明的所有变量进行量化。他们只对有界变量进行量化，这里是i。