From f89e133d52e8c43c57441a08068e6037a50256d0 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Date: Mon, 28 Apr 2025 16:07:46 -0700
Subject: [PATCH] revert the behavior of add_zero_assumption (#7631)

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/nlsat/nlsat_explain.cpp | 25 -------------------------
 src/nlsat/nlsat_solver.cpp  |  2 +-
 2 files changed, 1 insertion(+), 26 deletions(-)

diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index cda44bdd4..58b185e4c 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -282,8 +282,6 @@ namespace nlsat {
             // then only the factors that are zero in the current interpretation needed to be considered.
             // I don't want to create a nested conjunction in the clause. 
             // Then, I assert p_i1 * ... * p_im  != 0
-            bool is_linear = true;
-            unsigned x = max_var(p);
             {
                 restore_factors _restore(m_factors, m_factors_save);
                 factor(p, m_factors);
@@ -296,33 +294,10 @@ namespace nlsat {
                     if (is_zero(sign(f))) {
                         m_zero_fs.push_back(m_factors.get(i));
                         m_is_even.push_back(false);
-                        is_linear &= m_pm.degree(f, x) <= 1;
                     }
                 }
             }
-
-            if (!is_linear) {
-                scoped_anum_vector& roots = m_roots_tmp;
-                roots.reset();
-                m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots);
-                unsigned num_roots = roots.size();
-                if (num_roots > 0) {
-                    anum const& x_val = m_assignment.value(x);
-                    for (unsigned i = 0; i < num_roots; i++) {
-                        int s = m_am.compare(x_val, roots[i]);
-                        if (s != 0)
-                            continue;
-                        TRACE("nlsat_explain", tout << "adding (zero assumption) root " << "\n");
-                        add_root_literal(atom::ROOT_EQ, x, i + 1, p);
-                        return;
-                    }
-                    display(verbose_stream() << "polynomial ", p);
-                    m_solver.display(verbose_stream());
-                    UNREACHABLE();
-                }
-            }
             SASSERT(!m_zero_fs.empty()); // one of the factors must be zero in the current interpretation, since p is zero in it.
-
             literal l = m_solver.mk_ineq_literal(atom::EQ, m_zero_fs.size(), m_zero_fs.data(), m_is_even.data());
             l.neg();
             TRACE("nlsat_explain", tout << "adding (zero assumption) literal:\n"; display(tout, l); tout << "\n";);
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 98b9d7706..3d496fe45 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -3400,7 +3400,7 @@ namespace nlsat {
             case atom::ROOT_GT: out << "(> "; proc(out, a.x()); out << " " << yn << ")"; break;
             case atom::ROOT_LE: out << "(<= "; proc(out, a.x()); out << " " << yn << ")"; break;
             case atom::ROOT_GE: out << "(>= "; proc(out, a.x()); out << " " << yn << ")"; break;
-            case atom::ROOT_EQ: out << "(= "; proc(out, a.x()); out << " " << yn << ")"; NOT_IMPLEMENTED_YET(); break;
+            case atom::ROOT_EQ: out << "(= "; proc(out, a.x()); out << " " << yn << ")"; break;
             default: UNREACHABLE(); break;
             }
             out << "))";