在C中運行Z3時出現錯誤＃

任何人都可以請幫忙！當我試圖運行下面的代碼，我得到這個錯誤：在C中運行Z3時出現錯誤＃

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

    } 
}

}

來源

2012-06-21 user1327010

我想你是在64位機器上引用32位'Microsoft.Z3.dll'，反之亦然。確保你參考了正確的Z3版本，並在此評論中查看編譯過程：http://stackoverflow.com/questions/10663994/evaluation-of-a-logical-formula-at-many-values-in-z3 – pad

謝謝，但我在64位機器推薦64位Microsoft.Z3.dll – user1327010

最簡單的方法是使用build.cmd腳本examples/dotnet文件夾並根據您的需要進行修改。該腳本將Microsoft.Z3.dll和z3.dll複製到工作目錄並編譯相應平臺上的代碼。

如果您從Visual Studio編譯：

確保您引用Microsoft.Z3.dll的版本與你編譯到平臺（86，64，......）相匹配。在bin和x64文件夾中有兩個Z3版本。
包含文件夾包含Microsoft.Z3.dll在項目屬性 - >參考路徑。原因是Microsoft.Z3.dll使用非託管z3.dll，它不能在Visual Studio中直接引用。

來源

2012-06-21 11:45:10 pad

我遵循所有說明，但真的沒有工作！有沒有其他建議？ – user1327010

什麼是Visual Studio中的「平臺」選項（x86，x64，AnyCPU）？你是如何運行代碼的？ – pad

我在Visual Studio中使用（x86），並且複製了x86文件夾下的所有.dlls和Microsoft.Z3.dll，並將它們粘貼到具有c＃代碼的相同路徑中 – user1327010

在對此問題的以前的答案的評論中，提到了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位體系結構64位（稱爲而非）機器。也可以在32位機器上編譯64位二進制文件。根據正在編譯什麼樣的二進制文件，必須添加正確的dll集。重要的設置是在Visual Studio中的項目的構建配置中（通常位於選擇調試/發佈模式的位置旁邊）。在編譯階段，執行編譯的機器類型無關緊要。當試圖在32位機器上運行64位二進制文件時（但錯誤信息與報告的錯誤信息不同），實際機器纔有意義。在64位機器上運行32位二進制文件通常可以正常工作（但程序的最大內存使用量將受到限制）。

我希望這有助於消除一些混亂！另外，我們同意包含兩個版本的合併分發會造成一些不必要的混淆，因此將來我們會考慮爲32位和64位二進制文件分發單獨的安裝程序。

來源

2012-06-27 18:35:13

在C中運行Z3時出現錯誤＃

回答

相關問題