mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 13:06:05 +00:00
Code Activity

closer to the paper

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-13 12:38:39 -07:00
parent 516a3d5594
commit b15162d7ef
3 changed files with 128 additions and 66 deletions
Download patch file Download diff file Expand all files Collapse all files

105
src/nlsat/levelwise.cpp
View file

@ -1,12 +1,13 @@
#include "nlsat/levelwise.h" #include "nlsat/levelwise.h"
#include "nlsat/nlsat_types.h" #include "nlsat/nlsat_types.h"
#include <vector> #include <vector>
#include <unordered_map>
namespace nlsat { namespace nlsat {
// Local enums reused from previous scaffolding // Local enums reused from previous scaffolding
enum class property_mapping_case : unsigned { case1 = 0, case2 = 1, case3 = 2 }; enum class property_mapping_case : unsigned { case1 = 0, case2 = 1, case3 = 2 };
enum class polynom_property : unsigned { enum class prop : unsigned {
ir_ord, ir_ord,
an_del, an_del,
non_null, non_null,
@ -20,32 +21,33 @@ enum class polynom_property : unsigned {
_count _count
}; };
struct property_goal { struct property_goal {
polynom_property prop; prop prop;
poly* p = nullptr; poly* p = nullptr;
unsigned s_idx = 0; // index into current sample roots on level, if applicable unsigned s_idx = 0; // index into current sample roots on level, if applicable
unsigned level = 0; unsigned level = 0;
}; };
struct levelwise::impl { struct levelwise::impl {
polynomial_ref_vector const& m_ps; polynomial_ref_vector const& m_P;
var m_max_x; var m_max_x;
assignment const& m_sample; assignment const& m_s;
std::vector<property_goal> m_goals; std::vector<property_goal> 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) impl(polynomial_ref_vector const& ps, var max_x, assignment const& s)
: m_ps(ps), m_max_x(max_x), m_sample(s) { : m_P(ps), m_max_x(max_x), m_s(s) {
seed_initial_goals(); seed_initial_goals();
} }
void 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 // 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) { for (unsigned i = 0; i < m_P.size(); ++i) {
poly* p = m_ps.get(i); poly* p = m_P.get(i);
m_goals.push_back(property_goal{ polynom_property::sgn_inv_irreducible /*or reducible later*/, p, /*s_idx*/0, /*level*/0}); m_Q.push_back(property_goal{ prop::sgn_inv_irreducible, p, /*s_idx*/0, /* level */ m_max_x});
} }
} }
}; };
levelwise::levelwise(polynomial_ref_vector const& ps, var max_x, assignment const& s) levelwise::levelwise(polynomial_ref_vector const& ps, var n, assignment const& s)
: m_impl(new impl(ps, max_x, s)) {} : m_impl(new impl(ps, n, s)) {}
levelwise::~levelwise() { delete m_impl; } levelwise::~levelwise() { delete m_impl; }
levelwise::levelwise(levelwise&& o) noexcept : m_impl(o.m_impl) { o.m_impl = nullptr; } levelwise::levelwise(levelwise&& o) noexcept : m_impl(o.m_impl) { o.m_impl = nullptr; }
@ -53,27 +55,88 @@ levelwise::levelwise(levelwise&& o) noexcept : m_impl(o.m_impl) { o.m_impl = nul
levelwise& levelwise::operator=(levelwise&& o) noexcept { if (this != &o) { delete m_impl; m_impl = o.m_impl; o.m_impl = nullptr; } return *this; } 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. // 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) { polynomial_ref_vector levelwise_project(polynomial_ref_vector & ps, var max_x, assignment const& s) {
struct impl { struct impl {
polynomial_ref_vector const& m_ps; polynomial_ref_vector const& m_P;
var m_max_x; var m_max_x;
assignment const& m_sample; assignment const& m_sample;
std::vector<property_goal> m_goals; std::vector<property_goal> 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<size_t>(k.pr);
h ^= (reinterpret_cast<size_t>(k.p) >> 3) + 0x9e3779b97f4a7c15ULL + (h<<6) + (h>>2);
h ^= static_cast<size_t>(k.s_idx) + 0x9e3779b9 + (h<<6) + (h>>2);
h ^= static_cast<size_t>(k.level) + 0x9e3779b9 + (h<<6) + (h>>2);
return h;
}
};
std::unordered_map<key, unsigned, key_hash> m_index; // key -> fact id
std::vector<property_goal> m_facts; // id -> fact
std::vector<unsigned> m_worklist;
impl(polynomial_ref_vector const& ps_, var mx, assignment const& sa) impl(polynomial_ref_vector const& ps_, var mx, assignment const& sa)
: m_ps(ps_), m_max_x(mx), m_sample(sa) { : m_P(ps_), m_max_x(mx), m_sample(sa) {
seed_initial_goals(); seed_initial_goals();
} }
void seed_initial_goals() { void seed_initial_goals() {
for (unsigned i = 0; i < m_ps.size(); ++i) { for (unsigned i = 0; i < m_P.size(); ++i) {
poly* p = m_ps.get(i); poly* p = m_P.get(i);
m_goals.push_back(property_goal{ polynom_property::sgn_inv_irreducible, p, /*s_idx*/0, /*level*/0 }); m_goals.push_back(property_goal{ prop::sgn_inv_irreducible, p, /*s_idx*/0, /*level*/0 });
} }
} }
void run() { unsigned intern(property_goal const& g) {
// TODO: apply Levelwise rules to discharge goals and build a proof. key k{ g.prop, g.p, g.s_idx, g.level };
auto it = m_index.find(k);
if (it != m_index.end())
return it->second;
unsigned id = static_cast<unsigned>(m_facts.size());
m_index.emplace(k, id);
m_facts.push_back(g);
m_worklist.push_back(id);
return id;
} }
} I(ps, max_x, s); bool pop(unsigned& id) {
I.run(); if (m_worklist.empty())
return false;
id = m_worklist.back();
m_worklist.pop_back();
return true;
}
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 });
}
}
// Construct an interval at level n = m_max_x around the current sample s per the levelwise paper.
void 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.
(void)m_P; (void)m_max_x; (void)m_sample;
}
void single_cell() {
construct_interval();
}
}; // end of impl structure
impl m_impl(ps, max_x, s);
m_impl.single_cell();
return ps;
} }
} // namespace nlsat } // namespace nlsat

2
src/nlsat/levelwise.h
View file

@ -21,6 +21,6 @@ public:
}; };
// Convenience free-function driver prototype // Convenience free-function driver prototype
void levelwise_project(polynomial_ref_vector const& ps, var max_x, assignment const& s); polynomial_ref_vector levelwise_project(polynomial_ref_vector& ps, var max_x, assignment const& s);
} // namespace nlsat } // namespace nlsat

3
src/nlsat/nlsat_explain.cpp
View file

@ -1245,8 +1245,7 @@ namespace nlsat {
// Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
polynomial_ref_vector samples(m_pm); polynomial_ref_vector samples(m_pm);
ps = levelwise_project(ps, max_x, this->m_assignment);
levelwise_project(ps, max_x, this->m_assignment);
if (x < max_x) if (x < max_x)
cac_add_cell_lits(ps, x, samples); cac_add_cell_lits(ps, x, samples);