Z3 Microsoft Research
Functions
Theory plugin examples

Functions

void exitf (const char *message)
 exit gracefully in case of error.
void error_handler (Z3_context ctx, Z3_error_code e)
 Simpler error handler.
Z3_context mk_context_custom (Z3_config cfg, Z3_error_handler err)
 Create a logical context.
Z3_context mk_context ()
 Create a logical context.
Z3_ast mk_var (Z3_context ctx, const char *name, Z3_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_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 display_eqc (Z3_theory t, Z3_ast n)
 Display equivalence class containing n.
void display_eqc_parents (Z3_theory t, Z3_ast n)
 Display the parent theory operators of the equivalence class containing n.
Z3_ast get_eqc_value (Z3_theory t, Z3_ast n)
 If the equivalence class containing n contains a theory value, then return it. Otherwise, return 0.

Simple Theory

The theory has a binary function f, and a unit element u. The theory axioms are:

  • forall X. f(X, u) = X
  • forall X. f(u, X) = X
  • forall X. p(X, X)
typedef struct _SimpleTheoryData SimpleTheoryData
 Data-structure for storing theory specific data.
void Th_delete (Z3_theory t)
 Callback: invoked when t is deleted. This callback can be used to free theory specific data-structures.
Z3_bool Th_reduce_app (Z3_theory t, Z3_func_decl d, unsigned n, Z3_ast const args[], Z3_ast *result)
 The reduce_app callback can be used to extend Z3's simplifier. The simplifier is used to preprocess formulas.
void Th_new_app (Z3_theory t, Z3_ast n)
 Callback: invoked when n is finally added to the logical context. n is an application of the form g(...) where g is an interpreted function symbol of t.
void Th_new_elem (Z3_theory t, Z3_ast n)
 Callback: invoked when n is finally added to the logical context. n is an expression of sort s, where s is an interpreted sort of t.
void Th_init_search (Z3_theory t)
 Callback: invoked when Z3 starts the search for a satisfying assignment.
void Th_push (Z3_theory t)
 Callback: invoked when Z3 creates a case-split (aka backtracking point).
void Th_pop (Z3_theory t)
 Callback: invoked when Z3 backtracks a case-split.
void Th_reset (Z3_theory t)
 Callback: invoked when the logical context containing t is reset.
void Th_restart (Z3_theory t)
 Callback: invoked when Z3 restarts the search for a satisfying assignment.
void apply_unit_axiom_for_parents_of (Z3_theory t, Z3_ast n)
 Instantiate the unit axiom for the parents of n because n is now equal to unit u in the logical context.
void Th_new_eq (Z3_theory t, Z3_ast n1, Z3_ast n2)
 Callback: invoked when n1 = n2 is true in the logical context.
void Th_new_diseq (Z3_theory t, Z3_ast n1, Z3_ast n2)
 Callback: invoked when n1 = n2 is false in the logical context.
void Th_new_relevant (Z3_theory t, Z3_ast n)
 Callback: invoked when n becomes relevant in the current search branch. Irrelevant expressions may be ignored by the theory solver.
void Th_new_assignment (Z3_theory t, Z3_ast n, Z3_bool v)
 Callback: invoked when n is assigned to true/false.
Z3_bool Th_final_check (Z3_theory t)
 Callback: invoked before Z3 starts building a model. This callback can be used to perform expensive operations lazily.
Z3_theory mk_simple_theory (Z3_context ctx)
 Simple theory example. The theory has a binary function f, and a unit element u.
void simple_example1 ()
 Test simple theory simplifier.
void simple_example2 ()
 Test simple theory.

Procedural Attachment Example

The API for creating external theories can be used to implement procedural attachments in Z3. The idea is to use C functions to give the interpretation of function and predicate symbols.

The general template consists in:

  • Defining theory values for each C value that we want to manipulate in a Z3 formula. These values may be created on demand.
  • Defining a theory function declaration for each C function we want to make available in a Z3 formula.

In this file, we show how to create a procedural attachment for the C function strcmp. Our theory provides a function for creating string values, and the implementation consists in the following simple rule:

  t1 = str_value1
  t2 = str_value2
  strcmp(str_of(str_value1), str_of(str_value2)) == 0
  ===>
  Compare(t1, t2) = true
  

This rule should be read as

  IF

  • the term t1 is known to be equal to a theory value str_value1, and
  • the term t2 is known to be equal to a theory value str_value2, and
  • the C function strcmp returns 0 when the strings associated with str_value1 and str_value2 are used as arguments THEN
  • The theory atom Compare(t1, t2) must be true.
  Similarly, we have
  
  c1 = str_value1
  c2 = str_value2
  strcmp(str_of(str_value1), str_of(str_value2)) != 0
  ===>
  Compare(v1, v2) = false
  
  This solution has its limitations. For example, the theory does not restrict
  the interpretation of Compare(t1, t2) when t1 and t2 are
  not known to be equal to any theory value. Our example solver will simply
  return unknown in this case.
typedef struct _PATheoryData PATheoryData
 Theory specific data-structures.
Z3_ast PATh_mk_string_value (Z3_theory t, char const *str)
 Create a new string interpreted value using the C string str.
void PATh_delete (Z3_theory t)
 Callback: delete for PATheory.
Z3_lbool Compare (Z3_theory t, Z3_ast n1, Z3_ast n2)
 Compare the theory values in the equivalence classes of n1 and n2 using strcmp.
Z3_bool PATh_reduce_app (Z3_theory t, Z3_func_decl d, unsigned n, Z3_ast const args[], Z3_ast *result)
 Callback: reduce_app for PATheory.
void apply_compare_axiom_for_parents_of (Z3_theory t, Z3_ast n, Z3_ast v)
 Try to apply Compare axiom using the fact that n = v, where v is a theory value.
void PATh_new_eq (Z3_theory t, Z3_ast n1, Z3_ast n2)
 Callback: new_eq for PATheory.
Z3_bool PATh_final_check (Z3_theory t)
 Callback: final_check for PATheory.
Z3_theory mk_pa_theory (Z3_context ctx)
 Procedural attachment theory example.
void pa_theory_example1 ()
 Test Procedural Attachment Theory Simplifier.
void pa_theory_example2 (int assert_b_eq_hello)
 Test Procedural Attachment Theory.
void model_display_example ()
 Simple example to display model.

Typedef Documentation

typedef struct _PATheoryData PATheoryData

Theory specific data-structures.

Definition at line 623 of file test_user_theory.c.

typedef struct _SimpleTheoryData SimpleTheoryData

Data-structure for storing theory specific data.

Definition at line 239 of file test_user_theory.c.


Function Documentation

void apply_compare_axiom_for_parents_of ( Z3_theory  t,
Z3_ast  n,
Z3_ast  v 
)

Try to apply Compare axiom using the fact that n = v, where v is a theory value.

Definition at line 704 of file test_user_theory.c.

Referenced by PATh_new_eq().

                                                                         {
    PATheoryData * td = (PATheoryData*)Z3_theory_get_ext_data(t);
    Z3_context c = Z3_theory_get_context(t);
    Z3_ast n_prime = Z3_theory_get_eqc_root(t, n);
    do {
        unsigned num_parents = Z3_theory_get_num_parents(t, n_prime);
        unsigned i;
        for (i = 0; i < num_parents; i++) {
            Z3_app parent = Z3_to_app(c, Z3_theory_get_parent(t, n_prime, i));
            if (Z3_get_app_decl(c, parent) == td->Compare) {
                Z3_ast arg1 = Z3_get_app_arg(c, parent, 0);
                Z3_ast arg2 = Z3_get_app_arg(c, parent, 1);
                if (Z3_theory_get_eqc_root(t, arg1) == n)
                    arg1 = v;
                else
                    arg1 = get_eqc_value(t, arg1);
                if (Z3_theory_get_eqc_root(t, arg2) == n)
                    arg2 = v;
                else
                    arg2 = get_eqc_value(t, arg2);
                if (arg1 != 0 && arg2 != 0) {
                    switch (Compare(t, arg1, arg2)) {
                    case Z3_L_TRUE:
                        // assert axiom: Compare(arg1, arg2)
                        Z3_theory_assert_axiom(t, mk_binary_app(c, td->Compare, arg1, arg2));
                        break;
                    case Z3_L_FALSE:
                        // assert axiom: !Compare(arg1, arg2)
                        Z3_theory_assert_axiom(t, Z3_mk_not(c, mk_binary_app(c, td->Compare, arg1, arg2)));
                        break;
                    case Z3_L_UNDEF:
                        // do nothing
                        break; 
                    }
                }
            }
        }
        n_prime = Z3_theory_get_eqc_next(t, n_prime);
    }
    while (n_prime != n);
}
void apply_unit_axiom_for_parents_of ( Z3_theory  t,
Z3_ast  n 
)

Instantiate the unit axiom for the parents of n because n is now equal to unit u in the logical context.

Definition at line 336 of file test_user_theory.c.

Referenced by Th_new_eq().

                                                            {
    SimpleTheoryData * td = (SimpleTheoryData*)Z3_theory_get_ext_data(t);
    Z3_context c = Z3_theory_get_context(t);
    /*
      The following idiom is the standard approach for traversing
      applications of the form
      
      g(..., n', ...) 
      where
      - g is an interpreted function symbol of \c t.
      - n' is in the same equivalence class of n.
    */
    Z3_ast n_prime = n;
    do {
        unsigned num_parents = Z3_theory_get_num_parents(t, n_prime);
        unsigned i;
        for (i = 0; i < num_parents; i++) {
            Z3_app parent = Z3_to_app(c, Z3_theory_get_parent(t, n_prime, i));
            /* check whether current parent is of the form f(a, n_prime) */
            if (Z3_get_app_decl(c, parent) == td->f && Z3_get_app_arg(c, parent, 1) == n_prime) {
                /* assert f(a, u) = a */
                Z3_ast a = Z3_get_app_arg(c, parent, 0);
                Z3_theory_assert_axiom(t, Z3_mk_eq(c, mk_binary_app(c, td->f, a, td->u), a));
                /* Instead of asserting f(a, u) = a, we could also have asserted
                   the clause:
                   (not (n_prime = u)) or (f(a, n_prime) = a)
                   
                   However, this solution is wasteful, because the axiom 
                   assert f(a, u) = a is simpler and more general.
                   Note that n_prime is in the equivalence class of n,
                   and n is now equal to u. So, n_prime is also equal to u.
                   Then, using congruence, Z3 will also deduce that f(a, n_prime) = a
                   using the simpler axiom.
                */
            }
            /* check whether current parent is of the form f(n_prime, a) */
            if (Z3_get_app_decl(c, parent) == td->f && Z3_get_app_arg(c, parent, 0) == n_prime) {
                /* assert f(u, a) = a */
                Z3_ast a = Z3_get_app_arg(c, parent, 1);
                Z3_theory_assert_axiom(t, Z3_mk_eq(c, mk_binary_app(c, td->f, td->u, a), a));
            }
        }
        n_prime = Z3_theory_get_eqc_next(t, n_prime);
    }
    while (n_prime != n);
}
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 128 of file test_user_theory.c.

{
    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");
    }
}
Z3_lbool Compare ( Z3_theory  t,
Z3_ast  n1,
Z3_ast  n2 
)

