CODEWITHSUNDEEP
c#visual-studio-2012z3
jtony
jtony

Reputation: 101

C# Z3 API calling problems in Visual studio 2012

After I imported Z3 in the visual studio 2012, When I try to run a example in my visual studio 2012 , I found that the visual studio cannot find Microsoft.Z3 pakage, after I tried to import again it can find the Microsoft.Z3 but still it cannot find the Config keyword,Can anyboday help me ? or provide me a detailed way to use Z3 in Visual studio 2012? I followed the follwing steps and the above problem occured.

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

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

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.

My codes are as following:

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

                }

            }
        }
    }
}

Upvotes: 0

Views: 329

Answers (1)

Taylor T. Johnson
Taylor T. Johnson

Reputation: 2884

It looks like you are using a very outdated version of Z3 (3.2), the latest major release is 4.3.x, please follow the build instructions here to create the library (the unstable branch is probably the best choice):

http://z3.codeplex.com/SourceControl/latest#README

then make sure you add the library to the reference path in your solution/project (which it sounds like you've tried to do with the old library), then you can check this example to see how to call the API:

http://z3.codeplex.com/SourceControl/latest#examples/dotnet/Program.cs

Upvotes: 1

Related Questions