experiments with arith

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

src/ast/rewriter/bit_blaster/bit_blaster_tpl.h

@@ -37,6 +37,7 @@ protected:
     unsigned long long m_max_memory;
     void checkpoint();
 
+
 public:
     bit_blaster_tpl(Cfg const & cfg = Cfg(), unsigned long long max_memory = UINT64_MAX):
         Cfg(cfg),
@@ -119,6 +120,8 @@ public:
     void mk_carry_save_adder(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr * const * c_bits, expr_ref_vector & sum_bits, expr_ref_vector & carry_bits);
     bool mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
     void mk_const_case_multiplier(bool is_a, unsigned i, unsigned sz, ptr_buffer<expr, 128>& a_bits, ptr_buffer<expr, 128>& b_bits, expr_ref_vector & out_bits);
+    void mk_const_case1_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
+    void mk_generic_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits);
 
     bool is_bool_const(expr* e) const { return m().is_true(e) || m().is_false(e); }
     void mk_abs(unsigned sz, expr * const * a_bits, expr_ref_vector & out_bits);

src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h

@@ -183,24 +183,29 @@ void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, exp
     SASSERT(sz > 0);
     numeral n_a, n_b;
     out_bits.reset();
-    if (is_numeral(sz, a_bits, n_b))
+    if (is_numeral(sz, b_bits, n_b))
         std::swap(a_bits, b_bits);
-    if (is_minus_one(sz, b_bits)) {
-        mk_neg(sz, a_bits, out_bits);
+    if (is_minus_one(sz, a_bits)) {
+        mk_neg(sz, b_bits, out_bits);
         SASSERT(sz == out_bits.size());
-        return;
     }
-    if (is_numeral(sz, a_bits, n_a)) {
+    else if (is_numeral(sz, b_bits, n_a)) {
         n_a *= n_b;
         num2bits(n_a, sz, out_bits);
         SASSERT(sz == out_bits.size());
-        return;
     }
-   
-    if (mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) {
+    else if (is_numeral(sz, a_bits, n_a)) 
+        mk_const_case1_multiplier(sz, a_bits, b_bits, out_bits);
+    else if (mk_const_case_multiplier(sz, a_bits, b_bits, out_bits)) {
         SASSERT(sz == out_bits.size());
-        return;
     }
+    else 
+        mk_generic_multiplier(sz, a_bits, b_bits, out_bits);
+}
+
+template<typename Cfg>
+void bit_blaster_tpl<Cfg>::mk_generic_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
+
     out_bits.reset();
 #if 0
     static unsigned counter = 0;
@@ -268,7 +273,6 @@ void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, exp
             out_bits.push_back(out);
         }
     }
-
 }
 
 
@@ -1113,6 +1117,124 @@ void bit_blaster_tpl<Cfg>::mk_carry_save_adder(unsigned sz, expr * const * a_bit
     }
 }
 