Compare the theory values in the equivalence classes of n1 and n2 using strcmp.

Return Z3_L_UNDEF if the equivalence class of n1 or n2 does not contain a theory value.

Definition at line 650 of file test_user_theory.c.

Referenced by apply_compare_axiom_for_parents_of(), and PATh_reduce_app().

                                                    {
    Z3_context ctx      = Z3_theory_get_context(t);
    printf("Compare(%s", Z3_ast_to_string(ctx, n1));
    printf(", %s)", Z3_ast_to_string(ctx, n2));
    if (Z3_theory_is_value(t, n1) && Z3_theory_is_value(t, n2)) {
        Z3_func_decl d1     = Z3_get_app_decl(ctx, Z3_to_app(ctx, n1));
        Z3_func_decl d2     = Z3_get_app_decl(ctx, Z3_to_app(ctx, n2));
        Z3_symbol    s1     = Z3_get_decl_name(ctx, d1);
        Z3_symbol    s2     = Z3_get_decl_name(ctx, d2);
        Z3_string    str1   = Z3_get_symbol_string(ctx, s1);
        Z3_string    str2;
        int strcmp_result;
        /* the next call to Z3_get_symbol_string will invalidate str1, so we need to create a copy */
        char * str1_copy    = strdup(str1);
        str2                = Z3_get_symbol_string(ctx, s2);
        strcmp_result       = strcmp(str1_copy, str2);
        free(str1_copy);
        if (strcmp_result == 0) {
            printf(" = true\n");
            return Z3_L_TRUE;
        }
        else {
            printf(" = false\n");
            return Z3_L_FALSE;
        }
    }
    printf(" = unknown\n");
    return Z3_L_UNDEF;
}
void display_eqc ( Z3_theory  t,
Z3_ast  n 
)

