mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-02 21:36:09 +00:00
Code Activity

make normalize optional

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-18 10:02:51 -10:00
parent 84fccbee4a
commit b88b4211d7
4 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/nlsat/levelwise.cpp
View file

@ -508,6 +508,8 @@ namespace nlsat {
} }
void normalize(polynomial_ref & p) { void normalize(polynomial_ref & p) {
if (!m_solver.lws_norm())
return;
unsigned level = max_var(p); unsigned level = max_var(p);
if (find_in_Q(p, level)) return; if (find_in_Q(p, level)) return;
TRACE(lws_norm, tout << "p:" << p << std::endl;); TRACE(lws_norm, tout << "p:" << p << std::endl;);

1
src/nlsat/nlsat_params.pyg
View file

@ -24,5 +24,6 @@ def_module_params('nlsat',
('zero_disc', BOOL, False, "add_zero_assumption to the vanishing discriminant."), ('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"), ('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."),
('lws_norm', BOOL, True, "normalize polynomials in levelwise."),
('canonicalize', BOOL, True, "canonicalize polynomials.") ('canonicalize', BOOL, True, "canonicalize polynomials.")
)) ))

3
src/nlsat/nlsat_solver.cpp
View file

@ -250,6 +250,7 @@ namespace nlsat {
stats m_stats; stats m_stats;
std::string m_debug_known_solution_file_name; std::string m_debug_known_solution_file_name;
bool m_apply_lws; bool m_apply_lws;
bool m_lws_norm;
imp(solver& s, ctx& c): imp(solver& s, ctx& c):
m_ctx(c), m_ctx(c),
m_solver(s), m_solver(s),
@ -310,6 +311,7 @@ namespace nlsat {
m_variable_ordering_strategy = p.variable_ordering_strategy(); m_variable_ordering_strategy = p.variable_ordering_strategy();
m_debug_known_solution_file_name = p.known_sat_assignment_file_name(); m_debug_known_solution_file_name = p.known_sat_assignment_file_name();
m_apply_lws = p.apply_levelwise(); m_apply_lws = p.apply_levelwise();
m_lws_norm = p.lws_norm();
m_check_lemmas |= !(m_debug_known_solution_file_name.empty()); m_check_lemmas |= !(m_debug_known_solution_file_name.empty());
m_cell_sample = p.cell_sample(); m_cell_sample = p.cell_sample();
@ -4661,6 +4663,7 @@ namespace nlsat {
} }
bool solver::apply_levelwise() const { return m_imp->m_apply_lws; } bool solver::apply_levelwise() const { return m_imp->m_apply_lws; }
bool solver::lws_norm() const { return m_imp->m_lws_norm; }
}; };

1
src/nlsat/nlsat_solver.h
View file

@ -248,6 +248,7 @@ namespace nlsat {
const assignment& sample() const; const assignment& sample() const;
assignment& sample(); assignment& sample();
bool apply_levelwise() const; bool apply_levelwise() const;
bool lws_norm() const;
void reset(); void reset();
void collect_statistics(statistics & st); void collect_statistics(statistics & st);
void reset_statistics(); void reset_statistics();