TestManaged Class Reference
[Managed (.NET) API examples]

Class encapsulating Z3 tests. More...

Public Member Functions
void	mk_context ()
	Create a logical context with model construction enabled.
Sort	mk_int_type ()
	Create an integer type.
Sort	mk_bv_type (uint num_bytes)
	Create a bit-vector type.
Term	mk_var (string name, Sort ty)
	Create a variable using the given name and type.
Term	mk_bool_var (string name)
	Create a boolean variable using the given name.
Term	mk_int_var (string name)
	Create an integer variable using the given name.
Term	mk_bv_var (string name, uint num_bytes)
	Create a bit-vector variable using the given name.
void	check (LBool expected_result, out Model model)
	Check whether the logical context is satisfiable, and compare the result with the expected result. If the context is satisfiable, then display the model.
void	check2 (LBool expected_result)
	Similar to check, but uses display_model instead of Z3's native display method.
void	prove (Term f)
	Prove that the constraints already asserted into the logical context implies the given formula. The result of the proof is displayed.
void	prove2 (Term f, bool is_valid)
	Prove that the constraints already asserted into the logical context implies the given formula. The result of the proof is displayed.
void	assert_inj_axiom (FuncDecl f, int i)
	Assert the axiom: function f is injective in the i-th argument.
void	assert_inj_axiom_abs (FuncDecl f, int i)
	Assert the axiom: function f is injective in the i-th argument.
void	simple_example ()
	"Hello world" example: create a Z3 logical context, and delete it.
void	find_model_example1 ()
	Find a model for x xor y.
void	find_model_example2 ()
	Find a model for x < y + 1, x > 2. Then, assert not(x = y), and find another model.
void	prove_example1 ()
	Prove x = y implies g(x) = g(y), and disprove x = y implies g(g(x)) = g(y).
void	prove_example2 ()
	Prove not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0 . Then, show that z < -1 is not implied.
void	push_pop_example1 ()
	Show how push & pop can be used to create "backtracking" points.
void	quantifier_example1 ()
	Prove that f(x, y) = f(w, v) implies y = v when f is injective in the second argument.
void	quantifier_example1_abs ()
	Prove that f(x, y) = f(w, v) implies y = v when f is injective in the second argument.
void	array_example1 ()
	Prove store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3)).
void	array_example2 ()
	Show that distinct(a_0, ... , a_n) is unsatisfiable when a_i's are arrays from boolean to boolean and n > 4.
void	tuple_example ()
	Tuples.
void	bitvector_example1 ()
	Simple bit-vector example. This example disproves that x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers.
void	bitvector_example2 ()
	Find x and y such that: x ^ y - 103 == x * y.
void	injective_example ()
	Injective functions.
void	parser_example1 ()
	Demonstrates how to use the SMTLIB parser.
void	parser_example2 ()
	Demonstrates how to initialize the parser symbol table.
void	parser_example3 ()
	Demonstrates how to initialize the parser symbol table.
void	parser_example4 ()
	Display the declarations, assumptions and formulas in a SMT-LIB string.
void	parser_example5 ()
	Demonstrates how to handle parser errors using Z3 error handling support.
void	ite_example ()
	Create an ite-term (if-then-else terms).
void	enum_example ()
	Create an enumeration data type.
void	list_example ()
	Create a list datatype.
void	tree_example ()
	Create a binary tree datatype.
void	forest_example ()
	Create a forest of trees.
void	eval_example1 ()
	Demonstrate how to use Eval.
void	eval_example2 ()
	Demonstrate how to use Eval on tuples.
void	check_small (Term[] to_minimize)
	Demonstrate how to use Push and Pop to control the size of models.
void	find_small_model_example ()
	Reduced-size model generation example.
void	simplifier_example ()
	Simplifier example.
void	unsat_core_and_proof_example ()
	Extract unsatisfiable core example.
void	get_implied_equalities_example ()
	Extract implied equalities.

---

Detailed Description

Class encapsulating Z3 tests.

Definition at line 13 of file test_managed.cs.

---

Member Function Documentation

void array_example1

(

)

[inline]

Prove store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3)).

This example demonstrates how to use the array theory.

Definition at line 830 of file test_managed.cs.

    {

        Console.WriteLine("array_example1");

        mk_context();

        Sort int_type = mk_int_type();
        Sort array_type = z3.MkArraySort(int_type, int_type);

        Term a1 = mk_var("a1", array_type);
        Term a2 = mk_var("a2", array_type);
        Term i1 = mk_var("i1", int_type);
        Term i2 = mk_var("i2", int_type);
        Term i3 = mk_var("i3", int_type);
        Term v1 = mk_var("v1", int_type);
        Term v2 = mk_var("v2", int_type);

        Term st1 = z3.MkArrayStore(a1, i1, v1);
        Term st2 = z3.MkArrayStore(a2, i2, v2);

        Term sel1 = z3.MkArraySelect(a1, i3);
        Term sel2 = z3.MkArraySelect(a2, i3);

        /* create antecedent */
        Term antecedent = z3.MkEq(st1, st2);

        /* create consequent: i1 = i3 or  i2 = i3 or select(a1, i3) = select(a2, i3) */
        Term consequent = z3.MkOr(new Term[] { z3.MkEq(i1, i3), z3.MkEq(i2, i3), z3.MkEq(sel1, sel2) });

        /* prove store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3)) */
        Term thm = z3.MkImplies(antecedent, consequent);
        Console.WriteLine("prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))");
        Console.WriteLine("{0}", z3.ToString(thm));
        prove(thm);
    }

void array_example2

(

)

[inline]

Show that distinct(a_0, ... , a_n) is unsatisfiable when a_i's are arrays from boolean to boolean and n > 4.

This example also shows how to use the distinct construct.

Definition at line 873 of file test_managed.cs.

    {
        Console.WriteLine("array_example2");

        for (int n = 2; n <= 5; n++)
        {
            Console.WriteLine("n = {0}", n);
            mk_context();

            if (n == 3)
            {
                z3.OpenLog("array3.z3");
            }
            Sort bool_type = z3.MkBoolSort();
            Sort array_type = z3.MkArraySort(bool_type, bool_type);
            Term[] a = new Term[n];

            /* create arrays */
            for (int i = 0; i < n; i++)
            {
                a[i] = z3.MkConst(String.Format("array_{0}", i), array_type);
            }

            /* assert distinct(a[0], ..., a[n]) */
            Term d = z3.MkDistinct(a);
            Console.WriteLine("{0}", z3.ToString(d));
            z3.AssertCnstr(d);

            /* context is satisfiable if n < 5 */
            Model model = null;
            check(n < 5 ? LBool.True : LBool.False, out model);
            if (n < 5)
            {
                for (int i = 0; i < n; i++)
                {
                    Console.WriteLine("{0} = {1}",
                                      z3.ToString(a[i]),
                                      z3.ToString(model.Eval(a[i])));
                }
            }
            if (model != null)
            {
                model.Dispose();
            }
        }
    }

void assert_inj_axiom	(	FuncDecl	f,
		int	i
	)			[inline]

Assert the axiom: function f is injective in the i-th argument.

The following axiom is asserted into the logical context:

       forall (x_0, ..., x_n) finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i

Where, finv is a fresh function declaration.

