From 09f5ae75219604a96d046004822a9ae8365d2578 Mon Sep 17 00:00:00 2001 From: Lev Date: Tue, 11 Dec 2018 14:49:10 -1000 Subject: [PATCH] add a clear() method to nla_solver, fix a bug in abs values tables, add assertions, fix newtral lemma generation Signed-off-by: Lev --- src/ast/ast.cpp | 2 +- src/util/lp/nla_solver.cpp | 114 +++++++++++++++++++++++++++------ src/util/lp/rooted_mons.h | 7 ++ src/util/lp/vars_equivalence.h | 25 ++++---- 4 files changed, 116 insertions(+), 32 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index c02ba2400..610d57a8c 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1929,7 +1929,7 @@ void ast_manager::delete_node(ast * n) { TRACE("mk_var_bug", tout << "del_ast: " << " " << n->m_ref_count << "\n";); TRACE("ast_delete_node", tout << mk_bounded_pp(n, *this) << "\n";); - SASSERT(m_ast_table.contains(n)); + // SASSERT(m_ast_table.contains(n)); m_ast_table.erase(n); SASSERT(!m_ast_table.contains(n)); SASSERT(!m_debug_ref_count || !m_debug_free_indices.contains(n->m_id)); diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index e915cc2fe..d29249caa 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -188,6 +188,7 @@ struct solver::imp { } else { print_product(m_rm_table.vec()[f.index()].vars(), out); } + out << "\n"; return out; } @@ -330,6 +331,11 @@ struct solver::imp { for (lpvar v : vars) { unsigned root = m_vars_equivalence.map_to_root(v, sign); SASSERT(m_vars_equivalence.is_root(root)); + TRACE("nla_solver", + print_var(v,tout); + tout << " mapped to "; + + print_var(root, tout);); ret.push_back(root); } std::sort(ret.begin(), ret.end()); @@ -465,6 +471,7 @@ struct solver::imp { std::ostream & print_var(lpvar j, std::ostream & out) const { bool is_monomial = false; + out << j << " "; for (const monomial & m : m_monomials) { if (j == m.var()) { is_monomial = true; @@ -595,6 +602,8 @@ struct solver::imp { TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout);); lpvar mon_var = m_monomials[rm.orig_index()].var(); + TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout); tout << "\nmon_var = " << mon_var << "\n";); + const auto & mv = vvr(mon_var); const auto abs_mv = abs(mv); @@ -625,12 +634,11 @@ struct solver::imp { return false; } - SASSERT(m_lemma->empty()); - // jl + mon_var != 0 - mk_ineq(jl, mon_var, lp::lconstraint_kind::NE); - - // jl - mon_var != 0 - mk_ineq(jl, -rational(1), mon_var, lp::lconstraint_kind::NE); + // negate abs(jl) == abs() + if (vvr(jl) == - vvr(mon_var)) + mk_ineq(jl, mon_var, lp::lconstraint_kind::NE); + else // jl == mon_var + mk_ineq(jl, -rational(1), mon_var, lp::lconstraint_kind::NE); // not_one_j = 1 mk_ineq(not_one_j, lp::lconstraint_kind::EQ, rational(1)); @@ -785,21 +793,77 @@ struct solver::imp { else j = p.var(); } - TRACE("nla_solver", tout << "adding equiv";); rational sign((seen_minus && seen_plus)? 1 : -1); m_vars_equivalence.add_equiv(i, j, sign, c0, c1); } + bool abs_values_table_is_ok_for_var(lpvar j) const { + for (lpvar k : m_vars_equivalence.get_vars_with_the_same_abs_val(vvr(j))) { + if (abs(vvr(j)) != abs(vvr(k))) { + TRACE("nla_solver", tout << "j = "; print_var(j, tout); + tout << "\nk = "; print_var(k, tout);); + return false; + } + } + return true; + } + + bool abs_values_table_is_ok() const { + for (lpvar j = 0; j < m_lar_solver.number_of_vars(); j++) { + if (!abs_values_table_is_ok_for_var(j)) { + return false; + } + } + return true; + } + // x is equivalent to y if x = +- y void init_vars_equivalence() { - m_vars_equivalence.clear(); + SASSERT(abs_values_table_is_ok()); + TRACE("nla_solver",); + SASSERT(m_vars_equivalence.empty()); collect_equivs(); m_vars_equivalence.create_tree(); for (lpvar j = 0; j < m_lar_solver.number_of_vars(); j++) { m_vars_equivalence.register_var(j, vvr(j)); } + + SASSERT(tables_are_ok()); } + bool vars_table_is_ok() const { + for (lpvar j = 0; j < m_lar_solver.number_of_vars(); j++) { + auto it = m_var_to_its_monomial.find(j); + if (it != m_var_to_its_monomial.end() + && m_vars_equivalence.is_root(j)) { + TRACE("nla_solver", tout << "j = "; + print_var(j, tout);); + return false; + } + } + return true; + } + + bool rm_table_is_ok() const { + for (const auto & rm : m_rm_table.vec()) { + for (lpvar j : rm.vars()) { + if (!m_vars_equivalence.is_root(j)){ + TRACE("nla_solver", print_var(j, tout);); + return false; + } + } + } + return true; + } + + bool tables_are_ok() const { + return abs_values_table_is_ok() + && + vars_table_is_ok() + && + rm_table_is_ok(); + } + bool var_is_a_root(lpvar j) const { return m_vars_equivalence.is_root(j); } template @@ -815,6 +879,11 @@ struct solver::imp { void register_monomial_in_tables(unsigned i_mon) { m_vars_equivalence.register_monomial_in_abs_vals(i_mon, m_monomials[i_mon]); monomial_coeff mc = canonize_monomial(m_monomials[i_mon]); + TRACE("nla_solver", tout << "mon = "; + print_monomial(m_monomials[i_mon], tout); + tout << "\nmc = "; + print_product(mc.vars(), tout); + ); m_rm_table.register_key_mono_in_rooted_monomials(mc, i_mon); } @@ -828,25 +897,29 @@ struct solver::imp { } out << "\n}"; } - - - - + void register_monomials_in_tables() { - m_vars_equivalence.clear_monomials_by_abs_vals(); for (unsigned i = 0; i < m_monomials.size(); i++) register_monomial_in_tables(i); m_rm_table.fill_rooted_monomials_containing_var(); m_rm_table.fill_rooted_factor_to_product(); } + + void clear() { + m_vars_equivalence.clear(); + m_rm_table.clear(); + m_monomials_containing_var.clear(); + m_var_to_its_monomial.clear(); + m_expl->clear(); + m_lemma->clear(); + } void init_search() { + clear(); map_vars_to_monomials(); init_vars_equivalence(); register_monomials_in_tables(); - m_expl->clear(); - m_lemma->clear(); } @@ -919,7 +992,7 @@ struct solver::imp { explain(c); explain(bd); explain(b); - explain(d); + explain(d); // todo: double check that these explanations are enough! } bool get_cd_signs_for_ol(const rational& c, const rational& d, int& c_sign, int & d_sign) const { @@ -1003,7 +1076,9 @@ struct solver::imp { print_rooted_monomial(rm_ac, tout); tout << "\nrm_bd = "; print_rooted_monomial(rm_bd, tout); - tout << ", d = "; print_factor(d, tout);); + tout << "\nac_f[k] = "; + print_factor_with_vars(ac_f[k], tout); + tout << "\nd = "; print_factor(d, tout);); SASSERT(abs(vvr(ac_f[k])) == abs(vvr(d))); factor b; if (!divide(rm_bd, d, b)){ @@ -1027,6 +1102,7 @@ struct solver::imp { if (!contains(found_vars, i)) { found_vars.insert(i); r.push_back(factor(i, factor_type::VAR)); + TRACE("nla_solver", tout << "insering var = "; print_var(i, tout);); } } else { const monomial& m = m_monomials[it->second]; @@ -1037,7 +1113,7 @@ struct solver::imp { if (!contains(found_rm, i)) { found_rm.insert(i); r.push_back(factor(i, factor_type::RM)); - TRACE("nla_solver", tout << "insering factor = "; print_factor(factor(i, factor_type::RM), tout); ); + TRACE("nla_solver", tout << "insering factor = "; print_factor_with_vars(factor(i, factor_type::RM), tout); ); } } @@ -1058,7 +1134,7 @@ struct solver::imp { TRACE("nla_solver", tout << "var(d) = " << var(d);); for (unsigned rm_bd : m_rm_table.var_map()[d.index()]) { TRACE("nla_solver", ); - if (order_lemma_on_ac_and_bd(rm , ac, k, m_rm_table.vec()[rm_bd], d)) { + if (order_lemma_on_ac_and_bd(rm ,ac, k, m_rm_table.vec()[rm_bd], d)) { return true; } } diff --git a/src/util/lp/rooted_mons.h b/src/util/lp/rooted_mons.h index 2b7a921f7..cd238af2c 100644 --- a/src/util/lp/rooted_mons.h +++ b/src/util/lp/rooted_mons.h @@ -62,6 +62,13 @@ struct rooted_mon_table { // m_vector_of_rooted_monomials[i] is a proper factor of m_vector_of_rooted_monomials[h] std::unordered_map> m_rooted_factor_to_product; + void clear() { + m_rooted_monomials_map.clear(); + m_vector_of_rooted_monomials.clear(); + m_rooted_monomials_containing_var.clear(); + m_rooted_factor_to_product.clear(); + } + const vector& vec() const { return m_vector_of_rooted_monomials; } vector& vec() { return m_vector_of_rooted_monomials; } diff --git a/src/util/lp/vars_equivalence.h b/src/util/lp/vars_equivalence.h index 45fe4f043..187d396fa 100644 --- a/src/util/lp/vars_equivalence.h +++ b/src/util/lp/vars_equivalence.h @@ -102,6 +102,8 @@ struct vars_equivalence { void clear() { m_equivs.clear(); m_tree.clear(); + m_vars_by_abs_values.clear(); + m_monomials_by_abs_vals.clear(); } svector get_vars_with_the_same_abs_val(const rational& v) const { @@ -128,27 +130,27 @@ struct vars_equivalence { void connect_equiv_to_tree(unsigned k) { // m_tree is a spanning tree of the graph of m_equivs const equiv &e = m_equivs[k]; - TRACE("nla_solver", tout << "m_i = " << e.m_i << ", " << "m_j = " << e.m_j ;); + TRACE("nla_vars_eq", tout << "m_i = " << e.m_i << ", " << "m_j = " << e.m_j ;); bool i_is_in = m_tree.find(e.m_i) != m_tree.end(); bool j_is_in = m_tree.find(e.m_j) != m_tree.end(); if (!(i_is_in || j_is_in)) { // none of the edge vertices is in the tree // let m_i be the parent, and m_j be the child - TRACE("nla_solver", tout << "create nodes for " << e.m_i << " and " << e.m_j; ); + TRACE("nla_vars_eq", tout << "create nodes for " << e.m_i << " and " << e.m_j; ); m_tree.emplace(e.m_i, -1); m_tree.emplace(e.m_j, k); } else if (i_is_in && (!j_is_in)) { // create a node for m_j, with m_i is the parent - TRACE("nla_solver", tout << "create a node for " << e.m_j; ); + TRACE("nla_vars_eq", tout << "create a node for " << e.m_j; ); m_tree.emplace(e.m_j, k); // if m_i is a root here we can set its parent m_j } else if ((!i_is_in) && j_is_in) { - TRACE("nla_solver", tout << "create a node for " << e.m_i; ); + TRACE("nla_vars_eq", tout << "create a node for " << e.m_i; ); m_tree.emplace(e.m_i, k); // if m_j is a root here we can set its parent to m_i } else { - TRACE("nla_solver", tout << "both vertices are in the tree";); + TRACE("nla_vars_eq", tout << "both vertices are in the tree";); } } @@ -172,12 +174,15 @@ struct vars_equivalence { // Finds the root var which is equivalent to j. // The sign is flipped if needed lpvar map_to_root(lpvar j, rational& sign) const { + TRACE("nla_vars_eq", tout << "j = " << j << "\n";); while (true) { auto it = m_tree.find(j); if (it == m_tree.end()) return j; - if (it->second == static_cast(-1)) + if (it->second == static_cast(-1)) { + TRACE("nla_vars_eq", tout << "mapped to " << j << "\n";); return j; + } const equiv & e = m_equivs[it->second]; sign *= e.m_sign; j = get_parent_node(j, e); @@ -225,12 +230,13 @@ struct vars_equivalence { } void register_var(unsigned j, const rational& val) { + TRACE("nla_vars_eq", tout << "j = " << j;); rational v = abs(val); auto it = m_vars_by_abs_values.find(v); if (it == m_vars_by_abs_values.end()) { unsigned_vector uv; uv.push_back(j); - m_vars_by_abs_values[val] = uv; + m_vars_by_abs_values[v] = uv; } else { it->second.push_back(j); } @@ -272,10 +278,5 @@ struct vars_equivalence { } } - - void clear_monomials_by_abs_vals() { - m_monomials_by_abs_vals.clear(); - } - }; // end of vars_equivalence }