2

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

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

这意味着从理论上可以推断出发生(move(obj1)) ，但发生(move(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))

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

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

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

1 回答 1

3

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

于 2012-10-29T21:58:13.703 回答