Definition at line 312 of file test_managed.cs.

Referenced by quantifier_example1().

    {
        Sort[] domain = z3.GetDomain(f);
        uint sz = (uint)domain.Length;

        if (i >= sz)
        {
            Console.WriteLine("failed to create inj axiom");
            return;
        }

        /* declare the i-th inverse of f: finv */
        Sort finv_domain = z3.GetRange(f);
        Sort finv_range = domain[i];
        FuncDecl finv = z3.MkFuncDecl("f_fresh", finv_domain, finv_range);

        /* allocate temporary arrays */
        Term[] xs = new Term[sz];
        Symbol[] names = new Symbol[sz];
        Sort[] types = new Sort[sz];

        /* fill types, names and xs */

        for (uint j = 0; j < sz; j++)
        {
            types[j] = domain[j];
            names[j] = z3.MkSymbol(String.Format("x_{0}", j));
            xs[j] = z3.MkBound(j, types[j]);
        }
        Term x_i = xs[i];

        /* create f(x_0, ..., x_i, ..., x_{n-1}) */
        Term fxs = z3.MkApp(f, xs);

        /* create f_inv(f(x_0, ..., x_i, ..., x_{n-1})) */
        Term finv_fxs = mk_unary_app(finv, fxs);

        /* create finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i */
        Term eq = z3.MkEq(finv_fxs, x_i);

        /* use f(x_0, ..., x_i, ..., x_{n-1}) as the pattern for the quantifier */
        Pattern p = z3.MkPattern(new Term[] { fxs });
        Console.WriteLine("pattern {0}", z3.ToString(p));

        /* create & assert quantifier */
        Term q = z3.MkForall(
            0, /* using default weight */
            new Pattern[] { p }, /* patterns */
            types, /* types of quantified variables */
            names, /* names of quantified variables */
            eq);

        Console.WriteLine("assert axiom {0}", z3.ToString(q));
        z3.AssertCnstr(q);

    }

void assert_inj_axiom_abs	(	FuncDecl	f,
		int	i
	)			[inline]

Assert the axiom: function f is injective in the i-th argument.

The following axiom is asserted into the logical context:

       forall (x_0, ..., x_n) finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i

Where, finv is a fresh function declaration.

Definition at line 379 of file test_managed.cs.

Referenced by quantifier_example1_abs().

    {
        Sort[] domain = z3.GetDomain(f);
        uint sz = (uint)domain.Length;

        if (i >= sz)
        {
            Console.WriteLine("failed to create inj axiom");
            return;
        }

        /* declare the i-th inverse of f: finv */
        Sort finv_domain = z3.GetRange(f);
        Sort finv_range = domain[i];
        FuncDecl finv = z3.MkFuncDecl("f_fresh", finv_domain, finv_range);

        /* allocate temporary arrays */
        Term[] xs = new Term[sz];

        /* fill types, names and xs */

        for (uint j = 0; j < sz; j++)
        {
            xs[j] = z3.MkConst(String.Format("x_{0}", j), domain[j]);
        }
        Term x_i = xs[i];

        /* create f(x_0, ..., x_i, ..., x_{n-1}) */
        Term fxs = z3.MkApp(f, xs);

        /* create f_inv(f(x_0, ..., x_i, ..., x_{n-1})) */
        Term finv_fxs = mk_unary_app(finv, fxs);

        /* create finv(f(x_0, ..., x_i, ..., x_{n-1})) = x_i */
        Term eq = z3.MkEq(finv_fxs, x_i);

        /* use f(x_0, ..., x_i, ..., x_{n-1}) as the pattern for the quantifier */
        Pattern p = z3.MkPattern(new Term[] { fxs });
        Console.WriteLine("pattern {0}", z3.ToString(p));

        /* create & assert quantifier */
        Term q = z3.MkForall(
            0, /* using default weight */
            xs,    /* the list of bound variables */
            new Pattern[] { p }, /* patterns */
            eq);

        Console.WriteLine("assert axiom {0}", z3.ToString(q));
        z3.AssertCnstr(q);

    }

void bitvector_example1

(

)

[inline]

Simple bit-vector example. This example disproves that x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers.

Definition at line 952 of file test_managed.cs.

    {
        Console.WriteLine("\nbitvector_example1");

        mk_context();

        Sort bv_type = z3.MkBvSort(32);
        Term x = mk_var("x", bv_type);
        Term zero = z3.MkNumeral("0", bv_type);
        Term ten = z3.MkNumeral("10", bv_type);
        Term x_minus_ten = z3.MkBvSub(x, ten);
        /* bvsle is signed less than or equal to */
        Term c1 = z3.MkBvSle(x, ten);
        Term c2 = z3.MkBvSle(x_minus_ten, zero);
        Term thm = z3.MkIff(c1, c2);
        Console.WriteLine("disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers");
        prove(thm);
    }

void bitvector_example2

(

)

[inline]

Find x and y such that: x ^ y - 103 == x * y.

Definition at line 974 of file test_managed.cs.

    {
        mk_context();

        /* construct x ^ y - 103 == x * y */
        Sort bv_type = z3.MkBvSort(32);
        Term x = mk_var("x", bv_type);
        Term y = mk_var("y", bv_type);
        Term x_xor_y = z3.MkBvXor(x, y);
        Term c103 = z3.MkNumeral("103", bv_type);
        Term lhs = z3.MkBvSub(x_xor_y, c103);
        Term rhs = z3.MkBvMul(x, y);
        Term ctr = z3.MkEq(lhs, rhs);

        Console.WriteLine("\nbitvector_example2");
        Console.WriteLine("find values of x and y, such that x ^ y - 103 == x * y");

        /* add the constraint <tt>x ^ y - 103 == x * y<\tt> to the logical context */
        z3.AssertCnstr(ctr);

        /* find a model (i.e., values for x an y that satisfy the constraint */
        check2(LBool.True);
    }

void check	(	LBool	expected_result,
		out Model	model
	)			[inline]

Check whether the logical context is satisfiable, and compare the result with the expected result. If the context is satisfiable, then display the model.

Definition at line 119 of file test_managed.cs.

Referenced by array_example2(), find_model_example1(), find_model_example2(), and push_pop_example1().

    {
        LBool result = z3.CheckAndGetModel(out model);
        switch (result)
        {
            case LBool.False:
                Console.WriteLine("unsat");
                break;
            case LBool.Undef:
                Console.WriteLine("unknown");
                break;
            case LBool.True:
                Console.WriteLine("sat");
                model.Display(Console.Out);
                break;
        }
        if (result != expected_result)
        {
            Console.WriteLine("BUG: unexpected result");
        }
    }

void check2

(

LBool

expected_result

)

[inline]

Similar to check, but uses display_model instead of Z3's native display method.

Definition at line 144 of file test_managed.cs.

Referenced by bitvector_example2(), parser_example1(), parser_example2(), prove_example1(), and push_pop_example1().

    {
        Model model = null;
        LBool result = z3.CheckAndGetModel(out model);
        switch (result)
        {
            case LBool.False:
                Console.WriteLine("unsat");
                break;
            case LBool.Undef:
                Console.WriteLine("unknown");
                break;
            case LBool.True:
                Console.WriteLine("sat");
                display_model(Console.Out, model);
                break;
        }
        if (result != expected_result)
        {
            Console.WriteLine("BUG: unexpected result");
        }
        if (model != null)
        {
            model.Dispose();
        }
    }

