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<Z3_lbool>(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<Z3_lbool>(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);
}