是否有 SMT 语言或 Z3 扩展中的全局 forall 构造？
Is there a global forall construct in SMT language or a Z3 extension?
默认情况下，全局变量被视为存在量化。例如
(declare-const x Int)
(assert (exists ((y Int)) (and (= x y) (= x y))))
(check-sat)
(get-model)
给予
sat
(model
(define-fun y!0 () Int
0)
(define-fun x () Int
0)
)
如何让它将 x 视为 forall x，如以下查询：
(assert (forall ((x Int)) (exists ((y Int)) (and (= x y) (= x y)))))
(check-sat)
(get-model)
获取值y依赖于x:
sat
(model
(define-fun y!0 ((x!1 Int)) Int
x!1)
)
这应该只是语法问题。在 z3 中可以吗？在另一个 SMT 求解器中？
编辑：
我想要实现的是执行如下脚本：
(declare-forall-const x Int)
(declare-const y Int)
(assert (and (= x y) (= x y)))
(check-sat)
(get-model)
并得到如下响应：
sat
(model
(define-fun y!0 ((x!1 Int)) Int
x!1)
)
换句话说，我想全局声明"forall"参数，并在后续断言中引用它。
这不可能。在 SMT 求解器中，所有最外层变量都是存在的，但没有人强迫您只使用最外层变量。如果您只有一个量词范围，一种流行的方法是否定查询，即，您可以检查 exists x . not phi(x) 的不可满足性，而不是检查 forall x . phi(x) 的可满足性。
默认情况下，全局变量被视为存在量化。例如
(declare-const x Int)
(assert (exists ((y Int)) (and (= x y) (= x y))))
(check-sat)
(get-model)
给予
sat
(model
(define-fun y!0 () Int
0)
(define-fun x () Int
0)
)
如何让它将 x 视为 forall x，如以下查询：
(assert (forall ((x Int)) (exists ((y Int)) (and (= x y) (= x y)))))
(check-sat)
(get-model)
获取值y依赖于x:
sat
(model
(define-fun y!0 ((x!1 Int)) Int
x!1)
)
这应该只是语法问题。在 z3 中可以吗？在另一个 SMT 求解器中？
编辑：
我想要实现的是执行如下脚本：
(declare-forall-const x Int)
(declare-const y Int)
(assert (and (= x y) (= x y)))
(check-sat)
(get-model)
并得到如下响应：
sat
(model
(define-fun y!0 ((x!1 Int)) Int
x!1)
)
换句话说，我想全局声明"forall"参数，并在后续断言中引用它。
这不可能。在 SMT 求解器中，所有最外层变量都是存在的，但没有人强迫您只使用最外层变量。如果您只有一个量词范围，一种流行的方法是否定查询，即，您可以检查 exists x . not phi(x) 的不可满足性，而不是检查 forall x . phi(x) 的可满足性。