1
默认情况下，全局变量被视为存在量化。例如。在SMT语言或Z3扩展中是否存在全局构造？
(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'中。所以我想逐步构建查询，将条件和变量（存在性和通用性）一个接一个地引入到上下文中 – Necto
我仍然没有看到问题所在。请注意，您可以使用多个量词，例如（forall（exists（forall（exists ....））））。 –