void check_small

(

Term[]

to_minimize

)

[inline]

Demonstrate how to use Push and Pop to control the size of models.

Note: this test is specialized to 32-bit bitvectors.

Definition at line 1547 of file test_managed.cs.

    {

        Sort bv32 = mk_bv_type(32);

        int num_terms = to_minimize.Length;
        UInt32[] upper = new UInt32[num_terms];
        UInt32[] lower = new UInt32[num_terms];
        Term[] values = new Term[num_terms];
        for (int i = 0; i < upper.Length; ++i)
        {
            upper[i] = UInt32.MaxValue;
            lower[i] = 0;
        }
        bool some_work = true;
        int last_index = -1;
        UInt32 last_upper = 0;
        while (some_work)
        {
            z3.Push();

            bool check_is_sat = true;
            while (check_is_sat && some_work)
            {
                // Assert all feasible bounds.
                for (int i = 0; i < num_terms; ++i)
                {
                    z3.AssertCnstr(z3.MkBvUle(to_minimize[i], mk_bv32(upper[i])));
                }
                Model model = null;
                check_is_sat = LBool.True == z3.CheckAndGetModel(out model);
                if (!check_is_sat)
                {
                    if (last_index != -1)
                    {
                        lower[last_index] = last_upper + 1;
                    }
                    if (model != null)
                    {
                        model.Dispose();
                    }
                    break;
                }
                model.Display(Console.Out);

                // narrow the bounds based on the current model.
                for (int i = 0; i < num_terms; ++i)
                {
                    Term v = model.Eval(to_minimize[i]);
                    UInt64 ui = z3.GetNumeralUInt64(v);
                    if (ui < upper[i])
                    {
                        upper[i] = (UInt32)ui;
                    }
                    Console.WriteLine("{0} {1} {2}", i, lower[i], upper[i]);
                }
                model.Dispose();
                // find a new bound to add
                some_work = false;
                last_index = 0;
                for (int i = 0; i < num_terms; ++i)
                {
                    if (lower[i] < upper[i])
                    {
                        last_upper = (upper[i] + lower[i]) / 2;
                        last_index = i;
                        z3.AssertCnstr(z3.MkBvUle(to_minimize[i], mk_bv32(last_upper)));
                        some_work = true;
                        break;
                    }
                }
            }
            z3.Pop();
        }
    }

void enum_example

(

)

[inline]

Create an enumeration data type.

Definition at line 1176 of file test_managed.cs.

    {
        mk_context();
        Symbol name = z3.MkSymbol("fruit");

        FuncDecl[] enum_consts = new FuncDecl[3];
        FuncDecl[] enum_testers = new FuncDecl[3];

        Console.WriteLine("\nenum_example");


        Sort fruit = z3.MkEnumerationSort("fruit", new string[] { "apple", "banana", "orange" }, enum_consts, enum_testers);

        Console.WriteLine("{0}", (enum_consts[0]));
        Console.WriteLine("{0}", (enum_consts[1]));
        Console.WriteLine("{0}", (enum_consts[2]));

        Console.WriteLine("{0}", (enum_testers[0]));
        Console.WriteLine("{0}", (enum_testers[1]));
        Console.WriteLine("{0}", (enum_testers[2]));

        Term apple = z3.MkConst(enum_consts[0]);
        Term banana = z3.MkConst(enum_consts[1]);
        Term orange = z3.MkConst(enum_consts[2]);

        /* Apples are different from oranges */
        prove2(z3.MkNot(z3.MkEq(apple, orange)), true);

        /* Apples pass the apple test */
        prove2(z3.MkApp(enum_testers[0], apple), true);

        /* Oranges fail the apple test */
        prove2(z3.MkApp(enum_testers[0], orange), false);
        prove2(z3.MkNot(z3.MkApp(enum_testers[0], orange)), true);

        Term fruity = mk_var("fruity", fruit);

        /* If something is fruity, then it is an apple, banana, or orange */

        prove2(z3.MkOr(new Term[] { z3.MkEq(fruity, apple), z3.MkEq(fruity, banana), z3.MkEq(fruity, orange) }), true);
    }

void eval_example1

(

)

[inline]

Demonstrate how to use Eval.

Definition at line 1460 of file test_managed.cs.

    {
        Console.WriteLine("\neval_example1");
        mk_context();
        Term x = mk_int_var("x");
        Term y = mk_int_var("y");
        Term two = mk_int(2);

        /* assert x < y */
        z3.AssertCnstr(z3.MkLt(x, y));

        /* assert x > 2 */
        z3.AssertCnstr(z3.MkGt(x, two));

        /* find model for the constraints above */
        Model model = null;
        if (LBool.True == z3.CheckAndGetModel(out model))
        {
            model.Display(Console.Out);
            Console.WriteLine("\nevaluating x+y");
            Term v = model.Eval(z3.MkAdd(x, y));
            if (v != null)
            {
                Console.WriteLine("result = {0}", z3.ToString(v));
            }
            else
            {
                Console.WriteLine("Failed to evaluate: x+y");
            }
            model.Dispose();
        }
        else
        {
            Console.WriteLine("BUG, the constraints are satisfiable.");
        }
    }

void eval_example2

(

)

[inline]

Demonstrate how to use Eval on tuples.

Definition at line 1500 of file test_managed.cs.

    {
        Console.WriteLine("\neval_example2");
        mk_context();
        Sort int_type = mk_int_type();
        FuncDecl[] decls = new FuncDecl[2];
        FuncDecl mk_tuple = null;
        Sort tuple = z3.MkTupleSort
        (
         z3.MkSymbol("mk_tuple"),                        // name of tuple constructor
         new Symbol[] { z3.MkSymbol("first"), z3.MkSymbol("second") },    // names of projection operators
         new Sort[] { int_type, int_type }, // types of projection operators
         out mk_tuple,
         decls                              // return declarations.
            );
        FuncDecl first = decls[0];     // declarations are for projections
        FuncDecl second = decls[1];
        Term tup1 = z3.MkConst("t1", tuple);
        Term tup2 = z3.MkConst("t2", tuple);
        /* assert tup1 != tup2 */
        z3.AssertCnstr(z3.MkNot(z3.MkEq(tup1, tup2)));
        /* assert first tup1 = first tup2 */
        z3.AssertCnstr(z3.MkEq(z3.MkApp(first, tup1), z3.MkApp(first, tup2)));

        /* find model for the constraints above */
        Model model = null;
        if (LBool.True == z3.CheckAndGetModel(out model))
        {
            model.Display(Console.Out);
            Console.WriteLine("evaluating tup1 {0}", z3.ToString(model.Eval(tup1)));
            Console.WriteLine("evaluating tup2 {0}", z3.ToString(model.Eval(tup2)));
            Console.WriteLine("evaluating second(tup2) {0}",
                      z3.ToString(model.Eval(z3.MkApp(second, tup2))));
            model.Dispose();
        }
        else
        {
            Console.WriteLine("BUG, the constraints are satisfiable.");
        }
    }

void find_model_example1

(

)

[inline]

Find a model for x xor y.

Definition at line 485 of file test_managed.cs.

    {
        Console.WriteLine("find_model_example1");

        mk_context();

        Term x = mk_bool_var("x");
        Term y = mk_bool_var("y");
        Term x_xor_y = z3.MkXor(x, y);

        z3.AssertCnstr(x_xor_y);

        Console.WriteLine("model for: x xor y");
        Model model = null;
        check(LBool.True, out model);
        Console.WriteLine("x = {0}, y = {1}",
                          z3.ToString(model.Eval(x)),
                      z3.ToString(model.Eval(y)));
        model.Dispose();
    }

void find_model_example2

(

)

[inline]

Find a model for x < y + 1, x > 2. Then, assert not(x = y), and find another model.

Definition at line 510 of file test_managed.cs.

    {
        Console.WriteLine("find_model_example2");

        mk_context();
        Term x = mk_int_var("x");
        Term y = mk_int_var("y");
        Term one = mk_int(1);
        Term two = mk_int(2);

        Term y_plus_one = z3.MkAdd(y, one);

        Term c1 = z3.MkLt(x, y_plus_one);
        Term c2 = z3.MkGt(x, two);

        z3.AssertCnstr(c1);
        z3.AssertCnstr(c2);

        Console.WriteLine("model for: x < y + 1, x > 2");
        Model model = null;
        check(LBool.True, out model);
        Console.WriteLine("x = {0}, y = {1}",
                          z3.ToString(model.Eval(x)),
                          z3.ToString(model.Eval(y)));
        model.Dispose();
        model = null;

        /* assert not(x = y) */
        Term x_eq_y = z3.MkEq(x, y);
        Term c3 = z3.MkNot(x_eq_y);
        z3.AssertCnstr(c3);

        Console.WriteLine("model for: x < y + 1, x > 2, not(x = y)");
        check(LBool.True, out model);
        Console.WriteLine("x = {0}, y = {1}",
                          z3.ToString(model.Eval(x)),
                          z3.ToString(model.Eval(y)));
        model.Dispose();
    }

void find_small_model_example

(

)

[inline]

Reduced-size model generation example.

Definition at line 1626 of file test_managed.cs.

    {
        mk_context();
        Term x = mk_bv_var("x", 32);
        Term y = mk_bv_var("y", 32);
        Term z = mk_bv_var("z", 32);
        Sort bv32 = mk_bv_type(32);
        z3.AssertCnstr(z3.MkBvUle(x, z3.MkBvAdd(y, z)));
        check_small(new Term[] { x, y, z });
    }

void forest_example

(

)

[inline]

Create a forest of trees.

forest ::= nil | cons(tree, forest) tree ::= nil | cons(forest, forest)

Definition at line 1351 of file test_managed.cs.

    {
        mk_context();
        Sort tree, forest;
        FuncDecl nil1_decl, is_nil1_decl, cons1_decl, is_cons1_decl, car1_decl, cdr1_decl;
        FuncDecl nil2_decl, is_nil2_decl, cons2_decl, is_cons2_decl, car2_decl, cdr2_decl;
        Term nil1, nil2, t1, t2, t3, t4, f1, f2, f3, l1, l2, x, y, u, v;

        //
        // Declare the names of the accessors for cons.
        // Then declare the sorts of the accessors. 
        // For this example, all sorts refer to the new types 'forest' and 'tree'
        // being declared, so we pass in null for both sorts1 and sorts2.
        // On the other hand, the sort_refs arrays contain the indices of the
        // two new sorts being declared. The first element in sort1_refs
        // points to 'tree', which has index 1, the second element in sort1_refs array
        // points to 'forest', which has index 0.
        // 
        string[] head_tail1 = new string[] { "head", "tail" };
        Sort[] sorts1 = new Sort[] { null, null };
        uint[] sort1_refs = new uint[] { 1, 0 }; // the first item points to a tree, the second to a forest

        string[] head_tail2 = new string[] { "car", "cdr" };
        Sort[] sorts2 = new Sort[] { null, null };
        uint[] sort2_refs = new uint[] { 0, 0 }; // both items point to the forest datatype.
        Constructor nil1_con, cons1_con, nil2_con, cons2_con;
        Constructor[] constructors1 = new Constructor[2], constructors2 = new Constructor[2];
        string[] sort_names = { "forest", "tree" };

        Console.WriteLine("\nforest_example");

        /* build a forest */
        nil1_con = z3.MkConstructor("nil", "is_nil", null, null, null);
        cons1_con = z3.MkConstructor("cons1", "is_cons1", head_tail1, sorts1, sort1_refs);
        constructors1[0] = nil1_con;
        constructors1[1] = cons1_con;

        /* build a tree */
        nil2_con = z3.MkConstructor("nil2", "is_nil2", null, null, null);
        cons2_con = z3.MkConstructor("cons2", "is_cons2", head_tail2, sorts2, sort2_refs);
        constructors2[0] = nil2_con;
        constructors2[1] = cons2_con;


        Constructor[][] clists = new Constructor[][] { constructors1, constructors2 };

        Sort[] sorts = z3.MkDataTypes(sort_names, clists);
        forest = sorts[0];
        tree = sorts[1];

        //
        // Now that the datatype has been created.
        // Query the constructors for the constructor
        // functions, testers, and field accessors.
        //
        nil1_decl = z3.GetConstructor(nil1_con);
        is_nil1_decl = z3.GetTester(nil1_con);
        cons1_decl = z3.GetConstructor(cons1_con);
        is_cons1_decl = z3.GetTester(cons1_con);
        FuncDecl[] cons1_accessors = z3.GetAccessors(cons1_con);
        car1_decl = cons1_accessors[0];
        cdr1_decl = cons1_accessors[1];

        nil2_decl = z3.GetConstructor(nil2_con);
        is_nil2_decl = z3.GetTester(nil2_con);
        cons2_decl = z3.GetConstructor(cons2_con);
        is_cons2_decl = z3.GetTester(cons2_con);
        FuncDecl[] cons2_accessors = z3.GetAccessors(cons2_con);
        car2_decl = cons2_accessors[0];
        cdr2_decl = cons2_accessors[1];


        nil1 = z3.MkConst(nil1_decl);
        nil2 = z3.MkConst(nil2_decl);
        f1 = mk_binary_app(cons1_decl, nil2, nil1);
        t1 = mk_binary_app(cons2_decl, nil1, nil1);
        t2 = mk_binary_app(cons2_decl, f1, nil1);
        t3 = mk_binary_app(cons2_decl, f1, f1);
        t4 = mk_binary_app(cons2_decl, nil1, f1);
        f2 = mk_binary_app(cons1_decl, t1, nil1);
        f3 = mk_binary_app(cons1_decl, t1, f1);


        /* nil != cons(nil,nil) */
        prove2(z3.MkNot(z3.MkEq(nil1, f1)), true);
        prove2(z3.MkNot(z3.MkEq(nil2, t1)), true);


        /* cons(x,u) = cons(x, v) => u = v */
        u = mk_var("u", forest);
        v = mk_var("v", forest);
        x = mk_var("x", tree);
        y = mk_var("y", tree);
        l1 = mk_binary_app(cons1_decl, x, u);
        l2 = mk_binary_app(cons1_decl, y, v);
        prove2(z3.MkImplies(z3.MkEq(l1, l2), z3.MkEq(u, v)), true);
        prove2(z3.MkImplies(z3.MkEq(l1, l2), z3.MkEq(x, y)), true);

        /* is_nil(u) or is_cons(u) */
        prove2(z3.MkOr(z3.MkApp(is_nil1_decl, u), z3.MkApp(is_cons1_decl, u)), true);

        /* occurs check u != cons(x,u) */
        prove2(z3.MkNot(z3.MkEq(u, l1)), true);
    }

