z3 - 简化 Z3 中未解释的函数

Question

有没有办法将简化应用于 z3 中定义的未解释函数，而不是目标和子目标？

我有以下 z3 代码:

(declare-fun f (Bool Bool) Bool)
(assert (forall ((b1 Bool) (b2 Bool))
        (implies b2 (f b1 b2))))
(assert (exists ((b1 Bool) (b2 Bool))
        (not (f b1 b2))))
(check-sat)
(get-model)

我得到以下输出:

sat
(model 
(define-fun b1!1 () Bool
  false)
(define-fun b2!0 () Bool
  false)
(define-fun k!7 ((x!1 Bool)) Bool
  false)
(define-fun f!8 ((x!1 Bool) (x!2 Bool)) Bool
  (ite (and (= x!1 false) (= x!2 true)) true
  false))
(define-fun k!6 ((x!1 Bool)) Bool
  (ite (= x!1 false) false
  true))
(define-fun f ((x!1 Bool) (x!2 Bool)) Bool
  (f!8 (k!7 x!1) (k!6 x!2)))
)

事实证明，通过对 f 的定义应用重写规则，我们可以得到
通过以下推导，f 等于第二个参数 (x!2):

(f!8 (k!7 x!1) (k!6 x!2))
= (f!8 false (k!6 x!2))
= (f!8 false x!2)
=(x!2) 

有没有办法让 z3 自动生成以下定义？

(define-fun f ((x!1 Bool) (x!2 Bool)) Bool
  (x!2))

谢谢你的帮助。
问候，
奥斯瓦尔多。

Answer 1

一种选择是让 Z3 计算表达式 (f x y)哪里x和 y是新的 bool 常量。 eval命令将被评估 (f x y)在当前模型中，将产生 y在你的例子中。这是完整的示例(也可在线获取 here):

(declare-fun f (Bool Bool) Bool)

; x and y are free Boolean constants that will be used to create the expression (f x y)
(declare-const x Bool)
(declare-const y Bool)

(assert (forall ((b1 Bool) (b2 Bool))
        (implies b2 (f b1 b2))))
(assert (exists ((b1 Bool) (b2 Bool))
        (not (f b1 b2))))
(check-sat)

(eval (f x y))