CODEWITHSUNDEEP
c#z3
user1327010
user1327010

Reputation: 21

Referencing Z3 from a C# Application

I am trying to run this Z3 code in C#, but there are lots of errors such as:

I ran Z3 and included it inside my program file, so how can this code work and are there any .NET references required?

class Program
{
    static void Main(string[] args)
    {
        {
            Console.WriteLine("prove_example1");
            mk_context();
            /* create uninterpreted type. */
            Sort U = z3.MkSort("U");
            /* declare function g */
            FuncDecl g = z3.MkFuncDecl("g", U, U);
            /* create x and y */
            Term x = z3.MkConst("x", U);
            Term y = z3.MkConst("y", U);
            /* create g(x), g(y) */
            Term gx = mk_unary_app(g, x);
            Term gy = mk_unary_app(g, y);
            /* assert x = y */
            Term eq = z3.MkEq(x, y);
            z3.AssertCnstr(eq);
            /* prove g(x) = g(y) */
            Term f = z3.MkEq(gx, gy);
            Console.WriteLine("prove: x = y implies g(x) = g(y)");
            prove(f);
            /* create g(g(x)) */
            Term ggx = mk_unary_app(g, gx);
           /* disprove g(g(x)) = g(y) */
            f = z3.MkEq(ggx, gy);
            Console.WriteLine("disprove: x = y implies g(g(x)) = g(y)");
            prove(f);
           /* Print the model using the custom model printer */
            z3.AssertCnstr(z3.MkNot(f));
            check2(LBool.True);
        }
    }
}
}

Upvotes: 1

Views: 460

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

It seems you copied this code fragment from an old Z3 C# API example. The original example had a field Context z3;. It also had several auxiliary methods: mk_context, prove, mk_unary_app, etc. You will not be able to compile your example without copying these additional methods. Moreover, this example is using the old C# API. Z3 4.0 has a new C# API. It is much easier to use. I suggest you switch to Z3 4.0 (if you are not already using it). The Z3 4.0 distribution has a directory called examples\dotnet. This directory contains a big example called Program.cs, and a batch file build.bat to build/compile it. This example demonstrates how to use the Z3 C# API. The following link contains a reference manual for the Z3 C# API: http://research.microsoft.com/en-us/um/redmond/projects/z3/class_microsoft_1_1_z3_1_1_context.html

Upvotes: 2

Related Questions