void get_implied_equalities_example

(

)

[inline]

Extract implied equalities.

Definition at line 1711 of file test_managed.cs.

                                                 {
        if (this.z3 != null)
        {
            this.z3.Dispose();
        }
        Config p = new Config();
        p.SetParamValue("ARITH_PROPAGATE_EXPENSIVE_EQS","true");
        p.SetParamValue("ARITH_EQ_BOUNDS","true");
        this.z3 = new Context(p);
        p.Dispose();

        Sort int_sort = z3.MkIntSort();
        Term a = mk_int_var("a");
        Term b = mk_int_var("b");
        Term c = mk_int_var("c");
        Term d = mk_int_var("d");
        FuncDecl f = z3.MkFuncDecl("f", int_sort, int_sort);
        Term fa = z3.MkApp(f,a);
        Term fb = z3.MkApp(f,b);
        Term fc = z3.MkApp(f,c);
        Term[] terms = new Term[]{ a, b, c, d, fa, fb, fc };
        uint[] class_ids;

        z3.AssertCnstr(z3.MkEq(a, b));
        z3.AssertCnstr(z3.MkEq(b, c));
        z3.AssertCnstr(z3.MkLe(fc, a));
        z3.AssertCnstr(z3.MkLe(b, fb));
        int num_terms = terms.Length;

        z3.GetImpliedEqualities(terms, out class_ids);
        for (int i = 0; i < num_terms; ++i) {
            Console.WriteLine("Class {0} |-> {1}", terms[i], class_ids[i]);
        }
    }

void injective_example

(

)

[inline]

Injective functions.

Check that the projection of a tuple returns the corresponding element.

Definition at line 1003 of file test_managed.cs.

    {
        mk_context();
        Sort int_type = mk_int_type();
        FuncDecl f = z3.MkInjectiveFunction("f_inj", new Sort[] { int_type }, int_type);
        Term x = z3.MkConst("x", int_type);
        Term y = z3.MkConst("y", int_type);
        Term fx = z3.MkApp(f, x);
        Term f_y = z3.MkApp(f, y);
        Term c = z3.MkImplies(z3.MkEq(fx, f_y), z3.MkEq(x, y));
        Console.WriteLine("Injective example: {0}", z3.ToString(c));
        prove(c);
    }

void ite_example

(

)

[inline]

Create an ite-term (if-then-else terms).

Definition at line 1160 of file test_managed.cs.

    {
        Console.WriteLine("\nite_example");
        mk_context();

        Term f = z3.MkFalse();
        Term one = mk_int(1);
        Term zero = mk_int(0);
        Term ite = z3.MkIte(f, one, zero);

        Console.WriteLine("term: {0}", ite);
    }

void list_example

(

)

[inline]

Create a list datatype.

Definition at line 1222 of file test_managed.cs.

    {
        mk_context();

        Sort int_ty, int_list;
        FuncDecl nil_decl, is_nil_decl, cons_decl, is_cons_decl, head_decl, tail_decl;
        Term nil, l1, l2, x, y, u, v, fml, fml1;

        Console.WriteLine("\nlist_example");

        int_ty = z3.MkIntSort();

        int_list = z3.MkListSort("int_list", int_ty,
                     out nil_decl, out is_nil_decl, out cons_decl, out is_cons_decl, out head_decl, out tail_decl);

        nil = z3.MkConst(nil_decl);
        l1 = mk_binary_app(cons_decl, mk_int(1), nil);
        l2 = mk_binary_app(cons_decl, mk_int(2), nil);

        /* nil != cons(1, nil) */
        prove2(z3.MkNot(z3.MkEq(nil, l1)), true);

        /* cons(2,nil) != cons(1, nil) */
        prove2(z3.MkNot(z3.MkEq(l1, l2)), true);

        /* cons(x,nil) = cons(y, nil) => x = y */
        x = mk_var("x", int_ty);
        y = mk_var("y", int_ty);
        l1 = mk_binary_app(cons_decl, x, nil);
        l2 = mk_binary_app(cons_decl, y, nil);
        prove2(z3.MkImplies(z3.MkEq(l1, l2), z3.MkEq(x, y)), true);

        /* cons(x,u) = cons(x, v) => u = v */
        u = mk_var("u", int_list);
        v = mk_var("v", int_list);
        l1 = mk_binary_app(cons_decl, x, u);
        l2 = mk_binary_app(cons_decl, y, v);
        prove2(z3.MkImplies(z3.MkEq(l1, l2), z3.MkEq(u, v)), true);
        prove2(z3.MkImplies(z3.MkEq(l1, l2), z3.MkEq(x, y)), true);

        /* is_nil(u) or is_cons(u) */
        prove2(z3.MkOr(z3.MkApp(is_nil_decl, u), z3.MkApp(is_cons_decl, u)), true);

        /* occurs check u != cons(x,u) */
        prove2(z3.MkNot(z3.MkEq(u, l1)), true);

        /* destructors: is_cons(u) => u = cons(head(u),tail(u)) */
        fml1 = z3.MkEq(u, mk_binary_app(cons_decl, mk_unary_app(head_decl, u), mk_unary_app(tail_decl, u)));
        fml = z3.MkImplies(z3.MkApp(is_cons_decl, u), fml1);
        Console.WriteLine("Formula {0}", fml);

        prove2(fml, true);

        prove2(fml1, false);
    }

Term mk_bool_var

(

string

name

)

[inline]

Create a boolean variable using the given name.

Definition at line 59 of file test_managed.cs.

Referenced by find_model_example1().

    {
        return mk_var(name, z3.MkBoolSort());
    }

Sort mk_bv_type

(

uint

num_bytes

)

[inline]

Create a bit-vector type.

Definition at line 45 of file test_managed.cs.

Referenced by mk_bv_var().

    {
        return z3.MkBvSort(num_bytes);
    }

Term mk_bv_var	(	string	name,
		uint	num_bytes
	)			[inline]

Create a bit-vector variable using the given name.

Definition at line 73 of file test_managed.cs.

    {
        return mk_var(name, mk_bv_type(num_bytes));
    }

void mk_context

(

)

[inline]

Create a logical context with model construction enabled.

Definition at line 23 of file test_managed.cs.

Referenced by array_example1(), array_example2(), bitvector_example1(), bitvector_example2(), enum_example(), find_model_example1(), find_model_example2(), injective_example(), ite_example(), parser_example1(), parser_example2(), parser_example3(), parser_example4(), prove_example1(), prove_example2(), push_pop_example1(), and tuple_example().

    {
        if (this.z3 != null)
        {
            this.z3.Dispose();
        }
        Config p = new Config();
        p.SetParamValue("MODEL", "true");
        this.z3 = new Context(p);
        p.Dispose();
    }

Sort mk_int_type

(

)

[inline]

Create an integer type.

Definition at line 38 of file test_managed.cs.

Referenced by array_example1(), injective_example(), mk_int_var(), prove_example2(), push_pop_example1(), quantifier_example1(), quantifier_example1_abs(), and tuple_example().

    {
        return z3.MkIntSort();
    }

Term mk_int_var

(

string

name

)

[inline]

Create an integer variable using the given name.

Definition at line 66 of file test_managed.cs.

Referenced by find_model_example2(), prove_example2(), quantifier_example1(), and quantifier_example1_abs().

    {
        return mk_var(name, mk_int_type());
    }

Term mk_var	(	string	name,
		Sort	ty
	)			[inline]

Create a variable using the given name and type.

Definition at line 52 of file test_managed.cs.

Referenced by array_example1(), bitvector_example1(), bitvector_example2(), enum_example(), mk_bool_var(), mk_bv_var(), and mk_int_var().

    {
        return z3.MkConst(name, ty);
    }

void parser_example1

(

)

[inline]

Demonstrates how to use the SMTLIB parser.

Definition at line 1020 of file test_managed.cs.

    {
        mk_context();

        Console.WriteLine("\nparser_example1");

        Term[] formulas, assumptions;
        FuncDecl[] decls;
        Sort[] sorts;
        string err;
        z3.ParseSmtlibString("(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))",
                             null, null, out assumptions, out formulas, out decls, out sorts, out err);
        foreach (var f in formulas)
        {
            Console.WriteLine("formula {0}", f);
            z3.AssertCnstr(f);
        }
        check2(LBool.True);
    }

void parser_example2

(

)

[inline]

Demonstrates how to initialize the parser symbol table.

Definition at line 1043 of file test_managed.cs.

    {
        mk_context();
        Console.WriteLine("\nparser_example2");

        /* 
           Z3_enable_arithmetic doesn't need to be invoked in this example
           because it will be implicitly invoked by mk_int_var.
        */

        FuncDecl a = z3.MkConstDecl("a", z3.MkIntSort());
        FuncDecl b = z3.MkConstDecl("b", z3.MkIntSort());
        FuncDecl[] decls = new FuncDecl[] { a, b };
        Term[] formulas, assumptions;
        FuncDecl[] new_decls;
        Sort[] sorts;
        string err;

        z3.ParseSmtlibString(
                             "(benchmark tst :formula (> a b))",
                             null,
                             decls,
                             out assumptions, out formulas, out new_decls, out sorts, out err);
        Term f = formulas[0];
        Console.WriteLine("formula: {0}", f);
        z3.AssertCnstr(f);
        check2(LBool.True);
    }

void parser_example3

(

)

[inline]

Demonstrates how to initialize the parser symbol table.

Definition at line 1075 of file test_managed.cs.

    {
        Console.WriteLine("\nparser_example3");

        mk_context();

        /* declare function g */
        Sort int_type = z3.MkIntSort();
        FuncDecl g = z3.MkFuncDecl("g", new Sort[] { int_type, int_type }, int_type);
        Term[] formulas, assumptions;
        FuncDecl[] new_decls;
        Sort[] sorts;
        string err;

        assert_comm_axiom(g);

        z3.ParseSmtlibString
            (
             "(benchmark tst :formula (forall (x Int) (y Int) (implies (= x y) (= (g x 0) (g 0 y)))))",
             null,
             new FuncDecl[] { g },
             out assumptions, out formulas, out new_decls, out sorts, out err);
        Term thm = formulas[0];
        Console.WriteLine("formula: {0}", thm);
        prove(thm);
    }

void parser_example4

(

)

[inline]

Display the declarations, assumptions and formulas in a SMT-LIB string.

Definition at line 1105 of file test_managed.cs.

    {
        mk_context();

        Console.WriteLine("\nparser_example4");

        Term[] formulas, assumptions;
        FuncDecl[] decls;
        Sort[] sorts;
        string err;
        z3.ParseSmtlibString
            ("(benchmark tst :extrafuns ((x Int) (y Int)) :assumption (= x 20) :formula (> x y) :formula (> x 0))",
             null, null,
             out assumptions, out formulas, out decls, out sorts, out err);
        foreach (var decl in decls)
        {
            Console.WriteLine("Declaration: {0}", decl);
        }
        foreach (var f in assumptions)
        {
            Console.WriteLine("Assumption: {0}", f);
        }
        foreach (var f in formulas)
        {
            Console.WriteLine("Formula: {0}", f);
        }
    }

void parser_example5

(

)

[inline]

Demonstrates how to handle parser errors using Z3 error handling support.

Definition at line 1136 of file test_managed.cs.

    {
        Console.WriteLine("\nparser_example5");

        Term[] formulas, assumptions;
        FuncDecl[] decls;
        Sort[] sorts;
        string err = "";
        try
        {
            z3.ParseSmtlibString(
                /* the following string has a parsing error: missing parenthesis */
                     "(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))",
                     null, null, out assumptions, out formulas, out decls, out sorts, out err);
        }
        catch (Z3Error e)
        {
            Console.WriteLine("Z3 error: {0} {1}", e, err);
        }
    }

void prove

(

Term

f

)

[inline]

Prove that the constraints already asserted into the logical context implies the given formula. The result of the proof is displayed.

Z3 is a satisfiability checker. So, one can prove f by showing that (not f) is unsatisfiable.

Definition at line 182 of file test_managed.cs.

Referenced by array_example1(), bitvector_example1(), injective_example(), parser_example3(), prove_example1(), prove_example2(), quantifier_example1(), quantifier_example1_abs(), and tuple_example().

    {
        /* save the current state of the context */
        z3.Push();

        Term not_f = z3.MkNot(f);
        z3.AssertCnstr(not_f);

        Model model = null;
        switch (z3.CheckAndGetModel(out model))
        {
            case LBool.False:
                /* proved */
                Console.WriteLine("valid");
                break;
            case LBool.Undef:
                /* Z3 failed to prove/disprove f. */
                Console.WriteLine("unknown");
                break;
            case LBool.True:
                /* disproved */
                Console.WriteLine("invalid");
                model.Display(Console.Out);
                break;
        }
        if (model != null)
        {
            model.Dispose();
        }

        /* restore context */
        z3.Pop(1);
    }

void prove2	(	Term	f,
		bool	is_valid
	)			[inline]

Prove that the constraints already asserted into the logical context implies the given formula. The result of the proof is displayed.

Z3 is a satisfiability checker. So, one can prove f by showing that (not f) is unsatisfiable.

Definition at line 225 of file test_managed.cs.

Referenced by enum_example().

    {
        /* save the current state of the context */
        z3.Push();

        Term not_f = z3.MkNot(f);
        z3.AssertCnstr(not_f);

        Model model = null;
        LBool result = z3.CheckAndGetModel(out model);
        switch (result)
        {
            case LBool.False:
                /* proved */
                Console.WriteLine("valid");
                if (!is_valid)
                {
                    exitf("Did not expecte valid");
                }
                break;
            case LBool.Undef:
                /* Z3 failed to prove/disprove f. */
                Console.WriteLine("unknown");
                if (is_valid)
                {
                    exitf("Expected valid");
                }
                break;
            case LBool.True:
                /* disproved */
                Console.WriteLine("invalid");
                model.Display(Console.Out);
                if (is_valid)
                {
                    exitf("Expected valid");
                }
                break;
        }
        if (model != null)
        {
            model.Dispose();
        }

        /* restore context */
        z3.Pop(1);

    }

