在C＃Z3运行时，会出现一个错误 [英] An error appears when running Z3 in C#

问题描述

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

Can anyone please help! When I tried to run the code below, I got this error:

无法加载文件或程序集微软。 Z3，版本= 4.0.0.0，
区域性=中性公钥= 9c8d792caae602a2'或其
依赖项。试图加载一个不正确的程序
格式为

" Could not load file or assembly 'Microsoft.Z3, Version=4.0.0.0, Culture=neutral, PublicKeyToken=9c8d792caae602a2' or one of its dependencies. An attempt was made to load a program with an incorrect format "

下面是代码：

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();
        }

    }
}

}

}

推荐答案

在评论以前这个问题的答案，参考了x86的分配和x64的分布作了，我我不知道这个问题解决了。为了澄清：

In the comments to the previous answers to this question, reference to the x86 distribution and to the x64 distribution were made, and I am not sure this issue is resolved. To clarify:

在编译一个64位二进制（在Visual Studio中称为64位），然后z3.dll和Microsoft.Z3.dll的64位版本需要。这些被称为 64 在Z3分布文件夹中找到。请注意，这样做的不可以依赖的Visual Studio正在运行的实际的机器上。

When compiling a 64-bit binary (called x64 in visual studio), then the 64-bit versions of z3.dll and Microsoft.Z3.dll are required. Those are found in the folder called x64 in the Z3 distribution. Note that this does not depend on the actual machine that Visual Studio is running on.

在编译一个32位二进制，则该dll文件从斌是必需的目录。同样，这确实的不可以依赖的Visual Studio正在运行的实际的机器上。

When compiling a 32-bit binary, then the dlls from the bin directory are required. Again, this does not depend on the actual machine that Visual Studio is running on.

Visual Studio中可以交叉编译从32到64位反之亦然，也就是说，它可以编译为二进制32位架构（名为 86 ，而不是 64 ）在64位机器。另外，也可以向编译一个32位机器上的64位二进制文​​件。根据一种二进制文件被编译什么，dll的权集必须添加。 ，重要的设置是在您的项目在Visual Studio中构建配置（顶部，平时旁边，其中选择调试/发布模式）。在此编译阶段，它无关紧要正在执行什么类型的机器的编制上。当试图运行在32位机器上的64位二进制文​​件的实际台机器只事项（但随后的错误信息将是一个不同的报道）。运行在64位机器上的32位二进制文​​件通常还不错（但该方案的最大内存使用量将受到限制）。

Visual Studio can cross-compile from 32 to 64 bit and vice versa, i.e., it is possible to compile a binary for the 32-bit architecture (called x86 as opposed to x64) on 64-bit machines. It is also possible to compile 64-bit binaries on a 32-bit machine. Depending on what kind of binary is being compiled, the right set of dlls must be added. The setting that matters is in the build configuration of your project in Visual Studio (on top, usually next to the where debug/release mode is selected). At this compilation stage, it does not matter what type of machine the compilation is being performed on. The actual machine only matters when an attempt is made to run a 64-bit binary on a 32-bit machine (but then the error message will be different from the one reported). Running 32-bit binaries on 64-bit machines usually works fine (but the maximum memory usage of the program will be limited).

我希望这有助于去掉一些混乱！

I hope this helped to remove some of the confusion!

此外，我们同意，包括两个版本的组合分配造成一些不必要的混乱，所以在未来我们会考虑在32位分配单独的安装和64位二进制文​​件。

Also, we agree that the combined distribution including both versions creates some unnecessary confusion, so in the future we will consider distributing separate installers for the 32-bit and the 64-bit binaries.

这篇关于在C＃Z3运行时，会出现一个错误的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！