+template<typename Cfg>
+void bit_blaster_tpl<Cfg>::mk_const_case1_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
+    DEBUG_CODE(for (unsigned i = 0; i < sz; ++i) VERIFY(is_bool_const(a_bits[i])););
+    
+    unsigned num_ones = 0;        
+    for (unsigned i = 0; i < sz; ++i)
+        if (m().is_true(a_bits[i]))
+            ++num_ones;
+
+
+    // for each run-length of ones, add contribution to out_bits.
+    // 
+    // c = 2^i + 2^{i+1} + ... + 2^k
+    // x * c 
+    //
+    // i = k
+    // x * 2^i
+    //
+    // i > 0, k < sz - 1
+    // x * (2^i + 2^{i+1} + ... + 2^k)
+    // x * (2^(k+1) - 2^{i})
+    // 4 + 8 + 16 = 32 - 4 = 30
+
+    // i = 0, k < sz - 1
+    // x * 2^(k+1) - 1
+
+    // i = 0, k = sz - 1
+    // -x
+
+    // i > 0, k = sz - 1
+    // x*2^{sz} - 1 - x*2^{i} + 1
+    // = -x - x*2^i + 1 
+    // 8 + 16 + 32 =
+    // 64 - 1 - 8 + 1
+
+    SASSERT(out_bits.empty());
+    for (unsigned i = 0; i < sz; ++i)
+        out_bits.push_back(m().mk_false());
+    expr_ref cout(m());
+
+    auto mul2_i = [&](unsigned i, ptr_buffer<expr, 128>& sbits) {
+        for (unsigned j = 0; j < sz; ++j)
+            if (j < i)
+                sbits.push_back(m().mk_false());
+            else
+                sbits.push_back(b_bits[j-i]);
+    };
+    
+    for (unsigned i = 0; i < sz; ++i) {
+        if (!m().is_true(a_bits[i]))
+            continue;
+
+        ptr_buffer<expr, 128> one, sbits;
+        expr_ref_vector out_bits1(m());
+
+        unsigned k = 0;
+        for (k = i + 1; k < sz && m().is_true(a_bits[k]); ++k);
+        --k;
+
+        if (i == 0 && k == 0) {
+            for (unsigned i = 0; i < sz; ++i)
+                out_bits[i] = b_bits[i];            
+        }
+        else if (i == 0 && k == sz - 1) {
+            out_bits.reset();
+            mk_neg(sz, b_bits, out_bits);
+        }
+        else if (i == 0) {
+            SASSERT(k < sz - 1);
+            // shift by k+1, subtract x
+            out_bits.reset();
+
+            mul2_i(k + 1, sbits);
+            mk_adder(sz, out_bits.data(), sbits.data(), out_bits1);
+            out_bits.reset();
+            out_bits.append(out_bits1);
+            out_bits1.reset();
+            
+            // subtract x
+            mk_subtracter(sz, out_bits.data(), b_bits, out_bits1, cout);
+            out_bits.reset();
+            out_bits.append(out_bits1);
+            out_bits1.reset();
+        }
+        else if (i == k) {
+            mul2_i(i, sbits);
+            mk_adder(sz, out_bits.data(), sbits.data(), out_bits1);
+            out_bits.reset();
+            out_bits.append(out_bits1);
+            out_bits1.reset();
+        }
+        else if (k == sz - 1) {
+            // 2^sz - 2^i = - 2^i
+            // -= x*2^i
+            mul2_i(i, sbits);
+            mk_subtracter(sz, out_bits.data(), sbits.data(), out_bits1, cout);
+            out_bits.reset();
+            out_bits.append(out_bits1);
+        }
+        else {
+            SASSERT(0 < i && i < k && k < sz - 1);                       
+            // += x*2^{k+1} - x*2^i           
+            mul2_i(i, ibits);
+            mul2_i(k + 1, kbits);
+            mk_adder(sz, kbits.data(), out_bits.data(), out_bits1);
+            out_bits.reset();
+            out_bits.append(out_bits1);
+            out_bits1.reset();
+            mk_subtracter(sz, out_bits.data(), ibits.data(), out_bits1, cout);
+            out_bits.reset();
+            out_bits.append(out_bits1);
+            out_bits1.reset(); 
+        }
+        i = k;
+    }
+}
+
+
 template<typename Cfg>
 bool bit_blaster_tpl<Cfg>::mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) {
     unsigned case_size = 1;
@@ -1133,10 +1255,11 @@ bool bit_blaster_tpl<Cfg>::mk_const_case_multiplier(unsigned sz, expr * const *
     na_bits.append(sz, a_bits);
     ptr_buffer<expr, 128> nb_bits;
     nb_bits.append(sz, b_bits);
-    mk_const_case_multiplier(true, 0, sz, na_bits, nb_bits, out_bits); 
+    mk_const_case_multiplier(true, 0, sz, na_bits, nb_bits, out_bits);
     return true;
 }
- 
+
+
 template<typename Cfg>
 void bit_blaster_tpl<Cfg>::mk_const_case_multiplier(bool is_a, unsigned i, unsigned sz, ptr_buffer<expr, 128>& a_bits, ptr_buffer<expr, 128>& b_bits, expr_ref_vector & out_bits) {
     while (is_a && i < sz && is_bool_const(a_bits[i])) ++i;

src/math/lp/int_solver.cpp

@@ -35,6 +35,152 @@ namespace lp {
         }
     }
 
+
+    unsigned int_solver::patcher::count_non_int() {
+        unsigned non_int = 0;
+        for (auto j : lra.r_basis()) 
+            if (lra.column_is_int(j) && !lra.column_value_is_int(j))
+                ++non_int;
+        return non_int;
+    }
+
+    lia_move int_solver::patcher::patch_basic_columns() {
+        remove_fixed_vars_from_base();
+        lia.settings().stats().m_patches++;
+        lp_assert(lia.is_feasible());
+
+        //unsigned non_int_before = count_non_int();
+        unsigned num = lra.A_r().column_count();
+        for (unsigned j : lra.r_basis()) 
+            if (!lra.get_value(j).is_int())
+                patch_basic_column(j);
+        //unsigned non_int_after = count_non_int();
+        // verbose_stream() << non_int_before << " -> " << non_int_after << "\n";
+        if (!lia.has_inf_int()) {
+            lia.settings().stats().m_patches_success++;
+            return lia_move::sat;
+        }
+        return lia_move::undef;
+    }
+
+    /***
+     * v + r + a*j = 0
+     * val(v) is rational
+     * a is rational
+     * val(j) is integer
+     * find min delta > 0 such that frac(a*delta) = frac(val(v)) 
+     * then r + a*(j - delta) is an integer
+     * find min delta > 0 such that frac(a*-delta) = frac(val(v))
+     * then r + a*(j + delta) is an integer
+     * 
+     * Note: frac(a*delta) = frac(frac(a)*delta)
+     * Let x1/x2 = frac(val(v))
+     * let a1/a2 = frac(a)
+     *
+     * x1/x2 = frac(a1*delta/a2)
+     * requires that a2 | x2, otherwise not possible.
+     * 
+     * x2 = a2, 0 < x1 < a2 
+     *  -> x1 = a1*delta mod a2
+     *  -> x1 = a1*delta + a2*gamma
+     * let g, x, y = extended_gcd(a1, a2)
+     * a1*x + a2*y = g
+     * if g does not divide x1 then no solution.
+     * therefore assume g | x1
+     * Set delta = x*x1/g
+     * 
+     * Initial experiment: use bare bones case x1/x2 = a1/a2, x1/x2 = 1 - a1/a2
+     */
+
+    bool int_solver::patcher::patch_basic_column(unsigned v, row_cell<mpq> const& c) {
+        if (v == c.var())
+            return false;
+        if (!lra.column_is_int(c.var())) // could use real to patch integer
+            return false;
+        if (c.coeff().is_int())
+            return false;
+        mpq a = fractional_part(c.coeff());
+        mpq r = fractional_part(lra.get_value(v));
+        SASSERT(0 < a && a < 1);
+        SASSERT(0 < r && r < 1);
+        if (!divides(denominator(a), denominator(r)))
+            return false;
+        // stronger filter for now:
+        if (denominator(a) != denominator(r))
+            return false;
+        if (a == r) {
+            if (try_patch_column(c.var(), mpq(a.is_pos() ? 1 : -1)))
+                return true;
+        }
+        if (a == 1 - r) {
+            if (try_patch_column(c.var(), mpq(a.is_pos() ? -1 : 1)))
+                return true;
+        }
+        rational x, y;
+        rational g = gcd(numerator(a), denominator(a), x, y);
+        // g = numerator(a)*x + denominator(a)*y
+        x = abs(x);
+        if (divides(g, numerator(r))) {
+            auto xs = a.is_pos() ? x : -x;
+            if (try_patch_column(c.var(), xs*(numerator(r)/g)))
+                return true;
+        }
+        if (divides(g, numerator(1 - r))) {
+            auto xs = a.is_pos() ? -x : x;
+            if (try_patch_column(c.var(), xs*(numerator(r)/g)))
+                return true;
+        }
+        return false;
+    }
+
+    bool int_solver::patcher::try_patch_column(unsigned j, mpq const& delta) {
+        const auto & A = lra.A_r();
+        unsigned make_count = 0, break_count = 0;
+        if (delta < 0) {
+            if (lia.has_lower(j) && lia.get_value(j) + impq(delta) < lra.get_lower_bound(j))
+                return false;
+        }
+        else {
+            if (lia.has_upper(j) && lia.get_value(j) + impq(delta) > lra.get_upper_bound(j))
+                return false;
+        }
+        for (auto const& c : A.column(j)) {
+            unsigned row_index = c.var();
+            unsigned i = lrac.m_r_basis[row_index];
+            auto old_val = lia.get_value(i);
+            auto new_val = old_val - impq(c.coeff()*delta);
+            if (lia.has_lower(i) && new_val < lra.get_lower_bound(i))
+                return false;
+            if (lia.has_upper(i) && new_val > lra.get_upper_bound(i))
+                return false;
+            if (old_val.is_int() && !new_val.is_int())
+                break_count++;
+            else if (!old_val.is_int() && new_val.is_int())
+                make_count++;
+        }
+        if (make_count > break_count) {
+#if 0
+            for (auto const& c : A.column(j)) {
+                unsigned row_index = c.var();
+                unsigned i = lrac.m_r_basis[row_index];
+                verbose_stream() << "basis " << i << "\n";
+            }
+            verbose_stream() << j << " delta " << delta << " make " << make_count << " break " << break_count << "\n";
+            lra.display(verbose_stream());
+#endif
+            lra.set_value_for_nbasic_column(j, lia.get_value(j) + impq(delta));
+            return true;
+        }
+        return false;
+    }
+    
+    void int_solver::patcher::patch_basic_column(unsigned v) {
+        SASSERT(!lia.is_fixed(v));
+        for (auto const& c : lra.basic2row(v))
+            if (patch_basic_column(v, c))
+                return;                                       
+    }
+
     lia_move int_solver::patcher::patch_nbasic_columns() {
         remove_fixed_vars_from_base();
         lia.settings().stats().m_patches++;
@@ -43,6 +189,8 @@ namespace lp {
         m_patch_fail = 0;
         m_num_ones = 0;
         m_num_divides = 0;
+        //unsigned non_int_before = count_non_int();
+
         unsigned num = lra.A_r().column_count();
         for (unsigned v = 0; v < num; v++) {
             if (lia.is_base(v))
@@ -55,9 +203,12 @@ namespace lp {
                 ++num_fixed;
             
         lp_assert(lia.is_feasible());
-        verbose_stream() << "patch " << m_patch_success << " fails " << m_patch_fail << " ones " << m_num_ones << " divides " << m_num_divides << " num fixed " << num_fixed << "\n";
+        //verbose_stream() << "patch " << m_patch_success << " fails " << m_patch_fail << " ones " << m_num_ones << " divides " << m_num_divides << " num fixed " << num_fixed << "\n";
         //lra.display(verbose_stream());
         //exit(0);
+        //unsigned non_int_after = count_non_int();
+
+        // verbose_stream() << non_int_before << " -> " << non_int_after << "\n";
         if (!lia.has_inf_int()) {
             lia.settings().stats().m_patches_success++;
             return lia_move::sat;
@@ -76,19 +227,30 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
     bool m_is_one = m.is_one();
     bool val_is_int = lia.value_is_int(j);
 
-
-
+    const auto & A = lra.A_r();
     // check whether value of j is already a multiple of m.
     if (val_is_int && (m_is_one || (val.x / m).is_int())) {
         if (m_is_one)
             ++m_num_ones;
         else
             ++m_num_divides;
+#if 0
+        for (auto c : A.column(j)) {
+            unsigned row_index = c.var();
+            unsigned i = lrac.m_r_basis[row_index];
+            if (!lia.get_value(i).is_int() ||
+                (lia.has_lower(i) && lia.get_value(i) < lra.get_lower_bound(i)) ||
+                (lia.has_upper(i) && lia.get_value(i) > lra.get_upper_bound(i))) {
+                verbose_stream() << "skip " << j << " " << m << ": ";
+                lia.display_row(verbose_stream(), A.m_rows[row_index]);
+                verbose_stream() << "\n";                    
+            }
+        }
+#endif
         return;
     }
 
 #if 0
-    const auto & A = lra.A_r();
     if (!m_is_one) {
         // lia.display_column(verbose_stream(), j);
         for (auto c : A.column(j)) {
@@ -120,12 +282,19 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
 
 #if 0
     verbose_stream() << "TARGET v" << j << " -> [";
-    if (inf_l) verbose_stream() << "-oo"; else verbose_stream() << ceil(l.x);
+    if (inf_l) verbose_stream() << "-oo"; else verbose_stream() << ceil(l.x) << " " << l << "\n";
     verbose_stream() << ", ";
-    if (inf_u) verbose_stream() << "oo"; else verbose_stream() << floor(u.x);
+    if (inf_u) verbose_stream() << "oo"; else verbose_stream() << floor(u.x) << " " << u << "\n";
     verbose_stream() << "]";
     verbose_stream() << ", m: " << m << ", val: " << val << ", is_int: " << lra.column_is_int(j) << "\n";
 #endif
+
+#if 0
+    if (!inf_l)
+        l = impq(ceil(l));
+    if (!inf_u)
+        u = impq(floor(u));
+#endif
     
     if (!inf_l) {
         l = impq(m_is_one ? ceil(l) : m * ceil(l / m));
@@ -134,10 +303,23 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
             lra.set_value_for_nbasic_column(j, l);
         }
         else {
-            verbose_stream() << "fail: " << j << " " << m << "\n";
-            --m_patch_success;
+            //verbose_stream() << "fail: " << j << " " << m << "\n";
             ++m_patch_fail;
             TRACE("patch_int", tout << "not patching " << l << "\n";);
+#if 0
+            verbose_stream() << "not patched\n";
+            for (auto c : A.column(j)) {
+                unsigned row_index = c.var();
+                unsigned i = lrac.m_r_basis[row_index];
+                if (!lia.get_value(i).is_int() ||
+                    (lia.has_lower(i) && lia.get_value(i) < lra.get_lower_bound(i)) ||
+                    (lia.has_upper(i) && lia.get_value(i) > lra.get_upper_bound(i))) {
+                    lia.display_row(verbose_stream(), A.m_rows[row_index]);
+                    verbose_stream() << "\n";                    
+                }
+            }
+#endif
+            return;
         }
     }
     else if (!inf_u) {
@@ -150,6 +332,20 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
         TRACE("patch_int", tout << "patching with 0\n";);
     }
     ++m_patch_success;
+#if 0
+    verbose_stream() << "patched " << j << "\n";
+    for (auto c : A.column(j)) {
+        unsigned row_index = c.var();
+        unsigned i = lrac.m_r_basis[row_index];
+        if (!lia.get_value(i).is_int() ||
+            (lia.has_lower(i) && lia.get_value(i) < lra.get_lower_bound(i)) ||
+            (lia.has_upper(i) && lia.get_value(i) > lra.get_upper_bound(i))) {
+            lia.display_row(verbose_stream(), A.m_rows[row_index]);
+            verbose_stream() << "\n";                    
+        }
+    }
+#endif
+    
 }
 
 int_solver::int_solver(lar_solver& lar_slv) :
@@ -398,10 +594,9 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
         unsigned i = lrac.m_r_basis[row_index];
         impq const & xi = get_value(i);
         lp_assert(lrac.m_r_solver.column_is_feasible(i));
-        if (column_is_int(i) && !a.is_int())
+        if (column_is_int(i) && !a.is_int() && xi.is_int()) 
             m = lcm(m, denominator(a));
-
-
+        
         if (!inf_l && !inf_u) {
             if (l == u) 
                 continue;            
@@ -409,15 +604,15 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
 
         if (a.is_neg()) {
             if (has_lower(i)) 
-                set_lower(l, inf_l, delta(a, xi, lrac.m_r_lower_bounds()[i]));
+                set_lower(l, inf_l, delta(a, xi, lra.get_lower_bound(i)));
             if (has_upper(i)) 
-                set_upper(u, inf_u, delta(a, xi, lrac.m_r_upper_bounds()[i]));
+                set_upper(u, inf_u, delta(a, xi, lra.get_upper_bound(i)));
         }
         else {
             if (has_upper(i)) 
-                set_lower(l, inf_l, delta(a, xi, lrac.m_r_upper_bounds()[i]));
+                set_lower(l, inf_l, delta(a, xi, lra.get_upper_bound(i)));
             if (has_lower(i)) 
-                set_upper(u, inf_u, delta(a, xi, lrac.m_r_lower_bounds()[i]));
+                set_upper(u, inf_u, delta(a, xi, lra.get_lower_bound(i)));
         }
     }
 
@@ -575,7 +770,8 @@ bool int_solver::shift_var(unsigned j, unsigned range) {
     bool inf_l = false, inf_u = false;
     impq l, u;
     mpq m;
-    VERIFY(get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m) || settings().get_cancel_flag());
+    if (!get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m))
+        return false;
     if (settings().get_cancel_flag())
         return false;
     const impq & x = get_value(j);

src/math/lp/int_solver.h

@@ -51,11 +51,16 @@ class int_solver {
     public:
         patcher(int_solver& lia);
         bool should_apply() const { return true; }
-        lia_move operator()() { return patch_nbasic_columns(); }
+        lia_move operator()() { return patch_basic_columns(); }
         void patch_nbasic_column(unsigned j);
+        bool patch_basic_column(unsigned v, row_cell<mpq> const& c);
+        void patch_basic_column(unsigned j);
+        bool try_patch_column(unsigned j, mpq const& delta);
+        unsigned count_non_int();
     private:
         void remove_fixed_vars_from_base();
         lia_move patch_nbasic_columns();
+        lia_move patch_basic_columns();
     };
 
     lar_solver&         lra;

src/math/lp/nla_core.cpp

@@ -1373,7 +1373,7 @@ void core::patch_monomial(lpvar j) {
     // handle perfect squares
     if ((*m_patched_monic).vars().size() == 2 && (*m_patched_monic).vars()[0] == (*m_patched_monic).vars()[1]) {        
         rational root;
-        if (v.is_perfect_square(root)) {
+        if (v.get_num_bits() <= 1024 && v.is_perfect_square(root)) {
             m_patched_var = (*m_patched_monic).vars()[0];
             if (!var_breaks_correct_monic(m_patched_var) && (try_to_patch(root) || try_to_patch(-root))) { 
                 TRACE("nla_solver", tout << "patched square\n";);
@@ -1420,11 +1420,12 @@ void core::patch_monomials_on_to_refine() {
 }
 
 void core::patch_monomials() {
-    m_cautious_patching = true;
-    patch_monomials_on_to_refine();
     if (m_to_refine.size() == 0 || !m_nla_settings.expensive_patching) {
         return;
     }
+    m_cautious_patching = true;
+    patch_monomials_on_to_refine();
+
     NOT_IMPLEMENTED_YET();
     m_cautious_patching = false; 
     patch_monomials_on_to_refine();

src/math/lp/numeric_pair.h

@@ -269,12 +269,12 @@ numeric_pair<T> operator*(const numeric_pair<T> & r, const X & a) {
     return numeric_pair<T>(a * r.x, a * r.y);
 }
 
-
 template <typename T, typename X>
 numeric_pair<T> operator/(const numeric_pair<T> & r, const X & a) {
     return numeric_pair<T>(r.x / a,  r.y / a);
 }
 
+
 template <typename T> double get_double(const lp::numeric_pair<T> & ) { /* UNREACHABLE(); */ return 0;}
 template <typename T>
 class numeric_traits<lp::numeric_pair<T>> {

src/params/tactic_params.pyg

@@ -10,6 +10,7 @@ def_module_params('tactic',
                           ('blast_term_ite.max_steps', UINT, UINT_MAX, "maximal number of steps allowed for tactic."),
                           ('propagate_values.max_rounds', UINT, 4, "maximal number of rounds to propagate values."),
                           ('default_tactic', SYMBOL, '', "overwrite default tactic in strategic solver"),
+			  ('local_ctx', BOOL, True, "enable local context simplifier in default tactic pre-amble"),
 
                      #     ('aig.per_assertion', BOOL, True, "process one assertion at a time"),
                      #     ('add_bounds.lower, INT, -2, "lower bound to be added to unbounded variables."),

src/smt/smt_context_pp.cpp

@@ -166,7 +166,7 @@ namespace smt {
         unsigned num = get_num_bool_vars();
         for (unsigned v = 0; v < num; v++) {
             expr * n = m_bool_var2expr[v];
-            ast_def_ll_pp(out << v << " ", m, n, get_pp_visited(), true, false);
+            out << "b" << v << " := #" << n->get_id() << "\n";
         }
     }
 

src/smt/theory_arith_aux.h

@@ -582,12 +582,14 @@ namespace smt {
                         // If the row contains non integer coefficients, then v may be assigned
                         // to a non-integer value even if all non-base variables are integer.
                         // So, v should not be "eliminated"
-                        break; 
+                        break;
+                    verbose_stream() << "eliminate " << v << "\n";
                     eliminate<false>(v, m_eager_gcd);
                     break;
                 case NON_BASE: {
                     col_entry const * entry = get_row_for_eliminating(v);
                     if (entry) {
+                        verbose_stream() << "moving " << v << "\n";
                         TRACE("move_unconstrained_to_base", tout << "moving v" << v << " to the base\n";);
                         row & r = m_rows[entry->m_row_id];
                         SASSERT(r[entry->m_row_idx].m_var == v);
@@ -2144,7 +2146,7 @@ namespace smt {
         if (candidates.empty())
             return;
 
-        verbose_stream() << "candidates " << candidates.size() << "\n";
+        // verbose_stream() << "candidates " << candidates.size() << "\n";
         m_tmp_var_set.reset();
         m_tmp_var_set2.reset();
         for (theory_var v : candidates) {

src/smt/theory_arith_core.h

@@ -1466,6 +1466,7 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::restart_eh() {
+        return;
         m_arith_eq_adapter.restart_eh();
     }
 
@@ -1556,6 +1557,11 @@ namespace smt {
 
     template<typename Ext>
     final_check_status theory_arith<Ext>::final_check_eh() {
+ 
+        // verbose_stream() << "final " << ctx.get_scope_level() << " " << ctx.assigned_literals().size() << "\n";
+        //     ctx.display(verbose_stream());
+        // exit(0);
+               
         TRACE("arith_eq_adapter_info", m_arith_eq_adapter.display_already_processed(tout););
         TRACE("arith", display(tout););
 

src/smt/theory_arith_int.h

@@ -958,7 +958,7 @@ namespace smt {
             }
             if (!inf_l && !inf_u && l > u) {
                 ++num_not_patched;
-                verbose_stream() << "fail: " << v << " " << m << "\n";
+                // verbose_stream() << "fail: " << v << " " << m << "\n";
                 continue; // cannot patch
             }
             ++num_patched;
@@ -968,9 +968,20 @@ namespace smt {
                 set_value(v, u);
             else 
                 set_value(v, inf_numeral(0));
+
+#if 0
+            verbose_stream() << "Patch " << v << "\n";
+            for (auto const& ce : m_columns[v]) {
+                if (ce.is_dead())
+                    continue;
+                row const & r = m_rows[ce.m_row_id];
+                theory_var s = r.get_base_var();
+                display_row(verbose_stream() << s << " " << get_value(s) << " ", r, true);
+            }
+#endif       
         }
         SASSERT(m_to_patch.empty());
-        verbose_stream() << "patched " << num_patched << " not patched " << num_not_patched << " ones " << num_one << " divides " << num_divides << " fixed " << num_fixed << "\n";
+        // verbose_stream() << "patched " << num_patched << " not patched " << num_not_patched << " ones " << num_one << " divides " << num_divides << " fixed " << num_fixed << "\n";
         //display(verbose_stream());
         //exit(0);
     }

src/smt/theory_lra.cpp

@@ -458,9 +458,19 @@ class theory_lra::imp {
         if (!ctx().relevancy())
             mk_idiv_mod_axioms(n->get_arg(0), n->get_arg(1));
         return s;
-
     }
 
+    theory_var internalize_div(app * n) {
+        rational r(1);
+        theory_var s      = mk_binary_op(n);
+        if (!a.is_numeral(n->get_arg(1), r) || r.is_zero())
+            found_underspecified(n);
+        if (!ctx().relevancy())
+            mk_div_axiom(n->get_arg(0), n->get_arg(1));
+        return s;
+    }
+
+
     theory_var mk_binary_op(app * n) {
         SASSERT(n->get_num_args() == 2);
         if (ctx().e_internalized(n))
@@ -499,24 +509,23 @@ class theory_lra::imp {
             return internalize_mod(n);
         else if (a.is_idiv(n))
             return internalize_mod(n);
+        else if (a.is_div(n))
+            return internalize_div(n);
+        else if (a.get_family_id() == n->get_family_id()) {
+            if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n))
+                found_unsupported(n);
+            if (ctx().e_internalized(n))
+                return mk_var(n);
+            for (expr* arg : *n)
+                ctx().internalize(arg, false);
+            mk_enode(n);
+            return mk_var(n);
+        }
         else if (a.is_arith_expr(n)) {
             verbose_stream() << "nyi " << mk_pp(n, m) << "\n";
             NOT_IMPLEMENTED_YET();
         }
 #if 0
-
-        else if (a.is_div(n))
-            return internalize_div(n);
-        else if (a.is_rem(n))
-            return internalize_rem(n);
-        else if (a.is_to_real(n))
-            return internalize_to_real(n);
-        else if (a.is_to_int(n))
-            return internalize_to_int(n);
-
-        else if (a.is_sub(n))
-            return internalize_sub(n);
-        if (a.is_power(n)) {
             // unsupported
             found_unsupported_op(n);
             return mk_binary_op(n);
@@ -527,14 +536,6 @@ class theory_lra::imp {
             enode* e = mk_enode(n);
             return mk_var(e);
         }
-        if (a.get_family_id() == n->get_family_id()) {
-            if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n))
-                found_unsupported_op(n);
-            if (ctx().e_internalized(n))
-                return expr2var(n);
-            for (expr* arg : *n)
-                ctx().internalize(arg, false);
-            return mk_var(mk_enode(n));
     }
 
 #endif
@@ -1097,7 +1098,6 @@ class theory_lra::imp {
                     return v;
                 }
                 if (!st.offset().is_zero()) {
-                    verbose_stream() << "Offset row " << st.offset() << "\n";
                     m_left_side.push_back({ st.offset(), get_one(a.is_int(term)) });
                 }
                 
@@ -1255,13 +1255,21 @@ public:
     }
         
     void internalize_eq_eh(app * atom, bool_var) {
+        return;
+        if (!ctx().get_fparams().m_arith_eager_eq_axioms)
+            return;
         expr* lhs = nullptr, *rhs = nullptr;
         VERIFY(m.is_eq(atom, lhs, rhs));
         enode * n1 = get_enode(lhs);
         enode * n2 = get_enode(rhs);
-        TRACE("arith_verbose", tout << mk_pp(atom, m) << " " << is_arith(n1) << " " << is_arith(n2) << "\n";);
-        if (is_arith(n1) && is_arith(n2) && n1 != n2) 
+        if (is_arith(n1) && is_arith(n2) &&
+            n1->get_th_var(get_id()) != null_theory_var &&
+            n2->get_th_var(get_id()) != null_theory_var && n1 != n2) {
+            verbose_stream() << "ineq\n";
             m_arith_eq_adapter.mk_axioms(n1, n2);
+        }
+        else
+            verbose_stream() << "skip\n";
     }
 
     void assign_eh(bool_var v, bool is_true) {
@@ -1353,6 +1361,7 @@ public:
     }
 
     void restart_eh() {
+        return;
         m_arith_eq_adapter.restart_eh();
     }
 
@@ -1778,7 +1787,7 @@ public:
                       tout << "v" << v << " ";
               tout << "\n"; );
         if (!vars.empty()) {
-            verbose_stream() << "random update " << vars.size() << "\n";
+            // verbose_stream() << "random update " << vars.size() << "\n";
             lp().random_update(vars.size(), vars.data());
             m_changed_assignment = true;
         }
@@ -1933,6 +1942,11 @@ public:
     bool m_changed_assignment = false;
 
     final_check_status final_check_eh() {
+
+        verbose_stream() << "final " << ctx().get_scope_level() << " " << ctx().assigned_literals().size() << "\n";
+        //ctx().display(verbose_stream());
+        //exit(0);
+        
         TRACE("arith_eq_adapter_info", m_arith_eq_adapter.display_already_processed(tout););
         TRACE("arith", display(tout););
 
@@ -2525,6 +2539,7 @@ public:
             m_bv_to_propagate.reset();
             return true;
         }
+        
 
         lbool lbl = make_feasible();
         if (!m.inc())
@@ -2629,9 +2644,7 @@ public:
                 continue;
             TRACE("arith", tout << lit << " bound: " << *b << " first: " << first << "\n";);
             ctx().display_literal_verbose(verbose_stream() << "miss ", lit) << "\n";
-            display(verbose_stream());
             TRACE("arith", ctx().display_literal_verbose(tout << "miss ", lit) << "\n");
-            exit(0);
             
             ++count;
         }
@@ -3562,6 +3575,7 @@ public:
         TRACE("arith", tout << "status treated as inconclusive: " << status << "\n";);
             // TENTATIVE_UNBOUNDED, UNBOUNDED, TENTATIVE_DUAL_UNBOUNDED, DUAL_UNBOUNDED, 
             // TIME_EXAUSTED, EMPTY, UNSTABLE
+        
         return l_undef;
     }
  

src/tactic/smtlogics/qflia_tactic.cpp

@@ -34,6 +34,7 @@ Notes:
 #include "sat/tactic/sat_tactic.h"
 #include "ast/simplifiers/bound_manager.h"
 #include "tactic/arith/probe_arith.h"
+#include "params/tactic_params.hpp"
 
 struct quasi_pb_probe : public probe {
     result operator()(goal const & g) override {
@@ -181,6 +182,7 @@ static tactic * mk_bounded_tactic(ast_manager & m) {
 tactic * mk_preamble_tactic(ast_manager& m) {
 
     params_ref pull_ite_p;
+    tactic_params tp;
     pull_ite_p.set_bool("pull_cheap_ite", true);
     pull_ite_p.set_bool("push_ite_arith", false);
     pull_ite_p.set_bool("local_ctx", true);
@@ -195,7 +197,7 @@ tactic * mk_preamble_tactic(ast_manager& m) {
         and_then(
             mk_simplify_tactic(m),
             mk_propagate_values_tactic(m),
-            using_params(mk_ctx_simplify_tactic(m), ctx_simp_p),
+            tp.local_ctx() ? using_params(mk_ctx_simplify_tactic(m), ctx_simp_p) : mk_skip_tactic(),
             using_params(mk_simplify_tactic(m), pull_ite_p),
             mk_solve_eqs_tactic(m),
             mk_elim_uncnstr_tactic(m));

src/test/bit_blaster.cpp

@@ -23,6 +23,10 @@ Revision History:
 #include "ast/rewriter/bit_blaster/bit_blaster.h"
 #include "model/model.h"
 #include "model/model_evaluator.h"
+#include "smt/smt_kernel.h"
+#include "smt/params/smt_params.h"
+#include "ast/for_each_expr.h"
+
 
 void mk_bits(ast_manager & m, char const * prefix, unsigned sz, expr_ref_vector & r) {
     sort_ref b(m);
@@ -184,6 +188,41 @@ void tst_multiplier(ast_manager & m, bit_blaster & blaster) {
     ENSURE_INT(mdl, c, 7); // b111 * b001
 }
 
+void tst_const_multiplier(ast_manager& m, bit_blaster & blaster, unsigned sz) {
+    expr_ref_vector x(m);
+    mk_bits(m, "x", sz, x);
+    for (unsigned i = 0; i < (1ul << sz); ++i) {
+        expr_ref_vector c(m), out1(m), out2(m);
+        for (unsigned j = 0; j < sz; ++j) 
+            c.push_back((i & (1ul << j)) ? m.mk_true() : m.mk_false());
+        for (auto xi : x)
+            verbose_stream() << mk_pp(xi, m);
+        verbose_stream() << " ";
+        for (auto ci : c)
+            verbose_stream() << mk_pp(ci, m);
+        verbose_stream() << "\n";
+        blaster.mk_const_case1_multiplier(sz, c.data(), x.data(), out1);
+        
+        blaster.mk_generic_multiplier(sz, c.data(), x.data(), out2);
+        expr_ref fml(m.mk_true(), m);
+        for (unsigned j = 0; j < sz; ++j)
+            fml = m.mk_and(fml, m.mk_eq(out1.get(j), out2.get(j)));
+        smt_params fp;
+        smt::kernel solver(m, fp);
+        solver.assert_expr(m.mk_not(fml));
+        auto r = solver.check();
+        verbose_stream() << r << "\n";
+        VERIFY(r == l_false);
+        expr_mark vis1, vis2;
+        unsigned sz1 = 0, sz2 = 0;
+        for (auto o : out1)            
+            sz1 += get_num_exprs(o, vis1);
+        for (auto o : out2)            
+            sz2 += get_num_exprs(o, vis2);
+        verbose_stream() << "sizes " << sz1 << " vs " << sz2 << "\n";
+    }
+}
+
 void tst_le(ast_manager & m, unsigned sz) {
 //     expr_ref_vector a(m);
 //     expr_ref_vector b(m);
@@ -233,6 +272,7 @@ void tst_bit_blaster() {
     bit_blaster_params params;
     bit_blaster blaster(m, params);
 
+    tst_const_multiplier(m, blaster, 7);
     tst_adder(m, blaster);
     tst_multiplier(m, blaster);
     tst_le(m, 4);