diff --git a/src/util/lp/mon_eq.h b/src/util/lp/mon_eq.h index cc44ff5ca..2af42bf39 100644 --- a/src/util/lp/mon_eq.h +++ b/src/util/lp/mon_eq.h @@ -12,6 +12,7 @@ namespace nra { lp::var_index m_v; svector m_vs; unsigned var() const { return m_v; } + unsigned size() const { return m_vs.size(); } }; typedef std::unordered_map variable_map_type; diff --git a/src/util/lp/niil_solver.cpp b/src/util/lp/niil_solver.cpp index e68a2abe8..d1ae01258 100644 --- a/src/util/lp/niil_solver.cpp +++ b/src/util/lp/niil_solver.cpp @@ -20,23 +20,75 @@ Revision History: #include "util/lp/niil_solver.h" #include "util/map.h" #include "util/lp/mon_eq.h" +#include "util/lp/lp_utils.h" namespace niil { typedef nra::mon_eq mon_eq; - +typedef lp::var_index lpvar; struct solver::imp { + struct vars_equivalence { + typedef std::pair lppair; + std::unordered_map + > m_map; + void add_equivalence_maybe(const lp::lar_term *t) { + if (t->size() != 2) + return; + bool seen_minus = false; + bool seen_plus = false; + lpvar i = -1, j; + for(const auto & p : *t) { + const auto & c = p.coeff(); + if (c == 1) { + seen_plus = true; + } else if (c == - 1) { + seen_minus = true; + } else { + return; + } + if (i == static_cast(-1)) + i = p.var(); + else + j = p.var(); + } + SASSERT(i != j && i != static_cast(-1)); + if (i < j) { // swap if i > j ordered + lpvar tmp = i; + i = j; + j = tmp; + } + if (seen_minus && seen_plus) + m_map[lppair(i, j)] = -1; // we have x_i == - x_j + else + m_map[lppair(i, j)] = 1; // we have an equality + + } + vars_equivalence(const lp::lar_solver& s) { + for (const lp::lar_term *t : s.terms()) + add_equivalence_maybe(t); + } + lpvar get_equivalent_var(lpvar j, bool & sign) { + SASSERT(false); + return false; + } + bool empty() const { + return m_map.empty(); + } + }; + vars_equivalence m_vars_equivalence; vector m_monomials; unsigned_vector m_monomials_lim; lp::lar_solver& m_lar_solver; - std::unordered_map> m_var_to_monomials; + std::unordered_map> m_var_to_monomials; imp(lp::lar_solver& s, reslimit& lim, params_ref const& p) - : m_lar_solver(s) + : m_vars_equivalence(s), m_lar_solver(s) // m_limit(lim), // m_params(p) { } - void add(lp::var_index v, unsigned sz, lp::var_index const* vs) { + void add(lpvar v, unsigned sz, lpvar const* vs) { m_monomials.push_back(mon_eq(v, sz, vs)); } @@ -59,39 +111,77 @@ struct solver::imp { return r == model_val; } - bool generate_basic_lemma_for_mon_sign(const mon_eq& m, lemma& l) { + bool generate_basic_lemma_for_mon_sign_var_other_mon( unsigned j_var, + const svector & mon_vars, + const mon_eq& om, bool sign, lemma& l) { + if (mon_vars.size() != om.size()) + return false; + SASSERT(false); + return false; + } + + bool generate_basic_lemma_for_mon_sign_var(unsigned i_mon, + unsigned j_var, const svector& mon_vars, lemma& l, bool sign) { + auto it = m_var_to_monomials.find(j_var); + for (auto other_i_mon : it->second) { + if (other_i_mon == i_mon) continue; + if (generate_basic_lemma_for_mon_sign_var_other_mon(j_var, mon_vars, + m_monomials[other_i_mon], sign, l)) + return true; + } return false; } - bool generate_basic_lemma_for_mon_zero(const mon_eq& m, lemma& l) { + // replaces each variable by a smaller one and flips the sing if the var comes with a minus + void reduce_monomial_to_minimal(svector & vars, int & sign) { + + } + + bool generate_basic_lemma_for_mon_sign(unsigned i_mon, lemma& l) { + if (m_vars_equivalence.empty()) { + std::cout << "empty m_vars_equivalence\n"; + return false; + } + const mon_eq& m_of_i = m_monomials[i_mon]; + int sign = 1; + + auto mon_vars = m_of_i.m_vs; + reduce_monomial_to_minimal(mon_vars, sign); + for (unsigned j_var : mon_vars) + if (generate_basic_lemma_for_mon_sign_var(i_mon, j_var, mon_vars, l, sign)) + return true; return false; } - bool generate_basic_lemma_for_mon_neutral(const mon_eq& m, lemma& l) { + bool generate_basic_lemma_for_mon_zero(unsigned i_mon, lemma& l) { return false; } - bool generate_basic_lemma_for_mon_proportionality(const mon_eq& m, lemma& l) { + bool generate_basic_lemma_for_mon_neutral(unsigned i_mon, lemma& l) { return false; } - bool generate_basic_lemma_for_mon(const mon_eq& m, lemma & l) { - return generate_basic_lemma_for_mon_sign(m, l) - || generate_basic_lemma_for_mon_zero(m, l) - || generate_basic_lemma_for_mon_neutral(m, l) - || generate_basic_lemma_for_mon_proportionality(m, l); + bool generate_basic_lemma_for_mon_proportionality(unsigned i_mon, lemma& l) { + return false; + } + + bool generate_basic_lemma_for_mon(unsigned i_mon, lemma & l) { + return generate_basic_lemma_for_mon_sign(i_mon, l) + || generate_basic_lemma_for_mon_zero(i_mon, l) + || generate_basic_lemma_for_mon_neutral(i_mon, l) + || generate_basic_lemma_for_mon_proportionality(i_mon, l); } bool generate_basic_lemma(lemma & l, svector & to_refine) { for (unsigned i : to_refine) - if (generate_basic_lemma_for_mon(m_monomials[i], l)) + if (generate_basic_lemma_for_mon(i, l)) return true; return false; } void map_monominals_vars(unsigned i) { const mon_eq& m = m_monomials[i]; - for (lp::var_index j : m.m_vs) { + for (lpvar j : m.m_vs) { auto it = m_var_to_monomials.find(j); if (it == m_var_to_monomials.end()) { auto vect = svector(); @@ -131,10 +221,12 @@ struct solver::imp { return l_undef; } - + }; -void solver::add_monomial(lp::var_index v, unsigned sz, lp::var_index const* vs) { - std::cout << "called add_monomial\n"; + + +void solver::add_monomial(lpvar v, unsigned sz, lpvar const* vs) { + m_imp->add(v, sz, vs); } bool solver::need_check() { return true; }