C# API for Z3 Installation

Question

Could anyone please help me using C# Api in Z3. I have no idea what to do :-(

I wrote the followiing program in 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();
                    }

                }

            }
        }
    }
 }

---

Following errors occured :

---

The type or namespace name 'Z3' does not exist in the namespace 'Microsoft' (are you missing an assembly reference?)

Thank you

Answer 1

Notice that:

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

is not the numeral 1, but is an uninterpreted constant, whose name is "1".

If you want a numeral, then use:

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

Answer 2

To use the Microsoft Z3 library in your C# projects follow these steps:

1. Go to http://research.microsoft.com/en-us/downloads/0a7db466-c2d7-4c51-8246-07e25900c7e7/ and download + install the Z3 package.

2. Switch to Visual Studio. In the Solution Explorer window right click on the References tree node and select "Add Reference".
   In the "Add new reference" dialog navigate to the Microsoft.Z3.dll. You find the Microsoft.Z3.dll under c:\Program Files (x86)\Microsoft Research\Z3-3.2\bin on a Windows x64 bit machine or under c:\Program Files\Microsoft Research\Z3-3.2\bin on a Windows x86 machine. To use Parallel Z3 library choose the Microsoft.Z3.dll from the c:\Program Files (x86)\Microsoft Research\Z3-3.2\bin_mt or c:\Program Files\Microsoft Research\Z3-3.2\bin_mt directory.

A few notes regarding your code:

There is no method called CheckAndModel() on the Context class. There is only a method called CheckAndGetModel(). Furthermore there is no overload for the MkConst() of the form

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

Instead use the following overload:

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