Home	•	Docs	•	Download	•	Mail	•	FAQ	•	Awards	•	Status	•	MSR

An Efficient SMT Solver

C API examples

Auxiliary Functions
void	exitf (const char *message)
	exit gracefully in case of error.
void	unreachable ()
	exit if unreachable code was reached.
void	error_handler (Z3_error_code e)
	Simpler error handler.
void	throw_z3_error (Z3_error_code c)
	Low tech exceptions.
Z3_context	mk_context_custom (Z3_config cfg, Z3_error_handler err)
	Create a logical context.
Z3_context	mk_context ()
	Create a logical context.
Z3_ast	mk_var (Z3_context ctx, const char *name, Z3_type_ast ty)
	Create a variable using the given name and type.
Z3_ast	mk_bool_var (Z3_context ctx, const char *name)
	Create a boolean variable using the given name.
Z3_ast	mk_int_var (Z3_context ctx, const char *name)
	Create an integer variable using the given name.
Z3_ast	mk_int (Z3_context ctx, int v)
	Create a Z3 integer node using a C int.
Z3_ast	mk_real_var (Z3_context ctx, const char *name)
	Create a real variable using the given name.
Z3_ast	mk_unary_app (Z3_context ctx, Z3_const_decl_ast f, Z3_ast x)
	Create the unary function application: (f x).
Z3_ast	mk_binary_app (Z3_context ctx, Z3_const_decl_ast f, Z3_ast x, Z3_ast y)
	Create the binary function application: (f x y).
void	check (Z3_context ctx, Z3_lbool expected_result)
	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	prove (Z3_context ctx, Z3_ast f, Z3_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 (Z3_context ctx, Z3_const_decl_ast f, unsigned i)
	Assert the axiom: function f is injective in the i-th argument.
void	assert_comm_axiom (Z3_context ctx, Z3_const_decl_ast f)
	Assert the axiom: function f is commutative.
Z3_ast	mk_tuple_update (Z3_context c, Z3_ast t, unsigned i, Z3_ast new_val)
	Z3 does not support explicitly tuple updates. They can be easily implemented as macros. The argument t must have tuple type. A tuple update is a new tuple where field i has value new_val, and all other fields have the value of the respective field of t.
void	display_symbol (Z3_context c, FILE *out, Z3_symbol s)
	Display a symbol in the given output stream.
void	display_type (Z3_context c, FILE *out, Z3_type_ast ty)
	Display the given type.
void	display_value (Z3_context c, FILE *out, Z3_value v)
	Custom value pretty printer.
void	display_function_interpretations (Z3_context c, FILE *out, Z3_model m)
	Custom function interpretations pretty printer.
void	display_model (Z3_context c, FILE *out, Z3_model m)
	Custom model pretty printer.
void	check2 (Z3_context ctx, Z3_lbool expected_result)
	Similar to check, but uses display_model instead of Z3_model_to_string.
void	display_version ()
	Display Z3 version in the standard output.
Examples
void	simple_example ()
	"Hello world" example: create a Z3 logical context, and delete it.
void	demorgan ()
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	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	array_example3 ()
	Simple array type construction/deconstruction example.
void	tuple_example1 ()
	Simple tuple type example. It creates a tuple that is a pair of real numbers.
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	eval_example1 ()
	Demonstrate how to use Z3_eval.
void	two_contexts_example1 ()
	Several logical context can be used simultaneously.
void	error_code_example1 ()
	Demonstrates how error codes can be read insted of registering an error handler.
void	error_code_example2 ()
	Demonstrates how error handlers can be used.
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 ()
	Test ite-term (if-then-else terms).
void	simplifier_example ()
	Simplifier example.
void	print_term (Z3_context ctx, struct bound_list *bound_vars, Z3_ast t)
void	traverse_term_example ()

---

Function Documentation

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)).

This example demonstrates how to use the array theory.

Definition at line 1068 of file test_capi.c.

