From 4069e76ab0eceff02004a2ef45471f286e14face Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 May 2017 21:27:43 -0700 Subject: [PATCH 1/2] remove unused column function field, #1021 Signed-off-by: Nikolaj Bjorner --- src/util/lp/lar_solver.h | 34 ++++++++++++++++------------------ 1 file changed, 16 insertions(+), 18 deletions(-) diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index e2b1eb682..b74515566 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -34,25 +34,24 @@ namespace lean { class lar_solver : public column_namer { //////////////////// fields ////////////////////////// - lp_settings m_settings; - stacked_value m_status; - stacked_value m_simplex_strategy; + lp_settings m_settings; + stacked_value m_status; + stacked_value m_simplex_strategy; std::unordered_map m_ext_vars_to_columns; - vector m_columns_to_ext_vars_or_term_indices; - stacked_vector m_vars_to_ul_pairs; - vector m_constraints; - stacked_value m_constraint_count; + vector m_columns_to_ext_vars_or_term_indices; + stacked_vector m_vars_to_ul_pairs; + vector m_constraints; + stacked_value m_constraint_count; // the set of column indices j such that bounds have changed for j - int_set m_columns_with_changed_bound; - int_set m_rows_with_changed_bounds; - int_set m_basic_columns_with_changed_cost; - stacked_value m_infeasible_column_index; // such can be found at the initialization step - stacked_value m_term_count; - vector m_terms; - vector m_orig_terms; - const var_index m_terms_start_index; - indexed_vector m_column_buffer; - std::function m_column_type_function; + int_set m_columns_with_changed_bound; + int_set m_rows_with_changed_bounds; + int_set m_basic_columns_with_changed_cost; + stacked_value m_infeasible_column_index; // such can be found at the initialization step + stacked_value m_term_count; + vector m_terms; + vector m_orig_terms; + const var_index m_terms_start_index; + indexed_vector m_column_buffer; public: lar_core_solver m_mpq_lar_core_solver; unsigned constraint_count() const { @@ -83,7 +82,6 @@ public: lar_solver() : m_status(OPTIMAL), m_infeasible_column_index(-1), m_terms_start_index(1000000), - m_column_type_function ([this] (unsigned j) {return m_mpq_lar_core_solver.m_column_types()[j];}), m_mpq_lar_core_solver(m_settings, *this) {} From 79a8e9aab0e1c0b3f2d70037b21e2bca09cc816c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 May 2017 12:09:51 -0700 Subject: [PATCH 2/2] fix build break #1029 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 29 +---------------------------- src/smt/theory_seq.cpp | 2 ++ src/smt/theory_seq.h | 2 +- src/util/lp/mps_reader.h | 2 +- 4 files changed, 5 insertions(+), 30 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 01f4f924f..dc1931bac 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1423,37 +1423,10 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) { } /* - * (re.range c_1 c_n) = (re.union (str.to.re c1) (str.to.re c2) ... (str.to.re cn)) + * (re.range c_1 c_n) */ br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) { return BR_FAILED; - TRACE("seq", tout << "rewrite re.range [" << mk_pp(lo, m()) << " " << mk_pp(hi, m()) << "]\n";); - zstring str_lo, str_hi; - if (m_util.str.is_string(lo, str_lo) && m_util.str.is_string(hi, str_hi)) { - if (str_lo.length() == 1 && str_hi.length() == 1) { - unsigned int c1 = str_lo[0]; - unsigned int c2 = str_hi[0]; - if (c1 > c2) { - // exchange c1 and c2 - unsigned int tmp = c1; - c2 = c1; - c1 = tmp; - } - zstring s(c1); - expr_ref acc(m_util.re.mk_to_re(m_util.str.mk_string(s)), m()); - for (unsigned int ch = c1 + 1; ch <= c2; ++ch) { - zstring s_ch(ch); - expr_ref acc2(m_util.re.mk_to_re(m_util.str.mk_string(s_ch)), m()); - acc = m_util.re.mk_union(acc, acc2); - } - result = acc; - return BR_REWRITE2; - } else { - m().raise_exception("string constants in re.range must have length 1"); - } - } - - return BR_FAILED; } /* diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 7a9369fd3..3f8845546 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2176,6 +2176,8 @@ bool theory_seq::simplify_and_solve_eqs() { return m_new_propagation || ctx.inconsistent(); } +void theory_seq::internalize_eq_eh(app * atom, bool_var v) {} + bool theory_seq::internalize_term(app* term) { context & ctx = get_context(); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 2b8fb2fd7..e145d3077 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -343,7 +343,7 @@ namespace smt { virtual final_check_status final_check_eh(); virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); } virtual bool internalize_term(app*); - virtual void internalize_eq_eh(app * atom, bool_var v) {} + virtual void internalize_eq_eh(app * atom, bool_var v); virtual void new_eq_eh(theory_var, theory_var); virtual void new_diseq_eh(theory_var, theory_var); virtual void assign_eh(bool_var v, bool is_true); diff --git a/src/util/lp/mps_reader.h b/src/util/lp/mps_reader.h index 4c08ec8e6..af9ae6b4e 100644 --- a/src/util/lp/mps_reader.h +++ b/src/util/lp/mps_reader.h @@ -655,7 +655,7 @@ class mps_reader { sense interval G [rhs, rhs + |range|] L [rhs - |range|, rhs] - E [rhs, rhs + |range|] if range ¡Ý 0 [rhs - |range|, rhs] if range < 0 + E [rhs, rhs + |range|] if range in [rhs - |range|, rhs] if range < 0 where |range| is range's absolute value. */