1

我正在编写一个通用函数来使用Z3 的 .NET API从模型中获取对FuncDecl的解释。

这是一个简化的代码片段：

Model m = s.Model;
foreach (FuncDecl d in m.Decls)
    if (d.DomainSize == 0 && d.Arity == 0)
       Console.WriteLine(d.Name + " -> " + m.ConstInterp(d));
    else 
       Console.WriteLine(d.Name + " -> " + m.FuncInterp(d));

但是，当代码尝试调用ConstInterp.

Microsoft.Z3.Z3Exception：非零元函数和数组将 FunctionInterpretations 作为模型。使用 FuncInterp。

我检查了Model上的所有属性，但似乎没有任何属性有助于在数组声明上创建正确的条件。

我怎样才能解决这个问题？我是否也错过了任何其他类型的声明？

4

1 回答 1

1

数组常量在 Z3 中是一个例外，因为它们具有作为模型的函数解释。这就是为什么 ConstInterp 不适用并因此引发异常的原因。恐怕目前最好的解决方案只是检查 funcdecl 的范围，直到我们得到更好的解决方案。

例如，更换

if (d.DomainSize == 0 && d.Arity == 0)

和

if (d.DomainSize == 0 && d.Arity == 0 && d.Range.SortKind != Z3_ARRAY_SORT)
于 2013-01-10T18:21:28.317 回答