mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 04:56:03 +00:00
Code Activity

define symbolic_interval

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-13 15:53:22 -07:00
parent 1df11c7e4c
commit 34925acbf3
2 changed files with 59 additions and 77 deletions
Download patch file Download diff file Expand all files Collapse all files

109
src/nlsat/levelwise.cpp
View file

@ -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<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)
: m_P(ps), m_max_x(max_x), m_s(s) {
: m_P(ps), m_n(max_x), m_s(s) {
}
std::vector<property_goal> seed_initial_goals() {
std::vector<property_goal> seed_properties() {
std::vector<property_goal> 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;
}
struct result_struct {
symbolic_interval I;
std::vector<property_goal> Q;
bool status;
};
std::vector<symbolic_interval> single_cell() {
return std::vector<symbolic_interval>();
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<symbolic_interval> single_cell() {
std::vector<symbolic_interval> ret;
std::vector<property_goal> Q = seed_properties();
for (unsigned i = m_n; i >= 1; i--) {
auto result = construct_interval();
if (result.status == false)
return std::vector<symbolic_interval>(); // 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<symbolic_interval> levelwise::single_cell() {
/* struct impl {
polynomial_ref_vector const& m_P;
var m_n;
assignment const& m_sample;
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)
: 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<property_goal> 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<symbolic_interval> single_cell() {
std::vector<symbolic_interval> ret;
std::vector<property_goal> Q = seed_properties();
for (unsigned i = m_n; i >= 1; i--) {
auto result = construct_interval();
if (result.status == false)
return std::vector<symbolic_interval>();
Q
}
}
}; // end of impl structure
*/
std::vector<levelwise::symbolic_interval> levelwise::single_cell() {
return m_impl->single_cell();
}

25
src/nlsat/levelwise.h
View file

@ -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: