Z3中的定义理论

Question

我想将一阶理论放入Microsoft开发的SMT求解器Z3中。该理论包含两个对象 obj1 和 obj2 ，函数移动采用对象并返回一个动作，一个位置的谓词发生将动作作为参数。该理论包含公式发生（移动（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，我能够找到解决我的问题的解决方案。我需要做的是为操作提供唯一名称axioms ，在我的情况下是 move函数。我需要声明，当move具有两个不同的参数时，CC_2将永远不会返回cC_3的相同元素。这可以通过几种方式完成，但我发现这是最简洁的版本：

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

Answer 1

您假设您没有断言的约束。例如，没有什么使move成为恒定功能。Z3产生的模型是正确的。您可以通过在(check-sat)之后添加命令(get-model)来获取模型。命令(declare-sort Action 0)正在宣布一种不遗憾的排序。在Z3产生的模型中，排序Action的解释仅包含一个元素，而occurs和move是常数函数。这是一个模型，因为您的脚本中的所有断言都可以满足其满足。