From 38eca3b66a2cc169baf67898b441528090ee9573 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 23 Mar 2020 11:18:56 -0700 Subject: [PATCH] fixes in order lemmas and printing terms Signed-off-by: Lev Nachmanson --- src/math/lp/gomory.cpp | 2 +- src/math/lp/lar_solver.cpp | 4 +- src/math/lp/lp_utils.h | 9 ++- src/math/lp/nla_core.cpp | 9 +++ src/math/lp/nla_core.h | 2 + src/math/lp/nla_monotone_lemmas.cpp | 44 --------------- src/math/lp/nla_monotone_lemmas.h | 3 - src/math/lp/nla_order_lemmas.cpp | 86 ++++++++++++++++++----------- src/math/lp/nla_order_lemmas.h | 13 +++-- 9 files changed, 83 insertions(+), 89 deletions(-) diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp index fa506b277..0d7db428d 100644 --- a/src/math/lp/gomory.cpp +++ b/src/math/lp/gomory.cpp @@ -289,7 +289,7 @@ public: lia_move cut() { TRACE("gomory_cut", dump(tout);); - // gomory will be t <= k and the current solution has a property t > k + // gomory will be t >= k and the current solution has a property t < k m_k = 1; m_t.clear(); mpq m_lcm_den(1); diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 886c31f9f..1e8a31342 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -60,7 +60,7 @@ std::ostream& lar_solver::print_implied_bound(const implied_bound& be, std::ostr out << "implied bound\n"; unsigned v = be.m_j; if (tv::is_term(v)) { - out << "it is a term number " << be.m_j << std::endl; + out << "it is a term number " << tv::unmask_term(be.m_j) << std::endl; print_term(*m_terms[tv::unmask_term(v)], out); } else { @@ -1259,7 +1259,7 @@ void lar_solver::set_variable_name(var_index vi, std::string name) { std::string lar_solver::get_variable_name(var_index j) const { if (tv::is_term(j)) - return std::string("_t") + T_to_string(j); + return std::string("_t") + T_to_string(tv::unmask_term(j)); if (j >= m_var_register.size()) return std::string("_s") + T_to_string(j); diff --git a/src/math/lp/lp_utils.h b/src/math/lp/lp_utils.h index 9a8dc3fd3..387bc6cc5 100644 --- a/src/math/lp/lp_utils.h +++ b/src/math/lp/lp_utils.h @@ -20,6 +20,7 @@ Revision History: #pragma once #include #include "math/lp/numeric_pair.h" +#include "math/lp/lp_types.h" #include "util/debug.h" #include #include @@ -115,7 +116,13 @@ template std::ostream& print_linear_combination_of_column_indices_only(const vector> & coeffs, std::ostream & out) { return print_linear_combination_customized( coeffs, - [](unsigned j) {std::stringstream ss; ss << "v" << j; return ss.str();}, + [](unsigned j) {std::stringstream ss; + if (tv::is_term(j)) { + ss << "t" << tv::unmask_term(j); + } else { + ss << "v" << j; + } + return ss.str();}, out); } template diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index ca569b977..4f25f5648 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1027,6 +1027,15 @@ bool core::divide(const monic& bc, const factor& c, factor & b) const { return true; } +void core::negate_var_relation_strictly(lpvar a, lpvar b) { + SASSERT(val(a) != val(b)); + if (val(a) < val(b)) { + mk_ineq(a, -rational(1), b, llc::GT); + } else { + mk_ineq(a, -rational(1), b, llc::LT); + } +} + void core::negate_factor_equality(const factor& c, const factor& d) { if (c == d) diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index c1e3da387..bfc5481a4 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -363,6 +363,8 @@ public: void negate_factor_relation(const rational& a_sign, const factor& a, const rational& b_sign, const factor& b); + void negate_var_relation_strictly(lpvar a, lpvar b); + std::unordered_set collect_vars(const lemma& l) const; bool rm_check(const monic&) const; diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp index f72448335..d7e507b80 100644 --- a/src/math/lp/nla_monotone_lemmas.cpp +++ b/src/math/lp/nla_monotone_lemmas.cpp @@ -32,50 +32,6 @@ void monotone::monotonicity_lemma() { monotonicity_lemma(c().emons()[v]); } } - - -void monotone::negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict) { - rational av = val(a); - rational as = rational(nla::rat_sign(av)); - rational bv = val(b); - rational bs = rational(nla::rat_sign(bv)); - TRACE("nla_solver", tout << "av = " << av << ", bv = " << bv << "\n";); - SASSERT(as*av <= bs*bv); - llc mod_s = strict? (llc::LE): (llc::LT); - mk_ineq(as, a, mod_s); // |a| <= 0 || |a| < 0 - if (a != b) { - mk_ineq(bs, b, mod_s); // |b| <= 0 || |b| < 0 - mk_ineq(as, a, -bs, b, llc::GT); // negate |aj| <= |bj| - } -} - -void monotone::assert_abs_val_a_le_abs_var_b( - const monic& a, - const monic& b, - bool strict) { - lpvar aj = var(a); - lpvar bj = var(b); - rational av = val(aj); - rational as = rational(nla::rat_sign(av)); - rational bv = val(bj); - rational bs = rational(nla::rat_sign(bv)); - // TRACE("nla_solver", tout << "rmv = " << rmv << ", jv = " << jv << "\n";); - mk_ineq(as, aj, llc::LT); // |aj| < 0 - mk_ineq(bs, bj, llc::LT); // |bj| < 0 - mk_ineq(as, aj, -bs, bj, strict? llc::LT : llc::LE); // |aj| < |bj| -} - -void monotone::negate_abs_a_lt_abs_b(lpvar a, lpvar b) { - rational av = val(a); - rational as = rational(nla::rat_sign(av)); - rational bv = val(b); - rational bs = rational(nla::rat_sign(bv)); - TRACE("nla_solver", tout << "av = " << av << ", bv = " << bv << "\n";); - SASSERT(as*av < bs*bv); - mk_ineq(as, a, llc::LT); // |aj| < 0 - mk_ineq(bs, b, llc::LT); // |bj| < 0 - mk_ineq(as, a, -bs, b, llc::GE); // negate |aj| < |bj| -} void monotone::monotonicity_lemma(monic const& m) { SASSERT(!check_monic(m)); diff --git a/src/math/lp/nla_monotone_lemmas.h b/src/math/lp/nla_monotone_lemmas.h index 7330ed385..5b8a066dd 100644 --- a/src/math/lp/nla_monotone_lemmas.h +++ b/src/math/lp/nla_monotone_lemmas.h @@ -30,8 +30,5 @@ private: void monotonicity_lemma_lt(const monic& m, const rational& prod_val); std::vector get_sorted_key(const monic& rm) const; vector> get_sorted_key_with_rvars(const monic& a) const; - void negate_abs_a_le_abs_b(lpvar a, lpvar b, bool strict); - void negate_abs_a_lt_abs_b(lpvar a, lpvar b); - void assert_abs_val_a_le_abs_var_b(const monic& a, const monic& b, bool strict); }; } diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 9da589d7b..91aabae6e 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -255,20 +255,12 @@ bool order::order_lemma_on_ac_explore(const monic& rm, const factorization& ac, return false; } -// |c_sign| = 1, and c*c_sign > 0 -// ac > bc && ac/|c| > bc/|c| => a*c_sign > b*c_sign -void order::generate_ol(const monic& ac, - const factor& a, - int c_sign, - const factor& c, - const monic& bc, - const factor& b, - llc ab_cmp) { - - rational rc_sign = rational(c_sign); - rational sign_a = rc_sign * sign_to_rat(canonize_sign(a)); - rational sign_b = rc_sign * sign_to_rat(canonize_sign(b)); - rational sign_c = rc_sign * sign_to_rat(canonize_sign(c)); +void order::generate_ol_eq(const monic& ac, + const factor& a, + const factor& c, + const monic& bc, + const factor& b) { + add_empty_lemma(); #if 0 IF_VERBOSE(0, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac @@ -276,10 +268,11 @@ void order::generate_ol(const monic& ac, << " a " << sign_a << "*v" << var(a) << " " << val(a) << "\n" << " b " << sign_b << "*v" << var(b) << " " << val(b) << "\n" << " c " << sign_c << "*v" << var(c) << " " << val(c) << "\n"); -#endif - mk_ineq(sign_c, var(c), llc::LE); - mk_ineq(canonize_sign(ac), var(ac), !canonize_sign(bc), var(bc), ab_cmp); - mk_ineq(sign_a, var(a), - sign_b, var(b), negate(ab_cmp)); +#endif + // ac == bc + mk_ineq(c.var(),llc::EQ); // c is not equal to zero + mk_ineq(ac.var(), -rational(1), bc.var(), llc::NE); + mk_ineq(canonize_sign(a), a.var(), !canonize_sign(b), b.var(), llc::EQ); explain(ac); explain(a); explain(bc); @@ -288,27 +281,54 @@ void order::generate_ol(const monic& ac, TRACE("nla_solver", _().print_lemma(tout);); } +void order::generate_ol(const monic& ac, + const factor& a, + const factor& c, + const monic& bc, + const factor& b) { + + add_empty_lemma(); +#if 0 + IF_VERBOSE(0, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac + << " " << ab_cmp << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n" + << " a " << sign_a << "*v" << var(a) << " " << val(a) << "\n" + << " b " << sign_b << "*v" << var(b) << " " << val(b) << "\n" + << " c " << sign_c << "*v" << var(c) << " " << val(c) << "\n"); +#endif + // fix the sign of c + _().negate_relation(c.var(), rational(0)); + _().negate_var_relation_strictly(ac.var(), bc.var()); + _().negate_var_relation_strictly(a.var(), b.var()); + explain(ac); + explain(a); + explain(bc); + explain(b); + explain(c); + TRACE("nla_solver", _().print_lemma(tout);); +} + +// We have ac = a*c and bc = b*c. +// Suppose ac >= bc, then ac/|c| >= bc/|b| +// Notice that ac/|c| = a*rat_sign(val(c)|, and similar fo bc/|c|.// bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac, const factor& a, const factor& c, const monic& bc, const factor& b) { - auto cv = val(c); - int c_sign = nla::rat_sign(cv); - SASSERT(c_sign != 0); - auto av_c_s = val(a)*rational(c_sign); - auto bv_c_s = val(b)*rational(c_sign); - auto acv = var_val(ac); - auto bcv = var_val(bc); - TRACE("nla_solver", _().trace_print_ol(ac, a, c, bc, b, tout);); - // Suppose ac >= bc, then ac/|c| >= bc/|c|. - // Notice that ac/|c| = a*c_sign , and bc/|c| = b*c_sign, which are correspondingly av_c_s and bv_c_s - if (acv >= bcv && av_c_s < bv_c_s) { - generate_ol(ac, a, c_sign, c, bc, b, llc::LT); - return true; - } else if (acv <= bcv && av_c_s > bv_c_s) { - generate_ol(ac, a, c_sign, c, bc, b, llc::GT); + SASSERT(!val(c).is_zero()); + rational c_sign = rational(nla::rat_sign(val(c))); + auto av_c_s = val(a) * c_sign; + auto bv_c_s = val(b) * c_sign; + if ((var_val(ac) > var_val(bc) && av_c_s < bv_c_s) + || + (var_val(ac) < var_val(bc) && av_c_s > bv_c_s)) { + TRACE("nla_solver", _().trace_print_ol(ac, a, c, bc, b, tout);); + generate_ol(ac, a, c, bc, b); return true; + } else { + if((var_val(ac) == var_val(bc)) && (av_c_s != bv_c_s)) { + generate_ol_eq(ac, a, c, bc, b); + } } return false; } diff --git a/src/math/lp/nla_order_lemmas.h b/src/math/lp/nla_order_lemmas.h index 341bef43d..24b7b2cb4 100644 --- a/src/math/lp/nla_order_lemmas.h +++ b/src/math/lp/nla_order_lemmas.h @@ -68,15 +68,18 @@ private: void order_lemma_on_binomial_sign(const monic& ac, lpvar x, lpvar y, int sign); void order_lemma_on_binomial(const monic& ac); void order_lemma_on_monic(const monic& rm); - // |c_sign| = 1, and c*c_sign > 0 - // ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign + void generate_ol(const monic& ac, const factor& a, - int c_sign, const factor& c, const monic& bc, - const factor& b, - llc ab_cmp); + const factor& b); + + void generate_ol_eq(const monic& ac, + const factor& a, + const factor& c, + const monic& bc, + const factor& b); void generate_mon_ol(const monic& ac, lpvar a,