在 C# 中运行 Z3 时出现错误答案

【问题标题】：An error appears when running Z3 in C#在 C# 中运行 Z3 时出现错误
【发布时间】：2012-06-21 10:37:38
【问题描述】：

谁能帮忙！当我尝试运行下面的代码时，我得到了这个错误：

" 无法加载文件或程序集 '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();
        }

    }
}

}

【问题讨论】：

我认为您在 64 位机器中引用了 32 位 Microsoft.Z3.dll，反之亦然。确保您引用了正确的 Z3 版本并检查了 cmets 中的编译过程到此线程：stackoverflow.com/questions/10663994/…
谢谢，但我在 64 位机器上引用了 64 位 Microsoft.Z3.dll

标签： c# z3

【解决方案1】：

最简单的方法是使用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 中无法直接引用。

【讨论】：

我遵循了所有的说明，但真的没有用！！！请问还有什么建议吗？
Visual Studio 中的Platform 选项（x86、x64、AnyCPU）是什么？你是如何运行代码的？
我在 Visual Studio 中使用 (x86)，我复制了 x86 文件夹下的所有 .dll 和 Microsoft.Z3.dll，并使用 c# 代码将它们粘贴到同一路径中
如果你在 Visual Studio 中运行程序，应该没问题。如果你在VS之外运行程序，你应该将z3.dll和Microsoft.Z3.dll复制到与可执行文件相同的文件夹中。
实际上我在 Visual Studio 中运行它，这就是为什么我觉得这很奇怪

【解决方案2】：

在对这个问题的先前答案的 cmets 中，提到了 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 位，反之亦然，也就是说，可以为 32 位架构编译二进制文件（称为 x86 而不是 x64 ) 在 64 位机器上。也可以在 32 位机器上编译 64 位二进制文件。根据正在编译的二进制文件类型，必须添加正确的 dll 集。重要的设置是在 Visual Studio 中项目的构建配置中（在顶部，通常在选择调试/发布模式的位置旁边）。在这个编译阶段，在什么类型的机器上执行编译并不重要。实际机器仅在尝试在 32 位机器上运行 64 位二进制文件时才重要（但错误消息将与报告的不同）。在 64 位机器上运行 32 位二进制文件通常可以正常工作（但程序的最大内存使用量会受到限制）。

我希望这有助于消除一些困惑！

此外，我们同意包含两个版本的组合分发会造成一些不必要的混淆，因此未来我们将考虑为 32 位和 64 位二进制文件分发单独的安装程序。

【讨论】：