Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- /*
- 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))
- (forall ((i Int))
- (<= (+ (cu_a i) (* (- 1.0) (cu_v i))) 0.0))
- (= cu_d 4)
- (= (cu_n 0) 0)
- (= (cu_n 1) 0)
- (= (cu_n 2) 0)
- (= (cu_n 3) 0)
- (= (cu_a 0) cu_a_0)
- (= (cu_a 1) cu_a_1)
- (= (cu_a 2) cu_a_2)
- (= (cu_a 3) cu_a_3)
- (= (+ cu_a_0
- cu_a_1
- cu_a_2
- cu_a_3
- (* (- 1.0) cu_a_sum))
- 0.0)
- (= (cu_v 0) 0.0)
- (= (cu_v 1) 1.0)
- (= (cu_v 2) 1.0)
- (= (cu_v 3) 1.0)
- (forall ((i Int)) (or (<= (cu_a i) 0.0) (= (cu_a i) 1.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))
- (forall ((i Int)) (<= (+ (cu_a i) (* (- 1.0) (cu_v i))) 0.0))
- (= cu_d 4)
- (= (cu_n 0) 0)
- (= (cu_n 1) 0)
- (= (cu_n 2) 0)
- (= (cu_n 3) 0)
- (= (cu_a 0) cu_a_0)
- (= (cu_a 1) cu_a_1)
- (= (cu_a 2) cu_a_2)
- (= (cu_a 3) cu_a_3)
- (= (+ cu_a_0 cu_a_1 cu_a_2 cu_a_3 (* (- 1.0) cu_a_sum)) 0.0)
- (= (cu_v 0) 0.0)
- (= (cu_v 1) 1.0)
- (= (cu_v 2) 1.0)
- (= (cu_v 3) 1.0)
- (forall ((i Int)) (or (<= (cu_a i) 0.0) (= (cu_a i) 1.0))))
- sat:
- cu_a_sum -> 1
- cu_a_0 -> 0
- cu_a_1 -> 0
- cu_a_3 -> 0
- cu_a_2 -> 1
- cu_d -> 4
- cu_a -> {
- 2 -> 1
- else -> 0
- }
- cu_n -> {
- 0
- }
- cu_v -> {
- 0 -> 0
- 1 -> 1
- 2 -> 1
- 3 -> 1
- else -> (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
- a = Z3_parse_smtlib2_string(ctx,
- "(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))))",
- 0,0,0,0,0,0);
- Z3_assert_cnstr(ctx, a);
- 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;
- }
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement