我正在尝试将Z3 SMT 求解器用于我的项目。但是，Visual Studio 版本似乎不匹配，这给我带来了麻烦。我的 Visual Studio 2008 报告说
找不到引用的组件“Microsoft.Z3”。
虽然它确实在安装目录中（C:\Program Files\Microsoft Research\Z3-2.19\bin）。
编译项目时，另一个警告说
已解决的文件有错误的图像、没有元数据或无法访问。无法加载文件或程序集“C:\Program Files\Microsoft Research\Z3-2.19\bin\Microsoft.Z3.dll”或其依赖项之一。此程序集由比当前加载的运行时更新的运行时构建，无法加载。
以及其他错误，说明未找到 Z3 相关类型如上下文、术语等。
这是因为 Z3 的新版本是使用我没有的较新版本的 dotNet 框架编译的吗？我该如何解决这个问题？提前致谢！
PS：我在测试中使用的文件来自Z3教程（pdf），第5章，粘贴在下面。
using System;
using Microsoft.Z3;
class Program
{
Context ctx;
Term mk_int(int a) { return ctx.MkIntNumeral(a); }
Term mk_var(string name) { return ctx.MkConst(name, ctx.MkIntSort()); }
Term mk_lo(Term x) { return x >= mk_int(0); }
Term mk_mid(Term x, Term y, int a) { return y >= (x + mk_int(a)); }
Term mk_hi(Term y, int b) { return (y + mk_int(b)) <= mk_int(8); }
Term mk_precedence(Term x, Term y, int a, int b)
{
return ctx.MkAnd(new Term[] { mk_lo(x), mk_mid(x, y, a), mk_hi(y, b) });
}
Term mk_resource(Term x, Term y, int a, int b)
{
return (x >= (y + mk_int(a))) | (y >= (x + mk_int(b)));
}
void encode()
{
using (Config cfg = new Config())
{
cfg.SetParamValue("MODEL", "true");
using (Context ctx = new Context(cfg))
{
this.ctx = ctx;
Term t11 = mk_var("t11");
Term t12 = mk_var("t12");
Term t21 = mk_var("t21");
Term t22 = mk_var("t22");
Term t31 = mk_var("t31");
Term t32 = mk_var("t32");
ctx.AssertCnstr(mk_precedence(t11, t12, 2, 1));
ctx.AssertCnstr(mk_precedence(t21, t22, 3, 1));
ctx.AssertCnstr(mk_precedence(t31, t32, 2, 3));
ctx.AssertCnstr(mk_resource(t11, t21, 3, 2));
ctx.AssertCnstr(mk_resource(t11, t31, 2, 2));
ctx.AssertCnstr(mk_resource(t21, t31, 2, 3));
ctx.AssertCnstr(mk_resource(t12, t22, 2, 3));
ctx.AssertCnstr(mk_resource(t12, t32, 3, 1));
ctx.AssertCnstr(mk_resource(t22, t32, 3, 1));
Model m = null;
LBool r = ctx.CheckAndGetModel(out m);
if (m != null)
{
m.Display(System.Console.Out);
m.Dispose();
}
}
}
}
static void Main()
{
Program p = new Program();
p.encode();
}
};
更新：在对旧的 .msi 安装程序文件进行几次提取后，我发现使用低于 v4 的 dotNet Framework 的 Z3 的最新版本是 Z3 2.11；在这种情况下，我决定使用，而不是暂时更新我的 VS2008。