C # API для установки Z3

Question

Может ли кто-нибудь помочь мне с использованием C # Api в Z3. Понятия не имею, что делать: - (

Я написал следующую программу в Visual C # 2010 Express:

---

    using System;
    using System.Collections.Generic;
    using System.Linq;
    using System.Text; 
    using Microsoft.Z3;
    namespace ConsoleApplication1
    {
    class Program
    {
        static void Main(string[] args)
        {
            using (Config cfg = new Config()) {
                using (Context ctx = new Context(cfg)) {
                    Term x = ctx.MkConst("x", ctx.MkIntSort());
                    Term y = ctx.MkConst("y", ctx.MkIntSort());
                    Term zero = ctx.MkConst(0, ctx.MkIntSort());
                    Term one = ctx.MkConst(1, ctx.MkIntSort());
                    Term three = ctx.MkConst(3, ctx.MkIntSort());
                    Term fml = x > zero & ctx.MkEq(y, x + one) & y < three;
                    ctx.AssertCnstr(fml);
                    Model m = null;
                    LBool is_sat = ctx.CheckAndModel(out m);
                    System.Console.WriteLine(is_sat);

                    if (m != null)
                    {
                     m.Display(Console.Out);
                     m.Dispose();
                    }

                }

            }
        }
    }
 }

---

Произошли следующие ошибки:

---

Тип или имя пространства имен 'Z3' не существует в пространстве имен 'Microsoft' (отсутствует ссылка на сборку?)

Спасибо

Answer 1

Чтобы использовать библиотеку Microsoft Z3 в своих проектах на C #, выполните следующие действия:

1. Перейдите на http://research.microsoft.com/en-us/downloads/0a7db466-c2d7-4c51-8246-07e25900c7e7/ и загрузите + установите пакет Z3.

2. Переключиться на Visual Studio.В окне обозревателя решений щелкните правой кнопкой мыши узел дерева ссылок и выберите «Добавить ссылку».
   В диалоговом окне «Добавить новую ссылку» перейдите к файлу Microsoft.Z3.dll.Microsoft.Z3.dll находится под c:\Program Files (x86)\Microsoft Research\Z3-3.2\bin на компьютере с 64-разрядной версией Windows или под c:\Program Files\Microsoft Research\Z3-3.2\bin на компьютере под управлением Windows x86.Чтобы использовать библиотеку Parallel Z3, выберите Microsoft.Z3.dll из каталога c:\Program Files (x86)\Microsoft Research\Z3-3.2\bin_mt или c:\Program Files\Microsoft Research\Z3-3.2\bin_mt.

Несколько замечаний относительно вашего кода:

Существуетнет метода с именем CheckAndModel() в классе Context.Существует только метод с именем CheckAndGetModel().Кроме того, нет перегрузки для MkConst() формы

ctx.MkConst(1, ctx.MkIntSort());

Вместо этого используйте следующую перегрузку:

ctx.MkConst("1", ctx.MkIntSort());

Answer 2

Обратите внимание, что:

ctx.MkConst("1", ctx.MkIntSort());

- это не цифра 1, а неинтерпретированная константа, имя которой равно "1".

Если вы хотите цифру, используйте:

ctx.MkNumeral(1, ctx.MkIntSort());