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

pass pmanager

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-14 15:50:02 -07:00
parent 7949e77d1a
commit 62101fef90
3 changed files with 9 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/nlsat/levelwise.cpp
View file

@ -40,6 +40,7 @@ namespace nlsat {
polynomial_ref_vector const& m_P; polynomial_ref_vector const& m_P;
var m_n; var m_n;
assignment const& m_s; assignment const& m_s;
pmanager& m_pm;
anum_manager& m_am; anum_manager& m_am;
std::vector<property> m_Q; // the set of properties to prove as in single_cell std::vector<property> m_Q; // the set of properties to prove as in single_cell
bool m_fail = false; bool m_fail = false;
@ -50,8 +51,8 @@ namespace nlsat {
// Since m_p_relation holds (lesser -> greater), we invert edges when populating dom: greater ▹ lesser. // Since m_p_relation holds (lesser -> greater), we invert edges when populating dom: greater ▹ lesser.
std::vector<std::vector<bool>> m_prop_dom; std::vector<std::vector<bool>> m_prop_dom;
// max_x plays the role of n in algorith 1 of the levelwise paper. // 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, anum_manager& am) impl(polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am)
: m_P(ps), m_n(max_x), m_s(s), m_am(am) { : m_P(ps), m_n(max_x), m_s(s), m_pm(pm), m_am(am) {
init_relation(); init_relation();
} }
@ -176,7 +177,7 @@ namespace nlsat {
::sign sign(poly * p) { ::sign sign(poly * p) {
polynomial_ref pr(p, m_P.m()); polynomial_ref pr(p, m_P.m());
auto s = m_am.eval_sign_at(pr, m_s); auto s = m_am.eval_sign_at(pr, m_s);
TRACE(nlsat_explain, tout << "p: " << p << " var: " << m_P.m().max_var(p) << " sign: " << s << "\n";); TRACE(nlsat_explain, tout << "p: " << p << " var: " << m_pm.max_var(p) << " sign: " << s << "\n";);
return s; return s;
} }
result_struct construct_interval() { result_struct construct_interval() {
@ -232,8 +233,8 @@ namespace nlsat {
} }
}; };
// constructor // constructor
levelwise::levelwise(polynomial_ref_vector const& ps, var n, assignment const& s, anum_manager& am) levelwise::levelwise(polynomial_ref_vector const& ps, var n, assignment const& s, pmanager& pm, anum_manager& am)
: m_impl(new impl(ps, n, s, am)) {} : m_impl(new impl(ps, n, s, pm, am)) {}
levelwise::~levelwise() { delete m_impl; } levelwise::~levelwise() { delete m_impl; }

4
src/nlsat/levelwise.h
View file

@ -33,8 +33,8 @@ namespace nlsat {
struct impl; struct impl;
impl* m_impl; impl* m_impl;
public: public:
// Construct with polynomials ps, maximal variable max_x, current sample s, and algebraic-number manager am // Construct with polynomials ps, maximal variable max_x, current sample s, polynomial manager pm, and algebraic-number manager am
levelwise(polynomial_ref_vector const& ps, var max_x, assignment const& s, anum_manager& am); levelwise(polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am);
~levelwise(); ~levelwise();
levelwise(levelwise const&) = delete; levelwise(levelwise const&) = delete;

2
src/nlsat/nlsat_explain.cpp
View file

@ -1245,7 +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);
levelwise lws(ps, max_x, m_assignment, m_am); levelwise lws(ps, max_x, m_assignment, m_pm, m_am);
auto cell = lws.single_cell(); auto cell = lws.single_cell();
if (x < max_x) if (x < max_x)
cac_add_cell_lits(ps, x, samples); cac_add_cell_lits(ps, x, samples);