{
    Z3_context ctx;
    Z3_type_ast int_type, array_type;
    Z3_ast a1, a2, i1, v1, i2, v2, i3;
    Z3_ast st1, st2, sel1, sel2;
    Z3_ast antecedent, consequent;
    Z3_ast ds[3];
    Z3_ast thm;

    printf("\narray_example1\n");

    ctx = mk_context();

    int_type    = Z3_mk_int_type(ctx);
    array_type  = Z3_mk_array_type(ctx, int_type, int_type);

    a1          = mk_var(ctx, "a1", array_type);
    a2          = mk_var(ctx, "a2", array_type);
    i1          = mk_var(ctx, "i1", int_type);
    i2          = mk_var(ctx, "i2", int_type);
    i3          = mk_var(ctx, "i3", int_type);
    v1          = mk_var(ctx, "v1", int_type);
    v2          = mk_var(ctx, "v2", int_type);
    
    st1         = Z3_mk_store(ctx, a1, i1, v1);
    st2         = Z3_mk_store(ctx, a2, i2, v2);
    
    sel1        = Z3_mk_select(ctx, a1, i3);
    sel2        = Z3_mk_select(ctx, a2, i3);

    /* create antecedent */
    antecedent  = Z3_mk_eq(ctx, st1, st2);

    /* create consequent: i1 = i3 or  i2 = i3 or select(a1, i3) = select(a2, i3) */
    ds[0]       = Z3_mk_eq(ctx, i1, i3);
    ds[1]       = Z3_mk_eq(ctx, i2, i3);
    ds[2]       = Z3_mk_eq(ctx, sel1, sel2);
    consequent  = Z3_mk_or(ctx, 3, ds);

    /* prove store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3)) */
    thm         = Z3_mk_implies(ctx, antecedent, consequent);
    printf("prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))\n");
    printf("%s\n", Z3_ast_to_string(ctx, thm));
    prove(ctx, thm, Z3_TRUE);

    Z3_del_context(ctx);
}

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.

This example also shows how to use the distinct construct.

Definition at line 1124 of file test_capi.c.

{
    Z3_context ctx;
    Z3_type_ast bool_type, array_type;
    Z3_ast      a[5];
    Z3_ast      d;
    unsigned      i, n;

    printf("\narray_example2\n");

    for (n = 2; n <= 5; n++) {
        printf("n = %d\n", n);
        ctx = mk_context();
        
        bool_type   = Z3_mk_bool_type(ctx);
        array_type  = Z3_mk_array_type(ctx, bool_type, bool_type);
        
        /* create arrays */
        for (i = 0; i < n; i++) {
            Z3_symbol s = Z3_mk_int_symbol(ctx, i);
            a[i]          = Z3_mk_const(ctx, s, array_type);
        }
        
        /* assert distinct(a[0], ..., a[n]) */
        d = Z3_mk_distinct(ctx, n, a);
        printf("%s\n", Z3_ast_to_string(ctx, d));
        Z3_assert_cnstr(ctx, d);

        /* context is satisfiable if n < 5 */
        check2(ctx, n < 5 ? Z3_L_TRUE : Z3_L_FALSE);
        
        Z3_del_context(ctx);
    }
}

void array_example3

(

)

Simple array type construction/deconstruction example.

Definition at line 1162 of file test_capi.c.

{
    Z3_context ctx;
    Z3_type_ast bool_type, int_type, array_type;
    Z3_type_ast domain, range;
    printf("\narray_example3\n");

    ctx      = mk_context();

    bool_type  = Z3_mk_bool_type(ctx);
    int_type   = Z3_mk_int_type(ctx); 
    array_type = Z3_mk_array_type(ctx, int_type, bool_type);

    if (Z3_get_type_kind(ctx, array_type) != Z3_ARRAY_TYPE) {
        exitf("type must be an array type");
    }
    
    domain = Z3_get_array_type_domain(ctx, array_type);
    range  = Z3_get_array_type_range(ctx, array_type);

    printf("domain: ");
    display_type(ctx, stdout, domain);
    printf("\n");
    printf("range:  ");
    display_type(ctx, stdout, range);
    printf("\n");

    if (!Z3_is_eq(ctx, Z3_type_ast_to_ast(ctx, int_type),  Z3_type_ast_to_ast(ctx, domain)) ||
        !Z3_is_eq(ctx, Z3_type_ast_to_ast(ctx, bool_type), Z3_type_ast_to_ast(ctx, range))) {
        exitf("invalid array type");
    }

    Z3_del_context(ctx);
}

void assert_comm_axiom	(	Z3_context	ctx,
		Z3_const_decl_ast	f
	)

Assert the axiom: function f is commutative.

This example uses the SMT-LIB parser to simplify the axiom construction.

Definition at line 326 of file test_capi.c.

Referenced by parser_example3().

