error.c

/*
Error with nop theory plugin:
$ gcc -o error error.c -lz3
$ ./error
Z3 version 4.0.0.0
Context:
(solver
  (forall ((i Int)) (= (cu_a i) 0.0)))
Final check
Z3 check_and_get_model error: Z3 exception
    The mk_fresh_ext_data callback was not set for user theory, you must use Z3_theory_set_mk_fresh_ext_data_callback


No error without the plugin:
$ gcc -o error error.c -lz3 -DNO_THEORY
$ ./error
Z3 version 4.0.0.0
Context:
(solver
  (forall ((i Int)) (= (cu_a i) 0.0)))
sat:
cu_a -> {
  0
}


*/

#include<stdio.h>
#include<stdlib.h>
#include<string.h>
#include<stdarg.h>
#include<memory.h>
#include<z3.h>

typedef struct _nopTheoryData {
    int dummy;
} nopTheoryData;

static void Th_delete(Z3_theory t)
{
    nopTheoryData * td = (nopTheoryData *)Z3_theory_get_ext_data(t);
    free(td);
    return;
}
static Z3_bool Th_reduce_app(Z3_theory t, Z3_func_decl d,
                             unsigned n, Z3_ast const args[], Z3_ast * result)
{
    return Z3_FALSE;
}
static Z3_bool Th_reduce_eq(Z3_theory t, Z3_ast a, Z3_ast b, Z3_ast *r)
{
    return Z3_FALSE;
}
static Z3_bool Th_reduce_distinct(Z3_theory t, unsigned int n, const Z3_ast x[],
                                  Z3_ast *y)
{
    return Z3_FALSE;
}
static void Th_new_app(Z3_theory t, Z3_ast n) {
    return;
}
static void Th_new_elem(Z3_theory t, Z3_ast n) {
    return;
}
static void Th_init_search(Z3_theory t) {
    return;
}
static void Th_push(Z3_theory t) {
    return;
}
static void Th_pop(Z3_theory t) {
    return;
}
static void Th_restart(Z3_theory t) {
    return;
}
static void Th_reset(Z3_theory t) {
    return;
}
static Z3_bool Th_final_check(Z3_theory t)
{
    fprintf(stderr, "Final check\n");
    fflush(stderr);
    return Z3_TRUE;
}
static void Th_new_eq(Z3_theory t, Z3_ast n1, Z3_ast n2)
{
    return;
}
static void Th_new_diseq(Z3_theory t, Z3_ast n1, Z3_ast n2)
{
    return;
}
static void Th_new_relevant(Z3_theory t, Z3_ast n)
{
    return;
}
static void Th_new_assignment(Z3_theory t, Z3_ast n, Z3_bool v)
{
    return;
}
static Z3_theory mk_simple_theory(Z3_context ctx) {
    nopTheoryData *td = (nopTheoryData*)malloc(sizeof(nopTheoryData));
    Z3_theory Th      = Z3_mk_theory(ctx, "simple_th", td);

    Z3_set_delete_callback(Th, Th_delete);
    Z3_set_reduce_app_callback(Th, Th_reduce_app);
    Z3_set_reduce_eq_callback(Th, Th_reduce_eq);
    Z3_set_reduce_distinct_callback(Th, Th_reduce_distinct);
    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_restart_callback(Th, Th_restart);
    Z3_set_reset_callback(Th, Th_reset);
    Z3_set_final_check_callback(Th, Th_final_check);
    Z3_set_new_eq_callback(Th, Th_new_eq);
    Z3_set_new_diseq_callback(Th, Th_new_diseq);
    Z3_set_new_assignment_callback(Th, Th_new_assignment);
    Z3_set_new_relevant_callback(Th, Th_new_relevant);

    return Th;
}
/* end simple theory */

static int z3_error = 0;
static void throw_z3_error(Z3_context ctx, Z3_error_code e)
{
    z3_error = e;
}

static void nop_example()
{
    Z3_ast a;
    Z3_context ctx;
    Z3_theory Th;
    Z3_config conf = Z3_mk_config();
    Z3_lbool result;
    Z3_model m;
    unsigned major, minor, build, revision;

    Z3_get_version(&major, &minor, &build, &revision);
    fprintf(stderr, "Z3 version %d.%d.%d.%d\n",
            major, minor, build, revision);
    fflush(stderr);

    ctx = Z3_mk_context(conf);
    Z3_del_config(conf);
    Z3_set_error_handler(ctx, throw_z3_error);

#ifndef NO_THEORY
    Th = mk_simple_theory(ctx);
#endif

    {
        Z3_sort      cu_a_dom  = Z3_mk_int_sort(ctx);
        Z3_symbol    cu_a_sym  = Z3_mk_string_symbol(ctx, "cu_a");
        Z3_func_decl cu_a_decl;

        cu_a_decl = Z3_mk_func_decl(ctx,cu_a_sym,1,&cu_a_dom,Z3_mk_real_sort(ctx));

#ifdef PARSE_SMTLIB2
        a = Z3_parse_smtlib2_string(ctx,
          "(assert (forall ((i Int)) (= (cu_a i) 0.0)))",
            0,0,0,
          1,&cu_a_sym,&cu_a_decl);
        Z3_assert_cnstr(ctx, a);
#elif PARSE_SMTLIB
        Z3_parse_smtlib_string(ctx,
          "(benchmark tst :formula (forall ((i Int)) (= (cu_a i) 0.0)))",
          0,0,0, 1, &cu_a_sym, &cu_a_decl);
        int nf = Z3_get_smtlib_num_formulas(ctx);
        int i;
        for (i = 0; i < nf; i++) {
            Z3_ast f = Z3_get_smtlib_formula(ctx, i);
            Z3_assert_cnstr(ctx, f);
        }
#else
        Z3_sort   int_sort = Z3_mk_int_sort(ctx);
        Z3_symbol i_sym    = Z3_mk_string_symbol(ctx, "i");
        Z3_ast    i_var    = Z3_mk_const(ctx, i_sym, int_sort);
        Z3_app    i_app    = Z3_to_app(ctx, i_var);
        Z3_ast    app      = Z3_mk_app(ctx, cu_a_decl, 1, &i_var);
        Z3_ast    eq       = Z3_mk_eq(ctx, app, Z3_mk_real(ctx, 0, 1));
        Z3_ast    fa       = Z3_mk_forall_const(ctx, 0, 1, &i_app, 0, 0, eq);
        Z3_assert_cnstr(ctx, fa);
#endif
    }

    printf("Context:\n%s\n", Z3_context_to_string(ctx));
    result = Z3_check_and_get_model(ctx, &m);
    if (z3_error != 0) {
        fprintf(stderr, "Z3 check_and_get_model error: %s\n",
            Z3_get_error_msg((Z3_error_code)z3_error));
        if (z3_error == Z3_EXCEPTION) {
            fprintf(stderr, "\t%s\n", Z3_get_error_msg_ex(ctx, z3_error));
        }
        fflush(stderr);
        return;
    }
    switch (result) {
        case Z3_L_FALSE:
            fprintf(stderr, "unsat\n");
            fflush(stderr);
            break;
        case Z3_L_UNDEF:
            fprintf(stderr, "unknown: potential model:\n %s\n", Z3_model_to_string(ctx,m));
            fflush(stderr);
            break;
        case Z3_L_TRUE:
            fprintf(stderr, "sat:\n%s\n", Z3_model_to_string(ctx, m));
            fflush(stderr);
            break;
    }
    Z3_del_context(ctx);
}

int main()
{
    nop_example();
    return 0;
}