Z3中的量词

Question

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

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

如何将此量词应用于我的模型？我知道你可以写(assert(> x 10))来实现这一点.但我的意思是我想在我的模型量词所以每次我宣布一个整型常量,其值是保证时间将超过10所以我不必为每一个整型常量,我insert语句(主张(>×10))声明.

Answer 1

当你使用时(assert (forall ((i Int)) (> i 10))),i是一个有界变量,量化的公式相当于一个真值,false在这种情况下.

我想你想用量词来定义一个宏:

(declare-fun greaterThan10 (Int) Bool)
(assert (forall ((i Int)) (= (greaterThan10 i) (> i 10))))

您可以使用它们来避免代码重复:

(declare-const x (Int))
(declare-const y (Int))
(assert (greaterThan10 x))
(assert (greaterThan10 y))
(check-sat)

它实质上是在使用Z3 API时使用未解释函数定义宏的方法.请注意,您必须(set-option :macro-finder true)按顺序设置Z3将通用量词替换为这些函数的主体.

但是,如果您正在使用文本界面,define-funSMT-LIB v2中的宏是一种更简单的方法来执行您想要的操作:

(define-fun greaterThan10 ((i Int)) Bool
  (> i 10))