Z3 Microsoft Research
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_context c, Z3_error_code e)
 Simpler error handler.
void throw_z3_error (Z3_context c, Z3_error_code e)
 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_context mk_proof_context ()
 Create a logical context.
Z3_ast mk_var (Z3_context ctx, const char *name, Z3_sort 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_func_decl f, Z3_ast x)
 Create the unary function application: (f x).
Z3_ast mk_binary_app (Z3_context ctx, Z3_func_decl 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_func_decl f, unsigned i)
 Assert the axiom: function f is injective in the i-th argument.
void assert_comm_axiom (Z3_context ctx, Z3_func_decl 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_sort (Z3_context c, FILE *out, Z3_sort ty)
 Display the given type.
void display_ast (Z3_context c, FILE *out, Z3_ast v)
 Custom ast 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

typedef Z3_ext_context_struct * Z3_ext_context
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 numeral_example ()
 Demonstrate different ways of creating rational numbers: decimal and fractional representations.
void ite_example ()
 Test 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 binary_tree_example ()
 Create a binary tree datatype of the form BinTree ::= nil | node(value : Int, left : BinTree, right : BinTree)
void unsat_core_and_proof_example ()
 Prove a theorem and extract, and print the proof.
void get_implied_equalities_example ()
 Extract classes of implied equalities.
Z3_ext_context mk_ext_context ()
 Create a logical context wrapper with support for retractable constraints.
void del_ext_context (Z3_ext_context ctx)
 Delete the given logical context wrapper.
unsigned assert_retractable_cnstr (Z3_ext_context ctx, Z3_ast c)
 Create a retractable constraint.
void retract_cnstr (Z3_ext_context ctx, unsigned id)
 Retract an constraint asserted using assert_retractable_cnstr.
void reassert_cnstr (Z3_ext_context ctx, unsigned id)
 Reassert a constraint retracted using retract_cnstr.
Z3_lbool ext_check (Z3_ext_context ctx)
 Check whether the logical context wrapper with support for retractable assertions is feasible or not.
void incremental_example1 ()
 Simple example using the functions: mk_ext_context, assert_retractable_cnstr, retract_cnstr, reassert_cnstr and del_ext_context.
void reference_counter_example ()
 Simple example showing how to use reference counters in Z3 to manage memory efficiently.
void smt2parser_example ()
 Demonstrates how to use SMT2 parser.
void substitute_example ()
 Demonstrates how to use the function Z3_substitute to replace subexpressions in a Z3 AST.
void substitute_vars_example ()
 Demonstrates how to use the function Z3_substitute_vars to replace (free) variables with expressions in a Z3 AST.
#define MAX_RETRACTABLE_ASSERTIONS   1024

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

{
    Z3_context ctx;
    Z3_sort int_sort, array_sort;
    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");
    LOG_MSG("array_example1");

    ctx = mk_context();

    int_sort    = Z3_mk_int_sort(ctx);
    array_sort  = Z3_mk_array_sort(ctx, int_sort, int_sort);

    a1          = mk_var(ctx, "a1", array_sort);
    a2          = mk_var(ctx, "a2", array_sort);
    i1          = mk_var(ctx, "i1", int_sort);
    i2          = mk_var(ctx, "i2", int_sort);
    i3          = mk_var(ctx, "i3", int_sort);
    v1          = mk_var(ctx, "v1", int_sort);
    v2          = mk_var(ctx, "v2", int_sort);
    
    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 1156 of file test_capi.c.

{
    Z3_context ctx;
    Z3_sort bool_sort, array_sort;
    Z3_ast      a[5];
    Z3_ast      d;
    unsigned      i, n;

    printf("\narray_example2\n");
    LOG_MSG("array_example2");

    for (n = 2; n <= 5; n++) {
        printf("n = %d\n", n);
        ctx = mk_context();
        
        bool_sort   = Z3_mk_bool_sort(ctx);
        array_sort  = Z3_mk_array_sort(ctx, bool_sort, bool_sort);
        
        /* 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_sort);
        }
        
        /* 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 1195 of file test_capi.c.

{
    Z3_context ctx;
    Z3_sort bool_sort, int_sort, array_sort;
    Z3_sort domain, range;
    printf("\narray_example3\n");
    LOG_MSG("array_example3");

    ctx      = mk_context();

    bool_sort  = Z3_mk_bool_sort(ctx);
    int_sort   = Z3_mk_int_sort(ctx); 
    array_sort = Z3_mk_array_sort(ctx, int_sort, bool_sort);

    if (Z3_get_sort_kind(ctx, array_sort) != Z3_ARRAY_SORT) {
        exitf("type must be an array type");
    }
    
    domain = Z3_get_array_sort_domain(ctx, array_sort);
    range  = Z3_get_array_sort_range(ctx, array_sort);

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

        if (int_sort != domain || bool_sort != range) {
        exitf("invalid array type");
    }

    Z3_del_context(ctx);
}
void assert_comm_axiom ( Z3_context  ctx,
Z3_func_decl  f 
)

Assert the axiom: function f is commutative.

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

Definition at line 349 of file test_capi.c.

Referenced by parser_example3().

{
    Z3_sort 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_func_decl  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 278 of file test_capi.c.

Referenced by quantifier_example1().

{
    unsigned sz, j;
    Z3_sort finv_domain, finv_range;
    Z3_func_decl finv;
    Z3_sort * 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 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_sort *) malloc(sizeof(Z3_sort) * 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_pattern_to_string(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);
}
unsigned assert_retractable_cnstr ( Z3_ext_context  ctx,
Z3_ast  c 
)

Create a retractable constraint.

Returns:
An id that can be used to retract/reassert the constraint.

Definition at line 2343 of file test_capi.c.

Referenced by incremental_example1().

                                                                {
    unsigned result;
    Z3_sort ty;
    Z3_ast ans_lit;
    Z3_ast args[2];
    if (ctx->m_num_answer_literals == MAX_RETRACTABLE_ASSERTIONS) {
        exitf("maximum number of retractable constraints was exceeded.");
    }
    ty      = Z3_mk_bool_sort(ctx->m_context);
    ans_lit = Z3_mk_fresh_const(ctx->m_context, "k", ty);
    result  = ctx->m_num_answer_literals;
    ctx->m_answer_literals[result] = ans_lit;
    ctx->m_retracted[result]       = Z3_FALSE;
    ctx->m_num_answer_literals++;
    // assert: c OR (not ans_lit)
    args[0] = c;
    args[1] = Z3_mk_not(ctx->m_context, ans_lit);
    Z3_assert_cnstr(ctx->m_context, Z3_mk_or(ctx->m_context, 2, args));
    return result;
}
void binary_tree_example ( )

Create a binary tree datatype of the form BinTree ::= nil | node(value : Int, left : BinTree, right : BinTree)

Definition at line 2102 of file test_capi.c.

                           {
    Z3_context ctx = mk_context();
    Z3_sort cell;
    Z3_func_decl 
        nil_decl, /* nil : BinTree   (constructor) */
        is_nil_decl, /* is_nil : BinTree -> Bool (tester, return true if the given BinTree is a nil) */
        node_decl, /* node : Int, BinTree, BinTree -> BinTree  (constructor) */
        is_node_decl, /* is_node : BinTree -> Bool (tester, return true if the given BinTree is a node) */
        value_decl,  /* value : BinTree -> Int  (accessor for nodes) */
        left_decl,   /* left : BinTree -> BinTree (accessor for nodes, retrieves the left child of a node) */
        right_decl;  /* right : BinTree -> BinTree (accessor for nodes, retrieves the right child of a node) */
    Z3_symbol node_accessor_names[3] = { Z3_mk_string_symbol(ctx, "value"), Z3_mk_string_symbol(ctx, "left"), Z3_mk_string_symbol(ctx, "right") };
    Z3_sort   node_accessor_sorts[3] = { Z3_mk_int_sort(ctx), 0, 0 };
    unsigned  node_accessor_sort_refs[3] = { 0, 0, 0 };
    Z3_constructor nil_con, node_con;
    Z3_constructor constructors[2];
    Z3_func_decl node_accessors[3];

    printf("\nbinary_tree_example\n");
    LOG_MSG("binary_tree_example");

    /* nil_con and node_con are auxiliary datastructures used to create the new recursive datatype BinTree */
    nil_con  = Z3_mk_constructor(ctx, Z3_mk_string_symbol(ctx, "nil"), Z3_mk_string_symbol(ctx, "is-nil"), 0, 0, 0, 0);
    node_con = Z3_mk_constructor(ctx, Z3_mk_string_symbol(ctx, "node"), Z3_mk_string_symbol(ctx, "is-cons"), 
                                 3, node_accessor_names, node_accessor_sorts, node_accessor_sort_refs);
    constructors[0] = nil_con;
    constructors[1] = node_con;
    
    /* create the new recursive datatype */
    cell = Z3_mk_datatype(ctx, Z3_mk_string_symbol(ctx, "BinTree"), 2, constructors);

    /* retrieve the new declarations: constructors (nil_decl, node_decl), testers (is_nil_decl, is_cons_del), and 
       accessors (value_decl, left_decl, right_decl */
    Z3_query_constructor(ctx, nil_con, 0, &nil_decl, &is_nil_decl, 0);
    Z3_query_constructor(ctx, node_con, 3, &node_decl, &is_node_decl, node_accessors);
    value_decl = node_accessors[0];
    left_decl  = node_accessors[1];
    right_decl = node_accessors[2];

    /* delete auxiliary/helper structures */
    Z3_del_constructor(ctx, nil_con);
    Z3_del_constructor(ctx, node_con);

    /* small example using the recursive datatype BinTree */
    {
        /* create nil */
        Z3_ast nil = Z3_mk_app(ctx, nil_decl, 0, 0);
        /* create node1 ::= node(10, nil, nil) */
        Z3_ast args1[3] = { mk_int(ctx, 10), nil, nil };
        Z3_ast node1    = Z3_mk_app(ctx, node_decl, 3, args1);
        /* create node2 ::= node(30, node1, nil) */
        Z3_ast args2[3] = { mk_int(ctx, 30), node1, nil };
        Z3_ast node2    = Z3_mk_app(ctx, node_decl, 3, args2);
        /* create node3 ::= node(20, node2, node1); */
        Z3_ast args3[3] = { mk_int(ctx, 20), node2, node1 };
        Z3_ast node3    = Z3_mk_app(ctx, node_decl, 3, args3);

        /* prove that nil != node1 */
        prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, node1)), Z3_TRUE);

        /* prove that nil = left(node1) */
        prove(ctx, Z3_mk_eq(ctx, nil, mk_unary_app(ctx, left_decl, node1)), Z3_TRUE);

        /* prove that node1 = right(node3) */
        prove(ctx, Z3_mk_eq(ctx, node1, mk_unary_app(ctx, right_decl, node3)), Z3_TRUE);

        /* prove that !is-nil(node2) */
        prove(ctx, Z3_mk_not(ctx, mk_unary_app(ctx, is_nil_decl, node2)), Z3_TRUE);

        /* prove that value(node2) >= 0 */
        prove(ctx, Z3_mk_ge(ctx, mk_unary_app(ctx, value_decl, node2), mk_int(ctx, 0)), Z3_TRUE);
    }

    /* delete logical context */
    Z3_del_context(ctx);
}
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 1347 of file test_capi.c.

