z3 - 指定 Z3 的初始模型值

Question

如何为模型指定初始“软”值？该初始模型是解决类似查询的结果，并且该模型很可能具有正确的部分，甚至对于当前查询可能是正确的。

目前，我正在通过增量求解和 hard/soft constraints 对此进行模拟。 :

(define-fun trans_assumed ((a Int)) Int
; an initial model, which may be (partially) true
)

(declare-fun trans_sought ((a Int)) Int) 

(declare-const p Bool)
(assert (=> p (forall ((a Int)) (= (trans_assumed a) (trans_sought a)))))
(check-sat p) ; in hope that trans_assumed values will be used as initial below

; add here the main constraints for trans_sought function

(check-sat) ; Z3 will use trans_assumed as a starting point for trans_sought

这是否真的为 trans_sought 指定了初始值？成为 trans_assumed ?

与顺序相比，增量求解模式较慢。有没有更好的方法来引入初始值？

Answer 1

我认为这是一个很好的方法，但您可以考虑使用更多的 bool 变量。现在，它是一种“全部”或“无”方法。在您的脚本中，当 (check-sat p)执行后，Z3 将寻找一个模型，其中 trans_assumed和 trans_sought有相同的解释。如果这样的模型不存在，它将返回包含 p 的 unsat 核心。 .当(check)被执行，Z3 可以自由分配 p至 false ，而全称量词本质上是一个无关紧要的。即，trans_assumed和 trans_sought可以完全不同。

如果使用多个 bool 变量来控制 trans_sought 的解释，您将拥有更大的灵活性。
如果您的问题的其余部分没有量词，您应该考虑删除全称量词。如果您只关心 trans_sought 的值，则可以这样做。在有限数量的点上。

假设我们有 trans_assumed(0) = 1和 trans_assumed(1) = 10 .然后，我们可以写:

assert (=> p0 (= (trans_sought 0) 1)))
assert (=> p1 (= (trans_sought 1) 10)))

在这种编码中，我们可以查询 (check-sat p0 p1) , (check-sat p0) , (check-sat p1)