diff --git a/contrib/cmake/src/ast/rewriter/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/CMakeLists.txt index 921cace75..14bcebf46 100644 --- a/contrib/cmake/src/ast/rewriter/CMakeLists.txt +++ b/contrib/cmake/src/ast/rewriter/CMakeLists.txt @@ -20,6 +20,8 @@ z3_add_component(rewriter seq_rewriter.cpp th_rewriter.cpp var_subst.cpp + bv_trailing.cpp + mk_extract_proc.cpp COMPONENT_DEPENDENCIES ast automata diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp index 7967cdb63..eb24ee927 100644 --- a/src/ackermannization/ackr_model_converter.cpp +++ b/src/ackermannization/ackr_model_converter.cpp @@ -63,19 +63,13 @@ protected: void add_entry(model_evaluator & evaluator, app* term, expr* value, obj_map& interpretations); - void convert_sorts(model * source, model * destination); void convert_constants(model * source, model * destination); }; void ackr_model_converter::convert(model * source, model * destination) { - //SASSERT(source->get_num_functions() == 0); - for (unsigned i = 0; i < source->get_num_functions(); i++) { - func_decl * const fd = source->get_function(i); - func_interp * const fi = source->get_func_interp(fd); - destination->register_decl(fd, fi); - } + destination->copy_func_interps(*source); + destination->copy_usort_interps(*source); convert_constants(source,destination); - convert_sorts(source,destination); } void ackr_model_converter::convert_constants(model * source, model * destination) { @@ -136,14 +130,6 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator, } } -void ackr_model_converter::convert_sorts(model * source, model * destination) { - for (unsigned i = 0; i < source->get_num_uninterpreted_sorts(); i++) { - sort * const s = source->get_uninterpreted_sort(i); - ptr_vector u = source->get_universe(s); - destination->register_usort(s, u.size(), u.c_ptr()); - } -} - model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info) { return alloc(ackr_model_converter, m, info); } diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 5c7a819da..7c846cc99 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4538,6 +4538,9 @@ extern "C" { If \c model_completion is Z3_TRUE, then Z3 will assign an interpretation for any constant or function that does not have an interpretation in \c m. These constants and functions were essentially don't cares. + If \c model_completion is Z3_FALSE, then Z3 will not assign interpretations to constants for functions that do + not have interpretations in \c m. Evaluation behaves as the identify function in this case. + The evaluation may fail for the following reasons: - \c t contains a quantifier. @@ -4547,6 +4550,8 @@ extern "C" { - \c t is type incorrect. + - \c Z3_interrupt was invoked during evaluation. + def_API('Z3_model_eval', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _in(BOOL), _out(AST))) */ Z3_bool_opt Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast * v); diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index b1f3491fe..03b4fe637 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -51,7 +51,7 @@ void bv_decl_plugin::set_manager(ast_manager * m, family_id id) { m_bit1 = m->mk_const_decl(symbol("bit1"), get_bv_sort(1), func_decl_info(m_family_id, OP_BIT1)); m->inc_ref(m_bit0); m->inc_ref(m_bit1); - + sort * b = m->mk_bool_sort(); sort * d[3] = {b, b, b}; m_carry = m_manager->mk_func_decl(symbol("carry"), 3, d, b, func_decl_info(m_family_id, OP_CARRY)); @@ -105,7 +105,7 @@ void bv_decl_plugin::finalize() { DEC_REF(m_bv_slt); DEC_REF(m_bv_ugt); DEC_REF(m_bv_sgt); - + DEC_REF(m_bv_and); DEC_REF(m_bv_or); DEC_REF(m_bv_not); @@ -113,7 +113,7 @@ void bv_decl_plugin::finalize() { DEC_REF(m_bv_nand); DEC_REF(m_bv_nor); DEC_REF(m_bv_xnor); - + DEC_REF(m_bv_redor); DEC_REF(m_bv_redand); DEC_REF(m_bv_comp); @@ -181,7 +181,7 @@ sort * bv_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter c func_decl * bv_decl_plugin::mk_binary(ptr_vector & decls, decl_kind k, char const * name, unsigned bv_size, bool ac, bool idempotent) { force_ptr_array_size(decls, bv_size + 1); - + if (decls[bv_size] == 0) { sort * s = get_bv_sort(bv_size); func_decl_info info(m_family_id, k); @@ -198,7 +198,7 @@ func_decl * bv_decl_plugin::mk_binary(ptr_vector & decls, decl_kind k func_decl * bv_decl_plugin::mk_unary(ptr_vector & decls, decl_kind k, char const * name, unsigned bv_size) { force_ptr_array_size(decls, bv_size + 1); - + if (decls[bv_size] == 0) { sort * s = get_bv_sort(bv_size); decls[bv_size] = m_manager->mk_func_decl(symbol(name), s, s, func_decl_info(m_family_id, k)); @@ -223,7 +223,7 @@ func_decl * bv_decl_plugin::mk_int2bv(unsigned bv_size, unsigned num_parameters, if (m_int2bv[bv_size] == 0) { sort * s = get_bv_sort(bv_size); - m_int2bv[bv_size] = m_manager->mk_func_decl(symbol("int2bv"), domain[0], s, + m_int2bv[bv_size] = m_manager->mk_func_decl(symbol("int2bv"), domain[0], s, func_decl_info(m_family_id, OP_INT2BV, num_parameters, parameters)); m_manager->inc_ref(m_int2bv[bv_size]); } @@ -239,9 +239,9 @@ func_decl * bv_decl_plugin::mk_bv2int(unsigned bv_size, unsigned num_parameters, m_manager->raise_exception("expecting one argument to bv2int"); return 0; } - + if (m_bv2int[bv_size] == 0) { - m_bv2int[bv_size] = m_manager->mk_func_decl(symbol("bv2int"), domain[0], m_int_sort, + m_bv2int[bv_size] = m_manager->mk_func_decl(symbol("bv2int"), domain[0], m_int_sort, func_decl_info(m_family_id, OP_BV2INT)); m_manager->inc_ref(m_bv2int[bv_size]); } @@ -251,7 +251,7 @@ func_decl * bv_decl_plugin::mk_bv2int(unsigned bv_size, unsigned num_parameters, func_decl * bv_decl_plugin::mk_pred(ptr_vector & decls, decl_kind k, char const * name, unsigned bv_size) { force_ptr_array_size(decls, bv_size + 1); - + if (decls[bv_size] == 0) { sort * s = get_bv_sort(bv_size); decls[bv_size] = m_manager->mk_func_decl(symbol(name), s, s, m_manager->mk_bool_sort(), func_decl_info(m_family_id, k)); @@ -263,7 +263,7 @@ func_decl * bv_decl_plugin::mk_pred(ptr_vector & decls, decl_kind k, func_decl * bv_decl_plugin::mk_reduction(ptr_vector & decls, decl_kind k, char const * name, unsigned bv_size) { force_ptr_array_size(decls, bv_size + 1); - + if (decls[bv_size] == 0) { sort * d = get_bv_sort(bv_size); sort * r = get_bv_sort(1); @@ -276,7 +276,7 @@ func_decl * bv_decl_plugin::mk_reduction(ptr_vector & decls, decl_kin func_decl * bv_decl_plugin::mk_comp(unsigned bv_size) { force_ptr_array_size(m_bv_comp, bv_size + 1); - + if (m_bv_comp[bv_size] == 0) { sort * d = get_bv_sort(bv_size); sort * r = get_bv_sort(1); @@ -326,7 +326,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned bv_size) { case OP_BXOR: return mk_binary(m_bv_xor, k, "bvxor", bv_size, true); case OP_BNAND: return mk_binary(m_bv_nand, k, "bvnand", bv_size, false); case OP_BNOR: return mk_binary(m_bv_nor, k, "bvnor", bv_size, false); - case OP_BXNOR: return mk_binary(m_bv_xnor, k, "bvxnor", bv_size, false); + case OP_BXNOR: return mk_binary(m_bv_xnor, k, "bvxnor", bv_size, false); case OP_BREDOR: return mk_reduction(m_bv_redor, k, "bvredor", bv_size); case OP_BREDAND: return mk_reduction(m_bv_redand, k, "bvredand", bv_size); @@ -334,7 +334,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned bv_size) { case OP_BUMUL_NO_OVFL: return mk_pred(m_bv_mul_ovfl, k, "bvumul_noovfl", bv_size); case OP_BSMUL_NO_OVFL: return mk_pred(m_bv_smul_ovfl, k, "bvsmul_noovfl", bv_size); case OP_BSMUL_NO_UDFL: return mk_pred(m_bv_smul_udfl, k, "bvsmul_noudfl", bv_size); - + case OP_BSHL: return mk_binary(m_bv_shl, k, "bvshl", bv_size, false); case OP_BLSHR: return mk_binary(m_bv_lshr, k, "bvlshr", bv_size, false); case OP_BASHR: return mk_binary(m_bv_ashr, k, "bvashr", bv_size, false); @@ -369,23 +369,24 @@ bool bv_decl_plugin::get_concat_size(unsigned arity, sort * const * domain, int return true; } -bool bv_decl_plugin::get_extend_size(unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, int & result) { +bool bv_decl_plugin::get_extend_size(unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, int & result) { int arg_sz; - if (arity != 1 || num_parameters != 1 || !parameters[0].is_int() || !get_bv_size(domain[0], arg_sz)) { + if (arity != 1 || !get_bv_size(domain[0], arg_sz) || + num_parameters != 1 || !parameters[0].is_int() || parameters[0].get_int() < 0) { return false; } result = arg_sz + parameters[0].get_int(); return true; } -bool bv_decl_plugin::get_extract_size(unsigned num_parameters, parameter const * parameters, +bool bv_decl_plugin::get_extract_size(unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, int & result) { int arg_sz; if (arity != 1 || - !get_bv_size(domain[0], arg_sz) || - num_parameters != 2 || - !parameters[0].is_int() || + !get_bv_size(domain[0], arg_sz) || + num_parameters != 2 || + !parameters[0].is_int() || !parameters[1].is_int() || parameters[1].get_int() > parameters[0].get_int() || parameters[0].get_int() >= arg_sz) { @@ -432,7 +433,7 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const return m_manager->mk_const_decl(m_bv_sym, bv, func_decl_info(m_family_id, OP_BV_NUM, num_parameters, ps)); } -func_decl * bv_decl_plugin::mk_bit2bool(unsigned bv_size, unsigned num_parameters, parameter const * parameters, +func_decl * bv_decl_plugin::mk_bit2bool(unsigned bv_size, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain) { if (!(num_parameters == 1 && parameters[0].is_int() && arity == 1 && parameters[0].get_int() < static_cast(bv_size))) { m_manager->raise_exception("invalid bit2bool declaration"); @@ -443,7 +444,7 @@ func_decl * bv_decl_plugin::mk_bit2bool(unsigned bv_size, unsigned num_parameter ptr_vector & v = m_bit2bool[bv_size]; v.reserve(bv_size, 0); if (v[idx] == 0) { - v[idx] = m_manager->mk_func_decl(m_bit2bool_sym, domain[0], m_manager->mk_bool_sort(), + v[idx] = m_manager->mk_func_decl(m_bit2bool_sym, domain[0], m_manager->mk_bool_sort(), func_decl_info(m_family_id, OP_BIT2BOOL, num_parameters, parameters)); m_manager->inc_ref(v[idx]); } @@ -520,34 +521,34 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p switch (k) { case OP_BIT2BOOL: return mk_bit2bool(bv_size, num_parameters, parameters, arity, domain); - case OP_INT2BV: + case OP_INT2BV: return mk_int2bv(bv_size, num_parameters, parameters, arity, domain); - case OP_BV2INT: + case OP_BV2INT: return mk_bv2int(bv_size, num_parameters, parameters, arity, domain); - case OP_CONCAT: + case OP_CONCAT: if (!get_concat_size(arity, domain, r_size)) m_manager->raise_exception("invalid concat application"); - return m_manager->mk_func_decl(m_concat_sym, arity, domain, get_bv_sort(r_size), + return m_manager->mk_func_decl(m_concat_sym, arity, domain, get_bv_sort(r_size), func_decl_info(m_family_id, k)); case OP_SIGN_EXT: if (!get_extend_size(num_parameters, parameters, arity, domain, r_size)) m_manager->raise_exception("invalid sign_extend application"); - return m_manager->mk_func_decl(m_sign_extend_sym, arity, domain, get_bv_sort(r_size), + return m_manager->mk_func_decl(m_sign_extend_sym, arity, domain, get_bv_sort(r_size), func_decl_info(m_family_id, k, num_parameters, parameters)); case OP_ZERO_EXT: if (!get_extend_size(num_parameters, parameters, arity, domain, r_size)) m_manager->raise_exception("invalid zero_extend application"); - return m_manager->mk_func_decl(m_zero_extend_sym, arity, domain, get_bv_sort(r_size), + return m_manager->mk_func_decl(m_zero_extend_sym, arity, domain, get_bv_sort(r_size), func_decl_info(m_family_id, k, num_parameters, parameters)); case OP_EXTRACT: if (!get_extract_size(num_parameters, parameters, arity, domain, r_size)) m_manager->raise_exception("invalid extract application"); - return m_manager->mk_func_decl(m_extract_sym, arity, domain, get_bv_sort(r_size), + return m_manager->mk_func_decl(m_extract_sym, arity, domain, get_bv_sort(r_size), func_decl_info(m_family_id, k, num_parameters, parameters)); case OP_ROTATE_LEFT: if (arity != 1) m_manager->raise_exception("rotate left expects one argument"); - return m_manager->mk_func_decl(m_rotate_left_sym, arity, domain, domain[0], + return m_manager->mk_func_decl(m_rotate_left_sym, arity, domain, domain[0], func_decl_info(m_family_id, k, num_parameters, parameters)); case OP_ROTATE_RIGHT: if (arity != 1) @@ -561,14 +562,14 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p m_manager->raise_exception("repeat expects one nonzero integer parameter"); if (!get_bv_size(domain[0], bv_size)) m_manager->raise_exception("repeat expects an argument with bit-vector sort"); - return m_manager->mk_func_decl(m_repeat_sym, arity, domain, get_bv_sort(bv_size * parameters[0].get_int()), + return m_manager->mk_func_decl(m_repeat_sym, arity, domain, get_bv_sort(bv_size * parameters[0].get_int()), func_decl_info(m_family_id, k, num_parameters, parameters)); default: return 0; } } -func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned num_args, expr * const * args, sort * range) { ast_manager& m = *m_manager; int bv_size; @@ -657,7 +658,7 @@ bool bv_decl_plugin::are_distinct(app * a, app * b) const { expr * b_term; get_offset_term(a, a_term, a_offset); get_offset_term(b, b_term, b_offset); - TRACE("bv_are_distinct", + TRACE("bv_are_distinct", tout << mk_ismt2_pp(a, *m_manager) << "\n" << mk_ismt2_pp(b, *m_manager) << "\n"; tout << "---->\n"; tout << "a: " << a_offset << " + " << mk_ismt2_pp(a_term, *m_manager) << "\n"; @@ -715,24 +716,24 @@ void bv_decl_plugin::get_op_names(svector & op_names, symbol const op_names.push_back(builtin_name("bvashr",OP_BASHR)); op_names.push_back(builtin_name("rotate_left",OP_ROTATE_LEFT)); op_names.push_back(builtin_name("rotate_right",OP_ROTATE_RIGHT)); - + if (logic == symbol::null) { op_names.push_back(builtin_name("bvumul_noovfl",OP_BUMUL_NO_OVFL)); op_names.push_back(builtin_name("bvsmul_noovfl",OP_BSMUL_NO_OVFL)); op_names.push_back(builtin_name("bvsmul_noudfl",OP_BSMUL_NO_UDFL)); - + op_names.push_back(builtin_name("bvsdiv0", OP_BSDIV0)); op_names.push_back(builtin_name("bvudiv0", OP_BUDIV0)); op_names.push_back(builtin_name("bvsrem0", OP_BSREM0)); op_names.push_back(builtin_name("bvurem0", OP_BUREM0)); op_names.push_back(builtin_name("bvsmod0", OP_BSMOD0)); - + op_names.push_back(builtin_name("bvsdiv_i", OP_BSDIV_I)); op_names.push_back(builtin_name("bvudiv_i", OP_BUDIV_I)); op_names.push_back(builtin_name("bvsrem_i", OP_BSREM_I)); op_names.push_back(builtin_name("bvurem_i", OP_BUREM_I)); op_names.push_back(builtin_name("bvumod_i", OP_BSMOD_I)); - + op_names.push_back(builtin_name("ext_rotate_left",OP_EXT_ROTATE_LEFT)); op_names.push_back(builtin_name("ext_rotate_right",OP_EXT_ROTATE_RIGHT)); op_names.push_back(builtin_name("int2bv",OP_INT2BV)); @@ -755,7 +756,7 @@ rational bv_recognizers::norm(rational const & val, unsigned bv_size, bool is_si if (r >= rational::power_of_two(bv_size - 1)) { r -= rational::power_of_two(bv_size); } - if (r < -rational::power_of_two(bv_size - 1)) { + if (r < -rational::power_of_two(bv_size - 1)) { r += rational::power_of_two(bv_size); } } @@ -770,7 +771,7 @@ bool bv_recognizers::has_sign_bit(rational const & n, unsigned bv_size) const { } bool bv_recognizers::is_bv_sort(sort const * s) const { - return (s->get_family_id() == get_fid() && s->get_decl_kind() == BV_SORT && s->get_num_parameters() == 1); + return (s->get_family_id() == get_fid() && s->get_decl_kind() == BV_SORT && s->get_num_parameters() == 1); } bool bv_recognizers::is_numeral(expr const * n, rational & val, unsigned & bv_size) const { @@ -821,11 +822,11 @@ bool bv_recognizers::mult_inverse(rational const & n, unsigned bv_size, rational result = n; return true; } - + if (!mod(n, rational(2)).is_one()) { return false; } - + rational g; rational x; rational y; @@ -874,5 +875,5 @@ unsigned bv_util::get_int2bv_size(parameter const& p) { app * bv_util::mk_bv2int(expr* e) { sort* s = m_manager.mk_sort(m_manager.mk_family_id("arith"), INT_SORT); parameter p(s); - return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e); + return m_manager.mk_app(get_fid(), OP_BV2INT, 1, &p, 1, &e); } diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 7322977a0..def05f014 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -22,45 +22,13 @@ Notes: #include"ast_smt2_pp.h" -mk_extract_proc::mk_extract_proc(bv_util & u): - m_util(u), - m_high(0), - m_low(UINT_MAX), - m_domain(0), - m_f_cached(0) { -} - -mk_extract_proc::~mk_extract_proc() { - if (m_f_cached) { - // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain - ast_manager & m = m_util.get_manager(); - m.dec_ref(m_f_cached); - } -} - -app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) { - ast_manager & m = m_util.get_manager(); - sort * s = m.get_sort(arg); - if (m_low == low && m_high == high && m_domain == s) - return m.mk_app(m_f_cached, arg); - // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain - if (m_f_cached) - m.dec_ref(m_f_cached); - app * r = to_app(m_util.mk_extract(high, low, arg)); - m_high = high; - m_low = low; - m_domain = s; - m_f_cached = r->get_decl(); - m.inc_ref(m_f_cached); - return r; -} - void bv_rewriter::updt_local_params(params_ref const & _p) { bv_rewriter_params p(_p); m_hi_div0 = p.hi_div0(); m_elim_sign_ext = p.elim_sign_ext(); m_mul2concat = p.mul2concat(); m_bit2bool = p.bit2bool(); + m_trailing = p.bv_trailing(); m_blast_eq_value = p.blast_eq_value(); m_split_concat_eq = p.split_concat_eq(); m_udiv2mul = p.udiv2mul(); @@ -2124,6 +2092,15 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { return st; } + if (m_trailing) { + st = m_rm_trailing.eq_remove_trailing(lhs, rhs, result); + m_rm_trailing.reset_cache(1 << 12); + if (st != BR_FAILED) { + TRACE("eq_remove_trailing", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result, m()) << "\n";); + return st; + } + } + st = mk_mul_eq(lhs, rhs, result); if (st != BR_FAILED) { TRACE("mk_mul_eq", tout << mk_ismt2_pp(lhs, m()) << "\n=\n" << mk_ismt2_pp(rhs, m()) << "\n----->\n" << mk_ismt2_pp(result,m()) << "\n";); @@ -2187,6 +2164,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { return BR_FAILED; } + br_status bv_rewriter::mk_mkbv(unsigned num, expr * const * args, expr_ref & result) { if (m_mkbv2num) { unsigned i; diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index f01743ca9..7135c52ba 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -22,18 +22,8 @@ Notes: #include"poly_rewriter.h" #include"bv_decl_plugin.h" #include"arith_decl_plugin.h" - -class mk_extract_proc { - bv_util & m_util; - unsigned m_high; - unsigned m_low; - sort * m_domain; - func_decl * m_f_cached; -public: - mk_extract_proc(bv_util & u); - ~mk_extract_proc(); - app * operator()(unsigned high, unsigned low, expr * arg); -}; +#include"mk_extract_proc.h" +#include"bv_trailing.h" class bv_rewriter_core { protected: @@ -58,6 +48,7 @@ public: class bv_rewriter : public poly_rewriter { mk_extract_proc m_mk_extract; + bv_trailing m_rm_trailing; arith_util m_autil; bool m_hi_div0; bool m_elim_sign_ext; @@ -69,6 +60,7 @@ class bv_rewriter : public poly_rewriter { bool m_udiv2mul; bool m_bvnot2arith; bool m_bv_sort_ac; + bool m_trailing; bool is_zero_bit(expr * x, unsigned idx); @@ -148,6 +140,7 @@ public: bv_rewriter(ast_manager & m, params_ref const & p = params_ref()): poly_rewriter(m, p), m_mk_extract(m_util), + m_rm_trailing(m_mk_extract), m_autil(m) { updt_local_params(p); } diff --git a/src/ast/rewriter/bv_rewriter_params.pyg b/src/ast/rewriter/bv_rewriter_params.pyg index 5feece753..0f0163fb1 100644 --- a/src/ast/rewriter/bv_rewriter_params.pyg +++ b/src/ast/rewriter/bv_rewriter_params.pyg @@ -9,5 +9,6 @@ def_module_params(module_name='rewriter', ("hi_div0", BOOL, True, "use the 'hardware interpretation' for division by zero (for bit-vector terms)"), ("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation"), ("bvnot2arith", BOOL, False, "replace (bvnot x) with (bvsub -1 x)"), - ("bv_sort_ac", BOOL, False, "sort the arguments of all AC operators") + ("bv_sort_ac", BOOL, False, "sort the arguments of all AC operators"), + ("bv_trailing", BOOL, False, "lean removal of trailing zeros") )) diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp new file mode 100644 index 000000000..d3087e776 --- /dev/null +++ b/src/ast/rewriter/bv_trailing.cpp @@ -0,0 +1,402 @@ +/*++ + Copyright (c) 2016 Microsoft Corporation + + Module Name: + + bv_trailing.cpp + + Abstract: + + + Author: + + Mikolas Janota (MikolasJanota) + + Revision History: +--*/ +#include"bv_trailing.h" +#include"bv_decl_plugin.h" +#include"ast_smt2_pp.h" + +// The analyzer gives up analysis after going TRAILING_DEPTH deep. +// This number shouldn't be too big. +#define TRAILING_DEPTH 5 + +struct bv_trailing::imp { + typedef rational numeral; + typedef obj_map > map; + mk_extract_proc& m_mk_extract; + bv_util& m_util; + ast_manager& m; + + // keep a cache for each depth, using the convention that m_count_cache[TRAILING_DEPTH] is top-level + map* m_count_cache[TRAILING_DEPTH + 1]; + + imp(mk_extract_proc& mk_extract) + : m_mk_extract(mk_extract) + , m_util(mk_extract.bvutil()) + , m(mk_extract.m()) { + for (unsigned i = 0; i <= TRAILING_DEPTH; ++i) + m_count_cache[i] = NULL; + } + + virtual ~imp() { + reset_cache(0); + } + + br_status eq_remove_trailing(expr * e1, expr * e2, expr_ref& result) { + TRACE("bv-trailing", tout << mk_ismt2_pp(e1, m) << "\n=\n" << mk_ismt2_pp(e2, m) << "\n";); + SASSERT(m_util.is_bv(e1) && m_util.is_bv(e2)); + SASSERT(m_util.get_bv_size(e1) == m_util.get_bv_size(e2)); + unsigned max1, min1, max2, min2; + count_trailing(e1, min1, max1, TRAILING_DEPTH); + count_trailing(e2, min2, max2, TRAILING_DEPTH); + if (min1 > max2 || min2 > max1) { // bounds have empty intersection + result = m.mk_false(); + return BR_DONE; + } + const unsigned min = std::min(min1, min2); // remove the minimum of the two lower bounds + if (min == 0) { // nothing to remove + result = m.mk_eq(e1, e2); + return BR_FAILED; + } + const unsigned sz = m_util.get_bv_size(e1); + if (min == sz) { // everything removed, unlikely but we check anyhow for safety + result = m.mk_true(); + return BR_DONE; + } + expr_ref out1(m); + expr_ref out2(m); + const unsigned rm1 = remove_trailing(e1, min, out1, TRAILING_DEPTH); + const unsigned rm2 = remove_trailing(e2, min, out2, TRAILING_DEPTH); + SASSERT(rm1 == min && rm2 == min); + const bool are_eq = m.are_equal(out1, out2); + result = are_eq ? m.mk_true() : m.mk_eq(out1, out2); + return are_eq ? BR_DONE : BR_REWRITE2; + } + + // This routine needs to be implemented carefully so that whenever it + // returns a lower bound on trailing zeros min, the routine remove_trailing + // must be capable of removing at least that many zeros from the expression. + void count_trailing(expr * e, unsigned& min, unsigned& max, unsigned depth) { + SASSERT(e && m_util.is_bv(e)); + if (is_cached(depth, e, min, max)) return; + count_trailing_core(e, min, max, depth); + TRACE("bv-trailing", tout << mk_ismt2_pp(e, m) << "\n:" << min << " - " << max << "\n";); + SASSERT(min <= max); + SASSERT(max <= m_util.get_bv_size(e)); + cache(depth, e, min, max); // store result into the cache + } + + unsigned remove_trailing(expr * e, unsigned n, expr_ref& result, unsigned depth) { + const unsigned retv = remove_trailing_core(e, n, result, depth); + CTRACE("bv-trailing", result.get(), tout << mk_ismt2_pp(e, m) << "\n--->\n" << mk_ismt2_pp(result.get(), m) << "\n";); + CTRACE("bv-trailing", !result.get(), tout << mk_ismt2_pp(e, m) << "\n---> [EMPTY]\n";); + return retv; + } + + // Assumes that count_trailing gives me a lower bound that we can also remove from each summand. + unsigned remove_trailing_add(app * a, unsigned n, expr_ref& result, unsigned depth) { + SASSERT(m_util.is_bv_add(a)); + const unsigned num = a->get_num_args(); + if (depth <= 1) { + result = a; + return 0; + } + unsigned min, max; + count_trailing(a, min, max, depth); // caching is important here + const unsigned to_rm = std::min(min, n); + if (to_rm == 0) { + result = a; + return 0; + } + + const unsigned sz = m_util.get_bv_size(a); + + if (to_rm == sz) { + result = NULL; + return sz; + } + + expr_ref_vector new_args(m); + expr_ref tmp(m); + for (unsigned i = 0; i < num; ++i) { + expr * const curr = a->get_arg(i); + const unsigned crm = remove_trailing(curr, to_rm, tmp, depth - 1); + new_args.push_back(tmp); + SASSERT(crm == to_rm); + } + result = m.mk_app(m_util.get_fid(), OP_BADD, new_args.size(), new_args.c_ptr()); + return to_rm; + } + + unsigned remove_trailing_mul(app * a, unsigned n, expr_ref& result, unsigned depth) { + SASSERT(m_util.is_bv_mul(a)); + const unsigned num = a->get_num_args(); + if (depth <= 1 || !num) { + result = a; + return 0; + } + expr_ref tmp(m); + expr * const coefficient = a->get_arg(0); + const unsigned retv = remove_trailing(coefficient, n, tmp, depth - 1); + SASSERT(retv <= n); + if (retv == 0) { + result = a; + return 0; + } + expr_ref_vector new_args(m); + numeral c_val; + unsigned c_sz; + if (!m_util.is_numeral(tmp, c_val, c_sz) || !c_val.is_one()) + new_args.push_back(tmp); + const unsigned sz = m_util.get_bv_size(coefficient); + const unsigned new_sz = sz - retv; + + if (!new_sz) { + result = NULL; + return retv; + } + + SASSERT(m_util.get_bv_size(tmp) == new_sz); + for (unsigned i = 1; i < num; i++) { + expr * const curr = a->get_arg(i); + new_args.push_back(m_mk_extract(new_sz - 1, 0, curr)); + } + switch (new_args.size()) { + case 0: result = m_util.mk_numeral(1, new_sz); break; + case 1: result = new_args.get(0); break; + default: result = m.mk_app(m_util.get_fid(), OP_BMUL, new_args.size(), new_args.c_ptr()); + } + return retv; + } + + unsigned remove_trailing_concat(app * a, unsigned n, expr_ref& result, unsigned depth) { + SASSERT(m_util.is_concat(a)); + if (depth <= 1) { + result = a; + return 0; + } + const unsigned num = a->get_num_args(); + unsigned retv = 0; + unsigned i = num; + expr_ref new_last(NULL, m); + while (i && retv < n) { + i--; + expr * const curr = a->get_arg(i); + const unsigned cur_rm = remove_trailing(curr, n, new_last, depth - 1); + const unsigned curr_sz = m_util.get_bv_size(curr); + retv += cur_rm; + if (cur_rm < curr_sz) break; + } + if (retv == 0) { + result = a; + return 0; + } + + if (!i) {// all args eaten completely + SASSERT(new_last.get() == NULL); + SASSERT(retv == m_util.get_bv_size(a)); + result = NULL; + return retv; + } + + expr_ref_vector new_args(m); + for (unsigned j = 0; j < i; ++j) + new_args.push_back(a->get_arg(j)); + if (new_last.get()) new_args.push_back(new_last); + result = new_args.size() == 1 ? new_args.get(0) + : m_util.mk_concat(new_args.size(), new_args.c_ptr()); + return retv; + } + + unsigned remove_trailing(size_t max_rm, numeral& a) { + numeral two(2); + unsigned retv = 0; + while (max_rm && a.is_even()) { + div(a, two, a); + ++retv; + --max_rm; + } + return retv; + } + + unsigned remove_trailing_core(expr * e, unsigned n, expr_ref& result, unsigned depth) { + SASSERT(m_util.is_bv(e)); + if (!depth || !n) return 0; + unsigned sz; + unsigned retv = 0; + numeral e_val; + if (m_util.is_numeral(e, e_val, sz)) { + retv = remove_trailing(n, e_val); + const unsigned new_sz = sz - retv; + result = new_sz ? (retv ? m_util.mk_numeral(e_val, new_sz) : e) : NULL; + return retv; + } + if (m_util.is_bv_mul(e)) + return remove_trailing_mul(to_app(e), n, result, depth); + if (m_util.is_bv_add(e)) + return remove_trailing_add(to_app(e), n, result, depth); + if (m_util.is_concat(e)) + return remove_trailing_concat(to_app(e), n, result, depth); + return 0; + } + + + void count_trailing_concat(app * a, unsigned& min, unsigned& max, unsigned depth) { + if (depth <= 1) { + min = 0; + max = m_util.get_bv_size(a); + } + max = min = 0; // treat empty concat as the empty string + unsigned num = a->get_num_args(); + bool update_min = true; + bool update_max = true; + unsigned tmp_min, tmp_max; + while (num-- && update_max) { + expr * const curr = a->get_arg(num); + const unsigned curr_sz = m_util.get_bv_size(curr); + count_trailing(curr, tmp_min, tmp_max, depth - 1); + SASSERT(curr_sz != tmp_min || curr_sz == tmp_max); + max += tmp_max; + if (update_min) min += tmp_min; + // continue updating only if eaten away completely + update_min &= curr_sz == tmp_min; + update_max &= curr_sz == tmp_max; + } + } + + void count_trailing_add(app * a, unsigned& min, unsigned& max, unsigned depth) { + if (depth <= 1) { + min = 0; + max = m_util.get_bv_size(a); + } + const unsigned num = a->get_num_args(); + const unsigned sz = m_util.get_bv_size(a); + min = max = sz; // treat empty addition as 0 + unsigned tmp_min; + unsigned tmp_max; + bool known_parity = true; + bool is_odd = false; + for (unsigned i = 0; i < num; ++i) { + expr * const curr = a->get_arg(i); + count_trailing(curr, tmp_min, tmp_max, depth - 1); + min = std::min(min, tmp_min); + known_parity = known_parity && (!tmp_max || tmp_min); + if (known_parity && !tmp_max) is_odd = !is_odd; + if (!known_parity && !min) break; // no more information can be gained + } + max = known_parity && is_odd ? 0 : sz; // max is known if parity is 1 + } + + void count_trailing_mul(app * a, unsigned& min, unsigned& max, unsigned depth) { + if (depth <= 1) { + min = 0; + max = m_util.get_bv_size(a); + } + + const unsigned num = a->get_num_args(); + if (!num) { + max = min = 0; // treat empty multiplication as 1 + return; + } + // assume that numerals are pushed in the front, count only for the first element + expr * const curr = a->get_arg(0); + unsigned tmp_max; + count_trailing(curr, min, tmp_max, depth - 1); + max = num == 1 ? tmp_max : m_util.get_bv_size(a); + return; + } + + void count_trailing_core(expr * e, unsigned& min, unsigned& max, unsigned depth) { + if (!depth) { + min = 0; + max = m_util.get_bv_size(e); + return; + } + unsigned sz; + numeral e_val; + if (m_util.is_numeral(e, e_val, sz)) { + min = max = 0; + numeral two(2); + while (sz-- && e_val.is_even()) { + ++max; + ++min; + div(e_val, two, e_val); + } + return; + } + if (m_util.is_bv_mul(e)) count_trailing_mul(to_app(e), min, max, depth); + else if (m_util.is_bv_add(e)) count_trailing_add(to_app(e), min, max, depth); + else if (m_util.is_concat(e)) count_trailing_concat(to_app(e), min, max, depth); + else { + min = 0; + max = m_util.get_bv_size(e); + } + } + + void cache(unsigned depth, expr * e, unsigned min, unsigned max) { + SASSERT(depth <= TRAILING_DEPTH); + if (depth == 0) return; + if (m_count_cache[depth] == NULL) + m_count_cache[depth] = alloc(map); + m.inc_ref(e); + m_count_cache[depth]->insert(e, std::make_pair(min, max)); + TRACE("bv-trailing", tout << "caching@" << depth <<": " << mk_ismt2_pp(e, m) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";); + } + + bool is_cached(unsigned depth, expr * e, unsigned& min, unsigned& max) { + SASSERT(depth <= TRAILING_DEPTH); + if (depth == 0) { + min = 0; + max = m_util.get_bv_size(e); + return true; + } + if (m_count_cache[depth] == NULL) + return false; + const map::obj_map_entry * const oe = m_count_cache[depth]->find_core(e); + if (oe == NULL) return false; + min = oe->get_data().m_value.first; + max = oe->get_data().m_value.second; + TRACE("bv-trailing", tout << "cached@" << depth << ": " << mk_ismt2_pp(e, m) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";); + return true; + } + + void reset_cache(unsigned condition) { + SASSERT(m_count_cache[0] == NULL); + for (unsigned i = 1; i <= TRAILING_DEPTH; ++i) { + if (m_count_cache[i] == NULL) continue; + if (m_count_cache[i]->size() < condition) continue; + map::iterator it = m_count_cache[i]->begin(); + map::iterator end = m_count_cache[i]->end(); + for (; it != end; ++it) m.dec_ref(it->m_key); + dealloc(m_count_cache[i]); + m_count_cache[i] = NULL; + } + } + +}; + +bv_trailing::bv_trailing(mk_extract_proc& mk_extract) { + m_imp = alloc(imp, mk_extract); +} + +bv_trailing::~bv_trailing() { + dealloc(m_imp); +} + +br_status bv_trailing::eq_remove_trailing(expr * e1, expr * e2, expr_ref& result) { + return m_imp->eq_remove_trailing(e1, e2, result); +} + +void bv_trailing::count_trailing(expr * e, unsigned& min, unsigned& max) { + m_imp->count_trailing(e, min, max, TRAILING_DEPTH); +} + +unsigned bv_trailing::remove_trailing(expr * e, unsigned n, expr_ref& result) { + return m_imp->remove_trailing(e, n, result, TRAILING_DEPTH); +} + +void bv_trailing::reset_cache(unsigned condition) { + m_imp->reset_cache(condition); +} diff --git a/src/ast/rewriter/bv_trailing.h b/src/ast/rewriter/bv_trailing.h new file mode 100644 index 000000000..862a1bea6 --- /dev/null +++ b/src/ast/rewriter/bv_trailing.h @@ -0,0 +1,46 @@ + /*++ + Copyright (c) 2016 Microsoft Corporation + + Module Name: + + bv_trailing.h + + Abstract: + + A utility to count trailing zeros of an expression. Treats 2x and x++0 equivalently. + + + Author: + + Mikolas Janota (MikolasJanota) + + Revision History: + --*/ +#ifndef BV_TRAILING_H_ +#define BV_TRAILING_H_ +#include"ast.h" +#include"rewriter_types.h" +#include"mk_extract_proc.h" +class bv_trailing { + public: + bv_trailing(mk_extract_proc& ep); + virtual ~bv_trailing(); + public: + // Remove trailing zeros from both sides of an equality (might give False). + br_status eq_remove_trailing(expr * e1, expr * e2, expr_ref& result); + + // Gives a lower and upper bound on trailing zeros in e. + void count_trailing(expr * e, unsigned& min, unsigned& max); + + // Attempts removing n trailing zeros from e. Returns how many were successfully removed. + // We're assuming that it can remove at least as many zeros as min returned by count_training. + // Removing the bit-width of e, sets result to NULL. + unsigned remove_trailing(expr * e, unsigned n, expr_ref& result); + + // Reset cache(s) if it exceeded size condition. + void reset_cache(unsigned condition); + protected: + struct imp; + imp * m_imp; +}; +#endif /* BV_TRAILING_H_ */ diff --git a/src/ast/rewriter/mk_extract_proc.cpp b/src/ast/rewriter/mk_extract_proc.cpp new file mode 100644 index 000000000..5f470acd3 --- /dev/null +++ b/src/ast/rewriter/mk_extract_proc.cpp @@ -0,0 +1,49 @@ +/*++ + Copyright (c) 2016 Microsoft Corporation + + Module Name: + + mk_extract_proc.cpp + + Abstract: + + + Author: + + Mikolas Janota (MikolasJanota) + + Revision History: +--*/ +#include"mk_extract_proc.h" +mk_extract_proc::mk_extract_proc(bv_util & u): + m_util(u), + m_high(0), + m_low(UINT_MAX), + m_domain(0), + m_f_cached(0) { +} + +mk_extract_proc::~mk_extract_proc() { + if (m_f_cached) { + // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain + ast_manager & m = m_util.get_manager(); + m.dec_ref(m_f_cached); + } +} + +app * mk_extract_proc::operator()(unsigned high, unsigned low, expr * arg) { + ast_manager & m = m_util.get_manager(); + sort * s = m.get_sort(arg); + if (m_low == low && m_high == high && m_domain == s) + return m.mk_app(m_f_cached, arg); + // m_f_cached has a reference to m_domain, so, I don't need to inc_ref m_domain + if (m_f_cached) + m.dec_ref(m_f_cached); + app * r = to_app(m_util.mk_extract(high, low, arg)); + m_high = high; + m_low = low; + m_domain = s; + m_f_cached = r->get_decl(); + m.inc_ref(m_f_cached); + return r; +} diff --git a/src/ast/rewriter/mk_extract_proc.h b/src/ast/rewriter/mk_extract_proc.h new file mode 100644 index 000000000..2b242d0f5 --- /dev/null +++ b/src/ast/rewriter/mk_extract_proc.h @@ -0,0 +1,34 @@ + /*++ + Copyright (c) 2016 Microsoft Corporation + + Module Name: + + mk_extract_proc.h + + Abstract: + + + Author: + + Mikolas Janota (MikolasJanota) + + Revision History: + --*/ +#ifndef MK_EXTRACT_PROC_H_ +#define MK_EXTRACT_PROC_H_ +#include"ast.h" +#include"bv_decl_plugin.h" +class mk_extract_proc { + bv_util & m_util; + unsigned m_high; + unsigned m_low; + sort * m_domain; + func_decl * m_f_cached; +public: + mk_extract_proc(bv_util & u); + ~mk_extract_proc(); + app * operator()(unsigned high, unsigned low, expr * arg); + ast_manager & m() { return m_util.get_manager(); } + bv_util & bvutil() { return m_util; } +}; +#endif /* MK_EXTRACT_PROC_H_ */ diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index 63bdbd519..962c9660e 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -825,15 +825,17 @@ br_status poly_rewriter::cancel_monomials(expr * lhs, expr * rhs, bool m if (c_at_rhs) { c.neg(); normalize(c); - new_rhs_monomials[0] = mk_numeral(c); - lhs_result = mk_add_app(new_lhs_monomials.size() - 1, new_lhs_monomials.c_ptr() + 1); - rhs_result = mk_add_app(new_rhs_monomials.size(), new_rhs_monomials.c_ptr()); - } - else { - new_lhs_monomials[0] = mk_numeral(c); - lhs_result = mk_add_app(new_lhs_monomials.size(), new_lhs_monomials.c_ptr()); - rhs_result = mk_add_app(new_rhs_monomials.size() - 1, new_rhs_monomials.c_ptr() + 1); } + // When recreating the lhs and rhs also insert coefficient on the appropriate side. + // Ignore coefficient if it's 0 and there are no other summands. + const bool insert_c_lhs = !c_at_rhs && (new_lhs_monomials.size() == 1 || !c.is_zero()); + const bool insert_c_rhs = c_at_rhs && (new_rhs_monomials.size() == 1 || !c.is_zero()); + const unsigned lhs_offset = insert_c_lhs ? 0 : 1; + const unsigned rhs_offset = insert_c_rhs ? 0 : 1; + new_rhs_monomials[0] = insert_c_rhs ? mk_numeral(c) : NULL; + new_lhs_monomials[0] = insert_c_lhs ? mk_numeral(c) : NULL; + lhs_result = mk_add_app(new_lhs_monomials.size() - lhs_offset, new_lhs_monomials.c_ptr() + lhs_offset); + rhs_result = mk_add_app(new_rhs_monomials.size() - rhs_offset, new_rhs_monomials.c_ptr() + rhs_offset); return BR_DONE; } diff --git a/src/model/model.cpp b/src/model/model.cpp index f4f9af873..951c7f744 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -25,7 +25,7 @@ Revision History: #include"used_symbols.h" #include"model_evaluator.h" -model::model(ast_manager & m): +model::model(ast_manager & m): model_core(m) { } @@ -56,7 +56,7 @@ void model::copy_func_interps(model const & source) { register_decl(it2->m_key, it2->m_value->copy()); } } - + void model::copy_usort_interps(model const & source) { sort2universe::iterator it3 = source.m_usort2universe.begin(); sort2universe::iterator end3 = source.m_usort2universe.end(); @@ -67,7 +67,7 @@ void model::copy_usort_interps(model const & source) { model * model::copy() const { model * m = alloc(model, m_manager); - + m->copy_const_interps(*this); m->copy_func_interps(*this); m->copy_usort_interps(*this); @@ -121,16 +121,15 @@ bool model::has_uninterpreted_sort(sort * s) const { return u != 0; } -unsigned model::get_num_uninterpreted_sorts() const { - return m_usorts.size(); +unsigned model::get_num_uninterpreted_sorts() const { + return m_usorts.size(); } -sort * model::get_uninterpreted_sort(unsigned idx) const { - return m_usorts[idx]; +sort * model::get_uninterpreted_sort(unsigned idx) const { + return m_usorts[idx]; } void model::register_usort(sort * s, unsigned usize, expr * const * universe) { - SASSERT(m_manager.is_uninterp(s)); sort2universe::obj_map_entry * entry = m_usort2universe.insert_if_not_there2(s, 0); m_manager.inc_array_ref(usize, universe); if (entry->get_data().m_value == 0) { @@ -151,7 +150,7 @@ void model::register_usort(sort * s, unsigned usize, expr * const * universe) { } model * model::translate(ast_translation & translator) const { - model * res = alloc(model, translator.to()); + model * res = alloc(model, translator.to()); // Translate const interps decl2expr::iterator it1 = m_interp.begin(); @@ -167,7 +166,7 @@ model * model::translate(ast_translation & translator) const { func_interp * fi = it2->m_value; res->register_decl(translator(it2->m_key), fi->translate(translator)); } - + // Translate usort interps sort2universe::iterator it3 = m_usort2universe.begin(); sort2universe::iterator end3 = m_usort2universe.end(); @@ -175,8 +174,8 @@ model * model::translate(ast_translation & translator) const { ptr_vector new_universe; for (unsigned i=0; im_value->size(); i++) new_universe.push_back(translator(it3->m_value->get(i))); - res->register_usort(translator(it3->m_key), - new_universe.size(), + res->register_usort(translator(it3->m_key), + new_universe.size(), new_universe.c_ptr()); } diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 3a3a8a93a..3c10f8704 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -31,7 +31,7 @@ model_core::~model_core() { for (; it2 != end2; ++it2) { m_manager.dec_ref(it2->m_key); dealloc(it2->m_value); - } + } } bool model_core::eval(func_decl* f, expr_ref & r) const { diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index f4a890a2c..3111f2b6c 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -30,6 +30,7 @@ Revision History: #include"fpa_rewriter.h" #include"rewriter_def.h" #include"cooperate.h" +#include"ast_pp.h" struct evaluator_cfg : public default_rewriter_cfg { @@ -42,6 +43,7 @@ struct evaluator_cfg : public default_rewriter_cfg { pb_rewriter m_pb_rw; fpa_rewriter m_f_rw; seq_rewriter m_seq_rw; + array_util m_ar; unsigned long long m_max_memory; unsigned m_max_steps; bool m_model_completion; @@ -59,7 +61,8 @@ struct evaluator_cfg : public default_rewriter_cfg { m_dt_rw(m), m_pb_rw(m), m_f_rw(m), - m_seq_rw(m) { + m_seq_rw(m), + m_ar(m) { bool flat = true; m_b_rw.set_flat(flat); m_a_rw.set_flat(flat); @@ -116,6 +119,7 @@ struct evaluator_cfg : public default_rewriter_cfg { if (val != 0) { result = val; return BR_DONE; +// return m().is_value(val)?BR_DONE:BR_REWRITE_FULL; } if (m_model_completion) { @@ -146,6 +150,8 @@ struct evaluator_cfg : public default_rewriter_cfg { st = m_f_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_seq_rw.get_fid()) st = m_seq_rw.mk_eq_core(args[0], args[1], result); + else if (fid == m_ar_rw.get_fid()) + st = mk_array_eq(args[0], args[1], result); if (st != BR_FAILED) return st; } @@ -182,6 +188,7 @@ struct evaluator_cfg : public default_rewriter_cfg { return st; } + bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) { #define TRACE_MACRO TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";); @@ -230,6 +237,85 @@ struct evaluator_cfg : public default_rewriter_cfg { bool cache_results() const { return m_cache; } + + br_status mk_array_eq(expr* a, expr* b, expr_ref& result) { + if (a == b) { + result = m().mk_true(); + return BR_DONE; + } + vector stores; + expr_ref else1(m()), else2(m()); + if (extract_array_func_interp(a, stores, else1) && + extract_array_func_interp(b, stores, else2)) { + expr_ref_vector conj(m()), args1(m()), args2(m()); + conj.push_back(m().mk_eq(else1, else2)); + args1.push_back(a); + args2.push_back(b); + for (unsigned i = 0; i < stores.size(); ++i) { + args1.resize(1); args1.append(stores[i].size() - 1, stores[i].c_ptr()); + args2.resize(1); args2.append(stores[i].size() - 1, stores[i].c_ptr()); + expr* s1 = m_ar.mk_select(args1.size(), args1.c_ptr()); + expr* s2 = m_ar.mk_select(args2.size(), args2.c_ptr()); + conj.push_back(m().mk_eq(s1, s2)); + } + result = m().mk_and(conj.size(), conj.c_ptr()); + return BR_REWRITE_FULL; + } + return BR_FAILED; + } + + bool extract_array_func_interp(expr* a, vector& stores, expr_ref& else_case) { + SASSERT(m_ar.is_array(a)); + + while (m_ar.is_store(a)) { + expr_ref_vector store(m()); + store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1); + stores.push_back(store); + a = to_app(a)->get_arg(0); + } + + if (m_ar.is_const(a)) { + else_case = to_app(a)->get_arg(0); + return true; + } + + if (m_ar.is_as_array(a)) { + func_decl* f = m_ar.get_as_array_func_decl(to_app(a)); + func_interp* g = m_model.get_func_interp(f); + unsigned sz = g->num_entries(); + unsigned arity = f->get_arity(); + for (unsigned i = 0; i < sz; ++i) { + expr_ref_vector store(m()); + func_entry const* fe = g->get_entry(i); + store.append(arity, fe->get_args()); + store.push_back(fe->get_result()); + for (unsigned j = 0; j < store.size(); ++j) { + if (!is_ground(store[j].get())) { + TRACE("model_evaluator", tout << "could not extract array interpretation: " << mk_pp(a, m()) << "\n" << mk_pp(store[j].get(), m()) << "\n";); + return false; + } + } + stores.push_back(store); + } + else_case = g->get_else(); + if (!else_case) { + TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m()) << "\n";); + return false; + } + if (!is_ground(else_case)) { + TRACE("model_evaluator", tout << "non-ground else case " << mk_pp(a, m()) << "\n" << mk_pp(else_case, m()) << "\n";); + return false; + } + TRACE("model_evaluator", tout << "else case: " << mk_pp(else_case, m()) << "\n";); + return true; + } + TRACE("model_evaluator", tout << "no translation: " << mk_pp(a, m()) << "\n";); + + return false; + } + + + }; template class rewriter_tpl; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index db62febbd..b200524e7 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -401,7 +401,7 @@ namespace sat { literal_vector::iterator l_it = m_bs_ls.begin(); for (; it != end; ++it, ++l_it) { clause & c2 = *(*it); - if (*l_it == null_literal) { + if (!c2.was_removed() && *l_it == null_literal) { // c2 was subsumed if (c1.is_learned() && !c2.is_learned()) c1.unset_learned(); diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index 036a09bb6..a7875e99e 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -34,7 +34,7 @@ proto_model::proto_model(ast_manager & m, params_ref const & p): register_factory(alloc(basic_factory, m)); m_user_sort_factory = alloc(user_sort_factory, m); register_factory(m_user_sort_factory); - + m_model_partial = model_params(p).partial(); } @@ -85,8 +85,8 @@ expr * proto_model::mk_some_interp_for(func_decl * d) { bool proto_model::is_select_of_model_value(expr* e) const { - return - is_app_of(e, m_afid, OP_SELECT) && + return + is_app_of(e, m_afid, OP_SELECT) && is_as_array(to_app(e)->get_arg(0)) && has_interpretation(array_util(m_manager).get_as_array_func_decl(to_app(to_app(e)->get_arg(0)))); } @@ -115,7 +115,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { It returns \c true if succeeded, and false otherwise. If the evaluation fails, then r contains a term that is simplified as much as possible using the interpretations available in the model. - + When model_completion == true, if the model does not assign an interpretation to a declaration it will build one for it. Moreover, partial functions will also be completed. So, if model_completion == true, the evaluator never fails if it doesn't contain quantifiers. @@ -194,7 +194,7 @@ void proto_model::cleanup_func_interp(func_interp * fi, func_decl_set & found_au if (!cache.find(fi_else, a)) { UNREACHABLE(); } - + fi->set_else(a); } @@ -225,12 +225,12 @@ void proto_model::cleanup() { func_interp * fi = (*it).m_value; cleanup_func_interp(fi, found_aux_fs); } - + // remove auxiliary declarations that are not used. if (found_aux_fs.size() != m_aux_decls.size()) { remove_aux_decls_not_in_set(m_decls, found_aux_fs); remove_aux_decls_not_in_set(m_func_decls, found_aux_fs); - + func_decl_set::iterator it2 = m_aux_decls.begin(); func_decl_set::iterator end2 = m_aux_decls.end(); for (; it2 != end2; ++it2) { @@ -262,7 +262,6 @@ void proto_model::freeze_universe(sort * s) { \brief Return the known universe of an uninterpreted sort. */ obj_hashtable const & proto_model::get_known_universe(sort * s) const { - SASSERT(m_manager.is_uninterp(s)); return m_user_sort_factory->get_known_universe(s); } @@ -277,13 +276,13 @@ ptr_vector const & proto_model::get_universe(sort * s) const { return tmp; } -unsigned proto_model::get_num_uninterpreted_sorts() const { - return m_user_sort_factory->get_num_sorts(); +unsigned proto_model::get_num_uninterpreted_sorts() const { + return m_user_sort_factory->get_num_sorts(); } -sort * proto_model::get_uninterpreted_sort(unsigned idx) const { - SASSERT(idx < get_num_uninterpreted_sorts()); - return m_user_sort_factory->get_sort(idx); +sort * proto_model::get_uninterpreted_sort(unsigned idx) const { + SASSERT(idx < get_num_uninterpreted_sorts()); + return m_user_sort_factory->get_sort(idx); } /** @@ -301,7 +300,7 @@ expr * proto_model::get_some_value(sort * s) { else { family_id fid = s->get_family_id(); value_factory * f = get_factory(fid); - if (f) + if (f) return f->get_some_value(s); // there is no factory for the family id, then assume s is uninterpreted. return m_user_sort_factory->get_some_value(s); @@ -315,7 +314,7 @@ bool proto_model::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) { else { family_id fid = s->get_family_id(); value_factory * f = get_factory(fid); - if (f) + if (f) return f->get_some_values(s, v1, v2); else return false; @@ -327,9 +326,9 @@ expr * proto_model::get_fresh_value(sort * s) { return m_user_sort_factory->get_fresh_value(s); } else { - family_id fid = s->get_family_id(); + family_id fid = s->get_family_id(); value_factory * f = get_factory(fid); - if (f) + if (f) return f->get_fresh_value(s); else // Use user_sort_factory if the theory has no support for model construnction. @@ -374,7 +373,7 @@ void proto_model::complete_partial_func(func_decl * f) { func_interp * fi = get_func_interp(f); if (fi && fi->is_partial()) { expr * else_value = 0; -#if 0 +#if 0 // For UFBV benchmarks, setting the "else" to false is not a good idea. // TODO: find a permanent solution. A possibility is to add another option. if (m_manager.is_bool(f->get_range())) { @@ -395,7 +394,7 @@ void proto_model::complete_partial_func(func_decl * f) { } /** - \brief Set the (else) field of function interpretations... + \brief Set the (else) field of function interpretations... */ void proto_model::complete_partial_funcs() { if (m_model_partial) @@ -424,7 +423,7 @@ model * proto_model::mk_model() { m->register_decl(it2->m_key, it2->m_value); m_manager.dec_ref(it2->m_key); } - + m_finterp.reset(); // m took the ownership of the func_interp's unsigned sz = get_num_uninterpreted_sorts(); @@ -450,7 +449,7 @@ model * proto_model::mk_model() { // It uses the simplifier s during the computation. bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & result) { bool actuals_are_values = true; - + if (fi.num_entries() != 0) { for (unsigned i = 0; actuals_are_values && i < fi.get_arity(); i++) { actuals_are_values = fi.m().is_value(args[i]); @@ -462,16 +461,16 @@ bool eval(func_interp & fi, simplifier & s, expr * const * args, expr_ref & resu result = entry->get_result(); return true; } - - TRACE("func_interp", tout << "failed to find entry for: "; - for(unsigned i = 0; i < fi.get_arity(); i++) - tout << mk_pp(args[i], fi.m()) << " "; + + TRACE("func_interp", tout << "failed to find entry for: "; + for(unsigned i = 0; i < fi.get_arity(); i++) + tout << mk_pp(args[i], fi.m()) << " "; tout << "\nis partial: " << fi.is_partial() << "\n";); - + if (!fi.eval_else(args, result)) { return false; } - + if (actuals_are_values && fi.args_are_values()) { // cheap case... we are done return true; @@ -506,14 +505,14 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { SASSERT(is_well_sorted(m_manager, e)); TRACE("model_eval", tout << mk_pp(e, m_manager) << "\n"; tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n";); - + obj_map eval_cache; expr_ref_vector trail(m_manager); sbuffer, 128> todo; ptr_buffer args; expr * null = static_cast(0); todo.push_back(std::make_pair(e, null)); - + simplifier m_simplifier(m_manager); expr * a; @@ -528,7 +527,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { SASSERT(r != 0); todo.pop_back(); eval_cache.insert(a, r); - TRACE("model_eval", + TRACE("model_eval", tout << "orig:\n" << mk_pp(a, m_manager) << "\n"; tout << "after beta reduction:\n" << mk_pp(expanded_a, m_manager) << "\n"; tout << "new:\n" << mk_pp(r, m_manager) << "\n";); @@ -556,7 +555,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { SASSERT(args.size() == t->get_num_args()); expr_ref new_t(m_manager); func_decl * f = t->get_decl(); - + if (!has_interpretation(f)) { // the model does not assign an interpretation to f. SASSERT(new_t.get() == 0); @@ -606,7 +605,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { if (!::eval(*fi, m_simplifier, args.c_ptr(), r1)) { SASSERT(fi->is_partial()); // fi->eval only fails when fi is partial. if (model_completion) { - expr * r = get_some_value(f->get_range()); + expr * r = get_some_value(f->get_range()); fi->set_else(r); SASSERT(!fi->is_partial()); new_t = r; @@ -635,7 +634,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { } } } - TRACE("model_eval", + TRACE("model_eval", tout << "orig:\n" << mk_pp(t, m_manager) << "\n"; tout << "new:\n" << mk_pp(new_t, m_manager) << "\n";); todo.pop_back(); @@ -643,12 +642,12 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { eval_cache.insert(t, new_t); break; } - case AST_VAR: + case AST_VAR: SASSERT(a != 0); eval_cache.insert(a, a); todo.pop_back(); break; - case AST_QUANTIFIER: + case AST_QUANTIFIER: TRACE("model_eval", tout << "found quantifier\n" << mk_pp(a, m_manager) << "\n";); is_ok = false; // evaluator does not handle quantifiers. SASSERT(a != 0); @@ -669,12 +668,12 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { result = a; std::cout << mk_pp(e, m_manager) << "\n===>\n" << result << "\n"; - TRACE("model_eval", + TRACE("model_eval", ast_ll_pp(tout << "original: ", m_manager, e); ast_ll_pp(tout << "evaluated: ", m_manager, a); ast_ll_pp(tout << "reduced: ", m_manager, result.get()); tout << "sort: " << mk_pp(m_manager.get_sort(e), m_manager) << "\n"; - ); + ); SASSERT(is_well_sorted(m_manager, result.get())); return is_ok; } diff --git a/src/smt/smt_farkas_util.cpp b/src/smt/smt_farkas_util.cpp index c1a303299..c5ff42e3e 100644 --- a/src/smt/smt_farkas_util.cpp +++ b/src/smt/smt_farkas_util.cpp @@ -62,7 +62,7 @@ namespace smt { app* farkas_util::mk_ge(expr* e1, expr* e2) { mk_coerce(e1, e2); - return a.mk_gt(e1, e2); + return a.mk_ge(e1, e2); } app* farkas_util::mk_gt(expr* e1, expr* e2) { diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 6ebbbbf0d..8a83b93bd 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -3212,7 +3212,8 @@ namespace smt { template bool theory_arith::get_value(enode * n, expr_ref & r) { theory_var v = n->get_th_var(get_id()); - return v != null_theory_var && to_expr(get_value(v), is_int(v), r); + inf_numeral val; + return v != null_theory_var && (val = get_value(v), (!is_int(v) || val.is_int())) && to_expr(val, is_int(v), r); } template diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index adff16c35..7703f70aa 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -15,7 +15,6 @@ Author: Revision History: - // Use instead reference counts for dependencies to GC? --*/ @@ -258,7 +257,7 @@ final_check_status theory_seq::final_check_eh() { TRACE("seq", tout << ">>fixed_length\n";); return FC_CONTINUE; } - if (branch_variable()) { + if (reduce_length_eq() || branch_unit_variable() || branch_binary_variable() || branch_variable_mb() || branch_variable()) { ++m_stats.m_branch_variable; TRACE("seq", tout << ">>branch_variable\n";); return FC_CONTINUE; @@ -291,8 +290,7 @@ final_check_status theory_seq::final_check_eh() { return FC_GIVEUP; } - -bool theory_seq::branch_variable() { +bool theory_seq::reduce_length_eq() { context& ctx = get_context(); unsigned sz = m_eqs.size(); int start = ctx.get_random_value(); @@ -304,25 +302,344 @@ bool theory_seq::branch_variable() { return true; } } + return false; +} + +bool theory_seq::branch_binary_variable() { + unsigned sz = m_eqs.size(); + for (unsigned i = 0; i < sz; ++i) { + eq const& e = m_eqs[i]; + if (branch_binary_variable(e)) { + return true; + } + } + return false; +} + +bool theory_seq::branch_binary_variable(eq const& e) { + if (is_complex(e)) { + return false; + } + ptr_vector xs, ys; + expr* x, *y; + bool is_binary = is_binary_eq(e.ls(), e.rs(), x, xs, ys, y); + if (!is_binary) { + is_binary = is_binary_eq(e.rs(), e.ls(), x, xs, ys, y); + } + if (!is_binary) { + return false; + } + if (x == y) { + return false; + } + + // Equation is of the form x ++ xs = ys ++ y + // where xs, ys are units. + // x is either a prefix of ys, all of ys ++ y or ys ++ y1, such that y = y1 ++ y2, y2 = xs + + rational lenX, lenY; + context& ctx = get_context(); + if (branch_variable(e)) { + return true; + } + if (!get_length(x, lenX)) { + enforce_length(ensure_enode(x)); + return true; + } + if (!get_length(y, lenY)) { + enforce_length(ensure_enode(y)); + return true; + } + if (lenX + rational(xs.size()) != lenY + rational(ys.size())) { + // |x| - |y| = |ys| - |xs| + expr_ref a(mk_sub(m_util.str.mk_length(x), m_util.str.mk_length(y)), m); + expr_ref b(m_autil.mk_int(ys.size()-xs.size()), m); + propagate_lit(e.dep(), 0, 0, mk_eq(a, b, false)); + return true; + } + if (lenX <= rational(ys.size())) { + expr_ref_vector Ys(m); + Ys.append(ys.size(), ys.c_ptr()); + branch_unit_variable(e.dep(), x, Ys); + return true; + } + expr_ref le(m_autil.mk_le(m_util.str.mk_length(x), m_autil.mk_int(ys.size())), m); + literal lit = mk_literal(le); + if (l_false == ctx.get_assignment(lit)) { + // |x| > |ys| => x = ys ++ y1, y = y1 ++ y2, y2 = xs + expr_ref Y1(mk_skolem(symbol("seq.left"), x, y), m); + expr_ref Y2(mk_skolem(symbol("seq.right"), x, y), m); + ys.push_back(Y1); + expr_ref ysY1(m_util.str.mk_concat(ys.size(), ys.c_ptr()), m); + expr_ref xsE(m_util.str.mk_concat(xs.size(), xs.c_ptr()), m); + expr_ref Y1Y2(m_util.str.mk_concat(Y1, Y2), m); + literal_vector lits; + lits.push_back(~lit); + dependency* dep = e.dep(); + propagate_eq(dep, lits, x, ysY1, true); + propagate_eq(dep, lits, y, Y1Y2, true); + propagate_eq(dep, lits, Y2, xsE, true); + } + else { + ctx.mark_as_relevant(lit); + } + return true; +} + +bool theory_seq::branch_unit_variable() { + unsigned sz = m_eqs.size(); + for (unsigned i = 0; i < sz; ++i) { + eq const& e = m_eqs[i]; + if (is_unit_eq(e.ls(), e.rs())) { + branch_unit_variable(e.dep(), e.ls()[0], e.rs()); + return true; + } + else if (is_unit_eq(e.rs(), e.ls())) { + branch_unit_variable(e.dep(), e.rs()[0], e.ls()); + return true; + } + } + return false; +} + +/** + \brief ls := X... == rs := abcdef +*/ +bool theory_seq::is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs) { + if (ls.empty() || !is_var(ls[0])) { + return false; + } + for (unsigned i = 0; i < rs.size(); ++i) { + if (!m_util.str.is_unit(rs[i])) { + return false; + } + } + return true; +} + +void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units) { + SASSERT(is_var(X)); + context& ctx = get_context(); + rational lenX; + if (!get_length(X, lenX)) { + enforce_length(ensure_enode(X)); + return; + } + if (lenX > rational(units.size())) { + expr_ref le(m_autil.mk_le(m_util.str.mk_length(X), m_autil.mk_int(units.size())), m); + propagate_lit(dep, 0, 0, mk_literal(le)); + return; + } + SASSERT(lenX.is_unsigned()); + unsigned lX = lenX.get_unsigned(); + if (lX == 0) { + set_empty(X); + } + else { + literal lit = mk_eq(m_autil.mk_int(lX), m_util.str.mk_length(X), false); + if (l_true == ctx.get_assignment(lit)) { + expr_ref R(m_util.str.mk_concat(lX, units.c_ptr()), m); + literal_vector lits; + lits.push_back(lit); + propagate_eq(dep, lits, X, R, true); + } + else { + ctx.mark_as_relevant(lit); + ctx.force_phase(lit); + } + } +} + +bool theory_seq::branch_variable_mb() { + context& ctx = get_context(); + bool change = false; + for (unsigned i = 0; i < m_eqs.size(); ++i) { + eq const& e = m_eqs[i]; + vector len1, len2; + if (!is_complex(e)) { + continue; + } + if (e.ls().empty() || e.rs().empty() || + (!is_var(e.ls()[0]) && !is_var(e.rs()[0]))) { + continue; + } + + if (!enforce_length(e.ls(), len1) || !enforce_length(e.rs(), len2)) { + change = true; + continue; + } + rational l1, l2; + for (unsigned j = 0; j < len1.size(); ++j) l1 += len1[j]; + for (unsigned j = 0; j < len2.size(); ++j) l2 += len2[j]; + if (l1 != l2) { + TRACE("seq", tout << "lengths are not compatible\n";); + expr_ref l = mk_concat(e.ls().size(), e.ls().c_ptr()); + expr_ref r = mk_concat(e.rs().size(), e.rs().c_ptr()); + expr_ref lnl(m_util.str.mk_length(l), m), lnr(m_util.str.mk_length(r), m); + literal_vector lits; + propagate_eq(e.dep(), lits, lnl, lnr, false); + change = true; + continue; + } + if (split_lengths(e.dep(), e.ls(), e.rs(), len1, len2)) { + TRACE("seq", tout << "split lengths\n";); + return true; + } + } + return change; +} - unsigned s = 0; +bool theory_seq::is_complex(eq const& e) { + unsigned num_vars1 = 0, num_vars2 = 0; + for (unsigned i = 0; i < e.ls().size(); ++i) { + if (is_var(e.ls()[i])) ++num_vars1; + } + for (unsigned i = 0; i < e.rs().size(); ++i) { + if (is_var(e.rs()[i])) ++num_vars2; + } + return num_vars1 > 0 && num_vars2 > 0 && num_vars1 + num_vars2 > 2; +} + +/* + \brief Decompose ls = rs into Xa = bYc, such that + 1. + - X != Y + - |b| <= |X| <= |bY| in currrent model + - b is non-empty. + 2. X != Y + - b is empty + - |X| <= |Y| + 3. |X| = 0 + - propagate X = empty +*/ +bool theory_seq::split_lengths(dependency* dep, + expr_ref_vector const& ls, expr_ref_vector const& rs, + vector const& ll, vector const& rl) { + context& ctx = get_context(); + expr_ref X(m), Y(m), b(m); + if (ls.empty() || rs.empty()) { + return false; + } + if (is_var(ls[0]) && ll[0].is_zero()) { + return set_empty(ls[0]); + } + if (is_var(rs[0]) && rl[0].is_zero()) { + return set_empty(rs[0]); + } + if (is_var(rs[0]) && !is_var(ls[0])) { + return split_lengths(dep, rs, ls, rl, ll); + } + if (!is_var(ls[0])) { + return false; + } + X = ls[0]; + rational lenX = ll[0]; + expr_ref_vector bs(m); + SASSERT(lenX.is_pos()); + rational lenB(0), lenY(0); + for (unsigned i = 0; lenX > lenB && i < rs.size(); ++i) { + bs.push_back(rs[i]); + lenY = rl[i]; + lenB += lenY; + } + SASSERT(lenX <= lenB); + SASSERT(!bs.empty()); + Y = bs.back(); + bs.pop_back(); + if (!is_var(Y) && !m_util.str.is_unit(Y)) { + TRACE("seq", tout << "TBD: non variable or unit split: " << Y << "\n";); + return false; + } + if (X == Y) { + TRACE("seq", tout << "Cycle: " << X << "\n";); + return false; + } + if (lenY.is_zero()) { + return set_empty(Y); + } + b = mk_concat(bs, m.get_sort(X)); + + SASSERT(X != Y); + + + // |b| < |X| <= |b| + |Y| => x = bY1, Y = Y1Y2 + expr_ref lenXE(m_util.str.mk_length(X), m); + expr_ref lenYE(m_util.str.mk_length(Y), m); + expr_ref lenb(m_util.str.mk_length(b), m); + expr_ref le1(m_autil.mk_le(mk_sub(lenXE, lenb), m_autil.mk_int(0)), m); + expr_ref le2(m_autil.mk_le(mk_sub(mk_sub(lenXE, lenb), lenYE), + m_autil.mk_int(0)), m); + literal lit1(~mk_literal(le1)); + literal lit2(mk_literal(le2)); + literal_vector lits; + lits.push_back(lit1); + lits.push_back(lit2); + + if (ctx.get_assignment(lit1) != l_true || + ctx.get_assignment(lit2) != l_true) { + ctx.mark_as_relevant(lit1); + ctx.mark_as_relevant(lit2); + } + else if (m_util.str.is_unit(Y)) { + SASSERT(lenB == lenX); + bs.push_back(Y); + expr_ref bY(m_util.str.mk_concat(bs), m); + propagate_eq(dep, lits, X, bY, true); + } + else { + SASSERT(is_var(Y)); + expr_ref Y1(mk_skolem(symbol("seq.left"), X, b, Y), m); + expr_ref Y2(mk_skolem(symbol("seq.right"), X, b, Y), m); + expr_ref bY1(m_util.str.mk_concat(b, Y1), m); + expr_ref Y1Y2(m_util.str.mk_concat(Y1, Y2), m); + propagate_eq(dep, lits, X, bY1, true); + propagate_eq(dep, lits, Y, Y1Y2, true); + } + return true; +} + +bool theory_seq::set_empty(expr* x) { + add_axiom(~mk_eq(m_autil.mk_int(0), m_util.str.mk_length(x), false), mk_eq_empty(x)); + return true; +} + +bool theory_seq::enforce_length(expr_ref_vector const& es, vector & len) { + bool all_have_length = true; + rational val; + zstring s; + for (unsigned i = 0; i < es.size(); ++i) { + expr* e = es[i]; + if (m_util.str.is_unit(e)) { + len.push_back(rational(1)); + } + else if (m_util.str.is_empty(e)) { + len.push_back(rational(0)); + } + else if (m_util.str.is_string(e, s)) { + len.push_back(rational(s.length())); + } + else if (get_length(e, val)) { + len.push_back(val); + } + else { + enforce_length(ensure_enode(e)); + all_have_length = false; + } + } + return all_have_length; +} + +bool theory_seq::branch_variable() { + context& ctx = get_context(); + unsigned sz = m_eqs.size(); + int start = ctx.get_random_value(); + for (unsigned i = 0; i < sz; ++i) { unsigned k = (i + start) % sz; eq const& e = m_eqs[k]; - unsigned id = e.id(); - s = find_branch_start(2*id); - TRACE("seq", tout << s << " " << id << ": " << e.ls() << " = " << e.rs() << "\n";); - bool found = find_branch_candidate(s, e.dep(), e.ls(), e.rs()); - insert_branch_start(2*id, s); - if (found) { - return true; - } - s = find_branch_start(2*id + 1); - found = find_branch_candidate(s, e.dep(), e.rs(), e.ls()); - insert_branch_start(2*id + 1, s); - if (found) { + if (branch_variable(e)) { return true; } @@ -338,6 +655,22 @@ bool theory_seq::branch_variable() { return ctx.inconsistent(); } +bool theory_seq::branch_variable(eq const& e) { + unsigned id = e.id(); + unsigned s = find_branch_start(2*id); + TRACE("seq", tout << s << " " << id << ": " << e.ls() << " = " << e.rs() << "\n";); + bool found = find_branch_candidate(s, e.dep(), e.ls(), e.rs()); + insert_branch_start(2*id, s); + if (found) { + return true; + } + s = find_branch_start(2*id + 1); + found = find_branch_candidate(s, e.dep(), e.rs(), e.ls()); + insert_branch_start(2*id + 1, s); + + return found; +} + void theory_seq::insert_branch_start(unsigned k, unsigned s) { m_branch_start.insert(k, s); m_trail_stack.push(pop_branch(k)); @@ -483,7 +816,6 @@ lbool theory_seq::assume_equality(expr* l, expr* r) { return l_false; } return ctx.get_assignment(mk_eq(l, r, false)); - //return l_undef; } @@ -1901,12 +2233,15 @@ void theory_seq::display(std::ostream & out) const { void theory_seq::display_equations(std::ostream& out) const { for (unsigned i = 0; i < m_eqs.size(); ++i) { - eq const& e = m_eqs[i]; - out << e.ls() << " = " << e.rs() << " <- \n"; - display_deps(out, e.dep()); + display_equation(out, m_eqs[i]); } } +void theory_seq::display_equation(std::ostream& out, eq const& e) const { + out << e.ls() << " = " << e.rs() << " <- \n"; + display_deps(out, e.dep()); +} + void theory_seq::display_disequations(std::ostream& out) const { bool first = true; for (unsigned i = 0; i < m_nqs.size(); ++i) { @@ -3050,6 +3385,9 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { else if (m_util.str.is_in_re(e)) { propagate_in_re(e, is_true); } + else if (is_skolem(symbol("seq.split"), e)) { + // propagate equalities + } else { UNREACHABLE(); } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 8206eeca4..fc37a8f06 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -358,6 +358,10 @@ namespace smt { void init_model(expr_ref_vector const& es); // final check bool simplify_and_solve_eqs(); // solve unitary equalities + bool reduce_length_eq(); + bool branch_unit_variable(); // branch on XYZ = abcdef + bool branch_binary_variable(); // branch on abcX = Ydefg + bool branch_variable_mb(); // branch on a variable, model based on length bool branch_variable(); // branch on a variable bool split_variable(); // split a variable bool is_solved(); @@ -366,7 +370,16 @@ namespace smt { bool check_length_coherence(expr* e); bool fixed_length(); bool fixed_length(expr* e); + void branch_unit_variable(dependency* dep, expr* X, expr_ref_vector const& units); + bool branch_variable(eq const& e); + bool branch_binary_variable(eq const& e); + bool is_unit_eq(expr_ref_vector const& ls, expr_ref_vector const& rs); bool propagate_length_coherence(expr* e); + bool split_lengths(dependency* dep, + expr_ref_vector const& ls, expr_ref_vector const& rs, + vector const& ll, vector const& rl); + bool set_empty(expr* x); + bool is_complex(eq const& e); bool check_extensionality(); bool check_contains(); @@ -465,6 +478,7 @@ namespace smt { bool has_length(expr *e) const { return m_length.contains(e); } void add_length(expr* e); void enforce_length(enode* n); + bool enforce_length(expr_ref_vector const& es, vector& len); void enforce_length_coherence(enode* n1, enode* n2); void add_elim_string_axiom(expr* n); @@ -532,6 +546,7 @@ namespace smt { // diagnostics void display_equations(std::ostream& out) const; + void display_equation(std::ostream& out, eq const& e) const; void display_disequations(std::ostream& out) const; void display_disequation(std::ostream& out, ne const& e) const; void display_deps(std::ostream& out, dependency* deps) const; diff --git a/src/tactic/extension_model_converter.cpp b/src/tactic/extension_model_converter.cpp index 89c1bb4f5..ebd530a58 100644 --- a/src/tactic/extension_model_converter.cpp +++ b/src/tactic/extension_model_converter.cpp @@ -43,6 +43,41 @@ static void display_decls_info(std::ostream & out, model_ref & md) { } } +bool extension_model_converter::is_fi_entry_expr(expr * e, unsigned arity, ptr_vector & args) { + args.reset(); + if (!is_app(e) || !m().is_ite(to_app(e))) + return false; + + app * a = to_app(e); + expr * c = a->get_arg(0); + expr * t = a->get_arg(1); + expr * f = a->get_arg(2); + + if ((arity == 0) || + (arity == 1 && (!m().is_eq(c) || to_app(c)->get_num_args() != 2)) || + (arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != arity))) + return false; + + args.resize(arity, 0); + for (unsigned i = 0; i < arity; i++) { + expr * ci = (arity == 1 && i == 0) ? to_app(c) : to_app(c)->get_arg(i); + + if (!m().is_eq(ci) || to_app(ci)->get_num_args() != 2) + return false; + + expr * a0 = to_app(ci)->get_arg(0); + expr * a1 = to_app(ci)->get_arg(1); + if (is_var(a0) && to_var(a0)->get_idx() == i) + args[i] = a1; + else if (is_var(a1) && to_var(a1)->get_idx() == i) + args[i] = a0; + else + return false; + } + + return true; +} + void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) { SASSERT(goal_idx == 0); TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md);); @@ -62,7 +97,14 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) { } else { func_interp * new_fi = alloc(func_interp, m(), arity); - new_fi->set_else(val); + expr * e = val.get(); + ptr_vector args; + while (is_fi_entry_expr(e, arity, args)) { + TRACE("extension_mc", tout << "fi entry: " << mk_ismt2_pp(e, m()) << std::endl;); + new_fi->insert_entry(args.c_ptr(), to_app(e)->get_arg(1)); + e = to_app(e)->get_arg(2); + } + new_fi->set_else(e); md->register_decl(f, new_fi); } } @@ -86,10 +128,10 @@ void extension_model_converter::display(std::ostream & out) { } model_converter * extension_model_converter::translate(ast_translation & translator) { - extension_model_converter * res = alloc(extension_model_converter, translator.to()); + extension_model_converter * res = alloc(extension_model_converter, translator.to()); for (unsigned i = 0; i < m_vars.size(); i++) res->m_vars.push_back(translator(m_vars[i].get())); for (unsigned i = 0; i < m_defs.size(); i++) - res->m_defs.push_back(translator(m_defs[i].get())); + res->m_defs.push_back(translator(m_defs[i].get())); return res; } diff --git a/src/tactic/extension_model_converter.h b/src/tactic/extension_model_converter.h index 7124c3bee..9431906f3 100644 --- a/src/tactic/extension_model_converter.h +++ b/src/tactic/extension_model_converter.h @@ -27,14 +27,14 @@ Notes: class extension_model_converter : public model_converter { func_decl_ref_vector m_vars; expr_ref_vector m_defs; -public: +public: extension_model_converter(ast_manager & m):m_vars(m), m_defs(m) { } - + virtual ~extension_model_converter(); - + ast_manager & m() const { return m_vars.get_manager(); } - + virtual void operator()(model_ref & md, unsigned goal_idx); virtual void display(std::ostream & out); @@ -43,6 +43,9 @@ public: void insert(func_decl * v, expr * def); virtual model_converter * translate(ast_translation & translator); + +private: + bool is_fi_entry_expr(expr * e, unsigned arity, ptr_vector & args); };