有没有办法将简化应用于 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))
谢谢你的帮助。问候,奥斯瓦尔多。