mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-26 03:48:42 +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 e542a5e520
commit cc56749e84
4 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/nlsat/nlsat_solver.cpp
View file

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