mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-18 18:28:33 +00:00
Code Activity

canonicalize polynomials in nlsat

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-10 07:56:29 -10:00
parent 3004222f15
commit 1cb0743e2b
6 changed files with 14 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/nlsat/levelwise.cpp
View file

@ -184,7 +184,7 @@ namespace nlsat {
// 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, polynomial::cache & cache)
: m_solver(solver), m_P(ps), m_n(max_x), m_pm(pm), m_am(am), m_cache(cache), m_todo_set(cache) {
: m_solver(solver), m_P(ps), m_n(max_x), m_pm(pm), m_am(am), m_cache(cache), m_todo_set(cache, true) {
TRACE(lws, tout << "m_n:" << m_n << "\n";);
m_I.reserve(m_n); // cannot just resize bcs of the absence of the default constructor of root_function_interval
for (unsigned i = 0; i < m_n; ++i)

2
src/nlsat/nlsat_common.h
View file

@ -29,7 +29,7 @@ namespace nlsat {
svector<char> m_in_set;
bool m_canonicalize;
todo_set(polynomial::cache& u, bool canonicalize = false);
todo_set(polynomial::cache& u, bool canonicalize);
void reset();
void insert(poly* p);

14
src/nlsat/nlsat_explain.cpp
View file

@ -50,7 +50,7 @@ namespace nlsat {
bool m_factor;
bool m_add_all_coeffs;
bool m_add_zero_disc;
bool m_cell_sample;
bool m_sample_cell_project;
assignment const & sample() const { return m_solver.sample(); }
assignment & sample() { return m_solver.sample(); }
@ -69,7 +69,7 @@ namespace nlsat {
evaluator & m_evaluator;
imp(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq,
evaluator & ev, bool is_sample):
evaluator & ev, bool sample_cell_project, bool canonicalize):
m_solver(s),
m_atoms(atoms),
m_x2eq(x2eq),
@ -82,8 +82,8 @@ namespace nlsat {
m_factors(m_pm),
m_factors_save(m_pm),
m_roots_tmp(m_am),
m_cell_sample(is_sample),
m_todo(u),
m_sample_cell_project(sample_cell_project),
m_todo(u, canonicalize),
m_core1(s),
m_core2(s),
m_evaluator(ev) {
@ -1109,7 +1109,7 @@ namespace nlsat {
}
void project(polynomial_ref_vector & ps, var max_x) {
if (m_cell_sample) {
if (m_sample_cell_project) {
project_cdcac(ps, max_x);
}
else {
@ -1791,8 +1791,8 @@ namespace nlsat {
};
explain::explain(solver & s, assignment const & x2v, polynomial::cache & u,
atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool use_cell_sample) {
m_imp = alloc(imp, s, x2v, u, atoms, x2eq, ev, use_cell_sample);
atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool use_cell_sample, bool canonicalize) {
m_imp = alloc(imp, s, x2v, u, atoms, x2eq, ev, use_cell_sample, canonicalize);
}
explain::~explain() {

2
src/nlsat/nlsat_explain.h
View file

@ -35,7 +35,7 @@ namespace nlsat {
imp * m_imp;
public:
explain(solver & s, assignment const & x2v, polynomial::cache & u,
atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool use_cell_sample_proj);
atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev, bool use_cell_sample_proj, bool canonicalize);
~explain();

3
src/nlsat/nlsat_params.pyg
View file

@ -23,5 +23,6 @@ def_module_params('nlsat',
('add_all_coeffs', BOOL, False, "add all polynomial coefficients during projection."),
('zero_disc', BOOL, False, "add_zero_assumption to the vanishing discriminant."),
('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only"),
('apply_levelwise', BOOL, True, "apply levelwise.")
('apply_levelwise', BOOL, True, "apply levelwise."),
('canonicalize', BOOL, True, "canonicalize polynomials.")
))

3
src/nlsat/nlsat_solver.cpp
View file

@ -266,7 +266,7 @@ namespace nlsat {
m_simplify(s, m_atoms, m_clauses, m_learned, m_pm),
m_display_var(m_perm),
m_display_assumption(nullptr),
m_explain(s, m_assignment, m_cache, m_atoms, m_var2eq, m_evaluator, nlsat_params(c.m_params).cell_sample()),
m_explain(s, m_assignment, m_cache, m_atoms, m_var2eq, m_evaluator, nlsat_params(c.m_params).cell_sample(), nlsat_params(c.m_params).canonicalize()),
m_scope_lvl(0),
m_lemma(s),
m_lazy_clause(s),
@ -4635,5 +4635,6 @@ namespace nlsat {
}
bool solver::apply_levelwise() const { return m_imp->m_apply_lws; }
};