{
    Z3_context         ctx;
    Z3_sort        bv_sort;
    Z3_ast             x, zero, ten, x_minus_ten, c1, c2, thm;

    printf("\nbitvector_example1\n");
    LOG_MSG("bitvector_example1");
    
    ctx       = mk_context();
    
    bv_sort   = Z3_mk_bv_sort(ctx, 32);
    
    x           = mk_var(ctx, "x", bv_sort);
    zero        = Z3_mk_numeral(ctx, "0", bv_sort);
    ten         = Z3_mk_numeral(ctx, "10", bv_sort);
    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 1377 of file test_capi.c.

{
    Z3_context ctx = mk_context();
 
    /* construct x ^ y - 103 == x * y */
    Z3_sort bv_sort = Z3_mk_bv_sort(ctx, 32);
    Z3_ast x = mk_var(ctx, "x", bv_sort);
    Z3_ast y = mk_var(ctx, "y", bv_sort);
    Z3_ast x_xor_y = Z3_mk_bvxor(ctx, x, y);
    Z3_ast c103 = Z3_mk_numeral(ctx, "103", bv_sort);
    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");
    LOG_MSG("bitvector_example2");
    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 181 of file test_capi.c.

Referenced by bitvector_example2(), find_model_example1(), find_model_example2(), model_display_example(), pa_theory_example2(), parser_example1(), parser_example2(), reference_counter_example(), and simple_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(ctx, 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 619 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(ctx, m);
    }
    if (result != expected_result) {
        exitf("unexpected result");
    }
}
void del_ext_context ( Z3_ext_context  ctx)

Delete the given logical context wrapper.

Definition at line 2333 of file test_capi.c.

Referenced by incremental_example1().

                                         {
    Z3_del_context(ctx->m_context);
    free(ctx);
}
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 682 of file test_capi.c.

{
    Z3_config cfg;
    Z3_context ctx;
    Z3_sort bool_sort;
    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");
    LOG_MSG("DeMorgan");
    
    cfg                = Z3_mk_config();
    ctx                = Z3_mk_context(cfg);
    Z3_del_config(cfg);
    bool_sort          = Z3_mk_bool_sort(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_sort);
    y                  = Z3_mk_const(ctx, symbol_y, bool_sort);
    
    /* 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_ast ( Z3_context  c,
FILE *  out,
Z3_ast  v 
)

Custom ast pretty printer.

This function demonstrates how to use the API to navigate terms.

Definition at line 504 of file test_capi.c.

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

{
    switch (Z3_get_ast_kind(c, v)) {
    case Z3_NUMERAL_AST: {
        Z3_sort t;
        fprintf(out, "%s", Z3_get_numeral_string(c, v));
        t = Z3_get_sort(c, v);
        fprintf(out, ":");
        display_sort(c, out, t);
        break;
    }
    case Z3_APP_AST: {
        unsigned i;
        Z3_app app = Z3_to_app(c, v);
        unsigned num_fields = Z3_get_app_num_args(c, app);
        Z3_func_decl d = Z3_get_app_decl(c, app);
        fprintf(out, "%s", Z3_func_decl_to_string(c, d));
        if (num_fields > 0) {
            fprintf(out, "[");
            for (i = 0; i < num_fields; i++) {
                if (i > 0) {
                    fprintf(out, ", ");
                }
                display_ast(c, out, Z3_get_app_arg(c, app, i));
            }
            fprintf(out, "]");
        }
        break;
    }
    case Z3_QUANTIFIER_AST: {
        fprintf(out, "quantifier");
        ;       
    }
    default:
        fprintf(out, "#unknown");
    }
}
void display_function_interpretations ( Z3_context  c,
FILE *  out,
Z3_model  m 
)

Custom function interpretations pretty printer.

Definition at line 545 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++) {
        Z3_func_decl fdecl;
        Z3_symbol name;
        Z3_ast 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_ast(c, out, Z3_get_model_func_entry_arg(c, m, i, j, k));
            }
            fprintf(out, "|->");
            display_ast(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_ast(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 593 of file test_capi.c.

Referenced by check2(), and unsat_core_and_proof_example().

{
    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_func_decl cnst = Z3_get_model_constant(c, m, i);
        Z3_ast a, v;
        Z3_bool ok;
        name = Z3_get_decl_name(c, cnst);
        display_symbol(c, out, name);
        fprintf(out, " = ");
        a = Z3_mk_app(c, cnst, 0, 0);
        v = a;
        ok = Z3_eval(c, m, a, &v);
        display_ast(c, out, v);
        fprintf(out, "\n");
    }
    display_function_interpretations(c, out, m);
}
void display_sort ( Z3_context  c,
FILE *  out,
Z3_sort  ty 
)

Display the given type.

Definition at line 446 of file test_capi.c.

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

{
    switch (Z3_get_sort_kind(c, ty)) {
    case Z3_UNINTERPRETED_SORT:
        display_symbol(c, out, Z3_get_sort_name(c, ty));
        break;
    case Z3_BOOL_SORT:
        fprintf(out, "bool");
        break;
    case Z3_INT_SORT:
        fprintf(out, "int");
        break;
    case Z3_REAL_SORT:
        fprintf(out, "real");
        break;
    case Z3_BV_SORT:
        fprintf(out, "bv%d", Z3_get_bv_sort_size(c, ty));
        break;
    case Z3_ARRAY_SORT: 
        fprintf(out, "[");
        display_sort(c, out, Z3_get_array_sort_domain(c, ty));
        fprintf(out, "->");
        display_sort(c, out, Z3_get_array_sort_range(c, ty));
        fprintf(out, "]");
        break;
    case Z3_DATATYPE_SORT:
                if (Z3_get_datatype_sort_num_constructors(c, ty) != 1) 
                {
                        fprintf(out, "%s", Z3_sort_to_string(c,ty));
                        break;
                }
                {
        unsigned num_fields = Z3_get_tuple_sort_num_fields(c, ty);
        unsigned i;
        fprintf(out, "(");
        for (i = 0; i < num_fields; i++) {
            Z3_func_decl field = Z3_get_tuple_sort_field_decl(c, ty, i);
            if (i > 0) {
                fprintf(out, ", ");
            }
            display_sort(c, out, Z3_get_range(c, field));
        }
        fprintf(out, ")");
        break;
    }
    default:
        fprintf(out, "unknown[");
        display_symbol(c, out, Z3_get_sort_name(c, ty));
        fprintf(out, "]");
        break;
    }
}
void display_symbol ( Z3_context  c,
FILE *  out,
Z3_symbol  s 
)

Display a symbol in the given output stream.

Definition at line 429 of file test_capi.c.

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

{
    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, "%s", Z3_get_symbol_string(c, s));
        break;
    default:
        unreachable();
    }
}
void display_version ( )

Display Z3 version in the standard output.

Definition at line 648 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 enum_example ( )

Create an enumeration data type.

Definition at line 1795 of file test_capi.c.

                    {
    Z3_context ctx = mk_context();
    Z3_sort fruit;
    Z3_symbol name = Z3_mk_string_symbol(ctx, "fruit");
    Z3_symbol enum_names[3];
    Z3_func_decl enum_consts[3];
    Z3_func_decl enum_testers[3];
    Z3_ast apple, orange, banana, fruity;
    Z3_ast ors[3];
    
    printf("\nenum_example\n");
    LOG_MSG("enum_example");

    enum_names[0] = Z3_mk_string_symbol(ctx,"apple");
    enum_names[1] = Z3_mk_string_symbol(ctx,"banana");
    enum_names[2] = Z3_mk_string_symbol(ctx,"orange");

    fruit = Z3_mk_enumeration_sort(ctx, name, 3, enum_names, enum_consts, enum_testers);
       
    printf("%s\n", Z3_func_decl_to_string(ctx, enum_consts[0]));
    printf("%s\n", Z3_func_decl_to_string(ctx, enum_consts[1]));
    printf("%s\n", Z3_func_decl_to_string(ctx, enum_consts[2]));

    printf("%s\n", Z3_func_decl_to_string(ctx, enum_testers[0]));
    printf("%s\n", Z3_func_decl_to_string(ctx, enum_testers[1]));
    printf("%s\n", Z3_func_decl_to_string(ctx, enum_testers[2]));

    apple  = Z3_mk_app(ctx, enum_consts[0], 0, 0);
    banana = Z3_mk_app(ctx, enum_consts[1], 0, 0);
    orange = Z3_mk_app(ctx, enum_consts[2], 0, 0);

    /* Apples are different from oranges */
    prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, apple, orange)), Z3_TRUE);

    /* Apples pass the apple test */
    prove(ctx, Z3_mk_app(ctx, enum_testers[0], 1, &apple), Z3_TRUE);

    /* Oranges fail the apple test */
    prove(ctx, Z3_mk_app(ctx, enum_testers[0], 1, &orange), Z3_FALSE);
    prove(ctx, Z3_mk_not(ctx, Z3_mk_app(ctx, enum_testers[0], 1, &orange)), Z3_TRUE);

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

    /* If something is fruity, then it is an apple, banana, or orange */
    ors[0] = Z3_mk_eq(ctx, fruity, apple);
    ors[1] = Z3_mk_eq(ctx, fruity, banana);
    ors[2] = Z3_mk_eq(ctx, fruity, orange);

    prove(ctx, Z3_mk_or(ctx, 3, ors), Z3_TRUE);

    /* delete logical context */
    Z3_del_context(ctx);
}
void error_code_example1 ( )

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

