0

この Z3 コードを C# で実行しようとしていますが、次のようなエラーがたくさんあります。

  • Z3V3 参照が必要
  • z3.MkSort("U") では、z3 が存在しないと表示されます
  • 用語参照必須参照

Z3 を実行してプログラム ファイルに含めましたが、このコードはどのように機能し、必要な .NET 参照はありますか?

class Program
{
    static void Main(string[] args)
    {
        {
            Console.WriteLine("prove_example1");
            mk_context();
            /* create uninterpreted type. */
            Sort U = z3.MkSort("U");
            /* declare function g */
            FuncDecl g = z3.MkFuncDecl("g", U, U);
            /* create x and y */
            Term x = z3.MkConst("x", U);
            Term y = z3.MkConst("y", U);
            /* create g(x), g(y) */
            Term gx = mk_unary_app(g, x);
            Term gy = mk_unary_app(g, y);
            /* assert x = y */
            Term eq = z3.MkEq(x, y);
            z3.AssertCnstr(eq);
            /* prove g(x) = g(y) */
            Term f = z3.MkEq(gx, gy);
            Console.WriteLine("prove: x = y implies g(x) = g(y)");
            prove(f);
            /* create g(g(x)) */
            Term ggx = mk_unary_app(g, gx);
           /* disprove g(g(x)) = g(y) */
            f = z3.MkEq(ggx, gy);
            Console.WriteLine("disprove: x = y implies g(g(x)) = g(y)");
            prove(f);
           /* Print the model using the custom model printer */
            z3.AssertCnstr(z3.MkNot(f));
            check2(LBool.True);
        }
    }
}
}
4

1 に答える 1

2

古い Z3 C# API の例からこのコード フラグメントをコピーしたようです。元の例にはフィールドがありましたContext z3;。mk_context、prove、などのいくつかの補助メソッドもありましたmk_unary_app。これらの追加メソッドをコピーしないと、例をコンパイルすることはできません。さらに、この例では古い C# API を使用しています。Z3 4.0 には新しい C# API があります。はるかに使いやすいです。Z3 4.0 に切り替えることをお勧めします (まだ使用していない場合)。Z3 4.0 ディストリビューションには、 というディレクトリがありexamples\dotnetます。このディレクトリには、 という大きな例と、それをビルド/コンパイルするためProgram.csのバッチ ファイルが含まれています。build.batこの例は、Z3 C# API の使用方法を示しています。次のリンクには、Z3 C# API のリファレンス マニュアルが含まれています。http://research.microsoft.com/en-us/um/redmond/projects/z3/class_microsoft_1_1_z3_1_1_context.html

于 2012-07-31T01:34:19.427 に答える