From 60dde9f3d53c2bdbc03e380939ba3b84ce87716e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 24 Oct 2019 10:32:56 -0700
Subject: [PATCH] unit test for #2650

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/nlsat/nlsat_explain.cpp | 17 +++++-----
 src/test/nlsat.cpp          | 63 +++++++++++++++++++++++++++++++++++++
 2 files changed, 72 insertions(+), 8 deletions(-)

diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 97a789f0321..3ed62cb81ae 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -707,15 +707,14 @@ namespace nlsat {
             m_result = nullptr;
         }
 
+        
         void add_root_literal(atom::kind k, var y, unsigned i, poly * p) {
             polynomial_ref pr(p, m_pm);
             TRACE("nlsat_explain", 
                   display(tout << "x" << y << " " << k << "[" << i << "](", pr); tout << ")\n";);
-
+            
             if (!mk_linear_root(k, y, i, p) &&
-                //!mk_plinear_root(k, y, i, p) &&
-                !mk_quadratic_root(k, y, i, p)&&
-                true) {                
+                !mk_quadratic_root(k, y, i, p)) {
                 bool_var b = m_solver.mk_root_atom(k, y, i, p);
                 literal l(b, true);
                 TRACE("nlsat_explain", tout << "adding literal\n"; display(tout, l); tout << "\n";);
@@ -726,7 +725,7 @@ namespace nlsat {
         /**
          * literal can be expressed using a linear ineq_atom
          */
-        bool mk_linear_root(atom::kind k, var y, unsigned i, poly * p) {
+        bool mk_linear_root(atom::kind k, var y, unsigned i, poly * p) {            
             scoped_mpz c(m_pm.m());
             if (m_pm.degree(p, y) == 1 && m_pm.const_coeff(p, y, 1, c)) {
                 SASSERT(!m_pm.m().is_zero(c));
@@ -949,11 +948,9 @@ namespace nlsat {
             }
 
             if (!lower_inf) {
-                TRACE("nlsat_explain", tout << "lower_inf: " << lower_inf << " upper_inf: " << upper_inf << " " << p_lower << "\n";);            
                 add_root_literal(m_full_dimensional ? atom::ROOT_GE : atom::ROOT_GT, y, i_lower, p_lower);
             }
             if (!upper_inf) {
-                TRACE("nlsat_explain", tout << "lower_inf: " << lower_inf << " upper_inf: " << upper_inf << " " << p_upper << "\n";);            
                 add_root_literal(m_full_dimensional ? atom::ROOT_LE : atom::ROOT_LT, y, i_upper, p_upper);
             }
         }
@@ -1475,7 +1472,11 @@ namespace nlsat {
         void operator()(unsigned num, literal const * ls, scoped_literal_vector & result) {
             SASSERT(check_already_added());
             SASSERT(num > 0);
-            TRACE("nlsat_explain", tout << "[explain] set of literals is infeasible in the current interpretation\n"; display(tout, num, ls) << "\n";);
+            TRACE("nlsat_explain", 
+                  tout << "[explain] set of literals is infeasible in the current interpretation\n"; 
+                  display(tout, num, ls) << "\n";
+                  m_assignment.display(tout);
+                  );
             m_result = &result;
             process(num, ls);
             reset_already_added();
diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp
index 9e3971bb2e0..cba351b743e 100644
--- a/src/test/nlsat.cpp
+++ b/src/test/nlsat.cpp
@@ -315,6 +315,20 @@ static void project(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned
     std::cout << "\n";
 }
 
+static void project_fa(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned num, nlsat::literal const* lits) {
+    std::cout << "Project ";
+    nlsat::scoped_literal_vector result(s);
+    ex(num, lits, result);
+    std::cout << "(or";
+    for (auto l : result) {
+        s.display(std::cout << " ", l);
+    }
+    for (unsigned i = 0; i < num; ++i) {
+        s.display(std::cout << " ", ~lits[i]);
+    }
+    std::cout << ")\n";
+}
+
 static nlsat::literal mk_gt(nlsat::solver& s, nlsat::poly* p) {
     nlsat::poly * _p[1] = { p };
     bool is_even[1] = { false };
@@ -695,7 +709,56 @@ static void tst10() {
     std::cout << "\n";
 }
 
+static void tst11() {
+    params_ref      ps;
+    reslimit        rlim;
+    nlsat::solver s(rlim, ps, false);
+    anum_manager & am     = s.am();
+    nlsat::pmanager & pm  = s.pm();
+    nlsat::assignment as(am);
+    nlsat::explain& ex    = s.get_explain();
+    nlsat::var x, y, z;
+    y = s.mk_var(false);
+    z = s.mk_var(false);
+    x = s.mk_var(false);
+    polynomial_ref p1(pm), p2(pm), _x(pm), _y(pm), _z(pm);
+    _x = pm.mk_polynomial(x);
+    _y = pm.mk_polynomial(y);
+    _z = pm.mk_polynomial(z);
+
+    nlsat::scoped_literal_vector lits(s);
+    scoped_anum zero(am), one(am), five(am);
+    am.set(zero, 0);
+    am.set(one, 1);
+    am.set(five, 5);
+    as.set(z, zero);
+    as.set(y, five);
+    as.set(x, five);
+    s.set_rvalues(as);
+
+
+    p1 = (_x - _y);
+    p2 = ((_x*_x) - (_x*_y) - _z);
+    lits.reset();
+    lits.push_back(mk_gt(s, p1));
+    lits.push_back(mk_eq(s, p2));
+    project_fa(s, ex, x, 2, lits.c_ptr());
+    return;
+    
+    p1 = (_x - _y);
+    p2 = ((_x*_x) - (_x*_y));
+    lits.reset();
+    lits.push_back(mk_gt(s, p1));
+    lits.push_back(mk_eq(s, p2));
+    project_fa(s, ex, x, 2, lits.c_ptr());
+
+
+}
+
 void tst_nlsat() {
+    tst11();
+    std::cout << "------------------\n";
+    return;
     tst10();
     std::cout << "------------------\n";
     tst9();