From 21a31fcd2610f1e3b3163ea432d71e5c4f320193 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Apr 2020 02:07:16 -0700 Subject: [PATCH] add missing fixed propagations on negated integer inequalities Signed-off-by: Nikolaj Bjorner --- src/math/lp/lar_solver.h | 37 +++++++-------- src/math/lp/lp_types.h | 5 ++ src/math/lp/nla_core.cpp | 24 +++++----- src/qe/qe_arith_plugin.cpp | 30 ++++-------- src/smt/smt_case_split_queue.cpp | 4 -- src/smt/theory_arith_aux.h | 2 +- src/smt/theory_lra.cpp | 79 +++++++++++++++++--------------- src/smt/theory_str_mc.cpp | 1 + src/solver/parallel_tactic.cpp | 4 +- 9 files changed, 92 insertions(+), 94 deletions(-) diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 399ea3ca8..53427955f 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -46,9 +46,6 @@ Revision History: namespace lp { -typedef unsigned lpvar; -const lpvar null_lpvar = UINT_MAX; -const constraint_index null_ci = UINT_MAX; class lar_solver : public column_namer { struct term_hasher { @@ -123,9 +120,7 @@ public: static_matrix & A_d(); static_matrix const & A_d() const; - static bool valid_index(unsigned j){ return static_cast(j) >= 0;} - - bool column_is_int(column_index const& j) const { return column_is_int((unsigned)j); } + static bool valid_index(unsigned j) { return static_cast(j) >= 0;} bool column_is_int(unsigned j) const; bool column_value_is_int(unsigned j) const { return m_mpq_lar_core_solver.m_r_x[j].is_int(); } @@ -136,7 +131,8 @@ public: } unsigned external_to_column_index(unsigned) const; - + + // NSB code review: function seems misnamed. 'j' can be a term index. Columns are not term indices. const mpq& get_column_value_rational(unsigned j) const { if (tv::is_term(j)) { j = m_var_register.external_to_local(j); @@ -147,8 +143,6 @@ public: bool column_is_fixed(unsigned j) const; bool column_is_free(unsigned j) const; - bool well_formed(lar_term const& t) const; - const lar_term & get_term(unsigned j) const; public: @@ -203,6 +197,14 @@ public: bool compare_values(impq const& lhs, lconstraint_kind k, const mpq & rhs); + // columns + + bool column_is_int(column_index const& j) const { return column_is_int((unsigned)j); } + column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); } + bool is_fixed(column_index const& j) const { return column_is_fixed(j); } + const impq& get_value(column_index const& j) const { return get_column_value(j); } + + void update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); void update_column_type_and_bound_with_ub(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); void update_column_type_and_bound_with_no_ub(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); @@ -280,14 +282,13 @@ public: var_index external_to_local(unsigned j) const { var_index local_j; - if ( - m_var_register.external_is_used(j, local_j) || - m_term_register.external_is_used(j, local_j)) - { - return local_j; - } - else + if (m_var_register.external_is_used(j, local_j) || + m_term_register.external_is_used(j, local_j)) { + return local_j; + } + else { return -1; + } } bool column_has_upper_bound(unsigned j) const { @@ -298,11 +299,11 @@ public: return m_mpq_lar_core_solver.m_r_solver.column_has_lower_bound(j); } - const impq& get_upper_bound(unsigned j) const { + const impq& get_upper_bound(column_index j) const { return m_mpq_lar_core_solver.m_r_solver.m_upper_bounds[j]; } - const impq& get_lower_bound(unsigned j) const { + const impq& get_lower_bound(column_index j) const { return m_mpq_lar_core_solver.m_r_solver.m_lower_bounds[j]; } diff --git a/src/math/lp/lp_types.h b/src/math/lp/lp_types.h index 05193a9b4..41aeaa9cf 100644 --- a/src/math/lp/lp_types.h +++ b/src/math/lp/lp_types.h @@ -27,10 +27,14 @@ namespace nla { } namespace lp { + typedef unsigned var_index; typedef unsigned constraint_index; typedef unsigned row_index; enum lconstraint_kind { LE = -2, LT = -1 , GE = 2, GT = 1, EQ = 0, NE = 3 }; +typedef unsigned lpvar; +const lpvar null_lpvar = UINT_MAX; +const constraint_index null_ci = UINT_MAX; // index that comes from term or variable. @@ -79,6 +83,7 @@ class column_index { public: column_index(unsigned j): m_index(j) {} unsigned index() const { return m_index; } + bool is_null() const { return m_index == null_lpvar; } }; } diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index c36e7ac12..1b655a264 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1371,19 +1371,19 @@ void core::update_to_refine_of_var(lpvar j) { } bool core::patch_blocker(lpvar u, const monic& m) const { - SASSERT(m_to_refine.contains(m.var())); - if (var_is_used_in_a_correct_monic(u)) { - TRACE("nla_solver", tout << "u = " << u << " blocked as used in a correct monomial\n";); - return true; - } - - bool ret = u == m.var() || m.contains_var(u); - - TRACE("nla_solver", tout << "u = " << u << ", m = "; print_monic(m, tout) << - "ret = " << ret << "\n";); - - return ret; + SASSERT(m_to_refine.contains(m.var())); + if (var_is_used_in_a_correct_monic(u)) { + TRACE("nla_solver", tout << "u = " << u << " blocked as used in a correct monomial\n";); + return true; } + + bool ret = u == m.var() || m.contains_var(u); + + TRACE("nla_solver", tout << "u = " << u << ", m = "; print_monic(m, tout) << + "ret = " << ret << "\n";); + + return ret; +} bool core::try_to_patch(lpvar k, const rational& v, const monic & m) { return m_lar_solver.try_to_patch(k, v, diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp index cea44043b..6b7eb2897 100644 --- a/src/qe/qe_arith_plugin.cpp +++ b/src/qe/qe_arith_plugin.cpp @@ -750,9 +750,7 @@ namespace qe { expr_ref tmp1(m), tmp2(m); expr *a0, *a1; eqs.reset(); - conj_enum::iterator it = conjs.begin(), end = conjs.end(); - for (; it != end; ++it) { - expr* e = *it; + for (expr* e : conjs) { bool is_leq = false; if (m.is_eq(e, a0, a1) && is_arith(a0)) { @@ -1548,10 +1546,8 @@ public: {} ~arith_plugin() override { - bounds_cache::iterator it = m_bounds_cache.begin(), end = m_bounds_cache.end(); - for (; it != end; ++it) { - dealloc(it->get_value()); - } + for (auto & kv : m_bounds_cache) + dealloc(kv.get_value()); } void assign(contains_app& contains_x, expr* fml, rational const& vl) override { @@ -2397,9 +2393,7 @@ public: bool update_bounds(bounds_proc& bounds, contains_app& contains_x, expr* fml, atom_set const& tbl, bool is_pos) { app_ref tmp(m); - atom_set::iterator it = tbl.begin(), end = tbl.end(); - for (; it != end; ++it) { - app* e = *it; + for (app* e : tbl) { if (!contains_x(e)) { continue; } @@ -2468,14 +2462,10 @@ public: } ~nlarith_plugin() override { - bcs_t::iterator it = m_cache.begin(), end = m_cache.end(); - for (; it != end; ++it) { - dealloc(it->get_value()); - } - weights_t::iterator it2 = m_weights.begin(), e2 = m_weights.end(); - for (; it2 != e2; ++it2) { - dealloc(it2->get_value()); - } + for (auto & kv : m_cache) + dealloc(kv.get_value()); + for (auto& kv : m_weights) + dealloc(kv.get_value()); } bool simplify(expr_ref& fml) override { @@ -2605,9 +2595,7 @@ public: } void update_bounds(expr_ref_vector& lits, atom_set const& tbl, bool is_pos) { - atom_set::iterator it = tbl.begin(), end = tbl.end(); - for (; it != end; ++it) { - app* e = *it; + for (app* e : tbl) { lits.push_back(is_pos?e:m.mk_not(e)); } } diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp index 2ce274b51..ddb66ec33 100644 --- a/src/smt/smt_case_split_queue.cpp +++ b/src/smt/smt_case_split_queue.cpp @@ -974,9 +974,6 @@ namespace { } void assign_lit_eh(literal l) override { - // if (m_current_generation > stop_gen) - // m_current_generation--; - expr * e = m_context.bool_var2expr(l.var()); if (e == m_current_goal) return; @@ -1096,7 +1093,6 @@ namespace { void set_goal(expr * e) { - if (e == m_current_goal) return; GOAL_START(); diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index d5a80f85c..202d85c23 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -468,7 +468,7 @@ namespace smt { SASSERT(upper || new_bound->get_bound_kind() == B_LOWER); theory_var v = new_bound->get_var(); set_bound_core(v, new_bound, upper); - if ((propagate_eqs() || propagate_diseqs()) && is_fixed(v)) + if ((propagate_eqs() || propagate_diseqs()) && is_fixed(v)) fixed_var_eh(v); } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 6e3d5718f..ce54fd33d 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -84,7 +84,7 @@ public: } virtual ~bound() {} smt::theory_var get_var() const { return m_var; } - lpvar lp_solver_var() const { return m_vi; } + lp::tv tv() const { return lp::tv::raw(m_vi); } smt::bool_var get_bv() const { return m_bv; } bound_kind get_bound_kind() const { return m_bound_kind; } bool is_int() const { return m_is_int; } @@ -114,7 +114,6 @@ std::ostream& operator<<(std::ostream& out, bound const& b) { struct stats { unsigned m_assert_lower; unsigned m_assert_upper; - unsigned m_add_rows; unsigned m_bounds_propagations; unsigned m_num_iterations; unsigned m_num_iterations_with_no_progress; @@ -842,26 +841,21 @@ class theory_lra::imp { void add_eq_constraint(lp::constraint_index index, enode* n1, enode* n2) { m_constraint_sources.setx(index, equality_source, null_source); m_equalities.setx(index, enode_pair(n1, n2), enode_pair(0, 0)); - ++m_stats.m_add_rows; } void add_ineq_constraint(lp::constraint_index index, literal lit) { m_constraint_sources.setx(index, inequality_source, null_source); m_inequalities.setx(index, lit, null_literal); - ++m_stats.m_add_rows; - TRACE("arith", lp().constraints().display(tout, index) << " m_stats.m_add_rows = " << m_stats.m_add_rows << "\n";); } void add_def_constraint(lp::constraint_index index) { m_constraint_sources.setx(index, definition_source, null_source); m_definitions.setx(index, null_theory_var, null_theory_var); - ++m_stats.m_add_rows; } void add_def_constraint(lp::constraint_index index, theory_var v) { m_constraint_sources.setx(index, definition_source, null_source); m_definitions.setx(index, v, null_theory_var); - ++m_stats.m_add_rows; } @@ -1609,8 +1603,8 @@ public: if (!th.is_relevant_and_shared(n1)) { continue; } - lpvar vj = lp().external_to_column_index(v); - if (vj == lp::null_lpvar) + lp::column_index vj = lp().to_column_index(v); + if (vj.is_null()) continue; theory_var other = m_model_eqs.insert_if_not_there(v); if (other == v) { @@ -1619,14 +1613,14 @@ public: enode * n2 = get_enode(other); if (n1->get_root() == n2->get_root()) continue; - if (!lp().column_is_fixed(vj)) { - vars.push_back(vj); + if (!lp().is_fixed(vj)) { + vars.push_back(vj.index()); } else if (!m_tmp_var_set.contains(other) ) { - unsigned other_j = lp().external_to_column_index(other); - if (!lp().column_is_fixed(other_j)) { + lp::column_index other_j = lp().to_column_index(other); + if (!lp().is_fixed(other_j)) { m_tmp_var_set.insert(other); - vars.push_back(other_j); + vars.push_back(other_j.index()); } } } @@ -2447,6 +2441,7 @@ public: }); ++m_stats.m_bound_propagations1; assign(lit, m_core, m_eqs, m_params); + } } @@ -2999,6 +2994,8 @@ public: void assert_bound(bool_var bv, bool is_true, lp_api::bound& b) { lp::constraint_index ci = b.get_constraint(is_true); + lp::column_index j = lp().to_column_index(b.get_var()); + bool was_fixed = lp().is_fixed(j); m_solver->activate(ci); if (is_infeasible()) { return; @@ -3010,7 +3007,10 @@ public: else { ++m_stats.m_assert_upper; } - propagate_eqs(b.lp_solver_var(), ci, k, b); + inf_rational const& value = b.get_value(is_true); + if (value.is_rational()) { + propagate_eqs(b.tv(), ci, k, b, value.get_rational()); + } } lp_api::bound* mk_var_bound(bool_var bv, theory_var v, lp_api::bound_kind bk, rational const& bound) { @@ -3054,22 +3054,30 @@ public: typedef map > value2var; value2var m_fixed_var_table; - void propagate_eqs(lpvar vi, lp::constraint_index ci, lp::lconstraint_kind k, lp_api::bound& b) { - if (propagate_eqs()) { - rational const& value = b.get_value(); + void propagate_eqs(lp::tv t, lp::constraint_index ci, lp::lconstraint_kind k, lp_api::bound& b, rational const& value) { + bool best_bound = false; + if (k == lp::GE) { + best_bound = set_lower_bound(t, ci, value); + } + else if (k == lp::LE) { + best_bound = set_upper_bound(t, ci, value); + } + + if (propagate_eqs() && best_bound) { if (k == lp::GE) { - if (set_lower_bound(vi, ci, value) && has_upper_bound(vi, ci, value)) { + if (has_upper_bound(t.index(), ci, value)) { fixed_var_eh(b.get_var(), value); } } else if (k == lp::LE) { - if (set_upper_bound(vi, ci, value) && has_lower_bound(vi, ci, value)) { + if (has_lower_bound(t.index(), ci, value)) { fixed_var_eh(b.get_var(), value); } } } } + bool dump_lemmas() const { return m_arith_params.m_arith_dump_lemmas; } bool propagate_eqs() const { return m_arith_params.m_arith_propagate_eqs && m_num_conflicts < m_arith_params.m_arith_propagation_threshold; } @@ -3080,9 +3088,9 @@ public: bool proofs_enabled() const { return m.proofs_enabled(); } - bool set_upper_bound(lpvar vi, lp::constraint_index ci, rational const& v) { return set_bound(vi, ci, v, false); } + bool set_upper_bound(lp::tv t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, false); } - bool set_lower_bound(lpvar vi, lp::constraint_index ci, rational const& v) { return set_bound(vi, ci, v, true); } + bool set_lower_bound(lp::tv t, lp::constraint_index ci, rational const& v) { return set_bound(t, ci, v, true); } vector m_history; template @@ -3106,17 +3114,16 @@ public: }; - bool set_bound(lpvar vi, lp::constraint_index ci, rational const& v, bool is_lower) { - - if (lp::tv::is_term(vi)) { - lpvar ti = lp::tv::unmask_term(vi); + bool set_bound(lp::tv tv, lp::constraint_index ci, rational const& v, bool is_lower) { + if (tv.is_term()) { + lpvar ti = tv.id(); auto& vec = is_lower ? m_lower_terms : m_upper_terms; if (vec.size() <= ti) { vec.resize(ti + 1, constraint_bound(UINT_MAX, rational())); } constraint_bound& b = vec[ti]; if (b.first == UINT_MAX || (is_lower? b.second < v : b.second > v)) { - TRACE("arith", tout << "tighter bound " << lp().get_variable_name(vi) << "\n";); + TRACE("arith", tout << "tighter bound " << tv.to_string() << "\n";); m_history.push_back(vec[ti]); ctx().push_trail(history_trail(vec, ti, m_history)); b.first = ci; @@ -3125,17 +3132,16 @@ public: return true; } else { - TRACE("arith", tout << "not a term " << vi << "\n";); + TRACE("arith", tout << "not a term " << tv.to_string() << "\n";); // m_solver already tracks bounds on proper variables, but not on terms. bool is_strict = false; rational b; if (is_lower) { - return lp().has_lower_bound(vi, ci, b, is_strict) && !is_strict && b == v; + return lp().has_lower_bound(tv.id(), ci, b, is_strict) && !is_strict && b == v; } else { - return lp().has_upper_bound(vi, ci, b, is_strict) && !is_strict && b == v; - } - + return lp().has_upper_bound(tv.id(), ci, b, is_strict) && !is_strict && b == v; + } } } @@ -3188,11 +3194,13 @@ public: } } - - bool is_equal(theory_var x, theory_var y) const { return get_enode(x)->get_root() == get_enode(y)->get_root(); } - + bool is_equal(theory_var x, theory_var y) const { + return get_enode(x)->get_root() == get_enode(y)->get_root(); + } void fixed_var_eh(theory_var v1, rational const& bound) { + // IF_VERBOSE(0, verbose_stream() << "fix " << mk_bounded_pp(get_owner(v1), m) << " " << bound << "\n"); + theory_var v2; value_sort_pair key(bound, is_int(v1)); if (m_fixed_var_table.find(key, v2)) { @@ -3888,7 +3896,6 @@ public: m_arith_eq_adapter.collect_statistics(st); st.update("arith-lower", m_stats.m_assert_lower); st.update("arith-upper", m_stats.m_assert_upper); - st.update("arith-add-rows", m_stats.m_add_rows); st.update("arith-propagations", m_stats.m_bounds_propagations); st.update("arith-iterations", m_stats.m_num_iterations); st.update("arith-factorizations", lp().settings().stats().m_num_factorizations); diff --git a/src/smt/theory_str_mc.cpp b/src/smt/theory_str_mc.cpp index 3a51a2061..5f1c48c21 100644 --- a/src/smt/theory_str_mc.cpp +++ b/src/smt/theory_str_mc.cpp @@ -631,6 +631,7 @@ namespace smt { cex = expr_ref(m_autil.mk_ge(mk_strlen(term), mk_int(0)), m); return false; } + SASSERT(varLen_value.is_unsigned() && "actually arithmetic solver can assign it a very large number"); TRACE("str_fl", tout << "creating character terms for variable " << mk_pp(term, m) << ", length = " << varLen_value << std::endl;); ptr_vector new_chars; for (unsigned i = 0; i < varLen_value.get_unsigned(); ++i) { diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index 67e91d5f9..3520fc8cd 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -313,7 +313,7 @@ class parallel_tactic : public tactic { unsigned mult = static_cast(pow(exp, m_depth - 1)); p.set_uint("inprocess.max", pp.simplify_inprocess_max() * mult); p.set_uint("restart.max", pp.simplify_restart_max() * mult); - p.set_bool("lookahead_simplify", true); + p.set_bool("lookahead_simplify", m_depth > 2); p.set_bool("retain_blocked_clauses", retain_blocked); p.set_uint("max_conflicts", pp.simplify_max_conflicts()); if (m_depth > 1) p.set_uint("bce_delay", 0); @@ -475,8 +475,8 @@ private: simplify_again: ++num_simplifications; - s.inc_depth(1); // simplify + s.inc_depth(1); if (canceled(s)) return; switch (s.simplify()) { case l_undef: break;