From 516a3d55948f959e23bafa9456ae71ca242fb6a2 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 12 Aug 2025 18:25:20 -0700 Subject: [PATCH] scaffolding Signed-off-by: Lev Nachmanson --- src/nlsat/levelwise.cpp | 341 +++++++----------------------------- src/nlsat/levelwise.h | 22 ++- src/nlsat/nlsat_explain.cpp | 2 +- 3 files changed, 87 insertions(+), 278 deletions(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 41193ab9c..67dfe864f 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -1,290 +1,79 @@ -#include "levelwise.h" +#include "nlsat/levelwise.h" +#include "nlsat/nlsat_types.h" #include -#include -#include - namespace nlsat { - // Context for property propagation (e.g., which case of rule 4.2 applies) - enum class property_mapping_case : unsigned { - case1 = 0, - case2 = 1, - case3 = 2, - }; +// Local enums reused from previous scaffolding +enum class property_mapping_case : unsigned { case1 = 0, case2 = 1, case3 = 2 }; - /** - * Properties for indexed roots, in the order specified by the levelwise paper. - * The order is important for the algorithm and must match the paper exactly. - */ - enum class polynom_property : unsigned { - ir_ord, // ir_ord(≼, s) for all ≼ for roots of level i and s ∈ Ri−1 - an_del, // an_del(p) for all p of level i - non_null, // non_null(p) for all p of level i - ord_inv_reducible, // ord_inv(p) for all reducible p of level i - ord_inv_irreducible, // ord_inv(p) for all irreducible p of level i - sgn_inv_reducible, // sgn_inv(p) for all reducible p of level i - sgn_inv_irreducible, // sgn_inv(p) for all irreducible p of level i - connected, // connected(i) - an_sub, // an_sub(i) - sample, // sample(s) for all s ∈ Ri of level i - repr, // repr(I, s) for all I of level i and s ∈ ... - holds, // marker for "goal holds" (terminal) - _count // always last: number of properties - }; +enum class polynom_property : unsigned { + ir_ord, + an_del, + non_null, + sgn_inv_reducible, + sgn_inv_irreducible, + connected, + an_sub, + sample, + repr, + holds, + _count +}; +struct property_goal { + polynom_property prop; + poly* p = nullptr; + unsigned s_idx = 0; // index into current sample roots on level, if applicable + unsigned level = 0; +}; +struct levelwise::impl { + polynomial_ref_vector const& m_ps; + var m_max_x; + assignment const& m_sample; + std::vector m_goals; - // Utility: property to string (for debugging, logging, etc.) - inline const char* to_string(polynom_property prop) { - switch (prop) { - case polynom_property::ir_ord: return "ir_ord"; - case polynom_property::an_del: return "an_del"; - case polynom_property::non_null: return "non_null"; - case polynom_property::ord_inv_reducible: return "ord_inv_reducible"; - case polynom_property::ord_inv_irreducible: return "ord_inv_irreducible"; - case polynom_property::sgn_inv_reducible: return "sgn_inv_reducible"; - case polynom_property::sgn_inv_irreducible: return "sgn_inv_irreducible"; - case polynom_property::connected: return "connected"; - case polynom_property::an_sub: return "an_sub"; - case polynom_property::sample: return "sample"; - case polynom_property::repr: return "repr"; - case polynom_property::holds: return "holds"; - default: return "?"; + impl(polynomial_ref_vector const& ps, var max_x, assignment const& s) + : m_ps(ps), m_max_x(max_x), m_sample(s) { + seed_initial_goals(); + } + void seed_initial_goals() { + // 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_ps.size(); ++i) { + poly* p = m_ps.get(i); + m_goals.push_back(property_goal{ polynom_property::sgn_inv_irreducible /*or reducible later*/, p, /*s_idx*/0, /*level*/0}); } } +}; - // A single property instance ("fact") subject. - // Note: Not all fields are used by every property; unused fields are left at defaults. - struct property_inst { - polynom_property prop; - // Optional subject parameters - poly* p = nullptr; // for properties about a polynomial p - var y = -1; // variable (e.g., indexed root variable) - unsigned i = 0; // level/index (paper's i) - unsigned s_idx = 0; // index for "s ∈ R_i" (sample/root index), if applicable - unsigned I_idx = 0; // index for interval I (for repr), if applicable - unsigned ord_id = 0; // identifier for an indexed root ordering ≼, if applicable +levelwise::levelwise(polynomial_ref_vector const& ps, var max_x, assignment const& s) + : m_impl(new impl(ps, max_x, s)) {} - // Convenience builders - static property_inst of(poly* p, polynom_property prop, unsigned level) { - property_inst r{prop}; r.p = p; r.i = level; return r; +levelwise::~levelwise() { delete m_impl; } +levelwise::levelwise(levelwise&& o) noexcept : m_impl(o.m_impl) { o.m_impl = nullptr; } + +levelwise& levelwise::operator=(levelwise&& o) noexcept { if (this != &o) { delete m_impl; m_impl = o.m_impl; o.m_impl = nullptr; } return *this; } + +// Free-function driver: create a local implementation and seed initial goals. +void levelwise_project(polynomial_ref_vector const& ps, var max_x, assignment const& s) { + struct impl { + polynomial_ref_vector const& m_ps; + var m_max_x; + assignment const& m_sample; + std::vector m_goals; + impl(polynomial_ref_vector const& ps_, var mx, assignment const& sa) + : m_ps(ps_), m_max_x(mx), m_sample(sa) { + seed_initial_goals(); } - static property_inst at_level(polynom_property prop, unsigned level) { - property_inst r{prop}; r.i = level; return r; - } - static property_inst sample_at(unsigned s_idx, unsigned level) { - property_inst r{polynom_property::sample}; r.s_idx = s_idx; r.i = level; return r; - } - static property_inst repr_of(unsigned I_idx, unsigned s_idx, unsigned level) { - property_inst r{polynom_property::repr}; r.I_idx = I_idx; r.s_idx = s_idx; r.i = level; return r; - } - - // Display - std::string str() const { - std::ostringstream out; - out << to_string(prop) << "("; - bool first = true; - auto add = [&](std::string const& k, uint64_t v) { - if (!first) out << ", "; - first = false; - out << k << "=" << v; - }; - if (p) add("p", reinterpret_cast(p)); - if (y != -1) add("y", static_cast(y)); - add("i", i); - if (s_idx) add("s", s_idx); - if (I_idx) add("I", I_idx); - if (ord_id) add("ord", ord_id); - out << ")"; - return out.str(); - } - - // Equality (coarse; pointer identity for p is intentional) - bool operator==(property_inst const& o) const { - return prop == o.prop && - p == o.p && - y == o.y && - i == o.i && - s_idx == o.s_idx && - I_idx == o.I_idx && - ord_id == o.ord_id; - } - }; - - // Proof rule identifiers (align roughly with paper sections; can be refined later). - enum class proof_rule : unsigned { - // Skeleton rules; refine/extend as we implement specific inferences - axiom, // introduce a known/assumed property - derive, // generic derivation step (placeholder) - r_ir_ord, // rules for ir_ord propagation - r_an_del, - r_non_null, - r_ord_inv_red, - r_ord_inv_irred, - r_sgn_inv_red, - r_sgn_inv_irred, - r_connected, - r_an_sub, - r_sample, - r_repr, - r_close_holds // closes to 'holds' - }; - - inline const char* to_string(proof_rule r) { - switch (r) { - case proof_rule::axiom: return "axiom"; - case proof_rule::derive: return "derive"; - case proof_rule::r_ir_ord: return "r_ir_ord"; - case proof_rule::r_an_del: return "r_an_del"; - case proof_rule::r_non_null: return "r_non_null"; - case proof_rule::r_ord_inv_red: return "r_ord_inv_red"; - case proof_rule::r_ord_inv_irred:return "r_ord_inv_irred"; - case proof_rule::r_sgn_inv_red: return "r_sgn_inv_red"; - case proof_rule::r_sgn_inv_irred:return "r_sgn_inv_irred"; - case proof_rule::r_connected: return "r_connected"; - case proof_rule::r_an_sub: return "r_an_sub"; - case proof_rule::r_sample: return "r_sample"; - case proof_rule::r_repr: return "r_repr"; - case proof_rule::r_close_holds: return "r_close_holds"; - default: return "?"; - } - } - - // A single proof step: premises -> conclusion, with metadata. - struct proof_step { - proof_rule rule; - property_mapping_case ctx = property_mapping_case::case1; // for multi-case rules (e.g., 4.2) - std::vector premises; // indices into facts_ - unsigned conclusion; // index into facts_ - - std::string str(std::vector const& facts) const { - std::ostringstream out; - out << to_string(rule) << "[case=" << static_cast(ctx) << "]: "; - out << "{"; - for (unsigned k = 0; k < premises.size(); ++k) { - if (k) out << ", "; - out << facts[premises[k]].str(); + void seed_initial_goals() { + for (unsigned i = 0; i < m_ps.size(); ++i) { + poly* p = m_ps.get(i); + m_goals.push_back(property_goal{ polynom_property::sgn_inv_irreducible, p, /*s_idx*/0, /*level*/0 }); } - out << "} => " << facts[conclusion].str(); - return out.str(); } - }; - - // A lightweight proof object to manage facts and steps. - class levelwise_proof { - std::vector m_facts; - std::vector m_steps; - - // Linear lookup to avoid hashing complexity here. - int find_fact(property_inst const& f) const { - for (unsigned i = 0; i < m_facts.size(); ++i) - if (m_facts[i] == f) return static_cast(i); - return -1; + void run() { + // TODO: apply Levelwise rules to discharge goals and build a proof. } + } I(ps, max_x, s); + I.run(); +} - public: - unsigned intern_fact(property_inst const& f) { - int idx = find_fact(f); - if (idx >= 0) return static_cast(idx); - m_facts.push_back(f); - return static_cast(m_facts.size() - 1); - } - - unsigned add_axiom(property_inst const& concl) { - unsigned c = intern_fact(concl); - m_steps.push_back(proof_step{proof_rule::axiom, property_mapping_case::case1, {}, c}); - return c; - } - - unsigned add_step(proof_rule rule, - property_mapping_case ctx, - std::vector const& premises, - property_inst const& conclusion) { - unsigned c = intern_fact(conclusion); - m_steps.push_back(proof_step{rule, ctx, premises, c}); - return c; - } - - std::string dump() const { - std::ostringstream out; - for (auto const& st : m_steps) - out << st.str(m_facts) << "\n"; - return out.str(); - } - - std::vector const& facts() const { return m_facts; } - std::vector const& steps() const { return m_steps; } - }; - - // Property propagation mapping: for each property, the set of properties it implies (see levelwise paper, e.g., rule 4.2) - // Overload: property_dependencies with context (for rules like 4.2 with multiple cases). - // Note: This is a scaffold. Fill per paper’s precise rules (TODO). - inline std::vector - get_property_dependencies(polynom_property prop, property_mapping_case /*p_case*/, polynomial_ref& /*p*/, unsigned /*i*/) { - std::vector ret; - switch (prop) { - case polynom_property::ir_ord: - // TODO: fill using Property 4.3 / Rule 4.2 cases; currently no direct property implications recorded here. - break; - - case polynom_property::an_del: - // Example: an_del(p) might imply non_null(p) or be used in combination with others; leave empty until specified. - break; - - case polynom_property::non_null: - // Usually terminal for p; no generic implications without context. - break; - - case polynom_property::ord_inv_reducible: - // Often accompanies sign invariance for reducible polynomials; no generic implication recorded here. - break; - - case polynom_property::ord_inv_irreducible: - // Likewise for irreducible. - break; - - case polynom_property::sgn_inv_reducible: - // In many presentations, sign invariance implies order invariance on reducible components. - // If the paper states so, uncomment: - // ret.push_back(polynom_property::ord_inv_reducible); - break; - - case polynom_property::sgn_inv_irreducible: - // If sign invariance implies order invariance for irreducible p, uncomment: - // ret.push_back(polynom_property::ord_inv_irreducible); - break; - - case polynom_property::connected: - // connected(i) might enable sample or representation derivations; leave empty here. - break; - - case polynom_property::an_sub: - // an_sub(i) may enable additional sampling; leave empty here. - break; - - case polynom_property::sample: - // sample(s) is often a leaf for evaluating properties at s. - break; - - case polynom_property::repr: - // repr(I, s) together with others may lead to holds; no generic implication alone. - break; - - case polynom_property::holds: - // Terminal goal, no further implications. - break; - - default: - break; - } - return ret; - } - - // Example driver/stub that will eventually orchestrate Levelwise projection with proof logging. - void lewelwise_project(polynomial_ref_vector & /*ps*/, var /*max_x*/) { - //std::cout << "call\n"; - //exit(0); - // Scaffold example (no-ops for now): - // levelwise_proof pr; - // for (auto* p : ps) { pr.add_axiom(property_inst::of(p, polynom_property::an_del, /*level*/0)); } - // std::cout << pr.dump(); - } -} \ No newline at end of file +} // namespace nlsat diff --git a/src/nlsat/levelwise.h b/src/nlsat/levelwise.h index 29ac9a0e6..3b5c2c90c 100644 --- a/src/nlsat/levelwise.h +++ b/src/nlsat/levelwise.h @@ -1,6 +1,26 @@ #pragma once #include "nlsat_types.h" + namespace nlsat { - void lewelwise_project(polynomial_ref_vector & ps, var max_x); + +class assignment; // forward declared in nlsat_types.h + +// Levelwise driver (PIMPL). Orchestrates property-based projection/proof. +class levelwise { + struct impl; + impl* m_impl; +public: + // Construct with polynomials ps, maximal variable max_x, and current sample s (assignment of vars < max_x) + levelwise(polynomial_ref_vector const& ps, var max_x, assignment const& s); + ~levelwise(); + + levelwise(levelwise const&) = delete; + levelwise& operator=(levelwise const&) = delete; + levelwise(levelwise&&) noexcept; + levelwise& operator=(levelwise&&) noexcept; +}; + +// Convenience free-function driver prototype +void levelwise_project(polynomial_ref_vector const& ps, var max_x, assignment const& s); } // namespace nlsat diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 2f1b900b1..50b0ef665 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1246,7 +1246,7 @@ namespace nlsat { polynomial_ref_vector samples(m_pm); - lewelwise_project(ps, max_x); + levelwise_project(ps, max_x, this->m_assignment); if (x < max_x) cac_add_cell_lits(ps, x, samples);