mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

enable always add all coeffs in nlsat

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-24 17:47:16 -07:00 • committed by Nikolaj Bjorner
parent 7b095ca733
commit e980f92a9e
4 changed files with 11 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/nlsat/nlsat_explain.cpp
View file

@ -44,6 +44,7 @@ namespace nlsat {
bool m_full_dimensional; bool m_full_dimensional;
bool m_minimize_cores; bool m_minimize_cores;
bool m_factor; bool m_factor;
bool m_add_all_coeffs;
bool m_signed_project; bool m_signed_project;
bool m_cell_sample; bool m_cell_sample;
@ -154,6 +155,7 @@ namespace nlsat {
m_simplify_cores = false; m_simplify_cores = false;
m_full_dimensional = false; m_full_dimensional = false;
m_minimize_cores = false; m_minimize_cores = false;
m_add_all_coeffs = true;
m_signed_project = false; m_signed_project = false;
} }
@ -622,6 +624,8 @@ namespace nlsat {
//"An improved projection operation for cylindrical algebraic decomposition of three-dimensional space", by McCallum, Scott //"An improved projection operation for cylindrical algebraic decomposition of three-dimensional space", by McCallum, Scott
bool is_square_free(polynomial_ref_vector &ps, var x) { bool is_square_free(polynomial_ref_vector &ps, var x) {
if (m_add_all_coeffs)
return false;
polynomial_ref p(m_pm); polynomial_ref p(m_pm);
polynomial_ref lc_poly(m_pm); polynomial_ref lc_poly(m_pm);
polynomial_ref disc_poly(m_pm); polynomial_ref disc_poly(m_pm);
@ -2135,6 +2139,10 @@ namespace nlsat {
m_imp->m_factor = f; m_imp->m_factor = f;
} }
void explain::set_add_all_coeffs(bool f) {
m_imp->m_add_all_coeffs = f;
}
void explain::set_signed_project(bool f) { void explain::set_signed_project(bool f) {
m_imp->m_signed_project = f; m_imp->m_signed_project = f;
} }
@ -2185,4 +2193,3 @@ void pp_lit(nlsat::explain::imp & ex, nlsat::literal l) {
std::cout << std::endl; std::cout << std::endl;
} }
#endif #endif

2
src/nlsat/nlsat_explain.h
View file

@ -44,6 +44,7 @@ namespace nlsat {
void set_full_dimensional(bool f); void set_full_dimensional(bool f);
void set_minimize_cores(bool f); void set_minimize_cores(bool f);
void set_factor(bool f); void set_factor(bool f);
void set_add_all_coeffs(bool f);
void set_signed_project(bool f); void set_signed_project(bool f);
/** /**
@ -109,4 +110,3 @@ namespace nlsat {
}; };
}; };

1
src/nlsat/nlsat_params.pyg
View file

@ -19,5 +19,6 @@ def_module_params('nlsat',
('inline_vars', BOOL, False, "inline variables that can be isolated from equations (not supported in incremental mode)"), ('inline_vars', BOOL, False, "inline variables that can be isolated from equations (not supported in incremental mode)"),
('seed', UINT, 0, "random seed."), ('seed', UINT, 0, "random seed."),
('factor', BOOL, True, "factor polynomials produced during conflict resolution."), ('factor', BOOL, True, "factor polynomials produced during conflict resolution."),
('add_all_coeffs', BOOL, False, "add all polynomial coefficients during projection."),
('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")
)) ))

1
src/nlsat/nlsat_solver.cpp
View file

@ -306,6 +306,7 @@ namespace nlsat {
m_explain.set_simplify_cores(m_simplify_cores); m_explain.set_simplify_cores(m_simplify_cores);
m_explain.set_minimize_cores(min_cores); m_explain.set_minimize_cores(min_cores);
m_explain.set_factor(p.factor()); m_explain.set_factor(p.factor());
m_explain.set_add_all_coeffs(p.add_all_coeffs());
m_am.updt_params(p.p); m_am.updt_params(p.p);
} }