Pastebin launched a little side project called VERYVIRAL.com, check it out ;-) Want more features on Pastebin? Sign Up, it's FREE!
Guest

error.c

By: a guest on Jul 25th, 2012  |  syntax: C  |  size: 5.49 KB  |  views: 12  |  expires: Never
download  |  raw  |  embed  |  report abuse  |  print
Text below is selected. Please press Ctrl+C to copy to your clipboard. (⌘+C on Mac)
  1. /*
  2. Error with nop theory plugin:
  3. $ gcc -o error error.c -lz3
  4. $ ./error
  5. Z3 version 4.0.0.0
  6. Context:
  7. (solver
  8.   (forall ((i Int)) (= (cu_a i) 0.0)))
  9. Final check
  10. Z3 check_and_get_model error: Z3 exception
  11.         The mk_fresh_ext_data callback was not set for user theory, you must use Z3_theory_set_mk_fresh_ext_data_callback
  12.  
  13.  
  14. No error without the plugin:
  15. $ gcc -o error error.c -lz3 -DNO_THEORY
  16. $ ./error
  17. Z3 version 4.0.0.0
  18. Context:
  19. (solver
  20.   (forall ((i Int)) (= (cu_a i) 0.0)))
  21. sat:
  22. cu_a -> {
  23.   0
  24. }
  25.  
  26.  
  27. */
  28.  
  29. #include<stdio.h>
  30. #include<stdlib.h>
  31. #include<string.h>
  32. #include<stdarg.h>
  33. #include<memory.h>
  34. #include<z3.h>
  35.  
  36. typedef struct _nopTheoryData {
  37.         int dummy;
  38. } nopTheoryData;
  39.  
  40. static void Th_delete(Z3_theory t)
  41. {
  42.         nopTheoryData * td = (nopTheoryData *)Z3_theory_get_ext_data(t);
  43.         free(td);
  44.         return;
  45. }
  46. static Z3_bool Th_reduce_app(Z3_theory t, Z3_func_decl d,
  47.                              unsigned n, Z3_ast const args[], Z3_ast * result)
  48. {
  49.         return Z3_FALSE;
  50. }
  51. static Z3_bool Th_reduce_eq(Z3_theory t, Z3_ast a, Z3_ast b, Z3_ast *r)
  52. {
  53.         return Z3_FALSE;
  54. }
  55. static Z3_bool Th_reduce_distinct(Z3_theory t, unsigned int n, const Z3_ast x[],
  56.                                   Z3_ast *y)
  57. {
  58.         return Z3_FALSE;
  59. }
  60. static void Th_new_app(Z3_theory t, Z3_ast n) {
  61.         return;
  62. }
  63. static void Th_new_elem(Z3_theory t, Z3_ast n) {
  64.         return;
  65. }
  66. static void Th_init_search(Z3_theory t) {
  67.         return;
  68. }
  69. static void Th_push(Z3_theory t) {
  70.         return;
  71. }
  72. static void Th_pop(Z3_theory t) {
  73.         return;
  74. }
  75. static void Th_restart(Z3_theory t) {
  76.         return;
  77. }
  78. static void Th_reset(Z3_theory t) {
  79.         return;
  80. }
  81. static Z3_bool Th_final_check(Z3_theory t)
  82. {
  83.         fprintf(stderr, "Final check\n");
  84.         fflush(stderr);
  85.         return Z3_TRUE;
  86. }
  87. static void Th_new_eq(Z3_theory t, Z3_ast n1, Z3_ast n2)
  88. {
  89.         return;
  90. }
  91. static void Th_new_diseq(Z3_theory t, Z3_ast n1, Z3_ast n2)
  92. {
  93.         return;
  94. }
  95. static void Th_new_relevant(Z3_theory t, Z3_ast n)
  96. {
  97.         return;
  98. }
  99. static void Th_new_assignment(Z3_theory t, Z3_ast n, Z3_bool v)
  100. {
  101.         return;
  102. }
  103. static Z3_theory mk_simple_theory(Z3_context ctx) {
  104.         nopTheoryData *td = (nopTheoryData*)malloc(sizeof(nopTheoryData));  
  105.         Z3_theory Th      = Z3_mk_theory(ctx, "simple_th", td);
  106.  
  107.         Z3_set_delete_callback(Th, Th_delete);
  108.         Z3_set_reduce_app_callback(Th, Th_reduce_app);
  109.         Z3_set_reduce_eq_callback(Th, Th_reduce_eq);
  110.         Z3_set_reduce_distinct_callback(Th, Th_reduce_distinct);
  111.         Z3_set_new_app_callback(Th, Th_new_app);
  112.         Z3_set_new_elem_callback(Th, Th_new_elem);
  113.         Z3_set_init_search_callback(Th, Th_init_search);
  114.         Z3_set_push_callback(Th, Th_push);
  115.         Z3_set_pop_callback(Th, Th_pop);
  116.         Z3_set_restart_callback(Th, Th_restart);
  117.         Z3_set_reset_callback(Th, Th_reset);
  118.         Z3_set_final_check_callback(Th, Th_final_check);
  119.         Z3_set_new_eq_callback(Th, Th_new_eq);
  120.         Z3_set_new_diseq_callback(Th, Th_new_diseq);
  121.         Z3_set_new_assignment_callback(Th, Th_new_assignment);
  122.         Z3_set_new_relevant_callback(Th, Th_new_relevant);
  123.  
  124.         return Th;
  125. }
  126. /* end simple theory */
  127.  
  128. static int z3_error = 0;
  129. static void throw_z3_error(Z3_context ctx, Z3_error_code e)
  130. {
  131.         z3_error = e;
  132. }
  133.  
  134. static void nop_example()
  135. {
  136.         Z3_ast a;
  137.         Z3_context ctx;
  138.         Z3_theory Th;
  139.         Z3_config conf = Z3_mk_config();
  140.         Z3_lbool result;
  141.         Z3_model m;
  142.         unsigned major, minor, build, revision;
  143.  
  144.         Z3_get_version(&major, &minor, &build, &revision);
  145.         fprintf(stderr, "Z3 version %d.%d.%d.%d\n",
  146.                 major, minor, build, revision);
  147.         fflush(stderr);
  148.  
  149.         ctx = Z3_mk_context(conf);
  150.         Z3_del_config(conf);
  151.         Z3_set_error_handler(ctx, throw_z3_error);
  152.  
  153. #ifndef NO_THEORY
  154.         Th = mk_simple_theory(ctx);
  155. #endif
  156.  
  157.         {
  158.                 Z3_sort      cu_a_dom  = Z3_mk_int_sort(ctx);
  159.                 Z3_symbol    cu_a_sym  = Z3_mk_string_symbol(ctx, "cu_a");
  160.                 Z3_func_decl cu_a_decl;
  161.  
  162.                 cu_a_decl = Z3_mk_func_decl(ctx,cu_a_sym,1,&cu_a_dom,Z3_mk_real_sort(ctx));
  163.  
  164. #ifdef PARSE_SMTLIB2
  165.                 a = Z3_parse_smtlib2_string(ctx,
  166.                   "(assert (forall ((i Int)) (= (cu_a i) 0.0)))",
  167.                         0,0,0,
  168.                   1,&cu_a_sym,&cu_a_decl);
  169.                 Z3_assert_cnstr(ctx, a);
  170. #elif PARSE_SMTLIB
  171.                 Z3_parse_smtlib_string(ctx,
  172.                   "(benchmark tst :formula (forall ((i Int)) (= (cu_a i) 0.0)))",
  173.                   0,0,0, 1, &cu_a_sym, &cu_a_decl);
  174.                 int nf = Z3_get_smtlib_num_formulas(ctx);
  175.                 int i;
  176.                 for (i = 0; i < nf; i++) {
  177.                         Z3_ast f = Z3_get_smtlib_formula(ctx, i);
  178.                         Z3_assert_cnstr(ctx, f);
  179.                 }
  180. #else
  181.                 Z3_sort   int_sort = Z3_mk_int_sort(ctx);
  182.                 Z3_symbol i_sym    = Z3_mk_string_symbol(ctx, "i");
  183.                 Z3_ast    i_var    = Z3_mk_const(ctx, i_sym, int_sort);
  184.                 Z3_app    i_app    = Z3_to_app(ctx, i_var);
  185.                 Z3_ast    app      = Z3_mk_app(ctx, cu_a_decl, 1, &i_var);
  186.                 Z3_ast    eq       = Z3_mk_eq(ctx, app, Z3_mk_real(ctx, 0, 1));
  187.                 Z3_ast    fa       = Z3_mk_forall_const(ctx, 0, 1, &i_app, 0, 0, eq);
  188.                 Z3_assert_cnstr(ctx, fa);
  189. #endif
  190.         }
  191.  
  192.         printf("Context:\n%s\n", Z3_context_to_string(ctx));
  193.         result = Z3_check_and_get_model(ctx, &m);
  194.         if (z3_error != 0) {
  195.                 fprintf(stderr, "Z3 check_and_get_model error: %s\n",
  196.                         Z3_get_error_msg((Z3_error_code)z3_error));
  197.                 if (z3_error == Z3_EXCEPTION) {
  198.                         fprintf(stderr, "\t%s\n", Z3_get_error_msg_ex(ctx, z3_error));
  199.                 }
  200.                 fflush(stderr);
  201.                 return;
  202.         }
  203.         switch (result) {
  204.                 case Z3_L_FALSE:
  205.                         fprintf(stderr, "unsat\n");
  206.                         fflush(stderr);
  207.                         break;
  208.                 case Z3_L_UNDEF:
  209.                         fprintf(stderr, "unknown: potential model:\n %s\n", Z3_model_to_string(ctx,m));
  210.                         fflush(stderr);
  211.                         break;
  212.                 case Z3_L_TRUE:
  213.                         fprintf(stderr, "sat:\n%s\n", Z3_model_to_string(ctx, m));
  214.                         fflush(stderr);
  215.                         break;
  216.         }
  217.         Z3_del_context(ctx);
  218. }
  219.  
  220. int main()
  221. {
  222.         nop_example();
  223.         return 0;
  224. }