{
    Z3_type_ast t;
    Z3_symbol f_name, t_name;
    Z3_ast q;

    t = Z3_get_range(ctx, f);

    if (Z3_get_domain_size(ctx, f) != 2 ||
        Z3_get_domain(ctx, f, 0) != t ||
        Z3_get_domain(ctx, f, 1) != t) {
        exitf("function must be binary, and argument types must be equal to return type");
    } 
    
    /* Inside the parser, function f will be referenced using the symbol 'f'. */
    f_name = Z3_mk_string_symbol(ctx, "f");
    
    /* Inside the parser, type t will be referenced using the symbol 'T'. */
    t_name = Z3_mk_string_symbol(ctx, "T");

    Z3_parse_smtlib_string(ctx, 
                           "(benchmark comm :formula (forall (x T) (y T) (= (f x y) (f y x))))",
                           1, &t_name, &t,
                           1, &f_name, &f);
    q = Z3_get_smtlib_formula(ctx, 0);
    printf("assert axiom:\n%s\n", Z3_ast_to_string(ctx, q));
    Z3_assert_cnstr(ctx, q);
}

void assert_inj_axiom	(	Z3_context	ctx,
		Z3_const_decl_ast	f,
		unsigned	i
	)

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 255 of file test_capi.c.

Referenced by quantifier_example1().

{
    unsigned sz, j;
    Z3_type_ast finv_domain, finv_range;
    Z3_const_decl_ast finv;
    Z3_type_ast * types; /* types of the quantified variables */
    Z3_symbol *   names; /* names of the quantified variables */
    Z3_ast * xs;         /* arguments for the application f(x_0, ..., x_i, ..., x_{n-1}) */
    Z3_ast   x_i, fxs, finv_fxs, eq;
    Z3_pattern_ast p;
    Z3_ast   q;
    sz = Z3_get_domain_size(ctx, f);

    if (i >= sz) {
        exitf("failed to create inj axiom");
    }
    
    /* declare the i-th inverse of f: finv */
    finv_domain = Z3_get_range(ctx, f);
    finv_range  = Z3_get_domain(ctx, f, i);
    finv        = Z3_mk_fresh_func_decl(ctx, "inv", 1, &finv_domain, finv_range);

    /* allocate temporary arrays */
    types       = (Z3_type_ast *) malloc(sizeof(Z3_type_ast) * sz);
    names       = (Z3_symbol *) malloc(sizeof(Z3_symbol) * sz);
    xs          = (Z3_ast *) malloc(sizeof(Z3_ast) * sz);
    
    /* fill types, names and xs */
    for (j = 0; j < sz; j++) { types[j] = Z3_get_domain(ctx, f, j); };
    for (j = 0; j < sz; j++) { names[j] = Z3_mk_int_symbol(ctx, j); };
    for (j = 0; j < sz; j++) { xs[j]    = Z3_mk_bound(ctx, j, types[j]); };

    x_i = xs[i];

    /* create f(x_0, ..., x_i, ..., x_{n-1}) */ 
    fxs         = Z3_mk_app(ctx, f, sz, xs);

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

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

    /* use f(x_0, ..., x_i, ..., x_{n-1}) as the pattern for the quantifier */
    p           = Z3_mk_pattern(ctx, 1, &fxs);
    printf("pattern: %s\n", Z3_ast_to_string(ctx, Z3_pattern_ast_to_ast(ctx, p)));
    printf("\n");

    /* create & assert quantifier */
    q           = Z3_mk_forall(ctx, 
                                 0, /* using default weight */
                                 1, /* number of patterns */
                                 &p, /* address of the "array" of patterns */
                                 sz, /* number of quantified variables */
                                 types, 
                                 names,
                                 eq);
    printf("assert axiom:\n%s\n", Z3_ast_to_string(ctx, q));
    Z3_assert_cnstr(ctx, q);

    /* free temporary arrays */
    free(types);
    free(names);
    free(xs);
}

void bitvector_example1

(

)

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

Definition at line 1313 of file test_capi.c.

{
    Z3_context         ctx;
    Z3_type_ast        bv_type;
    Z3_ast             x, zero, ten, x_minus_ten, c1, c2, thm;

    printf("\nbitvector_example1\n");
    
    ctx       = mk_context();
    
    bv_type   = Z3_mk_bv_type(ctx, 32);
    
    x           = mk_var(ctx, "x", bv_type);
    zero        = Z3_mk_numeral(ctx, "0", bv_type);
    ten         = Z3_mk_numeral(ctx, "10", bv_type);
    x_minus_ten = Z3_mk_bvsub(ctx, x, ten);
    /* bvsle is signed less than or equal to */
    c1          = Z3_mk_bvsle(ctx, x, ten);
    c2          = Z3_mk_bvsle(ctx, x_minus_ten, zero);
    thm         = Z3_mk_iff(ctx, c1, c2);
    printf("disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers\n");
    prove(ctx, thm, Z3_FALSE);
    
    Z3_del_context(ctx);
}

void bitvector_example2

(

)

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

Definition at line 1342 of file test_capi.c.

{
    Z3_context ctx = mk_context();
 
    /* construct x ^ y - 103 == x * y */
    Z3_type_ast bv_type = Z3_mk_bv_type(ctx, 32);
    Z3_ast x = mk_var(ctx, "x", bv_type);
    Z3_ast y = mk_var(ctx, "y", bv_type);
    Z3_ast x_xor_y = Z3_mk_bvxor(ctx, x, y);
    Z3_ast c103 = Z3_mk_numeral(ctx, "103", bv_type);
    Z3_ast lhs = Z3_mk_bvsub(ctx, x_xor_y, c103);
    Z3_ast rhs = Z3_mk_bvmul(ctx, x, y);
    Z3_ast ctr = Z3_mk_eq(ctx, lhs, rhs);

    printf("\nbitvector_example2\n");
    printf("find values of x and y, such that x ^ y - 103 == x * y\n");
    
    /* add the constraint <tt>x ^ y - 103 == x * y<\tt> to the logical context */
    Z3_assert_cnstr(ctx, ctr);
    
    /* find a model (i.e., values for x an y that satisfy the constraint */
    check(ctx, Z3_L_TRUE);
    
    Z3_del_context(ctx);
}

void check	(	Z3_context	ctx,
		Z3_lbool	expected_result
	)

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 158 of file test_capi.c.

Referenced by bitvector_example2(), find_model_example1(), find_model_example2(), parser_example1(), and parser_example2().

{
    Z3_model m      = 0;
    Z3_lbool result = Z3_check_and_get_model(ctx, &m);
    switch (result) {
    case Z3_L_FALSE:
        printf("unsat\n");
        break;
    case Z3_L_UNDEF:
        printf("unknown\n");
        printf("potential model:\n%s\n", Z3_model_to_string(ctx, m));
        break;
    case Z3_L_TRUE:
        printf("sat\n%s\n", Z3_model_to_string(ctx, m));
        break;
    }
    if (m) {
        Z3_del_model(m);
    }
    if (result != expected_result) {
        exitf("unexpected result");
    }
}

void check2	(	Z3_context	ctx,
		Z3_lbool	expected_result
	)

Similar to check, but uses display_model instead of Z3_model_to_string.

Definition at line 603 of file test_capi.c.

Referenced by array_example2(), push_pop_example1(), and quantifier_example1().

{
    Z3_model m      = 0;
    Z3_lbool result = Z3_check_and_get_model(ctx, &m);
    switch (result) {
    case Z3_L_FALSE:
        printf("unsat\n");
        break;
    case Z3_L_UNDEF:
        printf("unknown\n");
        printf("potential model:\n");
        display_model(ctx, stdout, m);
        break;
    case Z3_L_TRUE:
        printf("sat\n");
        display_model(ctx, stdout, m);
        break;
    }
    if (m) {
        Z3_del_model(m);
    }
    if (result != expected_result) {
        exitf("unexpected result");
    }
}

void demorgan

(

)

Demonstration of how Z3 can be used to prove validity of De Morgan's Duality Law: {e not(x and y) <-> (not x) or ( not y) }

Definition at line 666 of file test_capi.c.