Definition at line 1484 of file test_capi.c.

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

    printf("\nerror_code_example1\n");
    LOG_MSG("error_code_example11");

    /* 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_app_decl(ctx, Z3_to_app(ctx, x));
    Z3_assert_cnstr(ctx, x);
    
    if (Z3_check_and_get_model(ctx, &m) != Z3_L_TRUE) {
        exitf("unexpected result");
    }

    if (!Z3_eval_func_decl(ctx, m, x_decl, &v)) {
        exitf("did not obtain value for declaration.\n");
    }
    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_string(ctx, v);
    if (Z3_get_error_code(ctx) != Z3_OK) {
        printf("last call failed.\n");
    }
    Z3_del_model(ctx, m);
    Z3_del_context(ctx);
}
void error_code_example2 ( )

Demonstrates how error handlers can be used.

Definition at line 1528 of file test_capi.c.

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

    printf("\nerror_code_example2\n");
    LOG_MSG("error_code_example2");
    
    /* 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((Z3_error_code)r));
        if (ctx != NULL) {
            Z3_del_context(ctx);
        }
    }
}
void error_handler ( Z3_context  c,
Z3_error_code  e 
)

Simpler error handler.

Definition at line 45 of file test_capi.c.

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

{
    printf("Error code: %d\n", e);
    exitf("incorrect use of Z3");
}
void eval_example1 ( )

Demonstrate how to use Z3_eval.

Definition at line 1407 of file test_capi.c.

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

    printf("\neval_example1\n");
    LOG_MSG("eval_example1");
    
    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_ast 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_ast(ctx, stdout, v);
            printf("\n");
        }
        else {
            exitf("failed to evaluate: x+y");
        }
        Z3_del_model(ctx, m);
    }
    else {
        exitf("the constraints are satisfiable");
    }

    Z3_del_context(ctx);
}
void exitf ( const char *  message)
Z3_lbool ext_check ( Z3_ext_context  ctx)

Check whether the logical context wrapper with support for retractable assertions is feasible or not.

Definition at line 2387 of file test_capi.c.

Referenced by incremental_example1().

                                       {
    Z3_lbool result;
    unsigned num_assumptions = 0;
    Z3_ast assumptions[MAX_RETRACTABLE_ASSERTIONS];
    Z3_ast core[MAX_RETRACTABLE_ASSERTIONS];
    unsigned core_size;
    Z3_ast   dummy_proof = 0; // we don't care about the proof in this example.
    Z3_model dummy_model = 0; // we don't care about the model in this example.
    unsigned i;
    for (i = 0; i < ctx->m_num_answer_literals; i++) {
        if (ctx->m_retracted[i] == Z3_FALSE) {
            // Since the answer literal was not retracted, we added it as an assumption.
            // Recall that we assert (C \/ (not ans_lit)). Therefore, adding ans_lit as an assumption has the effect of "asserting" C.
            // If the constraint was "retracted" (ctx->m_retracted[i] == Z3_true), then we don't really need to add (not ans_lit) as an assumption.
            assumptions[num_assumptions] = ctx->m_answer_literals[i];
            num_assumptions ++;
        }
    }
    result = Z3_check_assumptions(ctx->m_context, num_assumptions, assumptions, &dummy_model, &dummy_proof, &core_size, core);
    if (result == Z3_L_FALSE) {
        // Display the UNSAT core
        printf("unsat core: ");
        for (i = 0; i < core_size; i++) {
            // In this example, we display the core based on the assertion ids.
            unsigned j;
            for (j = 0; j < ctx->m_num_answer_literals; j++) {
                if (core[i] == ctx->m_answer_literals[j]) {
                    printf("%d ", j);
                    break;
                }
            }
            if (j == ctx->m_num_answer_literals) {
                exitf("bug in Z3, the core contains something that is not an assumption.");
            }
        }
        printf("\n");
    }

    if (dummy_model) {
        Z3_del_model(ctx->m_context, dummy_model);
    }

    return result;
}
void find_model_example1 ( )

Find a model for x xor y.

Definition at line 738 of file test_capi.c.

{
    Z3_context ctx;
    Z3_ast x, y, x_xor_y;

    printf("\nfind_model_example1\n");
    LOG_MSG("find_model_example1");

    ctx     = mk_context();

    x       = mk_bool_var(ctx, "x");
    y       = mk_bool_var(ctx, "y");
    x_xor_y = Z3_mk_xor(ctx, x, y);
    
    Z3_assert_cnstr(ctx, x_xor_y);

    printf("model for: x xor y\n");
    check(ctx, Z3_L_TRUE);

    Z3_del_context(ctx);
}
void find_model_example2 ( )

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

Definition at line 764 of file test_capi.c.

{
    Z3_context ctx;
    Z3_ast x, y, one, two, y_plus_one;
    Z3_ast x_eq_y;
    Z3_ast args[2];
    Z3_ast c1, c2, c3;

    printf("\nfind_model_example2\n");
    LOG_MSG("find_model_example2");
    
    ctx        = mk_context();
    x          = mk_int_var(ctx, "x");
    y          = mk_int_var(ctx, "y");
    one        = mk_int(ctx, 1);
    two        = mk_int(ctx, 2);

    args[0]    = y;
    args[1]    = one;
    y_plus_one = Z3_mk_add(ctx, 2, args);

    c1         = Z3_mk_lt(ctx, x, y_plus_one);
    c2         = Z3_mk_gt(ctx, x, two);
    
    Z3_assert_cnstr(ctx, c1);
    Z3_assert_cnstr(ctx, c2);

    printf("model for: x < y + 1, x > 2\n");
    check(ctx, Z3_L_TRUE);

    /* assert not(x = y) */
    x_eq_y     = Z3_mk_eq(ctx, x, y);
    c3         = Z3_mk_not(ctx, x_eq_y);
    Z3_assert_cnstr(ctx, c3);

    printf("model for: x < y + 1, x > 2, not(x = y)\n");
    check(ctx, Z3_L_TRUE);

    Z3_del_context(ctx);
}
void forest_example ( )

Create a forest of trees.

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

Definition at line 1994 of file test_capi.c.

                      {
    Z3_context ctx = mk_context();
    Z3_sort tree, forest;
    Z3_func_decl nil1_decl, is_nil1_decl, cons1_decl, is_cons1_decl, car1_decl, cdr1_decl;
    Z3_func_decl nil2_decl, is_nil2_decl, cons2_decl, is_cons2_decl, car2_decl, cdr2_decl;
    Z3_ast nil1, nil2, t1, t2, t3, t4, f1, f2, f3, l1, l2, x, y, u, v;
    Z3_symbol head_tail[2] = { Z3_mk_string_symbol(ctx, "car"), Z3_mk_string_symbol(ctx, "cdr") };
    Z3_sort sorts[2] = { 0, 0 };
    unsigned sort_refs[2] = { 0, 0 };
    Z3_constructor nil1_con, cons1_con, nil2_con, cons2_con;
    Z3_constructor constructors1[2], constructors2[2];
    Z3_func_decl cons_accessors[2];
    Z3_ast ors[2];
    Z3_constructor_list clist1, clist2;
    Z3_constructor_list clists[2];
    Z3_symbol sort_names[2] = { Z3_mk_string_symbol(ctx, "forest"), Z3_mk_string_symbol(ctx, "tree") };

    printf("\nforest_example\n");
    LOG_MSG("forest_example");

    /* build a forest */
    nil1_con  = Z3_mk_constructor(ctx, Z3_mk_string_symbol(ctx, "nil1"), Z3_mk_string_symbol(ctx, "is_nil1"), 0, 0, 0, 0);
    sort_refs[0] = 1; /* the car of a forest is a tree */
    sort_refs[1] = 0;
    cons1_con = Z3_mk_constructor(ctx, Z3_mk_string_symbol(ctx, "cons1"), Z3_mk_string_symbol(ctx, "is_cons1"), 2, head_tail, sorts, sort_refs);
    constructors1[0] = nil1_con;
    constructors1[1] = cons1_con;

    /* build a tree */
    nil2_con  = Z3_mk_constructor(ctx, Z3_mk_string_symbol(ctx, "nil2"), Z3_mk_string_symbol(ctx, "is_nil2"),0, 0, 0, 0);
    sort_refs[0] = 0; /* both branches of a tree are forests */
    sort_refs[1] = 0;
    cons2_con = Z3_mk_constructor(ctx, Z3_mk_string_symbol(ctx, "cons2"), Z3_mk_string_symbol(ctx, "is_cons2"),2, head_tail, sorts, sort_refs);
    constructors2[0] = nil2_con;
    constructors2[1] = cons2_con;
    
    clist1 = Z3_mk_constructor_list(ctx, 2, constructors1);
    clist2 = Z3_mk_constructor_list(ctx, 2, constructors2);

    clists[0] = clist1;
    clists[1] = clist2;

    Z3_mk_datatypes(ctx, 2, sort_names, sorts, clists);
    forest = sorts[0];
    tree = sorts[1];

    Z3_query_constructor(ctx, nil1_con, 0, &nil1_decl, &is_nil1_decl, 0);
    Z3_query_constructor(ctx, cons1_con, 2, &cons1_decl, &is_cons1_decl, cons_accessors);
    car1_decl = cons_accessors[0];
    cdr1_decl = cons_accessors[1];

    Z3_query_constructor(ctx, nil2_con, 0, &nil2_decl, &is_nil2_decl, 0);
    Z3_query_constructor(ctx, cons2_con, 2, &cons2_decl, &is_cons2_decl, cons_accessors);
    car2_decl = cons_accessors[0];
    cdr2_decl = cons_accessors[1];
    
    Z3_del_constructor_list(ctx, clist1);
    Z3_del_constructor_list(ctx, clist2);
    Z3_del_constructor(ctx,nil1_con);
    Z3_del_constructor(ctx,cons1_con);
    Z3_del_constructor(ctx,nil2_con);
    Z3_del_constructor(ctx,cons2_con);

    nil1 = Z3_mk_app(ctx, nil1_decl, 0, 0);
    nil2 = Z3_mk_app(ctx, nil2_decl, 0, 0);
    f1 = mk_binary_app(ctx, cons1_decl, nil2, nil1);
    t1 = mk_binary_app(ctx, cons2_decl, nil1, nil1);
    t2 = mk_binary_app(ctx, cons2_decl, f1, nil1);
    t3 = mk_binary_app(ctx, cons2_decl, f1, f1);
    t4 = mk_binary_app(ctx, cons2_decl, nil1, f1);
    f2 = mk_binary_app(ctx, cons1_decl, t1, nil1);
    f3 = mk_binary_app(ctx, cons1_decl, t1, f1);


    /* nil != cons(nil,nil) */
    prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil1, f1)), Z3_TRUE);
    prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil2, t1)), Z3_TRUE);


    /* cons(x,u) = cons(x, v) => u = v */
    u = mk_var(ctx, "u", forest);
    v = mk_var(ctx, "v", forest);    
    x = mk_var(ctx, "x", tree);
    y = mk_var(ctx, "y", tree);
    l1 = mk_binary_app(ctx, cons1_decl, x, u);
    l2 = mk_binary_app(ctx, cons1_decl, y, v);
    prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE);
    prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);

    /* is_nil(u) or is_cons(u) */
    ors[0] = Z3_mk_app(ctx, is_nil1_decl, 1, &u);
    ors[1] = Z3_mk_app(ctx, is_cons1_decl, 1, &u);
    prove(ctx, Z3_mk_or(ctx, 2, ors), Z3_TRUE);

    /* occurs check u != cons(x,u) */    
    prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE);

    /* delete logical context */
    Z3_del_context(ctx);
}
void get_implied_equalities_example ( )

Extract classes of implied equalities.

This example illustrates the use of Z3_get_implied_equalities.

