1

任何人都可以请帮助！当我尝试运行下面的代码时，我收到了这个错误：

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

    }
}

}

4

2 回答 2

1

在对这个问题的先前答案的评论中，提到了 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 位二进制文​​件分发单独的安装程序。

于 2012-06-27T18:35:13.893 回答
1

最简单的方法是使用文件夹中的build.cmd脚本examples/dotnet并根据需要进行修改。该脚本将Microsoft.Z3.dll和复制z3.dll到工作目录并在相应平台上编译代码。

如果从 Visual Studio 编译：

  • 确保Microsoft.Z3.dll您引用的版本与您正在编译的平台（x86、x64、...）相匹配。bin和x64文件夹中有两个Z3版本。
  • 包括包含Project Properties -> Reference PathsMicrosoft.Z3.dll的文件夹。原因是使用 unmanaged ，您无法在 Visual Studio 中直接引用。Microsoft.Z3.dllz3.dll
于 2012-06-21T11:45:10.187 回答