mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 12:51:22 +00:00
Code Activity

SMT2 compliancy fix; NRA includes conversion of Int numerals

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-03-28 18:17:22 +01:00
parent 0c4b792dac
commit 041520f727
2 changed files with 36 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

59
src/ast/arith_decl_plugin.cpp
View file

@ -35,7 +35,7 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
~algebraic_numbers_wrapper() { ~algebraic_numbers_wrapper() {
} }
unsigned mk_id(algebraic_numbers::anum const & val) { unsigned mk_id(algebraic_numbers::anum const & val) {
SASSERT(!m_amanager.is_rational(val)); SASSERT(!m_amanager.is_rational(val));
unsigned new_id = m_id_gen.mk(); unsigned new_id = m_id_gen.mk();
@ -121,7 +121,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
m_int_decl = m->mk_sort(symbol("Int"), sort_info(id, INT_SORT)); m_int_decl = m->mk_sort(symbol("Int"), sort_info(id, INT_SORT));
m->inc_ref(m_int_decl); m->inc_ref(m_int_decl);
sort * i = m_int_decl; sort * i = m_int_decl;
sort * b = m->mk_bool_sort(); sort * b = m->mk_bool_sort();
#define MK_PRED(FIELD, NAME, KIND, SORT) { \ #define MK_PRED(FIELD, NAME, KIND, SORT) { \
@ -140,7 +140,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
MK_PRED(m_i_ge_decl, ">=", OP_GE, i); MK_PRED(m_i_ge_decl, ">=", OP_GE, i);
MK_PRED(m_i_lt_decl, "<", OP_LT, i); MK_PRED(m_i_lt_decl, "<", OP_LT, i);
MK_PRED(m_i_gt_decl, ">", OP_GT, i); MK_PRED(m_i_gt_decl, ">", OP_GT, i);
#define MK_AC_OP(FIELD, NAME, KIND, SORT) { \ #define MK_AC_OP(FIELD, NAME, KIND, SORT) { \
func_decl_info info(id, KIND); \ func_decl_info info(id, KIND); \
info.set_associative(); \ info.set_associative(); \
@ -205,7 +205,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
MK_UNARY(m_asinh_decl, "asinh", OP_ASINH, r); MK_UNARY(m_asinh_decl, "asinh", OP_ASINH, r);
MK_UNARY(m_acosh_decl, "acosh", OP_ACOSH, r); MK_UNARY(m_acosh_decl, "acosh", OP_ACOSH, r);
MK_UNARY(m_atanh_decl, "atanh", OP_ATANH, r); MK_UNARY(m_atanh_decl, "atanh", OP_ATANH, r);
func_decl * pi_decl = m->mk_const_decl(symbol("pi"), r, func_decl_info(id, OP_PI)); func_decl * pi_decl = m->mk_const_decl(symbol("pi"), r, func_decl_info(id, OP_PI));
m_pi = m->mk_const(pi_decl); m_pi = m->mk_const(pi_decl);
m->inc_ref(m_pi); m->inc_ref(m_pi);
@ -213,7 +213,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
func_decl * e_decl = m->mk_const_decl(symbol("euler"), r, func_decl_info(id, OP_E)); func_decl * e_decl = m->mk_const_decl(symbol("euler"), r, func_decl_info(id, OP_E));
m_e = m->mk_const(e_decl); m_e = m->mk_const(e_decl);
m->inc_ref(m_e); m->inc_ref(m_e);
func_decl * z_pw_z_int = m->mk_const_decl(symbol("0^0-int"), i, func_decl_info(id, OP_0_PW_0_INT)); func_decl * z_pw_z_int = m->mk_const_decl(symbol("0^0-int"), i, func_decl_info(id, OP_0_PW_0_INT));
m_0_pw_0_int = m->mk_const(z_pw_z_int); m_0_pw_0_int = m->mk_const(z_pw_z_int);
m->inc_ref(m_0_pw_0_int); m->inc_ref(m_0_pw_0_int);
@ -221,7 +221,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
func_decl * z_pw_z_real = m->mk_const_decl(symbol("0^0-real"), r, func_decl_info(id, OP_0_PW_0_REAL)); func_decl * z_pw_z_real = m->mk_const_decl(symbol("0^0-real"), r, func_decl_info(id, OP_0_PW_0_REAL));
m_0_pw_0_real = m->mk_const(z_pw_z_real); m_0_pw_0_real = m->mk_const(z_pw_z_real);
m->inc_ref(m_0_pw_0_real); m->inc_ref(m_0_pw_0_real);
MK_OP(m_neg_root_decl, "neg-root", OP_NEG_ROOT, r); MK_OP(m_neg_root_decl, "neg-root", OP_NEG_ROOT, r);
MK_UNARY(m_div_0_decl, "/0", OP_DIV_0, r); MK_UNARY(m_div_0_decl, "/0", OP_DIV_0, r);
MK_UNARY(m_idiv_0_decl, "div0", OP_IDIV_0, i); MK_UNARY(m_idiv_0_decl, "div0", OP_IDIV_0, i);
@ -285,7 +285,8 @@ arith_decl_plugin::arith_decl_plugin():
m_idiv_0_decl(0), m_idiv_0_decl(0),
m_mod_0_decl(0), m_mod_0_decl(0),
m_u_asin_decl(0), m_u_asin_decl(0),
m_u_acos_decl(0) { m_u_acos_decl(0),
m_convert_int_numerals_to_real(false) {
} }
arith_decl_plugin::~arith_decl_plugin() { arith_decl_plugin::~arith_decl_plugin() {
@ -418,7 +419,7 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
if (val.is_unsigned()) { if (val.is_unsigned()) {
unsigned u_val = val.get_unsigned(); unsigned u_val = val.get_unsigned();
if (u_val < MAX_SMALL_NUM_TO_CACHE) { if (u_val < MAX_SMALL_NUM_TO_CACHE) {
if (is_int) { if (is_int && !m_convert_int_numerals_to_real) {
app * r = m_small_ints.get(u_val, 0); app * r = m_small_ints.get(u_val, 0);
if (r == 0) { if (r == 0) {
parameter p[2] = { parameter(val), parameter(1) }; parameter p[2] = { parameter(val), parameter(1) };
@ -442,7 +443,7 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
} }
parameter p[2] = { parameter(val), parameter(static_cast<int>(is_int)) }; parameter p[2] = { parameter(val), parameter(static_cast<int>(is_int)) };
func_decl * decl; func_decl * decl;
if (is_int) if (is_int && !m_convert_int_numerals_to_real)
decl = m_manager->mk_const_decl(m_intv_sym, m_int_decl, func_decl_info(m_family_id, OP_NUM, 2, p)); decl = m_manager->mk_const_decl(m_intv_sym, m_int_decl, func_decl_info(m_family_id, OP_NUM, 2, p));
else else
decl = m_manager->mk_const_decl(m_realv_sym, m_real_decl, func_decl_info(m_family_id, OP_NUM, 2, p)); decl = m_manager->mk_const_decl(m_realv_sym, m_real_decl, func_decl_info(m_family_id, OP_NUM, 2, p));
@ -479,14 +480,14 @@ static bool has_real_arg(ast_manager * m, unsigned num_args, expr * const * args
} }
static bool is_const_op(decl_kind k) { static bool is_const_op(decl_kind k) {
return return
k == OP_PI || k == OP_PI ||
k == OP_E || k == OP_E ||
k == OP_0_PW_0_INT || k == OP_0_PW_0_INT ||
k == OP_0_PW_0_REAL; k == OP_0_PW_0_REAL;
} }
func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) { unsigned arity, sort * const * domain, sort * range) {
if (k == OP_NUM) if (k == OP_NUM)
return mk_num_decl(num_parameters, parameters, arity); return mk_num_decl(num_parameters, parameters, arity);
@ -503,7 +504,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
} }
} }
func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range) { unsigned num_args, expr * const * args, sort * range) {
if (k == OP_NUM) if (k == OP_NUM)
return mk_num_decl(num_parameters, parameters, num_args); return mk_num_decl(num_parameters, parameters, num_args);
@ -521,9 +522,17 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
} }
void arith_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const & logic) { void arith_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const & logic) {
// TODO: only define Int and Real in the right logics if (logic == "NRA" ||
sort_names.push_back(builtin_name("Int", INT_SORT)); logic == "QF_NRA" ||
sort_names.push_back(builtin_name("Real", REAL_SORT)); logic == "QF_UFNRA") {
m_convert_int_numerals_to_real = true;
sort_names.push_back(builtin_name("Real", REAL_SORT));
}
else {
// TODO: only define Int and Real in the right logics
sort_names.push_back(builtin_name("Int", INT_SORT));
sort_names.push_back(builtin_name("Real", REAL_SORT));
}
} }
void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const & logic) { void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol const & logic) {
@ -563,16 +572,16 @@ void arith_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
} }
bool arith_decl_plugin::is_value(app * e) const { bool arith_decl_plugin::is_value(app * e) const {
return return
is_app_of(e, m_family_id, OP_NUM) || is_app_of(e, m_family_id, OP_NUM) ||
is_app_of(e, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM) || is_app_of(e, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM) ||
is_app_of(e, m_family_id, OP_PI) || is_app_of(e, m_family_id, OP_PI) ||
is_app_of(e, m_family_id, OP_E); is_app_of(e, m_family_id, OP_E);
} }
bool arith_decl_plugin::is_unique_value(app * e) const { bool arith_decl_plugin::is_unique_value(app * e) const {
return return
is_app_of(e, m_family_id, OP_NUM) || is_app_of(e, m_family_id, OP_NUM) ||
is_app_of(e, m_family_id, OP_PI) || is_app_of(e, m_family_id, OP_PI) ||
is_app_of(e, m_family_id, OP_E); is_app_of(e, m_family_id, OP_E);
} }
@ -671,7 +680,7 @@ expr_ref arith_util::mk_mul_simplify(expr_ref_vector const& args) {
} }
expr_ref arith_util::mk_mul_simplify(unsigned sz, expr* const* args) { expr_ref arith_util::mk_mul_simplify(unsigned sz, expr* const* args) {
expr_ref result(m_manager); expr_ref result(m_manager);
switch (sz) { switch (sz) {
case 0: case 0:
result = mk_numeral(rational(1), true); result = mk_numeral(rational(1), true);
@ -681,7 +690,7 @@ expr_ref arith_util::mk_mul_simplify(unsigned sz, expr* const* args) {
break; break;
default: default:
result = mk_mul(sz, args); result = mk_mul(sz, args);
break; break;
} }
return result; return result;
} }
@ -692,7 +701,7 @@ expr_ref arith_util::mk_add_simplify(expr_ref_vector const& args) {
} }
expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) { expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) {
expr_ref result(m_manager); expr_ref result(m_manager);
switch (sz) { switch (sz) {
case 0: case 0:
result = mk_numeral(rational(0), true); result = mk_numeral(rational(0), true);
@ -702,7 +711,7 @@ expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) {
break; break;
default: default:
result = mk_add(sz, args); result = mk_add(sz, args);
break; break;
} }
return result; return result;
} }

2
src/ast/arith_decl_plugin.h
View file

@ -152,6 +152,8 @@ protected:
ptr_vector<app> m_small_ints; ptr_vector<app> m_small_ints;
ptr_vector<app> m_small_reals; ptr_vector<app> m_small_reals;
bool m_convert_int_numerals_to_real;
func_decl * mk_func_decl(decl_kind k, bool is_real); func_decl * mk_func_decl(decl_kind k, bool is_real);
virtual void set_manager(ast_manager * m, family_id id); virtual void set_manager(ast_manager * m, family_id id);
decl_kind fix_kind(decl_kind k, unsigned arity); decl_kind fix_kind(decl_kind k, unsigned arity);