Definition at line 2257 of file test_capi.c.

                                      {
    Z3_config cfg = Z3_mk_config();
    Z3_context ctx; 

    printf("\nget_implied_equalities example\n");
    LOG_MSG("get_implied_equalities example");
    
    Z3_set_param_value(cfg, "ARITH_PROCESS_ALL_EQS", "true");
    Z3_set_param_value(cfg, "ARITH_EQ_BOUNDS", "true");
    ctx = Z3_mk_context(cfg);
    Z3_del_config(cfg);
    {
        Z3_sort int_ty = Z3_mk_int_sort(ctx);
        Z3_ast a = mk_int_var(ctx,"a");
        Z3_ast b = mk_int_var(ctx,"b");
        Z3_ast c = mk_int_var(ctx,"c");
        Z3_ast d = mk_int_var(ctx,"d");
        Z3_func_decl f = Z3_mk_func_decl(ctx, Z3_mk_string_symbol(ctx,"f"), 1, &int_ty, int_ty);
        Z3_ast fa = Z3_mk_app(ctx, f, 1, &a);
        Z3_ast fb = Z3_mk_app(ctx, f, 1, &b);
        Z3_ast fc = Z3_mk_app(ctx, f, 1, &c);
        unsigned const num_terms = 7;
        unsigned i;
        Z3_ast terms[7] = { a, b, c, d, fa, fb, fc };
        unsigned class_ids[7] = { 0, 0, 0, 0, 0, 0, 0 };
        
        Z3_assert_cnstr(ctx, Z3_mk_eq(ctx, a, b));
        Z3_assert_cnstr(ctx, Z3_mk_eq(ctx, b, c));
        Z3_assert_cnstr(ctx, Z3_mk_le(ctx, fc, b));
        Z3_assert_cnstr(ctx, Z3_mk_le(ctx, b, fa));
        
        Z3_get_implied_equalities(ctx, num_terms, terms, class_ids);
        for (i = 0; i < num_terms; ++i) {
            printf("Class %s |-> %d\n", Z3_ast_to_string(ctx, terms[i]), class_ids[i]);
        }
        printf("asserting f(a) <= b\n");
        Z3_assert_cnstr(ctx, Z3_mk_le(ctx, fa, b));
        Z3_get_implied_equalities(ctx, num_terms, terms, class_ids);
        for (i = 0; i < num_terms; ++i) {
            printf("Class %s |-> %d\n", Z3_ast_to_string(ctx, terms[i]), class_ids[i]);
        }
    }
    /* delete logical context */
    Z3_del_context(ctx);
}
void incremental_example1 ( )

Simple example using the functions: mk_ext_context, assert_retractable_cnstr, retract_cnstr, reassert_cnstr and del_ext_context.

Definition at line 2435 of file test_capi.c.

                            {
    Z3_ext_context ext_ctx = mk_ext_context();
    Z3_context     ctx     = ext_ctx->m_context;
    Z3_ast x, y, z, two, one;
    unsigned c1, c2, c3, c4;
    Z3_bool result;

    printf("\nincremental_example1\n");
    LOG_MSG("incremental_example1");

    x          = mk_int_var(ctx, "x");
    y          = mk_int_var(ctx, "y");
    z          = mk_int_var(ctx, "z");
    two        = mk_int(ctx, 2);
    one        = mk_int(ctx, 1);
    
    /* assert x < y */
    c1 = assert_retractable_cnstr(ext_ctx, Z3_mk_lt(ctx, x, y));
    /* assert x = z */
    c2 = assert_retractable_cnstr(ext_ctx, Z3_mk_eq(ctx, x, z));
    /* assert x > 2 */
    c3 = assert_retractable_cnstr(ext_ctx, Z3_mk_gt(ctx, x, two));
    /* assert y < 1 */
    c4 = assert_retractable_cnstr(ext_ctx, Z3_mk_lt(ctx, y, one));
    
    result = ext_check(ext_ctx); 
    if (result != Z3_L_FALSE)
        exitf("bug in Z3");
    printf("unsat\n");

    retract_cnstr(ext_ctx, c4);
    result = ext_check(ext_ctx);
    if (result != Z3_L_TRUE)
        exitf("bug in Z3");
    printf("sat\n");

    reassert_cnstr(ext_ctx, c4);
    result = ext_check(ext_ctx);
    if (result != Z3_L_FALSE)
        exitf("bug in Z3");
    printf("unsat\n");

    retract_cnstr(ext_ctx, c2);
    result = ext_check(ext_ctx);
    if (result != Z3_L_FALSE)
        exitf("bug in Z3");
    printf("unsat\n");

    retract_cnstr(ext_ctx, c3);
    result = ext_check(ext_ctx);
    if (result != Z3_L_TRUE)
        exitf("bug in Z3");
    printf("sat\n");

    del_ext_context(ext_ctx);
}
void ite_example ( )

Test ite-term (if-then-else terms).

Definition at line 1771 of file test_capi.c.

{
    Z3_context ctx;
    Z3_ast f, one, zero, ite;
    
    printf("\nite_example\n");
    LOG_MSG("ite_example");

    ctx = mk_context();
    
    f    = Z3_mk_false(ctx);
    one  = mk_int(ctx, 1);
    zero = mk_int(ctx, 0);
    ite  = Z3_mk_ite(ctx, f, one, zero);
    
    printf("term: %s\n", Z3_ast_to_string(ctx, ite));

    /* delete logical context */
    Z3_del_context(ctx);
}
void list_example ( )

Create a list datatype.

Definition at line 1852 of file test_capi.c.

                    {
    Z3_context ctx = mk_context();
    Z3_sort int_ty, int_list;
    Z3_func_decl nil_decl, is_nil_decl, cons_decl, is_cons_decl, head_decl, tail_decl;
    Z3_ast nil, l1, l2, x, y, u, v, fml, fml1;
    Z3_ast ors[2];
    

    printf("\nlist_example\n");
    LOG_MSG("list_example");

    int_ty = Z3_mk_int_sort(ctx);

    int_list = Z3_mk_list_sort(ctx, Z3_mk_string_symbol(ctx, "int_list"), int_ty,
                               &nil_decl, &is_nil_decl, &cons_decl, &is_cons_decl, &head_decl, &tail_decl);
                    
    nil = Z3_mk_app(ctx, nil_decl, 0, 0);
    l1 = mk_binary_app(ctx, cons_decl, mk_int(ctx, 1), nil);
    l2 = mk_binary_app(ctx, cons_decl, mk_int(ctx, 2), nil);

    /* nil != cons(1, nil) */
    prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, l1)), Z3_TRUE);

    /* cons(2,nil) != cons(1, nil) */
    prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, l1, l2)), Z3_TRUE);

    /* cons(x,nil) = cons(y, nil) => x = y */
    x = mk_var(ctx, "x", int_ty);
    y = mk_var(ctx, "y", int_ty);    
    l1 = mk_binary_app(ctx, cons_decl, x, nil);
        l2 = mk_binary_app(ctx, cons_decl, y, nil);
    prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);

    /* cons(x,u) = cons(x, v) => u = v */
    u = mk_var(ctx, "u", int_list);
    v = mk_var(ctx, "v", int_list);    
    l1 = mk_binary_app(ctx, cons_decl, x, u);
        l2 = mk_binary_app(ctx, cons_decl, y, v);
    prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE);
    prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);

    /* is_nil(u) or is_cons(u) */
    ors[0] = Z3_mk_app(ctx, is_nil_decl, 1, &u);
    ors[1] = Z3_mk_app(ctx, is_cons_decl, 1, &u);
    prove(ctx, Z3_mk_or(ctx, 2, ors), Z3_TRUE);

    /* occurs check u != cons(x,u) */    
    prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE);

    /* destructors: is_cons(u) => u = cons(head(u),tail(u)) */
    fml1 = Z3_mk_eq(ctx, u, mk_binary_app(ctx, cons_decl, mk_unary_app(ctx, head_decl, u), mk_unary_app(ctx, tail_decl, u)));
    fml = Z3_mk_implies(ctx, Z3_mk_app(ctx, is_cons_decl, 1, &u), fml1);
    printf("Formula %s\n", Z3_ast_to_string(ctx, fml));
    prove(ctx, fml, Z3_TRUE);

    prove(ctx, fml1, Z3_FALSE);

    /* delete logical context */
    Z3_del_context(ctx);
}
Z3_ast mk_binary_app ( Z3_context  ctx,
Z3_func_decl  f,
Z3_ast  x,
Z3_ast  y 
)

Create the binary function application: (f x y).

Definition at line 171 of file test_capi.c.

Referenced by apply_compare_axiom_for_parents_of(), apply_unit_axiom_for_parents_of(), forest_example(), list_example(), pa_theory_example1(), pa_theory_example2(), quantifier_example1(), simple_example1(), simple_example2(), tree_example(), and tuple_example1().

{
    Z3_ast args[2] = {x, y};
    return Z3_mk_app(ctx, f, 2, args);
}
Z3_ast mk_bool_var ( Z3_context  ctx,
const char *  name 
)

Create a boolean variable using the given name.

Definition at line 126 of file test_capi.c.

{
    Z3_sort ty = Z3_mk_bool_sort(ctx);
    return mk_var(ctx, name, ty);
}
Z3_context mk_context ( )

Create a logical context.

Enable model construction only.

Also enable tracing to stderr and register standard error handler.

Definition at line 87 of file test_capi.c.

{
    Z3_config  cfg;
    Z3_context ctx;
    cfg = Z3_mk_config();
    ctx = mk_context_custom(cfg, error_handler);
    Z3_del_config(cfg);
    return ctx;
}
Z3_context mk_context_custom ( Z3_config  cfg,
Z3_error_handler  err 
)

Create a logical context.

Enable model construction. Other configuration parameters can be passed in the cfg variable.

Also enable tracing to stderr and register custom error handler.

Definition at line 69 of file test_capi.c.

Referenced by error_code_example1(), error_code_example2(), mk_context(), mk_proof_context(), parser_example3(), parser_example5(), and quantifier_example1().

{
    Z3_context ctx;
    
    Z3_set_param_value(cfg, "MODEL", "true");
    ctx = Z3_mk_context(cfg);
    Z3_set_error_handler(ctx, err);
    
    return ctx;
}
Z3_ext_context mk_ext_context ( )

Create a logical context wrapper with support for retractable constraints.

Definition at line 2323 of file test_capi.c.

Referenced by incremental_example1().

                                {
    Z3_ext_context ctx         = (Z3_ext_context) malloc(sizeof(Z3_ext_context_struct));
    ctx->m_context             = mk_context();
    ctx->m_num_answer_literals = 0;
    return ctx;
}
Z3_ast mk_int ( Z3_context  ctx,
int  v 
)

Create a Z3 integer node using a C int.

Definition at line 144 of file test_capi.c.

Referenced by binary_tree_example(), eval_example1(), find_model_example2(), incremental_example1(), ite_example(), list_example(), and prove_example2().

{
    Z3_sort ty = Z3_mk_int_sort(ctx);
    return Z3_mk_int(ctx, v, ty);
}
Z3_ast mk_int_var ( Z3_context  ctx,
const char *  name 
)

Create an integer variable using the given name.

Definition at line 135 of file test_capi.c.

