mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-02 05:16:08 +00:00
Code Activity

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-01-09 13:29:46 -10:00
parent a75718fe2b
commit ae8763d760
3 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/nlsat/levelwise.cpp
View file

@ -127,7 +127,6 @@ struct levelwise::impl {
chain.reset(); chain.reset();
m_cache.psc_chain(p, d, x, chain); m_cache.psc_chain(p, d, x, chain);
polynomial_ref disc(m_pm); polynomial_ref disc(m_pm);
// Iterate forward: S[0] is the resultant (after reverse in psc_chain)
for (unsigned i = 0; i < chain.size(); ++i) { for (unsigned i = 0; i < chain.size(); ++i) {
disc = polynomial_ref(chain.get(i), m_pm); disc = polynomial_ref(chain.get(i), m_pm);
if (!disc || is_zero(disc)) if (!disc || is_zero(disc))

2
src/nlsat/nlsat_params.pyg
View file

@ -23,6 +23,6 @@ def_module_params('nlsat',
('add_all_coeffs', BOOL, False, "add all polynomial coefficients during projection."), ('add_all_coeffs', BOOL, False, "add all polynomial coefficients during projection."),
('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."), ('lws', BOOL, True, "apply levelwise."),
('canonicalize', BOOL, True, "canonicalize polynomials.") ('canonicalize', BOOL, True, "canonicalize polynomials.")
)) ))

2
src/nlsat/nlsat_solver.cpp
View file

@ -309,7 +309,7 @@ namespace nlsat {
m_check_lemmas = p.check_lemmas(); m_check_lemmas = p.check_lemmas();
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.lws();
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();