{
    Z3_config cfg;
    Z3_context ctx;
    Z3_type_ast bool_type;
    Z3_symbol symbol_x, symbol_y;
    Z3_ast x, y, not_x, not_y, x_and_y, ls, rs, conjecture, negated_conjecture;
    Z3_ast args[2];

    printf("\nDeMorgan\n");
    
    cfg                = Z3_mk_config();
    ctx                = Z3_mk_context(cfg);
    Z3_del_config(cfg);
#ifdef TRACING
    Z3_trace_to_stderr(ctx);
#endif
    bool_type          = Z3_mk_bool_type(ctx);
    symbol_x           = Z3_mk_int_symbol(ctx, 0);
    symbol_y           = Z3_mk_int_symbol(ctx, 1);
    x                  = Z3_mk_const(ctx, symbol_x, bool_type);
    y                  = Z3_mk_const(ctx, symbol_y, bool_type);
    
    /* De Morgan - with a negation around */
    /* !(!(x && y) <-> (!x || !y)) */
    not_x              = Z3_mk_not(ctx, x);
    not_y              = Z3_mk_not(ctx, y);
    args[0]            = x;
    args[1]            = y;
    x_and_y            = Z3_mk_and(ctx, 2, args);
    ls                 = Z3_mk_not(ctx, x_and_y);
    args[0]            = not_x;
    args[1]            = not_y;
    rs                 = Z3_mk_or(ctx, 2, args);
    conjecture         = Z3_mk_iff(ctx, ls, rs);
    negated_conjecture = Z3_mk_not(ctx, conjecture);
    
    Z3_assert_cnstr(ctx, negated_conjecture);
    switch (Z3_check(ctx)) {
    case Z3_L_FALSE:
        /* The negated conjecture was unsatisfiable, hence the conjecture is valid */
        printf("DeMorgan is valid\n");
        break;
    case Z3_L_UNDEF:
        /* Check returned undef */
        printf("Undef\n");
        break;
    case Z3_L_TRUE:
        /* The negated conjecture was satisfiable, hence the conjecture is not valid */
        printf("DeMorgan is not valid\n");
        break;
    }
    Z3_del_context(ctx);
}

void display_function_interpretations	(	Z3_context	c,
		FILE *	out,
		Z3_model	m
	)

Custom function interpretations pretty printer.

Definition at line 532 of file test_capi.c.

Referenced by display_model().

{
    unsigned num_functions, i;

    fprintf(out, "function interpretations:\n");

    num_functions = Z3_get_model_num_funcs(c, m);
    for (i = 0; i < num_functions; i++) {
        if (!Z3_is_model_func_internal(c, m, i)) {
            Z3_const_decl_ast fdecl;
            Z3_symbol name;
            Z3_value func_else;
            unsigned num_entries, j;

            fdecl = Z3_get_model_func_decl(c, m, i);
            name = Z3_get_decl_name(c, fdecl);
            display_symbol(c, out, name);
            fprintf(out, " = {");
            num_entries = Z3_get_model_func_num_entries(c, m, i);
            for (j = 0; j < num_entries; j++) {
                unsigned num_args, k;
                if (j > 0) {
                    fprintf(out, ", ");
                }
                num_args = Z3_get_model_func_entry_num_args(c, m, i, j);
                fprintf(out, "(");
                for (k = 0; k < num_args; k++) {
                    if (k > 0) {
                        fprintf(out, ", ");
                    }
                    display_value(c, out, Z3_get_model_func_entry_arg(c, m, i, j, k));
                }
                fprintf(out, "|->");
                display_value(c, out, Z3_get_model_func_entry_value(c, m, i, j));
                fprintf(out, ")");
            }
            if (num_entries > 0) {
                fprintf(out, ", ");
            }
            fprintf(out, "(else|->");
            func_else = Z3_get_model_func_else(c, m, i);
            display_value(c, out, func_else);
            fprintf(out, ")}\n");
        }
    }
}

void display_model	(	Z3_context	c,
		FILE *	out,
		Z3_model	m
	)

Custom model pretty printer.

Definition at line 582 of file test_capi.c.

Referenced by check2().

{
    unsigned num_constants;
    unsigned i;

    num_constants = Z3_get_model_num_constants(c, m);
    for (i = 0; i < num_constants; i++) {
        Z3_symbol name;
        Z3_const_decl_ast cnst = Z3_get_model_constant(c, m, i);
        name = Z3_get_decl_name(c, cnst);
        display_symbol(c, out, name);
        fprintf(out, " = ");
        display_value(c, out, Z3_get_value(c, m, cnst));
        fprintf(out, "\n");
    }
    display_function_interpretations(c, out, m);
}

void display_symbol	(	Z3_context	c,
		FILE *	out,
		Z3_symbol	s
	)

Display a symbol in the given output stream.

Definition at line 405 of file test_capi.c.

Referenced by display_function_interpretations(), display_model(), display_type(), and print_term().

