This week only. Pastebin PRO Accounts Christmas Special! Don't miss out!Want more features on Pastebin? Sign Up, it's FREE!
Guest

error.c

By: a guest on Jul 25th, 2012  |  syntax: C  |  size: 6.32 KB  |  views: 21  |  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.   (forall ((i Int))
  10.     (<= (+ (cu_a i) (* (- 1.0) (cu_v i))) 0.0))
  11.   (= cu_d 4)
  12.   (= (cu_n 0) 0)
  13.   (= (cu_n 1) 0)
  14.   (= (cu_n 2) 0)
  15.   (= (cu_n 3) 0)
  16.   (= (cu_a 0) cu_a_0)
  17.   (= (cu_a 1) cu_a_1)
  18.   (= (cu_a 2) cu_a_2)
  19.   (= (cu_a 3) cu_a_3)
  20.   (= (+ cu_a_0
  21.         cu_a_1
  22.         cu_a_2
  23.         cu_a_3
  24.         (* (- 1.0) cu_a_sum))
  25.      0.0)
  26.   (= (cu_v 0) 0.0)
  27.   (= (cu_v 1) 1.0)
  28.   (= (cu_v 2) 1.0)
  29.   (= (cu_v 3) 1.0)
  30.   (forall ((i Int)) (or (<= (cu_a i) 0.0) (= (cu_a i) 1.0))))
  31. Final check
  32. Z3 check_and_get_model error: Z3 exception
  33.         The mk_fresh_ext_data callback was not set for user theory, you must use Z3_theory_set_mk_fresh_ext_data_callback
  34.  
  35. No error without the plugin:
  36. $ gcc -o error error.c -lz3 -DNO_THEORY
  37. $ ./error
  38. Z3 version 4.0.0.0
  39. Context:
  40. (solver
  41.   (forall ((i Int)) (>= (cu_a i) 0.0))
  42.   (forall ((i Int)) (<= (+ (cu_a i) (* (- 1.0) (cu_v i))) 0.0))
  43.   (= cu_d 4)
  44.   (= (cu_n 0) 0)
  45.   (= (cu_n 1) 0)
  46.   (= (cu_n 2) 0)
  47.   (= (cu_n 3) 0)
  48.   (= (cu_a 0) cu_a_0)
  49.   (= (cu_a 1) cu_a_1)
  50.   (= (cu_a 2) cu_a_2)
  51.   (= (cu_a 3) cu_a_3)
  52.   (= (+ cu_a_0 cu_a_1 cu_a_2 cu_a_3 (* (- 1.0) cu_a_sum)) 0.0)
  53.   (= (cu_v 0) 0.0)
  54.   (= (cu_v 1) 1.0)
  55.   (= (cu_v 2) 1.0)
  56.   (= (cu_v 3) 1.0)
  57.   (forall ((i Int)) (or (<= (cu_a i) 0.0) (= (cu_a i) 1.0))))
  58. sat:
  59. cu_a_sum -> 1
  60. cu_a_0 -> 0
  61. cu_a_1 -> 0
  62. cu_a_3 -> 0
  63. cu_a_2 -> 1
  64. cu_d -> 4
  65. cu_a -> {
  66.   2 -> 1
  67.   else -> 0
  68. }
  69. cu_n -> {
  70.   0
  71. }
  72. cu_v -> {
  73.   0 -> 0
  74.   1 -> 1
  75.   2 -> 1
  76.   3 -> 1
  77.   else -> (cu_a #0)
  78. }
  79.  
  80. */
  81.  
  82. #include<stdio.h>
  83. #include<stdlib.h>
  84. #include<string.h>
  85. #include<stdarg.h>
  86. #include<memory.h>
  87. #include<z3.h>
  88.  
  89. typedef struct _nopTheoryData {
  90.         int dummy;
  91. } nopTheoryData;
  92.  
  93. static void Th_delete(Z3_theory t)
  94. {
  95.         nopTheoryData * td = (nopTheoryData *)Z3_theory_get_ext_data(t);
  96.         free(td);
  97.         return;
  98. }
  99. static Z3_bool Th_reduce_app(Z3_theory t, Z3_func_decl d,
  100.                              unsigned n, Z3_ast const args[], Z3_ast * result)
  101. {
  102.         return Z3_FALSE;
  103. }
  104. static Z3_bool Th_reduce_eq(Z3_theory t, Z3_ast a, Z3_ast b, Z3_ast *r)
  105. {
  106.         return Z3_FALSE;
  107. }
  108. static Z3_bool Th_reduce_distinct(Z3_theory t, unsigned int n, const Z3_ast x[],
  109.                                   Z3_ast *y)
  110. {
  111.         return Z3_FALSE;
  112. }
  113. static void Th_new_app(Z3_theory t, Z3_ast n) {
  114.         return;
  115. }
  116. static void Th_new_elem(Z3_theory t, Z3_ast n) {
  117.         return;
  118. }
  119. static void Th_init_search(Z3_theory t) {
  120.         return;
  121. }
  122. static void Th_push(Z3_theory t) {
  123.         return;
  124. }
  125. static void Th_pop(Z3_theory t) {
  126.         return;
  127. }
  128. static void Th_restart(Z3_theory t) {
  129.         return;
  130. }
  131. static void Th_reset(Z3_theory t) {
  132.         return;
  133. }
  134. static Z3_bool Th_final_check(Z3_theory t)
  135. {
  136.         fprintf(stderr, "Final check\n");
  137.         fflush(stderr);
  138.         return Z3_TRUE;
  139. }
  140. static void Th_new_eq(Z3_theory t, Z3_ast n1, Z3_ast n2)
  141. {
  142.         return;
  143. }
  144. static void Th_new_diseq(Z3_theory t, Z3_ast n1, Z3_ast n2)
  145. {
  146.         return;
  147. }
  148. static void Th_new_relevant(Z3_theory t, Z3_ast n)
  149. {
  150.         return;
  151. }
  152. static void Th_new_assignment(Z3_theory t, Z3_ast n, Z3_bool v)
  153. {
  154.         return;
  155. }
  156. static Z3_theory mk_simple_theory(Z3_context ctx) {
  157.         nopTheoryData *td = (nopTheoryData*)malloc(sizeof(nopTheoryData));  
  158.         Z3_theory Th      = Z3_mk_theory(ctx, "simple_th", td);
  159.  
  160.         Z3_set_delete_callback(Th, Th_delete);
  161.         Z3_set_reduce_app_callback(Th, Th_reduce_app);
  162.         Z3_set_reduce_eq_callback(Th, Th_reduce_eq);
  163.         Z3_set_reduce_distinct_callback(Th, Th_reduce_distinct);
  164.         Z3_set_new_app_callback(Th, Th_new_app);
  165.         Z3_set_new_elem_callback(Th, Th_new_elem);
  166.         Z3_set_init_search_callback(Th, Th_init_search);
  167.         Z3_set_push_callback(Th, Th_push);
  168.         Z3_set_pop_callback(Th, Th_pop);
  169.         Z3_set_restart_callback(Th, Th_restart);
  170.         Z3_set_reset_callback(Th, Th_reset);
  171.         Z3_set_final_check_callback(Th, Th_final_check);
  172.         Z3_set_new_eq_callback(Th, Th_new_eq);
  173.         Z3_set_new_diseq_callback(Th, Th_new_diseq);
  174.         Z3_set_new_assignment_callback(Th, Th_new_assignment);
  175.         Z3_set_new_relevant_callback(Th, Th_new_relevant);
  176.  
  177.         return Th;
  178. }
  179. /* end simple theory */
  180.  
  181. static int z3_error = 0;
  182. static void throw_z3_error(Z3_context ctx, Z3_error_code e)
  183. {
  184.         z3_error = e;
  185. }
  186.  
  187. static void nop_example()
  188. {
  189.         Z3_ast a;
  190.         Z3_context ctx;
  191.         Z3_theory Th;
  192.         Z3_config conf = Z3_mk_config();
  193.         Z3_lbool result;
  194.         Z3_model m;
  195.         unsigned major, minor, build, revision;
  196.  
  197.         Z3_get_version(&major, &minor, &build, &revision);
  198.         fprintf(stderr, "Z3 version %d.%d.%d.%d\n",
  199.                 major, minor, build, revision);
  200.         fflush(stderr);
  201.  
  202.         ctx = Z3_mk_context(conf);
  203.         Z3_del_config(conf);
  204.         Z3_set_error_handler(ctx, throw_z3_error);
  205.  
  206. #ifndef NO_THEORY
  207.         Th = mk_simple_theory(ctx);
  208. #endif
  209.  
  210.         a = Z3_parse_smtlib2_string(ctx,
  211.           "(declare-const cu_d Int)(declare-const cu_a_sum Real)(declare-fun cu_v (Int) Real)(declare-fun cu_a (Int) Real)(declare-fun cu_n  (Int) Int)(assert (forall ((i Int)) (>= (cu_a i) 0.0)))(assert (forall ((i Int)) (<= (cu_a i) (cu_v i))))(assert (= cu_d 4))(assert (= (cu_n 0) 0))(assert (= (cu_n 1) 0))(assert (= (cu_n 2) 0))(assert (= (cu_n 3) 0))(declare-const cu_a_0 Real)(assert (= (cu_a 0) cu_a_0))(declare-const cu_a_1 Real)(assert (= (cu_a 1) cu_a_1))(declare-const cu_a_2 Real)(assert (= (cu_a 2) cu_a_2))(declare-const cu_a_3 Real)(assert (= (cu_a 3) cu_a_3))(assert (= cu_a_sum (+ cu_a_0 (+ cu_a_1 (+ cu_a_2 (+ cu_a_3 0.0))))))(assert (= (cu_v 0) 0.0))(assert (= (cu_v 1) 1.000000))(assert (= (cu_v 2) 1.000000))(assert (= (cu_v 3) 1.000000))(assert (forall ((i Int))(=> (> (cu_a i) 0.0)(= (cu_a i) 1.0))))",
  212.           0,0,0,0,0,0);
  213.         Z3_assert_cnstr(ctx, a);
  214.  
  215.         printf("Context:\n%s\n", Z3_context_to_string(ctx));
  216.         result = Z3_check_and_get_model(ctx, &m);
  217.         if (z3_error != 0) {
  218.                 fprintf(stderr, "Z3 check_and_get_model error: %s\n",
  219.                         Z3_get_error_msg((Z3_error_code)z3_error));
  220.                 if (z3_error == Z3_EXCEPTION) {
  221.                         fprintf(stderr, "\t%s\n", Z3_get_error_msg_ex(ctx, z3_error));
  222.                 }
  223.                 fflush(stderr);
  224.                 return;
  225.         }
  226.         switch (result) {
  227.                 case Z3_L_FALSE:
  228.                         fprintf(stderr, "unsat\n");
  229.                         fflush(stderr);
  230.                         break;
  231.                 case Z3_L_UNDEF:
  232.                         fprintf(stderr, "unknown: potential model:\n %s\n", Z3_model_to_string(ctx,m));
  233.                         fflush(stderr);
  234.                         break;
  235.                 case Z3_L_TRUE:
  236.                         fprintf(stderr, "sat:\n%s\n", Z3_model_to_string(ctx, m));
  237.                         fflush(stderr);
  238.                         break;
  239.         }
  240.         Z3_del_context(ctx);
  241. }
  242.  
  243. int main()
  244. {
  245.         nop_example();
  246.         return 0;
  247. }
clone this paste RAW Paste Data