add factoring

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/rewriter/arith_rewriter.cpp

@@ -515,6 +515,103 @@ br_status arith_rewriter::reduce_power(expr * arg1, expr * arg2, op_kind kind, e
     }
 }
 
+bool arith_rewriter::is_factor(expr* s, expr* t) {
+    if (m_util.is_mul(t))
+        return any_of(*to_app(t), [&](expr* m) { return m == s; });
+    if (m_util.is_add(t))
+        return all_of(*to_app(t), [&](expr* f) { return is_factor(s, f); });
+    return s == t;
+}
+
+expr_ref arith_rewriter::remove_factor(expr* s, expr* t) {
+
+    if (m_util.is_mul(t)) {
+        ptr_buffer<expr> r;
+        r.append(to_app(t)->get_num_args(), to_app(t)->get_args());
+        for (unsigned i = 0; i < r.size(); ++i) {
+            expr* arg = r[i];
+            if (s == arg) {
+                r[i] = r.back();
+                r.pop_back();
+                break;
+            }
+        }
+        SASSERT(to_app(t)->get_num_args() == r.size() + 1);
+        switch (r.size()) {
+        case 0:
+            return expr_ref(m_util.mk_numeral(rational(1), m_util.is_int(t)), m);
+        case 1:
+            return expr_ref(r[0], m);
+        default:
+            return expr_ref(m_util.mk_mul(r.size(), r.data()), m);
+        }
+    }
+    if (m_util.is_add(t)) {
+        expr_ref_vector sum(m);
+        for (expr* arg : *to_app(t))
+            sum.push_back(remove_factor(s, arg));
+        return expr_ref(m_util.mk_add(sum.size(), sum.data()), m);
+    }
+    SASSERT(s == t);
+    return expr_ref(m_util.mk_numeral(rational(1), m_util.is_int(t)), m);            
+}
+
+
+br_status arith_rewriter::factor_le_ge_eq(expr * arg1, expr * arg2, op_kind kind, expr_ref & result) {
+    auto is_nl_mul = [&](expr* t) {
+        if (!m_util.is_mul(t))
+            return false;
+        if (to_app(t)->get_num_args() <= 1)
+            return false;
+        unsigned num_vars = 0;
+        for (expr* arg : *to_app(t))
+            if (!m_util.is_numeral(arg))
+                ++num_vars;
+        return num_vars > 1;
+    };
+    auto find_nl_factor = [&](expr* s) -> expr* {
+        if (is_nl_mul(s)) {
+            for (expr* arg : *to_app(s))
+                if (!m_util.is_numeral(arg) && is_factor(arg, s))
+                    return arg;
+            return nullptr;
+        }
+        if (m_util.is_add(s)) {
+            for (expr* arg : *to_app(s)) {
+                if (is_nl_mul(arg)) {
+                    for (expr* arg1 : *to_app(arg))
+                        if (!m_util.is_numeral(arg1) && is_factor(arg1, s))
+                            return arg1;
+                    return nullptr;
+                }
+            }
+        }
+        return nullptr;
+    };
+
+    if (is_zero(arg2)) {
+        expr* f = find_nl_factor(arg1);
+        if (!f)
+            return BR_FAILED;
+        expr_ref f2 = remove_factor(f, arg1);
+        expr* z = m_util.mk_numeral(rational(0), m_util.is_int(arg1));
+        switch (kind) {
+        case EQ: 
+            result = m.mk_or(m_util.mk_eq(f, z), m_util.mk_eq(f2, z));
+            break;
+        case GE:
+            result = m.mk_iff(m_util.mk_ge(f, z), m_util.mk_ge(f2, z));
+            break;
+        case LE:
+            result = m.mk_xor(m_util.mk_ge(f, z), m_util.mk_ge(f2, z));
+            break;
+
+        }
+        return BR_REWRITE2;                    
+    }
+    return BR_FAILED;
+}
+
 br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kind, expr_ref & result) {
     expr *orig_arg1 = arg1, *orig_arg2 = arg2;
     expr_ref new_arg1(m);
@@ -528,6 +625,9 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
         arg1 = new_arg1;
         arg2 = new_arg2;
     }
+    st = factor_le_ge_eq(arg1, arg2, kind, result);
+    if (st != BR_FAILED) 
+        return st;
     expr_ref new_new_arg1(m);
     expr_ref new_new_arg2(m);
     if (m_elim_to_real && elim_to_real(arg1, arg2, new_new_arg1, new_new_arg2)) {

src/ast/rewriter/arith_rewriter.h

@@ -73,6 +73,9 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
     br_status is_separated(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);
     bool is_non_negative(expr* e);
     br_status mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);
+    bool is_factor(expr* s, expr* t);
+    expr_ref remove_factor(expr* s, expr* t);
+    br_status factor_le_ge_eq(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);
 
     bool elim_to_real_var(expr * var, expr_ref & new_var);
     bool elim_to_real_mon(expr * monomial, expr_ref & new_monomial);

src/ast/sls/sls_arith_base.cpp

@@ -537,7 +537,6 @@ namespace sls {
     bool arith_base<num_t>::repair(sat::literal lit) {
 
         //verbose_stream() << "repair " << lit << " " << (ctx.is_unit(lit)?"unit":"") << "\n";
-        //flet<bool> _tabu(m_use_tabu, m_use_tabu && lit != m_last_literal);
         m_last_literal = lit;
         find_moves(lit);
         static unsigned num_fail = 0;
@@ -546,7 +545,7 @@ namespace sls {
             return true;
 
 
-        flet<bool> _tabu(m_use_tabu, false);
+//        flet<bool> _tabu(m_use_tabu, false);
         find_reset_moves(lit);
 
         if (apply_update()) 
@@ -559,6 +558,7 @@ namespace sls {
             ctx.force_restart();
             num_fail = 0;
         }
+        m_stats.m_num_steps++;
         return false;
     }