0

我正在尝试在 C# 中运行此 Z3 代码，但有很多错误，例如：

  • 需要 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 回答