1

私は ConstInterp を使用して expr の定数リテラルの値を取得していました。

model.ConstInterp(lit)

しかし、奇妙なエラーが発生しました

... <body of some loop>
let x = model.ConstInterp(lit)
if solver.Check() == Status.SATISFIABLE
then model.ConstInterp(lit)

ConstInterpの2 回目の呼び出しでエラーが発生する

Unhandled Exception: Microsoft.Z3.Z3Exception: invalid argument
   at Microsoft.Z3.Native.Z3_model_get_const_interp(IntPtr a0,IntPtr a1,IntPtr a2)
   at Microsoft.Z3.Model.ConstInterp(FuncDecl f)
   at Microsoft.Z3.Model.ConstInterp(Expr a)

ただし、ConstInterp の代わりに Eval を使用した同じコードは問題ありません。ConstInterp の使用方法が間違っていませんか?

4

1 に答える 1

1

model.ConstInterp() への最初の呼び出しは、Check() への前回の呼び出し中に構築されたモデルを使用するため、異なる定数の解釈が含まれている可能性がありますが、これはここでは二次的な問題にすぎません。

すべてのモデルですべての定数が解釈される必要はありません。たとえば、すべての制約を満たすために定数の割り当てが必要ない場合は、割り当てられないままにすることができます (そのため、モデルに存在しません)。たとえば、次のプログラムを考えてみましょう。

Solver s = ctx.MkSolver();
s.Add(ctx.MkOr(
    ctx.MkEq(x, ctx.MkTrue()),
    ctx.MkEq(x, ctx.MkFalse()))); // Assert x = false OR x = true
s.Add(ctx.MkEq(y, ctx.MkTrue())); // Assert y = false
s.Check(); // Returns Status.SATISFIABLE

このプログラムは制約しませんxが、制約しますy。したがって、モデルには値が含まれずx、s.Model.ConstInterp(x)アサーションがスローされます。への呼び出しs.Model.Eval(x)はアサーションをスローしませんが、評価もしませんx。この例では、 を取得しますs.Model.Eval(x) == x。この動作は、 の 2 番目のパラメーターEval()を true に設定することで変更できます。これにより、モデルの完成が可能になります。つまり、

s.Model.Eval(x, true)

戻りfalseます。

別の方法として、配列s.Model.ConstDeclsには、モデルで解釈される定数のすべての関数宣言が含まれます。このセットに含まれていない定数には解釈がなく、「ドントケア」と見なすことができます。つまり、任意の値を割り当てることができます。

于 2013-03-26T15:59:27.453 に答える