プロジェクトで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' またはその依存関係の 1 つを読み込めませんでした。このアセンブリは、現在読み込まれているランタイムよりも新しいランタイムによってビルドされているため、読み込むことができません。
Context、TermなどのZ3関連タイプが見つからないという他のエラーとともに。
これは、Z3 の新しいバージョンが、私が持っていない新しいバージョンの dotNet Framework を使用してコンパイルされているためですか? この問題を解決するにはどうすればよいですか? 前もって感謝します！
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 を当面更新する代わりに、使用することにします。