Display equivalence class containing n.

Definition at line 155 of file test_user_theory.c.

                                        {
    Z3_context c = Z3_theory_get_context(t);
    Z3_ast curr = n;
    printf("  ----- begin eqc of %s", Z3_ast_to_string(c, n));
    printf(", root: %s\n", Z3_ast_to_string(c, Z3_theory_get_eqc_root(t, n)));
    do {
        printf("  %s\n", Z3_ast_to_string(c, curr));
        curr = Z3_theory_get_eqc_next(t, curr);
    }
    while (curr != n);
    printf("  ----- end of eqc\n");
}
void display_eqc_parents ( Z3_theory  t,
Z3_ast  n 
)

Display the parent theory operators of the equivalence class containing n.

Definition at line 171 of file test_user_theory.c.

                                                {
    Z3_context c = Z3_theory_get_context(t);
    Z3_ast curr = n;
    printf("  ----- begin eqc (theory) parents of %s\n", Z3_ast_to_string(c, n));
    do {
        unsigned num_parents = Z3_theory_get_num_parents(t, curr);
        unsigned i;
        for (i = 0; i < num_parents; i++) {
            Z3_ast p = Z3_theory_get_parent(t, curr, i);
            printf("  %s\n", Z3_ast_to_string(c, p));
        }
        curr = Z3_theory_get_eqc_next(t, curr);
    }
    while (curr != n);
    printf("  ----- end of eqc (theory) parents\n");
}
void error_handler ( Z3_context  ctx,
Z3_error_code  e 
)

