mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-09 18:40:51 +00:00
Code Activity

fixing factoring and hitting NOT_IMPLEMENTED on ir_ord

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-08 14:12:28 -07:00
parent f673fbf34d
commit 3cb6ed6227
5 changed files with 50 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/nlsat/nlsat_explain.cpp
View file

@ -194,16 +194,6 @@ namespace nlsat {
}
/**
\brief Wrapper for factorization
*/
void factor(polynomial_ref & p, polynomial_ref_vector & fs) {
// TODO: add params, caching
TRACE(nlsat_factor, tout << "factor\n" << p << "\n";);
fs.reset();
m_cache.factor(p.get(), fs);
}
/**
\brief Wrapper for psc chain computation
*/
@ -682,7 +672,7 @@ namespace nlsat {
return;
if (m_factor) {
restore_factors _restore(m_factors, m_factors_save);
factor(p, m_factors);
factor(p, m_cache, m_factors);
TRACE(nlsat_explain, display(tout << "adding factors of\n", m_solver, p); tout << "\n" << m_factors << "\n";);
polynomial_ref f(m_pm);
for (unsigned i = 0; i < m_factors.size(); ++i) {
@ -742,7 +732,7 @@ namespace nlsat {
// this function also explains the value 0, if met
bool coeffs_are_zeroes(polynomial_ref &s) {
restore_factors _restore(m_factors, m_factors_save);
factor(s, m_factors);
factor(s, m_cache, m_factors);
unsigned num_factors = m_factors.size();
m_zero_fs.reset();
m_is_even.reset();
@ -1109,8 +1099,8 @@ namespace nlsat {
}
}
bool levelwise_single_cell(polynomial_ref_vector & ps, var max_x) {
levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am);
bool levelwise_single_cell(polynomial_ref_vector & ps, var max_x, polynomial::cache & cache) {
levelwise lws(m_solver, ps, max_x, sample(), m_pm, m_am, cache);
auto cell = lws.single_cell();
if (lws.failed()) {
return false;
@ -1164,7 +1154,7 @@ namespace nlsat {
var x = m_todo.extract_max_polys(ps);
TRACE(nlsat_explain, tout << "m_solver.apply_levelwise():" << m_solver.apply_levelwise() << "\n";);
if (m_solver.apply_levelwise() && levelwise_single_cell(ps, max_x))
if (m_solver.apply_levelwise() && levelwise_single_cell(ps, max_x, m_cache))
return;
polynomial_ref_vector samples(m_pm);