Referenced by error_code_example2(), eval_example1(), find_model_example2(), get_implied_equalities_example(), incremental_example1(), parser_example2(), prove_example2(), quantifier_example1(), substitute_example(), and substitute_vars_example().

{
    Z3_sort ty = Z3_mk_int_sort(ctx);
    return mk_var(ctx, name, ty);
}
Z3_context mk_proof_context ( )

Create a logical context.

Enable fine-grained proof construction. Enable model construction.

Also enable tracing to stderr and register standard error handler.

Definition at line 105 of file test_capi.c.

Referenced by unsat_core_and_proof_example().

                              {
    Z3_config cfg = Z3_mk_config();
    Z3_context ctx;
    Z3_set_param_value(cfg, "PROOF_MODE", "2");
    ctx = mk_context_custom(cfg, throw_z3_error);
    Z3_del_config(cfg);
    return ctx;
}
Z3_ast mk_real_var ( Z3_context  ctx,
const char *  name 
)

Create a real variable using the given name.

Definition at line 153 of file test_capi.c.

Referenced by tuple_example1().

{
    Z3_sort ty = Z3_mk_real_sort(ctx);
    return mk_var(ctx, name, ty);
}
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.

update(t, i, new_val) is equivalent to mk_tuple(proj_0(t), ..., new_val, ..., proj_n(t))

Definition at line 388 of file test_capi.c.

Referenced by tuple_example1().

{
    Z3_sort         ty;
    Z3_func_decl   mk_tuple_decl;
    unsigned            num_fields, j;
    Z3_ast *            new_fields;
    Z3_ast              result;

    ty = Z3_get_sort(c, t);

    if (Z3_get_sort_kind(c, ty) != Z3_DATATYPE_SORT) {
        exitf("argument must be a tuple");
    }

    num_fields = Z3_get_tuple_sort_num_fields(c, ty);
    
    if (i >= num_fields) {
        exitf("invalid tuple update, index is too big");
    }
    
    new_fields = (Z3_ast*) malloc(sizeof(Z3_ast) * num_fields);
    for (j = 0; j < num_fields; j++) {
        if (i == j) {
            /* use new_val at position i */
            new_fields[j] = new_val;
        }
        else {
            /* use field j of t */
            Z3_func_decl proj_decl = Z3_get_tuple_sort_field_decl(c, ty, j);
            new_fields[j] = mk_unary_app(c, proj_decl, t);
        }
    }
    mk_tuple_decl = Z3_get_tuple_sort_mk_decl(c, ty);
    result = Z3_mk_app(c, mk_tuple_decl, num_fields, new_fields);
    free(new_fields);
    return result;
}
Z3_ast mk_unary_app ( Z3_context  ctx,
Z3_func_decl  f,
Z3_ast  x 
)

Create the unary function application: (f x).

Definition at line 162 of file test_capi.c.

Referenced by assert_inj_axiom(), binary_tree_example(), list_example(), mk_tuple_update(), prove_example1(), prove_example2(), simple_example2(), tree_example(), and tuple_example1().

{
    Z3_ast args[1] = {x};
    return Z3_mk_app(ctx, f, 1, args);
}
Z3_ast mk_var ( Z3_context  ctx,
const char *  name,
Z3_sort  ty 
)

Create a variable using the given name and type.

Definition at line 117 of file test_capi.c.

{
    Z3_symbol   s  = Z3_mk_string_symbol(ctx, name);
    return Z3_mk_const(ctx, s, ty);
}
void numeral_example ( )

Demonstrate different ways of creating rational numbers: decimal and fractional representations.

Definition at line 1745 of file test_capi.c.

                       {
    Z3_context ctx;
    Z3_ast n1, n2;
    Z3_sort real_ty;
    printf("\nnumeral_example\n");
    LOG_MSG("numeral_example");
    
    ctx        = mk_context();
    real_ty    = Z3_mk_real_sort(ctx);
    n1 = Z3_mk_numeral(ctx, "1/2", real_ty);
    n2 = Z3_mk_numeral(ctx, "0.5", real_ty);
    printf("Numerals n1:%s", Z3_ast_to_string(ctx, n1));
    printf(" n2:%s\n", Z3_ast_to_string(ctx, n2));
    prove(ctx, Z3_mk_eq(ctx, n1, n2), Z3_TRUE);

    n1 = Z3_mk_numeral(ctx, "-1/3", real_ty);
    n2 = Z3_mk_numeral(ctx, "-0.33333333333333333333333333333333333333333333333333", real_ty);
    printf("Numerals n1:%s", Z3_ast_to_string(ctx, n1));
    printf(" n2:%s\n", Z3_ast_to_string(ctx, n2));
    prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, n1, n2)), Z3_TRUE);
    Z3_del_context(ctx);
}
void parser_example1 ( )

Demonstrates how to use the SMTLIB parser.

Definition at line 1564 of file test_capi.c.

{
    Z3_context ctx;
    unsigned i, num_formulas;

    printf("\nparser_example1\n");
    LOG_MSG("parser_example1");
    
    ctx        = mk_context();
   
    Z3_parse_smtlib_string(ctx, 
                           "(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))",
                           0, 0, 0,
                           0, 0, 0);
    num_formulas = Z3_get_smtlib_num_formulas(ctx);
    for (i = 0; i < num_formulas; i++) {
        Z3_ast f = Z3_get_smtlib_formula(ctx, i);
        printf("formula %d: %s\n", i, Z3_ast_to_string(ctx, f));
        Z3_assert_cnstr(ctx, f);
    }
    
    check(ctx, Z3_L_TRUE);

    Z3_del_context(ctx);
}
void parser_example2 ( )

Demonstrates how to initialize the parser symbol table.

Definition at line 1593 of file test_capi.c.

{
    Z3_context ctx;
    Z3_ast x, y;
    Z3_symbol         names[2];
    Z3_func_decl decls[2];
    Z3_ast f;

    printf("\nparser_example2\n");
    LOG_MSG("parser_example2");

    ctx        = mk_context();

    /* Z3_enable_arithmetic doesn't need to be invoked in this example
       because it will be implicitly invoked by mk_int_var.
    */
    
    x        = mk_int_var(ctx, "x");
    decls[0] = Z3_get_app_decl(ctx, Z3_to_app(ctx, x));
    y        = mk_int_var(ctx, "y");
    decls[1] = Z3_get_app_decl(ctx, Z3_to_app(ctx, y));
    
    names[0] = Z3_mk_string_symbol(ctx, "a");
    names[1] = Z3_mk_string_symbol(ctx, "b");
    
    Z3_parse_smtlib_string(ctx, 
                           "(benchmark tst :formula (> a b))",
                           0, 0, 0,
                           /* 'x' and 'y' declarations are inserted as 'a' and 'b' into the parser symbol table. */
                           2, names, decls);
    f = Z3_get_smtlib_formula(ctx, 0);
    printf("formula: %s\n", Z3_ast_to_string(ctx, f));
    Z3_assert_cnstr(ctx, f);
    check(ctx, Z3_L_TRUE);

    Z3_del_context(ctx);
}
void parser_example3 ( )

Demonstrates how to initialize the parser symbol table.

Definition at line 1634 of file test_capi.c.

{
    Z3_config  cfg;
    Z3_context ctx;
    Z3_sort       int_sort;
    Z3_symbol     g_name;
    Z3_sort       g_domain[2];
    Z3_func_decl  g;
    Z3_ast        thm;

    printf("\nparser_example3\n");
    LOG_MSG("parser_example3");

    cfg = Z3_mk_config();
    /* See quantifer_example1 */
    Z3_set_param_value(cfg, "MODEL", "true");
    ctx = mk_context_custom(cfg, error_handler);
    Z3_del_config(cfg);

    /* declare function g */
    int_sort    = Z3_mk_int_sort(ctx);
    g_name      = Z3_mk_string_symbol(ctx, "g");
    g_domain[0] = int_sort;
    g_domain[1] = int_sort;
    g           = Z3_mk_func_decl(ctx, g_name, 2, g_domain, int_sort);
    
    assert_comm_axiom(ctx, g);

    Z3_parse_smtlib_string(ctx, 
                           "(benchmark tst :formula (forall (x Int) (y Int) (implies (= x y) (= (g x 0) (g 0 y)))))",
                           0, 0, 0,
                           1, &g_name, &g);
    thm = Z3_get_smtlib_formula(ctx, 0);
    printf("formula: %s\n", Z3_ast_to_string(ctx, thm));
    prove(ctx, thm, Z3_TRUE);

    Z3_del_context(ctx);
}
void parser_example4 ( )

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

Definition at line 1676 of file test_capi.c.

{
    Z3_context ctx;
    unsigned i, num_decls, num_assumptions, num_formulas;

    printf("\nparser_example4\n");
    LOG_MSG("parser_example4");
    
    ctx        = mk_context();
    
    Z3_parse_smtlib_string(ctx, 
                           "(benchmark tst :extrafuns ((x Int) (y Int)) :assumption (= x 20) :formula (> x y) :formula (> x 0))",
                           0, 0, 0,
                           0, 0, 0);
    num_decls = Z3_get_smtlib_num_decls(ctx);
    for (i = 0; i < num_decls; i++) {
        Z3_func_decl d = Z3_get_smtlib_decl(ctx, i);
        printf("declaration %d: %s\n", i, Z3_func_decl_to_string(ctx, d));
    }
    num_assumptions = Z3_get_smtlib_num_assumptions(ctx);
    for (i = 0; i < num_assumptions; i++) {
        Z3_ast a = Z3_get_smtlib_assumption(ctx, i);
        printf("assumption %d: %s\n", i, Z3_ast_to_string(ctx, a));
    }
    num_formulas = Z3_get_smtlib_num_formulas(ctx);
    for (i = 0; i < num_formulas; i++) {
        Z3_ast f = Z3_get_smtlib_formula(ctx, i);
        printf("formula %d: %s\n", i, Z3_ast_to_string(ctx, f));
    }
    Z3_del_context(ctx);
}
void parser_example5 ( )

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

Definition at line 1711 of file test_capi.c.

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

    printf("\nparser_example5\n");
    LOG_MSG("parser_example5");

    r = setjmp(g_catch_buffer);
    if (r == 0) {
        cfg = Z3_mk_config();
        ctx = mk_context_custom(cfg, throw_z3_error);
        Z3_del_config(cfg);
                
        Z3_parse_smtlib_string(ctx, 
                               /* the following string has a parsing error: missing parenthesis */
                               "(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))",
                               0, 0, 0,
                               0, 0, 0);
        unreachable();
        Z3_del_context(ctx);
    }
    else {
        printf("Z3 error: %s.\n", Z3_get_error_msg((Z3_error_code)r));
        if (ctx != NULL) {
            printf("Error message: '%s'.\n",Z3_get_smtlib_error(ctx));
            Z3_del_context(ctx);
        }
    }
}
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.

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

The context ctx is not modified by this function.

Definition at line 215 of file test_capi.c.