Simpler error handler.

Definition at line 24 of file test_user_theory.c.

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

exit gracefully in case of error.

Definition at line 15 of file test_user_theory.c.

{
  fprintf(stderr,"BUG: %s.\n", message);
  exit(1);
}
Z3_ast get_eqc_value ( Z3_theory  t,
Z3_ast  n 
)

If the equivalence class containing n contains a theory value, then return it. Otherwise, return 0.

Remarks:
An equivalence class may contain at most one theory value since theory values are different by definition.

Definition at line 205 of file test_user_theory.c.

Referenced by apply_compare_axiom_for_parents_of(), PATh_final_check(), and PATh_new_eq().

                                            {
    Z3_ast curr = n;
    do {
        if (Z3_theory_is_value(t, curr))
            return curr;
        curr = Z3_theory_get_eqc_next(t, curr);
    }
    while (curr != n);
    return 0;
}
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 118 of file test_user_theory.c.

{
    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 81 of file test_user_theory.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 58 of file test_user_theory.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 37 of file test_user_theory.c.

{
    Z3_context ctx;
    
    Z3_set_param_value(cfg, "MODEL", "true");
    ctx = Z3_mk_context(cfg);
#ifdef TRACING
    Z3_trace_to_stderr(ctx);
#endif
    Z3_set_error_handler(ctx, err);
    
    return ctx;
}
Z3_ast mk_int ( Z3_context  ctx,
int  v 
)

Create a Z3 integer node using a C int.

Definition at line 99 of file test_user_theory.c.

{
    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 90 of file test_user_theory.c.

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

Procedural attachment theory example.

Definition at line 792 of file test_user_theory.c.

Referenced by pa_theory_example1(), and pa_theory_example2().

                                       {
    Z3_sort compare_domain[2];
    Z3_symbol string_name  = Z3_mk_string_symbol(ctx, "String");
    Z3_symbol compare_name = Z3_mk_string_symbol(ctx, "Compare");
    Z3_sort B              = Z3_mk_bool_sort(ctx);
    PATheoryData * td      = (PATheoryData *)malloc(sizeof(PATheoryData));
    Z3_theory Th           = Z3_mk_theory(ctx, "CompareProcedurealAttachment", td);
    td->String             = Z3_theory_mk_sort(ctx, Th, string_name); 
    compare_domain[0] = td->String; 
    compare_domain[1] = td->String;
    td->Compare            = Z3_theory_mk_func_decl(ctx, Th, compare_name, 2, compare_domain, B);

    Z3_set_delete_callback(Th, PATh_delete);
    Z3_set_reduce_app_callback(Th, PATh_reduce_app);
    Z3_set_new_eq_callback(Th, PATh_new_eq);
    Z3_set_final_check_callback(Th, PATh_final_check);
    return Th;
}
Z3_theory mk_simple_theory ( Z3_context  ctx)

Simple theory example. The theory has a binary function f, and a unit element u.

The theory axioms are:

  • forall X. f(X, u) = X
  • forall X. f(u, X) = X

Definition at line 453 of file test_user_theory.c.

Referenced by simple_example1(), and simple_example2().

                                           {
    Z3_sort f_domain[2];
    Z3_symbol s_name      = Z3_mk_string_symbol(ctx, "S");
    Z3_symbol f_name      = Z3_mk_string_symbol(ctx, "f");
    Z3_symbol p_name      = Z3_mk_string_symbol(ctx, "p");
    Z3_symbol u_name      = Z3_mk_string_symbol(ctx, "u");
    Z3_sort B             = Z3_mk_bool_sort(ctx);
    SimpleTheoryData * td = (SimpleTheoryData*)malloc(sizeof(SimpleTheoryData));  
    Z3_theory Th          = Z3_mk_theory(ctx, "simple_th", td);
    td->S                 = Z3_theory_mk_sort(ctx, Th, s_name); 
    f_domain[0] = td->S; f_domain[1] = td->S;
    td->f                 = Z3_theory_mk_func_decl(ctx, Th, f_name, 2, f_domain, td->S);
    td->p                 = Z3_theory_mk_func_decl(ctx, Th, p_name, 1, &td->S, B); 
    td->u                 = Z3_theory_mk_constant(ctx, Th, u_name, td->S);

    Z3_set_delete_callback(Th, Th_delete);
    Z3_set_reduce_app_callback(Th, Th_reduce_app);
    Z3_set_new_app_callback(Th, Th_new_app);
    Z3_set_new_elem_callback(Th, Th_new_elem);
    Z3_set_init_search_callback(Th, Th_init_search);
    Z3_set_push_callback(Th, Th_push);
    Z3_set_pop_callback(Th, Th_pop);
    Z3_set_reset_callback(Th, Th_reset);
    Z3_set_restart_callback(Th, Th_restart);
    Z3_set_new_eq_callback(Th, Th_new_eq);
    Z3_set_new_diseq_callback(Th, Th_new_diseq);
    Z3_set_new_relevant_callback(Th, Th_new_relevant);
    Z3_set_new_assignment_callback(Th, Th_new_assignment);
    Z3_set_final_check_callback(Th, Th_final_check);
    return Th;
}
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 109 of file test_user_theory.c.

{
    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 72 of file test_user_theory.c.

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

Simple example to display model.

Definition at line 889 of file test_user_theory.c.

                             {
    Z3_ast x, y, z, c1, c2;
    Z3_ast args[2];
    Z3_sort s;
    Z3_context ctx;
    Z3_theory th;
    Z3_symbol c1_sym, c2_sym;
    printf("\nmodel_display_example\n");
    ctx = mk_context();
    th = Z3_mk_theory(ctx, "Alice And Bob", 0);
    s = Z3_theory_mk_sort(ctx, th, Z3_mk_string_symbol(ctx, "Name"));
    x  = mk_var(ctx, "x", s);
    y  = mk_var(ctx, "y", s);
    z  = mk_var(ctx, "z", s);

    c1_sym = Z3_mk_string_symbol(ctx, "Alice");
    c2_sym = Z3_mk_string_symbol(ctx, "Bob");        
    c1 = Z3_theory_mk_value(ctx, th, c1_sym, s);
    c2 = Z3_theory_mk_value(ctx, th, c2_sym, s);
    args[0] = Z3_mk_eq(ctx, x, c1);
    args[1] = Z3_mk_eq(ctx, x, c2);
    /* asserting x = c1 || x = c2 */
    Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, args));
    /* asserting y = z */
    Z3_assert_cnstr(ctx, Z3_mk_eq(ctx, y, z));
    check(ctx, Z3_L_TRUE);
    Z3_del_context(ctx);
}
void pa_theory_example1 ( )

Test Procedural Attachment Theory Simplifier.

Definition at line 814 of file test_user_theory.c.

{
    Z3_ast hello, world, c, d, n, r;
    Z3_context ctx;
    Z3_theory Th;
    PATheoryData * td;
    printf("\nprocedural attachment example1\n");
    ctx = mk_context();
    Th = mk_pa_theory(ctx);
    td = (PATheoryData*)Z3_theory_get_ext_data(Th);
    hello = PATh_mk_string_value(Th, "hello");
    world = PATh_mk_string_value(Th, "world");
    c  = mk_var(ctx, "c", td->String);
    d  = mk_var(ctx, "d", td->String);
    n  = Z3_mk_ite(ctx, mk_binary_app(ctx, td->Compare, hello, world), c, d);
    printf("%s\n==>\n", Z3_ast_to_string(ctx, n));
    r  = Z3_simplify(ctx, n);
    printf("%s\n",      Z3_ast_to_string(ctx, r));
    Z3_del_context(ctx);
}
void pa_theory_example2 ( int  assert_b_eq_hello)

Test Procedural Attachment Theory.

If assert_b_eq_hello != 0, then we also assert the atom "b = hello".

Definition at line 842 of file test_user_theory.c.

{
    Z3_ast hello, world, test, a, b;
    Z3_ast args[2];
    Z3_context ctx;
    Z3_theory Th;
    PATheoryData * td;
    printf("\nprocedural attachment example2\n");
    ctx = mk_context();
    Th = mk_pa_theory(ctx);
    td = (PATheoryData*)Z3_theory_get_ext_data(Th);
    hello = PATh_mk_string_value(Th, "hello");
    world = PATh_mk_string_value(Th, "world");
    test  = PATh_mk_string_value(Th, "test");
    a     = mk_var(ctx, "a", td->String);
    b     = mk_var(ctx, "b", td->String);
    /* assert a = world \/ a = test */
    args[0] = Z3_mk_eq(ctx, a, world);
    args[1] = Z3_mk_eq(ctx, a, test);
    Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, args));
    if (assert_b_eq_hello != 0) {
        /* assert b = hello */
        Z3_assert_cnstr(ctx, Z3_mk_eq(ctx, b, hello));
    }
    /* assert Compare(a, b) */
    Z3_assert_cnstr(ctx, mk_binary_app(ctx, td->Compare, a, b));
    
    if (assert_b_eq_hello != 0) {
        check(ctx, Z3_L_FALSE);
    }
    else {
        /* when "b = hello" is not asserted, the theory solver will
           fail to evaluate Compare(a, b)  */
        check(ctx, Z3_L_UNDEF);
    }
    Z3_del_context(ctx);
}
void PATh_delete ( Z3_theory  t)

