z3 - Z3 中的 FOL 定义理论

Question

我想把一阶理论放到微软开发的SMT求解器Z3中。该理论包含两个对象 obj1 和 obj2，一个函数 move 接受一个对象并返回一个 Action ，以及一个将 Action 作为参数的单置谓词发生。该理论包含公式出现(移动(obj1))，我想确保这是发生谓词为真的唯一方式。我通过给出发生的定义来做到这一点:

forall (A) (occurs(A) <-> (A = move(obj1)))

这意味着可以从理论中推断出发生(移动(obj1))，但发生(移动(obj2))不能。为了证明这一点，我将其翻译成 Z3 如下:

(declare-datatypes () (( Obj obj1 obj2 )))
(declare-sort Action 0)

(declare-fun occurs (Action) Bool)
(declare-fun move (Obj) Action)

(assert (forall ((A Action)) (
    = (occurs A) (= A (move obj1))
)))

(check-sat)
(get-value ((occurs (move obj1))))
(get-value ((occurs (move obj2))))

问题是这给出了以下输出:

sat
(((occurs (move obj1)) true))
(((occurs (move obj2)) true))

我不明白，因为发生的定义提供了谓词为真的所有必要和充分条件，所以我认为发生(移动(obj2))在任何模型中都不能为真。我做错了什么？

更新
多亏了 de Moura，我才能够为我的问题找到解决方案。我需要做的是为 Action 提供唯一的名称公理，在我的例子中是 move功能。我需要声明 move永远不会返回相同的排序元素 Action当它有两个不同的参数时。这可以通过多种方式完成，但我发现这是最简洁的版本:

(assert (forall ((o1 Obj) (o2 Obj)) 
    (=> (not (= o1 o2)) (not (= (move o1) (move o2))))))

Answer 1

您正在假设您没有断言的约束。例如，没有什么可以阻止 move为常数函数。
Z3生产的模型是正确的。您可以通过添加命令(get-model) 来获取模型。之后 (check-sat) .
命令 (declare-sort Action 0)正在声明一种未经解释的排序。
Z3出品的模型中，sort Action的解释只包含一个元素，并且 occurs和 move是常数函数。这是一个模型，因为脚本中的所有断言都由它满足。