Несоответствующие версии DLL? - PullRequest
Новая
       4

Несоответствующие версии DLL?

1 голос
/ 18 июля 2011

Я пытаюсь использовать Z3 SMT solver для своих проектов.Однако, похоже, что существует несоответствие версий Visual Studio, которое вызвало мои проблемы.My Visual Studio 2008 сообщает, что

Не удалось найти указанный компонент «Microsoft.Z3».

, хотя он действительно находится в каталоге установки (C: \ ProgramФайлы \ Microsoft Research \ Z3-2.19 \ bin).

Когда проект компилируется, появляется другое предупреждение:

В разрешенном файле неверное изображение, нет метаданных или он недоступен по другим причинам.,Не удалось загрузить файл или сборку «C: \ Program Files \ Microsoft Research \ Z3-2.19 \ bin \ Microsoft.Z3.dll» или одну из ее зависимостей.Эта сборка создается средой выполнения, более новой, чем текущая загруженная среда, и не может быть загружена.

вместе с другими ошибками, указывающими, что связанные с Z3 типы как Context, Term и т. Д. Не найдены.

Это потому, что новые версии 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 я обнаружил, что последней версией Z3, которая использует dotNet Framework менее v4, является Z3 2.11;в этом случае я решаю использовать вместо обновления своего VS2008 на данный момент.

1 Ответ

1 голос
/ 18 июля 2011

Вероятно, это связано с тем, что вы ориентируетесь на более старую .NET Framework, чем библиотеки Z3. Например, если вы ориентированы на версию Z3 .NET 4, убедитесь, что вы создали ее в Visual Studio 2010 и нацелены на .NET Framework 4.0.

...