2011-07-18 20 views
1

私のプロジェクトにZ3 SMT solverを使用しようとしています。しかし、それは私の問題を引き起こしたVisual Studioのバージョンの不一致があるようです。私のVisual Studio 2008レポートそのDLLバージョンが一致しませんか?

参照先のコンポーネント '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 Frameworkを使ってコンパイルされているので、これはありますか?この問題を解決するにはどうすればよいですか?前もって感謝します!

PS:私がテストで使用したファイルは、Z3 tutorial (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(); 
    } 
}; 

UPDATE:古いの.msiインストーラファイルのいくつか抽出した後、私はあまりV4はZ3 2.11であるよりも、DOTNETフレームワークを使用していますZ3の最新バージョンを発見しました。私のVS2008を現時点で更新するのではなく、使用することにしました。

+0

これまでにお聞きしたことがありますか? –

答えて

1

これは、Z3ライブラリよりも古い.NET Frameworkを対象としている可能性が高いためです。たとえば、Z3バージョンの.NET 4をターゲットにしている場合は、Visual Studio 2010でこれを作成し、.NET Framework 4.0をターゲットにしていることを確認します。

+0

クイック返信ありがとう。もう2つの質問があります。 1.私が持っているZ3 dllがVS2010から来ていることをどうすれば保証できますか?今私はこれが理由だと思うだけです。 2.そうなら、VS2008でそれを行う方法はありませんか?ありがとう! –

+0

@ Xiaopeng:私が知る唯一の "質問"はこれに関連しています。 VS 2010をダ​​ウンロードし、.NET 4をターゲットにする必要があります。問題が修正されます。あなたの他の質問は何ですか? –

+0

@ Xiaopeng:Ildasm(http://msdn.microsoft.com/en-us/library/f7dy01k1.aspx)で実行してください - フレームワークのバージョンがわかります。 .NET 4をターゲットにしている場合は、VS 2010が必要です.VS 2010 Expressはhttp://www.microsoft.com/express –

関連する問題