从C＃应用程序

Question

我试图运行在C＃这Z3代码引用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); 
     } 
    } 
} 
} 

Answer 1

看起来你从旧的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