fix unsoundness bug

Signed-off-by: Nikolaj Bjorner <[email protected]>
Z3Prover · May 1, 2024 · 04c55c3 · 04c55c3
1 parent 869643a
commit 04c55c3
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 4 deletions.
diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp
@@ -6317,6 +6317,27 @@ namespace polynomial {
             return R.mk();
         }        
 
+        // x*q = p
+        // 
+        // md = degree of x in p
+        // P = m0 + ...
+        // m0 = x^dm*m1
+        // m1 * p^dm * q^{md - dm}  
+        // P' = m1 + ...
+        // property would be that x*q = p => P > 0 <=> P' > 0
+        // requires that q > 0
+        // Reasoning:
+        //    P > 0 
+        // <=> { since q > 0 }
+        //    q^md * P > 0
+        // <=>
+        //    q^md*x^dm*m0 + .. > 0
+        // <=>
+        //    q^{md-dm}*(xq)^dm*m0 + ... > 0
+        // <=>
+        //    q^{md-dm}*p^dm + .. > 0
+        // <=>
+        //    P' > 0
         void substitute(polynomial const* r, var x, polynomial const* p, polynomial const* q, polynomial_ref& result) {
             unsigned md = degree(r, x);
             if (md == 0) {

diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
@@ -2742,10 +2742,8 @@ namespace nlsat {
 
                 while (elim_uncnstr())
                     ;
-
                 while (fm())
                     ;
-
                 if (!solve_eqs())
                     return false;
 
@@ -3017,6 +3015,8 @@ namespace nlsat {
             if (apply_fm_equality(x, clauses, lo, hi))
                 return true;
 
+            return false;
+
             if (!all_solved)
                 return false;
 
@@ -3104,6 +3104,13 @@ namespace nlsat {
             a1 = m_asm.mk_join(a1, a2);
             m_lemma_assumptions = a1;
 
+            polynomial_ref A(l.A), B(l.B);
+
+            if (m_pm.is_neg(l.A)) {
+                A = -A;
+                B = -B;
+            }
+
             // TODO: this can also replace solve_eqs
             for (auto c : clauses) {
                 if (c->is_removed())
@@ -3114,7 +3121,7 @@ namespace nlsat {
                 m_lemma.reset();
                 bool is_tautology = false;
                 for (literal lit : *c) {
-                    lit = substitute_var(x, l.A, l.B, lit);
+                    lit = substitute_var(x, A, B, lit);
                     m_lemma.push_back(lit);
                     if (lit == true_literal)
                         is_tautology = true;
@@ -3126,7 +3133,7 @@ namespace nlsat {
 
                 IF_VERBOSE(3,
                     if (cls) {
-                        verbose_stream() << "x" << x << " * " << l.A << " = " << l.B << "\n";
+                        m_display_var(verbose_stream(), x) << " * " << l.A << " = " << l.B << "\n";
                         display(verbose_stream(), *c) << " -> ";
                         display(verbose_stream(), *cls) << "\n";
                     });