void prove_example1

(

)

[inline]

Prove x = y implies g(x) = g(y), and disprove x = y implies g(g(x)) = g(y).

This function demonstrates how to create uninterpreted types and functions.

Definition at line 557 of file test_managed.cs.

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

void prove_example2

(

)

[inline]

Prove not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0 . Then, show that z < -1 is not implied.

This example demonstrates how to combine uninterpreted functions and arithmetic.

Definition at line 605 of file test_managed.cs.

    {
        Console.WriteLine("prove_example2");

        mk_context();

        /* declare function g */
        Sort int_type = mk_int_type();

        FuncDecl g = z3.MkFuncDecl("g", int_type, int_type);

        /* create x, y, and z */
        Term x = mk_int_var("x");
        Term y = mk_int_var("y");
        Term z = mk_int_var("z");

        /* create gx, gy, gz */
        Term gx = mk_unary_app(g, x);
        Term gy = mk_unary_app(g, y);
        Term gz = mk_unary_app(g, z);

        /* create zero */
        Term zero = mk_int(0);

        /* assert not(g(g(x) - g(y)) = g(z)) */
        Term gx_gy = z3.MkSub(gx, gy);
        Term ggx_gy = mk_unary_app(g, gx_gy);
        Term eq = z3.MkEq(ggx_gy, gz);
        Term c1 = z3.MkNot(eq);
        z3.AssertCnstr(c1);

        /* assert x + z <= y */
        Term x_plus_z = z3.MkAdd(x, z);
        Term c2 = z3.MkLe(x_plus_z, y);
        z3.AssertCnstr(c2);

        /* assert y <= x */
        Term c3 = z3.MkLe(y, x);
        z3.AssertCnstr(c3);

        /* prove z < 0 */
        Term f = z3.MkLt(z, zero);
        Console.WriteLine("prove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0");
        prove(f);

        /* disprove z < -1 */
        Term minus_one = mk_int(-1);
        f = z3.MkLt(z, minus_one);
        Console.WriteLine("disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1");
        prove(f);
    }

void push_pop_example1

(

)

[inline]

Show how push & pop can be used to create "backtracking" points.

This example also demonstrates how big numbers can be created in Z3.

Definition at line 662 of file test_managed.cs.

    {
        Console.WriteLine("push_pop_example1");

        mk_context();

        /* create a big number */
        Sort int_type = mk_int_type();
        Term big_number = z3.MkNumeral("1000000000000000000000000000000000000000000000000000000", int_type);

        /* create number 3 */
        Term three = z3.MkNumeral("3", int_type);

        /* create x */
        Term x = z3.MkConst("x", int_type);


        /* assert x >= "big number" */
        Term c1 = z3.MkGe(x, big_number);
        Console.WriteLine("assert: x >= 'big number'");
        z3.AssertCnstr(c1);

        /* create a backtracking point */
        Console.WriteLine("push");
        z3.Push();

        /* assert x <= 3 */
        Term c2 = z3.MkLe(x, three);
        Console.WriteLine("assert: x <= 3");
        z3.AssertCnstr(c2);

        /* context is inconsistent at this point */
        Model model = null;
        check(LBool.False, out model);

        /* backtrack: the constraint x <= 3 will be removed, since it was
           asserted after the last z3.Push. */
        Console.WriteLine("pop");
        z3.Pop(1);

        /* the context is consistent again. */
        check2(LBool.True);

        /* new constraints can be asserted... */

        /* create y */
        Term y = z3.MkConst("y", int_type);

        /* assert y > x */
        Term c3 = z3.MkGt(y, x);
        Console.WriteLine("assert: y > x");
        z3.AssertCnstr(c3);

        /* the context is still consistent. */
        check(LBool.True, out model);
        model.Dispose();
    }

void quantifier_example1

(

)

[inline]

Prove that f(x, y) = f(w, v) implies y = v when f is injective in the second argument.

See also:

assert_inj_axiom.

Definition at line 726 of file test_managed.cs.

    {
        Console.WriteLine("quantifier_example1");

        Config p = new Config();
        // p.SetParamValue("MODEL", "true");
        /* If quantified formulas are asserted in a logical context, then
           the model produced by Z3 should be viewed as a potential model.
           
        */
        if (this.z3 != null)
        {
            this.z3.Dispose();
        }
        this.z3 = new Context(p);
        p.Dispose();

        /* declare function f */
        Sort int_type = mk_int_type();
        FuncDecl f = z3.MkFuncDecl("f", new Sort[] { int_type, int_type }, int_type);

        /* assert that f is injective in the second argument. */
        assert_inj_axiom(f, 1);

        /* create x, y, v, w, fxy, fwv */
        Term x = mk_int_var("x");
        Term y = mk_int_var("y");
        Term v = mk_int_var("v");
        Term w = mk_int_var("w");
        Term fxy = mk_binary_app(f, x, y);
        Term fwv = mk_binary_app(f, w, v);

        /* assert f(x, y) = f(w, v) */
        Term p1 = z3.MkEq(fxy, fwv);
        z3.AssertCnstr(p1);

        /* prove f(x, y) = f(w, v) implies y = v */
        Term p2 = z3.MkEq(y, v);
        Console.WriteLine("prove: f(x, y) = f(w, v) implies y = v");
        prove(p2);

        /* disprove f(x, y) = f(w, v) implies x = w */
        Term p3 = z3.MkEq(x, w);
        Console.WriteLine("disprove: f(x, y) = f(w, v) implies x = w");
        prove(p3);
    }

void quantifier_example1_abs

(

)

[inline]

Prove that f(x, y) = f(w, v) implies y = v when f is injective in the second argument.

See also:

assert_inj_axiom.

Definition at line 778 of file test_managed.cs.

    {
        Console.WriteLine("quantifier_example1_abs");

        Config p = new Config();
        // p.SetParamValue("MODEL", "true");
        /* If quantified formulas are asserted in a logical context, then
           the model produced by Z3 should be viewed as a potential model.
           
        */
        if (this.z3 != null)
        {
            this.z3.Dispose();
        }
        this.z3 = new Context(p);
        p.Dispose();

        /* declare function f */
        Sort int_type = mk_int_type();
        FuncDecl f = z3.MkFuncDecl("f", new Sort[] { int_type, int_type }, int_type);

        /* assert that f is injective in the second argument. */
        assert_inj_axiom_abs(f, 1);

        /* create x, y, v, w, fxy, fwv */
        Term x = mk_int_var("x");
        Term y = mk_int_var("y");
        Term v = mk_int_var("v");
        Term w = mk_int_var("w");
        Term fxy = mk_binary_app(f, x, y);
        Term fwv = mk_binary_app(f, w, v);

        /* assert f(x, y) = f(w, v) */
        Term p1 = z3.MkEq(fxy, fwv);
        z3.AssertCnstr(p1);

        /* prove f(x, y) = f(w, v) implies y = v */
        Term p2 = z3.MkEq(y, v);
        Console.WriteLine("prove: f(x, y) = f(w, v) implies y = v");
        prove(p2);

        /* disprove f(x, y) = f(w, v) implies x = w */
        Term p3 = z3.MkEq(x, w);
        Console.WriteLine("disprove: f(x, y) = f(w, v) implies x = w");
        prove(p3);
    }

