mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-01 00:39:52 +00:00
Code Activity

refactor

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-15 11:47:34 -07:00
parent 3cff4d3410
commit 841775ffdd
4 changed files with 9 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/nlsat/levelwise.cpp
View file

@ -52,8 +52,8 @@ namespace nlsat {
// Since m_p_relation holds (lesser -> greater), we invert edges when populating dom: greater ▹ lesser.
std::vector<std::vector<bool>> m_prop_dom;
assignment const& sample() const { return m_solver.get_assignment();}
assignment & sample() { return m_solver.get_assignment(); }
assignment const& sample() const { return m_solver.sample();}
assignment & sample() { return m_solver.sample(); }
// max_x plays the role of n in algorith 1 of the levelwise paper.
impl(solver& solver, polynomial_ref_vector const& ps, var max_x, assignment const& s, pmanager& pm, anum_manager& am)