From c82aa5edce52ad1761cf099d809d879781eecba6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 28 Jun 2017 13:12:12 -0700 Subject: [PATCH] Dev (#56) * introduce int_solver.h Signed-off-by: Lev Nachmanson * add int_solver class Signed-off-by: Lev Nachmanson * track which var is an integer Signed-off-by: Lev Nachmanson * add queries for integrality of vars Signed-off-by: Lev Nachmanson * resurrect lp_tst in its own director lp Signed-off-by: Lev Nachmanson * add file Signed-off-by: Lev Nachmanson * add_constraint has got a body Signed-off-by: Lev Nachmanson * fix add_constraint and substitute_terms_in_linear_expression Signed-off-by: Lev Nachmanson * after merge with Z3Prover Signed-off-by: Lev Nachmanson * adding stub check_int_feasibility() Signed-off-by: Lev Nachmanson * Dev (#50) * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * small fix in lar_solver.cpp Signed-off-by: Lev Nachmanson * adding some content to the new check_int_feasibility() Signed-off-by: Lev Nachmanson * Dev (#51) * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * adding more nlsat Signed-off-by: Nikolaj Bjorner * nlsat integration Signed-off-by: Nikolaj Bjorner * adding constraints Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * add missing initialization Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * test Signed-off-by: Lev Nachmanson * Dev (#53) * change in a comment Signed-off-by: Lev Nachmanson * Disabled debug output * removing FOCI2 interface from interp * remove foci reference from cmakelist.txt Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * adding more nlsat Signed-off-by: Nikolaj Bjorner * nlsat integration Signed-off-by: Nikolaj Bjorner * adding constraints Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * add missing initialization Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * adding nra Signed-off-by: Nikolaj Bjorner * debugging nra Signed-off-by: Nikolaj Bjorner * updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver Signed-off-by: Nikolaj Bjorner * n/a Signed-off-by: Nikolaj Bjorner * integrate nlsat Signed-off-by: Nikolaj Bjorner * tidy Signed-off-by: Nikolaj Bjorner * preserve is_int flag Signed-off-by: Lev Nachmanson * remove a debug printout Signed-off-by: Lev Nachmanson * Dev (#54) * change in a comment Signed-off-by: Lev Nachmanson * Disabled debug output * removing FOCI2 interface from interp * remove foci reference from cmakelist.txt Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * adding more nlsat Signed-off-by: Nikolaj Bjorner * nlsat integration Signed-off-by: Nikolaj Bjorner * adding constraints Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * add missing initialization Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * adding nra Signed-off-by: Nikolaj Bjorner * debugging nra Signed-off-by: Nikolaj Bjorner * updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver Signed-off-by: Nikolaj Bjorner * n/a Signed-off-by: Nikolaj Bjorner * integrate nlsat Signed-off-by: Nikolaj Bjorner * tidy Signed-off-by: Nikolaj Bjorner * use integer test from lra solver, updated it to work on term variables Signed-off-by: Nikolaj Bjorner * fix equality check in assume-eq Signed-off-by: Nikolaj Bjorner * fix model_is_int_feasible Signed-off-by: Lev Nachmanson * untested gcd_test() Signed-off-by: Lev Nachmanson * call fill_explanation_from_fixed_columns() Signed-off-by: Lev Nachmanson * add the call to pivot_fixed_vars_from_basis() to int_solver.cpp::check() Signed-off-by: Lev Nachmanson * port more of theory_arith_int.h Signed-off-by: Lev Nachmanson * use statistics of lar_solver by theory_lra.cpp Signed-off-by: Lev Nachmanson * port more code to int_solver.cpp Signed-off-by: Lev Nachmanson * add an assert Signed-off-by: Lev Nachmanson * more int porting Signed-off-by: Lev Nachmanson * fix a bug in pivot_fixed_vars_from_basis Signed-off-by: Lev Nachmanson * small change Signed-off-by: Lev Nachmanson * implement find_inf_int_base_column() Signed-off-by: Lev Nachmanson * catch unregistered vars in add_var_bound Signed-off-by: Lev Nachmanson * add a file Signed-off-by: Lev Nachmanson * compile for vs2012 Signed-off-by: Lev Nachmanson * fix asserts in add_var_bound Signed-off-by: Lev Nachmanson * fix the lp_solver init when workig on an mps file Signed-off-by: Lev Nachmanson * towards int_solver::check() Signed-off-by: Lev Nachmanson * change in int_solver::check() signature Signed-off-by: Lev Nachmanson * add handlers for lia moves Signed-off-by: Nikolaj Bjorner * spacing Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 1 - src/ast/rewriter/arith_rewriter.cpp | 129 +- src/ast/rewriter/arith_rewriter.h | 5 +- src/ast/simplifier/arith_simplifier_plugin.h | 97 + src/math/polynomial/polynomial.h | 21 +- src/nlsat/nlsat_solver.h | 8 +- src/nlsat/nlsat_types.h | 8 +- src/sat/sat_types.h | 13 +- src/shell/lp_frontend.cpp | 1 - src/smt/theory_lra.cpp | 438 ++-- src/test/CMakeLists.txt | 2 + src/test/lp/CMakeLists.txt | 6 + src/test/{ => lp}/argument_parser.h | 0 src/test/{ => lp}/lp.cpp | 51 +- src/test/lp/lp_main.cpp | 14 + src/test/{ => lp}/smt_reader.h | 2 +- src/test/{ => lp}/test_file_reader.h | 0 src/util/lp/CMakeLists.txt | 5 + src/util/lp/indexed_vector.h | 2 +- src/util/lp/init_lar_solver.h | 591 ----- src/util/lp/int_solver.cpp | 606 ++++++ src/util/lp/int_solver.h | 100 + src/util/lp/lar_core_solver.h | 31 + src/util/lp/lar_solver.cpp | 2040 ++++++++++++++++++ src/util/lp/lar_solver.h | 276 +-- src/util/lp/lar_solver_instances.cpp | 13 + src/util/lp/lp_core_solver_base.h | 5 +- src/util/lp/lp_core_solver_base.hpp | 36 +- src/util/lp/lp_settings.h | 20 +- src/util/lp/mps_reader.h | 10 +- src/util/lp/nra_solver.cpp | 264 +++ src/util/lp/nra_solver.h | 70 + src/util/lp/numeric_pair.h | 27 + src/util/lp/quick_xplain.cpp | 4 +- src/util/lp/stacked_vector.h | 5 +- src/util/lp/static_matrix_instances.cpp | 6 + 36 files changed, 3785 insertions(+), 1122 deletions(-) create mode 100644 src/ast/simplifier/arith_simplifier_plugin.h create mode 100644 src/test/lp/CMakeLists.txt rename src/test/{ => lp}/argument_parser.h (100%) rename src/test/{ => lp}/lp.cpp (98%) create mode 100644 src/test/lp/lp_main.cpp rename src/test/{ => lp}/smt_reader.h (99%) rename src/test/{ => lp}/test_file_reader.h (100%) delete mode 100644 src/util/lp/init_lar_solver.h create mode 100644 src/util/lp/int_solver.cpp create mode 100644 src/util/lp/int_solver.h create mode 100644 src/util/lp/lar_solver.cpp create mode 100644 src/util/lp/lar_solver_instances.cpp create mode 100644 src/util/lp/nra_solver.cpp create mode 100644 src/util/lp/nra_solver.h diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 1b1be9b52..15de24ec5 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1714,7 +1714,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 379020331..9c166eb63 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -800,105 +800,56 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu result = m_util.mk_numeral(div(v1, v2), is_int); return BR_DONE; } - if (m_util.is_numeral(arg2, v2, is_int) && v2.is_one()) { - result = arg1; - return BR_DONE; - } if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) { - return BR_FAILED; + result = m_util.mk_idiv0(arg1); + return BR_REWRITE1; } - if (arg1 == arg2) { - expr_ref zero(m_util.mk_int(0), m()); - result = m().mk_ite(m().mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1)); - return BR_REWRITE3; - } - if (divides(arg1, arg2, result)) { - return BR_REWRITE_FULL; + 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; } - -// -// implement div ab ac = floor( ab / ac) = floor (b / c) = div b c -// -bool arith_rewriter::divides(expr* num, expr* den, expr_ref& result) { - expr_fast_mark1 mark; - rational num_r(1), den_r(1); - expr* num_e = nullptr, *den_e = nullptr; - ptr_buffer args1, args2; - flat_mul(num, args1); - flat_mul(den, args2); - for (expr * arg : args1) { - mark.mark(arg); - if (m_util.is_numeral(arg, num_r)) num_e = arg; - } - for (expr* arg : args2) { - if (mark.is_marked(arg)) { - result = remove_divisor(arg, num, den); - return true; - } - if (m_util.is_numeral(arg, den_r)) den_e = arg; - } - rational g = gcd(num_r, den_r); - if (!g.is_one()) { - SASSERT(g.is_pos()); - // replace num_e, den_e by their gcd reduction. - for (unsigned i = 0; i < args1.size(); ++i) { - if (args1[i] == num_e) { - args1[i] = m_util.mk_numeral(num_r / g, true); - break; - } - } - for (unsigned i = 0; i < args2.size(); ++i) { - if (args2[i] == den_e) { - args2[i] = m_util.mk_numeral(den_r / g, true); - break; - } - } - - num = m_util.mk_mul(args1.size(), args1.c_ptr()); - den = m_util.mk_mul(args2.size(), args2.c_ptr()); - result = m_util.mk_idiv(num, den); +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; } - return false; -} - -expr_ref arith_rewriter::remove_divisor(expr* arg, expr* num, expr* den) { - ptr_buffer args1, args2; - flat_mul(num, args1); - flat_mul(den, args2); - remove_divisor(arg, args1); - remove_divisor(arg, args2); - expr_ref zero(m_util.mk_int(0), m()); - num = args1.empty() ? m_util.mk_int(1) : m_util.mk_mul(args1.size(), args1.c_ptr()); - den = args2.empty() ? m_util.mk_int(1) : m_util.mk_mul(args2.size(), args2.c_ptr()); - return expr_ref(m().mk_ite(m().mk_eq(zero, arg), m_util.mk_idiv(zero, zero), m_util.mk_idiv(num, den)), m()); -} - -void arith_rewriter::flat_mul(expr* e, ptr_buffer& args) { - args.push_back(e); - for (unsigned i = 0; i < args.size(); ++i) { - e = args[i]; - if (m_util.is_mul(e)) { - args.append(to_app(e)->get_num_args(), to_app(e)->get_args()); - args[i] = args.back(); - args.shrink(args.size()-1); - --i; - } - } -} - -void arith_rewriter::remove_divisor(expr* d, ptr_buffer& args) { - for (unsigned i = 0; i < args.size(); ++i) { - if (args[i] == d) { - args[i] = args.back(); - args.shrink(args.size()-1); - return; + 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; + } + } } } - UNREACHABLE(); + return false; } br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) { diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index fa8677941..65fbfb43f 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -95,10 +95,7 @@ class arith_rewriter : public poly_rewriter { expr_ref neg_monomial(expr * e) const; expr * mk_sin_value(rational const & k); app * mk_sqrt(rational const & k); - bool divides(expr* d, expr* n, expr_ref& result); - expr_ref remove_divisor(expr* arg, expr* num, expr* den); - void flat_mul(expr* e, ptr_buffer& args); - void remove_divisor(expr* d, ptr_buffer& args); + 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.h b/src/ast/simplifier/arith_simplifier_plugin.h new file mode 100644 index 000000000..045ee0e71 --- /dev/null +++ b/src/ast/simplifier/arith_simplifier_plugin.h @@ -0,0 +1,97 @@ +/*++ +Copyright (c) 2007 Microsoft Corporation + +Module Name: + + arith_simplifier_plugin.h + +Abstract: + + Simplifier for the arithmetic family. + +Author: + + Leonardo (leonardo) 2008-01-08 + +--*/ +#ifndef ARITH_SIMPLIFIER_PLUGIN_H_ +#define ARITH_SIMPLIFIER_PLUGIN_H_ + +#include"basic_simplifier_plugin.h" +#include"poly_simplifier_plugin.h" +#include"arith_decl_plugin.h" +#include"arith_simplifier_params.h" + +/** + \brief Simplifier for the arith family. +*/ +class arith_simplifier_plugin : public poly_simplifier_plugin { +public: + enum op_kind { + LE, GE, EQ + }; +protected: + arith_simplifier_params & m_params; + arith_util m_util; + basic_simplifier_plugin & m_bsimp; + expr_ref m_int_zero; + expr_ref m_real_zero; + + bool is_neg_poly(expr * t) const; + + template + void mk_le_ge_eq_core(expr * arg1, expr * arg2, expr_ref & result); + + void prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result); + + void gcd_reduce_monomial(expr_ref_vector& monomials, numeral& k); + + 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); + ~arith_simplifier_plugin(); + arith_util & get_arith_util() { return m_util; } + virtual numeral norm(const numeral & n) { return n; } + virtual bool is_numeral(expr * n, rational & val) const { bool f; return m_util.is_numeral(n, val, f); } + bool is_numeral(expr * n) const { return m_util.is_numeral(n); } + virtual bool is_minus_one(expr * n) const { numeral tmp; return is_numeral(n, tmp) && tmp.is_minus_one(); } + virtual expr * get_zero(sort * s) const { return m_util.is_int(s) ? m_int_zero.get() : m_real_zero.get(); } + + virtual app * mk_numeral(numeral const & n) { return m_util.mk_numeral(n, m_curr_sort->get_decl_kind() == INT_SORT); } + app * mk_numeral(numeral const & n, bool is_int) { return m_util.mk_numeral(n, is_int); } + bool is_int_sort(sort const * s) const { return m_util.is_int(s); } + bool is_real_sort(sort const * s) const { return m_util.is_real(s); } + bool is_arith_sort(sort const * s) const { return is_int_sort(s) || is_real_sort(s); } + bool is_int(expr const * n) const { return m_util.is_int(n); } + bool is_le(expr const * n) const { return m_util.is_le(n); } + bool is_ge(expr const * n) const { return m_util.is_ge(n); } + + virtual bool is_le_ge(expr * n) const { return is_le(n) || is_ge(n); } + + void mk_le(expr * arg1, expr * arg2, expr_ref & result); + void mk_ge(expr * arg1, expr * arg2, expr_ref & result); + void mk_lt(expr * arg1, expr * arg2, expr_ref & result); + void mk_gt(expr * arg1, expr * arg2, expr_ref & result); + void mk_arith_eq(expr * arg1, expr * arg2, expr_ref & result); + void mk_div(expr * arg1, expr * arg2, expr_ref & result); + void mk_idiv(expr * arg1, expr * arg2, expr_ref & result); + void mk_mod(expr * arg1, expr * arg2, expr_ref & result); + void mk_rem(expr * arg1, expr * arg2, expr_ref & result); + void mk_to_real(expr * arg, expr_ref & result); + void mk_to_int(expr * arg, expr_ref & result); + void mk_is_int(expr * arg, expr_ref & result); + void mk_abs(expr * arg, expr_ref & result); + + virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); + virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result); + + bool is_arith_term(expr * n) const; + + void gcd_normalize(numeral & coeff, expr_ref& term); + +}; + +#endif /* ARITH_SIMPLIFIER_PLUGIN_H_ */ diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h index 374a51084..1f6386f2b 100644 --- a/src/math/polynomial/polynomial.h +++ b/src/math/polynomial/polynomial.h @@ -19,17 +19,16 @@ Notes: #ifndef POLYNOMIAL_H_ #define POLYNOMIAL_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" -#include "util/lbool.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.h b/src/nlsat/nlsat_solver.h index 4ba1225bd..85a9adea7 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/nlsat_types.h" -#include "util/params.h" -#include "util/statistics.h" -#include "util/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 647a5e3ee..1583da5be 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 "math/polynomial/polynomial.h" -#include "util/buffer.h" -#include "sat/sat_types.h" -#include "util/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 002e49006..bd321ee6d 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -19,13 +19,12 @@ Revision History: #ifndef SAT_TYPES_H_ #define SAT_TYPES_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 "util/uint_set.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 ad9bcbd54..9612deb0d 100644 --- a/src/shell/lp_frontend.cpp +++ b/src/shell/lp_frontend.cpp @@ -81,7 +81,6 @@ void run_solver(lp_params & params, char const * mps_file_name) { solver->settings().report_frequency = params.rep_freq(); solver->settings().print_statistics = params.print_stats(); solver->settings().simplex_strategy() = lp:: 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/theory_lra.cpp b/src/smt/theory_lra.cpp index de9b41f64..3d7ff8b4f 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -36,7 +36,10 @@ Revision History: #include "smt/smt_model_generator.h" #include "smt/arith_eq_adapter.h" #include "util/nat_set.h" -#include "tactic/generic_model_converter.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 lra_lp { enum bound_kind { lower_t, upper_t }; @@ -88,16 +91,12 @@ namespace lra_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)); @@ -119,9 +118,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; @@ -145,10 +141,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; @@ -197,16 +193,8 @@ namespace smt { coeffs().pop_back(); } }; - - 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) {} - }; + + typedef vector> var_coeffs; 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 @@ -225,11 +213,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; + svector m_asserted_atoms; expr* m_not_handled; ptr_vector m_underspecified; unsigned_vector m_var_trail; @@ -249,16 +233,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; @@ -290,14 +294,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) { @@ -367,6 +382,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; @@ -421,6 +444,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); @@ -465,6 +526,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); @@ -493,7 +562,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); @@ -555,16 +624,8 @@ 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, lp::EQ, -d.m_coeff), d.m_var); - } - - void internalize_eq(theory_var v1, theory_var v2) { + + void internalize_eq(theory_var v1, theory_var v2) { enode* n1 = get_enode(v1); enode* n2 = get_enode(v2); scoped_internalize_state st(*this); @@ -656,15 +717,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(nullptr), - m_asserted_qhead(0), + 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(nullptr), - m_resource_limit(*this) { + m_solver(0), + m_resource_limit(*this), + m_use_nra_model(false) { } ~imp() { @@ -677,12 +737,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) { @@ -717,53 +773,10 @@ namespace smt { 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 = nullptr, *n2 = nullptr; - rational r; - lra_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 = lra_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 = lra_lp::lower_t; - } - else { - TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";); - found_not_handled(atom); - return true; - } - lra_lp::bound* b = alloc(lra_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); } @@ -789,13 +802,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 { @@ -814,13 +822,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) { @@ -841,18 +847,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_scopes.resize(old_size); + 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";); } @@ -1086,7 +1090,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);); @@ -1135,55 +1141,70 @@ namespace smt { enode* n1 = get_enode(v1); enode* n2 = get_enode(v2); m_assume_eq_head++; - CTRACE("arith", - get_ivalue(v1) == get_ivalue(v2) && n1->get_root() != n2->get_root(), + CTRACE("arith", + 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() != lp::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 != nullptr) { - 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; @@ -1196,6 +1217,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 @@ -1265,14 +1350,12 @@ namespace smt { #else propagate_bound(bv, is_true, b); #endif - if (!m_delay_constraints) { - lra_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; } @@ -2141,18 +2224,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);); - lp::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 lp::lp_status::INFEASIBLE: return l_false; @@ -2205,11 +2278,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; @@ -2258,9 +2335,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) { @@ -2286,6 +2397,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(); @@ -2298,6 +2410,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); @@ -2309,6 +2422,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()))); @@ -2509,7 +2623,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); @@ -2517,10 +2631,10 @@ 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); + } }; theory_lra::theory_lra(ast_manager& m, theory_arith_params& ap): diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 7367a52ff..c2da596fa 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -1,4 +1,5 @@ add_subdirectory(fuzzing) +add_subdirectory(lp) ################################################################################ # z3-test executable ################################################################################ @@ -120,6 +121,7 @@ add_executable(test-z3 upolynomial.cpp var_subst.cpp vector.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 0f4186252..96188c14d 100644 --- a/src/test/lp.cpp +++ b/src/test/lp/lp.cpp @@ -2712,8 +2712,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)); @@ -2726,9 +2726,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) { @@ -2740,8 +2747,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; @@ -2775,9 +2782,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)); @@ -2840,8 +2847,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)); @@ -2854,8 +2861,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)); @@ -2870,8 +2877,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)); @@ -2885,9 +2892,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)); @@ -2909,9 +2916,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)); @@ -2935,9 +2942,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 437cb7a6b..faf57ebd7 100644 --- a/src/test/smt_reader.h +++ b/src/test/lp/smt_reader.h @@ -389,7 +389,7 @@ namespace lp { 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 70c5f9e3b..efe683b42 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,6 +20,7 @@ z3_add_component(lp lp_solver_instances.cpp lu_instances.cpp matrix_instances.cpp + nra_solver.cpp permutation_matrix_instances.cpp quick_xplain.cpp row_eta_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/indexed_vector.h b/src/util/lp/indexed_vector.h index 3b1258ed7..4de827e10 100644 --- a/src/util/lp/indexed_vector.h +++ b/src/util/lp/indexed_vector.h @@ -98,8 +98,8 @@ public: 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 5d78c3ba7..000000000 --- a/src/util/lp/init_lar_solver.h +++ /dev/null @@ -1,591 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - - -Abstract: - - - -Author: - - Lev Nachmanson (levnach) - -Revision History: - - ---*/ - -// here we are inside lp::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; - SASSERT (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; - } - SASSERT(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); - SASSERT(sizes_are_correct()); - return i; -} - -void register_new_ext_var_index(unsigned ext_v) { - SASSERT(!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; - SASSERT(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(); - SASSERT(m_mpq_lar_core_solver.m_d_x.size() == j); - // SASSERT(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); - SASSERT(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(); - SASSERT(m_mpq_lar_core_solver.m_r_x.size() == j); - // SASSERT(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); - SASSERT(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); - } - SASSERT(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) { - SASSERT(sizes_are_correct()); - add_row_from_term_no_constraint(term, term_ext_index); - SASSERT(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(); - SASSERT(!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); - } - SASSERT(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: - SASSERT(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) { - SASSERT(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)); - SASSERT(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size()); -} - -void decide_on_strategy_and_adjust_initial_state() { - SASSERT(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: - SASSERT(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(); - SASSERT(m_mpq_lar_core_solver.m_d_x.size() == j); - // SASSERT(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); - SASSERT(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) { - SASSERT(A.row_count() > 0); - SASSERT(A.column_count() > 0); - unsigned last_row = A.row_count() - 1; - SASSERT(A.m_rows[last_row].empty()); - - for (auto & t : ls->m_coeffs) { - SASSERT(!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; - SASSERT(m_mpq_lar_core_solver.m_column_types()[j] == column_type::upper_bound); - SASSERT(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; - SASSERT(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: - SASSERT(false); - - } - 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) { - SASSERT(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: - SASSERT(false); - - } -} - -void update_boxed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { - SASSERT(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; - SASSERT(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: - SASSERT(false); - - } -} -void update_low_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { - SASSERT(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: - SASSERT(false); - - } -} - -void update_fixed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) { - SASSERT(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])); - SASSERT(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: - SASSERT(false); - - } -} - 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 32229cf27..500dc0c90 100644 --- a/src/util/lp/lar_core_solver.h +++ b/src/util/lp/lar_core_solver.h @@ -811,6 +811,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 c26333edb..ed8d03fc1 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -45,19 +45,31 @@ Revision History: #include "util/lp/iterator_on_row.h" #include "util/lp/quick_xplain.h" #include "util/lp/conversion_helper.h" + namespace lp { + 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; @@ -69,12 +81,8 @@ class lar_solver : public column_namer { 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;} @@ -84,15 +92,17 @@ public: 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() {SASSERT(false); // not implemented } + void register_new_ext_var_index(unsigned ext_v, bool is_int); lar_solver() : m_status(OPTIMAL), m_infeasible_column_index(-1), @@ -104,28 +114,20 @@ public: m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows = v? (& m_rows_with_changed_bounds) : nullptr; } - 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; - } + bool var_is_int(var_index v) const; #include "util/lp/init_lar_solver.h" numeric_pair const& get_value(var_index vi) const { return m_mpq_lar_core_solver.m_r_x[vi]; } - bool is_term(var_index j) const { - return j >= m_terms_start_index && j - m_terms_start_index < m_terms.size(); - } + void add_new_var_to_core_fields_for_doubles(bool register_in_basis); unsigned adjust_term_index(unsigned j) const { SASSERT(is_term(j)); return j - m_terms_start_index; } + void decide_on_strategy_and_adjust_initial_state(); bool use_lu() const { return m_settings.simplex_strategy() == simplex_strategy_enum::lu; } @@ -244,8 +246,6 @@ public: 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 @@ -428,11 +428,9 @@ public: lp_status get_status() const { return m_status;} - void set_status(lp_status s) {m_status = s;} + lp_status get_status() const; - lp_status find_feasible_solution() { - if (strategy_is_undecided()) - decide_on_strategy_and_adjust_initial_state(); + void set_status(lp_status s); m_mpq_lar_core_solver.m_r_solver.m_look_for_feasible_solution_only = true; return solve(); @@ -454,50 +452,19 @@ public: 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(); } + // 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 shrink_inf_set_after_pop(unsigned n, int_set & set) { - clean_large_elements_after_pop(n, set); - set.resize(n); - } + static void clean_large_elements_after_pop(unsigned n, int_set& set); + 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()); @@ -669,27 +636,14 @@ public: return *m_terms[j - m_terms_start_index]; } - 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, @@ -727,7 +681,7 @@ public: m_rows_with_changed_bounds.insert(rc.m_i); } - 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; @@ -765,9 +719,7 @@ public: return true; } - 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; @@ -795,23 +747,7 @@ public: } } - 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) { @@ -941,19 +877,9 @@ public: } - 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) { SASSERT(A.row_count() > 0); @@ -1080,32 +1006,24 @@ public: return false; // it is unreachable } + bool try_to_set_fixed(column_info & ci); + + column_type get_column_type(const column_info & ci); + + std::string get_column_name(unsigned j) const; + + bool all_constrained_variables_are_registered(const vector>& left_side); + + 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; + + 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 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; - } + bool the_left_sides_sum_to_zero(const vector> & evidence) const; 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()) { @@ -1258,11 +1176,8 @@ public: void get_infeasibility_explanation_for_inf_sign( vector> & explanation, const vector> & inf_row, - int inf_sign) const { + 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]; @@ -1273,6 +1188,7 @@ public: } } + void get_model(std::unordered_map & variable_values) const; void get_model(std::unordered_map & variable_values) const { @@ -1306,28 +1222,9 @@ public: } // ********** 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 { - for (auto c : m_constraints) { - print_constraint(c, out); - } - } - - void print_terms(std::ostream& out) const { - for (auto it : m_terms) { - print_term(*it, out); - out << "\n"; - } - } + void print_constraints(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); @@ -1337,12 +1234,7 @@ public: } - 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); - } + void print_left_side_of_constraint(const lar_base_constraint * c, std::ostream & out) 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(); @@ -1355,10 +1247,7 @@ public: return ret; } - 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; - } + mpq get_left_side_val(const lar_base_constraint & cns, const std::unordered_map & var_map) const; void fill_var_set_for_random_update(unsigned sz, var_index const * vars, vector& column_list) { for (unsigned i = 0; i < sz; i++) { @@ -1373,22 +1262,21 @@ public: } } - 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 fill_var_set_for_random_update(unsigned sz, var_index const * vars, vector& column_list); + 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 try_pivot_fixed_vars_from_basis() { - m_mpq_lar_core_solver.m_r_solver.pivot_fixed_vars_from_basis(); - } - - void pop() { - pop(1); - } - + 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; bool column_represents_row_in_tableau(unsigned j) { return m_vars_to_ul_pairs()[j].m_i != static_cast(-1); 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 fd115669c..d9cae100b 100644 --- a/src/util/lp/lp_core_solver_base.h +++ b/src/util/lp/lp_core_solver_base.h @@ -444,6 +444,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() { @@ -583,8 +584,8 @@ public: default: SASSERT(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 b49dd0638..8cd14152a 100644 --- a/src/util/lp/lp_core_solver_base.hpp +++ b/src/util/lp/lp_core_solver_base.hpp @@ -938,7 +938,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 @@ -958,23 +978,11 @@ 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; } } SASSERT(m_factorization->get_status()== LU_status::OK); - } } template bool diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index cd9e78321..894b912a7 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -31,13 +31,16 @@ namespace lp { 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, @@ -91,11 +94,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)); } }; @@ -214,7 +220,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; } @@ -321,6 +328,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/mps_reader.h b/src/util/lp/mps_reader.h index 916e56322..f0b050c0f 100644 --- a/src/util/lp/mps_reader.h +++ b/src/util/lp/mps_reader.h @@ -825,7 +825,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); @@ -843,20 +843,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); @@ -865,7 +865,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 a8a743a71..a53b8b8b2 100644 --- a/src/util/lp/numeric_pair.h +++ b/src/util/lp/numeric_pair.h @@ -203,6 +203,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(); + } + }; @@ -328,4 +333,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 f9506c056..89c14c80f 100644 --- a/src/util/lp/quick_xplain.cpp +++ b/src/util/lp/quick_xplain.cpp @@ -35,7 +35,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)); @@ -109,7 +109,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 e8234d1e4..8da3cb144 100644 --- a/src/util/lp/stacked_vector.h +++ b/src/util/lp/stacked_vector.h @@ -48,7 +48,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 c57f31177..8fa66691c 100644 --- a/src/util/lp/static_matrix_instances.cpp +++ b/src/util/lp/static_matrix_instances.cpp @@ -17,7 +17,13 @@ Revision History: --*/ +======= +/* + Copyright (c) 2017 Microsoft Corporation + Author: Lev Nachmanson +*/ #include +#include "util/vector.h" #include #include #include "util/vector.h"