Ошибка при запуске Z3 в C#

Может ли кто-нибудь помочь? Когда я попытался запустить этот код, я получил эту ошибку:Ошибка при запуске Z3 в C#

" 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

Я думаю, что вы ссылаетесь на 32-разрядную «Microsoft.Z3.dll» на 64-битной машине или наоборот. Убедитесь, что вы ссылаетесь на правую версию Z3 и проверяете процедуру компиляции в комментариях к этой теме: http://stackoverflow.com/questions/10663994/evaluation-of-a-logical-formula-at-many-values-in-z3 – pad

спасибо, но я переписывал 64-разрядную версию Microsoft.Z3.dll в 64-разрядной машине – user1327010

Самый простой способ заключается в использовании build.cmd скрипт в examples/dotnet папке и изменить его в соответствии с вашими потребностями. Сценарий копирует Microsoft.Z3.dll и z3.dll в рабочий каталог и компилирует код на соответствующей платформе.

Если вы собираете из Visual Studio:

Убедитесь, что версия Microsoft.Z3.dll «s вы ссылаетесь совпадает с платформой (x86, x64, ...), которые вы собираете в. Существуют две версии Z3 в папке bin и x64.
Включите папку, содержащую Microsoft.Z3.dll, в Свойства проекта ->Пути ссылок. Причина в том, что Microsoft.Z3.dll использует неуправляемый z3.dll, который вы не можете напрямую ссылаться в Visual Studio.

источник

2012-06-21 11:45:10 pad

Я следил за всеми инструкциями, но на самом деле не работал !!! есть ли другое предложение, пожалуйста? – user1327010

Какова ваша опция «Платформа» (x86, x64, AnyCPU) в Visual Studio? Как вы запустили код? – pad

Я использую (x86) в Visual Studio, и я скопировал все .dlls и файлы Microsoft.Z3.dll, которые находятся в папке x86, и вставляют их в один и тот же путь с кодом C#. – user1327010

В комментариях к предыдущим ответам на этот вопрос были сделаны ссылки на дистрибутив x86 и на дистрибутив x64, и я не уверен, что эта проблема решена. Чтобы уточнить:

При компиляции 64-битного двоичного файла (называемого x64 в визуальной студии) необходимо 64-разрядные версии z3.dll и Microsoft.Z3.dll. Они находятся в папке с именем x64 в дистрибутиве Z3. Обратите внимание, что это не зависит от реального компьютера, на котором работает Visual Studio.

При компиляции 32-битного двоичного файла необходимы DLL из каталога bin. Опять же, это не зависит от фактического компьютера, на котором работает Visual Studio.

Visual Studio может пересечь компиляции от 32 до 64 бит, и наоборот, то есть, можно скомпилировать двоичный файл для 32-битной архитектуры (так называемый x86 в отличие от x64) на 64-битной машины. Также возможно скомпилировать 64-битные двоичные файлы на 32-битной машине. В зависимости от того, какой компилятор компилируется, необходимо добавить правильный набор dll. Этот параметр имеет значение в конфигурации сборки вашего проекта в Visual Studio (сверху, обычно рядом с тем, где выбран режим отладки/выпуска). На этом этапе компиляции не имеет значения, на каком типе машины выполняется компиляция. Фактическая машина имеет значение только при попытке запустить 64-битный двоичный файл на 32-битной машине (но тогда сообщение об ошибке будет отличаться от сообщенного сообщения). Запуск 32-разрядных двоичных файлов на 64-битных машинах обычно работает нормально (но максимальное использование памяти программой будет ограничено).

Надеюсь, это помогло устранить некоторые путаницы!

Кроме того, мы согласны с тем, что комбинированное распределение, включающее обе версии, создает некоторую ненужную путаницу, поэтому в будущем мы рассмотрим возможность распространения отдельных инсталляторов для 32-разрядных и 64-разрядных двоичных файлов.

источник

2012-06-27 18:35:13

Ошибка при запуске Z3 в C#

ответ

Смежные вопросы