Callback: delete for PATheory.

Definition at line 639 of file test_user_theory.c.

Referenced by mk_pa_theory().

                              {
    PATheoryData * td = (PATheoryData *)Z3_theory_get_ext_data(t);
    printf("Delete\n");
    free(td);
}
Z3_bool PATh_final_check ( Z3_theory  t)

Callback: final_check for PATheory.

Definition at line 766 of file test_user_theory.c.

Referenced by mk_pa_theory().

                                      {
    PATheoryData * td = (PATheoryData*)Z3_theory_get_ext_data(t);
    Z3_context c = Z3_theory_get_context(t);
    unsigned i, num;
    printf("Final check\n");
    /* check whether all (relevant) Compare(n1, n2) applications could be evaluated */
    num = Z3_theory_get_num_apps(t);
    for (i = 0; i < num; i++) {
        Z3_ast curr    = Z3_theory_get_app(t, i);
        Z3_func_decl d = Z3_get_app_decl(c, Z3_to_app(c, curr));
        if (d == td->Compare) {
            Z3_ast arg1 = Z3_get_app_arg(c, Z3_to_app(c, curr), 0);
            Z3_ast arg2 = Z3_get_app_arg(c, Z3_to_app(c, curr), 1);
            if (get_eqc_value(t, arg1) == 0 || get_eqc_value(t, arg2) == 0) {
                printf("failed to evaluate Compare(%s", Z3_ast_to_string(c, arg1));
                printf(", %s)\n", Z3_ast_to_string(c, arg2));
                return Z3_FALSE; /* giving up... could not evaluate this Compare application */
            }
        }
    }
    return Z3_TRUE;
}
Z3_ast PATh_mk_string_value ( Z3_theory  t,
char const *  str 
)

