C#学习教程:在C#中运行Z3时出现错误分享


在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.dllz3.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位二进制文​​件分配单独的安装程序。

上述就是C#学习教程:在C#中运行Z3时出现错误分享的全部内容,如果对大家有所用处且需要了解更多关于C#学习教程,希望大家多多关注—猴子技术宅(www.ssfiction.com)

本文来自网络收集,不代表猴子技术宅立场,如涉及侵权请点击右边联系管理员删除。

如若转载,请注明出处:https://www.ssfiction.com/ckf/959936.html

发表评论

邮箱地址不会被公开。 必填项已用*标注