mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-15 21:31:50 +00:00
Code Activity

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-09-27 07:02:45 -08:00
parent ece8a27c29
commit 25ee8b36bd
3 changed files with 96 additions and 66 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/nlsat/levelwise.h
View file

@ -13,19 +13,24 @@ namespace nlsat {
};
struct symbolic_interval {
bool section = false;
poly* l = nullptr;
polynomial_ref l;
unsigned l_index; // the root index
poly* u = nullptr;
polynomial_ref u;
unsigned u_index; // the root index
bool l_inf() const { return l == nullptr; }
bool u_inf() const { return u == nullptr; }
bool is_section() const { return section; }
bool is_sector() const { return !section; }
poly* section_poly() {
polynomial_ref& section_poly() {
SASSERT(is_section());
return l;
}
symbolic_interval(polynomial::manager & pm):l(pm), u(pm) {}
};
// Free pretty-printer declared here so external modules (e.g., nlsat_explain) can
// display intervals without depending on levelwise internals.
// Implemented in levelwise.cpp
friend std::ostream& display(std::ostream& out, solver& s, symbolic_interval const& I);
private:
@ -43,5 +48,7 @@ namespace nlsat {
};
//
// Free pretty-printer (non-member) for levelwise::symbolic_interval
std::ostream& display(std::ostream& out, solver& s, levelwise::symbolic_interval const& I);
} // namespace nlsat