Create a new string interpreted value using the C string str.

Definition at line 628 of file test_user_theory.c.

Referenced by pa_theory_example1(), and pa_theory_example2().

                                                           {
    Z3_context ctx      = Z3_theory_get_context(t);
    PATheoryData * td   = (PATheoryData *)Z3_theory_get_ext_data(t);
    /* store the string as the name of the new interpreted value */
    Z3_symbol str_sym   = Z3_mk_string_symbol(ctx, str);
    return Z3_theory_mk_value(ctx, t, str_sym, td->String);
}
void PATh_new_eq ( Z3_theory  t,
Z3_ast  n1,
Z3_ast  n2 
)

Callback: new_eq for PATheory.

Definition at line 749 of file test_user_theory.c.

Referenced by mk_pa_theory().

                                                    {
    PATheoryData * td = (PATheoryData*)Z3_theory_get_ext_data(t);
    Z3_context c = Z3_theory_get_context(t);
    Z3_ast v1 = get_eqc_value(t, n1);
    Z3_ast v2 = get_eqc_value(t, n2);
    display_new_eq(t, n1, n2);
    if (get_eqc_value(t, n1) != 0) {
        apply_compare_axiom_for_parents_of(t, n2, v1);
    }
    if (v2 != 0) {
        apply_compare_axiom_for_parents_of(t, n1, v2);
    }
}
Z3_bool PATh_reduce_app ( Z3_theory  t,
Z3_func_decl  d,
unsigned  n,
Z3_ast const  args[],
Z3_ast *  result 
)

Callback: reduce_app for PATheory.

Definition at line 683 of file test_user_theory.c.

