diff --git a/src/math/lp/active_set.h b/src/math/lp/active_set.h deleted file mode 100644 index 3b2ead8c2..000000000 --- a/src/math/lp/active_set.h +++ /dev/null @@ -1,76 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - - -Abstract: - - - -Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - -Revision History: - - ---*/ - -#pragma once -#include "math/lp/binary_heap_priority_queue.h" -namespace lp { -class active_set { - std::unordered_set m_cs; - binary_heap_priority_queue m_q; - std::unordered_map m_id_to_constraint; -public: - std::unordered_set cs() const { return m_cs;} - - bool contains(const constraint* c) const { - return m_id_to_constraint.find(c->id()) != m_id_to_constraint.end(); - } - - bool is_empty() const { return m_cs.size() == 0; } - // low priority will be dequeued first - void add_constraint(constraint* c, int priority) { - if (contains(c)) - return; - m_cs.insert(c); - m_id_to_constraint[c->id()] = c; - m_q.enqueue(c->id(), priority); - } - - void clear() { - m_cs.clear(); - m_id_to_constraint.clear(); - m_q.clear(); - } - - - constraint* remove_constraint() { - if (m_cs.size() == 0) - return nullptr; - unsigned id = m_q.dequeue(); - auto it = m_id_to_constraint.find(id); - lp_assert(it != m_id_to_constraint.end()); - constraint* c = it->second; - m_cs.erase(c); - m_id_to_constraint.erase(it); - return c; - } - - unsigned size() const { - return static_cast(m_cs.size()); - } - - void remove_constraint(constraint * c) { - if (! contains(c)) return; - - m_cs.erase(c); - m_id_to_constraint.erase(c->id()); - m_q.remove(c->id()); - } -}; -} diff --git a/src/math/lp/constraint.h b/src/math/lp/constraint.h deleted file mode 100644 index 84ec188d6..000000000 --- a/src/math/lp/constraint.h +++ /dev/null @@ -1,99 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - - -Abstract: - - - -Author: - Nikolaj Bjorner (nbjorner) - Lev Nachmanson (levnach) - -Revision History: - - ---*/ - -#pragma once -namespace lp { -class constraint; // forward definition -struct constraint_hash { - size_t operator() (const constraint* c) const; -}; - -struct constraint_equal { - bool operator() (const constraint * a, const constraint * b) const; -}; - -class constraint { // we only have less or equal for the inequality sign, which is enough for integral variables - int m_id; - bool m_is_ineq; - polynomial m_poly; - mpq m_d; // the divider for the case of a divisibility constraint - std::unordered_set m_assert_origins; // these indices come from the client and get collected during tightening -public : - unsigned id() const { return m_id; } - const polynomial & poly() const { return m_poly; } - polynomial & poly() { return m_poly; } - std::unordered_set & assert_origins() { return m_assert_origins;} - const std::unordered_set & assert_origins() const { return m_assert_origins;} - bool is_lemma() const { return !is_assert(); } - bool is_assert() const { return m_assert_origins.size() == 1; } - bool is_ineq() const { return m_is_ineq; } - const mpq & divider() const { return m_d; } -public: - constraint( - unsigned id, - constraint_index assert_origin, - const polynomial & p, - bool is_ineq): - m_id(id), - m_is_ineq(is_ineq), - m_poly(p) - { // creates an assert - m_assert_origins.insert(assert_origin); - } - constraint( - unsigned id, - const std::unordered_set& origins, - const polynomial & p, - bool is_ineq): - m_id(id), - m_is_ineq(is_ineq), - m_poly(p), - m_assert_origins(origins) - {} - - - - constraint( - unsigned id, - const polynomial & p, - bool is_ineq): - m_id(id), - m_is_ineq(is_ineq), - m_poly(p) { // creates a lemma - } - -public: - constraint() {} - - const mpq & coeff(var_index j) const { - return m_poly.coeff(j); - } - const vector& coeffs() const { return m_poly.m_coeffs;} - - bool is_tight(unsigned j) const { - const mpq & a = m_poly.coeff(j); - return a == 1 || a == -1; - } - void add_predecessor(const constraint* p) { - lp_assert(p != nullptr); - for (auto m : p->assert_origins()) - m_assert_origins.insert(m); } -}; -} diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp index 506a6de78..a3875e761 100644 --- a/src/math/lp/horner.cpp +++ b/src/math/lp/horner.cpp @@ -39,7 +39,7 @@ bool horner::row_has_monomial_to_refine(const T& row) const { // Returns true if the row has at least two monomials sharing a variable template bool horner::row_is_interesting(const T& row) const { - TRACE("nla_solver", m_core->print_term(row, tout);); + TRACE("nla_solver_details", m_core->print_term(row, tout);); SASSERT(row_has_monomial_to_refine(row)); std::unordered_set seen; for (const auto& p : row) { @@ -67,6 +67,7 @@ bool horner::lemmas_on_expr(nex& e) { TRACE("nla_horner", tout << "e = " << e << "\n";); bool conflict = false; cross_nested cn(e, [this, & conflict](const nex& n) { + TRACE("nla_horner", tout << "cross-nested n = " << n << "\n";); auto i = interval_of_expr(n); TRACE("nla_horner", tout << "callback n = " << n << "\ni="; m_intervals.display(tout, i) << "\n";); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 209003c6f..9150e7aa2 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1257,7 +1257,7 @@ lbool core::inner_check(bool derived) { return l_false; } - TRACE("nla_cn_details", print_terms(tout);); + TRACE("nla_solver", print_terms(tout); m_lar_solver.print_constraints(tout);); for (int search_level = 0; search_level < 3 && !done(); search_level++) { TRACE("nla_solver", tout << "derived = " << derived << ", search_level = " << search_level << "\n";); if (search_level == 0) { diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 3d9eba088..5fee3abc0 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -289,9 +289,6 @@ public: lp::lp_settings& lp_settings(); const lp::lp_settings& lp_settings() const; unsigned random(); - void map_monomial_vars_to_monomial_indices(unsigned i); - - void map_vars_to_monomials(); // we look for octagon constraints here, with a left part +-x +- y void collect_equivs();