在C＃中运行Z3时出现错误
谁能请帮忙！ 当我尝试运行下面的代码时，我收到此错误：
“无法加载文件或程序集’Microsoft.Z3，Version = 4.0.0.0，Culture = neutral，PublicKeyToken = 9c8d792caae602a2’或其依赖项之一。尝试加载格式不正确的程序”
这是代码：
class Program { static void Main(string[] args) { using (Context ctx = new Context()) { RealExpr c = ctx.MkRealConst("c"); BoolExpr Eqzero = ctx.MkGt(c, ctx.MkReal(0)); BoolExpr Gezero = ctx.MkGe(c, ctx.MkReal(0)); BoolExpr Lttwo = ctx.MkLt(c, ctx.MkReal(2)); BoolExpr Gtthree = ctx.MkGt(c, ctx.MkReal(3)); BoolExpr b1 = ctx.MkBoolConst("b1"); BoolExpr b2 = ctx.MkBoolConst("b2"); BoolExpr b3 = ctx.MkBoolConst("b3"); BoolExpr b0 = ctx.MkBoolConst("b0"); RealExpr[] lamb = new RealExpr[1]; lamb[0] = ctx.MkRealConst("lamb"); BoolExpr temp = ctx.MkAnd(ctx.MkGt(lamb[0], ctx.MkReal(0)), ctx.MkEq(b0, ctx.MkTrue()), ctx.MkEq(b1, ctx.MkTrue()), ctx.MkGe(ctx.MkAdd(c, lamb[0]), ctx.MkReal(0)), ctx.MkLe(ctx.MkAdd(c, lamb[0]), ctx.MkReal(3)), ctx.MkGe(c, ctx.MkReal(0)), ctx.MkLe(c, ctx.MkReal(3))); BoolExpr exist = ctx.MkExists(lamb, temp, 1, null, null, ctx.MkSymbol("Q2"), ctx.MkSymbol("skid2")); Console.WriteLine(exist.ToString()); Solver s1 = ctx.MkSolver(); s1.Assert(exist); if (s1.Check() == Status.SATISFIABLE) { Console.WriteLine("get pre"); Console.Write(s1); } else { Console.WriteLine("Not reach"); } Console.ReadKey(); } } } }
最简单的方法是在examples/dotnet文件夹中使用build.cmd脚本并根据需要进行修改。 该脚本将Microsoft.Z3.dll和z3.dll复制到工作目录，并在相应的平台上编译代码。
如果从Visual Studio编译：
- 确保您引用的
Microsoft.Z3.dll版本与您正在编译的平台（x86，x64，…）匹配。bin和x64文件夹中有两个Z3版本。 - 在项目属性 – > 参考路径中包含包含
Microsoft.Z3.dll的文件夹。 原因是Microsoft.Z3.dll使用非托管z3.dll，您无法在Visual Studio中直接引用它。
在对此问题的先前答案的评论中，提到了对x86分发和x64分发的引用，并且我不确定此问题是否已得到解决。 澄清：
编译64位二进制文件（在visual studio中称为x64）时，需要64位版本的z3.dll和Microsoft.Z3.dll。 这些可以在Z3发行版中名为x64的文件夹中找到。 请注意，这不依赖于运行Visual Studio的实际计算机。
编译32位二进制文件时，需要bin目录中的dll。 同样，这不依赖于运行Visual Studio的实际机器。
Visual Studio可以从32位到64位进行交叉编译，反之亦然，也就是说，可以在64位计算机上为32位体系结构（称为x86而不是x64 ）编译二进制文件。 也可以在32位机器上编译64位二进制文件。 根据正在编译的二进制类型，必须添加正确的dll集。 重要的设置是在Visual Studio中项目的构建配置中（在顶部，通常在选择调试/发布模式的位置旁边）。 在此编译阶段，正在执行编译的机器类型无关紧要。 实际的机器只在尝试在32位机器上运行64位二进制文件时才会起作用（但是错误消息将与报告的错误消息不同）。 在64位计算机上运行32位二进制文件通常可以正常工作（但程序的最大内存使用量将受到限制）。
我希望这有助于消除一些混乱！
此外，我们同意包括两个版本的组合分发会产生一些不必要的混淆，因此将来我们将考虑为32位和64位二进制文件分配单独的安装程序。