{
    switch (Z3_get_symbol_kind(c, s)) {
    case Z3_INT_SYMBOL:
        fprintf(out, "#%d", Z3_get_symbol_int(c, s));
        break;
    case Z3_STRING_SYMBOL:
        fprintf(out, Z3_get_symbol_string(c, s));
        break;
    default:
        unreachable();
    }
}

void display_type	(	Z3_context	c,
		FILE *	out,
		Z3_type_ast	ty
	)

Display the given type.

Definition at line 422 of file test_capi.c.

Referenced by array_example3(), display_value(), and tuple_example1().

{
    switch (Z3_get_type_kind(c, ty)) {
    case Z3_UNINTERPRETED_TYPE:
        display_symbol(c, out, Z3_get_type_name(c, ty));
        break;
    case Z3_BOOL_TYPE:
        fprintf(out, "bool");
        break;
    case Z3_INT_TYPE:
        fprintf(out, "int");
        break;
    case Z3_REAL_TYPE:
        fprintf(out, "real");
        break;
    case Z3_BV_TYPE:
        fprintf(out, "bv%d", Z3_get_bv_type_size(c, ty));
        break;
    case Z3_ARRAY_TYPE: 
        fprintf(out, "[");
        display_type(c, out, Z3_get_array_type_domain(c, ty));
        fprintf(out, "->");
        display_type(c, out, Z3_get_array_type_range(c, ty));
        fprintf(out, "]");
        break;
    case Z3_TUPLE_TYPE: {
        unsigned num_fields = Z3_get_tuple_type_num_fields(c, ty);
        unsigned i;
        fprintf(out, "(");
        for (i = 0; i < num_fields; i++) {
            Z3_const_decl_ast field = Z3_get_tuple_type_field_decl(c, ty, i);
            if (i > 0) {
                fprintf(out, ", ");
            }
            display_type(c, out, Z3_get_range(c, field));
        }
        fprintf(out, ")");
        break;
    }
    default:
        fprintf(out, "unknown[");
        display_symbol(c, out, Z3_get_type_name(c, ty));
        fprintf(out, "]");
        break;
    }
}

void display_value	(	Z3_context	c,
		FILE *	out,
		Z3_value	v
	)

Custom value pretty printer.

This function demonstrates how to use the API to navigate values found in Z3 models.

Definition at line 475 of file test_capi.c.

Referenced by display_function_interpretations(), display_model(), and eval_example1().

{
    switch (Z3_get_value_kind(c, v)) {
    case Z3_BOOL_VALUE:
        fprintf(out, Z3_get_bool_value_bool(c, v) ? "true" : "false");
        break;
    case Z3_NUMERAL_VALUE: {
        Z3_type_ast t;
        fprintf(out, Z3_get_numeral_value_string(c, v));
        t = Z3_get_value_type(c, v);
        fprintf(out, ":");
        display_type(c, out, t);
        break;
    }
    case Z3_TUPLE_VALUE: {
        unsigned i;
        unsigned num_fields = Z3_get_tuple_value_num_fields(c, v);
        fprintf(out, "[");
        for (i = 0; i < num_fields; i++) {
            if (i > 0) {
                fprintf(out, ", ");
            }
            display_value(c, out, Z3_get_tuple_value_field(c, v, i));
        }
        fprintf(out, "]");
        break;
    }
    case Z3_ARRAY_VALUE: {
        unsigned i;
        unsigned array_size = Z3_get_array_value_size(c, v);
        fprintf(out, "{");
        for (i = 0; i < array_size; i++) {
            if (i > 0) {
                fprintf(out, ", ");
            }
            fprintf(out, "(");
            display_value(c, out, Z3_get_array_value_entry_index(c, v, i));
            fprintf(out, "|->");
            display_value(c, out, Z3_get_array_value_entry_value(c, v, i));
            fprintf(out, ")");
        }
        if (array_size > 0) {
            fprintf(out, ", ");
        }
        fprintf(out, "(else|->");
        display_value(c, out, Z3_get_array_value_else(c, v));
        fprintf(out, ")}");
        break;
    }
    default:
        fprintf(out, "#unknown");
    }
}

void display_version

(

)

Display Z3 version in the standard output.

Definition at line 632 of file test_capi.c.

{
    unsigned major, minor, build, revision;
    Z3_get_version(&major, &minor, &build, &revision);
    printf("Z3 %d.%d.%d.%d\n", major, minor, build, revision);
}