Referenced by array_example1(), binary_tree_example(), bitvector_example1(), enum_example(), forest_example(), list_example(), numeral_example(), parser_example3(), prove_example1(), prove_example2(), quantifier_example1(), tree_example(), and tuple_example1().

{
    Z3_model m;
    Z3_ast   not_f;

    /* save the current state of the context */
    Z3_push(ctx);

    not_f = Z3_mk_not(ctx, f);
    Z3_assert_cnstr(ctx, not_f);
    
    m = 0;
    
    switch (Z3_check_and_get_model(ctx, &m)) {
    case Z3_L_FALSE:
        /* proved */
        printf("valid\n");
        if (!is_valid) {
            exitf("unexpected result");
        }
        break;
    case Z3_L_UNDEF:
        /* Z3 failed to prove/disprove f. */
        printf("unknown\n");
        if (m != 0) {
            /* m should be viewed as a potential counterexample. */
            printf("potential counterexample:\n%s\n", Z3_model_to_string(ctx, m));
        }
        if (is_valid) {
            exitf("unexpected result");
        }
        break;
    case Z3_L_TRUE:
        /* disproved */
        printf("invalid\n");
        if (m) {
            /* the model returned by Z3 is a counterexample */
            printf("counterexample:\n%s\n", Z3_model_to_string(ctx, m));
        }
        if (is_valid) {
            exitf("unexpected result");
        }
        break;
    }

    if (m) {
        Z3_del_model(ctx, m);
    }

    /* restore context */
    Z3_pop(ctx, 1);
}
void prove_example1 ( )

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

{
    Z3_context ctx;
    Z3_symbol U_name, g_name, x_name, y_name;
    Z3_sort U;
    Z3_sort g_domain[1];
    Z3_func_decl g;
    Z3_ast x, y, gx, ggx, gy;
    Z3_ast eq, f;

    printf("\nprove_example1\n");
    LOG_MSG("prove_example1");
    
    ctx        = mk_context();
    
    /* create uninterpreted type. */
    U_name     = Z3_mk_string_symbol(ctx, "U");
    U          = Z3_mk_uninterpreted_sort(ctx, U_name);
    
    /* declare function g */
    g_name      = Z3_mk_string_symbol(ctx, "g");
    g_domain[0] = U;
    g           = Z3_mk_func_decl(ctx, g_name, 1, g_domain, U);

    /* create x and y */
    x_name      = Z3_mk_string_symbol(ctx, "x");
    y_name      = Z3_mk_string_symbol(ctx, "y");
    x           = Z3_mk_const(ctx, x_name, U);
    y           = Z3_mk_const(ctx, y_name, U);
    /* create g(x), g(y) */
    gx          = mk_unary_app(ctx, g, x);
    gy          = mk_unary_app(ctx, g, y);
    
    /* assert x = y */
    eq          = Z3_mk_eq(ctx, x, y);
    Z3_assert_cnstr(ctx, eq);

    /* prove g(x) = g(y) */
    f           = Z3_mk_eq(ctx, gx, gy);
    printf("prove: x = y implies g(x) = g(y)\n");
    prove(ctx, f, Z3_TRUE);

    /* create g(g(x)) */
    ggx         = mk_unary_app(ctx, g, gx);
    
    /* disprove g(g(x)) = g(y) */
    f           = Z3_mk_eq(ctx, ggx, gy);
    printf("disprove: x = y implies g(g(x)) = g(y)\n");
    prove(ctx, f, Z3_FALSE);

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

This example demonstrates how to combine uninterpreted functions and arithmetic.

Definition at line 871 of file test_capi.c.

{
    Z3_context ctx;
    Z3_sort int_sort;
    Z3_symbol g_name;
    Z3_sort g_domain[1];
    Z3_func_decl g;
    Z3_ast x, y, z, zero, minus_one, x_plus_z, gx, gy, gz, gx_gy, ggx_gy;
    Z3_ast args[2];
    Z3_ast eq, c1, c2, c3, f;

    printf("\nprove_example2\n");
    LOG_MSG("prove_example2");
    
    ctx        = mk_context();

    /* declare function g */
    int_sort    = Z3_mk_int_sort(ctx);
    g_name      = Z3_mk_string_symbol(ctx, "g");
    g_domain[0] = int_sort;
    g           = Z3_mk_func_decl(ctx, g_name, 1, g_domain, int_sort);
    
    /* create x, y, and z */
    x           = mk_int_var(ctx, "x");
    y           = mk_int_var(ctx, "y");
    z           = mk_int_var(ctx, "z");

    /* create gx, gy, gz */
    gx          = mk_unary_app(ctx, g, x);
    gy          = mk_unary_app(ctx, g, y);
    gz          = mk_unary_app(ctx, g, z);
    
    /* create zero */
    zero        = mk_int(ctx, 0);

    /* assert not(g(g(x) - g(y)) = g(z)) */
    args[0]     = gx;
    args[1]     = gy;
    gx_gy       = Z3_mk_sub(ctx, 2, args);
    ggx_gy      = mk_unary_app(ctx, g, gx_gy);
    eq          = Z3_mk_eq(ctx, ggx_gy, gz);
    c1          = Z3_mk_not(ctx, eq);
    Z3_assert_cnstr(ctx, c1);

    /* assert x + z <= y */
    args[0]     = x;
    args[1]     = z;
    x_plus_z    = Z3_mk_add(ctx, 2, args);
    c2          = Z3_mk_le(ctx, x_plus_z, y);
    Z3_assert_cnstr(ctx, c2);

    /* assert y <= x */
    c3          = Z3_mk_le(ctx, y, x);
    Z3_assert_cnstr(ctx, c3);

    /* prove z < 0 */
    f           = Z3_mk_lt(ctx, z, zero);
    printf("prove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0\n");
    prove(ctx, f, Z3_TRUE);

    /* disprove z < -1 */
    minus_one   = mk_int(ctx, -1);
    f           = Z3_mk_lt(ctx, z, minus_one);
    printf("disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1\n");
    prove(ctx, f, Z3_FALSE);

    Z3_del_context(ctx);
}
void push_pop_example1 ( )

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

{
    Z3_context ctx;
    Z3_sort int_sort;
    Z3_symbol x_sym, y_sym;
    Z3_ast x, y, big_number, three;
    Z3_ast c1, c2, c3;

    printf("\npush_pop_example1\n");
    LOG_MSG("push_pop_example1");

    ctx        = mk_context();

    /* create a big number */
    int_sort   = Z3_mk_int_sort(ctx);
    big_number = Z3_mk_numeral(ctx, "1000000000000000000000000000000000000000000000000000000", int_sort);
    
    /* create number 3 */
    three      = Z3_mk_numeral(ctx, "3", int_sort);

    /* create x */
    x_sym      = Z3_mk_string_symbol(ctx, "x");
    x          = Z3_mk_const(ctx, x_sym, int_sort);

    /* assert x >= "big number" */
    c1         = Z3_mk_ge(ctx, x, big_number);
    printf("assert: x >= 'big number'\n");
    Z3_assert_cnstr(ctx, c1);

    /* create a backtracking point */
    printf("push\n");
    Z3_push(ctx);

    printf("number of scopes: %d\n", Z3_get_num_scopes(ctx));

    /* assert x <= 3 */
    c2         = Z3_mk_le(ctx, x, three);
    printf("assert: x <= 3\n");
    Z3_assert_cnstr(ctx, c2);

    /* context is inconsistent at this point */
    check2(ctx, Z3_L_FALSE);

    /* backtrack: the constraint x <= 3 will be removed, since it was
       asserted after the last Z3_push. */
    printf("pop\n");
    Z3_pop(ctx, 1);

    printf("number of scopes: %d\n", Z3_get_num_scopes(ctx));


    /* the context is consistent again. */
    check2(ctx, Z3_L_TRUE);

    /* new constraints can be asserted... */
    
    /* create y */
    y_sym      = Z3_mk_string_symbol(ctx, "y");
    y          = Z3_mk_const(ctx, y_sym, int_sort);

    /* assert y > x */
    c3         = Z3_mk_gt(ctx, y, x);
    printf("assert: y > x\n");
    Z3_assert_cnstr(ctx, c3);

    /* the context is still consistent. */
    check2(ctx, Z3_L_TRUE);
    
    Z3_del_context(ctx);
}
void quantifier_example1 ( )

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

{
    Z3_config  cfg;
    Z3_context ctx;
    Z3_sort       int_sort;
    Z3_symbol         f_name;
    Z3_sort       f_domain[2];
    Z3_func_decl f;
    Z3_ast            x, y, w, v, fxy, fwv;
    Z3_ast            p1, p2, p3, not_p3;

    printf("\nquantifier_example1\n");
    LOG_MSG("quantifier_example1");

    cfg = Z3_mk_config();
    /* If quantified formulas are asserted in a logical context, then
       Z3 may return L_UNDEF. In this case, the model produced by Z3 should be viewed as a potential/candidate model.
    */
    Z3_set_param_value(cfg, "MODEL", "true");
    /*
       The current model finder for quantified formulas cannot handle injectivity.
       So, we are limiting the number of iterations to avoid a long "wait".
    */
    Z3_set_param_value(cfg, "MBQI_MAX_ITERATIONS", "10");
    ctx = mk_context_custom(cfg, error_handler);
    Z3_del_config(cfg);

    /* declare function f */
    int_sort    = Z3_mk_int_sort(ctx);
    f_name      = Z3_mk_string_symbol(ctx, "f");
    f_domain[0] = int_sort;
    f_domain[1] = int_sort;
    f           = Z3_mk_func_decl(ctx, f_name, 2, f_domain, int_sort);
  
    /* assert that f is injective in the second argument. */
    assert_inj_axiom(ctx, f, 1);
    
    /* create x, y, v, w, fxy, fwv */
    x           = mk_int_var(ctx, "x");
    y           = mk_int_var(ctx, "y");
    v           = mk_int_var(ctx, "v");
    w           = mk_int_var(ctx, "w");
    fxy         = mk_binary_app(ctx, f, x, y);
    fwv         = mk_binary_app(ctx, f, w, v);
    
    /* assert f(x, y) = f(w, v) */
    p1          = Z3_mk_eq(ctx, fxy, fwv);
    Z3_assert_cnstr(ctx, p1);

    /* prove f(x, y) = f(w, v) implies y = v */
    p2          = Z3_mk_eq(ctx, y, v);
    printf("prove: f(x, y) = f(w, v) implies y = v\n");
    prove(ctx, p2, Z3_TRUE);

    /* disprove f(x, y) = f(w, v) implies x = w */
    /* using check2 instead of prove */
    p3          = Z3_mk_eq(ctx, x, w);
    not_p3      = Z3_mk_not(ctx, p3);
    Z3_assert_cnstr(ctx, not_p3);
    printf("disprove: f(x, y) = f(w, v) implies x = w\n");
    printf("that is: not(f(x, y) = f(w, v) implies x = w) is satisfiable\n");
    check2(ctx, Z3_L_UNDEF);
    printf("reason for last failure: %d (7 = quantifiers)\n", 
           Z3_get_search_failure(ctx));
    if (Z3_get_search_failure(ctx) != Z3_QUANTIFIERS) {
        exitf("unexpected result");
    }

    Z3_del_context(ctx);
}
void reassert_cnstr ( Z3_ext_context  ctx,
unsigned  id 
)

Reassert a constraint retracted using retract_cnstr.

Definition at line 2377 of file test_capi.c.

Referenced by incremental_example1().

                                                     {
    if (id >= ctx->m_num_answer_literals) {
        exitf("invalid constraint id.");
    }
    ctx->m_retracted[id] = Z3_FALSE;
}
void reference_counter_example ( )

Simple example showing how to use reference counters in Z3 to manage memory efficiently.

Definition at line 2496 of file test_capi.c.

                                 {
    Z3_config cfg;
    Z3_context ctx;
    Z3_sort ty;
    Z3_ast x, y, x_xor_y;
    Z3_symbol sx, sy;

    printf("\nreference_counter_example\n");
    LOG_MSG("reference_counter_example");

    cfg                = Z3_mk_config();
    Z3_set_param_value(cfg, "MODEL", "true");
    // Create a Z3 context where the user is reponsible for managing
    // Z3_ast reference counters.
    ctx                = Z3_mk_context_rc(cfg);
    Z3_del_config(cfg); 

    ty      = Z3_mk_bool_sort(ctx);
    Z3_inc_ref(ctx, Z3_sort_to_ast(ctx, ty)); // Z3_sort_to_ast(ty) is just syntax sugar for ((Z3_ast) ty)
    sx      = Z3_mk_string_symbol(ctx, "x");
    // Z3_symbol is not a Z3_ast. No reference counting is not needed.
    x       = Z3_mk_const(ctx, sx, ty);
    Z3_inc_ref(ctx, x);
    sy      = Z3_mk_string_symbol(ctx, "y");
    y       = Z3_mk_const(ctx, sy, ty);
    Z3_inc_ref(ctx, y);
    // ty is not needed anymore.
    Z3_dec_ref(ctx, Z3_sort_to_ast(ctx, ty)); 
    x_xor_y = Z3_mk_xor(ctx, x, y);
    Z3_inc_ref(ctx, x_xor_y);
    // x and y are not needed anymore.
    Z3_dec_ref(ctx, x); 
    Z3_dec_ref(ctx, y);
    Z3_assert_cnstr(ctx, x_xor_y);
    // x_or_y is not needed anymore.
    Z3_dec_ref(ctx, x_xor_y); 
    
    printf("model for: x xor y\n");
    check(ctx, Z3_L_TRUE);

    // Test push & pop
    Z3_push(ctx);
    Z3_pop(ctx, 1);

    Z3_del_context(ctx);
}
void retract_cnstr ( Z3_ext_context  ctx,
unsigned  id 
)

Retract an constraint asserted using assert_retractable_cnstr.

Definition at line 2367 of file test_capi.c.

Referenced by incremental_example1().

                                                    {
    if (id >= ctx->m_num_answer_literals) {
        exitf("invalid constraint id.");
    }
    ctx->m_retracted[id] = Z3_TRUE;
}
void simple_example ( )

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

Definition at line 663 of file test_capi.c.

{
    Z3_context ctx;
    LOG_MSG("simple_example");
    printf("\nsimple_example\n");
 
    ctx = mk_context();

    /* do something with the context */
    printf("CONTEXT:\n%sEND OF CONTEXT\n", Z3_context_to_string(ctx));

    /* delete logical context */
    Z3_del_context(ctx);
}
void smt2parser_example ( )

Demonstrates how to use SMT2 parser.

Definition at line 2546 of file test_capi.c.

                          {
    Z3_context ctx;
    Z3_ast fs;
    printf("\nsmt2parser_example\n");
    LOG_MSG("smt2parser_example");

    ctx = mk_context();
    fs  = Z3_parse_smtlib2_string(ctx, "(declare-fun a () (_ BitVec 8)) (assert (bvuge a #x10)) (assert (bvule a #xf0))", 0, 0, 0, 0, 0, 0);
    printf("formulas: %s\n", Z3_ast_to_string(ctx, fs));
    Z3_del_context(ctx);
}
void substitute_example ( )

Demonstrates how to use the function Z3_substitute to replace subexpressions in a Z3 AST.

Definition at line 2561 of file test_capi.c.

                          {
    Z3_context ctx;
    Z3_sort int_ty;
    Z3_ast a, b;
    Z3_func_decl f;
    Z3_func_decl g;
    Z3_ast fab, ga, ffabga, r;

    printf("\nsubstitute_example\n");
    LOG_MSG("substitute_example");

    ctx = mk_context();
    int_ty = Z3_mk_int_sort(ctx);
    a = mk_int_var(ctx,"a");
    b = mk_int_var(ctx,"b");
    { 
        Z3_sort f_domain[2] = { int_ty, int_ty };
        f = Z3_mk_func_decl(ctx, Z3_mk_string_symbol(ctx, "f"), 2, f_domain, int_ty);
    }
    g = Z3_mk_func_decl(ctx, Z3_mk_string_symbol(ctx, "g"), 1, &int_ty, int_ty);
    { 
        Z3_ast args[2] = { a, b };
        fab = Z3_mk_app(ctx, f, 2, args);
    }
    ga = Z3_mk_app(ctx, g, 1, &a);
    {
        Z3_ast args[2] = { fab, ga };
        ffabga = Z3_mk_app(ctx, f, 2, args);
    }
    // Replace b -> 0, g(a) -> 1 in f(f(a, b), g(a))
    {
        Z3_ast zero = Z3_mk_numeral(ctx, "0", int_ty);
        Z3_ast one  = Z3_mk_numeral(ctx, "1", int_ty);
        Z3_ast from[2] = { b, ga };
        Z3_ast to[2] = { zero, one };
        r = Z3_substitute(ctx, ffabga, 2, from, to);
    }
    // Display r
    printf("substitution result: %s\n", Z3_ast_to_string(ctx, r));
    Z3_del_context(ctx);
}
void substitute_vars_example ( )

Demonstrates how to use the function Z3_substitute_vars to replace (free) variables with expressions in a Z3 AST.

Definition at line 2606 of file test_capi.c.

                               {
    Z3_context ctx;
    Z3_sort int_ty;
    Z3_ast x0, x1;
    Z3_ast a, b, gb;
    Z3_func_decl f;
    Z3_func_decl g;
    Z3_ast f01, ff010, r;

    printf("\nsubstitute_vars_example\n");
    LOG_MSG("substitute_vars_example");

    ctx = mk_context();
    int_ty = Z3_mk_int_sort(ctx);
    x0 = Z3_mk_bound(ctx, 0, int_ty);
    x1 = Z3_mk_bound(ctx, 1, int_ty);
    { 
        Z3_sort f_domain[2] = { int_ty, int_ty };
        f = Z3_mk_func_decl(ctx, Z3_mk_string_symbol(ctx, "f"), 2, f_domain, int_ty);
    }
    g = Z3_mk_func_decl(ctx, Z3_mk_string_symbol(ctx, "g"), 1, &int_ty, int_ty);
    { 
        Z3_ast args[2] = { x0, x1 };
        f01 = Z3_mk_app(ctx, f, 2, args);
    }
    {
        Z3_ast args[2] = { f01, x0 };
        ff010 = Z3_mk_app(ctx, f, 2, args);
    }
    a = mk_int_var(ctx, "a");
    b = mk_int_var(ctx, "b");
    gb = Z3_mk_app(ctx, g, 1, &b);
    // Replace x0 -> a, x1 -> g(b) in f(f(x0,x1),x0)
    {
        Z3_ast to[2] = { a, gb };
        r = Z3_substitute_vars(ctx, ff010, 2, to);
    }
    // Display r
    printf("substitution result: %s\n", Z3_ast_to_string(ctx, r));
    Z3_del_context(ctx);
}
void throw_z3_error ( Z3_context  c,
Z3_error_code  e 
)

Low tech exceptions.

In high-level programming languages, an error handler can throw an exception.

Definition at line 57 of file test_capi.c.

Referenced by error_code_example2(), mk_proof_context(), and parser_example5().

{
    longjmp(g_catch_buffer, e);
}
void tree_example ( )

Create a binary tree datatype.

Definition at line 1916 of file test_capi.c.

                    {
    Z3_context ctx = mk_context();
    Z3_sort cell;
    Z3_func_decl nil_decl, is_nil_decl, cons_decl, is_cons_decl, car_decl, cdr_decl;
    Z3_ast nil, l1, l2, x, y, u, v, fml, fml1;
    Z3_symbol head_tail[2] = { Z3_mk_string_symbol(ctx, "car"), Z3_mk_string_symbol(ctx, "cdr") };
    Z3_sort sorts[2] = { 0, 0 };
    unsigned sort_refs[2] = { 0, 0 };
    Z3_constructor nil_con, cons_con;
    Z3_constructor constructors[2];
    Z3_func_decl cons_accessors[2];
    Z3_ast ors[2];

    printf("\ntree_example\n");
    LOG_MSG("tree_example");

    nil_con  = Z3_mk_constructor(ctx, Z3_mk_string_symbol(ctx, "nil"), Z3_mk_string_symbol(ctx, "is_nil"), 0, 0, 0, 0);
    cons_con = Z3_mk_constructor(ctx, Z3_mk_string_symbol(ctx, "cons"), Z3_mk_string_symbol(ctx, "is_cons"), 2, head_tail, sorts, sort_refs);
    constructors[0] = nil_con;
    constructors[1] = cons_con;
    
    cell = Z3_mk_datatype(ctx, Z3_mk_string_symbol(ctx, "cell"), 2, constructors);

    Z3_query_constructor(ctx, nil_con, 0, &nil_decl, &is_nil_decl, 0);
    Z3_query_constructor(ctx, cons_con, 2, &cons_decl, &is_cons_decl, cons_accessors);
    car_decl = cons_accessors[0];
    cdr_decl = cons_accessors[1];

    Z3_del_constructor(ctx,nil_con);
    Z3_del_constructor(ctx,cons_con);


    nil = Z3_mk_app(ctx, nil_decl, 0, 0);
    l1 = mk_binary_app(ctx, cons_decl, nil, nil);
    l2 = mk_binary_app(ctx, cons_decl, l1, nil);

    /* nil != cons(nil, nil) */
    prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, nil, l1)), Z3_TRUE);

    /* cons(x,u) = cons(x, v) => u = v */
    u = mk_var(ctx, "u", cell);
    v = mk_var(ctx, "v", cell);    
    x = mk_var(ctx, "x", cell);
    y = mk_var(ctx, "y", cell);    
    l1 = mk_binary_app(ctx, cons_decl, x, u);
    l2 = mk_binary_app(ctx, cons_decl, y, v);
    prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, u, v)), Z3_TRUE);
    prove(ctx, Z3_mk_implies(ctx, Z3_mk_eq(ctx,l1,l2), Z3_mk_eq(ctx, x, y)), Z3_TRUE);

    /* is_nil(u) or is_cons(u) */
    ors[0] = Z3_mk_app(ctx, is_nil_decl, 1, &u);
    ors[1] = Z3_mk_app(ctx, is_cons_decl, 1, &u);
    prove(ctx, Z3_mk_or(ctx, 2, ors), Z3_TRUE);

    /* occurs check u != cons(x,u) */    
    prove(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, u, l1)), Z3_TRUE);

    /* destructors: is_cons(u) => u = cons(car(u),cdr(u)) */
    fml1 = Z3_mk_eq(ctx, u, mk_binary_app(ctx, cons_decl, mk_unary_app(ctx, car_decl, u), mk_unary_app(ctx, cdr_decl, u)));
    fml = Z3_mk_implies(ctx, Z3_mk_app(ctx, is_cons_decl, 1, &u), fml1);
    printf("Formula %s\n", Z3_ast_to_string(ctx, fml));
    prove(ctx, fml, Z3_TRUE);

    prove(ctx, fml1, Z3_FALSE);

    /* delete logical context */
    Z3_del_context(ctx);


}
void tuple_example1 ( )

