Z3可以输出“任何东西"吗?对于无约束的 UF 值? [英] Can Z3 output "anything" for unconstrained values of UF?

问题描述

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

Some values of uninterpreted functions can be unconstrained during the search. For example, if in smt query only f(1) is called, then f(2), f(3) can be anything. Is there a way (some option may be) to know which values were not used during the solving and therefore can be anything?

推荐答案

对于没有量词的问题，您可以通过使用选项 :model-partial 到 true 来实现.这是一个示例(也可在此处获得):

For quantifier free problems, you can achieve that by using the option :model-partial to true. Here is an example (also available here):

(set-option :model-partial true)

(declare-fun f (Int) Int)

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

(check-sat)
(get-model)

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

In this example, we get the output:

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.在下一个版本中，选项按模块分组.

BTW, in the next release (Z3 4.3.2), this option is renamed to :model.partial. In the next release, the options are grouped in modules.

这篇关于Z3可以输出“任何东西"吗?对于无约束的 UF 值?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！