z3 - Z3 可以为无约束的 UF 值输出“任何东西”吗？

Question

在搜索过程中，一些未解释函数的值可以不受约束。例如，如果在 smt 中仅f(1)调用查询，则f(2),f(3)可以是任何东西。有没有办法（某些选项可能）知道在求解过程中没有使用哪些值，因此可以是任何值？

Answer 1

对于无量词问题，您可以使用 to 选项:model-partial来实现true。这是一个示例（也可在此处获得）：

(set-option :model-partial true)

(declare-fun f (Int) Int)

(assert (> (f 0) 0))
(assert (< (f 1) 0))

(check-sat)
(get-model)

在这个例子中，我们得到输出：

sat
(model 
  (define-fun f ((x!1 Int)) Int
    (ite (= x!1 0) 1
    (ite (= x!1 1) (- 1)
      #unspecified)))
)

顺便说一句，在下一个版本（Z3 4.3.2）中，这个选项被重命名为:model.partial. 在下一个版本中，这些选项按模块分组。