1

Z3 を使用して、変数のさまざまな値に対して式の値を評価する必要がありました。Z3 が満足度チェッカーであることは知っていますが、model.Eval(Args) は、モデルによって生成された変数の値で式の評価を引き起こします。

式を評価するためにさまざまな値を反復処理することは可能ですか。

例 : p および q のすべての可能な値での p および q (p,q はブール値)

したがって、ある意味では、再帰または反復を使用して、そこから真理値表を作成します。Z3がそうする方法はありますか？

C# API のヘルプはさらに改善されます。

ありがとう

4

1 に答える 1

1

SubstituteC# APIのメソッドを検討することができます。pやなどの定数を値で置き換えるために使用できqます。また、置換を適用した後に式を簡略化/評価します。

を使用した小さな C# の例 (回帰スイートから) を次に示しますSubstitute。

using Microsoft.Z3;
using System;
using System.Collections.Generic;

class Test
{
    public void Run()
    {
        Dictionary<string, string> cfg = new Dictionary<string, string>() { 
            { "AUTO_CONFIG", "true" } };

        using (Context ctx = new Context(cfg))
        {
            IntExpr x = ctx.MkIntConst("x");
            IntExpr y = ctx.MkIntConst("y");

            FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { ctx.IntSort, ctx.IntSort }, ctx.IntSort);
            FuncDecl g = ctx.MkFuncDecl("g", new Sort[] { ctx.IntSort }, ctx.IntSort);
            Expr n = f[f[g[x], g[g[x]]], g[g[y]]];

            Console.WriteLine(n);

            Expr nn = n.Substitute(new Expr[] { g[g[x]], g[y] }, 
                                   new Expr[] { y, ctx.MkAdd(x, ctx.MkInt(1)) } );

            Console.WriteLine(nn);

            Console.WriteLine(n.Substitute(g[g[x]], y));
        }
    }
}

もちろん、すべての可能な値を反復するループを作成する必要があります。Python では、リスト内包表記を使用できます: http://rise4fun.com/Z3Py/56 もう 1 つのオプションは、メソッドを使用することSimplifyです。pこのメソッドは、やなどの未解釈の記号を含まない式を評価するために使用できますq。Python での別の例を次に示します: http://rise4fun.com/Z3Py/PC ブラウザーで C# の例を実行するためのサポートがないため、私は Python を使用しています。C# の Z3 API には、Python のすべての機能が含まれていることに注意してください。

最後に、別の可能性はモデルを列挙することです。これを行うことで、式を満たす (つまり、真にする)pとのすべての値を生成することになります。qアイデアは、現在のモデルをブロックする新しい制約を追加し、再度解決することです。これを行うための Python の小さなスクリプトを次に示します: http://rise4fun.com/Z3Py/PDJ

制約blockは、現在のモデルをブロックするために使用されます。コメントを外すprint blockと、Z3 で生産されたモデルごとに印刷することもできます。もちろん、この例のように式を満たす無限のモデルがある場合、このアプローチは終了しません: http://rise4fun.com/Z3Py/X0l

これらの例は、C# でエンコードできます。モデル内の定数 (および関数) を反復処理し、その解釈を取得する方法を示す C# の例を次に示します。

using Microsoft.Z3;
using System;

class Test
{

    public void Run()
    {        
        using (Context ctx = new Context())
        {
            Sort U = ctx.MkUninterpretedSort("U");
            FuncDecl f = ctx.MkFuncDecl("f", U, U);
            Expr a = ctx.MkConst("a", U);
            Expr b = ctx.MkConst("b", U);
            Expr c = ctx.MkConst("c", U);

            Solver s = ctx.MkSolver();
            s.Assert(ctx.MkEq(f[f[a]], b),
                     ctx.MkNot(ctx.MkEq(f[b], c)),
                     ctx.MkEq(f[c], c));
            Console.WriteLine(s.Check());
            Model m = s.Model;
            foreach (FuncDecl d in m.Decls)
                if (d.DomainSize == 0)
                    Console.WriteLine(d.Name + " -> " + m.ConstInterp(d));
                else 
                    Console.WriteLine(d.Name + " -> " + m.FuncInterp(d));

            Console.WriteLine(m.NumSorts);
            Console.WriteLine(m.Sorts[0]);

            foreach(Sort srt in m.Sorts)
                Console.WriteLine(srt);

            foreach (Expr v in m.SortUniverse(U))
                Console.WriteLine(v);
        }
    }
}
于 2012-05-19T14:52:20.697 に答える