From bc17b18ed085ed7e2d83ac8c1c7590987b3ea9d8 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 5 Jul 2018 12:01:12 -0700 Subject: [PATCH 1/6] setting smt.arith.solver=6 by default Signed-off-by: Lev Nachmanson --- src/smt/params/smt_params_helper.pyg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 3f4105c34..c39b74722 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -40,7 +40,7 @@ def_module_params(module_name='smt', ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'), ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), - ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), + ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'), ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false'), ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'), From adf0d745c10d5ea791e7e72199807e978bcb8e23 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 6 Jul 2018 10:53:04 -0700 Subject: [PATCH 2/6] rebase Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 3bdd2d784..76852d34a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1168,9 +1168,8 @@ public: if (m_variable_values.count(vi) > 0) return m_variable_values[vi]; - if(!m_solver->is_term(vi)) - return rational::zero(); - + if (!m_solver->is_term(vi)) + return rational::zero(); m_todo_terms.push_back(std::make_pair(vi, rational::one())); rational result(0); while (!m_todo_terms.empty()) { From 3c230727bb35100bbc01dea26c6a4eb152b1902d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 6 Jul 2018 11:13:38 -0700 Subject: [PATCH 3/6] rebase Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 76852d34a..3bdd2d784 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1168,8 +1168,9 @@ public: if (m_variable_values.count(vi) > 0) return m_variable_values[vi]; - if (!m_solver->is_term(vi)) - return rational::zero(); + if(!m_solver->is_term(vi)) + return rational::zero(); + m_todo_terms.push_back(std::make_pair(vi, rational::one())); rational result(0); while (!m_todo_terms.empty()) { From 5cfc3591d21c88529d1d0e7366cb09444f9c8f0d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Sat, 7 Jul 2018 16:18:42 -0700 Subject: [PATCH 4/6] create hnf cuts too, when gomory_cut_period is 2 Signed-off-by: Lev Nachmanson --- src/smt/params/smt_params_helper.pyg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index c39b74722..3f4105c34 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -40,7 +40,7 @@ def_module_params(module_name='smt', ('bv.reflect', BOOL, True, 'create enode for every bit-vector term'), ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), - ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), + ('arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation'), ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false'), ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'), From 2dfb8f53b62b2f72cfed0a536dbeabaa599d9e77 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 10 Jul 2018 14:25:22 -0700 Subject: [PATCH 5/6] do not add term to hnf if one of the vars has v.y value Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.cpp | 32 ++++++++++++++++++++++---------- src/util/lp/lar_solver.h | 1 + 2 files changed, 23 insertions(+), 10 deletions(-) diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 99a0c5883..135700936 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -2227,6 +2227,17 @@ void lar_solver::round_to_integer_solution() { update_delta_for_terms(del, j, vars_to_terms[j]); } } +// return true if all y coords are zeroes +bool lar_solver::sum_first_coords(const lar_term& t, mpq & val) const { + val = zero_of_type(); + for (const auto & c : t) { + const auto & x = m_mpq_lar_core_solver.m_r_x[c.var()]; + if (!is_zero(x.y)) + return false; + val += x.x * c.coeff(); + } + return true; +} bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term_index, mpq & rs, constraint_index& ci) const { unsigned tj = term_index + m_terms_start_index; @@ -2236,26 +2247,27 @@ bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term return false; // the term does not have a bound because it does not correspond to a column if (!is_int) // todo - allow for the next version of hnf return false; - impq term_val; - bool term_val_ready = false; + bool rs_is_calculated = false; mpq b; bool is_strict; + const lar_term& t = *terms()[term_index]; if (has_upper_bound(j, ci, b, is_strict) && !is_strict) { lp_assert(b.is_int()); - term_val = terms()[term_index]->apply(m_mpq_lar_core_solver.m_r_x); - term_val_ready = true; - if (term_val.x == b) { - rs = b; + if (!sum_first_coords(t, rs)) + return false; + rs_is_calculated = true; + if (rs == b) { return true; } } if (has_lower_bound(j, ci, b, is_strict) && !is_strict) { - if (!term_val_ready) - term_val = terms()[term_index]->apply(m_mpq_lar_core_solver.m_r_x); + if (!rs_is_calculated){ + if (!sum_first_coords(t, rs)) + return false; + } lp_assert(b.is_int()); - if (term_val.x == b) { - rs = b; + if (rs == b) { return true; } } diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index f17aa4a0d..9e15fc472 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -577,5 +577,6 @@ public: bool remove_from_basis(unsigned); lar_term get_term_to_maximize(unsigned ext_j) const; void set_cut_strategy(unsigned cut_frequency); + bool sum_first_coords(const lar_term& t, mpq & val) const; }; } From e0e893b791ce661e68d0a9943b2ac1614637a79f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 11 Jul 2018 12:29:09 -0700 Subject: [PATCH 6/6] fix in hnf for the lower bounds Signed-off-by: Lev Nachmanson --- src/util/lp/general_matrix.h | 4 ++-- src/util/lp/hnf_cutter.h | 15 ++++++++++++--- src/util/lp/int_solver.cpp | 5 +++-- src/util/lp/lar_solver.cpp | 4 +++- src/util/lp/lar_solver.h | 2 +- 5 files changed, 21 insertions(+), 9 deletions(-) diff --git a/src/util/lp/general_matrix.h b/src/util/lp/general_matrix.h index ce510eb6e..1c643161a 100644 --- a/src/util/lp/general_matrix.h +++ b/src/util/lp/general_matrix.h @@ -105,12 +105,12 @@ public: } template - void init_row_from_container(int i, const T & c, std::function column_fix) { + void init_row_from_container(int i, const T & c, std::function column_fix, const mpq& sign) { auto & row = m_data[adjust_row(i)]; lp_assert(row_is_initialized_correctly(row)); for (const auto & p : c) { unsigned j = adjust_column(column_fix(p.var())); - row[j] = p.coeff(); + row[j] = sign * p.coeff(); } } diff --git a/src/util/lp/hnf_cutter.h b/src/util/lp/hnf_cutter.h index dff0b8ef8..061b3a130 100644 --- a/src/util/lp/hnf_cutter.h +++ b/src/util/lp/hnf_cutter.h @@ -29,6 +29,7 @@ class hnf_cutter { var_register m_var_register; general_matrix m_A; vector m_terms; + vector m_terms_upper; svector m_constraints_for_explanation; vector m_right_sides; lp_settings & m_settings; @@ -54,15 +55,22 @@ public: // m_A will be filled from scratch in init_matrix_A m_var_register.clear(); m_terms.clear(); + m_terms_upper.clear(); m_constraints_for_explanation.clear(); m_right_sides.clear(); m_abs_max = zero_of_type(); m_overflow = false; } - void add_term(const lar_term* t, const mpq &rs, constraint_index ci) { + void add_term(const lar_term* t, const mpq &rs, constraint_index ci, bool upper_bound) { m_terms.push_back(t); - m_right_sides.push_back(rs); + m_terms_upper.push_back(upper_bound); + if (upper_bound) + m_right_sides.push_back(rs); + else + m_right_sides.push_back(-rs); + m_constraints_for_explanation.push_back(ci); + for (const auto &p : *t) { m_var_register.add_var(p.var()); mpq t = abs(ceil(p.coeff())); @@ -76,7 +84,8 @@ public: } void initialize_row(unsigned i) { - m_A.init_row_from_container(i, * m_terms[i], [this](unsigned j) { return m_var_register.add_var(j);}); + mpq sign = m_terms_upper[i]? one_of_type(): - one_of_type(); + m_A.init_row_from_container(i, * m_terms[i], [this](unsigned j) { return m_var_register.add_var(j);}, sign); } void init_matrix_A() { diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index f49ecabfd..e58abb4fd 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -537,8 +537,9 @@ void int_solver::try_add_term_to_A_for_hnf(unsigned i) { mpq rs; const lar_term* t = m_lar_solver->terms()[i]; constraint_index ci; - if (!hnf_cutter_is_full() && m_lar_solver->get_equality_and_right_side_for_term_on_current_x(i, rs, ci)) { - m_hnf_cutter.add_term(t, rs, ci); + bool upper_bound; + if (!hnf_cutter_is_full() && m_lar_solver->get_equality_and_right_side_for_term_on_current_x(i, rs, ci, upper_bound)) { + m_hnf_cutter.add_term(t, rs, ci, upper_bound); } } diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 135700936..f8d16ab8c 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -2239,7 +2239,7 @@ bool lar_solver::sum_first_coords(const lar_term& t, mpq & val) const { return true; } -bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term_index, mpq & rs, constraint_index& ci) const { +bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term_index, mpq & rs, constraint_index& ci, bool &upper_bound) const { unsigned tj = term_index + m_terms_start_index; unsigned j; bool is_int; @@ -2257,6 +2257,7 @@ bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term return false; rs_is_calculated = true; if (rs == b) { + upper_bound = true; return true; } } @@ -2268,6 +2269,7 @@ bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term lp_assert(b.is_int()); if (rs == b) { + upper_bound = false; return true; } } diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 9e15fc472..72705dfb3 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -573,7 +573,7 @@ public: unsigned column_count() const { return A_r().column_count(); } const vector & r_basis() const { return m_mpq_lar_core_solver.r_basis(); } const vector & r_nbasis() const { return m_mpq_lar_core_solver.r_nbasis(); } - bool get_equality_and_right_side_for_term_on_current_x(unsigned i, mpq &rs, constraint_index& ci) const; + bool get_equality_and_right_side_for_term_on_current_x(unsigned i, mpq &rs, constraint_index& ci, bool &upper_bound) const; bool remove_from_basis(unsigned); lar_term get_term_to_maximize(unsigned ext_j) const; void set_cut_strategy(unsigned cut_frequency);