From 041520f72753f7c4283ccc9bc133df0da9f0d080 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 28 Mar 2017 18:17:22 +0100 Subject: [PATCH] SMT2 compliancy fix; NRA includes conversion of Int numerals --- src/ast/arith_decl_plugin.cpp | 59 ++++++++++++++++++++--------------- src/ast/arith_decl_plugin.h | 2 ++ 2 files changed, 36 insertions(+), 25 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 546f037de..1c01496cf 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -35,7 +35,7 @@ struct arith_decl_plugin::algebraic_numbers_wrapper { ~algebraic_numbers_wrapper() { } - + unsigned mk_id(algebraic_numbers::anum const & val) { SASSERT(!m_amanager.is_rational(val)); 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->inc_ref(m_int_decl); sort * i = m_int_decl; - + sort * b = m->mk_bool_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_lt_decl, "<", OP_LT, i); MK_PRED(m_i_gt_decl, ">", OP_GT, i); - + #define MK_AC_OP(FIELD, NAME, KIND, SORT) { \ func_decl_info info(id, KIND); \ 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_acosh_decl, "acosh", OP_ACOSH, 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)); m_pi = m->mk_const(pi_decl); 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)); m_e = m->mk_const(e_decl); 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)); m_0_pw_0_int = m->mk_const(z_pw_z_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)); m_0_pw_0_real = m->mk_const(z_pw_z_real); m->inc_ref(m_0_pw_0_real); - + 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_idiv_0_decl, "div0", OP_IDIV_0, i); @@ -285,7 +285,8 @@ arith_decl_plugin::arith_decl_plugin(): m_idiv_0_decl(0), m_mod_0_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() { @@ -418,7 +419,7 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) { if (val.is_unsigned()) { unsigned u_val = val.get_unsigned(); 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); if (r == 0) { 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(is_int)) }; 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)); else 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) { - return - k == OP_PI || + return + k == OP_PI || k == OP_E || k == OP_0_PW_0_INT || 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) { if (k == OP_NUM) 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) { if (k == OP_NUM) 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& sort_names, symbol const & logic) { - // 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)); + if (logic == "NRA" || + logic == "QF_NRA" || + 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& op_names, symbol const & logic) { @@ -563,16 +572,16 @@ void arith_decl_plugin::get_op_names(svector& op_names, symbol con } bool arith_decl_plugin::is_value(app * e) const { - return - is_app_of(e, m_family_id, OP_NUM) || + return + 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_PI) || is_app_of(e, m_family_id, OP_E); } bool arith_decl_plugin::is_unique_value(app * e) const { - return - is_app_of(e, m_family_id, OP_NUM) || + return + 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_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 result(m_manager); - + switch (sz) { case 0: result = mk_numeral(rational(1), true); @@ -681,7 +690,7 @@ expr_ref arith_util::mk_mul_simplify(unsigned sz, expr* const* args) { break; default: result = mk_mul(sz, args); - break; + break; } 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 result(m_manager); - + switch (sz) { case 0: result = mk_numeral(rational(0), true); @@ -702,7 +711,7 @@ expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) { break; default: result = mk_add(sz, args); - break; + break; } return result; } diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 410c50852..668eebcc9 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -152,6 +152,8 @@ protected: ptr_vector m_small_ints; ptr_vector m_small_reals; + bool m_convert_int_numerals_to_real; + func_decl * mk_func_decl(decl_kind k, bool is_real); virtual void set_manager(ast_manager * m, family_id id); decl_kind fix_kind(decl_kind k, unsigned arity);