z3 - 关于 Z3 中 Uninterpreted Function 的表示

Question

我有一个简短的问题。我写了一个简单的程序(使用 Z3 NET API)并得到如下输出。

程序(部分):

        Sort[] domain = new Sort[3];
        domain[0] = intT;  
        domain[1] = intT;          
        domain[2] = intT;  
        FPolicy = z3.MkFuncDecl("FPolicy", domain, boolT);      

        Term[] args = new Term[3];
        args[0] = z3.MkNumeral(0, intT);
        args[1] = z3.MkNumeral(1, intT);
        args[2] = z3.MkNumeral(30, intT);
        z3.AssertCnstr(z3.MkApp(FPolicy, args));

        args[1] = z3.MkNumeral(2, intT);
        args[2] = z3.MkNumeral(20, intT);
        z3.AssertCnstr(z3.MkApp(FPolicy, args));

输出:

FPolicy -> {
  0 1 30 -> true
  0 2 20 -> true     
  else -> true
}

我想知道我能否将“else -> true”设为 false(即“else -> false”)。

Answer 1

对于无量词的问题，Z3 (3.2) 将为 else 选择range 中出现频率更高的值.通过 range在这里，我指的是 Z3 分配给特定有限输入值集的有限值集。在我们的示例中，只有 true发生在 range .因此，true被选为 else值(value)。

对于无量词(和无数组)的问题，如果选项 :model-compact true不使用，那么else的值没关系。也就是说，如果公式 F是可满足的，Z3 将产生一个模型 M .然后，如果我们更改任何 else 的值在 M , 结果模型 M’仍然是F的模型.因此，您可以忽略 else ，或者假设它是你想要的任何东西，如果输入公式 F没有量词，F不使用数组理论，并且:model-compact true未使用。此属性基于当前在 Z3 中实现的算法，将来可能会发生变化。相比之下，mhs提供的解决方案不受Z3实现变化的影响。在他的编码中，任何 SMT 求解器(成功生成模型)都必须使用 false作为量词前件中未指定的每个点的函数值。

另一种选择是使用 default运算符，并使用数组对您的问题进行编码。什么时候，default使用运算符，我们应该将数组视为成对:(实际数组，默认值)。此默认值用于提供 else模型构建期间的值。Z3 还有几个内置公理来传播默认值:store和 map运营商。这是您使用这种方法编码的问题:

(set-option :produce-models true)
(declare-const FPolicy (Array Int Int Int Bool))

(assert (select FPolicy 0 1 30))
(assert (select FPolicy 0 2 20))
(assert (not (default FPolicy)))

(check-sat)
(get-model)