From 2fd32ce62d56a08b78c78438ee7b9589c4032830 Mon Sep 17 00:00:00 2001 From: Lev Date: Sat, 6 Oct 2018 15:51:06 -0700 Subject: [PATCH] rename Signed-off-by: Lev --- src/util/lp/int_solver.cpp | 2 - src/util/lp/mon_eq.cpp | 5 ++- src/util/lp/mon_eq.h | 60 --------------------------- src/util/lp/monomial.h | 83 +++++++++++++++++++++++++------------- src/util/lp/nla_solver.cpp | 77 +++++++++++++++++------------------ src/util/lp/nra_solver.cpp | 5 ++- 6 files changed, 99 insertions(+), 133 deletions(-) delete mode 100644 src/util/lp/mon_eq.h diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index e2670fad7..ef66f005b 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -169,8 +169,6 @@ unsigned int_solver::row_of_basic_column(unsigned j) const { // } -typedef monomial mono; - // this will allow to enable and disable tracking of the pivot rows struct check_return_helper { diff --git a/src/util/lp/mon_eq.cpp b/src/util/lp/mon_eq.cpp index d1a5ffeb3..dc11a5be9 100644 --- a/src/util/lp/mon_eq.cpp +++ b/src/util/lp/mon_eq.cpp @@ -3,8 +3,9 @@ Author: Nikolaj Bjorner */ #include "util/lp/lar_solver.h" -#include "util/lp/mon_eq.h" -namespace nra { +#include "util/lp/monomial.h" +namespace nla { +typedef monomial mon_eq; bool check_assignment(mon_eq const& m, variable_map_type & vars) { rational r1 = vars[m.var()]; if (r1.is_zero()) { diff --git a/src/util/lp/mon_eq.h b/src/util/lp/mon_eq.h deleted file mode 100644 index 4627cf102..000000000 --- a/src/util/lp/mon_eq.h +++ /dev/null @@ -1,60 +0,0 @@ -/* - Copyright (c) 2017 Microsoft Corporation - Author: Nikolaj Bjorner -*/ -#include "util/lp/lp_settings.h" -#include "util/vector.h" -#include "util/lp/lar_solver.h" - -namespace nra { - /* - * represents definition m_v = v1*v2*...*vn, - * where m_vs = [v1, v2, .., vn] - */ - class mon_eq { - // fields - lp::var_index m_v; - svector m_vs; - public: - // constructors - mon_eq(lp::var_index v, unsigned sz, lp::var_index const* vs): - m_v(v), m_vs(sz, vs) {} - mon_eq(lp::var_index v, const svector &vs): - m_v(v), m_vs(vs) {} - mon_eq() {} - unsigned var() const { return m_v; } - unsigned size() const { return m_vs.size(); } - unsigned operator[](unsigned idx) const { return m_vs[idx]; } - svector::const_iterator begin() const { return m_vs.begin(); } - svector::const_iterator end() const { return m_vs.end(); } - const svector vars() const { return m_vs; } - }; - - typedef std::unordered_map variable_map_type; - - bool check_assignment(mon_eq const& m, variable_map_type & vars); - - bool check_assignments(const vector & monomimials, - const lp::lar_solver& s, - variable_map_type & vars); - - - - /* - * represents definition m_v = coeff* v1*v2*...*vn, - * where m_vs = [v1, v2, .., vn] - */ - class mon_eq_coeff : public mon_eq { - rational m_coeff; - public: - mon_eq_coeff(mon_eq const& eq, rational const& coeff): - mon_eq(eq), m_coeff(coeff) {} - - mon_eq_coeff(lp::var_index v, const svector &vs, rational const& coeff): - mon_eq(v, vs), - m_coeff(coeff) {} - - rational const& coeff() const { return m_coeff; } - }; - -} diff --git a/src/util/lp/monomial.h b/src/util/lp/monomial.h index 5aa1eeb0c..c1fad7ba0 100644 --- a/src/util/lp/monomial.h +++ b/src/util/lp/monomial.h @@ -1,33 +1,60 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation +/* + Copyright (c) 2017 Microsoft Corporation + Author: Nikolaj Bjorner +*/ +#include "util/lp/lp_settings.h" +#include "util/vector.h" +#include "util/lp/lar_solver.h" -Module Name: +namespace nla { + /* + * represents definition m_v = v1*v2*...*vn, + * where m_vs = [v1, v2, .., vn] + */ + class monomial { + // fields + lp::var_index m_v; + svector m_vs; + public: + // constructors + monomial(lp::var_index v, unsigned sz, lp::var_index const* vs): + m_v(v), m_vs(sz, vs) {} + monomial(lp::var_index v, const svector &vs): + m_v(v), m_vs(vs) {} + monomial() {} + unsigned var() const { return m_v; } + unsigned size() const { return m_vs.size(); } + unsigned operator[](unsigned idx) const { return m_vs[idx]; } + svector::const_iterator begin() const { return m_vs.begin(); } + svector::const_iterator end() const { return m_vs.end(); } + const svector vars() const { return m_vs; } + }; - - -Abstract: - - - -Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - -Revision History: + typedef std::unordered_map variable_map_type; + + bool check_assignment(monomial const& m, variable_map_type & vars); + + bool check_assignments(const vector & monomimials, + const lp::lar_solver& s, + variable_map_type & vars); ---*/ -#pragma once -namespace lp { -struct monomial { - mpq m_coeff; // the coefficient of the monomial - var_index m_var; // the variable index -public: - monomial(const mpq& coeff, var_index var) : m_coeff(coeff), m_var(var) {} - monomial(var_index var) : monomial(one_of_type(), var) {} - const mpq & coeff() const { return m_coeff; } - mpq & coeff() { return m_coeff; } - var_index var() const { return m_var; } - std::pair to_pair() const { return std::make_pair(coeff(), var());} -}; + + /* + * represents definition m_v = coeff* v1*v2*...*vn, + * where m_vs = [v1, v2, .., vn] + */ + class monomial_coeff : public monomial { + rational m_coeff; + public: + monomial_coeff(monomial const& eq, rational const& coeff): + monomial(eq), m_coeff(coeff) {} + + monomial_coeff(lp::var_index v, const svector &vs, rational const& coeff): + monomial(v, vs), + m_coeff(coeff) {} + + rational const& coeff() const { return m_coeff; } + }; + } diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 496b37414..d69123cce 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -19,12 +19,11 @@ --*/ #include "util/lp/nla_solver.h" #include "util/map.h" -#include "util/lp/mon_eq.h" +#include "util/lp/monomial.h" #include "util/lp/lp_utils.h" namespace nla { typedef lp::constraint_index lpci; typedef std::unordered_set expl_set; -typedef nra::mon_eq mon_eq; typedef lp::var_index lpvar; struct hash_svector { @@ -170,7 +169,7 @@ struct solver::imp { }; vars_equivalence m_vars_equivalence; - vector m_monomials; + vector m_monomials; // maps the vector of the rooted monomial vars to the list of the indices of monomials having the same rooted monomial std::unordered_map, vector, hash_svector> m_rooted_monomials; @@ -178,7 +177,7 @@ struct solver::imp { lp::lar_solver& m_lar_solver; std::unordered_map m_var_to_mon_indices; - // mon_eq.var() -> monomial index + // monomial.var() -> monomial index u_map m_var_to_its_monomial; lp::explanation * m_expl; lemma * m_lemma; @@ -194,7 +193,7 @@ struct solver::imp { lp::impq vv(unsigned j) const { return m_lar_solver.get_column_value(j); } void add(lpvar v, unsigned sz, lpvar const* vs) { - m_monomials.push_back(mon_eq(v, sz, vs)); + m_monomials.push_back(monomial(v, sz, vs)); m_var_to_its_monomial.insert(v, m_monomials.size() - 1); } @@ -209,7 +208,7 @@ struct solver::imp { } // make sure that the monomial value is the product of the values of the factors - bool check_monomial(const mon_eq& m) { + bool check_monomial(const monomial& m) { SASSERT(m_lar_solver.get_column_value(m.var()).is_int()); const rational & model_val = m_lar_solver.get_column_value_rational(m.var()); rational r(1); @@ -228,7 +227,7 @@ struct solver::imp { return sign * m_lar_solver.get_column_value(j) != m_lar_solver.get_column_value(k); } - void add_explanation_of_reducing_to_rooted_monomial(const mon_eq& m, expl_set & exp) const { + void add_explanation_of_reducing_to_rooted_monomial(const monomial& m, expl_set & exp) const { m_vars_equivalence.add_explanation_of_reducing_to_rooted_monomial(m, exp); } @@ -239,7 +238,7 @@ struct solver::imp { add_explanation_of_reducing_to_rooted_monomial(m_monomials[index], exp); } - std::ostream& print_monomial(const mon_eq& m, std::ostream& out) const { + std::ostream& print_monomial(const monomial& m, std::ostream& out) const { out << m_lar_solver.get_variable_name(m.var()) << " = "; for (unsigned k = 0; k < m.size(); k++) { out << m_lar_solver.get_variable_name(m.vars()[k]); @@ -257,7 +256,7 @@ struct solver::imp { // the monomials should be equal by modulo sign, but they are not equal in the model by modulo sign - void fill_explanation_and_lemma_sign(const mon_eq& a, const mon_eq & b, rational const& sign) { + void fill_explanation_and_lemma_sign(const monomial& a, const monomial & b, rational const& sign) { expl_set expl; SASSERT(sign == 1 || sign == -1); add_explanation_of_reducing_to_rooted_monomial(a, expl); @@ -299,7 +298,7 @@ struct solver::imp { // m_v = coeff * w1 * ... * wn, where w1, .., wn are canonical // representative under current equations. // - nra::mon_eq_coeff canonize_mon_eq(mon_eq const& m) const { + monomial_coeff canonize_monomial(monomial const& m) const { svector vars; rational sign = rational(1); for (lpvar v : m.vars()) { @@ -308,7 +307,7 @@ struct solver::imp { vars.push_back(root); } std::sort(vars.begin(), vars.end()); - return nra::mon_eq_coeff(m.var(), vars, sign); + return monomial_coeff(m.var(), vars, sign); } bool list_contains_one_to_refine(const std::unordered_set & to_refine_set, @@ -424,7 +423,7 @@ struct solver::imp { int get_mon_sign_zero(unsigned i_mon, bool & strict) { int sign = 1; strict = true; - const mon_eq m = m_monomials[i_mon]; + const monomial m = m_monomials[i_mon]; for (lpvar j : m) { int s = get_mon_sign_zero_var(j, strict); if (s == 2) @@ -487,7 +486,7 @@ struct solver::imp { return true; } - void create_lemma_one_of_the_factors_is_zero(const mon_eq& m) { + void create_lemma_one_of_the_factors_is_zero(const monomial& m) { lpci lci, uci; rational b; bool is_strict; @@ -526,16 +525,16 @@ struct solver::imp { } std::ostream & print_var(lpvar j, std::ostream & out) const { - bool monomial = false; - for (const mon_eq & m : m_monomials) { + bool is_monomial = false; + for (const monomial & m : m_monomials) { if (j == m.var()) { - monomial = true; + is_monomial = true; print_monomial(m, out); out << " = " << m_lar_solver.get_column_value(j);; break; } } - if (!monomial) + if (!is_monomial) out << m_lar_solver.get_variable_name(j) << " = " << m_lar_solver.get_column_value(j); out <<";"; return out; @@ -609,7 +608,7 @@ struct solver::imp { } - void get_large_and_small_indices_of_monomimal(const mon_eq& m, + void get_large_and_small_indices_of_monomimal(const monomial& m, unsigned_vector & large, unsigned_vector & _small) { @@ -642,7 +641,7 @@ struct solver::imp { * v is the value of monomial, * vars is the array of reduced to minimum variables of the monomial */ - bool basic_neutral_for_reduced_monomial(const mon_eq & m, const rational & v, const svector & vars) { + bool basic_neutral_for_reduced_monomial(const monomial & m, const rational & v, const svector & vars) { vector ones_of_mon = get_ones_of_monomimal(vars); // if abs(m.vars()[j]) is 1, then ones_of_mon[j] = sign, where sign is 1 in case of m.vars()[j] = 1, or -1 otherwise. @@ -656,7 +655,7 @@ struct solver::imp { * \brief */ bool basic_lemma_for_mon_neutral(unsigned i_mon) { - const mon_eq & m = m_monomials[i_mon]; + const monomial & m = m_monomials[i_mon]; rational sign; svector reduced_vars = reduce_monomial_to_canonical(m.vars(), sign); rational v = m_lar_solver.get_column_value_rational(m.var()); @@ -666,7 +665,7 @@ struct solver::imp { } // returns the variable m_i, of a monomial if found and sets the sign, - bool find_monomial_of_vars(const svector& vars, mon_eq& m, rational & sign) const { + bool find_monomial_of_vars(const svector& vars, monomial& m, rational & sign) const { auto it = m_rooted_monomials.find(vars); if (it == m_rooted_monomials.end()) { return false; @@ -679,7 +678,7 @@ struct solver::imp { } bool find_complimenting_monomial(const svector & vars, lpvar & j) { - mon_eq m; + monomial m; rational other_sign; if (!find_monomial_of_vars(vars, m, other_sign)) { return false; @@ -689,13 +688,13 @@ struct solver::imp { } bool find_lpvar_and_sign_with_wrong_val( - const mon_eq& m, + const monomial& m, svector & vars, const rational& v, rational sign, lpvar& j) { rational other_sign; - mon_eq mn; + monomial mn; if (!find_monomial_of_vars(vars, mn, other_sign)) { return false; } @@ -715,7 +714,7 @@ struct solver::imp { // sign ? // j ? // - void equality_for_neutral_case(const mon_eq & m, + void equality_for_neutral_case(const monomial & m, const svector & mask, const vector& ones_of_monomial, lpvar j, rational const& sign) { expl_set expl; @@ -735,7 +734,7 @@ struct solver::imp { } // vars here are root vars for m.vs - bool process_ones_of_mon(const mon_eq& m, + bool process_ones_of_mon(const monomial& m, const vector& ones_of_monomial, const svector &min_vars, const rational& v) { svector mask(ones_of_monomial.size(), false); @@ -793,7 +792,7 @@ struct solver::imp { expl.insert(ci); } - void large_lemma_for_proportion_case_on_known_signs(const mon_eq& m, + void large_lemma_for_proportion_case_on_known_signs(const monomial& m, unsigned j, int mon_sign, int j_sign) { @@ -818,7 +817,7 @@ struct solver::imp { m_lemma->push_back(ineq(lp::lconstraint_kind::GE, t, rational::zero())); } - bool large_lemma_for_proportion_case(const mon_eq& m, const svector & mask, + bool large_lemma_for_proportion_case(const monomial& m, const svector & mask, const unsigned_vector & large, unsigned j) { TRACE("nla_solver", ); const rational j_val = m_lar_solver.get_column_value_rational(j); @@ -842,7 +841,7 @@ struct solver::imp { return true; } - bool small_lemma_for_proportion_case(const mon_eq& m, const svector & mask, + bool small_lemma_for_proportion_case(const monomial& m, const svector & mask, const unsigned_vector & _small, unsigned j) { TRACE("nla_solver", ); const rational j_val = m_lar_solver.get_column_value_rational(j); @@ -868,7 +867,7 @@ struct solver::imp { } // It is the case where |x[j]| >= |x[m.var()]| should hold in the model, but it does not. - void small_lemma_for_proportion_case_on_known_signs(const mon_eq& m, unsigned j, int mon_sign, int j_sign) { + void small_lemma_for_proportion_case_on_known_signs(const monomial& m, unsigned j, int mon_sign, int j_sign) { // Imagine that the signs are all positive. // For this case we would have x[j] < 0 || x[m.var()] < 0 || x[j] >= x[m.var()] // But for the general case we have @@ -954,7 +953,7 @@ struct solver::imp { // we derive a lemma from |x| >= 1 => |xy| >= |y| or |x| <= 1 => |xy| <= |y| bool basic_lemma_for_mon_proportionality_from_factors_to_product(unsigned i_mon) { - const mon_eq & m = m_monomials[i_mon]; + const monomial & m = m_monomials[i_mon]; unsigned_vector large; unsigned_vector _small; get_large_and_small_indices_of_monomimal(m, large, _small); @@ -1009,14 +1008,14 @@ struct solver::imp { struct binary_factorizations_of_monomial { unsigned m_i_mon; const imp& m_imp; - const mon_eq& m_mon; - nra::mon_eq_coeff m_cmon; + const monomial& m_mon; + monomial_coeff m_cmon; binary_factorizations_of_monomial(unsigned i_mon, const imp& s) : m_i_mon(i_mon), m_imp(s), m_mon(m_imp.m_monomials[i_mon]), - m_cmon(m_imp.canonize_mon_eq(m_mon)) { + m_cmon(m_imp.canonize_monomial(m_mon)) { } @@ -1056,7 +1055,7 @@ struct solver::imp { std::sort(j_vars.begin(), j_vars.end()); rational k_sign, j_sign; - mon_eq m; + monomial m; if (k_vars.size() == 1) { k = k_vars[0]; k_sign = 1; @@ -1391,7 +1390,7 @@ struct solver::imp { } void map_monomial_vars_to_monomial_indices(unsigned i) { - const mon_eq& m = m_monomials[i]; + const monomial& m = m_monomials[i]; for (lpvar j : m.vars()) { auto it = m_var_to_mon_indices.find(j); if (it == m_var_to_mon_indices.end()) { @@ -1459,7 +1458,7 @@ struct solver::imp { m_vars_equivalence.create_tree(); } - void register_key_mono_in_min_monomials(nra::mon_eq_coeff const& mc, unsigned i) { + void register_key_mono_in_min_monomials(monomial_coeff const& mc, unsigned i) { mono_index_with_sign ms(i, mc.coeff()); auto it = m_rooted_monomials.find(mc.vars()); @@ -1475,8 +1474,8 @@ struct solver::imp { } void register_monomial_in_min_map(unsigned i) { - const mon_eq& m = m_monomials[i]; - nra::mon_eq_coeff mc = canonize_mon_eq(m_monomials[i]); + const monomial& m = m_monomials[i]; + monomial_coeff mc = canonize_monomial(m_monomials[i]); register_key_mono_in_min_monomials(mc, i); } diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp index 90e28d76c..ee0752a54 100644 --- a/src/util/lp/nra_solver.cpp +++ b/src/util/lp/nra_solver.cpp @@ -9,11 +9,12 @@ #include "math/polynomial/polynomial.h" #include "math/polynomial/algebraic_numbers.h" #include "util/map.h" -#include "util/lp/mon_eq.h" +#include "util/lp/monomial.h" namespace nra { - +typedef nla::monomial mon_eq; +typedef nla::variable_map_type variable_map_type; struct solver::imp { lp::lar_solver& s; reslimit& m_limit;