mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

fix get_implied equalities and the unit test

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-12-11 21:39:31 -08:00
parent 89ddb5eac4
commit 635aabf2d5
3 changed files with 36 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/api/api_solver.cpp
View file

@ -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);
}
};

17
src/api/api_solver_old.cpp
View file

@ -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[],

28
src/test/get_implied_equalities.cpp
View file

@ -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);
}