Referenced by mk_pa_theory().

                                                                                                       {
    Z3_context ctx    = Z3_theory_get_context(t);
    PATheoryData * td = (PATheoryData*)Z3_theory_get_ext_data(t);
    if (d == td->Compare) {
        switch (Compare(t, args[0], args[1])) {
        case Z3_L_TRUE:
            *result = Z3_mk_true(ctx);
            return Z3_TRUE; 
        case Z3_L_FALSE:
            *result = Z3_mk_false(ctx);
            return Z3_TRUE;
        case Z3_L_UNDEF:
            return Z3_FALSE; // failed to simplify
        }
    }
    return Z3_FALSE; // failed to simplify
}
void simple_example1 ( )

Test simple theory simplifier.

Definition at line 488 of file test_user_theory.c.

{
    Z3_ast a, b, c, f1, f2, f3, r, i;
    Z3_context ctx;
    Z3_theory Th;
    SimpleTheoryData * td;
    printf("\nsimple_example1\n");
    ctx = mk_context();
    Th = mk_simple_theory(ctx);
    td = (SimpleTheoryData*)Z3_theory_get_ext_data(Th);
    a  = mk_var(ctx, "a", td->S);
    b  = mk_var(ctx, "b", td->S);
    c  = mk_var(ctx, "c", td->S);
    i  = Z3_mk_ite(ctx, Z3_mk_eq(ctx, td->u, td->u), c, td->u);
    f1 = mk_binary_app(ctx, td->f, a, i);
    f2 = mk_binary_app(ctx, td->f, td->u, f1);
    f3 = mk_binary_app(ctx, td->f, b, f2);
    printf("%s\n==>\n", Z3_ast_to_string(ctx, f3));
    r  = Z3_simplify(ctx, f3);
    printf("%s\n",      Z3_ast_to_string(ctx, r));

    Z3_del_context(ctx);
}
void simple_example2 ( )

Test simple theory.

Definition at line 515 of file test_user_theory.c.

{
    Z3_ast a, b, c, d, f1;
    Z3_ast args[2];
    Z3_context ctx;
    Z3_theory Th;
    SimpleTheoryData * td;
    printf("\nsimple_example2\n");
    ctx = mk_context();
    Th = mk_simple_theory(ctx);
    td = (SimpleTheoryData*)Z3_theory_get_ext_data(Th);

    a  = mk_var(ctx, "a", td->S);
    b  = mk_var(ctx, "b", td->S);
    c  = mk_var(ctx, "c", td->S);
    d  = mk_var(ctx, "d", td->S);
    f1 = mk_binary_app(ctx, td->f, a, b);
    /* asserting a = c \/ b = d */
    args[0] = Z3_mk_eq(ctx, a, c);
    args[1] = Z3_mk_eq(ctx, b, d);
    Z3_assert_cnstr(ctx, Z3_mk_or(ctx, 2, args));
    /* asserting c = u */
    Z3_assert_cnstr(ctx, Z3_mk_eq(ctx, c, td->u));
    /* asserting d = u */
    Z3_assert_cnstr(ctx, Z3_mk_eq(ctx, d, td->u));
    /* asserting b != f(a,b) */
    Z3_assert_cnstr(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, b, f1)));
    /* asserting a != f(a,b) */
    Z3_assert_cnstr(ctx, Z3_mk_not(ctx, Z3_mk_eq(ctx, a, f1)));
    /* asserting p(a) */
    Z3_assert_cnstr(ctx, mk_unary_app(ctx, td->p, a));
    /* asserting !p(b) */
    Z3_assert_cnstr(ctx, Z3_mk_not(ctx, mk_unary_app(ctx, td->p, b)));

    // printf("Context:\n%s\n", Z3_context_to_string(ctx));
    check(ctx, Z3_L_FALSE);
    Z3_del_context(ctx);
}
void Th_delete ( Z3_theory  t)

Callback: invoked when t is deleted. This callback can be used to free theory specific data-structures.

Definition at line 245 of file test_user_theory.c.

Referenced by mk_simple_theory().

                            {
    SimpleTheoryData * td = (SimpleTheoryData *)Z3_theory_get_ext_data(t);
    printf("Delete\n");
    free(td);
}
Z3_bool Th_final_check ( Z3_theory  t)

Callback: invoked before Z3 starts building a model. This callback can be used to perform expensive operations lazily.

Definition at line 440 of file test_user_theory.c.

Referenced by mk_simple_theory().

                                    {
    printf("Final check\n");
    return Z3_TRUE;
}
void Th_init_search ( Z3_theory  t)

Callback: invoked when Z3 starts the search for a satisfying assignment.

Definition at line 298 of file test_user_theory.c.

Referenced by mk_simple_theory().

                                 {
    printf("Starting search\n");
}
void Th_new_app ( Z3_theory  t,
Z3_ast  n 
)

Callback: invoked when n is finally added to the logical context. n is an application of the form g(...) where g is an interpreted function symbol of t.

Definition at line 281 of file test_user_theory.c.