void simple_example

(

)

[inline]

"Hello world" example: create a Z3 logical context, and delete it.

Definition at line 469 of file test_managed.cs.

    {
        Console.WriteLine("simple_example");
        Config p = new Config();
        Context z3 = new Context(p);

        /* do something with the context */

        /* be kind to dispose manually and not wait for the GC. */
        z3.Dispose();
        p.Dispose();
    }

void simplifier_example

(

)

[inline]

Simplifier example.

Definition at line 1640 of file test_managed.cs.

    {
        mk_context();
        Term x = mk_int_var("x");
        Term y = mk_int_var("y");
        Term z = mk_int_var("z");
        Term u = mk_int_var("u");

        Term t1 = z3.MkAdd(x, z3.MkSub(y, z3.MkAdd(x, z)));
        Term t2 = z3.Simplify(t1);
        Console.WriteLine("{0} -> {1}", z3.ToString(t1), z3.ToString(t2));
    }

void tree_example

(

)

[inline]

Create a binary tree datatype.

Definition at line 1283 of file test_managed.cs.

    {
        mk_context();
        Sort cell;
        FuncDecl nil_decl, is_nil_decl, cons_decl, is_cons_decl, car_decl, cdr_decl;
        Term nil, l1, l2, x, y, u, v, fml, fml1;
        string[] head_tail = new string[] { "car", "cdr" };
        Sort[] sorts = new Sort[] { null, null };
        uint[] sort_refs = new uint[] { 0, 0 };
        Constructor nil_con, cons_con;

        Console.WriteLine("\ntree_example");

        nil_con = z3.MkConstructor("nil", "is_nil", null, null, null);
        cons_con = z3.MkConstructor("cons", "is_cons", head_tail, sorts, sort_refs);
        Constructor[] constructors = new Constructor[] { nil_con, cons_con };

        cell = z3.MkDataType("cell", constructors);

        nil_decl = z3.GetConstructor(nil_con);
        is_nil_decl = z3.GetTester(nil_con);
        cons_decl = z3.GetConstructor(cons_con);
        is_cons_decl = z3.GetTester(cons_con);
        FuncDecl[] cons_accessors = z3.GetAccessors(cons_con);
        car_decl = cons_accessors[0];
        cdr_decl = cons_accessors[1];

        nil = z3.MkConst(nil_decl);
        l1 = mk_binary_app(cons_decl, nil, nil);
        l2 = mk_binary_app(cons_decl, l1, nil);

        /* nil != cons(nil, nil) */
        prove2(z3.MkNot(z3.MkEq(nil, l1)), true);

        /* cons(x,u) = cons(x, v) => u = v */
        u = mk_var("u", cell);
        v = mk_var("v", cell);
        x = mk_var("x", cell);
        y = mk_var("y", cell);
        l1 = mk_binary_app(cons_decl, x, u);
        l2 = mk_binary_app(cons_decl, y, v);
        prove2(z3.MkImplies(z3.MkEq(l1, l2), z3.MkEq(u, v)), true);
        prove2(z3.MkImplies(z3.MkEq(l1, l2), z3.MkEq(x, y)), true);

        /* is_nil(u) or is_cons(u) */
        prove2(z3.MkOr(z3.MkApp(is_nil_decl, u), z3.MkApp(is_cons_decl, u)), true);

        /* occurs check u != cons(x,u) */
        prove2(z3.MkNot(z3.MkEq(u, l1)), true);

        /* destructors: is_cons(u) => u = cons(car(u),cdr(u)) */
        fml1 = z3.MkEq(u, mk_binary_app(cons_decl, mk_unary_app(car_decl, u), mk_unary_app(cdr_decl, u)));
        fml = z3.MkImplies(z3.MkApp(is_cons_decl, u), fml1);
        Console.WriteLine("Formula {0}", fml);
        prove2(fml, true);

        prove2(fml1, false);

    }

void tuple_example

(

)

[inline]

Tuples.

Check that the projection of a tuple returns the corresponding element.

Definition at line 924 of file test_managed.cs.

    {
        mk_context();
        Sort int_type = mk_int_type();
        FuncDecl[] decls = new FuncDecl[2];
        FuncDecl mk_tuple = null;
        Sort tuple = z3.MkTupleSort
        (
         z3.MkSymbol("mk_tuple"),                        // name of tuple constructor
         new Symbol[] { z3.MkSymbol("first"), z3.MkSymbol("second") },    // names of projection operators
         new Sort[] { int_type, int_type }, // types of projection operators
         out mk_tuple,
         decls                              // return declarations.
            );
        FuncDecl first = decls[0];         // declarations are for projections
        FuncDecl second = decls[1];
        Term x = z3.MkConst("x", int_type);
        Term y = z3.MkConst("y", int_type);
        Term n1 = z3.MkApp(mk_tuple, x, y);
        Term n2 = z3.MkApp(first, n1);
        Term n3 = z3.MkEq(x, n2);
        Console.WriteLine("Tuple example: {0}", z3.ToString(n3));
        prove(n3);
    }

void unsat_core_and_proof_example

(

)

[inline]

Extract unsatisfiable core example.

Definition at line 1656 of file test_managed.cs.

    {
        if (this.z3 != null)
        {
            this.z3.Dispose();
        }
        Config p = new Config();
        // p.SetParamValue("MODEL","true");
        p.SetParamValue("PROOF_MODE", "2");
        this.z3 = new Context(p);
        p.Dispose();

        Term pa = mk_bool_var("PredA");
        Term pb = mk_bool_var("PredB");
        Term pc = mk_bool_var("PredC");
        Term pd = mk_bool_var("PredD");
        Term p1 = mk_bool_var("P1");
        Term p2 = mk_bool_var("P2");
        Term p3 = mk_bool_var("P3");
        Term p4 = mk_bool_var("P4");
        Term[] assumptions = new Term[] { z3.MkNot(p1), z3.MkNot(p2), z3.MkNot(p3), z3.MkNot(p4) };
        Term f1 = z3.MkAnd(new Term[] { pa, pb, pc });
        Term f2 = z3.MkAnd(new Term[] { pa, z3.MkNot(pb), pc });
        Term f3 = z3.MkOr(z3.MkNot(pa), z3.MkNot(pc));
        Term f4 = pd;

        z3.AssertCnstr(z3.MkOr(f1, p1));
        z3.AssertCnstr(z3.MkOr(f2, p2));
        z3.AssertCnstr(z3.MkOr(f3, p3));
        z3.AssertCnstr(z3.MkOr(f4, p4));
        Term[] core = null;
        Term proof;
        Model m = null;
        LBool result;

        result = z3.CheckAssumptions(out m, assumptions, out proof, out core);

        if (result == LBool.False)
        {
            Console.WriteLine("unsat");
            Console.WriteLine("proof: {0}", proof);
            foreach (Term c in core)
            {
                Console.WriteLine("{0}", c);
            }
        }
        if (m != null)
        {
            m.Dispose();
        }
    }