enable always add all coeffs in nlsat

Signed-off-by: Lev Nachmanson <[email protected]>

Author: levnach

src/nlsat/nlsat_explain.cpp

@@ -44,6 +44,7 @@ namespace nlsat {
         bool                    m_full_dimensional;
         bool                    m_minimize_cores;
         bool                    m_factor;
+        bool                    m_add_all_coeffs;
         bool                    m_signed_project;
         bool                    m_cell_sample;
 
@@ -154,6 +155,7 @@ namespace nlsat {
             m_simplify_cores   = false;
             m_full_dimensional = false;
             m_minimize_cores   = false;
+            m_add_all_coeffs   = true;
             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
 
         bool is_square_free(polynomial_ref_vector &ps, var x) {
+            if (m_add_all_coeffs)
+                return false;
             polynomial_ref p(m_pm);
             polynomial_ref lc_poly(m_pm);
             polynomial_ref disc_poly(m_pm); 
@@ -2135,6 +2139,10 @@ namespace nlsat {
         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) {
         m_imp->m_signed_project = f;
     }
@@ -2185,4 +2193,3 @@ void pp_lit(nlsat::explain::imp & ex, nlsat::literal l) {
     std::cout << std::endl;
 }
 #endif
-

src/nlsat/nlsat_explain.h

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

src/nlsat/nlsat_params.pyg

@@ -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)"),
                           ('seed', UINT, 0, "random seed."),
                           ('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")
                           ))         

src/nlsat/nlsat_solver.cpp

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