Pastebin launched a little side project called HostCabi.net, check it out ;-)Don't like ads? PRO users don't see any ads ;-)
Guest

error.c

By: a guest on Jul 25th, 2012  |  syntax: C  |  size: 4.71 KB  |  hits: 13  |  expires: Never
download  |  raw  |  embed  |  report abuse  |  print
This paste has a previous version, view the difference. 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. #include<stdio.h>
  29. #include<stdlib.h>
  30. #include<string.h>
  31. #include<stdarg.h>
  32. #include<memory.h>
  33. #include<z3.h>
  34.  
  35. typedef struct _nopTheoryData {
  36.         int dummy;
  37. } nopTheoryData;
  38.  
  39. static void Th_delete(Z3_theory t)
  40. {
  41.         nopTheoryData * td = (nopTheoryData *)Z3_theory_get_ext_data(t);
  42.         free(td);
  43.         return;
  44. }
  45. static Z3_bool Th_reduce_app(Z3_theory t, Z3_func_decl d,
  46.                              unsigned n, Z3_ast const args[], Z3_ast * result)
  47. {
  48.         return Z3_FALSE;
  49. }
  50. static Z3_bool Th_reduce_eq(Z3_theory t, Z3_ast a, Z3_ast b, Z3_ast *r)
  51. {
  52.         return Z3_FALSE;
  53. }
  54. static Z3_bool Th_reduce_distinct(Z3_theory t, unsigned int n, const Z3_ast x[],
  55.                                   Z3_ast *y)
  56. {
  57.         return Z3_FALSE;
  58. }
  59. static void Th_new_app(Z3_theory t, Z3_ast n) {
  60.         return;
  61. }
  62. static void Th_new_elem(Z3_theory t, Z3_ast n) {
  63.         return;
  64. }
  65. static void Th_init_search(Z3_theory t) {
  66.         return;
  67. }
  68. static void Th_push(Z3_theory t) {
  69.         return;
  70. }
  71. static void Th_pop(Z3_theory t) {
  72.         return;
  73. }
  74. static void Th_restart(Z3_theory t) {
  75.         return;
  76. }
  77. static void Th_reset(Z3_theory t) {
  78.         return;
  79. }
  80. static Z3_bool Th_final_check(Z3_theory t)
  81. {
  82.         fprintf(stderr, "Final check\n");
  83.         fflush(stderr);
  84.         return Z3_TRUE;
  85. }
  86. static void Th_new_eq(Z3_theory t, Z3_ast n1, Z3_ast n2)
  87. {
  88.         return;
  89. }
  90. static void Th_new_diseq(Z3_theory t, Z3_ast n1, Z3_ast n2)
  91. {
  92.         return;
  93. }
  94. static void Th_new_relevant(Z3_theory t, Z3_ast n)
  95. {
  96.         return;
  97. }
  98. static void Th_new_assignment(Z3_theory t, Z3_ast n, Z3_bool v)
  99. {
  100.         return;
  101. }
  102. static Z3_theory mk_simple_theory(Z3_context ctx) {
  103.         nopTheoryData *td = (nopTheoryData*)malloc(sizeof(nopTheoryData));  
  104.         Z3_theory Th      = Z3_mk_theory(ctx, "simple_th", td);
  105.  
  106.         Z3_set_delete_callback(Th, Th_delete);
  107.         Z3_set_reduce_app_callback(Th, Th_reduce_app);
  108.         Z3_set_reduce_eq_callback(Th, Th_reduce_eq);
  109.         Z3_set_reduce_distinct_callback(Th, Th_reduce_distinct);
  110.         Z3_set_new_app_callback(Th, Th_new_app);
  111.         Z3_set_new_elem_callback(Th, Th_new_elem);
  112.         Z3_set_init_search_callback(Th, Th_init_search);
  113.         Z3_set_push_callback(Th, Th_push);
  114.         Z3_set_pop_callback(Th, Th_pop);
  115.         Z3_set_restart_callback(Th, Th_restart);
  116.         Z3_set_reset_callback(Th, Th_reset);
  117.         Z3_set_final_check_callback(Th, Th_final_check);
  118.         Z3_set_new_eq_callback(Th, Th_new_eq);
  119.         Z3_set_new_diseq_callback(Th, Th_new_diseq);
  120.         Z3_set_new_assignment_callback(Th, Th_new_assignment);
  121.         Z3_set_new_relevant_callback(Th, Th_new_relevant);
  122.  
  123.         return Th;
  124. }
  125. /* end simple theory */
  126.  
  127. static int z3_error = 0;
  128. static void throw_z3_error(Z3_context ctx, Z3_error_code e)
  129. {
  130.         z3_error = e;
  131. }
  132.  
  133. static void nop_example()
  134. {
  135.         Z3_ast a;
  136.         Z3_context ctx;
  137.         Z3_theory Th;
  138.         Z3_config conf = Z3_mk_config();
  139.         Z3_lbool result;
  140.         Z3_model m;
  141.         unsigned major, minor, build, revision;
  142.  
  143.         Z3_get_version(&major, &minor, &build, &revision);
  144.         fprintf(stderr, "Z3 version %d.%d.%d.%d\n",
  145.                 major, minor, build, revision);
  146.         fflush(stderr);
  147.  
  148.         ctx = Z3_mk_context(conf);
  149.         Z3_del_config(conf);
  150.         Z3_set_error_handler(ctx, throw_z3_error);
  151.  
  152. #ifndef NO_THEORY
  153.         Th = mk_simple_theory(ctx);
  154. #endif
  155.  
  156.         {
  157.                 Z3_sort      cu_a_dom  = Z3_mk_int_sort(ctx);
  158.                 Z3_symbol    cu_a_sym  = Z3_mk_string_symbol(ctx, "cu_a");
  159.                 Z3_func_decl cu_a_decl;
  160.  
  161.                 cu_a_decl = Z3_mk_func_decl(ctx,cu_a_sym,1,&cu_a_dom,Z3_mk_real_sort(ctx));
  162.  
  163.                 a = Z3_parse_smtlib2_string(ctx,
  164.                   "(assert (forall ((i Int)) (= (cu_a i) 0.0)))",
  165.                         0,0,0,
  166.                   1,&cu_a_sym,&cu_a_decl);
  167.                 Z3_assert_cnstr(ctx, a);
  168.         }
  169.  
  170.         printf("Context:\n%s\n", Z3_context_to_string(ctx));
  171.         result = Z3_check_and_get_model(ctx, &m);
  172.         if (z3_error != 0) {
  173.                 fprintf(stderr, "Z3 check_and_get_model error: %s\n",
  174.                         Z3_get_error_msg((Z3_error_code)z3_error));
  175.                 if (z3_error == Z3_EXCEPTION) {
  176.                         fprintf(stderr, "\t%s\n", Z3_get_error_msg_ex(ctx, z3_error));
  177.                 }
  178.                 fflush(stderr);
  179.                 return;
  180.         }
  181.         switch (result) {
  182.                 case Z3_L_FALSE:
  183.                         fprintf(stderr, "unsat\n");
  184.                         fflush(stderr);
  185.                         break;
  186.                 case Z3_L_UNDEF:
  187.                         fprintf(stderr, "unknown: potential model:\n %s\n", Z3_model_to_string(ctx,m));
  188.                         fflush(stderr);
  189.                         break;
  190.                 case Z3_L_TRUE:
  191.                         fprintf(stderr, "sat:\n%s\n", Z3_model_to_string(ctx, m));
  192.                         fflush(stderr);
  193.                         break;
  194.         }
  195.         Z3_del_context(ctx);
  196. }
  197.  
  198. int main()
  199. {
  200.         nop_example();
  201.         return 0;
  202. }