From d235829b3dd9226830c2e3be1f49c1679b6721cd Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 9 Oct 2025 17:38:11 -0700 Subject: [PATCH] new file Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_common.cpp | 55 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 src/nlsat/nlsat_common.cpp diff --git a/src/nlsat/nlsat_common.cpp b/src/nlsat/nlsat_common.cpp new file mode 100644 index 000000000..136d1bd68 --- /dev/null +++ b/src/nlsat/nlsat_common.cpp @@ -0,0 +1,55 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + nlsat_common.cpp + +Abstract: + + some common routines from nlsat + +Author: + + Lev Nachmanson(levnach@hotmail.com) 2025-October. + +Revision History: + +--*/ +#include "nlsat/nlsat_common.h" +namespace nlsat { + /** + \brief Wrapper for factorization + */ + void factor(polynomial_ref & p, polynomial::cache& cache, polynomial_ref_vector & fs) { + TRACE(nlsat_factor, tout << "factor\n" << p << "\n";); + fs.reset(); + // Use a todo list to iteratively factor polynomials until every + // polynomial in fs is irreducible (cache.factor returns a single factor). + // Start with the input polynomial on the queue. + polynomial_ref_vector todo(fs.m()); + todo.push_back(p.get()); + for (unsigned idx = 0; idx < todo.size(); ++idx) { + polynomial_ref_vector tmp(fs.m()); + polynomial_ref cur_ref(todo.get(idx), fs.m()); + cache.factor(cur_ref.get(), tmp); + if (tmp.size() == 1) { + // single factor -> consider it irreducible and add to output + fs.push_back(tmp.get(0)); + } + else { + // Only multivariate factors are queued for further factoring. + // Univariate factors are considered final and pushed directly to the output vector `fs`. + for (unsigned i = 0; i < tmp.size(); ++i) { + if (polynomial::manager::is_univariate(tmp.get(i))) + fs.push_back(tmp.get(i)); + else + todo.push_back(tmp.get(i)); + } + } + } + TRACE(nlsat_factor, tout << fs.size() << " factors:\n"; + ::nlsat::display(tout, fs.m(), fs, polynomial::display_var_proc()) << "\n"; + ); + } +}