关于Z3中未解释函数的表示

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 选择在范围中更频繁出现的值。这里的范围是指 Z3 分配给特定有限输入值集的有限值集。在我们的示例中，range 中仅出现 true。因此，选择 true 作为 else 值。

对于无量词（和无数组）问题，如果不使用选项 :model-compact true ，则 else 的值并不重要。
也就是说，如果公式F可满足，Z3将产生模型M。然后，如果我们更改 M 中任何 else 的值，生成的模型 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)

Answer 2

以下内容怎么样（RiSE4fun 链接）？

(set-option :MBQI true)

(declare-fun FPolicy (Int Int Int) Bool)

(assert (forall ((x1 Int) (x2 Int) (x3 Int)) (!
  (implies
    (not
      (or
        (and (= x1 0) (= x2 1) (= x3 30))
        (and (= x1 0) (= x2 2) (= x3 20))))
      (= (FPolicy x1 x2 x3) false))
  :pattern (FPolicy x1 x2 x3))))

(assert (FPolicy 0 1 30))
(assert (FPolicy 0 2 20))

(check-sat)
(get-model)

我看到的优点是您可以更改它，使 FPolicy(0 1 30) == false 无需触及 forall-constraint。
明显的缺点是您基本上必须两次提及所有参数元组，并且创建的模型相当复杂。

我期待看到更好的解决方案:-)