【问题标题】：Is there a global forall construct in SMT language or a Z3 extension?是否有 SMT 语言或 Z3 扩展的全局 forall 构造？
【发布时间】：2016-05-24 11:29:32
【问题描述】：

默认情况下，全局变量被视为存在量化。例如

(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”参数，并在后续的断言中引用它。

【问题讨论】：

要让 Z3 将 x 视为通用的，您可以添加一个 forall 量词，就像您建议的那样。所以，我不确定问题是什么。
@ChristophWintersteiger，我想逐步介绍许多这样的变量x1、x2、...，而不是在单个assert 中。所以我想构建查询，将条件和变量（存在的和通用的）一个接一个地引入上下文
我还是不明白问题出在哪里。请注意，您可以使用多个量词，例如(forall (exists (forall (exists ....))))。
@ChristophWintersteiger，问题在于通过提供许多断言和声明逐步填充 z3 上下文来逐步构建查询。我想利用 z3 push/pop 指令，并为多个类似查询运行单个求解器实例（人们通常使用symbex 验证的方式）
是的，这很好，您可以逐步构建查询，并且可以使用 push/pop。我仍然不明白问题是什么。有什么不行的吗？

标签： constraints z3 solver smt

【解决方案1】：

这是不可能的。在 SMT 求解器中，所有最外层的变量都是存在的，但没有人强迫您只使用最外层的变量。如果您只有一个量词范围，一种流行的方法是否定查询，即，不是检查forall x . phi(x) 的可满足性，而是检查exists x . not phi(x) 的不可满足性。

【讨论】：