From 0ba8940ae7e99328237c442cab32ea80e4428c28 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 30 Jul 2019 12:01:41 -0700
Subject: [PATCH] more efficient code in has_common_factor

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/cross_nested.h | 21 ++++++++++++++-------
 src/math/lp/horner.h       |  1 -
 2 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index 4b281efdc..127bbd164 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -81,9 +81,16 @@ public:
     static bool has_common_factor(const nex& c) {
         TRACE("nla_cn", tout << "c=" << c << "\n";);
         SASSERT(c.is_sum());
-        unsigned size = c.children().size();
-        for(const auto & p : get_mult_occurences(c)) {
-            if (p.second.m_occs == size) {
+        auto & ch = c.children();
+        auto common_vars = get_vars_of_expr(ch[0]);
+        for (lpvar j : common_vars) {
+            bool divides_the_rest = true;
+            for(unsigned i = 1; i < ch.size() && divides_the_rest; i++) {
+                if (!ch[i].contains(j))
+                    divides_the_rest = false;
+            }
+            if (divides_the_rest) {
+                TRACE("nla_cn_common_factor", tout << c << "\n";);
                 return true;
             }
         }
@@ -341,13 +348,14 @@ public:
           to explore only such variables to create all cross-nested forms.
         */
         
-        if (has_common_factor(a))
+        if (has_common_factor(a)) {
             return false;
+        }
         update_front_with_split(e, j, front, a, b);
         return true;
     }
-    std::set<lpvar> get_vars_of_expr(const nex &e ) const {
-        std::set<lpvar> r;
+    static std::unordered_set<lpvar> get_vars_of_expr(const nex &e ) {
+        std::unordered_set<lpvar> r;
         switch (e.type()) {
         case expr_type::SCALAR:
             return r;
@@ -367,7 +375,6 @@ public:
             SASSERT(false);
             return r;
         }
-
     }
 
 };
diff --git a/src/math/lp/horner.h b/src/math/lp/horner.h
index a08852956..48aa3080f 100644
--- a/src/math/lp/horner.h
+++ b/src/math/lp/horner.h
@@ -45,7 +45,6 @@ public:
     intervals::interval interval_of_mul(const nex&);
     void set_interval_for_scalar(intervals::interval&, const rational&);
     void set_var_interval(lpvar j, intervals::interval&);
-    std::set<lpvar> get_vars_of_expr(const nex &) const;
     bool lemmas_on_expr(nex &);
 }; // end of horner
 }