1

Z3の.NETAPIを使用して、モデルから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 に答える