Referenced by mk_simple_theory().

                                       {
    Z3_context c = Z3_theory_get_context(t);
    printf("New app: %s\n", Z3_ast_to_string(c, n));
}
void Th_new_assignment ( Z3_theory  t,
Z3_ast  n,
Z3_bool  v 
)

Callback: invoked when n is assigned to true/false.

Z3 will only invoke this callback using a expression n s.t. Th_new_app or Th_new_elem was invoked for it.

Definition at line 431 of file test_user_theory.c.

Referenced by mk_simple_theory().

                                                         {
    Z3_context c = Z3_theory_get_context(t);
    printf("Assigned: %s --> %d\n", Z3_ast_to_string(c, n), v);
}
void Th_new_diseq ( Z3_theory  t,
Z3_ast  n1,
Z3_ast  n2 
)

Callback: invoked when n1 = n2 is false in the logical context.

Z3 will only invoke this callback using expressions n1 and n2 s.t. Th_new_app or Th_new_elem was invoked for them.

Definition at line 407 of file test_user_theory.c.

Referenced by mk_simple_theory().

                                                     {
    Z3_context c = Z3_theory_get_context(t);
    printf("New disequality: %s ", Z3_ast_to_string(c, n1));
    printf("!= %s\n", Z3_ast_to_string(c, n2));
}
void Th_new_elem ( Z3_theory  t,
Z3_ast  n 
)

Callback: invoked when n is finally added to the logical context. n is an expression of sort s, where s is an interpreted sort of t.

Definition at line 290 of file test_user_theory.c.

Referenced by mk_simple_theory().

                                        {
    Z3_context c = Z3_theory_get_context(t);
    printf("New elem: %s\n", Z3_ast_to_string(c, n));
}
void Th_new_eq ( Z3_theory  t,
Z3_ast  n1,
Z3_ast  n2 
)

Callback: invoked when n1 = n2 is true in the logical context.

Z3 will only invoke this callback using expressions n1 and n2 s.t. Th_new_app or Th_new_elem was invoked for them.

Definition at line 389 of file test_user_theory.c.

Referenced by mk_simple_theory().

void Th_new_relevant ( Z3_theory  t,
Z3_ast  n 
)

Callback: invoked when n becomes relevant in the current search branch. Irrelevant expressions may be ignored by the theory solver.

Z3 will only invoke this callback using a expression n s.t. Th_new_app or Th_new_elem was invoked for it.

Definition at line 420 of file test_user_theory.c.

Referenced by mk_simple_theory().

                                            {
    Z3_context c = Z3_theory_get_context(t);
    printf("Relevant: %s\n", Z3_ast_to_string(c, n));
}
void Th_pop ( Z3_theory  t)

Callback: invoked when Z3 backtracks a case-split.

See also:
Th_push

Definition at line 314 of file test_user_theory.c.

Referenced by mk_simple_theory().

                         {
    printf("Pop\n");
}
void Th_push ( Z3_theory  t)

Callback: invoked when Z3 creates a case-split (aka backtracking point).

Definition at line 305 of file test_user_theory.c.

Referenced by mk_simple_theory().

                          {
    printf("Push\n");
}
Z3_bool Th_reduce_app ( Z3_theory  t,
Z3_func_decl  d,
unsigned  n,
Z3_ast const  args[],
Z3_ast *  result 
)

The reduce_app callback can be used to extend Z3's simplifier. The simplifier is used to preprocess formulas.

Definition at line 255 of file test_user_theory.c.

Referenced by mk_simple_theory().

                                                                                                     {
    SimpleTheoryData * td = (SimpleTheoryData*)Z3_theory_get_ext_data(t);
    if (d == td->f) {
        if (args[0] == td->u) {
            *result = args[1];
            return Z3_TRUE;
        }
        else if (args[1] == td->u) {
            *result = args[0];
            return Z3_TRUE;
        }
    }
    else if (d == td->p) {
        if (args[0] == args[1]) {
            *result = Z3_mk_true(Z3_theory_get_context(t));
            return Z3_TRUE;
        }
    }
    return Z3_FALSE; // failed to simplify
}
void Th_reset ( Z3_theory  t)

Callback: invoked when the logical context containing t is reset.

Definition at line 321 of file test_user_theory.c.

Referenced by mk_simple_theory().

                           {
    printf("Reset\n");
}
void Th_restart ( Z3_theory  t)

Callback: invoked when Z3 restarts the search for a satisfying assignment.

Definition at line 328 of file test_user_theory.c.

Referenced by mk_simple_theory().

                             {
    printf("Restart\n");
}
Last modified Fri Oct 5 2012 11:32:38