diff --git a/contrib/cmake/src/test/lp/CMakeLists.txt b/contrib/cmake/src/test/lp/CMakeLists.txt new file mode 100644 index 000000000..6683a1758 --- /dev/null +++ b/contrib/cmake/src/test/lp/CMakeLists.txt @@ -0,0 +1,6 @@ +add_executable(lp_tst lp_main.cpp lp.cpp $ $ $ $ ) +target_compile_definitions(lp_tst PRIVATE ${Z3_COMPONENT_CXX_DEFINES}) +target_compile_options(lp_tst PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) +target_include_directories(lp_tst PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}) +target_link_libraries(lp_tst PRIVATE ${Z3_DEPENDENT_LIBS}) +z3_append_linker_flag_list_to_target(lp_tst ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index dd440b34d..a98f92ca3 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -35,10 +35,10 @@ endforeach() # raised if you try to declare a component is dependent on another component # that has not yet been declared. add_subdirectory(util) -add_subdirectory(util/lp) add_subdirectory(math/polynomial) add_subdirectory(sat) add_subdirectory(nlsat) +add_subdirectory(util/lp) add_subdirectory(math/hilbert) add_subdirectory(math/simplex) add_subdirectory(math/automata) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 5f2de5170..109657675 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1727,7 +1727,6 @@ ast * ast_manager::register_node_core(ast * n) { n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk(); - TRACE("ast", tout << "Object " << n->m_id << " was created.\n";); TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";); // increment reference counters diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 2b2087e3b..fa3d69602 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -738,9 +738,54 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu result = m_util.mk_idiv0(arg1); return BR_REWRITE1; } + expr_ref quot(m()); + if (divides(arg1, arg2, quot)) { + result = m_util.mk_mul(quot, m_util.mk_idiv(arg1, arg1)); + return BR_REWRITE2; + } return BR_FAILED; } +bool arith_rewriter::divides(expr* d, expr* n, expr_ref& quot) { + if (d == n) { + quot = m_util.mk_numeral(rational(1), m_util.is_int(d)); + return true; + } + if (m_util.is_mul(n)) { + expr_ref_vector muls(m()); + muls.push_back(n); + expr* n1, *n2; + rational r1, r2; + for (unsigned i = 0; i < muls.size(); ++i) { + if (m_util.is_mul(muls[i].get(), n1, n2)) { + muls[i] = n1; + muls.push_back(n2); + --i; + } + } + if (m_util.is_numeral(d, r1) && !r1.is_zero()) { + for (unsigned i = 0; i < muls.size(); ++i) { + if (m_util.is_numeral(muls[i].get(), r2) && (r2 / r1).is_int()) { + muls[i] = m_util.mk_numeral(r2 / r1, m_util.is_int(d)); + quot = m_util.mk_mul(muls.size(), muls.c_ptr()); + return true; + } + } + } + else { + for (unsigned i = 0; i < muls.size(); ++i) { + if (d == muls[i].get()) { + muls[i] = muls.back(); + muls.pop_back(); + quot = m_util.mk_mul(muls.size(), muls.c_ptr()); + return true; + } + } + } + } + return false; +} + br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) { set_curr_sort(m().get_sort(arg1)); numeral v1, v2; diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index 68a60e1f0..606d73ae1 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -90,6 +90,7 @@ class arith_rewriter : public poly_rewriter { bool is_pi_integer_offset(expr * t, expr * & m); expr * mk_sin_value(rational const & k); app * mk_sqrt(rational const & k); + bool divides(expr* d, expr* n, expr_ref& quot); public: arith_rewriter(ast_manager & m, params_ref const & p = params_ref()): diff --git a/src/ast/simplifier/arith_simplifier_plugin.cpp b/src/ast/simplifier/arith_simplifier_plugin.cpp index ef320578a..52f36ab04 100644 --- a/src/ast/simplifier/arith_simplifier_plugin.cpp +++ b/src/ast/simplifier/arith_simplifier_plugin.cpp @@ -267,10 +267,55 @@ void arith_simplifier_plugin::mk_idiv(expr * arg1, expr * arg2, expr_ref & resul bool is_int; if (m_util.is_numeral(arg1, v1, is_int) && m_util.is_numeral(arg2, v2, is_int) && !v2.is_zero()) result = m_util.mk_numeral(div(v1, v2), is_int); + else if (divides(arg2, arg1, result)) { + result = m_util.mk_mul(result, m_util.mk_idiv(arg2, arg2)); + } else result = m_util.mk_idiv(arg1, arg2); } +bool arith_simplifier_plugin::divides(expr* d, expr* n, expr_ref& quot) { + ast_manager& m = m_manager; + if (d == n) { + quot = m_util.mk_numeral(rational(1), m_util.is_int(d)); + return true; + } + if (m_util.is_mul(n)) { + expr_ref_vector muls(m); + muls.push_back(n); + expr* n1, *n2; + rational r1, r2; + for (unsigned i = 0; i < muls.size(); ++i) { + if (m_util.is_mul(muls[i].get(), n1, n2)) { + muls[i] = n1; + muls.push_back(n2); + --i; + } + } + if (m_util.is_numeral(d, r1) && !r1.is_zero()) { + for (unsigned i = 0; i < muls.size(); ++i) { + if (m_util.is_numeral(muls[i].get(), r2) && (r2 / r1).is_int()) { + muls[i] = m_util.mk_numeral(r2 / r1, m_util.is_int(d)); + quot = m_util.mk_mul(muls.size(), muls.c_ptr()); + return true; + } + } + } + else { + for (unsigned i = 0; i < muls.size(); ++i) { + if (d == muls[i].get()) { + muls[i] = muls.back(); + muls.pop_back(); + quot = m_util.mk_mul(muls.size(), muls.c_ptr()); + return true; + } + } + } + } + return false; +} + + void arith_simplifier_plugin::prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result) { SASSERT(m_util.is_int(e)); SASSERT(k.is_int() && k.is_pos()); diff --git a/src/ast/simplifier/arith_simplifier_plugin.h b/src/ast/simplifier/arith_simplifier_plugin.h index e6181e211..045ee0e71 100644 --- a/src/ast/simplifier/arith_simplifier_plugin.h +++ b/src/ast/simplifier/arith_simplifier_plugin.h @@ -48,6 +48,7 @@ protected: void div_monomial(expr_ref_vector& monomials, numeral const& g); void get_monomial_gcd(expr_ref_vector& monomials, numeral& g); + bool divides(expr* d, expr* n, expr_ref& quot); public: arith_simplifier_plugin(ast_manager & m, basic_simplifier_plugin & b, arith_simplifier_params & p); diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h index cb1880495..b2b61f079 100644 --- a/src/math/polynomial/polynomial.h +++ b/src/math/polynomial/polynomial.h @@ -19,16 +19,16 @@ Notes: #ifndef POLYNOMIAL_H_ #define POLYNOMIAL_H_ -#include"mpz.h" -#include"rational.h" -#include"obj_ref.h" -#include"ref_vector.h" -#include"z3_exception.h" -#include"scoped_numeral.h" -#include"scoped_numeral_vector.h" -#include"params.h" -#include"mpbqi.h" -#include"rlimit.h" +#include"util/mpz.h" +#include"util/rational.h" +#include"util/obj_ref.h" +#include"util/ref_vector.h" +#include"util/z3_exception.h" +#include"util/scoped_numeral.h" +#include"util/scoped_numeral_vector.h" +#include"util/params.h" +#include"util/mpbqi.h" +#include"util/rlimit.h" class small_object_allocator; diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 7582c8389..7ffb1b0a5 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -623,6 +623,7 @@ namespace nlsat { unsigned sz = cs.size(); for (unsigned i = 0; i < sz; i++) del_clause(cs[i]); + cs.reset(); } void del_clauses() { diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index 3668629cd..08902e709 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -21,10 +21,10 @@ Revision History: #ifndef NLSAT_SOLVER_H_ #define NLSAT_SOLVER_H_ -#include"nlsat_types.h" -#include"params.h" -#include"statistics.h" -#include"rlimit.h" +#include"nlsat/nlsat_types.h" +#include"util/params.h" +#include"util/statistics.h" +#include"util/rlimit.h" namespace nlsat { diff --git a/src/nlsat/nlsat_types.h b/src/nlsat/nlsat_types.h index 11e063a17..70da98e32 100644 --- a/src/nlsat/nlsat_types.h +++ b/src/nlsat/nlsat_types.h @@ -19,10 +19,10 @@ Revision History: #ifndef NLSAT_TYPES_H_ #define NLSAT_TYPES_H_ -#include"polynomial.h" -#include"buffer.h" -#include"sat_types.h" -#include"z3_exception.h" +#include"math/polynomial/polynomial.h" +#include"util/buffer.h" +#include"sat/sat_types.h" +#include"util/z3_exception.h" namespace algebraic_numbers { class anum; diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 28d8d761a..97c8e0e91 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -19,12 +19,12 @@ Revision History: #ifndef SAT_TYPES_H_ #define SAT_TYPES_H_ -#include"debug.h" -#include"approx_set.h" -#include"lbool.h" -#include"z3_exception.h" -#include"common_msgs.h" -#include"vector.h" +#include"util/debug.h" +#include"util/approx_set.h" +#include"util/lbool.h" +#include"util/z3_exception.h" +#include"util/common_msgs.h" +#include"util/vector.h" #include namespace sat { diff --git a/src/shell/lp_frontend.cpp b/src/shell/lp_frontend.cpp index 8acbd28ff..213f94cb2 100644 --- a/src/shell/lp_frontend.cpp +++ b/src/shell/lp_frontend.cpp @@ -80,8 +80,7 @@ void run_solver(lp_params & params, char const * mps_file_name) { solver->settings().set_message_ostream(&std::cout); solver->settings().report_frequency = params.rep_freq(); solver->settings().print_statistics = params.print_stats(); - solver->settings().simplex_strategy() = lean:: simplex_strategy_enum::lu; - + solver->settings().simplex_strategy() = lean::simplex_strategy_enum::lu; solver->find_maximal_solution(); *(solver->settings().get_message_ostream()) << "status is " << lp_status_to_string(solver->get_status()) << std::endl; diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index 41890dd05..3db66eb3e 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -70,6 +70,7 @@ z3_add_component(smt euclid fpa grobner + nlsat lp macros normal_forms diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index a501f474a..6d67bfd19 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -36,7 +36,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'), + ('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'), diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 943bd711e..e71c0adad 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -23,12 +23,13 @@ Revision History: #include"params.h" enum arith_solver_id { - AS_NO_ARITH, - AS_DIFF_LOGIC, - AS_ARITH, - AS_DENSE_DIFF_LOGIC, - AS_UTVPI, - AS_OPTINF + AS_NO_ARITH, // 0 + AS_DIFF_LOGIC, // 1 + AS_ARITH, // 2 + AS_DENSE_DIFF_LOGIC, // 3 + AS_UTVPI, // 4 + AS_OPTINF, // 5 + AS_LRA // 6 }; enum bound_prop_mode { diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index b9c1ac453..c319a8d7d 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -388,6 +388,7 @@ namespace smt { enode * n = *it3; if (is_uninterp_const(n->get_owner()) && m_context->is_relevant(n)) { func_decl * d = n->get_owner()->get_decl(); + TRACE("mg_top_sort", tout << d->get_name() << " " << (m_hidden_ufs.contains(d)?"hidden":"visible") << "\n";); if (m_hidden_ufs.contains(d)) continue; expr * val = get_value(n); m_model->register_decl(d, val); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 4dd1e2510..9646bce2b 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -724,8 +724,6 @@ namespace smt { } void setup::setup_r_arith() { - // to disable theory lra - // m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params)); } @@ -789,6 +787,9 @@ namespace smt { case AS_OPTINF: m_context.register_plugin(alloc(smt::theory_inf_arith, m_manager, m_params)); break; + case AS_LRA: + setup_r_arith(); + break; default: if (m_params.m_arith_int_only && int_only) m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 76e721faa..c35dbb94e 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -35,7 +35,10 @@ Revision History: #include "smt/smt_model_generator.h" #include "smt/arith_eq_adapter.h" #include "util/nat_set.h" +#include "util/lp/nra_solver.h" #include "tactic/filter_model_converter.h" +#include "math/polynomial/algebraic_numbers.h" +#include "math/polynomial/polynomial.h" namespace lp { enum bound_kind { lower_t, upper_t }; @@ -87,16 +90,12 @@ namespace lp { unsigned m_bounds_propagations; unsigned m_num_iterations; unsigned m_num_iterations_with_no_progress; - unsigned m_num_factorizations; unsigned m_need_to_solve_inf; unsigned m_fixed_eqs; unsigned m_conflicts; unsigned m_bound_propagations1; unsigned m_bound_propagations2; unsigned m_assert_diseq; - unsigned m_make_feasible; - unsigned m_max_cols; - unsigned m_max_rows; stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); @@ -118,9 +117,6 @@ namespace smt { unsigned m_bounds_lim; unsigned m_asserted_qhead; unsigned m_asserted_atoms_lim; - unsigned m_delayed_terms_lim; - unsigned m_delayed_equalities_lim; - unsigned m_delayed_defs_lim; unsigned m_underspecified_lim; unsigned m_var_trail_lim; expr* m_not_handled; @@ -144,10 +140,10 @@ namespace smt { ast_manager& m; theory_arith_params& m_arith_params; arith_util a; - arith_eq_adapter m_arith_eq_adapter; + vector m_columns; + - vector m_columns; // temporary values kept during internalization struct internalize_state { expr_ref_vector m_terms; @@ -198,14 +194,6 @@ namespace smt { }; typedef vector> var_coeffs; - struct delayed_def { - vector m_coeffs; - svector m_vars; - rational m_coeff; - theory_var m_var; - delayed_def(svector const& vars, vector const& coeffs, rational const& r, theory_var v): - m_coeffs(coeffs), m_vars(vars), m_coeff(r), m_var(v) {} - }; svector m_theory_var2var_index; // translate from theory variables to lar vars svector m_var_index2theory_var; // reverse map from lp_solver variables to theory variables @@ -224,11 +212,7 @@ namespace smt { svector m_equalities; // asserted rows corresponding to equalities. svector m_definitions; // asserted rows corresponding to definitions - bool m_delay_constraints; // configuration svector m_asserted_atoms; - app_ref_vector m_delayed_terms; - svector> m_delayed_equalities; - vector m_delayed_defs; expr* m_not_handled; ptr_vector m_underspecified; unsigned_vector m_var_trail; @@ -248,16 +232,36 @@ namespace smt { unsigned m_num_conflicts; + // non-linear arithmetic + scoped_ptr m_nra; + bool m_use_nra_model; + scoped_ptr m_a1, m_a2; + + // integer arithmetic + scoped_ptr m_lia; + struct var_value_eq { imp & m_th; var_value_eq(imp & th):m_th(th) {} - bool operator()(theory_var v1, theory_var v2) const { return m_th.get_ivalue(v1) == m_th.get_ivalue(v2) && m_th.is_int(v1) == m_th.is_int(v2); } + bool operator()(theory_var v1, theory_var v2) const { + if (m_th.is_int(v1) != m_th.is_int(v2)) { + return false; + } + return m_th.is_eq(v1, v2); + } }; struct var_value_hash { imp & m_th; var_value_hash(imp & th):m_th(th) {} - unsigned operator()(theory_var v) const { return (unsigned)std::hash()(m_th.get_ivalue(v)); } + unsigned operator()(theory_var v) const { + if (m_th.m_use_nra_model) { + return m_th.is_int(v); + } + else { + return (unsigned)std::hash()(m_th.get_ivalue(v)); + } + } }; int_hashtable m_model_eqs; @@ -289,14 +293,25 @@ namespace smt { m_solver->settings().bound_propagation() = BP_NONE != propagation_mode(); m_solver->set_propagate_bounds_on_pivoted_rows_mode(lp.bprop_on_pivoted_rows()); //m_solver->settings().set_ostream(0); + m_lia = alloc(lean::int_solver, m_solver.get()); } + void ensure_nra() { + if (!m_nra) { + m_nra = alloc(nra::solver, *m_solver.get(), m.limit(), ctx().get_params()); + for (unsigned i = 0; i < m_scopes.size(); ++i) { + m_nra->push(); + } + } + } + + void found_not_handled(expr* n) { m_not_handled = n; if (is_app(n) && is_underspecified(to_app(n))) { + TRACE("arith", tout << "Unhandled: " << mk_pp(n, m) << "\n";); m_underspecified.push_back(to_app(n)); } - TRACE("arith", tout << "Unhandled: " << mk_pp(n, m) << "\n";); } bool is_numeral(expr* term, rational& r) { @@ -366,6 +381,14 @@ namespace smt { terms[index] = n1; st.terms_to_internalize().push_back(n2); } + else if (a.is_mul(n)) { + theory_var v; + internalize_mul(to_app(n), v, r); + coeffs[index] *= r; + coeffs[vars.size()] = coeffs[index]; + vars.push_back(v); + ++index; + } else if (a.is_numeral(n, r)) { coeff += coeffs[index]*r; ++index; @@ -415,6 +438,44 @@ namespace smt { } } + void internalize_mul(app* t, theory_var& v, rational& r) { + SASSERT(a.is_mul(t)); + bool _has_var = has_var(t); + if (!_has_var) { + internalize_args(t); + mk_enode(t); + } + r = rational::one(); + rational r1; + v = mk_var(t); + svector vars; + ptr_vector todo; + todo.push_back(t); + while (!todo.empty()) { + expr* n = todo.back(); + todo.pop_back(); + expr* n1, *n2; + if (a.is_mul(n, n1, n2)) { + todo.push_back(n1); + todo.push_back(n2); + } + else if (a.is_numeral(n, r1)) { + r *= r1; + } + else { + if (!ctx().e_internalized(n)) { + ctx().internalize(n, false); + } + vars.push_back(get_var_index(mk_var(n))); + } + } + TRACE("arith", tout << mk_pp(t, m) << "\n";); + if (!_has_var) { + ensure_nra(); + m_nra->add_monomial(get_var_index(v), vars.size(), vars.c_ptr()); + } + } + enode * mk_enode(app * n) { if (ctx().e_internalized(n)) { return get_enode(n); @@ -459,6 +520,14 @@ namespace smt { return m_arith_params.m_arith_reflect || is_underspecified(n); } + bool has_var(expr* n) { + if (!ctx().e_internalized(n)) { + return false; + } + enode* e = get_enode(n); + return th.is_attached_to_var(e); + } + theory_var mk_var(expr* n, bool internalize = true) { if (!ctx().e_internalized(n)) { ctx().internalize(n, false); @@ -487,7 +556,7 @@ namespace smt { result = m_theory_var2var_index[v]; } if (result == UINT_MAX) { - result = m_solver->add_var(v); // TBD: is_int(v); + result = m_solver->add_var(v, is_int(v)); m_theory_var2var_index.setx(v, result, UINT_MAX); m_var_index2theory_var.setx(result, v, UINT_MAX); m_var_trail.push_back(v); @@ -549,14 +618,6 @@ namespace smt { m_definitions.setx(index, v, null_theory_var); ++m_stats.m_add_rows; } - - void internalize_eq(delayed_def const& d) { - scoped_internalize_state st(*this); - st.vars().append(d.m_vars); - st.coeffs().append(d.m_coeffs); - init_left_side(st); - add_def_constraint(m_solver->add_constraint(m_left_side, lean::EQ, -d.m_coeff), d.m_var); - } void internalize_eq(theory_var v1, theory_var v2) { enode* n1 = get_enode(v1); @@ -650,15 +711,14 @@ namespace smt { a(m), m_arith_eq_adapter(th, ap, a), m_internalize_head(0), - m_delay_constraints(false), - m_delayed_terms(m), m_not_handled(0), m_asserted_qhead(0), m_assume_eq_head(0), m_num_conflicts(0), m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)), m_solver(0), - m_resource_limit(*this) { + m_resource_limit(*this), + m_use_nra_model(false) { } ~imp() { @@ -671,12 +731,8 @@ namespace smt { } bool internalize_atom(app * atom, bool gate_ctx) { - if (m_delay_constraints) { - return internalize_atom_lazy(atom, gate_ctx); - } - else { - return internalize_atom_strict(atom, gate_ctx); - } + return internalize_atom_strict(atom, gate_ctx); + } bool internalize_atom_strict(app * atom, bool gate_ctx) { @@ -710,54 +766,11 @@ namespace smt { //add_use_lists(b); return true; } - - bool internalize_atom_lazy(app * atom, bool gate_ctx) { - SASSERT(!ctx().b_internalized(atom)); - bool_var bv = ctx().mk_bool_var(atom); - ctx().set_var_theory(bv, get_id()); - expr* n1, *n2; - rational r; - lp::bound_kind k; - theory_var v = null_theory_var; - scoped_internalize_state st(*this); - if (a.is_le(atom, n1, n2) && is_numeral(n2, r) && is_app(n1)) { - v = internalize_def(to_app(n1), st); - k = lp::upper_t; - } - else if (a.is_ge(atom, n1, n2) && is_numeral(n2, r) && is_app(n1)) { - v = internalize_def(to_app(n1), st); - k = lp::lower_t; - } - else { - TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";); - found_not_handled(atom); - return true; - } - lp::bound* b = alloc(lp::bound, bv, v, r, k); - m_bounds[v].push_back(b); - updt_unassigned_bounds(v, +1); - m_bounds_trail.push_back(v); - m_bool_var2bound.insert(bv, b); - TRACE("arith", tout << "Internalized " << mk_pp(atom, m) << "\n";); - if (!is_unit_var(st) && m_bounds[v].size() == 1) { - m_delayed_defs.push_back(delayed_def(st.vars(), st.coeffs(), st.coeff(), v)); - } - return true; - } bool internalize_term(app * term) { if (ctx().e_internalized(term) && th.is_attached_to_var(ctx().get_enode(term))) { // skip } - else if (m_delay_constraints) { - scoped_internalize_state st(*this); - linearize_term(term, st); // ensure that a theory_var was created. - SASSERT(ctx().e_internalized(term)); - if(!th.is_attached_to_var(ctx().get_enode(term))) { - mk_var(term); - } - m_delayed_terms.push_back(term); - } else { internalize_def(term); } @@ -783,13 +796,8 @@ namespace smt { } void new_eq_eh(theory_var v1, theory_var v2) { - if (m_delay_constraints) { - m_delayed_equalities.push_back(std::make_pair(v1, v2)); - } - else { - // or internalize_eq(v1, v2); - m_arith_eq_adapter.new_eq_eh(v1, v2); - } + // or internalize_eq(v1, v2); + m_arith_eq_adapter.new_eq_eh(v1, v2); } bool use_diseqs() const { @@ -808,13 +816,11 @@ namespace smt { s.m_bounds_lim = m_bounds_trail.size(); s.m_asserted_qhead = m_asserted_qhead; s.m_asserted_atoms_lim = m_asserted_atoms.size(); - s.m_delayed_terms_lim = m_delayed_terms.size(); - s.m_delayed_equalities_lim = m_delayed_equalities.size(); - s.m_delayed_defs_lim = m_delayed_defs.size(); s.m_not_handled = m_not_handled; s.m_underspecified_lim = m_underspecified.size(); s.m_var_trail_lim = m_var_trail.size(); - if (!m_delay_constraints) m_solver->push(); + m_solver->push(); + if (m_nra) m_nra->push(); } void pop_scope_eh(unsigned num_scopes) { @@ -835,18 +841,16 @@ namespace smt { m_theory_var2var_index[m_var_trail[i]] = UINT_MAX; } m_asserted_atoms.shrink(m_scopes[old_size].m_asserted_atoms_lim); - m_delayed_terms.shrink(m_scopes[old_size].m_delayed_terms_lim); - m_delayed_defs.shrink(m_scopes[old_size].m_delayed_defs_lim); - m_delayed_equalities.shrink(m_scopes[old_size].m_delayed_equalities_lim); m_asserted_qhead = m_scopes[old_size].m_asserted_qhead; m_underspecified.shrink(m_scopes[old_size].m_underspecified_lim); m_var_trail.shrink(m_scopes[old_size].m_var_trail_lim); m_not_handled = m_scopes[old_size].m_not_handled; m_scopes.resize(old_size); - if (!m_delay_constraints) m_solver->pop(num_scopes); + m_solver->pop(num_scopes); // VERIFY(l_false != make_feasible()); m_new_bounds.reset(); m_to_check.reset(); + if (m_nra) m_nra->pop(num_scopes); TRACE("arith", tout << "num scopes: " << num_scopes << " new scope level: " << m_scopes.size() << "\n";); } @@ -1080,7 +1084,9 @@ namespace smt { } tout << "\n"; ); - m_solver->random_update(vars.size(), vars.c_ptr()); + if (!m_use_nra_model) { + m_solver->random_update(vars.size(), vars.c_ptr()); + } m_model_eqs.reset(); TRACE("arith", display(tout);); @@ -1130,54 +1136,69 @@ namespace smt { enode* n2 = get_enode(v2); m_assume_eq_head++; CTRACE("arith", - get_ivalue(v1) == get_ivalue(v2) && n1->get_root() != n2->get_root(), + is_eq(v1, v2) && n1->get_root() != n2->get_root(), tout << "assuming eq: v" << v1 << " = v" << v2 << "\n";); - if (get_ivalue(v1) == get_ivalue(v2) && n1->get_root() != n2->get_root() && th.assume_eq(n1, n2)) { + if (is_eq(v1, v2) && n1->get_root() != n2->get_root() && th.assume_eq(n1, n2)) { return true; } } return false; } + bool is_eq(theory_var v1, theory_var v2) { + if (m_use_nra_model) { + return m_nra->am().eq(nl_value(v1, *m_a1), nl_value(v2, *m_a2)); + } + else { + return get_ivalue(v1) == get_ivalue(v2); + } + } + bool has_delayed_constraints() const { - return !(m_asserted_atoms.empty() && m_delayed_terms.empty() && m_delayed_equalities.empty()); + return !m_asserted_atoms.empty(); } final_check_status final_check_eh() { + m_use_nra_model = false; lbool is_sat = l_true; - if (m_delay_constraints) { - init_solver(); - for (unsigned i = 0; i < m_asserted_atoms.size(); ++i) { - bool_var bv = m_asserted_atoms[i].m_bv; - assert_bound(bv, m_asserted_atoms[i].m_is_true, *m_bool_var2bound.find(bv)); - } - for (unsigned i = 0; i < m_delayed_terms.size(); ++i) { - internalize_def(m_delayed_terms[i].get()); - } - for (unsigned i = 0; i < m_delayed_defs.size(); ++i) { - internalize_eq(m_delayed_defs[i]); - } - for (unsigned i = 0; i < m_delayed_equalities.size(); ++i) { - std::pair const& eq = m_delayed_equalities[i]; - internalize_eq(eq.first, eq.second); - } - is_sat = make_feasible(); - } - else if (m_solver->get_status() != lean::lp_status::OPTIMAL) { + if (m_solver->get_status() != lean::lp_status::OPTIMAL) { is_sat = make_feasible(); } + final_check_status st = FC_DONE; switch (is_sat) { case l_true: + if (delayed_assume_eqs()) { return FC_CONTINUE; } if (assume_eqs()) { return FC_CONTINUE; } - if (m_not_handled != 0) { - return FC_GIVEUP; + + switch (check_lia()) { + case l_true: + break; + case l_false: + return FC_CONTINUE; + case l_undef: + st = FC_GIVEUP; + break; } - return FC_DONE; + + switch (check_nra()) { + case l_true: + break; + case l_false: + return FC_CONTINUE; + case l_undef: + st = FC_GIVEUP; + break; + } + if (m_not_handled != 0) { + st = FC_GIVEUP; + } + + return st; case l_false: set_conflict(); return FC_CONTINUE; @@ -1190,6 +1211,70 @@ namespace smt { return FC_GIVEUP; } + // create a bound atom representing term >= k + lp::bound* mk_bound(lean::lar_term const& term, rational const& k) { + NOT_IMPLEMENTED_YET(); + lp::bound_kind bkind = lp::bound_kind::lower_t; + bool_var bv = null_bool_var; + theory_var v = null_theory_var; + lp::bound* result = alloc(lp::bound, bv, v, k, bkind); + return result; + } + + lbool check_lia() { + std::cout << "called check_lia()\n"; + lean::lar_term term; + lean::mpq k; + lean::explanation ex; // TBD, this should be streamlined accross different explanations + switch(m_lia->check(term, k, ex)) { + case lean::lia_move::ok: + return l_true; + case lean::lia_move::branch: + // branch on term <= k + NOT_IMPLEMENTED_YET(); + return l_false; + case lean::lia_move::cut: + // m_explanation implies term <= k + m_explanation = ex.m_explanation; + NOT_IMPLEMENTED_YET(); + return l_false; + case lean::lia_move::conflict: + // ex contains unsat core + m_explanation = ex.m_explanation; + set_conflict1(); + return l_false; + case lean::lia_move::give_up: + return l_undef; + default: + UNREACHABLE(); + } + return l_undef; + } + + lbool check_nra() { + m_use_nra_model = false; + if (m.canceled()) return l_undef; + if (!m_nra) return l_true; + if (!m_nra->need_check()) return l_true; + m_a1 = 0; m_a2 = 0; + lbool r = m_nra->check(m_explanation); + m_a1 = alloc(scoped_anum, m_nra->am()); + m_a2 = alloc(scoped_anum, m_nra->am()); + switch (r) { + case l_false: + set_conflict1(); + break; + case l_true: + m_use_nra_model = true; + if (assume_eqs()) { + return l_false; + } + break; + default: + break; + } + return r; + } /** \brief We must redefine this method, because theory of arithmetic contains @@ -1259,14 +1344,13 @@ namespace smt { #else propagate_bound(bv, is_true, b); #endif - if (!m_delay_constraints) { - lp::bound& b = *m_bool_var2bound.find(bv); - assert_bound(bv, is_true, b); - } + lp::bound& b = *m_bool_var2bound.find(bv); + assert_bound(bv, is_true, b); + ++m_asserted_qhead; } - if (m_delay_constraints || ctx().inconsistent()) { + if (ctx().inconsistent()) { m_to_check.reset(); return; } @@ -2133,18 +2217,8 @@ namespace smt { } lbool make_feasible() { - reset_variable_values(); - ++m_stats.m_make_feasible; - if (m_solver->A_r().column_count() > m_stats.m_max_cols) - m_stats.m_max_cols = m_solver->A_r().column_count(); - if (m_solver->A_r().row_count() > m_stats.m_max_rows) - m_stats.m_max_rows = m_solver->A_r().row_count(); + auto status = m_solver->find_feasible_solution(); TRACE("arith_verbose", display(tout);); - lean::lp_status status = m_solver->find_feasible_solution(); - m_stats.m_num_iterations = m_solver->settings().st().m_total_iterations; - m_stats.m_num_factorizations = m_solver->settings().st().m_num_factorizations; - m_stats.m_need_to_solve_inf = m_solver->settings().st().m_need_to_solve_inf; - switch (status) { case lean::lp_status::INFEASIBLE: return l_false; @@ -2197,11 +2271,15 @@ namespace smt { } void set_conflict() { + m_explanation.clear(); + m_solver->get_infeasibility_explanation(m_explanation); + set_conflict1(); + } + + void set_conflict1() { m_eqs.reset(); m_core.reset(); m_params.reset(); - m_explanation.clear(); - m_solver->get_infeasibility_explanation(m_explanation); // m_solver->shrink_explanation_to_minimum(m_explanation); // todo, enable when perf is fixed /* static unsigned cn = 0; @@ -2250,9 +2328,43 @@ namespace smt { TRACE("arith", display(tout);); } + nlsat::anum const& nl_value(theory_var v, scoped_anum& r) { + SASSERT(m_nra); + SASSERT(m_use_nra_model); + lean::var_index vi = m_theory_var2var_index[v]; + if (m_solver->is_term(vi)) { + lean::lar_term const& term = m_solver->get_term(vi); + scoped_anum r1(m_nra->am()); + m_nra->am().set(r, term.m_v.to_mpq()); + + for (auto const coeff : term.m_coeffs) { + lean::var_index wi = coeff.first; + m_nra->am().set(r1, coeff.second.to_mpq()); + m_nra->am().mul(m_nra->value(wi), r1, r1); + m_nra->am().add(r1, r, r); + } + return r; + } + else { + return m_nra->value(vi); + } + } + model_value_proc * mk_value(enode * n, model_generator & mg) { theory_var v = n->get_th_var(get_id()); - return alloc(expr_wrapper_proc, m_factory->mk_value(get_value(v), m.get_sort(n->get_owner()))); + expr* o = n->get_owner(); + if (m_use_nra_model) { + anum const& an = nl_value(v, *m_a1); + if (a.is_int(o) && !m_nra->am().is_int(an)) { + return alloc(expr_wrapper_proc, a.mk_numeral(rational::zero(), a.is_int(o))); + } + return alloc(expr_wrapper_proc, a.mk_numeral(nl_value(v, *m_a1), a.is_int(o))); + } + else { + rational r = get_value(v); + if (a.is_int(o) && !r.is_int()) r = floor(r); + return alloc(expr_wrapper_proc, m_factory->mk_value(r, m.get_sort(o))); + } } bool get_value(enode* n, expr_ref& r) { @@ -2278,6 +2390,7 @@ namespace smt { if (dump_lemmas()) { ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal); } + if (m_arith_params.m_arith_mode == AS_LRA) return true; context nctx(m, ctx().get_fparams(), ctx().get_params()); add_background(nctx); bool result = l_true != nctx.check(); @@ -2290,6 +2403,7 @@ namespace smt { if (dump_lemmas()) { ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit); } + if (m_arith_params.m_arith_mode == AS_LRA) return true; context nctx(m, ctx().get_fparams(), ctx().get_params()); m_core.push_back(~lit); add_background(nctx); @@ -2301,6 +2415,7 @@ namespace smt { } bool validate_eq(enode* x, enode* y) { + if (m_arith_params.m_arith_mode == AS_LRA) return true; context nctx(m, ctx().get_fparams(), ctx().get_params()); add_background(nctx); nctx.assert_expr(m.mk_not(m.mk_eq(x->get_owner(), y->get_owner()))); @@ -2496,7 +2611,7 @@ namespace smt { st.update("arith-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", m_stats.m_num_factorizations); + st.update("arith-factorizations", m_solver->settings().st().m_num_factorizations); st.update("arith-pivots", m_stats.m_need_to_solve_inf); st.update("arith-plateau-iterations", m_stats.m_num_iterations_with_no_progress); st.update("arith-fixed-eqs", m_stats.m_fixed_eqs); @@ -2504,9 +2619,9 @@ namespace smt { st.update("arith-bound-propagations-lp", m_stats.m_bound_propagations1); st.update("arith-bound-propagations-cheap", m_stats.m_bound_propagations2); st.update("arith-diseq", m_stats.m_assert_diseq); - st.update("arith-make-feasible", m_stats.m_make_feasible); - st.update("arith-max-columns", m_stats.m_max_cols); - st.update("arith-max-rows", m_stats.m_max_rows); + st.update("arith-make-feasible", m_solver->settings().st().m_make_feasible); + st.update("arith-max-columns", m_solver->settings().st().m_max_cols); + st.update("arith-max-rows", m_solver->settings().st().m_max_rows); } }; diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index b395c09e6..f92525069 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -1,4 +1,5 @@ add_subdirectory(fuzzing) +add_subdirectory(lp) ################################################################################ # z3-test executable ################################################################################ @@ -117,7 +118,7 @@ add_executable(test-z3 upolynomial.cpp var_subst.cpp vector.cpp - lp.cpp + lp/lp.cpp ${z3_test_extra_object_files} ) z3_add_install_tactic_rule(${z3_test_deps}) diff --git a/src/test/lp/CMakeLists.txt b/src/test/lp/CMakeLists.txt new file mode 100644 index 000000000..6683a1758 --- /dev/null +++ b/src/test/lp/CMakeLists.txt @@ -0,0 +1,6 @@ +add_executable(lp_tst lp_main.cpp lp.cpp $ $ $ $ ) +target_compile_definitions(lp_tst PRIVATE ${Z3_COMPONENT_CXX_DEFINES}) +target_compile_options(lp_tst PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) +target_include_directories(lp_tst PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}) +target_link_libraries(lp_tst PRIVATE ${Z3_DEPENDENT_LIBS}) +z3_append_linker_flag_list_to_target(lp_tst ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) diff --git a/src/test/argument_parser.h b/src/test/lp/argument_parser.h similarity index 100% rename from src/test/argument_parser.h rename to src/test/lp/argument_parser.h diff --git a/src/test/lp.cpp b/src/test/lp/lp.cpp similarity index 98% rename from src/test/lp.cpp rename to src/test/lp/lp.cpp index 9e05112f5..71032d013 100644 --- a/src/test/lp.cpp +++ b/src/test/lp/lp.cpp @@ -2695,8 +2695,8 @@ void test_term() { lar_solver solver; unsigned _x = 0; unsigned _y = 1; - var_index x = solver.add_var(_x); - var_index y = solver.add_var(_y); + var_index x = solver.add_var(_x, false); + var_index y = solver.add_var(_y, false); vector> term_ls; term_ls.push_back(std::pair((int)1, x)); @@ -2709,9 +2709,16 @@ void test_term() { ls.push_back(std::pair((int)1, z)); solver.add_constraint(ls, lconstraint_kind::EQ, mpq(0)); + ls.clear(); + ls.push_back(std::pair((int)1, x)); + solver.add_constraint(ls, lconstraint_kind::LT, mpq(0)); + ls.push_back(std::pair((int)2, y)); + solver.add_constraint(ls, lconstraint_kind::GT, mpq(0)); auto status = solver.solve(); std::cout << lp_status_to_string(status) << std::endl; std::unordered_map model; + if (status != OPTIMAL) + return; solver.get_model(model); for (auto & t : model) { @@ -2723,8 +2730,8 @@ void test_term() { void test_evidence_for_total_inf_simple(argument_parser & args_parser) { lar_solver solver; - var_index x = solver.add_var(0); - var_index y = solver.add_var(1); + var_index x = solver.add_var(0, false); + var_index y = solver.add_var(1, false); solver.add_var_bound(x, LE, -mpq(1)); solver.add_var_bound(y, GE, mpq(0)); vector> ls; @@ -2758,9 +2765,9 @@ If b becomes basic variable, then it is likely the old solver ends up with a row return true; }; lar_solver ls; - unsigned a = ls.add_var(0); - unsigned b = ls.add_var(1); - unsigned c = ls.add_var(2); + unsigned a = ls.add_var(0, false); + unsigned b = ls.add_var(1, false); + unsigned c = ls.add_var(2, false); vector> coeffs; coeffs.push_back(std::pair(1, a)); coeffs.push_back(std::pair(-1, c)); @@ -2823,8 +2830,8 @@ If x9 becomes basic variable, then it is likely the old solver ends up with a ro } void test_bound_propagation_one_row() { lar_solver ls; - unsigned x0 = ls.add_var(0); - unsigned x1 = ls.add_var(1); + unsigned x0 = ls.add_var(0, false); + unsigned x1 = ls.add_var(1, false); vector> c; c.push_back(std::pair(1, x0)); c.push_back(std::pair(-1, x1)); @@ -2837,8 +2844,8 @@ void test_bound_propagation_one_row() { } void test_bound_propagation_one_row_with_bounded_vars() { lar_solver ls; - unsigned x0 = ls.add_var(0); - unsigned x1 = ls.add_var(1); + unsigned x0 = ls.add_var(0, false); + unsigned x1 = ls.add_var(1, false); vector> c; c.push_back(std::pair(1, x0)); c.push_back(std::pair(-1, x1)); @@ -2853,8 +2860,8 @@ void test_bound_propagation_one_row_with_bounded_vars() { } void test_bound_propagation_one_row_mixed() { lar_solver ls; - unsigned x0 = ls.add_var(0); - unsigned x1 = ls.add_var(1); + unsigned x0 = ls.add_var(0, false); + unsigned x1 = ls.add_var(1, false); vector> c; c.push_back(std::pair(1, x0)); c.push_back(std::pair(-1, x1)); @@ -2868,9 +2875,9 @@ void test_bound_propagation_one_row_mixed() { void test_bound_propagation_two_rows() { lar_solver ls; - unsigned x = ls.add_var(0); - unsigned y = ls.add_var(1); - unsigned z = ls.add_var(2); + unsigned x = ls.add_var(0, false); + unsigned y = ls.add_var(1, false); + unsigned z = ls.add_var(2, false); vector> c; c.push_back(std::pair(1, x)); c.push_back(std::pair(2, y)); @@ -2892,9 +2899,9 @@ void test_bound_propagation_two_rows() { void test_total_case_u() { std::cout << "test_total_case_u\n"; lar_solver ls; - unsigned x = ls.add_var(0); - unsigned y = ls.add_var(1); - unsigned z = ls.add_var(2); + unsigned x = ls.add_var(0, false); + unsigned y = ls.add_var(1, false); + unsigned z = ls.add_var(2, false); vector> c; c.push_back(std::pair(1, x)); c.push_back(std::pair(2, y)); @@ -2918,9 +2925,9 @@ bool contains_j_kind(unsigned j, lconstraint_kind kind, const mpq & rs, const ve void test_total_case_l(){ std::cout << "test_total_case_l\n"; lar_solver ls; - unsigned x = ls.add_var(0); - unsigned y = ls.add_var(1); - unsigned z = ls.add_var(2); + unsigned x = ls.add_var(0, false); + unsigned y = ls.add_var(1, false); + unsigned z = ls.add_var(2, false); vector> c; c.push_back(std::pair(1, x)); c.push_back(std::pair(2, y)); diff --git a/src/test/lp/lp_main.cpp b/src/test/lp/lp_main.cpp new file mode 100644 index 000000000..a301f38c6 --- /dev/null +++ b/src/test/lp/lp_main.cpp @@ -0,0 +1,14 @@ +void gparams_register_modules(){} +void mem_initialize() {} +void mem_finalize() {} +#include "util/rational.h" +namespace lean { +void test_lp_local(int argc, char**argv); +} +int main(int argn, char**argv){ + rational::initialize(); + lean::test_lp_local(argn, argv); + rational::finalize(); + return 0; +} + diff --git a/src/test/smt_reader.h b/src/test/lp/smt_reader.h similarity index 99% rename from src/test/smt_reader.h rename to src/test/lp/smt_reader.h index 38e3f4157..dd38c6bcd 100644 --- a/src/test/smt_reader.h +++ b/src/test/lp/smt_reader.h @@ -376,7 +376,7 @@ namespace lean { void add_constraint_to_solver(lar_solver * solver, formula_constraint & fc) { vector> ls; for (auto & it : fc.m_coeffs) { - ls.push_back(std::make_pair(it.first, solver->add_var(register_name(it.second)))); + ls.push_back(std::make_pair(it.first, solver->add_var(register_name(it.second), false))); } solver->add_constraint(ls, fc.m_kind, fc.m_right_side); } diff --git a/src/test/test_file_reader.h b/src/test/lp/test_file_reader.h similarity index 100% rename from src/test/test_file_reader.h rename to src/test/lp/test_file_reader.h diff --git a/src/util/lp/CMakeLists.txt b/src/util/lp/CMakeLists.txt index 57ebecc8d..72c2482bb 100644 --- a/src/util/lp/CMakeLists.txt +++ b/src/util/lp/CMakeLists.txt @@ -8,6 +8,8 @@ z3_add_component(lp dense_matrix_instances.cpp eta_matrix_instances.cpp indexed_vector_instances.cpp + int_solver.cpp + lar_solver_instances.cpp lar_core_solver_instances.cpp lp_core_solver_base_instances.cpp lp_dual_core_solver_instances.cpp @@ -18,8 +20,9 @@ z3_add_component(lp lp_solver_instances.cpp lu_instances.cpp matrix_instances.cpp + nra_solver.cpp permutation_matrix_instances.cpp - quick_xplain.cpp + quick_xplain.cpp row_eta_matrix_instances.cpp scaler_instances.cpp sparse_matrix_instances.cpp @@ -28,6 +31,8 @@ z3_add_component(lp random_updater_instances.cpp COMPONENT_DEPENDENCIES util + polynomial + nlsat PYG_FILES lp_params.pyg ) diff --git a/src/util/lp/column_namer.h b/src/util/lp/column_namer.h index 1a10a5a23..a3fe05dd0 100644 --- a/src/util/lp/column_namer.h +++ b/src/util/lp/column_namer.h @@ -15,7 +15,7 @@ public: T a; unsigned i; while (it->next(a, i)) { - coeff.emplace_back(a, i); + coeff.push_back(std::make_pair(a, i)); } print_linear_combination_of_column_indices(coeff, out); } diff --git a/src/util/lp/indexed_vector.h b/src/util/lp/indexed_vector.h index 6e6a6009b..4b9a7767d 100644 --- a/src/util/lp/indexed_vector.h +++ b/src/util/lp/indexed_vector.h @@ -75,16 +75,7 @@ public: } void set_value(const T& value, unsigned index); - void set_value_as_in_dictionary(unsigned index) { - lean_assert(index < m_data.size()); - T & loc = m_data[index]; - if (is_zero(loc)) { - m_index.push_back(index); - loc = one_of_type(); // use as a characteristic function - } - } - void clear(); void clear_all(); const T& operator[] (unsigned i) const { diff --git a/src/util/lp/init_lar_solver.h b/src/util/lp/init_lar_solver.h deleted file mode 100644 index 3fc29f25b..000000000 --- a/src/util/lp/init_lar_solver.h +++ /dev/null @@ -1,576 +0,0 @@ -/* - Copyright (c) 2017 Microsoft Corporation - Author: Lev Nachmanson -*/ - -// here we are inside lean::lar_solver class - -bool strategy_is_undecided() const { - return m_settings.simplex_strategy() == simplex_strategy_enum::undecided; -} - -var_index add_var(unsigned ext_j) { - var_index i; - lean_assert (ext_j < m_terms_start_index); - - if (ext_j >= m_terms_start_index) - throw 0; // todo : what is the right way to exit? - - if (try_get_val(m_ext_vars_to_columns, ext_j, i)) { - return i; - } - lean_assert(m_vars_to_ul_pairs.size() == A_r().column_count()); - i = A_r().column_count(); - m_vars_to_ul_pairs.push_back (ul_pair(static_cast(-1))); - add_non_basic_var_to_core_fields(ext_j); - lean_assert(sizes_are_correct()); - return i; -} - -void register_new_ext_var_index(unsigned ext_v) { - lean_assert(!contains(m_ext_vars_to_columns, ext_v)); - unsigned j = static_cast(m_ext_vars_to_columns.size()); - m_ext_vars_to_columns[ext_v] = j; - lean_assert(m_columns_to_ext_vars_or_term_indices.size() == j); - m_columns_to_ext_vars_or_term_indices.push_back(ext_v); -} - -void add_non_basic_var_to_core_fields(unsigned ext_j) { - register_new_ext_var_index(ext_j); - m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column); - m_columns_with_changed_bound.increase_size_by_one(); - add_new_var_to_core_fields_for_mpq(false); - if (use_lu()) - add_new_var_to_core_fields_for_doubles(false); -} - -void add_new_var_to_core_fields_for_doubles(bool register_in_basis) { - unsigned j = A_d().column_count(); - A_d().add_column(); - lean_assert(m_mpq_lar_core_solver.m_d_x.size() == j); - // lean_assert(m_mpq_lar_core_solver.m_d_low_bounds.size() == j && m_mpq_lar_core_solver.m_d_upper_bounds.size() == j); // restore later - m_mpq_lar_core_solver.m_d_x.resize(j + 1 ); - m_mpq_lar_core_solver.m_d_low_bounds.resize(j + 1); - m_mpq_lar_core_solver.m_d_upper_bounds.resize(j + 1); - lean_assert(m_mpq_lar_core_solver.m_d_heading.size() == j); // as A().column_count() on the entry to the method - if (register_in_basis) { - A_d().add_row(); - m_mpq_lar_core_solver.m_d_heading.push_back(m_mpq_lar_core_solver.m_d_basis.size()); - m_mpq_lar_core_solver.m_d_basis.push_back(j); - }else { - m_mpq_lar_core_solver.m_d_heading.push_back(- static_cast(m_mpq_lar_core_solver.m_d_nbasis.size()) - 1); - m_mpq_lar_core_solver.m_d_nbasis.push_back(j); - } -} - -void add_new_var_to_core_fields_for_mpq(bool register_in_basis) { - unsigned j = A_r().column_count(); - A_r().add_column(); - lean_assert(m_mpq_lar_core_solver.m_r_x.size() == j); - // lean_assert(m_mpq_lar_core_solver.m_r_low_bounds.size() == j && m_mpq_lar_core_solver.m_r_upper_bounds.size() == j); // restore later - m_mpq_lar_core_solver.m_r_x.resize(j + 1); - m_mpq_lar_core_solver.m_r_low_bounds.increase_size_by_one(); - m_mpq_lar_core_solver.m_r_upper_bounds.increase_size_by_one(); - m_mpq_lar_core_solver.m_r_solver.m_inf_set.increase_size_by_one(); - m_mpq_lar_core_solver.m_r_solver.m_costs.resize(j + 1); - m_mpq_lar_core_solver.m_r_solver.m_d.resize(j + 1); - lean_assert(m_mpq_lar_core_solver.m_r_heading.size() == j); // as A().column_count() on the entry to the method - if (register_in_basis) { - A_r().add_row(); - m_mpq_lar_core_solver.m_r_heading.push_back(m_mpq_lar_core_solver.m_r_basis.size()); - m_mpq_lar_core_solver.m_r_basis.push_back(j); - if (m_settings.bound_propagation()) - m_rows_with_changed_bounds.insert(A_r().row_count() - 1); - } else { - m_mpq_lar_core_solver.m_r_heading.push_back(- static_cast(m_mpq_lar_core_solver.m_r_nbasis.size()) - 1); - m_mpq_lar_core_solver.m_r_nbasis.push_back(j); - } -} - - -var_index add_term_undecided(const vector> & coeffs, - const mpq &m_v) { - m_terms.push_back(new lar_term(coeffs, m_v)); - m_orig_terms.push_back(new lar_term(coeffs, m_v)); - return m_terms_start_index + m_terms.size() - 1; -} - -// terms -var_index add_term(const vector> & coeffs, - const mpq &m_v) { - if (strategy_is_undecided()) - return add_term_undecided(coeffs, m_v); - - m_terms.push_back(new lar_term(coeffs, m_v)); - m_orig_terms.push_back(new lar_term(coeffs, m_v)); - unsigned adjusted_term_index = m_terms.size() - 1; - var_index ret = m_terms_start_index + adjusted_term_index; - if (use_tableau() && !coeffs.empty()) { - add_row_for_term(m_orig_terms.back(), ret); - if (m_settings.bound_propagation()) - m_rows_with_changed_bounds.insert(A_r().row_count() - 1); - } - lean_assert(m_ext_vars_to_columns.size() == A_r().column_count()); - return ret; -} - -void add_row_for_term(const lar_term * term, unsigned term_ext_index) { - lean_assert(sizes_are_correct()); - add_row_from_term_no_constraint(term, term_ext_index); - lean_assert(sizes_are_correct()); -} - -void add_row_from_term_no_constraint(const lar_term * term, unsigned term_ext_index) { - register_new_ext_var_index(term_ext_index); - // j will be a new variable - unsigned j = A_r().column_count(); - ul_pair ul(j); - m_vars_to_ul_pairs.push_back(ul); - add_basic_var_to_core_fields(); - if (use_tableau()) { - auto it = iterator_on_term_with_basis_var(*term, j); - A_r().fill_last_row_with_pivoting(it, - m_mpq_lar_core_solver.m_r_solver.m_basis_heading); - m_mpq_lar_core_solver.m_r_solver.m_b.resize(A_r().column_count(), zero_of_type()); - } else { - fill_last_row_of_A_r(A_r(), term); - } - m_mpq_lar_core_solver.m_r_x[j] = get_basic_var_value_from_row_directly(A_r().row_count() - 1); - if (use_lu()) - fill_last_row_of_A_d(A_d(), term); -} - -void add_basic_var_to_core_fields() { - bool use_lu = m_mpq_lar_core_solver.need_to_presolve_with_double_solver(); - lean_assert(!use_lu || A_r().column_count() == A_d().column_count()); - m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column); - m_columns_with_changed_bound.increase_size_by_one(); - m_rows_with_changed_bounds.increase_size_by_one(); - add_new_var_to_core_fields_for_mpq(true); - if (use_lu) - add_new_var_to_core_fields_for_doubles(true); -} - -constraint_index add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) { - constraint_index ci = m_constraints.size(); - if (!is_term(j)) { // j is a var - auto vc = new lar_var_constraint(j, kind, right_side); - m_constraints.push_back(vc); - update_column_type_and_bound(j, kind, right_side, ci); - } else { - add_var_bound_on_constraint_for_term(j, kind, right_side, ci); - } - lean_assert(sizes_are_correct()); - return ci; -} - -void update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index) { - switch(m_mpq_lar_core_solver.m_column_types[j]) { - case column_type::free_column: - update_free_column_type_and_bound(j, kind, right_side, constr_index); - break; - case column_type::boxed: - update_boxed_column_type_and_bound(j, kind, right_side, constr_index); - break; - case column_type::low_bound: - update_low_bound_column_type_and_bound(j, kind, right_side, constr_index); - break; - case column_type::upper_bound: - update_upper_bound_column_type_and_bound(j, kind, right_side, constr_index); - break; - case column_type::fixed: - update_fixed_column_type_and_bound(j, kind, right_side, constr_index); - break; - default: - lean_assert(false); // cannot be here - } -} - -void add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { - lean_assert(is_term(j)); - unsigned adjusted_term_index = adjust_term_index(j); - unsigned term_j; - if (try_get_val(m_ext_vars_to_columns, j, term_j)) { - mpq rs = right_side - m_orig_terms[adjusted_term_index]->m_v; - m_constraints.push_back(new lar_term_constraint(m_orig_terms[adjusted_term_index], kind, right_side)); - update_column_type_and_bound(term_j, kind, rs, ci); - } - else { - add_constraint_from_term_and_create_new_column_row(j, m_orig_terms[adjusted_term_index], kind, right_side); - } -} - - -void add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term, - lconstraint_kind kind, const mpq & right_side) { - - add_row_from_term_no_constraint(term, term_j); - unsigned j = A_r().column_count() - 1; - update_column_type_and_bound(j, kind, right_side - term->m_v, m_constraints.size()); - m_constraints.push_back(new lar_term_constraint(term, kind, right_side)); - lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); -} - -void decide_on_strategy_and_adjust_initial_state() { - lean_assert(strategy_is_undecided()); - if (m_vars_to_ul_pairs.size() > m_settings.column_number_threshold_for_using_lu_in_lar_solver) { - m_settings.simplex_strategy() = simplex_strategy_enum::lu; - } else { - m_settings.simplex_strategy() = simplex_strategy_enum::tableau_rows; // todo: when to switch to tableau_costs? - } - adjust_initial_state(); -} - -void adjust_initial_state() { - switch (m_settings.simplex_strategy()) { - case simplex_strategy_enum::lu: - adjust_initial_state_for_lu(); - break; - case simplex_strategy_enum::tableau_rows: - adjust_initial_state_for_tableau_rows(); - break; - case simplex_strategy_enum::tableau_costs: - lean_assert(false); // not implemented - case simplex_strategy_enum::undecided: - adjust_initial_state_for_tableau_rows(); - break; - } -} - -void adjust_initial_state_for_lu() { - copy_from_mpq_matrix(A_d()); - unsigned n = A_d().column_count(); - m_mpq_lar_core_solver.m_d_x.resize(n); - m_mpq_lar_core_solver.m_d_low_bounds.resize(n); - m_mpq_lar_core_solver.m_d_upper_bounds.resize(n); - m_mpq_lar_core_solver.m_d_heading = m_mpq_lar_core_solver.m_r_heading; - m_mpq_lar_core_solver.m_d_basis = m_mpq_lar_core_solver.m_r_basis; - - /* - unsigned j = A_d().column_count(); - A_d().add_column(); - lean_assert(m_mpq_lar_core_solver.m_d_x.size() == j); - // lean_assert(m_mpq_lar_core_solver.m_d_low_bounds.size() == j && m_mpq_lar_core_solver.m_d_upper_bounds.size() == j); // restore later - m_mpq_lar_core_solver.m_d_x.resize(j + 1 ); - m_mpq_lar_core_solver.m_d_low_bounds.resize(j + 1); - m_mpq_lar_core_solver.m_d_upper_bounds.resize(j + 1); - lean_assert(m_mpq_lar_core_solver.m_d_heading.size() == j); // as A().column_count() on the entry to the method - if (register_in_basis) { - A_d().add_row(); - m_mpq_lar_core_solver.m_d_heading.push_back(m_mpq_lar_core_solver.m_d_basis.size()); - m_mpq_lar_core_solver.m_d_basis.push_back(j); - }else { - m_mpq_lar_core_solver.m_d_heading.push_back(- static_cast(m_mpq_lar_core_solver.m_d_nbasis.size()) - 1); - m_mpq_lar_core_solver.m_d_nbasis.push_back(j); - }*/ -} - -void adjust_initial_state_for_tableau_rows() { - for (unsigned j = 0; j < m_terms.size(); j++) { - if (contains(m_ext_vars_to_columns, j + m_terms_start_index)) - continue; - add_row_from_term_no_constraint(m_terms[j], j + m_terms_start_index); - } -} - -// this fills the last row of A_d and sets the basis column: -1 in the last column of the row -void fill_last_row_of_A_d(static_matrix & A, const lar_term* ls) { - lean_assert(A.row_count() > 0); - lean_assert(A.column_count() > 0); - unsigned last_row = A.row_count() - 1; - lean_assert(A.m_rows[last_row].empty()); - - for (auto & t : ls->m_coeffs) { - lean_assert(!is_zero(t.second)); - var_index j = t.first; - A.set(last_row, j, - t.second.get_double()); - } - - unsigned basis_j = A.column_count() - 1; - A.set(last_row, basis_j, - 1 ); -} - -void update_free_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_ind) { - mpq y_of_bound(0); - switch (kind) { - case LT: - y_of_bound = -1; - case LE: - m_mpq_lar_core_solver.m_column_types[j] = column_type::upper_bound; - lean_assert(m_mpq_lar_core_solver.m_column_types()[j] == column_type::upper_bound); - lean_assert(m_mpq_lar_core_solver.m_r_upper_bounds.size() > j); - { - auto up = numeric_pair(right_side, y_of_bound); - m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; - } - set_upper_bound_witness(j, constr_ind); - break; - case GT: - y_of_bound = 1; - case GE: - m_mpq_lar_core_solver.m_column_types[j] = column_type::low_bound; - lean_assert(m_mpq_lar_core_solver.m_r_upper_bounds.size() > j); - { - auto low = numeric_pair(right_side, y_of_bound); - m_mpq_lar_core_solver.m_r_low_bounds[j] = low; - } - set_low_bound_witness(j, constr_ind); - break; - case EQ: - m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed; - m_mpq_lar_core_solver.m_r_low_bounds[j] = m_mpq_lar_core_solver.m_r_upper_bounds[j] = numeric_pair(right_side, zero_of_type()); - set_upper_bound_witness(j, constr_ind); - set_low_bound_witness(j, constr_ind); - break; - - default: - lean_unreachable(); - - } - m_columns_with_changed_bound.insert(j); -} - -void update_upper_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { - lean_assert(m_mpq_lar_core_solver.m_column_types()[j] == column_type::upper_bound); - mpq y_of_bound(0); - switch (kind) { - case LT: - y_of_bound = -1; - case LE: - { - auto up = numeric_pair(right_side, y_of_bound); - if (up < m_mpq_lar_core_solver.m_r_upper_bounds()[j]) { - m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; - set_upper_bound_witness(j, ci); - m_columns_with_changed_bound.insert(j); - } - } - break; - case GT: - y_of_bound = 1; - case GE: - m_mpq_lar_core_solver.m_column_types[j] = column_type::boxed; - { - auto low = numeric_pair(right_side, y_of_bound); - m_mpq_lar_core_solver.m_r_low_bounds[j] = low; - set_low_bound_witness(j, ci); - m_columns_with_changed_bound.insert(j); - if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { - m_status = INFEASIBLE; - m_infeasible_column_index = j; - } else { - m_mpq_lar_core_solver.m_column_types[j] = m_mpq_lar_core_solver.m_r_low_bounds()[j] < m_mpq_lar_core_solver.m_r_upper_bounds()[j]? column_type::boxed : column_type::fixed; - } - } - break; - case EQ: - { - auto v = numeric_pair(right_side, zero_of_type()); - if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { - m_status = INFEASIBLE; - set_low_bound_witness(j, ci); - m_infeasible_column_index = j; - } else { - m_mpq_lar_core_solver.m_r_low_bounds[j] = m_mpq_lar_core_solver.m_r_upper_bounds[j] = v; - m_columns_with_changed_bound.insert(j); - set_low_bound_witness(j, ci); - set_upper_bound_witness(j, ci); - m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed; - } - break; - } - break; - - default: - lean_unreachable(); - - } -} - -void update_boxed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { - lean_assert(m_status == INFEASIBLE || (m_mpq_lar_core_solver.m_column_types()[j] == column_type::boxed && m_mpq_lar_core_solver.m_r_low_bounds()[j] < m_mpq_lar_core_solver.m_r_upper_bounds()[j])); - mpq y_of_bound(0); - switch (kind) { - case LT: - y_of_bound = -1; - case LE: - { - auto up = numeric_pair(right_side, y_of_bound); - if (up < m_mpq_lar_core_solver.m_r_upper_bounds[j]) { - m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; - set_upper_bound_witness(j, ci); - m_columns_with_changed_bound.insert(j); - } - - if (up < m_mpq_lar_core_solver.m_r_low_bounds[j]) { - m_status = INFEASIBLE; - lean_assert(false); - m_infeasible_column_index = j; - } else { - if (m_mpq_lar_core_solver.m_r_low_bounds()[j] == m_mpq_lar_core_solver.m_r_upper_bounds()[j]) - m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed; - } - } - break; - case GT: - y_of_bound = 1; - case GE: - { - auto low = numeric_pair(right_side, y_of_bound); - if (low > m_mpq_lar_core_solver.m_r_low_bounds[j]) { - m_mpq_lar_core_solver.m_r_low_bounds[j] = low; - m_columns_with_changed_bound.insert(j); - set_low_bound_witness(j, ci); - } - if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { - m_status = INFEASIBLE; - m_infeasible_column_index = j; - } else if ( low == m_mpq_lar_core_solver.m_r_upper_bounds[j]) { - m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed; - } - } - break; - case EQ: - { - auto v = numeric_pair(right_side, zero_of_type()); - if (v < m_mpq_lar_core_solver.m_r_low_bounds[j]) { - m_status = INFEASIBLE; - m_infeasible_column_index = j; - set_upper_bound_witness(j, ci); - } else if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { - m_status = INFEASIBLE; - m_infeasible_column_index = j; - set_low_bound_witness(j, ci); - } else { - m_mpq_lar_core_solver.m_r_low_bounds[j] = m_mpq_lar_core_solver.m_r_upper_bounds[j] = v; - set_low_bound_witness(j, ci); - set_upper_bound_witness(j, ci); - m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed; - m_columns_with_changed_bound.insert(j); - } - - break; - } - - default: - lean_unreachable(); - - } -} -void update_low_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { - lean_assert(m_mpq_lar_core_solver.m_column_types()[j] == column_type::low_bound); - mpq y_of_bound(0); - switch (kind) { - case LT: - y_of_bound = -1; - case LE: - { - auto up = numeric_pair(right_side, y_of_bound); - m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; - set_upper_bound_witness(j, ci); - m_columns_with_changed_bound.insert(j); - - if (up < m_mpq_lar_core_solver.m_r_low_bounds[j]) { - m_status = INFEASIBLE; - m_infeasible_column_index = j; - } else { - m_mpq_lar_core_solver.m_column_types[j] = m_mpq_lar_core_solver.m_r_low_bounds()[j] < m_mpq_lar_core_solver.m_r_upper_bounds()[j]? column_type::boxed : column_type::fixed; - } - } - break; - case GT: - y_of_bound = 1; - case GE: - { - auto low = numeric_pair(right_side, y_of_bound); - if (low > m_mpq_lar_core_solver.m_r_low_bounds[j]) { - m_mpq_lar_core_solver.m_r_low_bounds[j] = low; - m_columns_with_changed_bound.insert(j); - set_low_bound_witness(j, ci); - } - } - break; - case EQ: - { - auto v = numeric_pair(right_side, zero_of_type()); - if (v < m_mpq_lar_core_solver.m_r_low_bounds[j]) { - m_status = INFEASIBLE; - m_infeasible_column_index = j; - set_upper_bound_witness(j, ci); - } else { - m_mpq_lar_core_solver.m_r_low_bounds[j] = m_mpq_lar_core_solver.m_r_upper_bounds[j] = v; - set_low_bound_witness(j, ci); - set_upper_bound_witness(j, ci); - m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed; - } - m_columns_with_changed_bound.insert(j); - break; - } - - default: - lean_unreachable(); - - } -} - -void update_fixed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { - lean_assert(m_status == INFEASIBLE || (m_mpq_lar_core_solver.m_column_types()[j] == column_type::fixed && m_mpq_lar_core_solver.m_r_low_bounds()[j] == m_mpq_lar_core_solver.m_r_upper_bounds()[j])); - lean_assert(m_status == INFEASIBLE || (m_mpq_lar_core_solver.m_r_low_bounds()[j].y.is_zero() && m_mpq_lar_core_solver.m_r_upper_bounds()[j].y.is_zero())); - auto v = numeric_pair(right_side, mpq(0)); - - mpq y_of_bound(0); - switch (kind) { - case LT: - if (v <= m_mpq_lar_core_solver.m_r_low_bounds[j]) { - m_status = INFEASIBLE; - m_infeasible_column_index = j; - set_upper_bound_witness(j, ci); - } - break; - case LE: - { - if (v < m_mpq_lar_core_solver.m_r_low_bounds[j]) { - m_status = INFEASIBLE; - m_infeasible_column_index = j; - set_upper_bound_witness(j, ci); - } - } - break; - case GT: - { - if (v >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) { - m_status = INFEASIBLE; - m_infeasible_column_index =j; - set_low_bound_witness(j, ci); - } - } - break; - case GE: - { - if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { - m_status = INFEASIBLE; - m_infeasible_column_index = j; - set_low_bound_witness(j, ci); - } - } - break; - case EQ: - { - if (v < m_mpq_lar_core_solver.m_r_low_bounds[j]) { - m_status = INFEASIBLE; - m_infeasible_column_index = j; - set_upper_bound_witness(j, ci); - } else if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { - m_status = INFEASIBLE; - m_infeasible_column_index = j; - set_low_bound_witness(j, ci); - } - break; - } - - default: - lean_unreachable(); - - } -} - diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp new file mode 100644 index 000000000..e617a1e29 --- /dev/null +++ b/src/util/lp/int_solver.cpp @@ -0,0 +1,606 @@ +/* + Copyright (c) 2017 Microsoft Corporation + Author: Lev Nachmanson +*/ + +#include "util/lp/int_solver.h" +#include "util/lp/lar_solver.h" +namespace lean { + +void int_solver::fix_non_base_columns() { + auto & lcs = m_lar_solver->m_mpq_lar_core_solver; + for (unsigned j : lcs.m_r_nbasis) { + if (column_is_int_inf(j)) { + set_value(j, floor(lcs.m_r_x[j].x)); + } + } + if (m_lar_solver->find_feasible_solution() == INFEASIBLE) + failed(); +} + +void int_solver::failed() { + auto & lcs = m_lar_solver->m_mpq_lar_core_solver; + + for (unsigned j : m_old_values_set.m_index) { + lcs.m_r_x[j] = m_old_values_data[j]; + lean_assert(lcs.m_r_solver.column_is_feasible(j)); + lcs.m_r_solver.remove_column_from_inf_set(j); + } + lean_assert(lcs.m_r_solver.calc_current_x_is_feasible_include_non_basis()); + lean_assert(lcs.m_r_solver.current_x_is_feasible()); + m_old_values_set.clear(); +} + +void int_solver::trace_inf_rows() const { + unsigned num = m_lar_solver->A_r().column_count(); + for (unsigned v = 0; v < num; v++) { + if (is_int(v) && !get_value(v).is_int()) { + display_column(tout, v); + } + } + + num = 0; + for (unsigned i = 0; i < m_lar_solver->A_r().row_count(); i++) { + unsigned j = m_lar_solver->m_mpq_lar_core_solver.m_r_basis[i]; + if (column_is_int_inf(j)) { + num++; + iterator_on_row it(m_lar_solver->A_r().m_rows[i]); + m_lar_solver->print_linear_iterator(&it, tout); + tout << "\n"; + } + } + tout << "num of int infeasible: " << num << "\n"; +} + +int int_solver::find_inf_int_base_column() { + if (m_inf_int_set.is_empty()) + return -1; + int j = find_inf_int_boxed_base_column_with_smallest_range(); + if (j != -1) + return j; + unsigned k = settings().random_next() % m_inf_int_set.m_index.size(); + return m_inf_int_set.m_index[k]; +} + +int int_solver::find_inf_int_boxed_base_column_with_smallest_range() { + int result = -1; + mpq range; + mpq new_range; + mpq small_range_thresold(1024); + unsigned n = 0; + lar_core_solver & lcs = m_lar_solver->m_mpq_lar_core_solver; + + for (int j : m_inf_int_set.m_index) { + lean_assert(is_base(j) && column_is_int_inf(j)); + if (!is_boxed(j)) + continue; + new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_low_bounds()[j].x; + if (new_range > small_range_thresold) + continue; + if (result == -1) { + result = j; + range = new_range; + n = 1; + continue; + } + if (new_range < range) { + n = 1; + result = j; + range = new_range; + continue; + } + if (new_range == range) { + n++; + if (settings().random_next() % n == 0) { + result = j; + continue; + } + } + } + return result; + +} + +lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) { + lean_assert(is_feasible()); + init_inf_int_set(); + lean_assert(inf_int_set_is_correct()); + // currently it is a reimplementation of + // final_check_status theory_arith::check_int_feasibility() + // from theory_arith_int.h + if (m_lar_solver->model_is_int_feasible()) + return lia_move::ok; + if (!gcd_test(ex)) + return lia_move::conflict; + /* + if (m_params.m_arith_euclidean_solver) + apply_euclidean_solver(); + + */ + m_lar_solver->pivot_fixed_vars_from_basis(); + patch_int_infeasible_columns(); + fix_non_base_columns(); + lean_assert(is_feasible()); + TRACE("arith_int_rows", trace_inf_rows();); + + if (find_inf_int_base_column() == -1) + return lia_move::ok; + + + if ((++m_branch_cut_counter) % settings().m_int_branch_cut_threshold == 0) { + move_non_base_vars_to_bounds(); + /* + if (!make_feasible()) { + TRACE("arith_int", tout << "failed to move variables to bounds.\n";); + failed(); + return FC_CONTINUE; + } + int int_var = find_inf_int_base_var(); + if (int_var != null_int) { + TRACE("arith_int", tout << "v" << int_var << " does not have an integer assignment: " << get_value(int_var) << "\n";); + SASSERT(is_base(int_var)); + row const & r = m_rows[get_var_row(int_var)]; + if (!mk_gomory_cut(r)) { + // silent failure + } + return FC_CONTINUE; + }*/ + } + else { + int j = find_inf_int_base_column(); + /* + if (j != -1) { + TRACE("arith_int", tout << "v" << j << " does not have an integer assignment: " << get_value(j) << "\n";); + // apply branching + branch_infeasible_int_var(int_var); + return false; + }*/ + } + // return true; + return lia_move::give_up; +} + +void int_solver::move_non_base_vars_to_bounds() { + auto & lcs = m_lar_solver->m_mpq_lar_core_solver; + for (unsigned j : lcs.m_r_nbasis) { + auto & val = lcs.m_r_x[j]; + switch (lcs.m_column_types()[j]) { + case column_type::boxed: + if (val != lcs.m_r_low_bounds()[j] && val != lcs.m_r_upper_bounds()[j]) + set_value(j, lcs.m_r_low_bounds()[j]); + break; + case column_type::low_bound: + if (val != lcs.m_r_low_bounds()[j]) + set_value(j, lcs.m_r_low_bounds()[j]); + break; + case column_type::upper_bound: + if (val != lcs.m_r_upper_bounds()[j]) + set_value(j, lcs.m_r_upper_bounds()[j]); + break; + default: + if (is_int(j) && !val.is_int()) { + set_value(j, impq(floor(val))); + } + } + } +} + + + +void int_solver::set_value(unsigned j, const impq & new_val) { + auto & x = m_lar_solver->m_mpq_lar_core_solver.m_r_x[j]; + if (!m_old_values_set.contains(j)) { + m_old_values_set.insert(j); + m_old_values_data[j] = x; + } + auto delta = new_val - x; + x = new_val; + m_lar_solver->change_basic_x_by_delta_on_column(j, delta); + update_column_in_inf_set_set(j); +} + +void int_solver::patch_int_infeasible_columns() { + bool inf_l, inf_u; + impq l, u; + mpq m; + auto & lcs = m_lar_solver->m_mpq_lar_core_solver; + for (unsigned j : lcs.m_r_nbasis) { + if (!is_int(j)) + continue; + get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m); + impq & val = lcs.m_r_x[j]; + bool val_is_int = val.is_int(); + bool m_is_one = m.is_one(); + if (m.is_one() && val_is_int) + continue; + // check whether value of j is already a multiple of m. + if (val_is_int && (val.x / m).is_int()) + continue; + TRACE("patch_int", + tout << "TARGET j" << j << " -> ["; + if (inf_l) tout << "-oo"; else tout << l; + tout << ", "; + if (inf_u) tout << "oo"; else tout << u; + tout << "]"; + tout << ", m: " << m << ", val: " << val << ", is_int: " << m_lar_solver->column_is_int(j) << "\n";); + if (!inf_l) { + l = m_is_one? ceil(l) : m * ceil(l / m); + if (inf_u || l <= u) { + TRACE("patch_int", + tout << "patching with l: " << l << '\n';); + + set_value(j, l); + } else { + TRACE("patch_int", + tout << "not patching " << l << "\n";); + } + } else if (!inf_u) { + u = m_is_one? floor(u) : m * floor(u / m); + set_value(j, u); + TRACE("patch_int", + tout << "patching with u: " << u << '\n';); + } else { + set_value(j, impq(0)); + TRACE("patch_int", + tout << "patching with 0\n";); + } + } +} + +mpq get_denominators_lcm(iterator_on_row &it) { + mpq r(1); + mpq a; + unsigned j; + while (it.next(a, j)) { + r = lcm(r, denominator(a)); + } + return r; +} + +bool int_solver::gcd_test_for_row(static_matrix> & A, unsigned i, explanation & ex) { + iterator_on_row it(A.m_rows[i]); + std::cout << "gcd_test_for_row(" << i << ")\n"; + mpq lcm_den = get_denominators_lcm(it); + mpq consts(0); + mpq gcds(0); + mpq least_coeff(0); + bool least_coeff_is_bounded = false; + mpq a; + unsigned j; + while (it.next(a, j)) { + if (m_lar_solver->column_is_fixed(j)) { + mpq aux = lcm_den * a; + consts += aux * m_lar_solver->column_low_bound(j).x; + } + else if (m_lar_solver->column_is_real(j)) { + return true; + } + else if (gcds.is_zero()) { + gcds = abs(lcm_den * a); + least_coeff = gcds; + least_coeff_is_bounded = m_lar_solver->column_is_bounded(j); + } + else { + mpq aux = abs(lcm_den * a); + gcds = gcd(gcds, aux); + if (aux < least_coeff) { + least_coeff = aux; + least_coeff_is_bounded = m_lar_solver->column_is_bounded(j); + } + else if (least_coeff_is_bounded && aux == least_coeff) { + least_coeff_is_bounded = m_lar_solver->column_is_bounded(j); + } + } + SASSERT(gcds.is_int()); + SASSERT(least_coeff.is_int()); + TRACE("gcd_test_bug", tout << "coeff: " << a << ", gcds: " << gcds + << " least_coeff: " << least_coeff << " consts: " << consts << "\n";); + + } + + if (gcds.is_zero()) { + // All variables are fixed. + // This theory guarantees that the assignment satisfies each row, and + // fixed integer variables are assigned to integer values. + return true; + } + + if (!(consts / gcds).is_int()) + fill_explanation_from_fixed_columns(it, ex); + + if (least_coeff.is_one() && !least_coeff_is_bounded) { + SASSERT(gcds.is_one()); + return true; + } + + if (least_coeff_is_bounded) { + return ext_gcd_test(it, least_coeff, lcm_den, consts, ex); + } + return true; +} + +void int_solver::add_to_explanation_from_fixed_or_boxed_column(unsigned j, explanation & ex) { + constraint_index lc, uc; + m_lar_solver->get_bound_constraint_witnesses_for_column(j, lc, uc); + ex.m_explanation.push_back(std::make_pair(mpq(1), lc)); + ex.m_explanation.push_back(std::make_pair(mpq(1), uc)); +} +void int_solver::fill_explanation_from_fixed_columns(iterator_on_row & it, explanation & ex) { + it.reset(); + unsigned j; + while (it.next(j)) { + if (!m_lar_solver->column_is_fixed(j)) + continue; + add_to_explanation_from_fixed_or_boxed_column(j, ex); + } +} + +bool int_solver::gcd_test(explanation & ex) { + auto & A = m_lar_solver->A_r(); // getting the matrix + for (unsigned i = 0; i < A.row_count(); i++) + if (!gcd_test_for_row(A, i, ex)) { + std::cout << "false from gcd_test\n" ; + return false; + } + + return true; +} + +bool int_solver::ext_gcd_test(iterator_on_row & it, + mpq const & least_coeff, + mpq const & lcm_den, + mpq const & consts, explanation& ex) { + + std::cout << "calling ext_gcd_test" << std::endl; + mpq gcds(0); + mpq l(consts); + mpq u(consts); + + it.reset(); + mpq a; + unsigned j; + while (it.next(a, j)) { + if (m_lar_solver->column_is_fixed(j)) + continue; + SASSERT(!m_lar_solver->column_is_real(j)); + mpq ncoeff = lcm_den * a; + SASSERT(ncoeff.is_int()); + mpq abs_ncoeff = abs(ncoeff); + if (abs_ncoeff == least_coeff) { + SASSERT(m_lar_solver->column_is_bounded(j)); + if (ncoeff.is_pos()) { + // l += ncoeff * m_lar_solver->column_low_bound(j).x; + l.addmul(ncoeff, m_lar_solver->column_low_bound(j).x); + // u += ncoeff * m_lar_solver->column_upper_bound(j).x; + u.addmul(ncoeff, m_lar_solver->column_upper_bound(j).x); + } + else { + // l += ncoeff * upper_bound(j).get_rational(); + l.addmul(ncoeff, m_lar_solver->column_upper_bound(j).x); + // u += ncoeff * lower_bound(j).get_rational(); + u.addmul(ncoeff, m_lar_solver->column_low_bound(j).x); + } + add_to_explanation_from_fixed_or_boxed_column(j, ex); + } + else if (gcds.is_zero()) { + gcds = abs_ncoeff; + } + else { + gcds = gcd(gcds, abs_ncoeff); + } + SASSERT(gcds.is_int()); + } + + if (gcds.is_zero()) { + return true; + } + + mpq l1 = ceil(l/gcds); + mpq u1 = floor(u/gcds); + + if (u1 < l1) { + fill_explanation_from_fixed_columns(it, ex); + return false; + } + + return true; + +} + +linear_combination_iterator * int_solver::get_column_iterator(unsigned j) { + if (m_lar_solver->use_tableau()) + return new iterator_on_column(m_lar_solver->A_r().m_columns[j], m_lar_solver->A_r()); + return new iterator_on_indexed_vector(m_lar_solver->get_column_in_lu_mode(j)); +} + + +int_solver::int_solver(lar_solver* lar_slv) : + m_lar_solver(lar_slv), + m_branch_cut_counter(0) { + lean_assert(m_old_values_set.size() == 0); + m_old_values_set.resize(lar_slv->A_r().column_count()); + m_old_values_data.resize(lar_slv->A_r().column_count(), zero_of_type()); +} + +bool int_solver::lower(unsigned j) const { + switch (m_lar_solver->m_mpq_lar_core_solver.m_column_types()[j]) { + case column_type::fixed: + case column_type::boxed: + case column_type::low_bound: + return true; + default: + return false; + } +} + +bool int_solver::upper(unsigned j) const { + switch (m_lar_solver->m_mpq_lar_core_solver.m_column_types()[j]) { + case column_type::fixed: + case column_type::boxed: + case column_type::upper_bound: + return true; + default: + return false; + } +} + +const impq& int_solver::lower_bound(unsigned j) const { + return m_lar_solver->m_mpq_lar_core_solver.m_r_low_bounds()[j]; +} + +const impq& int_solver::upper_bound(unsigned j) const { + return m_lar_solver->m_mpq_lar_core_solver.m_r_upper_bounds()[j]; +} + + +void set_lower(impq & l, + bool & inf_l, + impq const & v ) { + if (inf_l || v > l) { + l = v; + inf_l = false; + } +} + +void set_upper(impq & u, + bool & inf_u, + impq const & v) { + if (inf_u || v < u) { + u = v; + inf_u = false; + } +} + +bool int_solver::get_freedom_interval_for_column(unsigned x_j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) { + auto & lcs = m_lar_solver->m_mpq_lar_core_solver; + if (lcs.m_r_heading[x_j] >= 0) // the basic var + return false; + + impq const & x_j_val = lcs.m_r_x[x_j]; + linear_combination_iterator *it = get_column_iterator(x_j); + + inf_l = true; + inf_u = true; + l = u = zero_of_type(); + m = mpq(1); + + if (lower(x_j)) { + set_lower(l, inf_l, lower_bound(x_j)); + } + if (upper(x_j)) { + set_upper(u, inf_u, upper_bound(x_j)); + } + + mpq a_ij; unsigned i; + while (it->next(a_ij, i)) { + unsigned x_i = lcs.m_r_basis[i]; + impq const & x_i_val = lcs.m_r_x[x_i]; + if (is_int(x_i) && is_int(x_j) && !a_ij.is_int()) + m = lcm(m, denominator(a_ij)); + bool x_i_lower = lower(x_i); + bool x_i_upper = upper(x_i); + if (a_ij.is_neg()) { + if (x_i_lower) { + impq new_l = x_j_val + ((x_i_val - lcs.m_r_low_bounds()[x_i]) / a_ij); + set_lower(l, inf_l, new_l); + if (!inf_l && !inf_u && l == u) break;; + } + if (x_i_upper) { + impq new_u = x_j_val + ((x_i_val - lcs.m_r_upper_bounds()[x_i]) / a_ij); + set_upper(u, inf_u, new_u); + if (!inf_l && !inf_u && l == u) break;; + } + } + else { + if (x_i_upper) { + impq new_l = x_j_val + ((x_i_val - lcs.m_r_upper_bounds()[x_i]) / a_ij); + set_lower(l, inf_u, new_l); + if (!inf_l && !inf_u && l == u) break;; + } + if (x_i_lower) { + impq new_u = x_j_val + ((x_i_val - lcs.m_r_low_bounds()[x_i]) / a_ij); + set_upper(u, inf_u, new_u); + if (!inf_l && !inf_u && l == u) break;; + } + } + } + + delete it; + TRACE("freedom_interval", + tout << "freedom variable for:\n"; + tout << m_lar_solver->get_column_name(x_j); + tout << "["; + if (inf_l) tout << "-oo"; else tout << l; + tout << "; "; + if (inf_u) tout << "oo"; else tout << u; + tout << "]\n";); + return true; + +} + +bool int_solver::is_int(unsigned j) const { + return m_lar_solver->column_is_int(j); +} + +bool int_solver::value_is_int(unsigned j) const { + return m_lar_solver->m_mpq_lar_core_solver.m_r_x[j].is_int(); +} + + + +bool int_solver::is_feasible() const { + auto & lcs = m_lar_solver->m_mpq_lar_core_solver; + lean_assert( + lcs.m_r_solver.calc_current_x_is_feasible_include_non_basis() == + lcs.m_r_solver.current_x_is_feasible()); + return lcs.m_r_solver.current_x_is_feasible(); +} +const impq & int_solver::get_value(unsigned j) const { + return m_lar_solver->m_mpq_lar_core_solver.m_r_x[j]; +} + +void int_solver::display_column(std::ostream & out, unsigned j) const { + m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out); +} + +bool int_solver::inf_int_set_is_correct() const { + for (unsigned j = 0; j < m_lar_solver->A_r().column_count(); j++) { + if (m_inf_int_set.contains(j) != is_int(j) && (!value_is_int(j))) + return false; + } + return true; +} + +bool int_solver::column_is_int_inf(unsigned j) const { + return is_int(j) && (!value_is_int(j)); +} + +void int_solver::init_inf_int_set() { + m_inf_int_set.clear(); + m_inf_int_set.resize(m_lar_solver->A_r().column_count()); + for (unsigned j : m_lar_solver->m_mpq_lar_core_solver.m_r_basis) { + if (column_is_int_inf(j)) + m_inf_int_set.insert(j); + } +} + +void int_solver::update_column_in_inf_set_set(unsigned j) { + if (is_int(j) && (!value_is_int(j))) + m_inf_int_set.insert(j); + else + m_inf_int_set.erase(j); +} + +bool int_solver::is_base(unsigned j) const { + return m_lar_solver->m_mpq_lar_core_solver.m_r_heading[j] >= 0; +} + +bool int_solver::is_boxed(unsigned j) const { + return m_lar_solver->m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed; +} + +lp_settings& int_solver::settings() { + return m_lar_solver->settings(); +} + +} diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h new file mode 100644 index 000000000..981127bc8 --- /dev/null +++ b/src/util/lp/int_solver.h @@ -0,0 +1,100 @@ +/* + Copyright (c) 2017 Microsoft Corporation + Author: Lev Nachmanson +*/ +#pragma once +#include "util/lp/lp_settings.h" +#include "util/lp/static_matrix.h" +#include "util/lp/iterator_on_row.h" +#include "util/lp/int_set.h" +#include "util/lp/lar_term.h" + +namespace lean { +class lar_solver; +template +struct lp_constraint; +enum class lia_move { + ok, + branch, + cut, + conflict, + give_up +}; + +struct explanation { + vector> m_explanation; +}; + +class int_solver { +public: + // fields + lar_solver *m_lar_solver; + int_set m_old_values_set; + vector m_old_values_data; + int_set m_inf_int_set; + unsigned m_branch_cut_counter; + // methods + int_solver(lar_solver* lp); + // main function to check that solution provided by lar_solver is valid for integral values, + // or provide a way of how it can be adjusted. + lia_move check(lar_term& t, mpq& k, explanation& ex); +private: + + // how to tighten bounds for integer variables. + + bool gcd_test_for_row(static_matrix> & A, unsigned i, explanation &); + + // gcd test + // 5*x + 3*y + 6*z = 5 + // suppose x is fixed at 2. + // so we have 10 + 3(y + 2z) = 5 + // 5 = -3(y + 2z) + // this is unsolvable because 5/3 is not an integer. + // so we create a lemma that rules out this condition. + // + bool gcd_test(explanation & ); // returns false in case of failure. Creates a theory lemma in case of failure. + + // create goromy cuts + // either creates a conflict or a bound. + + // branch and bound: + // decide what to branch and bound on + // creates a fresh inequality. + + bool branch(const lp_constraint & new_inequality); + bool ext_gcd_test(iterator_on_row & it, + mpq const & least_coeff, + mpq const & lcm_den, + mpq const & consts, + explanation & ex); + void fill_explanation_from_fixed_columns(iterator_on_row & it, explanation &); + void add_to_explanation_from_fixed_or_boxed_column(unsigned j, explanation &); + void remove_fixed_vars_from_base(); + void patch_int_infeasible_columns(); + bool get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m); + linear_combination_iterator * get_column_iterator(unsigned j); + bool lower(unsigned j) const; + bool upper(unsigned j) const; + const impq & lower_bound(unsigned j) const; + const impq & upper_bound(unsigned j) const; + bool is_int(unsigned j) const; + bool is_base(unsigned j) const; + bool is_boxed(unsigned j) const; + bool value_is_int(unsigned j) const; + void set_value(unsigned j, const impq & new_val); + void fix_non_base_columns(); + void failed(); + bool is_feasible() const; + const impq & get_value(unsigned j) const; + void display_column(std::ostream & out, unsigned j) const; + bool inf_int_set_is_correct() const; + void init_inf_int_set(); + void update_column_in_inf_set_set(unsigned j); + bool column_is_int_inf(unsigned j) const; + void trace_inf_rows() const; + int find_inf_int_base_column(); + int find_inf_int_boxed_base_column_with_smallest_range(); + lp_settings& settings(); + void move_non_base_vars_to_bounds(); +}; +} diff --git a/src/util/lp/lar_core_solver.h b/src/util/lp/lar_core_solver.h index 71d69c3a4..44a6349a7 100644 --- a/src/util/lp/lar_core_solver.h +++ b/src/util/lp/lar_core_solver.h @@ -796,6 +796,37 @@ public: return new iterator_on_indexed_vector(m_r_solver.m_ed); } } + + bool column_is_fixed(unsigned j) const { + return m_column_types()[j] == column_type::fixed || + ( m_column_types()[j] == column_type::boxed && + m_r_solver.m_low_bounds[j] == m_r_solver.m_upper_bounds[j]); + } + + const impq & low_bound(unsigned j) const { + lean_assert(m_column_types()[j] == column_type::fixed || + m_column_types()[j] == column_type::boxed || + m_column_types()[j] == column_type::low_bound); + return m_r_low_bounds[j]; + } + + const impq & upper_bound(unsigned j) const { + lean_assert(m_column_types()[j] == column_type::fixed || + m_column_types()[j] == column_type::boxed || + m_column_types()[j] == column_type::upper_bound); + return m_r_upper_bounds[j]; + } + + const bool column_is_bounded(unsigned j) const { + switch(m_column_types()[j]) { + case column_type::fixed: + case column_type::boxed: + return true; + default: + return false; + } + } + }; } diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp new file mode 100644 index 000000000..def72734c --- /dev/null +++ b/src/util/lp/lar_solver.cpp @@ -0,0 +1,2040 @@ +#include "util/lp/lar_solver.h" +/* + Copyright (c) 2017 Microsoft Corporation + Author: Lev Nachmanson +*/ + +namespace lean { + +unsigned lar_solver::constraint_count() const { + return m_constraints.size(); +} +const lar_base_constraint& lar_solver::get_constraint(unsigned ci) const { + return *(m_constraints[ci]); +} + +////////////////// methods //////////////////////////////// +static_matrix> & lar_solver::A_r() { return m_mpq_lar_core_solver.m_r_A;} +static_matrix> const & lar_solver::A_r() const { return m_mpq_lar_core_solver.m_r_A;} +static_matrix & lar_solver::A_d() { return m_mpq_lar_core_solver.m_d_A;} +static_matrix const & lar_solver::A_d() const { return m_mpq_lar_core_solver.m_d_A;} + +lp_settings & lar_solver::settings() { return m_settings;} + +lp_settings const & lar_solver::settings() const { return m_settings;} + +void clear() {lean_assert(false); // not implemented +} + + +lar_solver::lar_solver() : m_status(OPTIMAL), + m_infeasible_column_index(-1), + m_terms_start_index(1000000), + m_mpq_lar_core_solver(m_settings, *this) +{ +} + +void lar_solver::set_propagate_bounds_on_pivoted_rows_mode(bool v) { + m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows = v? (& m_rows_with_changed_bounds) : nullptr; +} + +lar_solver::~lar_solver(){ + for (auto c : m_constraints) + delete c; + for (auto t : m_terms) + delete t; +} + +numeric_pair const& lar_solver::get_value(var_index vi) const { return m_mpq_lar_core_solver.m_r_x[vi]; } + +bool lar_solver::is_term(var_index j) const { + return j >= m_terms_start_index && j - m_terms_start_index < m_terms.size(); +} + +unsigned lar_solver::adjust_term_index(unsigned j) const { + lean_assert(is_term(j)); + return j - m_terms_start_index; +} + + +bool lar_solver::use_lu() const { return m_settings.simplex_strategy() == simplex_strategy_enum::lu; } + +bool lar_solver::sizes_are_correct() const { + lean_assert(strategy_is_undecided() || !m_mpq_lar_core_solver.need_to_presolve_with_double_solver() || A_r().column_count() == A_d().column_count()); + lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_column_types.size()); + lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); + lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_x.size()); + return true; +} + + +void lar_solver::print_implied_bound(const implied_bound& be, std::ostream & out) const { + out << "implied bound\n"; + unsigned v = be.m_j; + if (is_term(v)) { + out << "it is a term number " << be.m_j << std::endl; + print_term(*m_terms[be.m_j - m_terms_start_index], out); + } + else { + out << get_column_name(v); + } + out << " " << lconstraint_kind_string(be.kind()) << " " << be.m_bound << std::endl; + // for (auto & p : be.m_explanation) { + // out << p.first << " : "; + // print_constraint(p.second, out); + // } + + // m_mpq_lar_core_solver.m_r_solver.print_column_info(be.m_j< m_terms_start_index? be.m_j : adjust_term_index(be.m_j), out); + out << "end of implied bound" << std::endl; +} + +bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be, const vector> & explanation) const { + std::unordered_map coeff_map; + auto rs_of_evidence = zero_of_type(); + unsigned n_of_G = 0, n_of_L = 0; + bool strict = false; + for (auto & it : explanation) { + mpq coeff = it.first; + constraint_index con_ind = it.second; + const auto & constr = *m_constraints[con_ind]; + lconstraint_kind kind = coeff.is_pos() ? constr.m_kind : flip_kind(constr.m_kind); + register_in_map(coeff_map, constr, coeff); + if (kind == GT || kind == LT) + strict = true; + if (kind == GE || kind == GT) n_of_G++; + else if (kind == LE || kind == LT) n_of_L++; + rs_of_evidence += coeff*constr.m_right_side; + } + lean_assert(n_of_G == 0 || n_of_L == 0); + lconstraint_kind kind = n_of_G ? GE : (n_of_L ? LE : EQ); + if (strict) + kind = static_cast((static_cast(kind) / 2)); + + if (!is_term(be.m_j)) { + if (coeff_map.size() != 1) + return false; + auto it = coeff_map.find(be.m_j); + if (it == coeff_map.end()) return false; + mpq ratio = it->second; + if (ratio < zero_of_type()) { + kind = static_cast(-kind); + } + rs_of_evidence /= ratio; + } else { + const lar_term * t = m_terms[adjust_term_index(be.m_j)]; + const auto first_coeff = *t->m_coeffs.begin(); + unsigned j = first_coeff.first; + auto it = coeff_map.find(j); + if (it == coeff_map.end()) + return false; + mpq ratio = it->second / first_coeff.second; + for (auto & p : t->m_coeffs) { + it = coeff_map.find(p.first); + if (it == coeff_map.end()) + return false; + if (p.second * ratio != it->second) + return false; + } + if (ratio < zero_of_type()) { + kind = static_cast(-kind); + } + rs_of_evidence /= ratio; + rs_of_evidence += t->m_v * ratio; + } + + return kind == be.kind() && rs_of_evidence == be.m_bound; +} + + +void lar_solver::analyze_new_bounds_on_row( + unsigned row_index, + bound_propagator & bp) { + lean_assert(!use_tableau()); + iterator_on_pivot_row it(m_mpq_lar_core_solver.get_pivot_row(), m_mpq_lar_core_solver.m_r_basis[row_index]); + + bound_analyzer_on_row ra_pos(it, + zero_of_type>(), + row_index, + bp + ); + ra_pos.analyze(); +} + +void lar_solver::analyze_new_bounds_on_row_tableau( + unsigned row_index, + bound_propagator & bp + ) { + + if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation) + return; + iterator_on_row it(A_r().m_rows[row_index]); + lean_assert(use_tableau()); + bound_analyzer_on_row::analyze_row(it, + zero_of_type>(), + row_index, + bp + ); +} + + +void lar_solver::substitute_basis_var_in_terms_for_row(unsigned i) { + // todo : create a map from term basic vars to the rows where they are used + unsigned basis_j = m_mpq_lar_core_solver.m_r_solver.m_basis[i]; + for (unsigned k = 0; k < m_terms.size(); k++) { + if (term_is_used_as_row(k)) + continue; + if (!m_terms[k]->contains(basis_j)) + continue; + m_terms[k]->subst(basis_j, m_mpq_lar_core_solver.m_r_solver.m_pivot_row); + } +} + +void lar_solver::calculate_implied_bounds_for_row(unsigned i, bound_propagator & bp) { + if(use_tableau()) { + analyze_new_bounds_on_row_tableau(i, bp); + } else { + m_mpq_lar_core_solver.calculate_pivot_row(i); + substitute_basis_var_in_terms_for_row(i); + analyze_new_bounds_on_row(i, bp); + } +} + + +linear_combination_iterator * lar_solver::create_new_iter_from_term(unsigned term_index) const { + lean_assert(false); // not implemented + return nullptr; + // new linear_combination_iterator_on_vector(m_terms[adjust_term_index(term_index)]->coeffs_as_vector()); +} + +unsigned lar_solver::adjust_column_index_to_term_index(unsigned j) const { + unsigned ext_var_or_term = m_columns_to_ext_vars_or_term_indices[j]; + return ext_var_or_term < m_terms_start_index ? j : ext_var_or_term; +} + +void lar_solver::propagate_bounds_on_a_term(const lar_term& t, bound_propagator & bp, unsigned term_offset) { + lean_assert(false); // not implemented +} + + +void lar_solver::explain_implied_bound(implied_bound & ib, bound_propagator & bp) { + unsigned i = ib.m_row_or_term_index; + int bound_sign = ib.m_is_low_bound? 1: -1; + int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign; + unsigned m_j = ib.m_j; + if (is_term(m_j)) { + auto it = m_ext_vars_to_columns.find(m_j); + lean_assert(it != m_ext_vars_to_columns.end()); + m_j = it->second.ext_j(); + } + for (auto const& r : A_r().m_rows[i]) { + unsigned j = r.m_j; + mpq const& a = r.get_val(); + if (j == m_j) continue; + if (is_term(j)) { + auto it = m_ext_vars_to_columns.find(j); + lean_assert(it != m_ext_vars_to_columns.end()); + j = it->second.ext_j(); + } + int a_sign = is_pos(a)? 1: -1; + int sign = j_sign * a_sign; + const ul_pair & ul = m_vars_to_ul_pairs[j]; + auto witness = sign > 0? ul.upper_bound_witness(): ul.low_bound_witness(); + lean_assert(is_valid(witness)); + bp.consume(a, witness); + } + // lean_assert(implied_bound_is_correctly_explained(ib, explanation)); +} + + +bool lar_solver::term_is_used_as_row(unsigned term) const { + lean_assert(is_term(term)); + return contains(m_ext_vars_to_columns, term); +} + +void lar_solver::propagate_bounds_on_terms(bound_propagator & bp) { + for (unsigned i = 0; i < m_terms.size(); i++) { + if (term_is_used_as_row(i + m_terms_start_index)) + 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); + } +} + + +// goes over touched rows and tries to induce bounds +void lar_solver::propagate_bounds_for_touched_rows(bound_propagator & bp) { + if (!use_tableau()) + return; // todo: consider to remove the restriction + + for (unsigned i : m_rows_with_changed_bounds.m_index) { + calculate_implied_bounds_for_row(i, bp); + } + m_rows_with_changed_bounds.clear(); + if (!use_tableau()) { + propagate_bounds_on_terms(bp); + } +} + +lp_status lar_solver::get_status() const { return m_status;} + +void lar_solver::set_status(lp_status s) {m_status = s;} + +lp_status lar_solver::find_feasible_solution() { + m_settings.st().m_make_feasible++; + if (A_r().column_count() > m_settings.st().m_max_cols) + m_settings.st().m_max_cols = A_r().column_count(); + if (A_r().row_count() > m_settings.st().m_max_rows) + m_settings.st().m_max_rows = A_r().row_count(); + if (strategy_is_undecided()) + decide_on_strategy_and_adjust_initial_state(); + + m_mpq_lar_core_solver.m_r_solver.m_look_for_feasible_solution_only = true; + return solve(); +} + +lp_status lar_solver::solve() { + if (m_status == INFEASIBLE) { + return m_status; + } + solve_with_core_solver(); + if (m_status != INFEASIBLE) { + if (m_settings.bound_propagation()) + detect_rows_with_changed_bounds(); + } + + m_columns_with_changed_bound.clear(); + return m_status; +} + +void lar_solver::fill_explanation_from_infeasible_column(vector> & evidence) const{ + + // this is the case when the lower bound is in conflict with the upper one + const ul_pair & ul = m_vars_to_ul_pairs[m_infeasible_column_index]; + evidence.push_back(std::make_pair(numeric_traits::one(), ul.upper_bound_witness())); + evidence.push_back(std::make_pair(-numeric_traits::one(), ul.low_bound_witness())); +} + + +unsigned lar_solver::get_total_iterations() const { return m_mpq_lar_core_solver.m_r_solver.total_iterations(); } +// see http://research.microsoft.com/projects/z3/smt07.pdf +// This method searches for a feasible solution with as many different values of variables, reverenced in vars, as it can find +// Attention, after a call to this method the non-basic variables don't necesserarly stick to their bounds anymore +vector lar_solver::get_list_of_all_var_indices() const { + vector ret; + for (unsigned j = 0; j < m_mpq_lar_core_solver.m_r_heading.size(); j++) + ret.push_back(j); + return ret; +} +void lar_solver::push() { + m_simplex_strategy = m_settings.simplex_strategy(); + m_simplex_strategy.push(); + m_status.push(); + m_vars_to_ul_pairs.push(); + m_infeasible_column_index.push(); + m_mpq_lar_core_solver.push(); + m_term_count = m_terms.size(); + m_term_count.push(); + m_constraint_count = m_constraints.size(); + m_constraint_count.push(); +} + +void lar_solver::clean_large_elements_after_pop(unsigned n, int_set& set) { + vector to_remove; + for (unsigned j: set.m_index) + if (j >= n) + to_remove.push_back(j); + for (unsigned j : to_remove) + set.erase(j); +} + +void lar_solver::shrink_inf_set_after_pop(unsigned n, int_set & set) { + clean_large_elements_after_pop(n, set); + set.resize(n); +} + + +void lar_solver::pop(unsigned k) { + int n_was = static_cast(m_ext_vars_to_columns.size()); + m_status.pop(k); + m_infeasible_column_index.pop(k); + unsigned n = m_vars_to_ul_pairs.peek_size(k); + for (unsigned j = n_was; j-- > n;) + m_ext_vars_to_columns.erase(m_columns_to_ext_vars_or_term_indices[j]); + m_columns_to_ext_vars_or_term_indices.resize(n); + if (m_settings.use_tableau()) { + pop_tableau(); + } + m_vars_to_ul_pairs.pop(k); + + m_mpq_lar_core_solver.pop(k); + clean_large_elements_after_pop(n, m_columns_with_changed_bound); + unsigned m = A_r().row_count(); + clean_large_elements_after_pop(m, m_rows_with_changed_bounds); + clean_inf_set_of_r_solver_after_pop(); + lean_assert(m_settings.simplex_strategy() == simplex_strategy_enum::undecided || + (!use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); + + + lean_assert(ax_is_correct()); + lean_assert(m_mpq_lar_core_solver.m_r_solver.inf_set_is_correct()); + m_constraint_count.pop(k); + for (unsigned i = m_constraint_count; i < m_constraints.size(); i++) + delete m_constraints[i]; + + m_constraints.resize(m_constraint_count); + m_term_count.pop(k); + for (unsigned i = m_term_count; i < m_terms.size(); i++) { + delete m_terms[i]; + } + m_terms.resize(m_term_count); + m_simplex_strategy.pop(k); + m_settings.simplex_strategy() = m_simplex_strategy; + lean_assert(sizes_are_correct()); + lean_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); +} + +vector lar_solver::get_all_constraint_indices() const { + vector ret; + constraint_index i = 0; + while ( i < m_constraints.size()) + ret.push_back(i++); + return ret; +} + +bool lar_solver::maximize_term_on_tableau(const vector> & term, + impq &term_max) { + if (settings().simplex_strategy() == simplex_strategy_enum::undecided) + decide_on_strategy_and_adjust_initial_state(); + + m_mpq_lar_core_solver.solve(); + if (m_mpq_lar_core_solver.m_r_solver.get_status() == UNBOUNDED) + return false; + + term_max = 0; + for (auto & p : term) + term_max += p.first * m_mpq_lar_core_solver.m_r_x[p.second]; + + return true; +} + +bool lar_solver::costs_are_zeros_for_r_solver() const { + for (unsigned j = 0; j < m_mpq_lar_core_solver.m_r_solver.m_costs.size(); j++) { + lean_assert(is_zero(m_mpq_lar_core_solver.m_r_solver.m_costs[j])); + } + return true; +} +bool lar_solver::reduced_costs_are_zeroes_for_r_solver() const { + for (unsigned j = 0; j < m_mpq_lar_core_solver.m_r_solver.m_d.size(); j++) { + lean_assert(is_zero(m_mpq_lar_core_solver.m_r_solver.m_d[j])); + } + return true; +} + +void lar_solver::set_costs_to_zero(const vector> & term) { + auto & rslv = m_mpq_lar_core_solver.m_r_solver; + auto & jset = m_mpq_lar_core_solver.m_r_solver.m_inf_set; // hijack this set that should be empty right now + lean_assert(jset.m_index.size()==0); + + for (auto & p : term) { + unsigned j = p.second; + rslv.m_costs[j] = zero_of_type(); + int i = rslv.m_basis_heading[j]; + if (i < 0) + jset.insert(j); + else { + for (auto & rc : A_r().m_rows[i]) + jset.insert(rc.m_j); + } + } + + for (unsigned j : jset.m_index) + rslv.m_d[j] = zero_of_type(); + + jset.clear(); + + lean_assert(reduced_costs_are_zeroes_for_r_solver()); + lean_assert(costs_are_zeros_for_r_solver()); +} + +void lar_solver::prepare_costs_for_r_solver(const vector> & term) { + + auto & rslv = m_mpq_lar_core_solver.m_r_solver; + rslv.m_using_infeas_costs = false; + lean_assert(costs_are_zeros_for_r_solver()); + lean_assert(reduced_costs_are_zeroes_for_r_solver()); + rslv.m_costs.resize(A_r().column_count(), zero_of_type()); + for (auto & p : term) { + unsigned j = p.second; + rslv.m_costs[j] = p.first; + if (rslv.m_basis_heading[j] < 0) + rslv.m_d[j] += p.first; + else + rslv.update_reduced_cost_for_basic_column_cost_change(- p.first, j); + } + lean_assert(rslv.reduced_costs_are_correct_tableau()); +} + +bool lar_solver::maximize_term_on_corrected_r_solver(const vector> & term, + impq &term_max) { + settings().backup_costs = 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(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(OPTIMAL); + return ret; + } + + case simplex_strategy_enum::lu: + lean_assert(false); // not implemented + return false; + default: + lean_unreachable(); // wrong mode + } + return false; +} +// starting from a given feasible state look for the maximum of the term +// return true if found and false if unbounded +bool lar_solver::maximize_term(const vector> & term, + impq &term_max) { + lean_assert(m_mpq_lar_core_solver.m_r_solver.current_x_is_feasible()); + m_mpq_lar_core_solver.m_r_solver.m_look_for_feasible_solution_only = false; + return maximize_term_on_corrected_r_solver(term, term_max); +} + + + +const lar_term & lar_solver::get_term(unsigned j) const { + lean_assert(j >= m_terms_start_index); + return *m_terms[j - m_terms_start_index]; +} + +void lar_solver::pop_core_solver_params() { + pop_core_solver_params(1); +} + +void lar_solver::pop_core_solver_params(unsigned k) { + A_r().pop(k); + A_d().pop(k); +} + + +void lar_solver::set_upper_bound_witness(var_index j, constraint_index ci) { + ul_pair ul = m_vars_to_ul_pairs[j]; + ul.upper_bound_witness() = ci; + m_vars_to_ul_pairs[j] = ul; +} + +void lar_solver::set_low_bound_witness(var_index j, constraint_index ci) { + ul_pair ul = m_vars_to_ul_pairs[j]; + ul.low_bound_witness() = ci; + m_vars_to_ul_pairs[j] = ul; +} + +void lar_solver::register_one_coeff_in_map(std::unordered_map & coeffs, const mpq & a, unsigned j) { + auto it = coeffs.find(j); + if (it == coeffs.end()) { + coeffs[j] = a; + } else { + it->second += a; + } +} + + +void lar_solver::substitute_terms_in_linear_expression(const vector>& left_side_with_terms, + vector> &left_side, mpq & right_side) const { + std::unordered_map coeffs; + for (auto & t : left_side_with_terms) { + unsigned j = t.second; + if (!is_term(j)) { + register_one_coeff_in_map(coeffs, t.first, j); + } else { + const lar_term & term = * m_terms[adjust_term_index(t.second)]; + for (auto & p : term.coeffs()){ + register_one_coeff_in_map(coeffs, t.first * p.second , p.first); + } + right_side += t.first * term.m_v; + } + } + + for (auto & p : coeffs) + left_side.push_back(std::make_pair(p.second, p.first)); +} + + +void lar_solver::detect_rows_of_bound_change_column_for_nbasic_column(unsigned j) { + if (A_r().row_count() != m_column_buffer.data_size()) + m_column_buffer.resize(A_r().row_count()); + else + m_column_buffer.clear(); + lean_assert(m_column_buffer.size() == 0 && m_column_buffer.is_OK()); + + m_mpq_lar_core_solver.m_r_solver.solve_Bd(j, m_column_buffer); + for (unsigned i : m_column_buffer.m_index) + m_rows_with_changed_bounds.insert(i); +} + + + +void lar_solver::detect_rows_of_bound_change_column_for_nbasic_column_tableau(unsigned j) { + for (auto & rc : m_mpq_lar_core_solver.m_r_A.m_columns[j]) + m_rows_with_changed_bounds.insert(rc.m_i); +} + +bool lar_solver::use_tableau() const { return m_settings.use_tableau(); } + +bool lar_solver::use_tableau_costs() const { + return m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs; +} + +void lar_solver::detect_rows_of_column_with_bound_change(unsigned j) { + if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) { // it is a basic column + // just mark the row at touched and exit + m_rows_with_changed_bounds.insert(m_mpq_lar_core_solver.m_r_heading[j]); + return; + } + + if (use_tableau()) + detect_rows_of_bound_change_column_for_nbasic_column_tableau(j); + else + detect_rows_of_bound_change_column_for_nbasic_column(j); +} + +void lar_solver::adjust_x_of_column(unsigned j) { + lean_assert(false); +} + +bool lar_solver::row_is_correct(unsigned i) const { + numeric_pair r = zero_of_type>(); + for (const auto & c : A_r().m_rows[i]) + r += c.m_value * m_mpq_lar_core_solver.m_r_x[c.m_j]; + return is_zero(r); +} + +bool lar_solver::ax_is_correct() const { + for (unsigned i = 0; i < A_r().row_count(); i++) { + if (!row_is_correct(i)) + return false; + } + return true; +} + +bool lar_solver::tableau_with_costs() const { + return m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs; +} + +bool lar_solver::costs_are_used() const { + return m_settings.simplex_strategy() != simplex_strategy_enum::tableau_rows; +} + +void lar_solver::change_basic_x_by_delta_on_column(unsigned j, const numeric_pair & delta) { + if (use_tableau()) { + for (const auto & c : A_r().m_columns[j]) { + unsigned bj = m_mpq_lar_core_solver.m_r_basis[c.m_i]; + m_mpq_lar_core_solver.m_r_x[bj] -= A_r().get_val(c) * delta; + if (tableau_with_costs()) { + m_basic_columns_with_changed_cost.insert(bj); + } + m_mpq_lar_core_solver.m_r_solver.update_column_in_inf_set(bj); + } + } else { + m_column_buffer.clear(); + m_column_buffer.resize(A_r().row_count()); + m_mpq_lar_core_solver.m_r_solver.solve_Bd(j, m_column_buffer); + for (unsigned i : m_column_buffer.m_index) { + unsigned bj = m_mpq_lar_core_solver.m_r_basis[i]; + m_mpq_lar_core_solver.m_r_x[bj] -= m_column_buffer[i] * delta; + m_mpq_lar_core_solver.m_r_solver.update_column_in_inf_set(bj); + } + } +} + +void lar_solver::update_x_and_inf_costs_for_column_with_changed_bounds(unsigned j) { + if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) { + if (costs_are_used()) { + bool was_infeas = m_mpq_lar_core_solver.m_r_solver.m_inf_set.contains(j); + m_mpq_lar_core_solver.m_r_solver.update_column_in_inf_set(j); + if (was_infeas != m_mpq_lar_core_solver.m_r_solver.m_inf_set.contains(j)) + m_basic_columns_with_changed_cost.insert(j); + } else { + m_mpq_lar_core_solver.m_r_solver.update_column_in_inf_set(j); + } + } else { + numeric_pair delta; + if (m_mpq_lar_core_solver.m_r_solver.make_column_feasible(j, delta)) + change_basic_x_by_delta_on_column(j, delta); + } +} + + +void lar_solver::detect_rows_with_changed_bounds_for_column(unsigned j) { + if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) { + m_rows_with_changed_bounds.insert(m_mpq_lar_core_solver.m_r_heading[j]); + return; + } + + if (use_tableau()) + detect_rows_of_bound_change_column_for_nbasic_column_tableau(j); + else + detect_rows_of_bound_change_column_for_nbasic_column(j); +} + +void lar_solver::detect_rows_with_changed_bounds() { + for (auto j : m_columns_with_changed_bound.m_index) + detect_rows_with_changed_bounds_for_column(j); +} + +void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds() { + for (auto j : m_columns_with_changed_bound.m_index) + update_x_and_inf_costs_for_column_with_changed_bounds(j); +} + +void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds_tableau() { + lean_assert(ax_is_correct()); + for (auto j : m_columns_with_changed_bound.m_index) + update_x_and_inf_costs_for_column_with_changed_bounds(j); + + if (tableau_with_costs()) { + for (unsigned j : m_basic_columns_with_changed_cost.m_index) + m_mpq_lar_core_solver.m_r_solver.update_inf_cost_for_column_tableau(j); + lean_assert(m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); + } +} + + +void lar_solver::solve_with_core_solver() { + if (!use_tableau()) + add_last_rows_to_lu(m_mpq_lar_core_solver.m_r_solver); + if (m_mpq_lar_core_solver.need_to_presolve_with_double_solver()) { + add_last_rows_to_lu(m_mpq_lar_core_solver.m_d_solver); + } + m_mpq_lar_core_solver.prefix_r(); + if (costs_are_used()) { + m_basic_columns_with_changed_cost.clear(); + m_basic_columns_with_changed_cost.resize(m_mpq_lar_core_solver.m_r_x.size()); + } + if (use_tableau()) + update_x_and_inf_costs_for_columns_with_changed_bounds_tableau(); + else + update_x_and_inf_costs_for_columns_with_changed_bounds(); + m_mpq_lar_core_solver.solve(); + set_status(m_mpq_lar_core_solver.m_r_solver.get_status()); + lean_assert(m_status != OPTIMAL || all_constraints_hold()); +} + + +numeric_pair lar_solver::get_basic_var_value_from_row_directly(unsigned i) { + numeric_pair r = zero_of_type>(); + + unsigned bj = m_mpq_lar_core_solver.m_r_solver.m_basis[i]; + for (const auto & c: A_r().m_rows[i]) { + if (c.m_j == bj) continue; + const auto & x = m_mpq_lar_core_solver.m_r_x[c.m_j]; + if (!is_zero(x)) + r -= c.m_value * x; + } + return r; +} + +numeric_pair lar_solver::get_basic_var_value_from_row(unsigned i) { + if (settings().use_tableau()) { + return get_basic_var_value_from_row_directly(i); + } + + numeric_pair r = zero_of_type>(); + m_mpq_lar_core_solver.calculate_pivot_row(i); + for (unsigned j : m_mpq_lar_core_solver.m_r_solver.m_pivot_row.m_index) { + lean_assert(m_mpq_lar_core_solver.m_r_solver.m_basis_heading[j] < 0); + r -= m_mpq_lar_core_solver.m_r_solver.m_pivot_row.m_data[j] * m_mpq_lar_core_solver.m_r_x[j]; + } + return r; +} + +template +void lar_solver::add_last_rows_to_lu(lp_primal_core_solver & s) { + auto & f = s.m_factorization; + if (f != nullptr) { + auto columns_to_replace = f->get_set_of_columns_to_replace_for_add_last_rows(s.m_basis_heading); + if (f->m_refactor_counter + columns_to_replace.size() >= 200 || f->has_dense_submatrix()) { + delete f; + f = nullptr; + } else { + f->add_last_rows_to_B(s.m_basis_heading, columns_to_replace); + } + } + if (f == nullptr) { + init_factorization(f, s.m_A, s.m_basis, m_settings); + if (f->get_status() != LU_status::OK) { + delete f; + f = nullptr; + } + } + +} + +bool lar_solver::x_is_correct() const { + if (m_mpq_lar_core_solver.m_r_x.size() != A_r().column_count()) { + // std::cout << "the size is off " << m_r_solver.m_x.size() << ", " << A().column_count() << std::endl; + return false; + } + for (unsigned i = 0; i < A_r().row_count(); i++) { + numeric_pair delta = A_r().dot_product_with_row(i, m_mpq_lar_core_solver.m_r_x); + if (!delta.is_zero()) { + // std::cout << "x is off ("; + // std::cout << "m_b[" << i << "] = " << m_b[i] << " "; + // std::cout << "left side = " << A().dot_product_with_row(i, m_r_solver.m_x) << ' '; + // std::cout << "delta = " << delta << ' '; + // std::cout << "iters = " << total_iterations() << ")" << std::endl; + // std::cout << "row " << i << " is off" << std::endl; + return false; + } + } + return true;; + +} + +bool lar_solver::var_is_registered(var_index vj) const { + if (vj >= m_terms_start_index) { + if (vj - m_terms_start_index >= m_terms.size()) + return false; + } else if ( vj >= A_r().column_count()) { + return false; + } + return true; +} + +unsigned lar_solver::constraint_stack_size() const { + return m_constraint_count.stack_size(); +} + +void lar_solver::fill_last_row_of_A_r(static_matrix> & A, const lar_term * ls) { + lean_assert(A.row_count() > 0); + lean_assert(A.column_count() > 0); + unsigned last_row = A.row_count() - 1; + lean_assert(A.m_rows[last_row].size() == 0); + for (auto & t : ls->m_coeffs) { + lean_assert(!is_zero(t.second)); + var_index j = t.first; + A.set(last_row, j, - t.second); + } + unsigned basis_j = A.column_count() - 1; + A.set(last_row, basis_j, mpq(1)); +} + +template +void lar_solver::create_matrix_A(static_matrix & matr) { + lean_assert(false); // not implemented + /* + unsigned m = number_or_nontrivial_left_sides(); + unsigned n = m_vec_of_canonic_left_sides.size(); + if (matr.row_count() == m && matr.column_count() == n) + return; + matr.init_empty_matrix(m, n); + copy_from_mpq_matrix(matr); + */ +} + +template +void lar_solver::copy_from_mpq_matrix(static_matrix & matr) { + matr.m_rows.resize(A_r().row_count()); + matr.m_columns.resize(A_r().column_count()); + for (unsigned i = 0; i < matr.row_count(); i++) { + for (auto & it : A_r().m_rows[i]) { + matr.set(i, it.m_j, convert_struct::convert(it.get_val())); + } + } +} + + +bool lar_solver::try_to_set_fixed(column_info & ci) { + if (ci.upper_bound_is_set() && ci.low_bound_is_set() && ci.get_upper_bound() == ci.get_low_bound() && !ci.is_fixed()) { + ci.set_fixed_value(ci.get_upper_bound()); + return true; + } + return false; +} + +column_type lar_solver::get_column_type(const column_info & ci) { + auto ret = ci.get_column_type_no_flipping(); + if (ret == column_type::boxed) { // changing boxed to fixed because of the no span + if (ci.get_low_bound() == ci.get_upper_bound()) + ret = column_type::fixed; + } + return ret; +} + +std::string lar_solver::get_column_name(unsigned j) const { + if (j >= m_terms_start_index) + return std::string("_t") + T_to_string(j); + if (j >= m_columns_to_ext_vars_or_term_indices.size()) + return std::string("_s") + T_to_string(j); + + return std::string("v") + T_to_string(m_columns_to_ext_vars_or_term_indices[j]); +} + +bool lar_solver::all_constrained_variables_are_registered(const vector>& left_side) { + for (auto it : left_side) { + if (! var_is_registered(it.second)) + return false; + } + return true; +} + +bool lar_solver::all_constraints_hold() const { + if (m_settings.get_cancel_flag()) + return true; + std::unordered_map var_map; + get_model(var_map); + + for (unsigned i = 0; i < m_constraints.size(); i++) { + if (!constraint_holds(*m_constraints[i], var_map)) { + print_constraint(i, std::cout); + return false; + } + } + return true; +} + +bool lar_solver::constraint_holds(const lar_base_constraint & constr, std::unordered_map & var_map) const { + mpq left_side_val = get_left_side_val(constr, var_map); + switch (constr.m_kind) { + case LE: return left_side_val <= constr.m_right_side; + case LT: return left_side_val < constr.m_right_side; + case GE: return left_side_val >= constr.m_right_side; + case GT: return left_side_val > constr.m_right_side; + case EQ: return left_side_val == constr.m_right_side; + default: + lean_unreachable(); + } + return false; // it is unreachable +} + +bool lar_solver::the_relations_are_of_same_type(const vector> & evidence, lconstraint_kind & the_kind_of_sum) const { + unsigned n_of_G = 0, n_of_L = 0; + bool strict = false; + for (auto & it : evidence) { + mpq coeff = it.first; + constraint_index con_ind = it.second; + lconstraint_kind kind = coeff.is_pos() ? + m_constraints[con_ind]->m_kind : + flip_kind(m_constraints[con_ind]->m_kind); + if (kind == GT || kind == LT) + strict = true; + if (kind == GE || kind == GT) n_of_G++; + else if (kind == LE || kind == LT) n_of_L++; + } + the_kind_of_sum = n_of_G ? GE : (n_of_L ? LE : EQ); + if (strict) + the_kind_of_sum = static_cast((static_cast(the_kind_of_sum) / 2)); + + return n_of_G == 0 || n_of_L == 0; +} + +void lar_solver::register_in_map(std::unordered_map & coeffs, const lar_base_constraint & cn, const mpq & a) { + for (auto & it : cn.get_left_side_coefficients()) { + unsigned j = it.second; + auto p = coeffs.find(j); + if (p == coeffs.end()) + coeffs[j] = it.first * a; + else { + p->second += it.first * a; + if (p->second.is_zero()) + coeffs.erase(p); + } + } +} + +bool lar_solver::the_left_sides_sum_to_zero(const vector> & evidence) const { + std::unordered_map coeff_map; + for (auto & it : evidence) { + mpq coeff = it.first; + constraint_index con_ind = it.second; + lean_assert(con_ind < m_constraints.size()); + register_in_map(coeff_map, *m_constraints[con_ind], coeff); + } + + if (!coeff_map.empty()) { + std::cout << "left side = "; + vector> t; + for (auto & it : coeff_map) { + t.push_back(std::make_pair(it.second, it.first)); + } + print_linear_combination_of_column_indices(t, std::cout); + std::cout << std::endl; + return false; + } + + return true; +} + +bool lar_solver::the_right_sides_do_not_sum_to_zero(const vector> & evidence) { + mpq ret = numeric_traits::zero(); + for (auto & it : evidence) { + mpq coeff = it.first; + constraint_index con_ind = it.second; + lean_assert(con_ind < m_constraints.size()); + const lar_constraint & constr = *m_constraints[con_ind]; + ret += constr.m_right_side * coeff; + } + return !numeric_traits::is_zero(ret); +} + +bool lar_solver::explanation_is_correct(const vector>& explanation) const { +#ifdef LEAN_DEBUG + lconstraint_kind kind; + lean_assert(the_relations_are_of_same_type(explanation, kind)); + lean_assert(the_left_sides_sum_to_zero(explanation)); + mpq rs = sum_of_right_sides_of_explanation(explanation); + switch (kind) { + case LE: lean_assert(rs < zero_of_type()); + break; + case LT: lean_assert(rs <= zero_of_type()); + break; + case GE: lean_assert(rs > zero_of_type()); + break; + case GT: lean_assert(rs >= zero_of_type()); + break; + case EQ: lean_assert(rs != zero_of_type()); + break; + default: + lean_assert(false); + return false; + } +#endif + return true; +} + +bool lar_solver::inf_explanation_is_correct() const { +#ifdef LEAN_DEBUG + vector> explanation; + get_infeasibility_explanation(explanation); + return explanation_is_correct(explanation); +#endif + return true; +} + +mpq lar_solver::sum_of_right_sides_of_explanation(const vector> & explanation) const { + mpq ret = numeric_traits::zero(); + for (auto & it : explanation) { + mpq coeff = it.first; + constraint_index con_ind = it.second; + lean_assert(con_ind < m_constraints.size()); + ret += (m_constraints[con_ind]->m_right_side - m_constraints[con_ind]->get_free_coeff_of_left_side()) * coeff; + } + return ret; +} + +bool lar_solver::has_lower_bound(var_index var, constraint_index& ci, mpq& value, bool& is_strict) { + + if (var >= m_vars_to_ul_pairs.size()) { + // TBD: bounds on terms could also be used, caller may have to track these. + return false; + } + const ul_pair & ul = m_vars_to_ul_pairs[var]; + ci = ul.low_bound_witness(); + if (ci != static_cast(-1)) { + auto& p = m_mpq_lar_core_solver.m_r_low_bounds()[var]; + value = p.x; + is_strict = p.y.is_pos(); + return true; + } + else { + return false; + } +} + +bool lar_solver::has_upper_bound(var_index var, constraint_index& ci, mpq& value, bool& is_strict) { + + if (var >= m_vars_to_ul_pairs.size()) { + // TBD: bounds on terms could also be used, caller may have to track these. + return false; + } + const ul_pair & ul = m_vars_to_ul_pairs[var]; + ci = ul.upper_bound_witness(); + if (ci != static_cast(-1)) { + auto& p = m_mpq_lar_core_solver.m_r_upper_bounds()[var]; + value = p.x; + is_strict = p.y.is_neg(); + return true; + } + else { + return false; + } +} + +void lar_solver::get_infeasibility_explanation(vector> & explanation) const { + explanation.clear(); + if (m_infeasible_column_index != -1) { + fill_explanation_from_infeasible_column(explanation); + return; + } + if (m_mpq_lar_core_solver.get_infeasible_sum_sign() == 0) { + return; + } + // the infeasibility sign + int inf_sign; + auto inf_row = m_mpq_lar_core_solver.get_infeasibility_info(inf_sign); + get_infeasibility_explanation_for_inf_sign(explanation, inf_row, inf_sign); + lean_assert(explanation_is_correct(explanation)); +} + + + +void lar_solver::get_infeasibility_explanation_for_inf_sign( + vector> & explanation, + const vector> & inf_row, + int inf_sign) const { + + for (auto & it : inf_row) { + mpq coeff = it.first; + unsigned j = it.second; + + int adj_sign = coeff.is_pos() ? inf_sign : -inf_sign; + const ul_pair & ul = m_vars_to_ul_pairs[j]; + + constraint_index bound_constr_i = adj_sign < 0 ? ul.upper_bound_witness() : ul.low_bound_witness(); + lean_assert(bound_constr_i < m_constraints.size()); + explanation.push_back(std::make_pair(coeff, bound_constr_i)); + } +} + +void lar_solver::get_model(std::unordered_map & variable_values) const { + mpq delta = mpq(1, 2); // start from 0.5 to have less clashes + lean_assert(m_status == OPTIMAL); + unsigned i; + do { + + // different pairs have to produce different singleton values + std::unordered_set set_of_different_pairs; + std::unordered_set set_of_different_singles; + delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta); + for (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]; + set_of_different_pairs.insert(rp); + mpq x = rp.x + delta * rp.y; + set_of_different_singles.insert(x); + if (set_of_different_pairs.size() + != set_of_different_singles.size()) { + delta /= mpq(2); + break; + } + + variable_values[i] = x; + } + } while (i != m_mpq_lar_core_solver.m_r_x.size()); +} + +std::string lar_solver::get_variable_name(var_index vi) const { + return get_column_name(vi); +} + +// ********** print region start +void lar_solver::print_constraint(constraint_index ci, std::ostream & out) const { + if (ci >= m_constraints.size()) { + out << "constraint " << T_to_string(ci) << " is not found"; + out << std::endl; + return; + } + + print_constraint(m_constraints[ci], out); +} + +void lar_solver::print_constraints(std::ostream& out) const { + for (auto c : m_constraints) { + print_constraint(c, out); + } +} + +void lar_solver::print_terms(std::ostream& out) const { + for (auto it : m_terms) { + print_term(*it, out); + out << "\n"; + } +} + +void lar_solver::print_left_side_of_constraint(const lar_base_constraint * c, std::ostream & out) const { + print_linear_combination_of_column_indices(c->get_left_side_coefficients(), out); + mpq free_coeff = c->get_free_coeff_of_left_side(); + if (!is_zero(free_coeff)) + out << " + " << free_coeff; + +} + +void lar_solver::print_term(lar_term const& term, std::ostream & out) const { + if (!numeric_traits::is_zero(term.m_v)) { + out << term.m_v << " + "; + } + print_linear_combination_of_column_indices(term.coeffs_as_vector(), out); +} + +mpq lar_solver::get_left_side_val(const lar_base_constraint & cns, const std::unordered_map & var_map) const { + mpq ret = cns.get_free_coeff_of_left_side(); + for (auto & it : cns.get_left_side_coefficients()) { + var_index j = it.second; + auto vi = var_map.find(j); + lean_assert(vi != var_map.end()); + ret += it.first * vi->second; + } + return ret; +} + +void lar_solver::print_constraint(const lar_base_constraint * c, std::ostream & out) const { + print_left_side_of_constraint(c, out); + out << " " << lconstraint_kind_string(c->m_kind) << " " << c->m_right_side << std::endl; +} + +void lar_solver::fill_var_set_for_random_update(unsigned sz, var_index const * vars, vector& column_list) { + for (unsigned i = 0; i < sz; i++) { + var_index var = vars[i]; + if (var >= m_terms_start_index) { // handle the term + for (auto & it : m_terms[var - m_terms_start_index]->m_coeffs) { + column_list.push_back(it.first); + } + } else { + column_list.push_back(var); + } + } +} + +void lar_solver::random_update(unsigned sz, var_index const * vars) { + vector column_list; + fill_var_set_for_random_update(sz, vars, column_list); + random_updater ru(m_mpq_lar_core_solver, column_list); + ru.update(); +} + + +void lar_solver::pivot_fixed_vars_from_basis() { + m_mpq_lar_core_solver.m_r_solver.pivot_fixed_vars_from_basis(); +} + +void lar_solver::pop() { + pop(1); +} + +bool lar_solver::column_represents_row_in_tableau(unsigned j) { + return m_vars_to_ul_pairs()[j].m_i != static_cast(-1); +} + +void lar_solver::make_sure_that_the_bottom_right_elem_not_zero_in_tableau(unsigned i, unsigned j) { + // i, j - is the indices of the bottom-right element of the tableau + lean_assert(A_r().row_count() == i + 1 && A_r().column_count() == j + 1); + auto & last_column = A_r().m_columns[j]; + int non_zero_column_cell_index = -1; + for (unsigned k = last_column.size(); k-- > 0;){ + auto & cc = last_column[k]; + if (cc.m_i == i) + return; + non_zero_column_cell_index = k; + } + + lean_assert(non_zero_column_cell_index != -1); + lean_assert(static_cast(non_zero_column_cell_index) != i); + m_mpq_lar_core_solver.m_r_solver.transpose_rows_tableau(last_column[non_zero_column_cell_index].m_i, i); +} + +void lar_solver::remove_last_row_and_column_from_tableau(unsigned j) { + lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); + auto & slv = m_mpq_lar_core_solver.m_r_solver; + unsigned i = A_r().row_count() - 1; //last row index + make_sure_that_the_bottom_right_elem_not_zero_in_tableau(i, j); + if (slv.m_basis_heading[j] < 0) { + slv.pivot_column_tableau(j, i); + } + + auto & last_row = A_r().m_rows[i]; + mpq &cost_j = m_mpq_lar_core_solver.m_r_solver.m_costs[j]; + bool cost_is_nz = !is_zero(cost_j); + for (unsigned k = last_row.size(); k-- > 0;) { + auto &rc = last_row[k]; + if (cost_is_nz) { + m_mpq_lar_core_solver.m_r_solver.m_d[rc.m_j] += cost_j*rc.get_val(); + } + + A_r().remove_element(last_row, rc); + } + lean_assert(last_row.size() == 0); + lean_assert(A_r().m_columns[j].size() == 0); + A_r().m_rows.pop_back(); + A_r().m_columns.pop_back(); + slv.m_b.pop_back(); +} + +void lar_solver::remove_last_column_from_tableau(unsigned j) { + lean_assert(j == A_r().column_count() - 1); + // the last column has to be empty + lean_assert(A_r().m_columns[j].size() == 0); + A_r().m_columns.pop_back(); +} + +void lar_solver::remove_last_column_from_basis_tableau(unsigned j) { + auto& rslv = m_mpq_lar_core_solver.m_r_solver; + int i = rslv.m_basis_heading[j]; + if (i >= 0) { // j is a basic var + int last_pos = static_cast(rslv.m_basis.size()) - 1; + lean_assert(last_pos >= 0); + if (i != last_pos) { + unsigned j_at_last_pos = rslv.m_basis[last_pos]; + rslv.m_basis[i] = j_at_last_pos; + rslv.m_basis_heading[j_at_last_pos] = i; + } + rslv.m_basis.pop_back(); // remove j from the basis + } else { + int last_pos = static_cast(rslv.m_nbasis.size()) - 1; + lean_assert(last_pos >= 0); + i = - 1 - i; + if (i != last_pos) { + unsigned j_at_last_pos = rslv.m_nbasis[last_pos]; + rslv.m_nbasis[i] = j_at_last_pos; + rslv.m_basis_heading[j_at_last_pos] = - i - 1; + } + rslv.m_nbasis.pop_back(); // remove j from the basis + } + rslv.m_basis_heading.pop_back(); + lean_assert(rslv.m_basis.size() == A_r().row_count()); + lean_assert(rslv.basis_heading_is_correct()); +} + +void lar_solver::remove_column_from_tableau(unsigned j) { + auto& rslv = m_mpq_lar_core_solver.m_r_solver; + lean_assert(j == A_r().column_count() - 1); + lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); + if (column_represents_row_in_tableau(j)) { + remove_last_row_and_column_from_tableau(j); + if (rslv.m_basis_heading[j] < 0) + rslv.change_basis_unconditionally(j, rslv.m_basis[A_r().row_count()]); // A_r().row_count() is the index of the last row in the basis still + } + else { + remove_last_column_from_tableau(j); + } + rslv.m_x.pop_back(); + rslv.m_d.pop_back(); + rslv.m_costs.pop_back(); + + remove_last_column_from_basis_tableau(j); + lean_assert(m_mpq_lar_core_solver.r_basis_is_OK()); + lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); +} + +void lar_solver::pop_tableau() { + lean_assert(m_mpq_lar_core_solver.m_r_solver.m_costs.size() == A_r().column_count()); + + lean_assert(m_mpq_lar_core_solver.m_r_solver.m_basis.size() == A_r().row_count()); + lean_assert(m_mpq_lar_core_solver.m_r_solver.basis_heading_is_correct()); + // We remove last variables starting from m_column_names.size() to m_vec_of_canonic_left_sides.size(). + // At this moment m_column_names is already popped + for (unsigned j = A_r().column_count(); j-- > m_columns_to_ext_vars_or_term_indices.size();) + remove_column_from_tableau(j); + lean_assert(m_mpq_lar_core_solver.m_r_solver.m_costs.size() == A_r().column_count()); + lean_assert(m_mpq_lar_core_solver.m_r_solver.m_basis.size() == A_r().row_count()); + lean_assert(m_mpq_lar_core_solver.m_r_solver.basis_heading_is_correct()); +} + +void lar_solver::clean_inf_set_of_r_solver_after_pop() { + vector became_feas; + clean_large_elements_after_pop(A_r().column_count(), m_mpq_lar_core_solver.m_r_solver.m_inf_set); + std::unordered_set basic_columns_with_changed_cost; + auto inf_index_copy = m_mpq_lar_core_solver.m_r_solver.m_inf_set.m_index; + for (auto j: inf_index_copy) { + if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) { + continue; + } + // some basic columns might become non-basic - these columns need to be made feasible + numeric_pair delta; + if (m_mpq_lar_core_solver.m_r_solver.make_column_feasible(j, delta)) + change_basic_x_by_delta_on_column(j, delta); + became_feas.push_back(j); + } + + for (unsigned j : became_feas) { + lean_assert(m_mpq_lar_core_solver.m_r_solver.m_basis_heading[j] < 0); + m_mpq_lar_core_solver.m_r_solver.m_d[j] -= m_mpq_lar_core_solver.m_r_solver.m_costs[j]; + m_mpq_lar_core_solver.m_r_solver.m_costs[j] = zero_of_type(); + m_mpq_lar_core_solver.m_r_solver.m_inf_set.erase(j); + } + became_feas.clear(); + for (unsigned j : m_mpq_lar_core_solver.m_r_solver.m_inf_set.m_index) { + lean_assert(m_mpq_lar_core_solver.m_r_heading[j] >= 0); + if (m_mpq_lar_core_solver.m_r_solver.column_is_feasible(j)) + became_feas.push_back(j); + } + for (unsigned j : became_feas) + m_mpq_lar_core_solver.m_r_solver.m_inf_set.erase(j); + + + if (use_tableau_costs()) { + for (unsigned j : became_feas) + m_mpq_lar_core_solver.m_r_solver.update_inf_cost_for_column_tableau(j); + for (unsigned j : basic_columns_with_changed_cost) + m_mpq_lar_core_solver.m_r_solver.update_inf_cost_for_column_tableau(j); + lean_assert(m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); + } +} + +void lar_solver::shrink_explanation_to_minimum(vector> & explanation) const { + // implementing quickXplain + quick_xplain::run(explanation, *this); + lean_assert(this->explanation_is_correct(explanation)); +} + +bool lar_solver::model_is_int_feasible() const { + unsigned n = A_r().column_count(); + for (unsigned j = 0; j < n; j++) { + if (column_is_int(j) && !column_value_is_integer(j)) + return false; + } + return true; +} + +bool lar_solver::term_is_int(const lar_term * t) const { + for (auto const & p : t->m_coeffs) + if (!column_is_int(p.first) || p.second.is_int()) + return false; + return t->m_v.is_int(); +} + +bool lar_solver::var_is_int(var_index v) const { + if (is_term(v)) { + lar_term const& t = get_term(v); + return term_is_int(&t); + } + else { + return column_is_int(v); + } +} + +bool lar_solver::column_is_int(unsigned j) const { + unsigned ext_var = m_columns_to_ext_vars_or_term_indices[j]; + lean_assert(contains(m_ext_vars_to_columns, ext_var)); + return m_ext_vars_to_columns.find(ext_var)->second.is_integer(); +} + +bool lar_solver::column_is_fixed(unsigned j) const { + return m_mpq_lar_core_solver.column_is_fixed(j); +} + + +bool lar_solver::ext_var_is_int(var_index ext_var) const { + auto it = m_ext_vars_to_columns.find(ext_var); + lean_assert(it != m_ext_vars_to_columns.end()); + return it == m_ext_vars_to_columns.end() || it->second.is_integer(); +} + + // below is the initialization functionality of lar_solver + +bool lar_solver::strategy_is_undecided() const { + return m_settings.simplex_strategy() == simplex_strategy_enum::undecided; +} + +var_index lar_solver::add_var(unsigned ext_j, bool is_int) { + TRACE("add_var", tout << "adding var " << ext_j << (is_int? " int" : " nonint") << std::endl;); + var_index i; + lean_assert(ext_j < m_terms_start_index); + + if (ext_j >= m_terms_start_index) + throw 0; // todo : what is the right way to exit? + auto it = m_ext_vars_to_columns.find(ext_j); + if (it != m_ext_vars_to_columns.end()) { + return it->second.ext_j(); + } + lean_assert(m_vars_to_ul_pairs.size() == A_r().column_count()); + i = A_r().column_count(); + m_vars_to_ul_pairs.push_back(ul_pair(static_cast(-1))); + add_non_basic_var_to_core_fields(ext_j, is_int); + lean_assert(sizes_are_correct()); + return i; +} + +void lar_solver::register_new_ext_var_index(unsigned ext_v, bool is_int) { + lean_assert(!contains(m_ext_vars_to_columns, ext_v)); + unsigned j = static_cast(m_ext_vars_to_columns.size()); + m_ext_vars_to_columns.insert(std::make_pair(ext_v, ext_var_info(j, is_int))); + lean_assert(m_columns_to_ext_vars_or_term_indices.size() == j); + m_columns_to_ext_vars_or_term_indices.push_back(ext_v); +} + +void lar_solver::add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int) { + register_new_ext_var_index(ext_j, is_int); + m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column); + m_columns_with_changed_bound.increase_size_by_one(); + add_new_var_to_core_fields_for_mpq(false); + if (use_lu()) + add_new_var_to_core_fields_for_doubles(false); +} + +void lar_solver::add_new_var_to_core_fields_for_doubles(bool register_in_basis) { + unsigned j = A_d().column_count(); + A_d().add_column(); + lean_assert(m_mpq_lar_core_solver.m_d_x.size() == j); + // lean_assert(m_mpq_lar_core_solver.m_d_low_bounds.size() == j && m_mpq_lar_core_solver.m_d_upper_bounds.size() == j); // restore later + m_mpq_lar_core_solver.m_d_x.resize(j + 1); + m_mpq_lar_core_solver.m_d_low_bounds.resize(j + 1); + m_mpq_lar_core_solver.m_d_upper_bounds.resize(j + 1); + lean_assert(m_mpq_lar_core_solver.m_d_heading.size() == j); // as A().column_count() on the entry to the method + if (register_in_basis) { + A_d().add_row(); + m_mpq_lar_core_solver.m_d_heading.push_back(m_mpq_lar_core_solver.m_d_basis.size()); + m_mpq_lar_core_solver.m_d_basis.push_back(j); + } + else { + m_mpq_lar_core_solver.m_d_heading.push_back(-static_cast(m_mpq_lar_core_solver.m_d_nbasis.size()) - 1); + m_mpq_lar_core_solver.m_d_nbasis.push_back(j); + } +} + +void lar_solver::add_new_var_to_core_fields_for_mpq(bool register_in_basis) { + unsigned j = A_r().column_count(); + A_r().add_column(); + lean_assert(m_mpq_lar_core_solver.m_r_x.size() == j); + // lean_assert(m_mpq_lar_core_solver.m_r_low_bounds.size() == j && m_mpq_lar_core_solver.m_r_upper_bounds.size() == j); // restore later + m_mpq_lar_core_solver.m_r_x.resize(j + 1); + m_mpq_lar_core_solver.m_r_low_bounds.increase_size_by_one(); + m_mpq_lar_core_solver.m_r_upper_bounds.increase_size_by_one(); + m_mpq_lar_core_solver.m_r_solver.m_inf_set.increase_size_by_one(); + m_mpq_lar_core_solver.m_r_solver.m_costs.resize(j + 1); + m_mpq_lar_core_solver.m_r_solver.m_d.resize(j + 1); + lean_assert(m_mpq_lar_core_solver.m_r_heading.size() == j); // as A().column_count() on the entry to the method + if (register_in_basis) { + A_r().add_row(); + m_mpq_lar_core_solver.m_r_heading.push_back(m_mpq_lar_core_solver.m_r_basis.size()); + m_mpq_lar_core_solver.m_r_basis.push_back(j); + if (m_settings.bound_propagation()) + m_rows_with_changed_bounds.insert(A_r().row_count() - 1); + } + else { + m_mpq_lar_core_solver.m_r_heading.push_back(-static_cast(m_mpq_lar_core_solver.m_r_nbasis.size()) - 1); + m_mpq_lar_core_solver.m_r_nbasis.push_back(j); + } +} + + +var_index lar_solver::add_term_undecided(const vector> & coeffs, + const mpq &m_v) { + m_terms.push_back(new lar_term(coeffs, m_v)); + return m_terms_start_index + m_terms.size() - 1; +} + +// terms +var_index lar_solver::add_term(const vector> & coeffs, + const mpq &m_v) { + if (strategy_is_undecided()) + return add_term_undecided(coeffs, m_v); + + m_terms.push_back(new lar_term(coeffs, m_v)); + unsigned adjusted_term_index = m_terms.size() - 1; + var_index ret = m_terms_start_index + adjusted_term_index; + if (use_tableau() && !coeffs.empty()) { + add_row_for_term(m_terms.back(), ret); + if (m_settings.bound_propagation()) + m_rows_with_changed_bounds.insert(A_r().row_count() - 1); + } + lean_assert(m_ext_vars_to_columns.size() == A_r().column_count()); + return ret; +} + +void lar_solver::add_row_for_term(const lar_term * term, unsigned term_ext_index) { + lean_assert(sizes_are_correct()); + add_row_from_term_no_constraint(term, term_ext_index); + lean_assert(sizes_are_correct()); +} + +void lar_solver::add_row_from_term_no_constraint(const lar_term * term, unsigned term_ext_index) { + register_new_ext_var_index(term_ext_index, term_is_int(term)); + // j will be a new variable + unsigned j = A_r().column_count(); + ul_pair ul(j); + m_vars_to_ul_pairs.push_back(ul); + add_basic_var_to_core_fields(); + if (use_tableau()) { + auto it = iterator_on_term_with_basis_var(*term, j); + A_r().fill_last_row_with_pivoting(it, + m_mpq_lar_core_solver.m_r_solver.m_basis_heading); + m_mpq_lar_core_solver.m_r_solver.m_b.resize(A_r().column_count(), zero_of_type()); + } + else { + fill_last_row_of_A_r(A_r(), term); + } + m_mpq_lar_core_solver.m_r_x[j] = get_basic_var_value_from_row_directly(A_r().row_count() - 1); + if (use_lu()) + fill_last_row_of_A_d(A_d(), term); +} + +void lar_solver::add_basic_var_to_core_fields() { + bool use_lu = m_mpq_lar_core_solver.need_to_presolve_with_double_solver(); + lean_assert(!use_lu || A_r().column_count() == A_d().column_count()); + m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column); + m_columns_with_changed_bound.increase_size_by_one(); + m_rows_with_changed_bounds.increase_size_by_one(); + add_new_var_to_core_fields_for_mpq(true); + if (use_lu) + add_new_var_to_core_fields_for_doubles(true); +} + +bool lar_solver::bound_is_integer_if_needed(unsigned j, const mpq & right_side) const { + if (!column_is_int(j)) + return true; + return right_side.is_int(); +} + +constraint_index lar_solver::add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) { + constraint_index ci = m_constraints.size(); + if (!is_term(j)) { // j is a var + lean_assert(bound_is_integer_if_needed(j, right_side)); + auto vc = new lar_var_constraint(j, kind, right_side); + m_constraints.push_back(vc); + update_column_type_and_bound(j, kind, right_side, ci); + } + else { + add_var_bound_on_constraint_for_term(j, kind, right_side, ci); + } + lean_assert(sizes_are_correct()); + return ci; +} + +void lar_solver::update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index) { + switch (m_mpq_lar_core_solver.m_column_types[j]) { + case column_type::free_column: + update_free_column_type_and_bound(j, kind, right_side, constr_index); + break; + case column_type::boxed: + update_boxed_column_type_and_bound(j, kind, right_side, constr_index); + break; + case column_type::low_bound: + update_low_bound_column_type_and_bound(j, kind, right_side, constr_index); + break; + case column_type::upper_bound: + update_upper_bound_column_type_and_bound(j, kind, right_side, constr_index); + break; + case column_type::fixed: + update_fixed_column_type_and_bound(j, kind, right_side, constr_index); + break; + default: + lean_assert(false); // cannot be here + } +} + +void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { + lean_assert(is_term(j)); + unsigned adjusted_term_index = adjust_term_index(j); + lean_assert(!term_is_int(m_terms[adjusted_term_index]) || right_side.is_int()); + auto it = m_ext_vars_to_columns.find(j); + if (it != m_ext_vars_to_columns.end()) { + unsigned term_j = it->second.ext_j(); + mpq rs = right_side - m_terms[adjusted_term_index]->m_v; + m_constraints.push_back(new lar_term_constraint(m_terms[adjusted_term_index], kind, right_side)); + update_column_type_and_bound(term_j, kind, rs, ci); + } + else { + add_constraint_from_term_and_create_new_column_row(j, m_terms[adjusted_term_index], kind, right_side); + } +} + +constraint_index lar_solver::add_constraint(const vector>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm) { + vector> left_side; + mpq rs = -right_side_parm; + substitute_terms_in_linear_expression(left_side_with_terms, left_side, rs); + unsigned term_index = add_term(left_side, zero_of_type()); + constraint_index ci = m_constraints.size(); + add_var_bound_on_constraint_for_term(term_index, kind_par, -rs, ci); + return ci; +} + +void lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term, + lconstraint_kind kind, const mpq & right_side) { + + add_row_from_term_no_constraint(term, term_j); + unsigned j = A_r().column_count() - 1; + update_column_type_and_bound(j, kind, right_side - term->m_v, m_constraints.size()); + m_constraints.push_back(new lar_term_constraint(term, kind, right_side)); + lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); +} + +void lar_solver::decide_on_strategy_and_adjust_initial_state() { + lean_assert(strategy_is_undecided()); + if (m_vars_to_ul_pairs.size() > m_settings.column_number_threshold_for_using_lu_in_lar_solver) { + m_settings.simplex_strategy() = simplex_strategy_enum::lu; + } + else { + m_settings.simplex_strategy() = simplex_strategy_enum::tableau_rows; // todo: when to switch to tableau_costs? + } + adjust_initial_state(); +} + +void lar_solver::adjust_initial_state() { + switch (m_settings.simplex_strategy()) { + case simplex_strategy_enum::lu: + adjust_initial_state_for_lu(); + break; + case simplex_strategy_enum::tableau_rows: + adjust_initial_state_for_tableau_rows(); + break; + case simplex_strategy_enum::tableau_costs: + lean_assert(false); // not implemented + case simplex_strategy_enum::undecided: + adjust_initial_state_for_tableau_rows(); + break; + } +} + +void lar_solver::adjust_initial_state_for_lu() { + copy_from_mpq_matrix(A_d()); + unsigned n = A_d().column_count(); + m_mpq_lar_core_solver.m_d_x.resize(n); + m_mpq_lar_core_solver.m_d_low_bounds.resize(n); + m_mpq_lar_core_solver.m_d_upper_bounds.resize(n); + m_mpq_lar_core_solver.m_d_heading = m_mpq_lar_core_solver.m_r_heading; + m_mpq_lar_core_solver.m_d_basis = m_mpq_lar_core_solver.m_r_basis; + + /* + unsigned j = A_d().column_count(); + A_d().add_column(); + lean_assert(m_mpq_lar_core_solver.m_d_x.size() == j); + // lean_assert(m_mpq_lar_core_solver.m_d_low_bounds.size() == j && m_mpq_lar_core_solver.m_d_upper_bounds.size() == j); // restore later + m_mpq_lar_core_solver.m_d_x.resize(j + 1 ); + m_mpq_lar_core_solver.m_d_low_bounds.resize(j + 1); + m_mpq_lar_core_solver.m_d_upper_bounds.resize(j + 1); + lean_assert(m_mpq_lar_core_solver.m_d_heading.size() == j); // as A().column_count() on the entry to the method + if (register_in_basis) { + A_d().add_row(); + m_mpq_lar_core_solver.m_d_heading.push_back(m_mpq_lar_core_solver.m_d_basis.size()); + m_mpq_lar_core_solver.m_d_basis.push_back(j); + }else { + m_mpq_lar_core_solver.m_d_heading.push_back(- static_cast(m_mpq_lar_core_solver.m_d_nbasis.size()) - 1); + m_mpq_lar_core_solver.m_d_nbasis.push_back(j); + }*/ +} + +void lar_solver::adjust_initial_state_for_tableau_rows() { + for (unsigned j = 0; j < m_terms.size(); j++) { + if (contains(m_ext_vars_to_columns, j + m_terms_start_index)) + continue; + add_row_from_term_no_constraint(m_terms[j], j + m_terms_start_index); + } +} + +// this fills the last row of A_d and sets the basis column: -1 in the last column of the row +void lar_solver::fill_last_row_of_A_d(static_matrix & A, const lar_term* ls) { + lean_assert(A.row_count() > 0); + lean_assert(A.column_count() > 0); + unsigned last_row = A.row_count() - 1; + lean_assert(A.m_rows[last_row].empty()); + + for (auto & t : ls->m_coeffs) { + lean_assert(!is_zero(t.second)); + var_index j = t.first; + A.set(last_row, j, -t.second.get_double()); + } + + unsigned basis_j = A.column_count() - 1; + A.set(last_row, basis_j, -1); +} + +void lar_solver::update_free_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_ind) { + mpq y_of_bound(0); + switch (kind) { + case LT: + y_of_bound = -1; + case LE: + m_mpq_lar_core_solver.m_column_types[j] = column_type::upper_bound; + lean_assert(m_mpq_lar_core_solver.m_column_types()[j] == column_type::upper_bound); + lean_assert(m_mpq_lar_core_solver.m_r_upper_bounds.size() > j); + { + auto up = numeric_pair(right_side, y_of_bound); + m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; + } + set_upper_bound_witness(j, constr_ind); + break; + case GT: + y_of_bound = 1; + case GE: + m_mpq_lar_core_solver.m_column_types[j] = column_type::low_bound; + lean_assert(m_mpq_lar_core_solver.m_r_upper_bounds.size() > j); + { + auto low = numeric_pair(right_side, y_of_bound); + m_mpq_lar_core_solver.m_r_low_bounds[j] = low; + } + set_low_bound_witness(j, constr_ind); + break; + case EQ: + m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed; + m_mpq_lar_core_solver.m_r_low_bounds[j] = m_mpq_lar_core_solver.m_r_upper_bounds[j] = numeric_pair(right_side, zero_of_type()); + set_upper_bound_witness(j, constr_ind); + set_low_bound_witness(j, constr_ind); + break; + + default: + lean_unreachable(); + + } + m_columns_with_changed_bound.insert(j); +} + +void lar_solver::update_upper_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { + lean_assert(m_mpq_lar_core_solver.m_column_types()[j] == column_type::upper_bound); + mpq y_of_bound(0); + switch (kind) { + case LT: + y_of_bound = -1; + case LE: + { + auto up = numeric_pair(right_side, y_of_bound); + if (up < m_mpq_lar_core_solver.m_r_upper_bounds()[j]) { + m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; + set_upper_bound_witness(j, ci); + m_columns_with_changed_bound.insert(j); + } + } + break; + case GT: + y_of_bound = 1; + case GE: + m_mpq_lar_core_solver.m_column_types[j] = column_type::boxed; + { + auto low = numeric_pair(right_side, y_of_bound); + m_mpq_lar_core_solver.m_r_low_bounds[j] = low; + set_low_bound_witness(j, ci); + m_columns_with_changed_bound.insert(j); + if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { + m_status = INFEASIBLE; + m_infeasible_column_index = j; + } + else { + m_mpq_lar_core_solver.m_column_types[j] = m_mpq_lar_core_solver.m_r_low_bounds()[j] < m_mpq_lar_core_solver.m_r_upper_bounds()[j] ? column_type::boxed : column_type::fixed; + } + } + break; + case EQ: + { + auto v = numeric_pair(right_side, zero_of_type()); + if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { + m_status = INFEASIBLE; + set_low_bound_witness(j, ci); + m_infeasible_column_index = j; + } + else { + m_mpq_lar_core_solver.m_r_low_bounds[j] = m_mpq_lar_core_solver.m_r_upper_bounds[j] = v; + m_columns_with_changed_bound.insert(j); + set_low_bound_witness(j, ci); + set_upper_bound_witness(j, ci); + m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed; + } + break; + } + break; + + default: + lean_unreachable(); + + } +} + +void lar_solver::update_boxed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { + lean_assert(m_status == INFEASIBLE || (m_mpq_lar_core_solver.m_column_types()[j] == column_type::boxed && m_mpq_lar_core_solver.m_r_low_bounds()[j] < m_mpq_lar_core_solver.m_r_upper_bounds()[j])); + mpq y_of_bound(0); + switch (kind) { + case LT: + y_of_bound = -1; + case LE: + { + auto up = numeric_pair(right_side, y_of_bound); + if (up < m_mpq_lar_core_solver.m_r_upper_bounds[j]) { + m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; + set_upper_bound_witness(j, ci); + m_columns_with_changed_bound.insert(j); + } + + if (up < m_mpq_lar_core_solver.m_r_low_bounds[j]) { + m_status = INFEASIBLE; + lean_assert(false); + m_infeasible_column_index = j; + } + else { + if (m_mpq_lar_core_solver.m_r_low_bounds()[j] == m_mpq_lar_core_solver.m_r_upper_bounds()[j]) + m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed; + } + } + break; + case GT: + y_of_bound = 1; + case GE: + { + auto low = numeric_pair(right_side, y_of_bound); + if (low > m_mpq_lar_core_solver.m_r_low_bounds[j]) { + m_mpq_lar_core_solver.m_r_low_bounds[j] = low; + m_columns_with_changed_bound.insert(j); + set_low_bound_witness(j, ci); + } + if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { + m_status = INFEASIBLE; + m_infeasible_column_index = j; + } + else if (low == m_mpq_lar_core_solver.m_r_upper_bounds[j]) { + m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed; + } + } + break; + case EQ: + { + auto v = numeric_pair(right_side, zero_of_type()); + if (v < m_mpq_lar_core_solver.m_r_low_bounds[j]) { + m_status = INFEASIBLE; + m_infeasible_column_index = j; + set_upper_bound_witness(j, ci); + } + else if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { + m_status = INFEASIBLE; + m_infeasible_column_index = j; + set_low_bound_witness(j, ci); + } + else { + m_mpq_lar_core_solver.m_r_low_bounds[j] = m_mpq_lar_core_solver.m_r_upper_bounds[j] = v; + set_low_bound_witness(j, ci); + set_upper_bound_witness(j, ci); + m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed; + m_columns_with_changed_bound.insert(j); + } + + break; + } + + default: + lean_unreachable(); + + } +} +void lar_solver::update_low_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { + lean_assert(m_mpq_lar_core_solver.m_column_types()[j] == column_type::low_bound); + mpq y_of_bound(0); + switch (kind) { + case LT: + y_of_bound = -1; + case LE: + { + auto up = numeric_pair(right_side, y_of_bound); + m_mpq_lar_core_solver.m_r_upper_bounds[j] = up; + set_upper_bound_witness(j, ci); + m_columns_with_changed_bound.insert(j); + + if (up < m_mpq_lar_core_solver.m_r_low_bounds[j]) { + m_status = INFEASIBLE; + m_infeasible_column_index = j; + } + else { + m_mpq_lar_core_solver.m_column_types[j] = m_mpq_lar_core_solver.m_r_low_bounds()[j] < m_mpq_lar_core_solver.m_r_upper_bounds()[j] ? column_type::boxed : column_type::fixed; + } + } + break; + case GT: + y_of_bound = 1; + case GE: + { + auto low = numeric_pair(right_side, y_of_bound); + if (low > m_mpq_lar_core_solver.m_r_low_bounds[j]) { + m_mpq_lar_core_solver.m_r_low_bounds[j] = low; + m_columns_with_changed_bound.insert(j); + set_low_bound_witness(j, ci); + } + } + break; + case EQ: + { + auto v = numeric_pair(right_side, zero_of_type()); + if (v < m_mpq_lar_core_solver.m_r_low_bounds[j]) { + m_status = INFEASIBLE; + m_infeasible_column_index = j; + set_upper_bound_witness(j, ci); + } + else { + m_mpq_lar_core_solver.m_r_low_bounds[j] = m_mpq_lar_core_solver.m_r_upper_bounds[j] = v; + set_low_bound_witness(j, ci); + set_upper_bound_witness(j, ci); + m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed; + } + m_columns_with_changed_bound.insert(j); + break; + } + + default: + lean_unreachable(); + + } +} + +void lar_solver::update_fixed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { + lean_assert(m_status == INFEASIBLE || (m_mpq_lar_core_solver.m_column_types()[j] == column_type::fixed && m_mpq_lar_core_solver.m_r_low_bounds()[j] == m_mpq_lar_core_solver.m_r_upper_bounds()[j])); + lean_assert(m_status == INFEASIBLE || (m_mpq_lar_core_solver.m_r_low_bounds()[j].y.is_zero() && m_mpq_lar_core_solver.m_r_upper_bounds()[j].y.is_zero())); + auto v = numeric_pair(right_side, mpq(0)); + + mpq y_of_bound(0); + switch (kind) { + case LT: + if (v <= m_mpq_lar_core_solver.m_r_low_bounds[j]) { + m_status = INFEASIBLE; + m_infeasible_column_index = j; + set_upper_bound_witness(j, ci); + } + break; + case LE: + { + if (v < m_mpq_lar_core_solver.m_r_low_bounds[j]) { + m_status = INFEASIBLE; + m_infeasible_column_index = j; + set_upper_bound_witness(j, ci); + } + } + break; + case GT: + { + if (v >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) { + m_status = INFEASIBLE; + m_infeasible_column_index = j; + set_low_bound_witness(j, ci); + } + } + break; + case GE: + { + if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { + m_status = INFEASIBLE; + m_infeasible_column_index = j; + set_low_bound_witness(j, ci); + } + } + break; + case EQ: + { + if (v < m_mpq_lar_core_solver.m_r_low_bounds[j]) { + m_status = INFEASIBLE; + m_infeasible_column_index = j; + set_upper_bound_witness(j, ci); + } + else if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) { + m_status = INFEASIBLE; + m_infeasible_column_index = j; + set_low_bound_witness(j, ci); + } + break; + } + + default: + lean_unreachable(); + + } +} + + +} // namespace lean + + diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index b74515566..dbccbc9cf 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -30,1520 +30,421 @@ #include "util/lp/iterator_on_row.h" #include "util/lp/quick_xplain.h" #include "util/lp/conversion_helper.h" +#include "util/lp/int_solver.h" +#include "util/lp/nra_solver.h" + namespace lean { + class lar_solver : public column_namer { + class ext_var_info { + unsigned m_ext_j; // the external index + bool m_is_integer; + public: + ext_var_info(unsigned j): ext_var_info(j, false) {} + ext_var_info(unsigned j , bool is_int) : m_ext_j(j), m_is_integer(is_int) {} + unsigned ext_j() const { return m_ext_j;} + bool is_integer() const {return m_is_integer;} + }; //////////////////// fields ////////////////////////// - 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; + 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; // 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; + 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; + 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 { - return m_constraints.size(); - } - const lar_base_constraint& get_constraint(unsigned ci) const { - return *(m_constraints[ci]); - } + unsigned constraint_count() const; + const lar_base_constraint& get_constraint(unsigned ci) const; ////////////////// methods //////////////////////////////// - static_matrix> & A_r() { return m_mpq_lar_core_solver.m_r_A;} - static_matrix> const & A_r() const { return m_mpq_lar_core_solver.m_r_A;} - static_matrix & A_d() { return m_mpq_lar_core_solver.m_d_A;} - static_matrix const & A_d() const { return m_mpq_lar_core_solver.m_d_A;} + static_matrix> & A_r(); + static_matrix> const & A_r() const; + 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(unsigned j) const; + bool column_is_fixed(unsigned j) const; public: - lp_settings & settings() { return m_settings;} - lp_settings const & settings() const { return m_settings;} + // init region + bool strategy_is_undecided() const; - void clear() {lean_assert(false); // not implemented - } + var_index add_var(unsigned ext_j, bool is_integer); + void register_new_ext_var_index(unsigned ext_v, bool is_int); - lar_solver() : m_status(OPTIMAL), - m_infeasible_column_index(-1), - m_terms_start_index(1000000), - m_mpq_lar_core_solver(m_settings, *this) - {} + bool term_is_int(const lar_term * t) const; + + bool var_is_int(var_index v) const; + + bool ext_var_is_int(var_index ext_var) const; - void set_propagate_bounds_on_pivoted_rows_mode(bool v) { - m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows = v? (& m_rows_with_changed_bounds) : nullptr; - } + void add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int); - virtual ~lar_solver(){ - for (auto c : m_constraints) - delete c; - for (auto t : m_terms) - delete t; - for (auto t : m_orig_terms) - delete t; - } + void add_new_var_to_core_fields_for_doubles(bool register_in_basis); -#include "util/lp/init_lar_solver.h" + void add_new_var_to_core_fields_for_mpq(bool register_in_basis); + + + var_index add_term_undecided(const vector> & coeffs, + const mpq &m_v); + + // terms + var_index add_term(const vector> & coeffs, + const mpq &m_v); + + void add_row_for_term(const lar_term * term, unsigned term_ext_index); + + void add_row_from_term_no_constraint(const lar_term * term, unsigned term_ext_index); + + void add_basic_var_to_core_fields(); + + constraint_index add_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) ; + + void update_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_index); + + void add_var_bound_on_constraint_for_term(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci); + + + void add_constraint_from_term_and_create_new_column_row(unsigned term_j, const lar_term* term, + lconstraint_kind kind, const mpq & right_side); + + void decide_on_strategy_and_adjust_initial_state(); + + void adjust_initial_state(); + + void adjust_initial_state_for_lu(); + + void adjust_initial_state_for_tableau_rows(); + + // this fills the last row of A_d and sets the basis column: -1 in the last column of the row + void fill_last_row_of_A_d(static_matrix & A, const lar_term* ls); + + void update_free_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_ind); + + void update_upper_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci); - numeric_pair const& get_value(var_index vi) const { return m_mpq_lar_core_solver.m_r_x[vi]; } + void update_boxed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci); + void update_low_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci); - bool is_term(var_index j) const { - return j >= m_terms_start_index && j - m_terms_start_index < m_terms.size(); - } + void update_fixed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci); + //end of init region + lp_settings & settings(); - unsigned adjust_term_index(unsigned j) const { - lean_assert(is_term(j)); - return j - m_terms_start_index; - } + lp_settings const & settings() const; + + void clear(); - bool use_lu() const { return m_settings.simplex_strategy() == simplex_strategy_enum::lu; } - - bool sizes_are_correct() const { - lean_assert(strategy_is_undecided() || !m_mpq_lar_core_solver.need_to_presolve_with_double_solver() || A_r().column_count() == A_d().column_count()); - lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_column_types.size()); - lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); - lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_x.size()); - return true; - } + lar_solver(); + void set_propagate_bounds_on_pivoted_rows_mode(bool v); + + virtual ~lar_solver(); + + numeric_pair const& get_value(var_index vi) const; + + bool is_term(var_index j) const; + + unsigned adjust_term_index(unsigned j) const; + + + bool use_lu() const; + bool sizes_are_correct() const; - void print_implied_bound(const implied_bound& be, std::ostream & out) const { - out << "implied bound\n"; - unsigned v = be.m_j; - if (is_term(v)) { - out << "it is a term number " << be.m_j << std::endl; - print_term(*m_orig_terms[be.m_j - m_terms_start_index], out); - } - else { - out << get_column_name(v); - } - out << " " << lconstraint_kind_string(be.kind()) << " " << be.m_bound << std::endl; - // for (auto & p : be.m_explanation) { - // out << p.first << " : "; - // print_constraint(p.second, out); - // } - - // m_mpq_lar_core_solver.m_r_solver.print_column_info(be.m_j< m_terms_start_index? be.m_j : adjust_term_index(be.m_j), out); - out << "end of implied bound" << std::endl; - } + void print_implied_bound(const implied_bound& be, std::ostream & out) const; - bool implied_bound_is_correctly_explained(implied_bound const & be, const vector> & explanation) const { - std::unordered_map coeff_map; - auto rs_of_evidence = zero_of_type(); - unsigned n_of_G = 0, n_of_L = 0; - bool strict = false; - for (auto & it : explanation) { - mpq coeff = it.first; - constraint_index con_ind = it.second; - const auto & constr = *m_constraints[con_ind]; - lconstraint_kind kind = coeff.is_pos() ? constr.m_kind : flip_kind(constr.m_kind); - register_in_map(coeff_map, constr, coeff); - if (kind == GT || kind == LT) - strict = true; - if (kind == GE || kind == GT) n_of_G++; - else if (kind == LE || kind == LT) n_of_L++; - rs_of_evidence += coeff*constr.m_right_side; - } - lean_assert(n_of_G == 0 || n_of_L == 0); - lconstraint_kind kind = n_of_G ? GE : (n_of_L ? LE : EQ); - if (strict) - kind = static_cast((static_cast(kind) / 2)); - - if (!is_term(be.m_j)) { - if (coeff_map.size() != 1) - return false; - auto it = coeff_map.find(be.m_j); - if (it == coeff_map.end()) return false; - mpq ratio = it->second; - if (ratio < zero_of_type()) { - kind = static_cast(-kind); - } - rs_of_evidence /= ratio; - } else { - const lar_term * t = m_orig_terms[adjust_term_index(be.m_j)]; - const auto first_coeff = *t->m_coeffs.begin(); - unsigned j = first_coeff.first; - auto it = coeff_map.find(j); - if (it == coeff_map.end()) - return false; - mpq ratio = it->second / first_coeff.second; - for (auto & p : t->m_coeffs) { - it = coeff_map.find(p.first); - if (it == coeff_map.end()) - return false; - if (p.second * ratio != it->second) - return false; - } - if (ratio < zero_of_type()) { - kind = static_cast(-kind); - } - rs_of_evidence /= ratio; - rs_of_evidence += t->m_v * ratio; - } - - return kind == be.kind() && rs_of_evidence == be.m_bound; - } - + bool implied_bound_is_correctly_explained(implied_bound const & be, const vector> & explanation) const; void analyze_new_bounds_on_row( unsigned row_index, - bound_propagator & bp) { - lean_assert(!use_tableau()); - iterator_on_pivot_row it(m_mpq_lar_core_solver.get_pivot_row(), m_mpq_lar_core_solver.m_r_basis[row_index]); - - bound_analyzer_on_row ra_pos(it, - zero_of_type>(), - row_index, - bp - ); - ra_pos.analyze(); - } + bound_propagator & bp); void analyze_new_bounds_on_row_tableau( unsigned row_index, bound_propagator & bp - ) { - - if (A_r().m_rows[row_index].size() > settings().max_row_length_for_bound_propagation) - return; - iterator_on_row it(A_r().m_rows[row_index]); - lean_assert(use_tableau()); - bound_analyzer_on_row::analyze_row(it, - zero_of_type>(), - row_index, - bp ); - } - void substitute_basis_var_in_terms_for_row(unsigned i) { - // todo : create a map from term basic vars to the rows where they are used - unsigned basis_j = m_mpq_lar_core_solver.m_r_solver.m_basis[i]; - for (unsigned k = 0; k < m_terms.size(); k++) { - if (term_is_used_as_row(k)) - continue; - if (!m_terms[k]->contains(basis_j)) - continue; - m_terms[k]->subst(basis_j, m_mpq_lar_core_solver.m_r_solver.m_pivot_row); - } - } + void substitute_basis_var_in_terms_for_row(unsigned i); - void calculate_implied_bounds_for_row(unsigned i, bound_propagator & bp) { - if(use_tableau()) { - analyze_new_bounds_on_row_tableau(i, bp); - } else { - m_mpq_lar_core_solver.calculate_pivot_row(i); - substitute_basis_var_in_terms_for_row(i); - analyze_new_bounds_on_row(i, bp); - } - } + void calculate_implied_bounds_for_row(unsigned i, bound_propagator & bp); - /* - void process_new_implied_evidence_for_low_bound( - implied_bound_explanation& implied_evidence, // not pushed yet - vector & bound_evidences, - std::unordered_map & improved_low_bounds) { - - unsigned existing_index; - if (try_get_val(improved_low_bounds, implied_evidence.m_j, existing_index)) { - // we are improving the existent bound - bound_evidences[existing_index] = fill_bound_evidence(implied_evidence); - } else { - improved_low_bounds[implied_evidence.m_j] = bound_evidences.size(); - bound_evidences.push_back(fill_bound_evidence(implied_evidence)); - } - } - - void fill_bound_evidence_on_term(implied_bound & ie, implied_bound& be) { - lean_assert(false); - } - void fill_implied_bound_on_row(implied_bound & ie, implied_bound& be) { - iterator_on_row it(A_r().m_rows[ie.m_row_or_term_index]); - mpq a; unsigned j; - bool toggle = ie.m_coeff_before_j_is_pos; - if (!ie.m_is_low_bound) - toggle = !toggle; - while (it.next(a, j)) { - if (j == ie.m_j) continue; - const ul_pair & ul = m_vars_to_ul_pairs[j]; - - if (is_neg(a)) { // so the monoid has a positive coeff on the right side - constraint_index witness = toggle ? ul.m_low_bound_witness : ul.m_upper_bound_witness; - lean_assert(is_valid(witness)); - be.m_explanation.emplace_back(a, witness); - } - } - } - */ - /* - implied_bound fill_implied_bound_for_low_bound(implied_bound& ie) { - implied_bound be(ie.m_j, ie.m_bound.y.is_zero() ? GE : GT, ie.m_bound.x); - if (is_term(ie.m_row_or_term_index)) { - fill_implied_bound_for_low_bound_on_term(ie, be); - } - else { - fill_implied_bound_for_low_bound_on_row(ie, be); - } - return be; - } - - implied_bound fill_implied_bound_for_upper_bound(implied_bound& implied_evidence) { - lean_assert(false); - - be.m_j = implied_evidence.m_j; - be.m_bound = implied_evidence.m_bound.x; - be.m_kind = implied_evidence.m_bound.y.is_zero() ? LE : LT; - for (auto t : implied_evidence.m_vector_of_bound_signatures) { - const ul_pair & ul = m_vars_to_ul_pairs[t.m_column_index]; - constraint_index witness = t.m_low_bound ? ul.m_low_bound_witness : ul.m_upper_bound_witness; - lean_assert(is_valid(witness)); - be.m_explanation.emplace_back(t.m_coeff, witness); - } - - } - */ - /* - void process_new_implied_evidence_for_upper_bound( - implied_bound& implied_evidence, - vector & implied_bounds, - std::unordered_map & improved_upper_bounds) { - unsigned existing_index; - if (try_get_val(improved_upper_bounds, implied_evidence.m_j, existing_index)) { - implied_bound & be = implied_bounds[existing_index]; - be.m_explanation.clear(); - // we are improving the existent bound improve the existing bound - be = fill_implied_bound_for_upper_bound(implied_evidence); - } else { - improved_upper_bounds[implied_evidence.m_j] = implied_bounds.size(); - implied_bounds.push_back(fill_implied_bound_for_upper_bound(implied_evidence)); - } - } - */ - // implied_bound * get_existing_ - linear_combination_iterator * create_new_iter_from_term(unsigned term_index) const { - lean_assert(false); // not implemented - return nullptr; - // new linear_combination_iterator_on_vector(m_terms[adjust_term_index(term_index)]->coeffs_as_vector()); - } + linear_combination_iterator * create_new_iter_from_term(unsigned term_index) const; - unsigned adjust_column_index_to_term_index(unsigned j) const { - unsigned ext_var_or_term = m_columns_to_ext_vars_or_term_indices[j]; - return ext_var_or_term < m_terms_start_index ? j : ext_var_or_term; - } + unsigned adjust_column_index_to_term_index(unsigned j) const; - void propagate_bounds_on_a_term(const lar_term& t, bound_propagator & bp, unsigned term_offset) { - lean_assert(false); // not implemented - } + void propagate_bounds_on_a_term(const lar_term& t, bound_propagator & bp, unsigned term_offset); - void explain_implied_bound(implied_bound & ib, bound_propagator & bp) { - unsigned i = ib.m_row_or_term_index; - int bound_sign = ib.m_is_low_bound? 1: -1; - int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign; - unsigned m_j = ib.m_j; - if (is_term(m_j)) { - m_j = m_ext_vars_to_columns[m_j]; - } - for (auto const& r : A_r().m_rows[i]) { - unsigned j = r.m_j; - mpq const& a = r.get_val(); - if (j == m_j) continue; - if (is_term(j)) { - j = m_ext_vars_to_columns[j]; - } - int a_sign = is_pos(a)? 1: -1; - int sign = j_sign * a_sign; - const ul_pair & ul = m_vars_to_ul_pairs[j]; - auto witness = sign > 0? ul.upper_bound_witness(): ul.low_bound_witness(); - lean_assert(is_valid(witness)); - bp.consume(a, witness); - } - // lean_assert(implied_bound_is_correctly_explained(ib, explanation)); - } + void explain_implied_bound(implied_bound & ib, bound_propagator & bp); - bool term_is_used_as_row(unsigned term) const { - lean_assert(is_term(term)); - return contains(m_ext_vars_to_columns, term); - } + bool term_is_used_as_row(unsigned term) const; - void propagate_bounds_on_terms(bound_propagator & bp) { - for (unsigned i = 0; i < m_terms.size(); i++) { - if (term_is_used_as_row(i + m_terms_start_index)) - 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); - } - } + void propagate_bounds_on_terms(bound_propagator & bp); // goes over touched rows and tries to induce bounds - void propagate_bounds_for_touched_rows(bound_propagator & bp) { - if (!use_tableau()) - return; // ! todo : enable bound propagaion here. The current bug is that after the pop - // the changed terms become incorrect! + void propagate_bounds_for_touched_rows(bound_propagator & bp); - for (unsigned i : m_rows_with_changed_bounds.m_index) { - calculate_implied_bounds_for_row(i, bp); - } - m_rows_with_changed_bounds.clear(); - if (!use_tableau()) { - propagate_bounds_on_terms(bp); - } - } + lp_status get_status() const; - lp_status get_status() const { return m_status;} + void set_status(lp_status s); - void set_status(lp_status s) {m_status = s;} - - lp_status find_feasible_solution() { - if (strategy_is_undecided()) - decide_on_strategy_and_adjust_initial_state(); - - m_mpq_lar_core_solver.m_r_solver.m_look_for_feasible_solution_only = true; - return solve(); - } + lp_status find_feasible_solution(); - lp_status solve() { - if (m_status == INFEASIBLE) { - return m_status; - } - solve_with_core_solver(); - if (m_status != INFEASIBLE) { - if (m_settings.bound_propagation()) - detect_rows_with_changed_bounds(); - } - - m_columns_with_changed_bound.clear(); - return m_status; - } + lp_status solve(); - void fill_explanation_from_infeasible_column(vector> & evidence) const{ - - // this is the case when the lower bound is in conflict with the upper one - const ul_pair & ul = m_vars_to_ul_pairs[m_infeasible_column_index]; - evidence.push_back(std::make_pair(numeric_traits::one(), ul.upper_bound_witness())); - evidence.push_back(std::make_pair(-numeric_traits::one(), ul.low_bound_witness())); - } + void fill_explanation_from_infeasible_column(explanation_t & evidence) const; - unsigned get_total_iterations() const { return m_mpq_lar_core_solver.m_r_solver.total_iterations(); } + unsigned get_total_iterations() const; // see http://research.microsoft.com/projects/z3/smt07.pdf // This method searches for a feasible solution with as many different values of variables, reverenced in vars, as it can find // Attention, after a call to this method the non-basic variables don't necesserarly stick to their bounds anymore - vector get_list_of_all_var_indices() const { - vector ret; - for (unsigned j = 0; j < m_mpq_lar_core_solver.m_r_heading.size(); j++) - ret.push_back(j); - return ret; - } - void push() { - m_simplex_strategy = m_settings.simplex_strategy(); - m_simplex_strategy.push(); - m_status.push(); - m_vars_to_ul_pairs.push(); - m_infeasible_column_index.push(); - m_mpq_lar_core_solver.push(); - m_term_count = m_terms.size(); - m_term_count.push(); - m_constraint_count = m_constraints.size(); - m_constraint_count.push(); - } + vector get_list_of_all_var_indices() const; + void push(); - static void clean_large_elements_after_pop(unsigned n, int_set& set) { - vector to_remove; - for (unsigned j: set.m_index) - if (j >= n) - to_remove.push_back(j); - for (unsigned j : to_remove) - set.erase(j); - } + static void clean_large_elements_after_pop(unsigned n, int_set& set); - static void shrink_inf_set_after_pop(unsigned n, int_set & set) { - clean_large_elements_after_pop(n, set); - set.resize(n); - } + static void shrink_inf_set_after_pop(unsigned n, int_set & set); - void pop(unsigned k) { - int n_was = static_cast(m_ext_vars_to_columns.size()); - m_status.pop(k); - m_infeasible_column_index.pop(k); - unsigned n = m_vars_to_ul_pairs.peek_size(k); - for (unsigned j = n_was; j-- > n;) - m_ext_vars_to_columns.erase(m_columns_to_ext_vars_or_term_indices[j]); - m_columns_to_ext_vars_or_term_indices.resize(n); - if (m_settings.use_tableau()) { - pop_tableau(); - } - m_vars_to_ul_pairs.pop(k); - - m_mpq_lar_core_solver.pop(k); - clean_large_elements_after_pop(n, m_columns_with_changed_bound); - unsigned m = A_r().row_count(); - clean_large_elements_after_pop(m, m_rows_with_changed_bounds); - clean_inf_set_of_r_solver_after_pop(); - lean_assert(m_settings.simplex_strategy() == simplex_strategy_enum::undecided || - (!use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); - - - lean_assert(ax_is_correct()); - lean_assert(m_mpq_lar_core_solver.m_r_solver.inf_set_is_correct()); - m_constraint_count.pop(k); - for (unsigned i = m_constraint_count; i < m_constraints.size(); i++) - delete m_constraints[i]; - - m_constraints.resize(m_constraint_count); - m_term_count.pop(k); - for (unsigned i = m_term_count; i < m_terms.size(); i++) { - delete m_terms[i]; - delete m_orig_terms[i]; - } - m_terms.resize(m_term_count); - m_orig_terms.resize(m_term_count); - m_simplex_strategy.pop(k); - m_settings.simplex_strategy() = m_simplex_strategy; - lean_assert(sizes_are_correct()); - lean_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); - } + void pop(unsigned k); - vector get_all_constraint_indices() const { - vector ret; - constraint_index i = 0; - while ( i < m_constraints.size()) - ret.push_back(i++); - return ret; - } + vector get_all_constraint_indices() const; bool maximize_term_on_tableau(const vector> & term, - impq &term_max) { - if (settings().simplex_strategy() == simplex_strategy_enum::undecided) - decide_on_strategy_and_adjust_initial_state(); - - m_mpq_lar_core_solver.solve(); - if (m_mpq_lar_core_solver.m_r_solver.get_status() == UNBOUNDED) - return false; + impq &term_max); - term_max = 0; - for (auto & p : term) - term_max += p.first * m_mpq_lar_core_solver.m_r_x[p.second]; - - return true; - } - - bool costs_are_zeros_for_r_solver() const { - for (unsigned j = 0; j < m_mpq_lar_core_solver.m_r_solver.m_costs.size(); j++) { - lean_assert(is_zero(m_mpq_lar_core_solver.m_r_solver.m_costs[j])); - } - return true; - } - bool reduced_costs_are_zeroes_for_r_solver() const { - for (unsigned j = 0; j < m_mpq_lar_core_solver.m_r_solver.m_d.size(); j++) { - lean_assert(is_zero(m_mpq_lar_core_solver.m_r_solver.m_d[j])); - } - return true; - } + bool costs_are_zeros_for_r_solver() const; + bool reduced_costs_are_zeroes_for_r_solver() const; - void set_costs_to_zero(const vector> & term) { - auto & rslv = m_mpq_lar_core_solver.m_r_solver; - auto & jset = m_mpq_lar_core_solver.m_r_solver.m_inf_set; // hijack this set that should be empty right now - lean_assert(jset.m_index.size()==0); - - for (auto & p : term) { - unsigned j = p.second; - rslv.m_costs[j] = zero_of_type(); - int i = rslv.m_basis_heading[j]; - if (i < 0) - jset.insert(j); - else { - for (auto & rc : A_r().m_rows[i]) - jset.insert(rc.m_j); - } - } + void set_costs_to_zero(const vector> & term); - for (unsigned j : jset.m_index) - rslv.m_d[j] = zero_of_type(); - - jset.clear(); - - lean_assert(reduced_costs_are_zeroes_for_r_solver()); - lean_assert(costs_are_zeros_for_r_solver()); - } - - void prepare_costs_for_r_solver(const vector> & term) { - - auto & rslv = m_mpq_lar_core_solver.m_r_solver; - rslv.m_using_infeas_costs = false; - lean_assert(costs_are_zeros_for_r_solver()); - lean_assert(reduced_costs_are_zeroes_for_r_solver()); - rslv.m_costs.resize(A_r().column_count(), zero_of_type()); - for (auto & p : term) { - unsigned j = p.second; - rslv.m_costs[j] = p.first; - if (rslv.m_basis_heading[j] < 0) - rslv.m_d[j] += p.first; - else - rslv.update_reduced_cost_for_basic_column_cost_change(- p.first, j); - } - lean_assert(rslv.reduced_costs_are_correct_tableau()); - } + void prepare_costs_for_r_solver(const vector> & term); bool maximize_term_on_corrected_r_solver(const vector> & term, - impq &term_max) { - settings().backup_costs = 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(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(OPTIMAL); - return ret; - } - - case simplex_strategy_enum::lu: - lean_assert(false); // not implemented - return false; - default: - lean_unreachable(); // wrong mode - } - return false; - } + impq &term_max); // starting from a given feasible state look for the maximum of the term // return true if found and false if unbounded bool maximize_term(const vector> & term, - impq &term_max) { - lean_assert(m_mpq_lar_core_solver.m_r_solver.current_x_is_feasible()); - m_mpq_lar_core_solver.m_r_solver.m_look_for_feasible_solution_only = false; - return maximize_term_on_corrected_r_solver(term, term_max); - } + impq &term_max); - const lar_term & get_term(unsigned j) const { - lean_assert(j >= m_terms_start_index); - return *m_terms[j - m_terms_start_index]; - } + const lar_term & get_term(unsigned j) const; - void pop_core_solver_params() { - pop_core_solver_params(1); - } + void pop_core_solver_params(); - void pop_core_solver_params(unsigned k) { - A_r().pop(k); - A_d().pop(k); - } + void pop_core_solver_params(unsigned k); - void set_upper_bound_witness(var_index j, constraint_index ci) { - ul_pair ul = m_vars_to_ul_pairs[j]; - ul.upper_bound_witness() = ci; - m_vars_to_ul_pairs[j] = ul; - } + void set_upper_bound_witness(var_index j, constraint_index ci); - void set_low_bound_witness(var_index j, constraint_index ci) { - ul_pair ul = m_vars_to_ul_pairs[j]; - ul.low_bound_witness() = ci; - m_vars_to_ul_pairs[j] = ul; - } + void set_low_bound_witness(var_index j, constraint_index ci); - void substitute_terms(const mpq & mult, - const vector>& left_side_with_terms, - vector> &left_side, mpq & right_side) const { - for (auto & t : left_side_with_terms) { - if (t.second < m_terms_start_index) { - lean_assert(t.second < A_r().column_count()); - left_side.push_back(std::pair(mult * t.first, t.second)); - } else { - const lar_term & term = * m_terms[adjust_term_index(t.second)]; - substitute_terms(mult * t.first, left_side_with_terms, left_side, right_side); - right_side -= mult * term.m_v; - } - } - } + void substitute_terms_in_linear_expression( const vector>& left_side_with_terms, + vector> &left_side, mpq & right_side) const; - void detect_rows_of_bound_change_column_for_nbasic_column(unsigned j) { - if (A_r().row_count() != m_column_buffer.data_size()) - m_column_buffer.resize(A_r().row_count()); - else - m_column_buffer.clear(); - lean_assert(m_column_buffer.size() == 0 && m_column_buffer.is_OK()); - - m_mpq_lar_core_solver.m_r_solver.solve_Bd(j, m_column_buffer); - for (unsigned i : m_column_buffer.m_index) - m_rows_with_changed_bounds.insert(i); - } + void detect_rows_of_bound_change_column_for_nbasic_column(unsigned j); - void detect_rows_of_bound_change_column_for_nbasic_column_tableau(unsigned j) { - for (auto & rc : m_mpq_lar_core_solver.m_r_A.m_columns[j]) - m_rows_with_changed_bounds.insert(rc.m_i); - } + void detect_rows_of_bound_change_column_for_nbasic_column_tableau(unsigned j); - bool use_tableau() const { return m_settings.use_tableau(); } + bool use_tableau() const; - bool use_tableau_costs() const { - return m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs; - } + bool use_tableau_costs() const; - void detect_rows_of_column_with_bound_change(unsigned j) { - if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) { // it is a basic column - // just mark the row at touched and exit - m_rows_with_changed_bounds.insert(m_mpq_lar_core_solver.m_r_heading[j]); - return; - } + void detect_rows_of_column_with_bound_change(unsigned j); - if (use_tableau()) - detect_rows_of_bound_change_column_for_nbasic_column_tableau(j); - else - detect_rows_of_bound_change_column_for_nbasic_column(j); - } + void adjust_x_of_column(unsigned j); - void adjust_x_of_column(unsigned j) { - lean_assert(false); - } - - bool row_is_correct(unsigned i) const { - numeric_pair r = zero_of_type>(); - for (const auto & c : A_r().m_rows[i]) - r += c.m_value * m_mpq_lar_core_solver.m_r_x[c.m_j]; - return is_zero(r); - } + bool row_is_correct(unsigned i) const; - bool ax_is_correct() const { - for (unsigned i = 0; i < A_r().row_count(); i++) { - if (!row_is_correct(i)) - return false; - } - return true; - } + bool ax_is_correct() const; - bool tableau_with_costs() const { - return m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs; - } + bool tableau_with_costs() const; - bool costs_are_used() const { - return m_settings.simplex_strategy() != simplex_strategy_enum::tableau_rows; - } + bool costs_are_used() const; - void change_basic_x_by_delta_on_column(unsigned j, const numeric_pair & delta) { - if (use_tableau()) { - for (const auto & c : A_r().m_columns[j]) { - unsigned bj = m_mpq_lar_core_solver.m_r_basis[c.m_i]; - m_mpq_lar_core_solver.m_r_x[bj] -= A_r().get_val(c) * delta; - if (tableau_with_costs()) { - m_basic_columns_with_changed_cost.insert(bj); - } - m_mpq_lar_core_solver.m_r_solver.update_column_in_inf_set(bj); - } - } else { - m_column_buffer.clear(); - m_column_buffer.resize(A_r().row_count()); - m_mpq_lar_core_solver.m_r_solver.solve_Bd(j, m_column_buffer); - for (unsigned i : m_column_buffer.m_index) { - unsigned bj = m_mpq_lar_core_solver.m_r_basis[i]; - m_mpq_lar_core_solver.m_r_x[bj] -= m_column_buffer[i] * delta; - m_mpq_lar_core_solver.m_r_solver.update_column_in_inf_set(bj); - } - } - } + void change_basic_x_by_delta_on_column(unsigned j, const numeric_pair & delta); - void update_x_and_inf_costs_for_column_with_changed_bounds(unsigned j) { - if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) { - if (costs_are_used()) { - bool was_infeas = m_mpq_lar_core_solver.m_r_solver.m_inf_set.contains(j); - m_mpq_lar_core_solver.m_r_solver.update_column_in_inf_set(j); - if (was_infeas != m_mpq_lar_core_solver.m_r_solver.m_inf_set.contains(j)) - m_basic_columns_with_changed_cost.insert(j); - } else { - m_mpq_lar_core_solver.m_r_solver.update_column_in_inf_set(j); - } - } else { - numeric_pair delta; - if (m_mpq_lar_core_solver.m_r_solver.make_column_feasible(j, delta)) - change_basic_x_by_delta_on_column(j, delta); - } - } + void update_x_and_inf_costs_for_column_with_changed_bounds(unsigned j); - void detect_rows_with_changed_bounds_for_column(unsigned j) { - if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) { - m_rows_with_changed_bounds.insert(m_mpq_lar_core_solver.m_r_heading[j]); - return; - } - - if (use_tableau()) - detect_rows_of_bound_change_column_for_nbasic_column_tableau(j); - else - detect_rows_of_bound_change_column_for_nbasic_column(j); - } + void detect_rows_with_changed_bounds_for_column(unsigned j); - void detect_rows_with_changed_bounds() { - for (auto j : m_columns_with_changed_bound.m_index) - detect_rows_with_changed_bounds_for_column(j); - } + void detect_rows_with_changed_bounds(); - void update_x_and_inf_costs_for_columns_with_changed_bounds() { - for (auto j : m_columns_with_changed_bound.m_index) - update_x_and_inf_costs_for_column_with_changed_bounds(j); - } + void update_x_and_inf_costs_for_columns_with_changed_bounds(); - void update_x_and_inf_costs_for_columns_with_changed_bounds_tableau() { - lean_assert(ax_is_correct()); - for (auto j : m_columns_with_changed_bound.m_index) - update_x_and_inf_costs_for_column_with_changed_bounds(j); - - if (tableau_with_costs()) { - for (unsigned j : m_basic_columns_with_changed_cost.m_index) - m_mpq_lar_core_solver.m_r_solver.update_inf_cost_for_column_tableau(j); - lean_assert(m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); - } - } + void update_x_and_inf_costs_for_columns_with_changed_bounds_tableau(); - void solve_with_core_solver() { - if (!use_tableau()) - add_last_rows_to_lu(m_mpq_lar_core_solver.m_r_solver); - if (m_mpq_lar_core_solver.need_to_presolve_with_double_solver()) { - add_last_rows_to_lu(m_mpq_lar_core_solver.m_d_solver); - } - m_mpq_lar_core_solver.prefix_r(); - if (costs_are_used()) { - m_basic_columns_with_changed_cost.clear(); - m_basic_columns_with_changed_cost.resize(m_mpq_lar_core_solver.m_r_x.size()); - } - if (use_tableau()) - update_x_and_inf_costs_for_columns_with_changed_bounds_tableau(); - else - update_x_and_inf_costs_for_columns_with_changed_bounds(); - m_mpq_lar_core_solver.solve(); - set_status(m_mpq_lar_core_solver.m_r_solver.get_status()); - lean_assert(m_status != OPTIMAL || all_constraints_hold()); - } + void solve_with_core_solver(); - numeric_pair get_basic_var_value_from_row_directly(unsigned i) { - numeric_pair r = zero_of_type>(); - - unsigned bj = m_mpq_lar_core_solver.m_r_solver.m_basis[i]; - for (const auto & c: A_r().m_rows[i]) { - if (c.m_j == bj) continue; - const auto & x = m_mpq_lar_core_solver.m_r_x[c.m_j]; - if (!is_zero(x)) - r -= c.m_value * x; - } - return r; - } + numeric_pair get_basic_var_value_from_row_directly(unsigned i); - numeric_pair get_basic_var_value_from_row(unsigned i) { - if (settings().use_tableau()) { - return get_basic_var_value_from_row_directly(i); - } - - numeric_pair r = zero_of_type>(); - m_mpq_lar_core_solver.calculate_pivot_row(i); - for (unsigned j : m_mpq_lar_core_solver.m_r_solver.m_pivot_row.m_index) { - lean_assert(m_mpq_lar_core_solver.m_r_solver.m_basis_heading[j] < 0); - r -= m_mpq_lar_core_solver.m_r_solver.m_pivot_row.m_data[j] * m_mpq_lar_core_solver.m_r_x[j]; - } - return r; - } + numeric_pair get_basic_var_value_from_row(unsigned i); template - void add_last_rows_to_lu(lp_primal_core_solver & s) { - auto & f = s.m_factorization; - if (f != nullptr) { - auto columns_to_replace = f->get_set_of_columns_to_replace_for_add_last_rows(s.m_basis_heading); - if (f->m_refactor_counter + columns_to_replace.size() >= 200 || f->has_dense_submatrix()) { - delete f; - f = nullptr; - } else { - f->add_last_rows_to_B(s.m_basis_heading, columns_to_replace); - } - } - if (f == nullptr) { - init_factorization(f, s.m_A, s.m_basis, m_settings); - if (f->get_status() != LU_status::OK) { - delete f; - f = nullptr; - } - } - - } + void add_last_rows_to_lu(lp_primal_core_solver & s); - bool x_is_correct() const { - if (m_mpq_lar_core_solver.m_r_x.size() != A_r().column_count()) { - // std::cout << "the size is off " << m_r_solver.m_x.size() << ", " << A().column_count() << std::endl; - return false; - } - for (unsigned i = 0; i < A_r().row_count(); i++) { - numeric_pair delta = A_r().dot_product_with_row(i, m_mpq_lar_core_solver.m_r_x); - if (!delta.is_zero()) { - // std::cout << "x is off ("; - // std::cout << "m_b[" << i << "] = " << m_b[i] << " "; - // std::cout << "left side = " << A().dot_product_with_row(i, m_r_solver.m_x) << ' '; - // std::cout << "delta = " << delta << ' '; - // std::cout << "iters = " << total_iterations() << ")" << std::endl; - // std::cout << "row " << i << " is off" << std::endl; - return false; - } - } - return true;; - - } + bool x_is_correct() const; - bool var_is_registered(var_index vj) const { - if (vj >= m_terms_start_index) { - if (vj - m_terms_start_index >= m_terms.size()) - return false; - } else if ( vj >= A_r().column_count()) { - return false; - } - return true; - } + bool var_is_registered(var_index vj) const; - unsigned constraint_stack_size() const { - return m_constraint_count.stack_size(); - } + unsigned constraint_stack_size() const; - void fill_last_row_of_A_r(static_matrix> & A, const lar_term * ls) { - lean_assert(A.row_count() > 0); - lean_assert(A.column_count() > 0); - unsigned last_row = A.row_count() - 1; - lean_assert(A.m_rows[last_row].size() == 0); - for (auto & t : ls->m_coeffs) { - lean_assert(!is_zero(t.second)); - var_index j = t.first; - A.set(last_row, j, - t.second); - } - unsigned basis_j = A.column_count() - 1; - A.set(last_row, basis_j, mpq(1)); - } + void fill_last_row_of_A_r(static_matrix> & A, const lar_term * ls); template - void create_matrix_A(static_matrix & matr) { - lean_assert(false); // not implemented - /* - unsigned m = number_or_nontrivial_left_sides(); - unsigned n = m_vec_of_canonic_left_sides.size(); - if (matr.row_count() == m && matr.column_count() == n) - return; - matr.init_empty_matrix(m, n); - copy_from_mpq_matrix(matr); - */ - } + void create_matrix_A(static_matrix & matr); template - void copy_from_mpq_matrix(static_matrix & matr) { - matr.m_rows.resize(A_r().row_count()); - matr.m_columns.resize(A_r().column_count()); - for (unsigned i = 0; i < matr.row_count(); i++) { - for (auto & it : A_r().m_rows[i]) { - matr.set(i, it.m_j, convert_struct::convert(it.get_val())); - } - } - } + void copy_from_mpq_matrix(static_matrix & matr); - bool try_to_set_fixed(column_info & ci) { - if (ci.upper_bound_is_set() && ci.low_bound_is_set() && ci.get_upper_bound() == ci.get_low_bound() && !ci.is_fixed()) { - ci.set_fixed_value(ci.get_upper_bound()); - return true; - } - return false; - } + bool try_to_set_fixed(column_info & ci); - column_type get_column_type(const column_info & ci) { - auto ret = ci.get_column_type_no_flipping(); - if (ret == column_type::boxed) { // changing boxed to fixed because of the no span - if (ci.get_low_bound() == ci.get_upper_bound()) - ret = column_type::fixed; - } - return ret; - } + column_type get_column_type(const column_info & ci); - std::string get_column_name(unsigned j) const { - if (j >= m_terms_start_index) - return std::string("_t") + T_to_string(j); - if (j >= m_columns_to_ext_vars_or_term_indices.size()) - return std::string("_s") + T_to_string(j); + std::string get_column_name(unsigned j) const; - return std::string("v") + T_to_string(m_columns_to_ext_vars_or_term_indices[j]); - } + bool all_constrained_variables_are_registered(const vector>& left_side); - bool all_constrained_variables_are_registered(const vector>& left_side) { - for (auto it : left_side) { - if (! var_is_registered(it.second)) - return false; - } - return true; - } + constraint_index add_constraint(const vector>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm); + bool all_constraints_hold() const; + bool constraint_holds(const lar_base_constraint & constr, std::unordered_map & var_map) const; + bool the_relations_are_of_same_type(const vector> & evidence, lconstraint_kind & the_kind_of_sum) const; - constraint_index add_constraint(const vector>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm) { - /* - mpq rs = right_side_parm; - vector> left_side; - substitute_terms(one_of_type(), left_side_with_terms, left_side, rs); - lean_assert(left_side.size() > 0); - lean_assert(all_constrained_variables_are_registered(left_side)); - lar_constraint original_constr(left_side, kind_par, rs); - unsigned j; // j is the index of the basic variables corresponding to the left side - canonic_left_side ls = create_or_fetch_canonic_left_side(left_side, j); - mpq ratio = find_ratio_of_original_constraint_to_normalized(ls, original_constr); - auto kind = ratio.is_neg() ? flip_kind(kind_par) : kind_par; - rs/= ratio; - lar_normalized_constraint normalized_constraint(ls, ratio, kind, rs, original_constr); - m_constraints.push_back(normalized_constraint); - constraint_index constr_ind = m_constraints.size() - 1; - update_column_type_and_bound(j, kind, rs, constr_ind); - return constr_ind; - */ - lean_assert(false); // not implemented - return 0; - } + static void register_in_map(std::unordered_map & coeffs, const lar_base_constraint & cn, const mpq & a); + static void register_one_coeff_in_map(std::unordered_map & coeffs, const mpq & a, unsigned j); - bool all_constraints_hold() const { - if (m_settings.get_cancel_flag()) - return true; - std::unordered_map var_map; - get_model(var_map); + + bool the_left_sides_sum_to_zero(const vector> & evidence) const; + + bool the_right_sides_do_not_sum_to_zero(const vector> & evidence); + + bool explanation_is_correct(const vector>& explanation) const; + + bool inf_explanation_is_correct() const; + + mpq sum_of_right_sides_of_explanation(const vector> & explanation) const; + + bool has_lower_bound(var_index var, constraint_index& ci, mpq& value, bool& is_strict); - for (unsigned i = 0; i < m_constraints.size(); i++) { - if (!constraint_holds(*m_constraints[i], var_map)) { - print_constraint(i, std::cout); - return false; - } - } - return true; - } - - bool constraint_holds(const lar_base_constraint & constr, std::unordered_map & var_map) const { - mpq left_side_val = get_left_side_val(constr, var_map); - switch (constr.m_kind) { - case LE: return left_side_val <= constr.m_right_side; - case LT: return left_side_val < constr.m_right_side; - case GE: return left_side_val >= constr.m_right_side; - case GT: return left_side_val > constr.m_right_side; - case EQ: return left_side_val == constr.m_right_side; - default: - lean_unreachable(); - } - return false; // it is unreachable - } + bool has_upper_bound(var_index var, constraint_index& ci, mpq& value, bool& is_strict); - - - - - - bool the_relations_are_of_same_type(const vector> & evidence, lconstraint_kind & the_kind_of_sum) const { - unsigned n_of_G = 0, n_of_L = 0; - bool strict = false; - for (auto & it : evidence) { - mpq coeff = it.first; - constraint_index con_ind = it.second; - lconstraint_kind kind = coeff.is_pos() ? - m_constraints[con_ind]->m_kind : - flip_kind(m_constraints[con_ind]->m_kind); - if (kind == GT || kind == LT) - strict = true; - if (kind == GE || kind == GT) n_of_G++; - else if (kind == LE || kind == LT) n_of_L++; - } - the_kind_of_sum = n_of_G ? GE : (n_of_L ? LE : EQ); - if (strict) - the_kind_of_sum = static_cast((static_cast(the_kind_of_sum) / 2)); - - return n_of_G == 0 || n_of_L == 0; - } - - static void register_in_map(std::unordered_map & coeffs, const lar_base_constraint & cn, const mpq & a) { - for (auto & it : cn.get_left_side_coefficients()) { - unsigned j = it.second; - auto p = coeffs.find(j); - if (p == coeffs.end()) - coeffs[j] = it.first * a; - else { - p->second += it.first * a; - if (p->second.is_zero()) - coeffs.erase(p); - } - } - } - bool the_left_sides_sum_to_zero(const vector> & evidence) const { - std::unordered_map coeff_map; - for (auto & it : evidence) { - mpq coeff = it.first; - constraint_index con_ind = it.second; - lean_assert(con_ind < m_constraints.size()); - register_in_map(coeff_map, *m_constraints[con_ind], coeff); - } - - if (!coeff_map.empty()) { - std::cout << "left side = "; - vector> t; - for (auto & it : coeff_map) { - t.push_back(std::make_pair(it.second, it.first)); - } - print_linear_combination_of_column_indices(t, std::cout); - std::cout << std::endl; - return false; - } - - return true; - } - - bool the_right_sides_do_not_sum_to_zero(const vector> & evidence) { - mpq ret = numeric_traits::zero(); - for (auto & it : evidence) { - mpq coeff = it.first; - constraint_index con_ind = it.second; - lean_assert(con_ind < m_constraints.size()); - const lar_constraint & constr = *m_constraints[con_ind]; - ret += constr.m_right_side * coeff; - } - return !numeric_traits::is_zero(ret); - } - - bool explanation_is_correct(const vector>& explanation) const { -#ifdef LEAN_DEBUG - lconstraint_kind kind; - lean_assert(the_relations_are_of_same_type(explanation, kind)); - lean_assert(the_left_sides_sum_to_zero(explanation)); - mpq rs = sum_of_right_sides_of_explanation(explanation); - switch (kind) { - case LE: lean_assert(rs < zero_of_type()); - break; - case LT: lean_assert(rs <= zero_of_type()); - break; - case GE: lean_assert(rs > zero_of_type()); - break; - case GT: lean_assert(rs >= zero_of_type()); - break; - case EQ: lean_assert(rs != zero_of_type()); - break; - default: - lean_assert(false); - return false; - } -#endif - return true; - } - - bool inf_explanation_is_correct() const { -#ifdef LEAN_DEBUG - vector> explanation; - get_infeasibility_explanation(explanation); - return explanation_is_correct(explanation); -#endif - return true; - } - - mpq sum_of_right_sides_of_explanation(const vector> & explanation) const { - mpq ret = numeric_traits::zero(); - for (auto & it : explanation) { - mpq coeff = it.first; - constraint_index con_ind = it.second; - lean_assert(con_ind < m_constraints.size()); - ret += (m_constraints[con_ind]->m_right_side - m_constraints[con_ind]->get_free_coeff_of_left_side()) * coeff; - } - return ret; - } - - bool has_lower_bound(var_index var, constraint_index& ci, mpq& value, bool& is_strict) { - - if (var >= m_vars_to_ul_pairs.size()) { - // TBD: bounds on terms could also be used, caller may have to track these. - return false; - } - const ul_pair & ul = m_vars_to_ul_pairs[var]; - ci = ul.low_bound_witness(); - if (ci != static_cast(-1)) { - auto& p = m_mpq_lar_core_solver.m_r_low_bounds()[var]; - value = p.x; - is_strict = p.y.is_pos(); - return true; - } - else { - return false; - } - } - - bool has_upper_bound(var_index var, constraint_index& ci, mpq& value, bool& is_strict) { - - if (var >= m_vars_to_ul_pairs.size()) { - // TBD: bounds on terms could also be used, caller may have to track these. - return false; - } - const ul_pair & ul = m_vars_to_ul_pairs[var]; - ci = ul.upper_bound_witness(); - if (ci != static_cast(-1)) { - auto& p = m_mpq_lar_core_solver.m_r_upper_bounds()[var]; - value = p.x; - is_strict = p.y.is_neg(); - return true; - } - else { - return false; - } - } - - - void get_infeasibility_explanation(vector> & explanation) const { - explanation.clear(); - if (m_infeasible_column_index != -1) { - fill_explanation_from_infeasible_column(explanation); - return; - } - if (m_mpq_lar_core_solver.get_infeasible_sum_sign() == 0) { - return; - } - // the infeasibility sign - int inf_sign; - auto inf_row = m_mpq_lar_core_solver.get_infeasibility_info(inf_sign); - get_infeasibility_explanation_for_inf_sign(explanation, inf_row, inf_sign); - lean_assert(explanation_is_correct(explanation)); - } + void get_infeasibility_explanation(vector> & explanation) const; void get_infeasibility_explanation_for_inf_sign( vector> & explanation, const vector> & inf_row, - int inf_sign) const { - - for (auto & it : inf_row) { - mpq coeff = it.first; - unsigned j = it.second; - - int adj_sign = coeff.is_pos() ? inf_sign : -inf_sign; - const ul_pair & ul = m_vars_to_ul_pairs[j]; - - constraint_index bound_constr_i = adj_sign < 0 ? ul.upper_bound_witness() : ul.low_bound_witness(); - lean_assert(bound_constr_i < m_constraints.size()); - explanation.push_back(std::make_pair(coeff, bound_constr_i)); - } - } + int inf_sign) const; - void get_model(std::unordered_map & variable_values) const { - mpq delta = mpq(1, 2); // start from 0.5 to have less clashes - lean_assert(m_status == OPTIMAL); - unsigned i; - do { - - // different pairs have to produce different singleton values - std::unordered_set set_of_different_pairs; - std::unordered_set set_of_different_singles; - delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta); - for (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]; - set_of_different_pairs.insert(rp); - mpq x = rp.x + delta * rp.y; - set_of_different_singles.insert(x); - if (set_of_different_pairs.size() - != set_of_different_singles.size()) { - delta /= mpq(2); - break; - } - - variable_values[i] = x; - } - } while (i != m_mpq_lar_core_solver.m_r_x.size()); - } + void get_model(std::unordered_map & variable_values) const; - std::string get_variable_name(var_index vi) const { - return get_column_name(vi); - } + std::string get_variable_name(var_index vi) const; // ********** print region start - void print_constraint(constraint_index ci, std::ostream & out) const { - if (ci >= m_constraints.size()) { - out << "constraint " << T_to_string(ci) << " is not found"; - out << std::endl; - return; - } + void print_constraint(constraint_index ci, std::ostream & out) const; - print_constraint(m_constraints[ci], out); - } + void print_constraints(std::ostream& out) const ; - void print_constraints(std::ostream& out) const { - for (auto c : m_constraints) { - print_constraint(c, out); - } - } + void print_terms(std::ostream& out) const ; - void print_terms(std::ostream& out) const { - for (auto it : m_terms) { - print_term(*it, out); - out << "\n"; - } - } + void print_left_side_of_constraint(const lar_base_constraint * c, std::ostream & out) const; - void print_left_side_of_constraint(const lar_base_constraint * c, std::ostream & out) const { - print_linear_combination_of_column_indices(c->get_left_side_coefficients(), out); - mpq free_coeff = c->get_free_coeff_of_left_side(); - if (!is_zero(free_coeff)) - out << " + " << free_coeff; - - } + void print_term(lar_term const& term, std::ostream & out) const; - void print_term(lar_term const& term, std::ostream & out) const { - if (!numeric_traits::is_zero(term.m_v)) { - out << term.m_v << " + "; - } - print_linear_combination_of_column_indices(term.coeffs_as_vector(), out); - } + mpq get_left_side_val(const lar_base_constraint & cns, const std::unordered_map & var_map) const; - mpq get_left_side_val(const lar_base_constraint & cns, const std::unordered_map & var_map) const { - mpq ret = cns.get_free_coeff_of_left_side(); - for (auto & it : cns.get_left_side_coefficients()) { - var_index j = it.second; - auto vi = var_map.find(j); - lean_assert(vi != var_map.end()); - ret += it.first * vi->second; - } - return ret; - } + void print_constraint(const lar_base_constraint * c, std::ostream & out) const; - void print_constraint(const lar_base_constraint * c, std::ostream & out) const { - print_left_side_of_constraint(c, out); - out << " " << lconstraint_kind_string(c->m_kind) << " " << c->m_right_side << std::endl; - } + void fill_var_set_for_random_update(unsigned sz, var_index const * vars, vector& column_list); - void fill_var_set_for_random_update(unsigned sz, var_index const * vars, vector& column_list) { - for (unsigned i = 0; i < sz; i++) { - var_index var = vars[i]; - if (var >= m_terms_start_index) { // handle the term - for (auto & it : m_terms[var - m_terms_start_index]->m_coeffs) { - column_list.push_back(it.first); - } - } else { - column_list.push_back(var); - } - } - } + void random_update(unsigned sz, var_index const * vars); + void pivot_fixed_vars_from_basis(); + void pop(); + bool column_represents_row_in_tableau(unsigned j); + void make_sure_that_the_bottom_right_elem_not_zero_in_tableau(unsigned i, unsigned j); + void remove_last_row_and_column_from_tableau(unsigned j); + void remove_last_column_from_tableau(unsigned j); - void random_update(unsigned sz, var_index const * vars) { - vector column_list; - fill_var_set_for_random_update(sz, vars, column_list); - random_updater ru(m_mpq_lar_core_solver, column_list); - ru.update(); - } + void remove_last_column_from_basis_tableau(unsigned j); + void remove_column_from_tableau(unsigned j); + void pop_tableau(); + void clean_inf_set_of_r_solver_after_pop(); + void shrink_explanation_to_minimum(vector> & explanation) const; - - void try_pivot_fixed_vars_from_basis() { - m_mpq_lar_core_solver.m_r_solver.pivot_fixed_vars_from_basis(); - } - - void pop() { - pop(1); - } - - - bool column_represents_row_in_tableau(unsigned j) { - return m_vars_to_ul_pairs()[j].m_i != static_cast(-1); - } - - void make_sure_that_the_bottom_right_elem_not_zero_in_tableau(unsigned i, unsigned j) { - // i, j - is the indices of the bottom-right element of the tableau - lean_assert(A_r().row_count() == i + 1 && A_r().column_count() == j + 1); - auto & last_column = A_r().m_columns[j]; - int non_zero_column_cell_index = -1; - for (unsigned k = last_column.size(); k-- > 0;){ - auto & cc = last_column[k]; - if (cc.m_i == i) - return; - non_zero_column_cell_index = k; - } - - lean_assert(non_zero_column_cell_index != -1); - lean_assert(static_cast(non_zero_column_cell_index) != i); - m_mpq_lar_core_solver.m_r_solver.transpose_rows_tableau(last_column[non_zero_column_cell_index].m_i, i); - } - - void remove_last_row_and_column_from_tableau(unsigned j) { - lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); - auto & slv = m_mpq_lar_core_solver.m_r_solver; - unsigned i = A_r().row_count() - 1; //last row index - make_sure_that_the_bottom_right_elem_not_zero_in_tableau(i, j); - if (slv.m_basis_heading[j] < 0) { - slv.pivot_column_tableau(j, i); - } - - auto & last_row = A_r().m_rows[i]; - mpq &cost_j = m_mpq_lar_core_solver.m_r_solver.m_costs[j]; - bool cost_is_nz = !is_zero(cost_j); - for (unsigned k = last_row.size(); k-- > 0;) { - auto &rc = last_row[k]; - if (cost_is_nz) { - m_mpq_lar_core_solver.m_r_solver.m_d[rc.m_j] += cost_j*rc.get_val(); - } - - A_r().remove_element(last_row, rc); - } - lean_assert(last_row.size() == 0); - lean_assert(A_r().m_columns[j].size() == 0); - A_r().m_rows.pop_back(); - A_r().m_columns.pop_back(); - slv.m_b.pop_back(); - } - - void remove_last_column_from_tableau(unsigned j) { - lean_assert(j == A_r().column_count() - 1); - // the last column has to be empty - lean_assert(A_r().m_columns[j].size() == 0); - A_r().m_columns.pop_back(); - } - - void remove_last_column_from_basis_tableau(unsigned j) { - auto& rslv = m_mpq_lar_core_solver.m_r_solver; - int i = rslv.m_basis_heading[j]; - if (i >= 0) { // j is a basic var - int last_pos = static_cast(rslv.m_basis.size()) - 1; - lean_assert(last_pos >= 0); - if (i != last_pos) { - unsigned j_at_last_pos = rslv.m_basis[last_pos]; - rslv.m_basis[i] = j_at_last_pos; - rslv.m_basis_heading[j_at_last_pos] = i; - } - rslv.m_basis.pop_back(); // remove j from the basis - } else { - int last_pos = static_cast(rslv.m_nbasis.size()) - 1; - lean_assert(last_pos >= 0); - i = - 1 - i; - if (i != last_pos) { - unsigned j_at_last_pos = rslv.m_nbasis[last_pos]; - rslv.m_nbasis[i] = j_at_last_pos; - rslv.m_basis_heading[j_at_last_pos] = - i - 1; - } - rslv.m_nbasis.pop_back(); // remove j from the basis - } - rslv.m_basis_heading.pop_back(); - lean_assert(rslv.m_basis.size() == A_r().row_count()); - lean_assert(rslv.basis_heading_is_correct()); - } - - void remove_column_from_tableau(unsigned j) { - auto& rslv = m_mpq_lar_core_solver.m_r_solver; - lean_assert(j == A_r().column_count() - 1); - lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); - if (column_represents_row_in_tableau(j)) { - remove_last_row_and_column_from_tableau(j); - if (rslv.m_basis_heading[j] < 0) - rslv.change_basis_unconditionally(j, rslv.m_basis[A_r().row_count()]); // A_r().row_count() is the index of the last row in the basis still - } - else { - remove_last_column_from_tableau(j); - } - rslv.m_x.pop_back(); - rslv.m_d.pop_back(); - rslv.m_costs.pop_back(); - - remove_last_column_from_basis_tableau(j); - lean_assert(m_mpq_lar_core_solver.r_basis_is_OK()); - lean_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); - } - - - void pop_tableau() { - lean_assert(m_mpq_lar_core_solver.m_r_solver.m_costs.size() == A_r().column_count()); - - lean_assert(m_mpq_lar_core_solver.m_r_solver.m_basis.size() == A_r().row_count()); - lean_assert(m_mpq_lar_core_solver.m_r_solver.basis_heading_is_correct()); - // We remove last variables starting from m_column_names.size() to m_vec_of_canonic_left_sides.size(). - // At this moment m_column_names is already popped - for (unsigned j = A_r().column_count(); j-- > m_columns_to_ext_vars_or_term_indices.size();) - remove_column_from_tableau(j); - lean_assert(m_mpq_lar_core_solver.m_r_solver.m_costs.size() == A_r().column_count()); - lean_assert(m_mpq_lar_core_solver.m_r_solver.m_basis.size() == A_r().row_count()); - lean_assert(m_mpq_lar_core_solver.m_r_solver.basis_heading_is_correct()); - } - - - - - void clean_inf_set_of_r_solver_after_pop() { - vector became_feas; - clean_large_elements_after_pop(A_r().column_count(), m_mpq_lar_core_solver.m_r_solver.m_inf_set); - std::unordered_set basic_columns_with_changed_cost; - auto inf_index_copy = m_mpq_lar_core_solver.m_r_solver.m_inf_set.m_index; - for (auto j: inf_index_copy) { - if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) { - continue; - } - // some basic columns might become non-basic - these columns need to be made feasible - numeric_pair delta; - if (m_mpq_lar_core_solver.m_r_solver.make_column_feasible(j, delta)) - change_basic_x_by_delta_on_column(j, delta); - became_feas.push_back(j); - } - - for (unsigned j : became_feas) { - lean_assert(m_mpq_lar_core_solver.m_r_solver.m_basis_heading[j] < 0); - m_mpq_lar_core_solver.m_r_solver.m_d[j] -= m_mpq_lar_core_solver.m_r_solver.m_costs[j]; - m_mpq_lar_core_solver.m_r_solver.m_costs[j] = zero_of_type(); - m_mpq_lar_core_solver.m_r_solver.m_inf_set.erase(j); - } - became_feas.clear(); - for (unsigned j : m_mpq_lar_core_solver.m_r_solver.m_inf_set.m_index) { - lean_assert(m_mpq_lar_core_solver.m_r_heading[j] >= 0); - if (m_mpq_lar_core_solver.m_r_solver.column_is_feasible(j)) - became_feas.push_back(j); - } - for (unsigned j : became_feas) - m_mpq_lar_core_solver.m_r_solver.m_inf_set.erase(j); - if (use_tableau_costs()) { - for (unsigned j : became_feas) - m_mpq_lar_core_solver.m_r_solver.update_inf_cost_for_column_tableau(j); - for (unsigned j : basic_columns_with_changed_cost) - m_mpq_lar_core_solver.m_r_solver.update_inf_cost_for_column_tableau(j); - lean_assert(m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); - } - } - - - void shrink_explanation_to_minimum(vector> & explanation) const { - // implementing quickXplain - quick_xplain::run(explanation, *this); - lean_assert(this->explanation_is_correct(explanation)); + bool column_value_is_integer(unsigned j) const { + const impq & v = m_mpq_lar_core_solver.m_r_x[j]; + return v.is_int(); } + + bool column_is_real(unsigned j) const { + return !column_is_int(j); + } + + bool model_is_int_feasible() const; + + const impq & column_low_bound(unsigned j) const { + return m_mpq_lar_core_solver.low_bound(j); + } + + const impq & column_upper_bound(unsigned j) const { + return m_mpq_lar_core_solver.upper_bound(j); + } + + bool column_is_bounded(unsigned j) const { + return m_mpq_lar_core_solver.column_is_bounded(j); + } + + void get_bound_constraint_witnesses_for_column(unsigned j, constraint_index & lc, constraint_index & uc) const { + const ul_pair & ul = m_vars_to_ul_pairs[j]; + lc = ul.low_bound_witness(); + uc = ul.upper_bound_witness(); + } + indexed_vector & get_column_in_lu_mode(unsigned j) { + m_column_buffer.clear(); + m_column_buffer.resize(A_r().row_count()); + m_mpq_lar_core_solver.m_r_solver.solve_Bd(j, m_column_buffer); + return m_column_buffer; + } + + bool bound_is_integer_if_needed(unsigned j, const mpq & right_side) const; }; } diff --git a/src/util/lp/lar_solver_instances.cpp b/src/util/lp/lar_solver_instances.cpp new file mode 100644 index 000000000..98f59edb9 --- /dev/null +++ b/src/util/lp/lar_solver_instances.cpp @@ -0,0 +1,13 @@ +/* + Copyright (c) 2017 Microsoft Corporation + Author: Lev Nachmanson +*/ + +#include "util/lp/lar_solver.cpp" + +template void lean::lar_solver::copy_from_mpq_matrix(class lean::static_matrix &); + + + + + diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h index a12b7b5d2..925206680 100644 --- a/src/util/lp/lp_core_solver_base.h +++ b/src/util/lp/lp_core_solver_base.h @@ -429,6 +429,7 @@ public: void init_lu(); int pivots_in_column_and_row_are_different(int entering, int leaving) const; void pivot_fixed_vars_from_basis(); + bool pivot_column_general(unsigned j, unsigned j_basic, indexed_vector & w); bool pivot_for_tableau_on_basis(); bool pivot_row_for_tableau_on_basis(unsigned row); void init_basic_part_of_basis_heading() { @@ -568,8 +569,8 @@ public: default: lean_assert(false); } - std::cout << "basis heading = " << m_basis_heading[j] << std::endl; - std::cout << "x = " << m_x[j] << std::endl; + out << "basis heading = " << m_basis_heading[j] << std::endl; + out << "x = " << m_x[j] << std::endl; /* std::cout << "cost = " << m_costs[j] << std::endl; std:: cout << "m_d = " << m_d[j] << std::endl;*/ diff --git a/src/util/lp/lp_core_solver_base.hpp b/src/util/lp/lp_core_solver_base.hpp index a0dba9de7..d551daf27 100644 --- a/src/util/lp/lp_core_solver_base.hpp +++ b/src/util/lp/lp_core_solver_base.hpp @@ -923,7 +923,27 @@ template void lp_core_solver_base::transpose_row transpose_basis(i, j); m_A.transpose_rows(i, j); } - +// j is the new basic column, j_basic - the leaving column +template bool lp_core_solver_base::pivot_column_general(unsigned j, unsigned j_basic, indexed_vector & w) { + unsigned row_index = m_basis_heading[j_basic]; + change_basis(j, j_basic); + if (m_settings.m_simplex_strategy == simplex_strategy_enum::lu) { + if (m_factorization->need_to_refactor()) { + init_lu(); + } else { + m_factorization->prepare_entering(j, w); // to init vector w + m_factorization->replace_column(zero_of_type(), w, row_index); + } + if (m_factorization->get_status() != LU_status::OK) { + change_basis(j_basic, j); + init_lu(); + return false; + } + } else { // the tableau case + pivot_column_tableau(j, row_index); + } + return true; +} template void lp_core_solver_base::pivot_fixed_vars_from_basis() { // run over basis and non-basis at the same time indexed_vector w(m_basis.size()); // the buffer @@ -943,22 +963,9 @@ template void lp_core_solver_base::pivot_fixed_v if (j >= m_nbasis.size()) break; j++; - if (m_factorization->need_to_refactor()) { - change_basis(jj, ii); - init_lu(); - } else { - m_factorization->prepare_entering(jj, w); // to init vector w - m_factorization->replace_column(zero_of_type(), w, m_basis_heading[ii]); - change_basis(jj, ii); - } - if (m_factorization->get_status() != LU_status::OK) { - change_basis(ii, jj); - init_lu(); - } else { + if (!pivot_column_general(jj, ii, w)) break; - } - } - lean_assert(m_factorization->get_status()== LU_status::OK); + } } } diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index aac3692f9..736e4cda4 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -16,13 +16,16 @@ namespace lean { typedef unsigned var_index; typedef unsigned constraint_index; typedef unsigned row_index; + +typedef vector> explanation_t; + enum class column_type { free_column = 0, - low_bound = 1, - upper_bound = 2, - boxed = 3, - fixed = 4 - }; + low_bound = 1, + upper_bound = 2, + boxed = 3, + fixed = 4 +}; enum class simplex_strategy_enum { undecided = 3, @@ -75,11 +78,14 @@ public: }; struct stats { + unsigned m_make_feasible; unsigned m_total_iterations; unsigned m_iters_with_no_cost_growing; unsigned m_num_factorizations; unsigned m_num_of_implied_bounds; unsigned m_need_to_solve_inf; + unsigned m_max_cols; + unsigned m_max_rows; stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } }; @@ -198,7 +204,8 @@ public: use_breakpoints_in_feasibility_search(false), max_row_length_for_bound_propagation(300), backup_costs(true), - column_number_threshold_for_using_lu_in_lar_solver(4000) + column_number_threshold_for_using_lu_in_lar_solver(4000), + m_int_branch_cut_threshold(10000000) {} void set_resource_limit(lp_resource_limit& lim) { m_resource_limit = &lim; } @@ -278,13 +285,13 @@ public: return m_simplex_strategy; } - bool use_lu() const { - return m_simplex_strategy == simplex_strategy_enum::lu; - } + bool use_lu() const { + return m_simplex_strategy == simplex_strategy_enum::lu; + } bool use_tableau() const { - return m_simplex_strategy == simplex_strategy_enum::tableau_rows || - m_simplex_strategy == simplex_strategy_enum::tableau_costs; + return m_simplex_strategy == simplex_strategy_enum::tableau_rows || + m_simplex_strategy == simplex_strategy_enum::tableau_costs; } bool use_tableau_rows() const { @@ -305,6 +312,7 @@ public: unsigned max_row_length_for_bound_propagation; bool backup_costs; unsigned column_number_threshold_for_using_lu_in_lar_solver; + unsigned m_int_branch_cut_threshold; }; // end of lp_settings class diff --git a/src/util/lp/lp_settings_instances.cpp b/src/util/lp/lp_settings_instances.cpp index e9a3888ba..ac2ed4b51 100644 --- a/src/util/lp/lp_settings_instances.cpp +++ b/src/util/lp/lp_settings_instances.cpp @@ -2,8 +2,8 @@ Copyright (c) 2017 Microsoft Corporation Author: Lev Nachmanson */ -#include "util/vector.h" #include +#include "util/vector.h" #include "util/lp/lp_settings.hpp" template bool lean::vectors_are_equal(vector const&, vector const&); template bool lean::vectors_are_equal(vector const&, vector const&); diff --git a/src/util/lp/mps_reader.h b/src/util/lp/mps_reader.h index 4c793d56e..eb83735ca 100644 --- a/src/util/lp/mps_reader.h +++ b/src/util/lp/mps_reader.h @@ -810,7 +810,7 @@ public: auto kind = get_lar_relation_from_row(row->m_type); vector> ls; for (auto s : row->m_row_columns) { - var_index i = solver->add_var(get_var_index(s.first)); + var_index i = solver->add_var(get_var_index(s.first), false); ls.push_back(std::make_pair(s.second, i)); } solver->add_constraint(ls, kind, row->m_right_side); @@ -828,20 +828,20 @@ public: void create_low_constraint_for_var(column* col, bound * b, lar_solver *solver) { vector> ls; - var_index i = solver->add_var(col->m_index); + var_index i = solver->add_var(col->m_index, false); ls.push_back(std::make_pair(numeric_traits::one(), i)); solver->add_constraint(ls, GE, b->m_low); } void create_upper_constraint_for_var(column* col, bound * b, lar_solver *solver) { - var_index i = solver->add_var(col->m_index); + var_index i = solver->add_var(col->m_index, false); vector> ls; ls.push_back(std::make_pair(numeric_traits::one(), i)); solver->add_constraint(ls, LE, b->m_upper); } void create_equality_contraint_for_var(column* col, bound * b, lar_solver *solver) { - var_index i = solver->add_var(col->m_index); + var_index i = solver->add_var(col->m_index, false); vector> ls; ls.push_back(std::make_pair(numeric_traits::one(), i)); solver->add_constraint(ls, EQ, b->m_fixed_value); @@ -850,7 +850,7 @@ public: void fill_lar_solver_on_columns(lar_solver * solver) { for (auto s : m_columns) { mps_reader::column * col = s.second; - solver->add_var(col->m_index); + solver->add_var(col->m_index, false); auto b = col->m_bound; if (b == nullptr) return; diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp new file mode 100644 index 000000000..81372be32 --- /dev/null +++ b/src/util/lp/nra_solver.cpp @@ -0,0 +1,264 @@ +/* + Copyright (c) 2017 Microsoft Corporation + Author: Lev Nachmanson +*/ + +#include "util/lp/lar_solver.h" +#include "util/lp/nra_solver.h" +#include "nlsat/nlsat_solver.h" +#include "math/polynomial/polynomial.h" +#include "math/polynomial/algebraic_numbers.h" +#include "util/map.h" + + +namespace nra { + + struct mon_eq { + mon_eq(lean::var_index v, unsigned sz, lean::var_index const* vs): + m_v(v), m_vs(sz, vs) {} + lean::var_index m_v; + svector m_vs; + }; + + struct solver::imp { + lean::lar_solver& s; + reslimit& m_limit; + params_ref m_params; + u_map m_lp2nl; // map from lar_solver variables to nlsat::solver variables + scoped_ptr m_nlsat; + vector m_monomials; + unsigned_vector m_monomials_lim; + mutable std::unordered_map m_variable_values; // current model + + imp(lean::lar_solver& s, reslimit& lim, params_ref const& p): + s(s), + m_limit(lim), + m_params(p) { + } + + bool need_check() { + return !m_monomials.empty() && !check_assignments(); + } + + void add(lean::var_index v, unsigned sz, lean::var_index const* vs) { + m_monomials.push_back(mon_eq(v, sz, vs)); + } + + void push() { + m_monomials_lim.push_back(m_monomials.size()); + } + + void pop(unsigned n) { + if (n == 0) return; + m_monomials.shrink(m_monomials_lim[m_monomials_lim.size() - n]); + m_monomials_lim.shrink(m_monomials_lim.size() - n); + } + + /* + \brief Check if polynomials are well defined. + multiply values for vs and check if they are equal to value for v. + epsilon has been computed. + */ + bool check_assignment(mon_eq const& m) const { + rational r1 = m_variable_values[m.m_v]; + rational r2(1); + for (auto w : m.m_vs) { + r2 *= m_variable_values[w]; + } + return r1 == r2; + } + + bool check_assignments() const { + s.get_model(m_variable_values); + for (auto const& m : m_monomials) { + if (!check_assignment(m)) return false; + } + return true; + } + + /** + \brief one-shot nlsat check. + A one shot checker is the least functionality that can + enable non-linear reasoning. + In addition to checking satisfiability we would also need + to identify equalities in the model that should be assumed + with the remaining solver. + + TBD: use partial model from lra_solver to prime the state of nlsat_solver. + TBD: explore more incremental ways of applying nlsat (using assumptions) + */ + lbool check(lean::explanation_t& ex) { + SASSERT(need_check()); + m_nlsat = alloc(nlsat::solver, m_limit, m_params); + m_lp2nl.reset(); + vector core; + + // add linear inequalities from lra_solver + for (unsigned i = 0; i < s.constraint_count(); ++i) { + add_constraint(i); + } + + // add polynomial definitions. + for (auto const& m : m_monomials) { + add_monomial_eq(m); + } + // TBD: add variable bounds? + + lbool r = m_nlsat->check(); + TRACE("arith", m_nlsat->display(tout << r << "\n");); + switch (r) { + case l_true: + break; + case l_false: + ex.reset(); + m_nlsat->get_core(core); + for (auto c : core) { + unsigned idx = static_cast(static_cast(c) - this); + ex.push_back(std::pair(rational(1), idx)); + TRACE("arith", tout << "ex: " << idx << "\n";); + } + break; + + case l_undef: + break; + } + return r; + } + + void add_monomial_eq(mon_eq const& m) { + polynomial::manager& pm = m_nlsat->pm(); + svector vars; + for (auto v : m.m_vs) { + vars.push_back(lp2nl(v)); + } + polynomial::monomial_ref m1(pm.mk_monomial(vars.size(), vars.c_ptr()), pm); + polynomial::monomial_ref m2(pm.mk_monomial(lp2nl(m.m_v), 1), pm); + polynomial::monomial* mls[2] = { m1, m2 }; + polynomial::scoped_numeral_vector coeffs(pm.m()); + coeffs.push_back(mpz(1)); + coeffs.push_back(mpz(-1)); + polynomial::polynomial_ref p(pm.mk_polynomial(2, coeffs.c_ptr(), mls), pm); + polynomial::polynomial* ps[1] = { p }; + bool even[1] = { false }; + nlsat::literal lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, even); + m_nlsat->mk_clause(1, &lit, 0); + } + + void add_constraint(unsigned idx) { + auto& c = s.get_constraint(idx); + auto& pm = m_nlsat->pm(); + auto k = c.m_kind; + auto rhs = c.m_right_side; + auto lhs = c.get_left_side_coefficients(); + auto sz = lhs.size(); + svector vars; + rational den = denominator(rhs); + for (auto kv : lhs) { + vars.push_back(lp2nl(kv.second)); + den = lcm(den, denominator(kv.first)); + } + vector coeffs; + for (auto kv : lhs) { + coeffs.push_back(den * kv.first); + } + rhs *= den; + polynomial::polynomial_ref p(pm.mk_linear(sz, coeffs.c_ptr(), vars.c_ptr(), -rhs), pm); + polynomial::polynomial* ps[1] = { p }; + bool is_even[1] = { false }; + nlsat::literal lit; + nlsat::assumption a = this + idx; + switch (k) { + case lean::lconstraint_kind::LE: + lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even); + break; + case lean::lconstraint_kind::GE: + lit = ~m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even); + break; + case lean::lconstraint_kind::LT: + lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::LT, 1, ps, is_even); + break; + case lean::lconstraint_kind::GT: + lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::GT, 1, ps, is_even); + break; + case lean::lconstraint_kind::EQ: + lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, is_even); + break; + } + m_nlsat->mk_clause(1, &lit, a); + } + + bool is_int(lean::var_index v) { + return s.var_is_int(v); + } + + + polynomial::var lp2nl(lean::var_index v) { + polynomial::var r; + if (!m_lp2nl.find(v, r)) { + r = m_nlsat->mk_var(is_int(v)); + m_lp2nl.insert(v, r); + } + return r; + } + + nlsat::anum const& value(lean::var_index v) const { + return m_nlsat->value(m_lp2nl.find(v)); + } + + nlsat::anum_manager& am() { + return m_nlsat->am(); + } + + std::ostream& display(std::ostream& out) const { + for (auto m : m_monomials) { + out << "v" << m.m_v << " = "; + for (auto v : m.m_vs) { + out << "v" << v << " "; + } + out << "\n"; + } + return out; + } + }; + + solver::solver(lean::lar_solver& s, reslimit& lim, params_ref const& p) { + m_imp = alloc(imp, s, lim, p); + } + + solver::~solver() { + dealloc(m_imp); + } + + void solver::add_monomial(lean::var_index v, unsigned sz, lean::var_index const* vs) { + m_imp->add(v, sz, vs); + } + + lbool solver::check(lean::explanation_t& ex) { + return m_imp->check(ex); + } + + bool solver::need_check() { + return m_imp->need_check(); + } + + void solver::push() { + m_imp->push(); + } + + void solver::pop(unsigned n) { + m_imp->pop(n); + } + + std::ostream& solver::display(std::ostream& out) const { + return m_imp->display(out); + } + + nlsat::anum const& solver::value(lean::var_index v) const { + return m_imp->value(v); + } + + nlsat::anum_manager& solver::am() { + return m_imp->am(); + } + +} diff --git a/src/util/lp/nra_solver.h b/src/util/lp/nra_solver.h new file mode 100644 index 000000000..0b02e7136 --- /dev/null +++ b/src/util/lp/nra_solver.h @@ -0,0 +1,70 @@ +/* + Copyright (c) 2017 Microsoft Corporation + Author: Lev Nachmanson +*/ + +#pragma once +#include "util/vector.h" +#include "util/lp/lp_settings.h" +#include "util/rlimit.h" +#include "util/params.h" +#include "nlsat/nlsat_solver.h" + +namespace lean { + class lar_solver; +} + + +namespace nra { + + + + class solver { + struct imp; + imp* m_imp; + + public: + + solver(lean::lar_solver& s, reslimit& lim, params_ref const& p = params_ref()); + + ~solver(); + + /* + \brief Add a definition v = vs[0]*vs[1]*...*vs[sz-1] + The variable v is equal to the product of variables vs. + */ + void add_monomial(lean::var_index v, unsigned sz, lean::var_index const* vs); + + /* + \brief Check feasiblity of linear constraints augmented by polynomial definitions + that are added. + */ + lbool check(lean::explanation_t& ex); + + /* + \brief determine whether nra check is needed. + */ + bool need_check(); + + /* + \brief Access model. + */ + nlsat::anum const& value(lean::var_index v) const; + + nlsat::anum_manager& am(); + + /* + \brief push and pop scope. + Monomial definitions are retraced when popping scope. + */ + void push(); + + void pop(unsigned n); + + /* + \brief display state + */ + std::ostream& display(std::ostream& out) const; + + }; +} diff --git a/src/util/lp/numeric_pair.h b/src/util/lp/numeric_pair.h index 84c99b3b1..db7b71119 100644 --- a/src/util/lp/numeric_pair.h +++ b/src/util/lp/numeric_pair.h @@ -199,6 +199,11 @@ struct numeric_pair { std::string to_string() const { return std::string("(") + T_to_string(x) + ", " + T_to_string(y) + ")"; } + + bool is_int() const { + return x.is_int() && y.is_zero(); + } + }; @@ -324,4 +329,26 @@ struct convert_struct { template bool is_epsilon_small(const X & v, const double &eps) { return convert_struct::is_epsilon_small(v, eps);} template bool below_bound_numeric(const X & x, const X & bound, const double& eps) { return convert_struct::below_bound_numeric(x, bound, eps);} template bool above_bound_numeric(const X & x, const X & bound, const double& eps) { return convert_struct::above_bound_numeric(x, bound, eps);} +template T floor(const numeric_pair & r) { + if (r.x.is_int()) { + if (r.y.is_nonneg()) { + return r.x; + } + return r.x - mpq::one(); + } + + return floor(r.x); +} + +template T ceil(const numeric_pair & r) { + if (r.x.is_int()) { + if (r.y.is_nonpos()) { + return r.x; + } + return r.x + mpq::one(); + } + + return ceil(r.x); +} + } diff --git a/src/util/lp/quick_xplain.cpp b/src/util/lp/quick_xplain.cpp index a4b6fb0e6..df409240e 100644 --- a/src/util/lp/quick_xplain.cpp +++ b/src/util/lp/quick_xplain.cpp @@ -20,7 +20,7 @@ void quick_xplain::copy_constraint_and_add_constraint_vars(const lar_constraint& vector < std::pair> ls; for (auto & p : lar_c.get_left_side_coefficients()) { unsigned j = p.second; - unsigned lj = m_qsol.add_var(j); + unsigned lj = m_qsol.add_var(j, false); ls.push_back(std::make_pair(p.first, lj)); } m_constraints_in_local_vars.push_back(lar_constraint(ls, lar_c.m_kind, lar_c.m_right_side)); @@ -94,7 +94,7 @@ bool quick_xplain::is_feasible(const vector & x, unsigned k) const { vector < std::pair> ls; const lar_constraint & c = m_constraints_in_local_vars[i]; for (auto & p : c.get_left_side_coefficients()) { - unsigned lj = l.add_var(p.second); + unsigned lj = l.add_var(p.second, false); ls.push_back(std::make_pair(p.first, lj)); } l.add_constraint(ls, c.m_kind, c.m_right_side); diff --git a/src/util/lp/stacked_vector.h b/src/util/lp/stacked_vector.h index 3f39dd346..14b0d0141 100644 --- a/src/util/lp/stacked_vector.h +++ b/src/util/lp/stacked_vector.h @@ -32,7 +32,10 @@ public: operator const B&() const { return m_vec.m_vector[m_i]; } - + + bool operator==(B const& other) const { + return m_vec.m_vector[m_i] == other; + } }; class ref_const { diff --git a/src/util/lp/static_matrix_instances.cpp b/src/util/lp/static_matrix_instances.cpp index d0e2045c0..59905929e 100644 --- a/src/util/lp/static_matrix_instances.cpp +++ b/src/util/lp/static_matrix_instances.cpp @@ -2,8 +2,8 @@ Copyright (c) 2017 Microsoft Corporation Author: Lev Nachmanson */ -#include "util/vector.h" #include +#include "util/vector.h" #include #include #include "util/lp/static_matrix.hpp"