void error_code_example1

(

)

Demonstrates how error codes can be read insted of registering an error handler.

Definition at line 1446 of file test_capi.c.

{
    Z3_config cfg;
    Z3_context ctx;
    Z3_ast x;
    Z3_model m;
    Z3_value v;
    Z3_const_decl_ast x_decl;
    const char * str;

    printf("\nerror_code_example1\n");
    
    /* Do not register an error handler, as we want to use Z3_get_error_code manually */
    cfg = Z3_mk_config();
    ctx = mk_context_custom(cfg, NULL);
    Z3_del_config(cfg);

    x          = mk_bool_var(ctx, "x");
    x_decl     = Z3_get_const_ast_decl(ctx, Z3_to_const_ast(ctx, x));
    Z3_assert_cnstr(ctx, x);
    
    if (Z3_check_and_get_model(ctx, &m) != Z3_L_TRUE) {
        exitf("unexpected result");
    }

    v = Z3_get_value(ctx, m, x_decl);
    if (Z3_get_error_code(ctx) == Z3_OK) {
        printf("last call succeeded.\n");
    }
    /* The following call will fail since the value of x is a boolean */
    str = Z3_get_numeral_value_string(ctx, v);
    if (Z3_get_error_code(ctx) != Z3_OK) {
        printf("last call failed.\n");
    }
    Z3_del_model(m);
    Z3_del_context(ctx);
}

void error_code_example2

(

)

Demonstrates how error handlers can be used.

Definition at line 1487 of file test_capi.c.

{
    Z3_config cfg;
    Z3_context ctx = NULL;
    int r;

    printf("\nerror_code_example2\n");
    
    /* low tech try&catch */
    r = setjmp(g_catch_buffer);
    if (r == 0) {
        Z3_ast x, y, app;
        
        cfg = Z3_mk_config();
        ctx = mk_context_custom(cfg, throw_z3_error);
        Z3_del_config(cfg);
        
        x   = mk_int_var(ctx, "x");
        y   = mk_bool_var(ctx, "y");
        printf("before Z3_mk_iff\n"); 
        /* the next call will produce an error */
        app = Z3_mk_iff(ctx, x, y);
        unreachable();
        Z3_del_context(ctx);
    }
    else {
        printf("Z3 error: %s.\n", Z3_get_error_msg(r));
        if (cfg != NULL) {
            Z3_del_context(ctx);
        }
    }
}

void error_handler

(

Z3_error_code

e

)

Simpler error handler.

Definition at line 37 of file test_capi.c.

Referenced by mk_context(), parser_example3(), and quantifier_example1().

{
  exitf("incorrect use of Z3");
}

void eval_example1

(

)

Demonstrate how to use Z3_eval.

Definition at line 1371 of file test_capi.c.

{
    Z3_context ctx;
    Z3_ast x, y, two;
    Z3_ast c1, c2;
    Z3_model m;

    printf("\neval_example1\n");
    
    ctx        = mk_context();
    x          = mk_int_var(ctx, "x");
    y          = mk_int_var(ctx, "y");
    two        = mk_int(ctx, 2);
    
    /* assert x < y */
    c1         = Z3_mk_lt(ctx, x, y);
    Z3_assert_cnstr(ctx, c1);

    /* assert x > 2 */
    c2         = Z3_mk_gt(ctx, x, two);
    Z3_assert_cnstr(ctx, c2);

    /* find model for the constraints above */
    if (Z3_check_and_get_model(ctx, &m) == Z3_L_TRUE) {
        Z3_ast   x_plus_y;
        Z3_ast   args[2] = {x, y};
        Z3_value v;
        printf("MODEL:\n%s", Z3_model_to_string(ctx, m));
        x_plus_y = Z3_mk_add(ctx, 2, args);
        printf("\nevaluating x+y\n");
        if (Z3_eval(ctx, m, x_plus_y, &v)) {
            printf("result = ");
            display_value(ctx, stdout, v);
            printf("\n");
        }
        else {
            exitf("failed to evaluate: x+y");
        }
        Z3_del_model(m);
    }
    else {
        exitf("the constraints are satisfiable");
    }

    Z3_del_context(ctx);
}

void exitf

(

const char *

message

)

exit gracefully in case of error.

Definition at line 20 of file test_capi.c.

Referenced by array_example3(), assert_comm_axiom(),