From 0a86bd14f792ef5fadb8eeb346729a612f7e1588 Mon Sep 17 00:00:00 2001 From: Lev Date: Tue, 9 Oct 2018 11:28:08 -0700 Subject: [PATCH] start on test nla Signed-off-by: Lev --- src/test/lp/lp.cpp | 10 ++++----- src/util/lp/nla_solver.cpp | 46 +++++++++++++++++++++----------------- src/util/lp/nla_solver.h | 2 +- 3 files changed, 31 insertions(+), 27 deletions(-) diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index fe3128159..a4bd66d2f 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -1896,7 +1896,7 @@ void test_replace_column() { void setup_args_parser(argument_parser & parser) { - parser.add_option_with_help_string("-nla", "test nla_solver"); + parser.add_option_with_help_string("-nla_fact", "test nla_solver"); parser.add_option_with_help_string("-hnf", "test hermite normal form"); parser.add_option_with_help_string("-gomory", "gomory"); parser.add_option_with_help_string("-intd", "test integer_domain"); @@ -3548,8 +3548,8 @@ void test_gomory_cut() { test_gomory_cut_1(); } -void test_nla() { - nla::solver::test(); +void test_nla_factorization() { + nla::solver::test_factorization(); } void test_lp_local(int argn, char**argv) { @@ -3568,9 +3568,9 @@ void test_lp_local(int argn, char**argv) { args_parser.print(); - if (args_parser.option_is_used("-nla")) { + if (args_parser.option_is_used("-nla_fact")) { #ifdef Z3DEBUG - test_nla(); + test_nla_factorization(); #endif return finalize(0); } diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 470859afb..086065f90 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -38,13 +38,16 @@ 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; - unsigned_vector m_monomials_lim; + std::unordered_map, + vector, + hash_svector> + m_rooted_monomials; + // this field is used for push/pop operations + unsigned_vector m_monomials_counts; lp::lar_solver& m_lar_solver; - std::unordered_map m_var_containing_monomials; + std::unordered_map m_monomials_containing_var; // monomial.var() -> monomial index u_map m_var_to_its_monomial; @@ -67,16 +70,16 @@ struct solver::imp { } void push() { - m_monomials_lim.push_back(m_monomials.size()); + m_monomials_counts.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); + m_monomials.shrink(m_monomials_counts[m_monomials_counts.size() - n]); + m_monomials_counts.shrink(m_monomials_counts.size() - n); } - // make sure that the monomial value is the product of the values of the factors + // return true if the monomial value is equal to the product of the values of the factors 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()); @@ -147,8 +150,9 @@ struct solver::imp { } // Replaces each variable index by the root in the tree and flips the sign if the var comes with a minus. + // Also sorts the result. // - svector reduce_monomial_to_canonical(const svector & vars, rational & sign) const { + svector reduce_monomial_to_rooted(const svector & vars, rational & sign) const { svector ret; sign = 1; for (lpvar v : vars) { @@ -167,7 +171,7 @@ struct solver::imp { // monomial_coeff canonize_monomial(monomial const& m) const { rational sign = rational(1); - svector vars = reduce_monomial_to_canonical(m.vars(), sign); + svector vars = reduce_monomial_to_rooted(m.vars(), sign); return monomial_coeff(m.var(), vars, sign); } @@ -226,7 +230,7 @@ struct solver::imp { // otherwise it remains false // Returns 2 if the sign is not defined. int get_mon_sign_zero_var(unsigned j, bool & strict) { - if (m_var_containing_monomials.find(j) == m_var_containing_monomials.end()) + if (m_monomials_containing_var.find(j) == m_monomials_containing_var.end()) return 2; lpci lci = -1; lpci uci = -1; @@ -518,7 +522,7 @@ struct solver::imp { bool basic_lemma_for_mon_neutral(unsigned i_mon) { const monomial & m = m_monomials[i_mon]; rational sign; - svector reduced_vars = reduce_monomial_to_canonical(m.vars(), sign); + svector reduced_vars = reduce_monomial_to_rooted(m.vars(), sign); rational v = m_lar_solver.get_column_value_rational(m.var()); if (sign == -1) v = -v; @@ -753,7 +757,7 @@ struct solver::imp { svector mask(large.size(), false); // init mask by false const auto & m = m_monomials[i_mon]; rational sign; - auto vars = reduce_monomial_to_canonical(m.vars(), sign); + auto vars = reduce_monomial_to_rooted(m.vars(), sign); auto vars_copy = vars; auto v = lp::abs(m_lar_solver.get_column_value_rational(m.var())); // We cross out from vars the "large" variables represented by the mask @@ -784,7 +788,7 @@ struct solver::imp { svector mask(_small.size(), false); // init mask by false const auto & m = m_monomials[i_mon]; rational sign; - auto vars = reduce_monomial_to_canonical(m.vars(), sign); + auto vars = reduce_monomial_to_rooted(m.vars(), sign); auto vars_copy = vars; auto v = lp::abs(m_lar_solver.get_column_value_rational(m.var())); // We cross out from vars the "large" variables represented by the mask @@ -1114,11 +1118,11 @@ struct solver::imp { void map_monomial_vars_to_monomial_indices(unsigned i) { const monomial& m = m_monomials[i]; for (lpvar j : m.vars()) { - auto it = m_var_containing_monomials.find(j); - if (it == m_var_containing_monomials.end()) { - unsigned_vector v; - v.push_back(i); - m_var_containing_monomials[j] = v; + auto it = m_monomials_containing_var.find(j); + if (it == m_monomials_containing_var.end()) { + unsigned_vector ms; + ms.push_back(i); + m_monomials_containing_var[j] = ms; } else { it->second.push_back(i); @@ -1289,7 +1293,7 @@ solver::~solver() { dealloc(m_imp); } -void solver::test() { +void solver::test_factorization() { lp::lar_solver s; unsigned a = 0, b = 1, c = 2, d = 3, e = 4, abcde = 5, ac = 6, bde = 7, acd = 8, be = 9; diff --git a/src/util/lp/nla_solver.h b/src/util/lp/nla_solver.h index 40afaa8bb..1de009013 100644 --- a/src/util/lp/nla_solver.h +++ b/src/util/lp/nla_solver.h @@ -46,6 +46,6 @@ public: void pop(unsigned scopes); bool need_check(); lbool check(lp::explanation&, lemma&); - static void test(); + static void test_factorization(); }; }