diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index f7e98028d..175a6965b 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -172,7 +172,7 @@ void lar_solver::analyze_new_bounds_on_row_tableau( return; lp_assert(use_tableau()); bound_analyzer_on_row>::analyze_row(A_r().m_rows[row_index], - static_cast(-1), + null_ci, zero_of_type>(), row_index, bp @@ -246,7 +246,7 @@ bool lar_solver::term_is_used_as_row(unsigned term) const { void lar_solver::propagate_bounds_on_terms(lp_bound_propagator & bp) { for (unsigned i = 0; i < m_terms.size(); i++) { - if (term_is_used_as_row(i + m_terms_start_index)) + if (term_is_used_as_row(i)) continue; // this term is used a left side of a constraint, // it was processed as a touched row if needed propagate_bounds_on_a_term(*m_terms[i], bp, i); @@ -1118,7 +1118,7 @@ bool lar_solver::has_lower_bound(var_index var, constraint_index& ci, mpq& value } const ul_pair & ul = m_columns_to_ul_pairs[var]; ci = ul.lower_bound_witness(); - if (ci != static_cast(-1)) { + if (ci != null_ci) { auto& p = m_mpq_lar_core_solver.m_r_lower_bounds()[var]; value = p.x; is_strict = p.y.is_pos(); @@ -1137,7 +1137,7 @@ bool lar_solver::has_upper_bound(var_index var, constraint_index& ci, mpq& value } const ul_pair & ul = m_columns_to_ul_pairs[var]; ci = ul.upper_bound_witness(); - if (ci != static_cast(-1)) { + if (ci != null_ci) { auto& p = m_mpq_lar_core_solver.m_r_upper_bounds()[var]; value = p.x; is_strict = p.y.is_neg(); @@ -1363,7 +1363,7 @@ void lar_solver::pop() { } bool lar_solver::column_represents_row_in_tableau(unsigned j) { - return m_columns_to_ul_pairs()[j].m_i != static_cast(-1); + return m_columns_to_ul_pairs()[j].m_i != UINT_MAX; } void lar_solver::make_sure_that_the_bottom_right_elem_not_zero_in_tableau(unsigned i, unsigned j) { @@ -1580,7 +1580,7 @@ var_index lar_solver::add_var(unsigned ext_j, bool is_int) { return local_j; lp_assert(m_columns_to_ul_pairs.size() == A_r().column_count()); local_j = A_r().column_count(); - m_columns_to_ul_pairs.push_back(ul_pair(static_cast(-1))); + m_columns_to_ul_pairs.push_back(ul_pair(UINT_MAX)); add_non_basic_var_to_core_fields(ext_j, is_int); lp_assert(sizes_are_correct()); return local_j; @@ -2330,6 +2330,18 @@ bool lar_solver::fetch_normalized_term_column(const lar_term& c, std::pair lar_solver::add_equality(lpvar j, lpvar k) { + vector> coeffs; + coeffs.push_back(std::make_pair(mpq(1),j)); + coeffs.push_back(std::make_pair(mpq(-1),k)); + unsigned ext_term_index = m_terms.size(); + unsigned term_index = add_term(coeffs, ext_term_index); + return std::pair( + add_var_bound(term_index, lconstraint_kind::LE, mpq(0)), + add_var_bound(term_index, lconstraint_kind::GE, mpq(0))); +} + } // namespace lp diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index 707225384..6e59c6607 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -47,6 +47,7 @@ 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 { @@ -536,6 +537,8 @@ public: return m_mpq_lar_core_solver.column_is_bounded(j); } + std::pair add_equality(lpvar j, lpvar k); + void get_bound_constraint_witnesses_for_column(unsigned j, constraint_index & lc, constraint_index & uc) const { const ul_pair & ul = m_columns_to_ul_pairs[j]; lc = ul.lower_bound_witness(); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index c08323726..52131b9dc 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, relevant only if smt.arith.solver=2'), ('arith.nl.gb', BOOL, True, 'groebner Basis computation, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=2'), ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters, relevant only if smt.arith.solver=2'), @@ -75,7 +75,7 @@ def_module_params(module_name='smt', ('arith.simplex_strategy', UINT, 0, 'simplex strategy for the solver'), ('arith.enable_hnf', BOOL, True, 'enable hnf (Hermite Normal Form) cuts'), ('arith.bprop_on_pivoted_rows', BOOL, True, 'propagate bounds on rows changed by the pivot operation'), - ('arith.nla', BOOL, True, 'call nonlinear solver'), + ('arith.nla', BOOL, True, 'call nonlinear integer solver with incremental linearization'), ('arith.print_ext_var_names', BOOL, False, 'print external variable names'), ('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'), ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'),