From 635aabf2d58763818acefbfe471eb7fb77b6fbfa Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Dec 2012 21:39:31 -0800 Subject: [PATCH] fix get_implied equalities and the unit test Signed-off-by: Nikolaj Bjorner --- src/api/api_solver.cpp | 19 +++++++++++++++++++ src/api/api_solver_old.cpp | 17 ----------------- src/test/get_implied_equalities.cpp | 28 +++++++++++++++++----------- 3 files changed, 36 insertions(+), 28 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 6bf184708..9ace149af 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -30,6 +30,7 @@ Revision History: #include"scoped_timer.h" #include"smt_strategic_solver.h" #include"smt_solver.h" +#include"smt_implied_equalities.h" extern "C" { @@ -357,4 +358,22 @@ extern "C" { return mk_c(c)->mk_external_string(buffer.str()); Z3_CATCH_RETURN(""); } + + + Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c, + Z3_solver s, + unsigned num_terms, + Z3_ast const terms[], + unsigned class_ids[]) { + Z3_TRY; + LOG_Z3_get_implied_equalities(c, s, num_terms, terms, class_ids); + ast_manager& m = mk_c(c)->m(); + RESET_ERROR_CODE(); + CHECK_SEARCHING(c); + init_solver(c, s); + lbool result = smt::implied_equalities(m, *to_solver_ref(s), num_terms, to_exprs(terms), class_ids); + return static_cast(result); + Z3_CATCH_RETURN(Z3_L_UNDEF); + } + }; diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp index d43e103c2..c89f89873 100644 --- a/src/api/api_solver_old.cpp +++ b/src/api/api_solver_old.cpp @@ -22,9 +22,7 @@ Revision History: #include"api_log_macros.h" #include"api_context.h" #include"api_model.h" -#include"smt_implied_equalities.h" #include"cancel_eh.h" -#include"api_solver.h" extern "C" { @@ -113,21 +111,6 @@ extern "C" { Z3_CATCH_RETURN(Z3_L_UNDEF); } - Z3_lbool Z3_API Z3_get_implied_equalities(Z3_context c, - Z3_solver s, - unsigned num_terms, - Z3_ast const terms[], - unsigned class_ids[]) { - Z3_TRY; - LOG_Z3_get_implied_equalities(c, s, num_terms, terms, class_ids); - ast_manager& m = mk_c(c)->m(); - RESET_ERROR_CODE(); - CHECK_SEARCHING(c); - lbool result = smt::implied_equalities(m, *to_solver_ref(s), num_terms, to_exprs(terms), class_ids); - return static_cast(result); - Z3_CATCH_RETURN(Z3_L_UNDEF); - } - Z3_lbool Z3_API Z3_check_assumptions(Z3_context c, unsigned num_assumptions, Z3_ast const assumptions[], diff --git a/src/test/get_implied_equalities.cpp b/src/test/get_implied_equalities.cpp index 91c71438f..2576920cc 100644 --- a/src/test/get_implied_equalities.cpp +++ b/src/test/get_implied_equalities.cpp @@ -3,11 +3,11 @@ #include "debug.h" static Z3_ast mk_var(Z3_context ctx, char const* name, Z3_sort s) { - return Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, name), s); + return Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, name), s); } static Z3_ast mk_int_var(Z3_context ctx, char const* name) { - return mk_var(ctx, name, Z3_mk_int_sort(ctx)); + return mk_var(ctx, name, Z3_mk_int_sort(ctx)); } @@ -29,13 +29,15 @@ static void tst_get_implied_equalities1() { unsigned i; Z3_ast terms[7] = { a, b, c, d, fa, fb, fc }; unsigned class_ids[7] = { 0, 0, 0, 0, 0, 0, 0 }; + Z3_solver solver = Z3_mk_simple_solver(ctx); + Z3_solver_inc_ref(ctx, solver); - Z3_assert_cnstr(ctx, Z3_mk_eq(ctx, a, b)); - Z3_assert_cnstr(ctx, Z3_mk_eq(ctx, b, d)); - Z3_assert_cnstr(ctx, Z3_mk_le(ctx, fa, fc)); - Z3_assert_cnstr(ctx, Z3_mk_le(ctx, fc, d)); + Z3_solver_assert(ctx, solver, Z3_mk_eq(ctx, a, b)); + Z3_solver_assert(ctx, solver, Z3_mk_eq(ctx, b, d)); + Z3_solver_assert(ctx, solver, Z3_mk_le(ctx, fa, fc)); + Z3_solver_assert(ctx, solver, Z3_mk_le(ctx, fc, d)); - Z3_get_implied_equalities(ctx, num_terms, terms, class_ids); + Z3_get_implied_equalities(ctx, solver, num_terms, terms, class_ids); for (i = 0; i < num_terms; ++i) { printf("Class %s |-> %d\n", Z3_ast_to_string(ctx, terms[i]), class_ids[i]); } @@ -48,8 +50,8 @@ static void tst_get_implied_equalities1() { SASSERT(class_ids[4] == class_ids[5]); printf("asserting b <= f(a)\n"); - Z3_assert_cnstr(ctx, Z3_mk_le(ctx, b, fa)); - Z3_get_implied_equalities(ctx, num_terms, terms, class_ids); + Z3_solver_assert(ctx, solver, Z3_mk_le(ctx, b, fa)); + Z3_get_implied_equalities(ctx, solver, num_terms, terms, class_ids); for (i = 0; i < num_terms; ++i) { printf("Class %s |-> %d\n", Z3_ast_to_string(ctx, terms[i]), class_ids[i]); } @@ -61,6 +63,7 @@ static void tst_get_implied_equalities1() { SASSERT(class_ids[6] == class_ids[0]); + Z3_solver_dec_ref(ctx, solver); /* delete logical context */ Z3_del_context(ctx); } @@ -72,6 +75,8 @@ static void tst_get_implied_equalities2() { Z3_config cfg = Z3_mk_config(); Z3_context ctx = Z3_mk_context(cfg); Z3_del_config(cfg); + Z3_solver solver = Z3_mk_simple_solver(ctx); + Z3_solver_inc_ref(ctx, solver); Z3_sort int_ty = Z3_mk_int_sort(ctx); Z3_ast a = mk_int_var(ctx,"a"); Z3_ast b = mk_int_var(ctx,"b"); @@ -87,7 +92,7 @@ static void tst_get_implied_equalities2() { Z3_ast terms[5] = { x, y, z, u, v}; unsigned class_ids[5] = { 0, 0, 0, 0, 0}; - Z3_get_implied_equalities(ctx, num_terms, terms, class_ids); + Z3_get_implied_equalities(ctx, solver, num_terms, terms, class_ids); for (i = 0; i < num_terms; ++i) { printf("Class %s |-> %d\n", Z3_ast_to_string(ctx, terms[i]), class_ids[i]); } @@ -100,9 +105,10 @@ static void tst_get_implied_equalities2() { SASSERT(class_ids[2] != class_ids[1]); SASSERT(class_ids[3] != class_ids[1]); SASSERT(class_ids[4] != class_ids[1]); - SASSERT(class_ids[3] != class_ids[2]); + SASSERT(class_ids[3] != class_ids[2]); /* delete logical context */ + Z3_solver_dec_ref(ctx, solver); Z3_del_context(ctx); }