new file

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

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";
+        );
+    }
+}