diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index f2e64ecef..cc824a909 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -28,27 +28,54 @@ namespace nlsat { }; struct levelwise::impl { polynomial_ref_vector const& m_P; - var m_max_x; + var m_n; assignment const& m_s; std::vector m_Q; // the set of properties to prove as in single_cell // max_x plays the role of n in algorith 1 of the levelwise paper. impl(polynomial_ref_vector const& ps, var max_x, assignment const& s) - : m_P(ps), m_max_x(max_x), m_s(s) { + : m_P(ps), m_n(max_x), m_s(s) { } - std::vector seed_initial_goals() { + std::vector seed_properties() { std::vector Q; // Algorithm 1: initial goals are sgn_inv(p, s) for p in ps at current level of max_x for (unsigned i = 0; i < m_P.size(); ++i) { poly* p = m_P.get(i); - Q.push_back(property_goal{ prop::sgn_inv_irreducible, p, /*s_idx*/0, /* level */ m_max_x}); + Q.push_back(property_goal{ prop::sgn_inv_irreducible, p, /*s_idx*/0, /* level */ m_n}); } return Q; } - - std::vector single_cell() { - return std::vector(); + struct result_struct { + symbolic_interval I; + std::vector Q; + bool status; + }; + + result_struct construct_interval() { + // TODO: Implement per Algorithm "construct_interval" in the paper: + // 1) Collect polynomials of level n (max_x) from m_P. + // 2) Compute relevant roots under current sample m_sample. + // 3) Build an interval I delimited by adjacent roots around s. + // 4) Select a representative sample within I. + // 5) Record properties (repr(I,s), sample(s), etc.) as needed. + // This is a placeholder skeleton; no-op for now. + result_struct ret; + return ret; } + // return an empty vector on failure + std::vector single_cell() { + std::vector ret; + std::vector Q = seed_properties(); + for (unsigned i = m_n; i >= 1; i--) { + auto result = construct_interval(); + if (result.status == false) + return std::vector(); // return empty + ret.push_back(result.I); + Q = result.Q; + } + + return ret; // the order is reversed! + } }; // constructor levelwise::levelwise(polynomial_ref_vector const& ps, var n, assignment const& s) @@ -56,75 +83,7 @@ namespace nlsat { levelwise::~levelwise() { delete m_impl; } - - std::vector levelwise::single_cell() { - /* struct impl { - polynomial_ref_vector const& m_P; - var m_n; - assignment const& m_sample; - std::vector m_goals; - // simple fact DB - struct key { - prop pr; - poly* p; - unsigned s_idx; - unsigned level; - bool operator==(key const& o) const noexcept { - return pr == o.pr && p == o.p && s_idx == o.s_idx && level == o.level; - } - }; - struct key_hash { - size_t operator()(key const& k) const noexcept { - size_t h = static_cast(k.pr); - h ^= (reinterpret_cast(k.p) >> 3) + 0x9e3779b97f4a7c15ULL + (h<<6) + (h>>2); - h ^= static_cast(k.s_idx) + 0x9e3779b9 + (h<<6) + (h>>2); - h ^= static_cast(k.level) + 0x9e3779b9 + (h<<6) + (h>>2); - return h; - } - }; - std::unordered_map m_index; // key -> fact id - std::vector m_facts; // id -> fact - std::vector m_worklist; - impl(polynomial_ref_vector const& ps_, var mx, assignment const& sa) - : m_P(ps_), m_n(mx), m_sample(sa) { - } - void derive_from(property_goal const& f) { - // Minimal rule: sgn_inv_irreducible(p) => non_null(p) and ir_ord(p) - if (f.prop == prop::sgn_inv_irreducible) { - intern(property_goal{ prop::non_null, f.p, f.s_idx, f.level }); - intern(property_goal{ prop::ir_ord, f.p, f.s_idx, f.level }); - } - } - struct result_struct { - symbolic_interval I; - std::vector Q; - bool status; - }; - // Construct an interval at level n = m_max_x around the current sample s per the levelwise paper. - result_struct construct_interval() { - // TODO: Implement per Algorithm "construct_interval" in the paper: - // 1) Collect polynomials of level n (max_x) from m_P. - // 2) Compute relevant roots under current sample m_sample. - // 3) Build an interval I delimited by adjacent roots around s. - // 4) Select a representative sample within I. - // 5) Record properties (repr(I,s), sample(s), etc.) as needed. - // This is a placeholder skeleton; no-op for now. - result_struct ret; - return ret; - } - std::vector single_cell() { - std::vector ret; - std::vector Q = seed_properties(); - for (unsigned i = m_n; i >= 1; i--) { - auto result = construct_interval(); - if (result.status == false) - return std::vector(); - Q - } - } - }; // end of impl structure - */ - + std::vector levelwise::single_cell() { return m_impl->single_cell(); } diff --git a/src/nlsat/levelwise.h b/src/nlsat/levelwise.h index 92ad076a4..9ca585525 100644 --- a/src/nlsat/levelwise.h +++ b/src/nlsat/levelwise.h @@ -4,9 +4,32 @@ namespace nlsat { class assignment; // forward declared in nlsat_types.h - struct symbolic_interval {}; class levelwise { + public: + struct indexed_root_expr { + poly* p; + short i; + }; + struct symbolic_interval { + bool section = true; + poly* l = nullptr; + short l_index; // the root index + poly* u = nullptr; + short u_index; // the root index + bool l_inf() const { return l == nullptr; } + bool u_inf() const { return u == nullptr; } + bool is_section() { return section; } + bool is_sector() { return !section; } + poly* section_poly() { + SASSERT(is_section()); + return l; + } + }; + + private: + + struct impl; impl* m_impl; public: