From e4cbe980e979e050caf82a642b2d03e512208ca7 Mon Sep 17 00:00:00 2001
From: Lev <levnach@hotmail.com>
Date: Wed, 21 Nov 2018 11:20:14 -0800
Subject: [PATCH] limit the number of tactics in qfnia

Signed-off-by: Lev <levnach@hotmail.com>
---
 src/tactic/smtlogics/qfnia_tactic.cpp |  4 +--
 src/util/lp/nla_solver.cpp            | 52 ++++++++++++++++++++++-----
 2 files changed, 46 insertions(+), 10 deletions(-)

diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp
index 1a22914f6..dc4af610f 100644
--- a/src/tactic/smtlogics/qfnia_tactic.cpp
+++ b/src/tactic/smtlogics/qfnia_tactic.cpp
@@ -119,10 +119,10 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
     return and_then(
         mk_report_verbose_tactic("(qfnia-tactic)", 10),
         mk_qfnia_preamble(m, p),
-                
         or_else(mk_qfnia_sat_solver(m, p),
                 try_for(mk_qfnia_smt_solver(m, p), 2000),
                 mk_qfnia_nlsat_solver(m, p),
                 mk_qfnia_smt_solver(m, p))
-        );
+        )
+        ;
 }
diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index ccef959f2..eb4f301c9 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -901,15 +901,52 @@ struct solver::imp {
         m_lemma->clear();
     }
 
+    static svector<lpvar> extract_all_but(const svector<lpvar> & vars, unsigned k) {
+        static svector<lpvar> ret;
+        for (unsigned j = 0; j < vars.size(); j++) {
+            if (j == k)
+                continue;
+            ret.push_back(vars[j]);
+        }
+        return ret;
+    }
+
     // a > b && c == d => ac > bd
     // ac is a factorization of m_monomials[i_mon]
     // ac[k] plays the role of c
     // d = +-c
+    // i_bd_equiv is a candidate for bd
+    bool order_lemma_on_factor_equiv_and_other_mon_eq(unsigned b,
+                                                      unsigned i_bd_equiv,
+                                                      unsigned i_bd,
+                                                      unsigned d, unsigned i_ac, const factorization& ac, unsigned k) {
+    }
+        
 
-    bool order_lemma_on_factor_equiv_and_other_mon_factor(unsigned i_f,
-                                                   unsigned o_i_mon, unsigned e_j, unsigned i_mon, const factorization& f, unsigned k) {
-        TRACE("nla_solver", tout << "i_f = "; print_monomial_with_vars(i_f, tout); );
-        NOT_IMPLEMENTED_YET();
+    // a > b && c == d => ac > bd
+    // ac is a factorization of m_monomials[i_mon]
+    // ac[k] plays the role of c
+    // d = +-c
+    // i_bd_equiv is a candidate for bd
+    bool order_lemma_on_factor_equiv_and_other_mon_eq(unsigned i_bd_equiv,
+                                                     unsigned i_bd,
+                                                     unsigned d, unsigned i_ac, const factorization& ac, unsigned k) {
+        TRACE("nla_solver", tout << "i_bd_equiv = "; print_monomial_with_vars(i_bd_equiv, tout); );
+        rational abs_d = abs(vvr(d));
+        for (unsigned k = 0; k < m_monomials[i_bd_equiv].size(); k++) {
+            if (abs(vvr(m_monomials[i_bd_equiv][k])) != abs_d)
+                continue;
+            svector<lpvar> b = extract_all_but(m_monomials[i_bd_equiv].vars(), k);
+            std::sort(b.begin(), b.end());
+            auto it = m_rooted_monomials_map.find(b);
+            if (it == m_rooted_monomials_map.end())
+                return false;
+            
+            for (const index_with_sign& s : it->second) {
+                if (order_lemma_on_factor_equiv_and_other_mon_eq_b(s.var(), i_bd, d, i_bd, d, i_ac, ac, k))
+                    return true;
+            }
+        }
         return false;
     }    
 
@@ -922,16 +959,15 @@ struct solver::imp {
         if (i_bd == i_ac) {
             return false;
         }
-        TRACE("nla_solver", );
+
         const monomial & m_bd = m_monomials[i_bd];
         monomial_coeff m_bd_rooted = canonize_monomial(m_bd);
         TRACE("nla_solver", tout << "i_bd monomial = "; print_monomial(m_bd, tout); );
-        TRACE("nla_solver", );
         auto it = m_rooted_monomials_map.find(m_bd_rooted.vars());
         if (it == m_rooted_monomials_map.end())
             return false;
-        for (const index_with_sign& i_s : it->second) {
-            if (order_lemma_on_factor_equiv_and_other_mon_factor(i_s.var(), i_bd, d, i_ac, ac, k))
+        for (const index_with_sign& s : it->second) {
+            if (order_lemma_on_factor_equiv_and_other_mon_eq(s.var(), i_bd, d, i_ac, ac, k))
                 return true;
         }
         return false;