diff --git a/src/tactic/fpa/fpa2bv_approx_tactic.cpp b/src/tactic/fpa/fpa2bv_approx_tactic.cpp index 211da9dc7..4d52a11ca 100644 --- a/src/tactic/fpa/fpa2bv_approx_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_approx_tactic.cpp @@ -30,6 +30,7 @@ #include"fpa2bv_converter_prec.h" #include"fpa2bv_model_converter.h" #include"fpa2bv_converter.h" +#include"propagate_values_tactic.h" #include"fpa2bv_rewriter_prec.h" #include"fpa2bv_approx_tactic.h" #include"const_intro_rewriter.h" @@ -402,6 +403,7 @@ class fpa2bv_approx_tactic: public tactic { mpf_mngr.round_to_integral(rm,est_arg_val[1],est_rhs_value); break; } + default: NOT_IMPLEMENTED_YET(); break; @@ -880,6 +882,8 @@ class fpa2bv_approx_tactic: public tactic { SASSERT(g->is_well_sorted()); + simplify(g); + //fpa2bv fpa2bv_rewriter_prec fpa2bv_rw(*m_temp_manager, fpa2bv, m_params); fpa2bv_rw.m_cfg.set_mappings(&const2prec_map); diff --git a/src/tactic/fpa/fpa2bv_rewriter_prec.h b/src/tactic/fpa/fpa2bv_rewriter_prec.h index 1e3cf71ac..051790ac3 100644 --- a/src/tactic/fpa/fpa2bv_rewriter_prec.h +++ b/src/tactic/fpa/fpa2bv_rewriter_prec.h @@ -75,9 +75,7 @@ struct fpa2bv_rewriter_prec_cfg : public default_rewriter_cfg { bool max_steps_exceeded(unsigned num_steps) const { cooperate("fpa2bv"); - if (memory::get_allocation_size() > m_max_memory) - throw tactic_exception(TACTIC_MAX_MEMORY_MSG); - return num_steps > m_max_steps; + return num_steps > m_max_steps; } br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { @@ -93,14 +91,20 @@ struct fpa2bv_rewriter_prec_cfg : public default_rewriter_cfg { return BR_DONE; } - if (m().is_eq(f)) { - SASSERT(num == 2); - if (m_conv.is_float(args[0])) { - m_conv.mk_eq(args[0], args[1], result); - return BR_DONE; - } - return BR_FAILED; - } + if (m().is_eq(f)) { + SASSERT(num == 2); + //SASSERT(m().get_sort(args[0]) == m().get_sort(args[1])); + sort * ds = f->get_domain()[0]; + if (m_conv.is_float(ds)) { + m_conv.mk_eq(args[0], args[1], result); + return BR_DONE; + } + else if (m_conv.is_rm(ds)) { + result = m().mk_eq(args[0], args[1]); + return BR_DONE; + } + return BR_FAILED; + } if (m().is_ite(f)) { SASSERT(num == 3); @@ -125,10 +129,9 @@ struct fpa2bv_rewriter_prec_cfg : public default_rewriter_cfg { case OP_FPA_NUM: m_conv.mk_numeral(f, num, args, result); return BR_DONE; case OP_FPA_PLUS_INF: m_conv.mk_pinf(f, result); return BR_DONE; case OP_FPA_MINUS_INF: m_conv.mk_ninf(f, result); return BR_DONE; - case OP_FPA_NAN: m_conv.mk_nan(f, result); return BR_DONE; - case OP_FPA_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE; + case OP_FPA_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE; case OP_FPA_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE; - //AZ: Added precision, if precision is MAX_PRECISION uses the regular implementation of the methods + case OP_FPA_NAN: m_conv.mk_nan(f, result); return BR_DONE; case OP_FPA_ADD: m_conv.mk_add(f,get_precision(f), num, args, result);return BR_DONE; case OP_FPA_SUB: @@ -141,14 +144,14 @@ struct fpa2bv_rewriter_prec_cfg : public default_rewriter_cfg { m_conv.mk_div(f, get_precision(f), num, args, result); return BR_DONE; case OP_FPA_REM: m_conv.mk_remainder(f, get_precision(f), num, args, result); return BR_DONE; - case OP_FPA_FMA: + case OP_FPA_ABS: m_conv.mk_abs(f, get_precision(f), num, args, result); return BR_DONE; + case OP_FPA_MIN: m_conv.mk_min(f, get_precision(f), num, args, result); return BR_DONE; + case OP_FPA_MAX: m_conv.mk_max(f, get_precision(f), num, args, result); return BR_DONE; + case OP_FPA_FMA: m_conv.mk_fusedma(f, get_precision(f), num, args, result); return BR_DONE; case OP_FPA_SQRT: m_conv.mk_sqrt(f, get_precision(f), num, args, result); return BR_DONE; - case OP_FPA_ABS: m_conv.mk_abs(f, get_precision(f), num, args, result); return BR_DONE; - case OP_FPA_MIN: m_conv.mk_min(f, get_precision(f), num, args, result); return BR_DONE; - case OP_FPA_MAX: m_conv.mk_max(f, get_precision(f), num, args, result); return BR_DONE; - case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, get_precision(f), num, args, result); return BR_DONE; + case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, get_precision(f), num, args, result); return BR_DONE; case OP_FPA_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE; case OP_FPA_LT: m_conv.mk_float_lt(f, num, args, result); return BR_DONE; case OP_FPA_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE; @@ -159,17 +162,45 @@ struct fpa2bv_rewriter_prec_cfg : public default_rewriter_cfg { case OP_FPA_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE; case OP_FPA_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE; case OP_FPA_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE; - case OP_FPA_IS_NEGATIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE; case OP_FPA_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE; + case OP_FPA_IS_NEGATIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE; case OP_FPA_TO_FP: m_conv.mk_to_fp(f, num, args, result); return BR_DONE; - case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; - default: - TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; - for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); - throw tactic_exception("NYI"); - } - } - return BR_FAILED; + case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE; + case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE; + case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE; + case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; + case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; + case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; + case OP_FPA_INTERNAL_BVWRAP: + case OP_FPA_INTERNAL_BVUNWRAP: + case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED; + default: + TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; + for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); + NOT_IMPLEMENTED_YET(); + } + } + + if (f->get_family_id() == null_family_id) + { + bool is_float_uf = m_conv.is_float(f->get_range()); + unsigned i = 0; + while (!is_float_uf && i < num) + { + is_float_uf = m_conv.is_float(f->get_domain()[i]); + i++; + } + + if (is_float_uf) + { + m_conv.mk_uninterpreted_function(f, num, args, result); + return BR_DONE; + } + } + + return BR_FAILED; } bool pre_visit(expr * t)