Simple tuple type example. It creates a tuple that is a pair of real numbers.

Definition at line 1233 of file test_capi.c.

{
    Z3_context         ctx;
    Z3_sort        real_sort, pair_sort;
    Z3_symbol          mk_tuple_name;
    Z3_func_decl  mk_tuple_decl;
    Z3_symbol          proj_names[2]; 
    Z3_sort        proj_sorts[2]; 
    Z3_func_decl  proj_decls[2];
    Z3_func_decl  get_x_decl, get_y_decl;

    printf("\ntuple_example1\n");
    LOG_MSG("tuple_example1");
    
    ctx       = mk_context();

    real_sort = Z3_mk_real_sort(ctx);

    /* Create pair (tuple) type */
    mk_tuple_name = Z3_mk_string_symbol(ctx, "mk_pair");
    proj_names[0] = Z3_mk_string_symbol(ctx, "get_x");
    proj_names[1] = Z3_mk_string_symbol(ctx, "get_y");
    proj_sorts[0] = real_sort;
    proj_sorts[1] = real_sort;
    /* Z3_mk_tuple_sort will set mk_tuple_decl and proj_decls */
    pair_sort     = Z3_mk_tuple_sort(ctx, mk_tuple_name, 2, proj_names, proj_sorts, &mk_tuple_decl, proj_decls);
    get_x_decl    = proj_decls[0]; /* function that extracts the first element of a tuple. */
    get_y_decl    = proj_decls[1]; /* function that extracts the second element of a tuple. */
    
    printf("tuple_sort: ");
    display_sort(ctx, stdout, pair_sort);
    printf("\n");

    {
        /* prove that get_x(mk_pair(x,y)) == 1 implies x = 1*/
        Z3_ast app1, app2, x, y, one;
        Z3_ast eq1, eq2, eq3, thm;
        
        x    = mk_real_var(ctx, "x");
        y    = mk_real_var(ctx, "y");
        app1 = mk_binary_app(ctx, mk_tuple_decl, x, y);
        app2 = mk_unary_app(ctx, get_x_decl, app1); 
        one  = Z3_mk_numeral(ctx, "1", real_sort);
        eq1  = Z3_mk_eq(ctx, app2, one);
        eq2  = Z3_mk_eq(ctx, x, one);
        thm  = Z3_mk_implies(ctx, eq1, eq2);
        printf("prove: get_x(mk_pair(x, y)) = 1 implies x = 1\n");
        prove(ctx, thm, Z3_TRUE);

        /* disprove that get_x(mk_pair(x,y)) == 1 implies y = 1*/
        eq3  = Z3_mk_eq(ctx, y, one);
        thm  = Z3_mk_implies(ctx, eq1, eq3);
        printf("disprove: get_x(mk_pair(x, y)) = 1 implies y = 1\n");
        prove(ctx, thm, Z3_FALSE);
    }

    {
        /* prove that get_x(p1) = get_x(p2) and get_y(p1) = get_y(p2) implies p1 = p2 */
        Z3_ast p1, p2, x1, x2, y1, y2;
        Z3_ast antecedents[2];
        Z3_ast antecedent, consequent, thm;
        
        p1             = mk_var(ctx, "p1", pair_sort);
        p2             = mk_var(ctx, "p2", pair_sort);
        x1             = mk_unary_app(ctx, get_x_decl, p1);
        y1             = mk_unary_app(ctx, get_y_decl, p1);
        x2             = mk_unary_app(ctx, get_x_decl, p2);
        y2             = mk_unary_app(ctx, get_y_decl, p2);
        antecedents[0] = Z3_mk_eq(ctx, x1, x2);
        antecedents[1] = Z3_mk_eq(ctx, y1, y2);
        antecedent     = Z3_mk_and(ctx, 2, antecedents);
        consequent     = Z3_mk_eq(ctx, p1, p2);
        thm            = Z3_mk_implies(ctx, antecedent, consequent);
        printf("prove: get_x(p1) = get_x(p2) and get_y(p1) = get_y(p2) implies p1 = p2\n");
        prove(ctx, thm, Z3_TRUE);

        /* disprove that get_x(p1) = get_x(p2) implies p1 = p2 */
        thm            = Z3_mk_implies(ctx, antecedents[0], consequent);
        printf("disprove: get_x(p1) = get_x(p2) implies p1 = p2\n");
        prove(ctx, thm, Z3_FALSE);
    }

    {
        /* demonstrate how to use the mk_tuple_update function */
        /* prove that p2 = update(p1, 0, 10) implies get_x(p2) = 10 */
        Z3_ast p1, p2, one, ten, updt, x, y;
        Z3_ast antecedent, consequent, thm;

        p1             = mk_var(ctx, "p1", pair_sort);
        p2             = mk_var(ctx, "p2", pair_sort);
        one            = Z3_mk_numeral(ctx, "1", real_sort);
        ten            = Z3_mk_numeral(ctx, "10", real_sort);
        updt           = mk_tuple_update(ctx, p1, 0, ten);
        antecedent     = Z3_mk_eq(ctx, p2, updt);
        x              = mk_unary_app(ctx, get_x_decl, p2);
        consequent     = Z3_mk_eq(ctx, x, ten);
        thm            = Z3_mk_implies(ctx, antecedent, consequent);
        printf("prove: p2 = update(p1, 0, 10) implies get_x(p2) = 10\n");
        prove(ctx, thm, Z3_TRUE);

        /* disprove that p2 = update(p1, 0, 10) implies get_y(p2) = 10 */
        y              = mk_unary_app(ctx, get_y_decl, p2);
        consequent     = Z3_mk_eq(ctx, y, ten);
        thm            = Z3_mk_implies(ctx, antecedent, consequent);
        printf("disprove: p2 = update(p1, 0, 10) implies get_y(p2) = 10\n");
        prove(ctx, thm, Z3_FALSE);
    }

    Z3_del_context(ctx);
}
void two_contexts_example1 ( )

Several logical context can be used simultaneously.

Definition at line 1458 of file test_capi.c.

{
    Z3_context ctx1, ctx2;
    Z3_ast x1, x2;

    printf("\ntwo_contexts_example1\n");
    LOG_MSG("two_contexts_example1");

    /* using the same (default) configuration to initialized both logical contexts. */
    ctx1 = mk_context();
    ctx2 = mk_context();
    
    x1 = Z3_mk_const(ctx1, Z3_mk_int_symbol(ctx1,0), Z3_mk_bool_sort(ctx1));
    x2 = Z3_mk_const(ctx2, Z3_mk_int_symbol(ctx2,0), Z3_mk_bool_sort(ctx2));

    Z3_del_context(ctx1);
    
    /* ctx2 can still be used. */
    printf("%s\n", Z3_ast_to_string(ctx2, x2));
    
    Z3_del_context(ctx2);
}
void unreachable ( )

exit if unreachable code was reached.

Definition at line 37 of file test_capi.c.

Referenced by display_symbol(), error_code_example2(), and parser_example5().

{
    exitf("unreachable code was reached");
}
void unsat_core_and_proof_example ( )

Prove a theorem and extract, and print the proof.

This example illustrates the use of Z3_check_assumptions.

Definition at line 2184 of file test_capi.c.

                                    {
    Z3_context ctx = mk_proof_context();
    Z3_ast pa = mk_bool_var(ctx, "PredA");
    Z3_ast pb = mk_bool_var(ctx, "PredB");
    Z3_ast pc = mk_bool_var(ctx, "PredC");
    Z3_ast pd = mk_bool_var(ctx, "PredD");
    Z3_ast p1 = mk_bool_var(ctx, "P1");
    Z3_ast p2 = mk_bool_var(ctx, "P2");
    Z3_ast p3 = mk_bool_var(ctx, "P3");
    Z3_ast p4 = mk_bool_var(ctx, "P4");
    Z3_ast assumptions[4] = { Z3_mk_not(ctx, p1), Z3_mk_not(ctx, p2), Z3_mk_not(ctx, p3), Z3_mk_not(ctx, p4) };
    Z3_ast args1[3] = { pa, pb, pc };
    Z3_ast f1 = Z3_mk_and(ctx, 3, args1);
    Z3_ast args2[3] = { pa, Z3_mk_not(ctx, pb), pc };
    Z3_ast f2 = Z3_mk_and(ctx, 3, args2);
    Z3_ast args3[2] = { Z3_mk_not(ctx, pa), Z3_mk_not(ctx, pc) };
    Z3_ast f3 = Z3_mk_or(ctx, 2, args3);
    Z3_ast f4 = pd;
    Z3_ast g1[2] = { f1, p1 };
    Z3_ast g2[2] = { f2, p2 };
    Z3_ast g3[2] = { f3, p3 };
    Z3_ast g4[2] = { f4, p4 };    
    Z3_ast core[4] = { 0, 0, 0, 0 };
    unsigned core_size = 4;
    Z3_ast proof;
    Z3_model m      = 0;
    Z3_lbool result;
    unsigned i;

    printf("\nunsat_core_and_proof_example\n");
    LOG_MSG("unsat_core_and_proof_example");
    
    Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, g1));
    Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, g2));
    Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, g3));
    Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, g4));

    result = Z3_check_assumptions(ctx, 4, assumptions, &m, &proof, &core_size, core);

    switch (result) {
    case Z3_L_FALSE:
        printf("unsat\n");
        printf("proof: %s\n", Z3_ast_to_string(ctx, proof));

        printf("\ncore:\n");
        for (i = 0; i < core_size; ++i) {
                        printf("%s\n", Z3_ast_to_string(ctx, core[i]));
        }
        printf("\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(ctx, m);
    }

    /* delete logical context */
    Z3_del_context(ctx);
}
Last modified Fri Oct 5 2012 11:32:38