From 3ee5c0e7d9d6b5cca9567631533f0e9569c6218b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Mar 2019 11:33:44 -0800 Subject: [PATCH] fix #2164 address some of simplification shortcommings from #2151 #2152 #2153 Signed-off-by: Nikolaj Bjorner --- src/api/api_tactic.cpp | 4 +- src/api/c++/z3++.h | 2 +- src/ast/array_decl_plugin.cpp | 4 + src/ast/array_decl_plugin.h | 7 ++ src/ast/rewriter/array_rewriter.cpp | 161 +++++++++++++--------------- src/cmd_context/eval_cmd.cpp | 1 + src/parsers/smt2/smt2parser.cpp | 1 + src/smt/theory_lra.cpp | 5 +- src/util/lp/lar_solver.cpp | 39 ++++--- src/util/lp/lar_solver.h | 1 + src/util/mpz.cpp | 2 +- 11 files changed, 120 insertions(+), 107 deletions(-) diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index 7c0143201..491fb8354 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -52,7 +52,9 @@ extern "C" { RESET_ERROR_CODE(); tactic_cmd * t = mk_c(c)->find_tactic_cmd(symbol(name)); if (t == nullptr) { - SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); + std::stringstream err; + err << "unknown tactic " << name; + SET_ERROR_CODE(Z3_INVALID_ARG, err.str().c_str()); RETURN_Z3(nullptr); } tactic * new_t = t->mk(mk_c(c)->m()); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 6113fdbe9..cbb12ea99 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2387,7 +2387,7 @@ namespace z3 { return *this; } void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); } - // void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); } + void add(expr_vector const& v) { check_context(*this, v); for (unsigned i = 0; i < v.size(); ++i) add(v[i]); } unsigned size() const { return Z3_goal_size(ctx(), m_goal); } expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); } Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); } diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 211c67953..7975a4d61 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -576,6 +576,10 @@ func_decl * array_recognizers::get_as_array_func_decl(func_decl * f) const { return to_func_decl(f->get_parameter(0).get_ast()); } +bool array_recognizers::is_const(expr* e, expr*& v) const { + return is_const(e) && (v = to_app(e)->get_arg(0), true); +} + array_util::array_util(ast_manager& m): array_recognizers(m.mk_family_id("array")), m_manager(m) { diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index c735fb811..1ae0c9593 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -152,6 +152,8 @@ public: bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); } func_decl * get_as_array_func_decl(expr * n) const; func_decl * get_as_array_func_decl(func_decl* f) const; + + bool is_const(expr* e, expr*& v) const; }; class array_util : public array_recognizers { @@ -178,6 +180,11 @@ public: parameter param(s); return m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, ¶m, 1, &v); } + app * mk_const_array(unsigned n, sort * const* s, expr * v) { + vector ps; + for (unsigned i = 0; i < n; ++i) ps.push_back(parameter(s[i])); + return m_manager.mk_app(m_fid, OP_CONST_ARRAY, n, ps.c_ptr(), 1, &v); + } app * mk_empty_set(sort * s) { return mk_const_array(s, m_manager.mk_false()); } diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 56e094dab..8ff6dd654 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -230,105 +230,92 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, } br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - SASSERT(num_args >= 0); - bool is_store0 = m_util.is_store(args[0]); - bool is_const0 = m_util.is_const(args[0]); - if (num_args == 1) { - // - // map_f (store a j v) = (store (map_f a) j (f v)) - // - if (is_store0) { - app * store_expr = to_app(args[0]); - unsigned num_args = store_expr->get_num_args(); - SASSERT(num_args >= 3); - expr * a = store_expr->get_arg(0); - expr * v = store_expr->get_arg(num_args-1); - - ptr_buffer new_args; - - new_args.push_back(m_util.mk_map(f, 1, &a)); // (map_f a) - new_args.append(num_args - 2, store_expr->get_args() + 1); // j - new_args.push_back(m().mk_app(f, v)); // (f v) - - result = m().mk_app(get_fid(), OP_STORE, new_args.size(), new_args.c_ptr()); - return BR_REWRITE2; - } - - // - // map_f (const v) = (const (f v)) - // - if (is_const0) { - expr * fv = m().mk_app(f, to_app(args[0])->get_arg(0)); - result = m_util.mk_const_array(m().get_sort(args[0]), fv); - return BR_REWRITE2; - } - return BR_FAILED; - } - SASSERT(num_args > 1); - - if (is_store0) { - unsigned num_indices = to_app(args[0])->get_num_args() - 2; - unsigned i; - for (i = 1; i < num_args; i++) { - if (!m_util.is_store(args[i])) - break; - unsigned j; - for (j = 1; j < num_indices+1; j++) { - if (to_app(args[0])->get_arg(j) != to_app(args[i])->get_arg(j)) - break; - } - if (j < num_indices+1) - break; + app* store_expr = nullptr; + unsigned num_indices = 0; + bool same_store = true; + for (unsigned i = 0; same_store && i < num_args; i++) { + expr* a = args[i]; + if (m_util.is_const(a)) { + continue; } - // - // map_f (store a_1 j v_1) ... (store a_n j v_n) --> (store (map_f a_1 ... a_n) j (f v_1 ... v_n)) - // - if (i == num_args) { - ptr_buffer arrays; - ptr_buffer values; - for (unsigned i = 0; i < num_args; i++) { - arrays.push_back(to_app(args[i])->get_arg(0)); - values.push_back(to_app(args[i])->get_arg(num_indices+1)); + else if (!m_util.is_store(a)) { + same_store = false; + } + else if (!store_expr) { + num_indices = to_app(a)->get_num_args() - 2; + store_expr = to_app(a); + } + else { + for (unsigned j = 1; same_store && j < num_indices + 1; j++) { + same_store = (store_expr->get_arg(j) == to_app(a)->get_arg(j)); } - ptr_buffer new_args; - new_args.push_back(m_util.mk_map(f, arrays.size(), arrays.c_ptr())); + } + } + + // + // map_f (store a_1 j v_1) ... (store a_n j v_n) --> (store (map_f a_1 ... a_n) j (f v_1 ... v_n)) + // + if (same_store) { + ptr_buffer arrays; + ptr_buffer values; + for (unsigned i = 0; i < num_args; i++) { + expr* a = args[i]; + if (m_util.is_const(a)) { + arrays.push_back(a); + values.push_back(to_app(a)->get_arg(0)); + } + else { + arrays.push_back(to_app(a)->get_arg(0)); + values.push_back(to_app(a)->get_arg(num_indices+1)); + } + } + ptr_buffer new_args; + new_args.push_back(m_util.mk_map(f, arrays.size(), arrays.c_ptr())); + if (store_expr) { new_args.append(num_indices, to_app(args[0])->get_args() + 1); new_args.push_back(m().mk_app(f, values.size(), values.c_ptr())); result = m().mk_app(get_fid(), OP_STORE, new_args.size(), new_args.c_ptr()); - return BR_REWRITE2; } - return BR_FAILED; + else { + result = m_util.mk_const_array(m().get_sort(args[0]), new_args.back()); + } + return BR_REWRITE2; } - if (is_const0) { - unsigned i; - for (i = 1; i < num_args; i++) { - if (!m_util.is_const(args[i])) - break; + // + // map_f (lambda x1 b1) ... (lambda x1 bn) -> lambda x1 (f b1 .. bn) + // + quantifier* lam = nullptr; + for (unsigned i = 0; i < num_args; ++i) { + if (is_lambda(args[i])) { + lam = to_quantifier(args[i]); } - if (i == num_args) { - // - // map_f (const v_1) ... (const v_n) = (const (f v_1 ... v_n)) - // - ptr_buffer values; - for (unsigned i = 0; i < num_args; i++) { - values.push_back(to_app(args[i])->get_arg(0)); + } + if (lam) { + expr_ref_vector args1(m()); + for (unsigned i = 0; i < num_args; ++i) { + expr* a = args[i]; + if (m_util.is_const(a)) { + args1.push_back(to_app(a)->get_arg(0)); + } + else if (is_lambda(a)) { + lam = to_quantifier(a); + args1.push_back(lam->get_expr()); + } + else { + expr_ref_vector sel(m()); + sel.push_back(a); + unsigned n = lam->get_num_decls(); + for (unsigned i = 0; i < n; ++i) { + sel.push_back(m().mk_var(n - i - 1, lam->get_decl_sort(i))); + } + args1.push_back(m_util.mk_select(sel.size(), sel.c_ptr())); } - - expr * fv = m().mk_app(f, values.size(), values.c_ptr()); - sort * in_s = get_sort(args[0]); - ptr_vector domain; - unsigned domain_sz = get_array_arity(in_s); - for (unsigned i = 0; i < domain_sz; i++) - domain.push_back(get_array_domain(in_s, i)); - sort_ref out_s(m()); - out_s = m_util.mk_array_sort(domain_sz, domain.c_ptr(), f->get_range()); - parameter p(out_s.get()); - result = m().mk_app(get_fid(), OP_CONST_ARRAY, 1, &p, 1, &fv); - return BR_REWRITE2; } - return BR_FAILED; + result = m().mk_app(f, args1.size(), args1.c_ptr()); + result = m().update_quantifier(lam, result); + return BR_REWRITE3; } return BR_FAILED; diff --git a/src/cmd_context/eval_cmd.cpp b/src/cmd_context/eval_cmd.cpp index a599cfa4a..e6980583a 100644 --- a/src/cmd_context/eval_cmd.cpp +++ b/src/cmd_context/eval_cmd.cpp @@ -71,6 +71,7 @@ public: expr_ref r(ctx.m()); unsigned timeout = m_params.get_uint("timeout", UINT_MAX); unsigned rlimit = m_params.get_uint("rlimit", 0); + md->compress(); model_evaluator ev(*(md.get()), m_params); ev.set_solver(alloc(th_solver, ctx)); cancel_eh eh(ctx.m().limit()); diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index c103b0276..b3b8082fe 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -2677,6 +2677,7 @@ namespace smt2 { m_ctx.regular_stream() << "("; expr ** expr_it = expr_stack().c_ptr() + spos; expr ** expr_end = expr_it + m_cached_strings.size(); + md->compress(); for (unsigned i = 0; expr_it < expr_end; expr_it++, i++) { model::scoped_model_completion _scm(md, true); expr_ref v = (*md)(*expr_it); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 81edb2c67..605498e53 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3329,13 +3329,12 @@ public: st = lp::lp_status::UNBOUNDED; } else { - vi = m_theory_var2var_index[v]; - st = m_solver->maximize_term(vi, term_max); + st = m_solver->maximize_term(v, term_max); } - TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n");); switch (st) { case lp::lp_status::OPTIMAL: { init_variable_values(); + TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n");); inf_rational val = get_value(v); // inf_rational val(term_max.x, term_max.y); blocker = mk_gt(v); diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index db81ad403..2daedc045 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -85,6 +85,15 @@ std::ostream& lar_solver::print_implied_bound(const implied_bound& be, std::ostr out << "end of implied bound" << std::endl; return out; } + +std::ostream& lar_solver::print_values(std::ostream& out) const { + for (unsigned i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) { + const numeric_pair & rp = m_mpq_lar_core_solver.m_r_x[i]; + out << this->get_column_name(i) << " -> " << rp << "\n"; + } + return out; +} + bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be, const vector> & explanation) const { std::unordered_map coeff_map; @@ -463,29 +472,28 @@ void lar_solver::prepare_costs_for_r_solver(const lar_term & term) { bool lar_solver::maximize_term_on_corrected_r_solver(lar_term & term, impq &term_max) { settings().backup_costs = false; + bool ret = false; switch (settings().simplex_strategy()) { case simplex_strategy_enum::tableau_rows: prepare_costs_for_r_solver(term); settings().simplex_strategy() = simplex_strategy_enum::tableau_costs; - { - bool ret = maximize_term_on_tableau(term, term_max); - settings().simplex_strategy() = simplex_strategy_enum::tableau_rows; - set_costs_to_zero(term); - m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL); - return ret; - } + ret = maximize_term_on_tableau(term, term_max); + settings().simplex_strategy() = simplex_strategy_enum::tableau_rows; + set_costs_to_zero(term); + m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL); + return ret; + case simplex_strategy_enum::tableau_costs: prepare_costs_for_r_solver(term); - { - bool ret = maximize_term_on_tableau(term, term_max); - set_costs_to_zero(term); - m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL); - return ret; - } - + ret = maximize_term_on_tableau(term, term_max); + set_costs_to_zero(term); + m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL); + return ret; + case simplex_strategy_enum::lu: lp_assert(false); // not implemented return false; + default: lp_unreachable(); // wrong mode } @@ -511,6 +519,7 @@ lar_term lar_solver::get_term_to_maximize(unsigned ext_j) const { lp_status lar_solver::maximize_term(unsigned ext_j, impq &term_max) { + TRACE("lar_solver", print_values(tout);); bool was_feasible = m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis(); impq prev_value; lar_term term = get_term_to_maximize(ext_j); @@ -559,6 +568,7 @@ lp_status lar_solver::maximize_term(unsigned ext_j, term_max = prev_value; m_mpq_lar_core_solver.m_r_x = backup; } + TRACE("lar_solver", print_values(tout);); return term_max == opt_val? lp_status::OPTIMAL :lp_status::FEASIBLE; } @@ -1185,6 +1195,7 @@ void lar_solver::get_model(std::unordered_map & variable_values) break; } + TRACE("get_model", tout << get_column_name(i) << " := " << x << "\n";); variable_values[i] = x; } } while (i != m_mpq_lar_core_solver.m_r_x.size()); diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 7af9cfacb..1dce8524e 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -457,6 +457,7 @@ public: std::ostream& print_implied_bound(const implied_bound& be, std::ostream & out) const; + std::ostream& print_values(std::ostream& out) const; mpq get_left_side_val(const lar_base_constraint & cns, const std::unordered_map & var_map) const; diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 6776acf65..178d5042d 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -1784,7 +1784,7 @@ void display_binary_data(std::ostream &out, unsigned val, unsigned numBits) { template void mpz_manager::display_bin(std::ostream & out, mpz const & a, unsigned num_bits) const { if (is_small(a)) { - display_binary_data(out, get_uint64(a), num_bits); + display_binary_data(out, static_cast(get_uint64(a)), num_bits); } else { #ifndef _MP_GMP digit_t *ds = digits(a);