Merge remote-tracking branch 'origin/polysat' into polysat

src/math/polysat/conflict.cpp

@@ -79,7 +79,11 @@ namespace polysat {
 
         // Analyse current conflict core to extract additional lemmas
         void find_extra_lemmas(conflict& core) {
+#if 1
+            // Don't do variable elimination for now
+#else
             m_free_variable_elimination.find_lemma(core);
+#endif
         }
     };
 

src/math/polysat/constraint_manager.cpp

@@ -446,14 +446,23 @@ namespace polysat {
     }
 
     pdd constraint_manager::lshr(pdd const& p, pdd const& q) {
+        if (p.is_val() && q.is_val() && q.val().is_unsigned()) {
+            return p.manager().mk_val(div(p.val(), rational::power_of_two(q.val().get_unsigned())));
+        }
         return mk_op_term(op_constraint::code::lshr_op, p, q);
     }
 
     pdd constraint_manager::shl(pdd const& p, pdd const& q) {
+        if (p.is_val() && q.is_val() && q.val().is_unsigned()) {
+            return p.manager().mk_val(p.val() * rational::power_of_two(q.val().get_unsigned()));
+        }
         return mk_op_term(op_constraint::code::shl_op, p, q);
     }
 
     pdd constraint_manager::band(pdd const& p, pdd const& q) {
+        if (p.is_val() && q.is_val()) {
+            return p.manager().mk_val(bitwise_and(p.val(), q.val()));
+        }
         return mk_op_term(op_constraint::code::and_op, p, q);
     }
 

src/math/polysat/constraint_manager.h

@@ -82,7 +82,7 @@ namespace polysat {
 
         void ensure_bvar(constraint* c);
         void erase_bvar(constraint* c);
-
+        
         signed_constraint mk_op_constraint(op_constraint::code op, pdd const& p, pdd const& q, pdd const& r);
         pdd mk_op_term(op_constraint::code op, pdd const& p, pdd const& q);
 

src/math/polysat/log.cpp

@@ -38,14 +38,14 @@ char const* color_reset()  { return "\x1B[0m"; }
 
 std::atomic<bool> g_log_enabled(true);
 
-bool get_log_enabled() {
-    return g_log_enabled;
-}
-
 void set_log_enabled(bool log_enabled) {
     g_log_enabled = log_enabled;
 }
 
+bool get_log_enabled() {
+  return g_log_enabled;
+}
+
 static LogLevel get_max_log_level(std::string const& fn, std::string const& pretty_fn) {
   (void)fn;
   (void)pretty_fn;

src/math/polysat/solver.h

@@ -376,7 +376,7 @@ namespace polysat {
 
         /** Create expression for the logical left shift of p by q. */
         pdd shl(pdd const& p, pdd const& q) { return m_constraints.shl(p, q); }
-
+        
         /** Create expression for the bit-wise negation of p. */
         pdd bnot(pdd const& p) { return m_constraints.bnot(p); }
 

src/math/polysat/variable_elimination.cpp

@@ -18,14 +18,226 @@ Author:
 #include <algorithm>
 
 namespace polysat {
+    
+    pdd free_variable_elimination::get_hamming_distance(pdd p) {
+        SASSERT(p.power_of_2() >= 8); // TODO: Implement special cases for smaller bit-width
+        // The trick works only for multiples of 8 (because of the final multiplication).
+        // Maybe it can be changed to work for all sizes
+        SASSERT(p.power_of_2() % 8 == 0); 
+        
+        // Proven for 8, 16, 24, 32 by bit-blasting in Z3
+        
+        // https://en.wikipedia.org/wiki/Hamming_weight
+        const unsigned char pattern_55 = 0x55; // 01010101
+        const unsigned char pattern_33 = 0x33; // 00110011
+        const unsigned char pattern_0f = 0x0f; // 00001111
+        const unsigned char pattern_01 = 0x01; // 00000001
+        
+        unsigned to_alloc = (p.power_of_2() + sizeof(unsigned) - 1) / sizeof(unsigned);
+        unsigned to_alloc_bits = to_alloc * sizeof(unsigned);
+        
+        // Cache this?
+        auto* scaled_55 = (unsigned*)alloca(to_alloc_bits);
+        auto* scaled_33 = (unsigned*)alloca(to_alloc_bits);
+        auto* scaled_0f = (unsigned*)alloca(to_alloc_bits);
+        auto* scaled_01 = (unsigned*)alloca(to_alloc_bits);
+        
+        memset(scaled_55, pattern_55, to_alloc_bits);
+        memset(scaled_33, pattern_33, to_alloc_bits);
+        memset(scaled_0f, pattern_0f, to_alloc_bits);
+        memset(scaled_01, pattern_01, to_alloc_bits);
+        
+        rational rational_scaled_55(scaled_55, to_alloc);
+        rational rational_scaled_33(scaled_33, to_alloc);
+        rational rational_scaled_0f(scaled_0f, to_alloc);
+        rational rational_scaled_01(scaled_01, to_alloc);
+        
+        auto& m = p.manager();
+        
+        pdd w = p - s.band(s.lshr(p, m.one()), m.mk_val(rational_scaled_55));
+        w = s.band(w, m.mk_val(rational_scaled_33)) + s.band(s.lshr(w, m.mk_val(2)), m.mk_val(rational_scaled_33));
+        w = s.band(w + s.lshr(w, m.mk_val(4)), m.mk_val(rational_scaled_0f));
+        //unsigned final_shift = p.power_of_2() - 8;
+        //final_shift = (final_shift + 7) / 8 * 8 - 1; // ceil final_shift to the next multiple of 8
+        return s.lshr(w * m.mk_val(rational_scaled_01), m.mk_val(p.power_of_2() - 8));
+    }
+    
+    pdd free_variable_elimination::get_odd(pdd p) {
+        SASSERT(p.is_val() || p.is_var()); // For now
+        
+        if (p.is_val()) {
+            const rational& v = p.val();
+            unsigned d = v.trailing_zeros(); 
+            if (!d)
+                return p.manager().mk_val(v);
+            return p.manager().mk_val(div(v, rational::power_of_two(d))); // TODO: Is there no shift?
+        }
+        pvar v = p.var();
+        if (m_rest_constants.size() > v && m_rest_constants[v] != -1)
+            return s.var(m_rest_constants[v]);
+        
+        pdd power = get_dyadic_valuation(p).second;
+        
+        pvar rest = s.add_var(p.power_of_2());
+        pdd rest_pdd = p.manager().mk_var(rest);
+        m_rest_constants.setx(v, rest, -1);
+        s.add_clause(s.eq(power * rest_pdd, p), false);
+        return rest_pdd;
+    }
+    
+    optional<pdd> free_variable_elimination::get_inverse(pdd p) {
+        SASSERT(p.is_val() || p.is_var()); // For now
+        
+        if (p.is_val()) {
+            pdd i = p.manager().zero();
+            if (!inv(p, i))
+                return {};
+            return optional<pdd>(i);
+        }
+        pvar v = p.var();
+        if (m_inverse_constants.size() > v && m_inverse_constants[v] != -1)
+            return optional<pdd>(s.var(m_inverse_constants[v]));
+        
+        pvar inv = s.add_var(p.power_of_2());
+        pdd inv_pdd = p.manager().mk_var(inv);
+        m_inverse_constants.setx(v, inv, -1);
+        s.add_clause(s.eq(inv_pdd * p, p.manager().one()), false);
+        return optional<pdd>(inv_pdd);
+    }
+    
+#define PV_MOD 2
+    
+    // symbolic version of "max_pow2_divisor" for checking if it is exactly "k"
+    void free_variable_elimination::add_dyadic_valuation(pvar v, unsigned k) {
+        // TODO: works for all values except 0; how to deal with this case?
+        pdd p = s.var(v);
+        auto& m = p.manager();
+        
+        pvar pv;
+        pvar pv2;
+        bool new_var = false;
+        if (m_pv_constants.size() <= v || m_pv_constants[v] == -1) {
+            pv = s.add_var(m.power_of_2()); // TODO: What's a good value? Unfortunately we cannot use a integer
+            pv2 = s.add_var(m.power_of_2());
+            m_pv_constants.setx(v, pv, -1);
+            m_pv_power_constants.setx(v, pv2, -1);
+            m.mk_var(pv);
+            m.mk_var(pv2);
+            new_var = true;
+        }
+        else {
+            pv = m_pv_constants[v];
+            pv2 = m_pv_power_constants[v];
+        }
+        
+        bool e = get_log_enabled();
+        set_log_enabled(false);
+
+        // For testing some different implementations
+#if PV_MOD == 1
+        // brute-force bit extraction and <=
+        signed_constraint c1 = s.eq(rational::power_of_two(p.power_of_2() - k - 1) * p, m.zero());
+        signed_constraint c2 = s.ule(m.mk_val(k), s.var(pv));
+        s.add_clause(~c1, c2, false);
+        s.add_clause(c1, ~c2, false);
+        
+        if (new_var) {
+            s.add_clause(s.eq(s.var(pv2), s.shl(m.one(), s.var(pv))), false);
+        }
+#elif PV_MOD == 2
+        // symbolic "maximal divisible"
+        signed_constraint c1 = s.eq(s.shl(s.lshr(p, s.var(pv)), s.var(pv)), p);
+        signed_constraint c2 = ~s.eq(s.shl(s.lshr(p, s.var(pv + 1)), s.var(pv + 1)), p);
+        
+        signed_constraint z = ~s.eq(p, p.manager().zero());
+        
+        // v != 0 ==> [(v >> pv) << pv == v && (v >> pv + 1) << pv + 1 != v]
+        s.add_clause(~z, c1, false);
+        s.add_clause(~z, c2, false);
+        
+        if (new_var) {
+            s.add_clause(s.eq(s.var(pv2), s.shl(m.one(), s.var(pv))), false);
+        }
+#elif PV_MOD == 3
+        // computing the complete function by hamming-distance
+        // proven equivalent with case 2 via bit-blasting for small sizes
+        s.add_clause(s.eq(s.var(pv), get_hamming_distance(s.bxor(p, p - 1)) - 1), false);
+        
+        // in case v == 0 ==> pv == k - 1 (we don't care)
+        
+        if (new_var) {
+            s.add_clause(s.eq(s.var(pv2), s.shl(m.one(), s.var(pv))), false);
+        }
+#elif PV_MOD == 4
+        // brute-force bit-and
+        // (pv = k && pv2 = 2^k) <==> ((v & (2^(k + 1) - 1)) = 2^k) 
+        
+        rational mask = rational::power_of_two(k + 1) - 1;
+        pdd masked = s.band(s.var(v), s.var(v).manager().mk_val(mask));
+        std::pair<pdd, pdd> odd_part = s.quot_rem(s.var(v), s.var(pv2));
+        
+        signed_constraint c1 = s.eq(s.var(pv), k);
+        signed_constraint c2 = s.eq(s.var(pv2), rational::power_of_two(k));
+        signed_constraint c3 = s.eq(masked, rational::power_of_two(k));
+        
+        s.add_clause(c1, ~c3, false);
+        s.add_clause(c2, ~c3, false);
+        s.add_clause(~c1, ~c2, c3, false);
+        
+        s.add_clause(s.eq(odd_part.second, 0), false); // The division has to be exact
+#endif
+        
+        set_log_enabled(e);
+    }
+    
+    std::pair<pdd, pdd> free_variable_elimination::get_dyadic_valuation(pdd p, unsigned short lower, unsigned short upper) {
+        SASSERT(p.is_val() || p.is_var()); // For now
+        SASSERT(lower == 0);
+        SASSERT(upper == p.power_of_2()); // Maybe we don't need all. However, for simplicity have this now
+        
+        if (p.is_val()) {
+            rational pv(p.val().trailing_zeros());
+            rational pv2 = rational::power_of_two(p.val().trailing_zeros());
+            return { p.manager().mk_val(pv), p.manager().mk_val(pv2) };
+        }
+        
+        pvar v = p.var();
+        unsigned short prev_lower = 0, prev_upper = 0;
+        if (m_has_validation_of_range.size() > v) {
+            unsigned range = m_has_validation_of_range[v];
+            prev_lower = range & 0xFFFF;
+            prev_upper = range >> 16;
+            if (lower >= prev_lower && upper <= prev_upper)
+                return { s.var(m_pv_constants[v]), s.var(m_pv_power_constants[v]) }; // exists already in the required range
+        }
+#if PV_MOD == 2 || PV_MOD == 3
+        LOG("Adding valuation function for variable " << v);
+        add_dyadic_valuation(v, 0);
+        m_has_validation_of_range.setx(v, (unsigned)UCHAR_MAX << 16, 0);
+#else
+        LOG("Adding valuation function for variable " << v  << " in [" << lower << "; " << upper << ")");
+        m_has_validation_of_range.setx(v, lower | (unsigned)upper << 16, 0);
+        for (unsigned i = lower; i < prev_lower; i++) {
+            add_dyadic_valuation(v, i);
+        }
+        for (unsigned i = prev_upper; i < upper; i++) {
+            add_dyadic_valuation(v, i);
+        }
+#endif
+        return { s.var(m_pv_constants[v]), s.var(m_pv_power_constants[v]) };
+    }
+    
+    std::pair<pdd, pdd> free_variable_elimination::get_dyadic_valuation(pdd p) {
+        return get_dyadic_valuation(p, 0, p.power_of_2()); 
+    }
 
     void free_variable_elimination::find_lemma(conflict& core) {
         LOG_H1("Free Variable Elimination");
         LOG("core: " << core);
         LOG("Free variables: " << s.m_free_pvars);
         for (pvar v : core.vars_occurring_in_constraints())
-            if (!s.is_assigned(v))  // TODO: too restrictive. should also consider variables that will be unassigned only after backjumping (can update this after assignment handling in search state is refactored.)
-                find_lemma(v, core);
+            //if (!s.is_assigned(v))  // TODO: too restrictive. should also consider variables that will be unassigned only after backjumping (can update this after assignment handling in search state is refactored.)
+            find_lemma(v, core);
     }
 
     void free_variable_elimination::find_lemma(pvar v, conflict& core) {
@@ -46,53 +258,157 @@ namespace polysat {
         pdd const& p = c.eq();
         SASSERT_EQ(p.degree(v), 1);
         auto& m = p.manager();
-        pdd lc = m.zero();
+        pdd fac = m.zero();
         pdd rest = m.zero();
-        p.factor(v, 1, lc, rest);
-        if (rest.is_val())
-            return;
-        // lc * v + rest == p == 0
-        // v == -1 * rest * lc^-1
-
-        SASSERT(!lc.free_vars().contains(v));
+        p.factor(v, 1, fac, rest);
+        //if (rest.is_val()) // TODO: Why do we need this?
+        //    return;
+        
+        SASSERT(!fac.free_vars().contains(v));
         SASSERT(!rest.free_vars().contains(v));
 
-        LOG("lc: " << lc);
+        LOG("fac: " << fac);
         LOG("rest: " << rest);
-
-        substitution sub(m);
-        pdd const lcs = eval(lc, core, sub);
-        LOG("lcs: " << lcs);
-        pdd lci = m.zero();
-        if (!inv(lcs, lci))
-            return;
-
-        pdd const rs = sub.apply_to(rest);
-        pdd const vs = -rs * lci;  // this is the polynomial that computes v
-        LOG("vs: " << vs);
-        SASSERT(!vs.free_vars().contains(v));
-
+        
         // Find another constraint where we want to substitute v
         for (signed_constraint c_target : core) {
+            
             if (c == c_target)
                 continue;
             if (c_target.vars().size() <= 1)
                 continue;
             if (!c_target.contains_var(v))
                 continue;
-
             // TODO: helper method constraint::subst(pvar v, pdd const& p)
             //       (or rather, add it on constraint_manager since we need to allocate/dedup the new constraint)
             //  For now, just restrict to ule_constraint.
-            if (!c_target->is_ule())
+            if (!c_target->is_ule()) // TODO: Remove?
                 continue;
-            // TODO: maybe apply assignment a here as well
-            pdd const lhs = c_target->to_ule().lhs().subst_pdd(v, vs);
-            pdd const rhs = c_target->to_ule().rhs().subst_pdd(v, vs);
-            signed_constraint c_new = s.ule(lhs, rhs);
+            if (c_target->to_ule().lhs().degree(v) > 1 || // TODO: Invert non-linear variable?
+                c_target->to_ule().rhs().degree(v) > 1)
+                continue;
+            
+            signed_constraint p1 = s.ule(m.zero(), m.zero()); 
+            signed_constraint p2 = s.ule(m.zero(), m.zero());
+            
+            pdd new_lhs = p.manager().zero();
+            pdd new_rhs = p.manager().zero();
+            
+            pdd fac_lhs = m.zero(); 
+            pdd fac_rhs = m.zero(); 
+            pdd rest_lhs = m.zero(); 
+            pdd rest_rhs = m.zero(); 
+            c_target->to_ule().lhs().factor(v, 1, fac_lhs, rest_lhs);
+            c_target->to_ule().rhs().factor(v, 1, fac_rhs, rest_rhs);
+            
+            LOG_H3("With constraint " << lit_pp(s, c_target) << ":");
+            LOG("c_target: " << lit_pp(s, c_target));
+            LOG("fac_lhs: " << fac_lhs);
+            LOG("rest_lhs: " << rest_lhs);
+            LOG("fac_rhs: " << fac_rhs);
+            LOG("rest_rhs: " << rest_rhs);
+            
+            pdd pv_equality = p.manager().zero();
+            pdd lhs_multiple = p.manager().zero(); 
+            pdd rhs_multiple = p.manager().zero(); 
+            pdd coeff_odd = p.manager().zero();
+            optional<pdd> fac_odd_inv;
+            
+            get_multiple_result multiple1 = get_multiple(fac_lhs, fac, new_lhs);
+            get_multiple_result multiple2 = get_multiple(fac_rhs, fac, new_rhs);
+
+            if (multiple1 == cannot_multiple || multiple2 == cannot_multiple)
+                continue;
+
+            bool evaluated = false;
+            substitution sub(m);
+
+            if (multiple1 == can_multiple || multiple2 == can_multiple) {
+                if (
+                        (!fac.is_val() && !fac.is_var()) ||
+                        (!fac_lhs.is_val() && !fac_lhs.is_var()) ||
+                        (!fac_rhs.is_val() && !fac_rhs.is_var())) {
+
+                    // TODO: We could introduce a new variable "new_var = lc" and add the valuation for this new variable
+                    if (s.is_assigned(v))
+                        continue; // We could not eliminate it symbolically and evaluating makes no sense as we already have a value for it
+
+                    pdd const fac_eval = eval(fac, core, sub);
+                    LOG("fac_eval: " << fac_eval);
+                    pdd fac_eval_inv = m.zero();
+
+                    // TODO: We can now again use multiples instead of failing if it is not invertible
+                    // e.g., x * y + x * z = z (with y = 0 eval)
+                    // and,  3 * x * z <= 0
+                    // We don't do anything, although we could
+                    // x * z = z
+                    // and multiplying with 3 results in a feasible replacement
+                    if (!inv(fac_eval, fac_eval_inv))
+                        continue;
+
+                    LOG("fac_eval_inv: " << fac_eval_inv);
+
+                    pdd const rest_eval = sub.apply_to(rest);
+                    LOG("rest_eval: " << rest_eval);
+                    pdd const vs = -rest_eval * fac_eval_inv;  // this is the polynomial that computes v
+                    LOG("vs: " << vs);
+                    SASSERT(!vs.free_vars().contains(v));
+
+                    // TODO: Why was the assignment (sub) not applied to the result in previous commits?
+                    new_lhs = sub.apply_to(c_target->to_ule().lhs().subst_pdd(v, vs));
+                    new_rhs = sub.apply_to(c_target->to_ule().rhs().subst_pdd(v, vs));
+                    evaluated = true;
+                }
+                else {
+                    pv_equality = get_dyadic_valuation(fac).first;
+                    LOG("pv_equality " << pv_equality);
+                    coeff_odd = get_odd(fac); // a'
+                    LOG("coeff_odd: " << coeff_odd);
+                    fac_odd_inv = get_inverse(coeff_odd); // a'^-1
+                    if (!fac_odd_inv)
+                        continue; // factor is for sure not invertible
+                    LOG("coeff_odd_inv: " << *fac_odd_inv);
+                }
+            }
+
+            if (!evaluated) {
+                if (multiple1 == can_multiple) {
+                    pdd pv_lhs = get_dyadic_valuation(fac_lhs).first;
+                    pdd odd_fac_lhs = get_odd(fac_lhs);
+                    pdd power_diff_lhs = s.shl(m.one(), pv_lhs - pv_equality);
+
+                    LOG("pv_lhs: " << pv_lhs);
+                    LOG("odd_fac_lhs: " << odd_fac_lhs);
+                    LOG("power_diff_lhs: " << power_diff_lhs);
+                    new_lhs = -rest * *fac_odd_inv * power_diff_lhs * odd_fac_lhs + rest_rhs;
+                    p1 = s.ule(get_dyadic_valuation(fac).first, get_dyadic_valuation(fac_lhs).first);
+                }
+                else {
+                    SASSERT(multiple1 == is_multiple);
+                    new_lhs = -rest * new_lhs + rest_lhs;
+                }
+
+                if (multiple2 == can_multiple) {
+                    pdd pv_rhs = get_dyadic_valuation(fac_rhs).first;
+                    pdd odd_fac_rhs = get_odd(fac_rhs);
+                    pdd power_diff_rhs = s.shl(m.one(), pv_rhs - pv_equality);
+
+                    LOG("pv_rhs: " << pv_rhs);
+                    LOG("odd_fac_rhs: " << odd_fac_rhs);
+                    LOG("power_diff_rhs: " << power_diff_rhs);
+                    new_rhs = -rest * *fac_odd_inv * power_diff_rhs * odd_fac_rhs + rest_rhs;
+                    p2 = s.ule(get_dyadic_valuation(fac).first, get_dyadic_valuation(fac_rhs).first);
+                }
+                else {
+                    SASSERT(multiple2 == is_multiple);
+                    new_rhs = -rest * new_rhs + rest_rhs;
+                }
+            }
+            
+            signed_constraint c_new = s.ule(new_lhs , new_rhs);
+            
             if (c_target.is_negative())
                 c_new.negate();
-            LOG("c_target: " << lit_pp(s, c_target));
             LOG("c_new:    " << lit_pp(s, c_new));
 
             // New constraint is already true (maybe we already derived it previously?)
@@ -100,14 +416,24 @@ namespace polysat {
             //       E.g., if the new clause could derive c_new at a lower decision level.
             if (c_new.bvalue(s) == l_true)
                 continue;
-
+            
+            LOG("p1:    " << p1);
+            LOG("p2:    " << p2);
+                        
             clause_builder cb(s);
-            for (auto [w, wv] : sub)
-                cb.insert(~s.eq(s.var(w), wv));
+
+            if (evaluated) {
+                for (auto [w, wv] : sub)
+                    cb.insert(~s.eq(s.var(w), wv));
+            }
             cb.insert(~c);
             cb.insert(~c_target);
+            cb.insert(~p1);
+            cb.insert(~p2);
             cb.insert(c_new);
-            core.add_lemma("variable elimination", cb.build());
+            ref<clause> c = cb.build();
+            if (c) // Can we get tautologies this way?
+                core.add_lemma("variable elimination", c);
         }
     }
 
@@ -117,15 +443,13 @@ namespace polysat {
         // TODO: recognize constraints of the form "v1 == 27" to be used in the assignment?
         //       (but maybe useful evaluations are always part of core.vars() anyway?)
 
-        substitution& sub = out_sub;
-        SASSERT(sub.empty());
+        SASSERT(out_sub.empty());
 
         for (auto v : p.free_vars())
             if (core.contains_pvar(v))
-                sub.add(v, s.get_value(v));
-
-        pdd q = sub.apply_to(p);
+                out_sub = out_sub.add(v, s.get_value(v));
 
+        pdd q = out_sub.apply_to(p);
         // TODO: like in the old conflict::minimize_vars, we can now try to remove unnecessary variables from a.
 
         return q;
@@ -143,5 +467,62 @@ namespace polysat {
         out_p_inv = p.manager().mk_val(iv);
         return true;
     }
+    
+    
+    free_variable_elimination::get_multiple_result free_variable_elimination::get_multiple(const pdd& p1, const pdd& p2, pdd& out) {
+        LOG("Check if there is an easy way to unify " << p2 << " and " << p1);
+        if (p1.is_zero()) {
+            out = p1.manager().zero();
+            return is_multiple;
+        }
+        if (p2.is_one()) {
+            out = p1;
+            return is_multiple;
+        }
+        if (!p1.is_monomial() || !p2.is_monomial())
+            // TODO: Actually, this could work as well. (4a*d + 6b*c*d) is a multiple of (2a + 3b*c) although none of them is a monomial
+            return can_multiple;
+        dd::pdd_monomial p1m = *p1.begin();
+        dd::pdd_monomial p2m = *p2.begin();
+        
+        unsigned tz1 = p1m.coeff.trailing_zeros();
+        unsigned tz2 = p2m.coeff.trailing_zeros();
+        
+        if (tz2 > tz1)
+            return cannot_multiple; // The constant coefficient is not invertible
+        
+        rational odd = div(p2m.coeff, rational::power_of_two(tz2));
+        rational inv;
+        bool succ = odd.mult_inverse(p1.power_of_2() - tz2, inv);
+        SASSERT(succ); // we divided by the even part so it has to be odd/invertible
+        inv *= div(p1m.coeff, rational::power_of_two(tz2));
+        
+        m_occ_cnt.reserve(s.m_vars.size(), (unsigned)0); // TODO: Are there duplicates in the list (e.g., v1 * v1)?)
+        
+        for (const auto& v1 : p1m.vars) {
+            if (m_occ_cnt[v1] == 0)
+                m_occ.push_back(v1);
+            m_occ_cnt[v1]++;
+        }
+        for (const auto& v2 : p2m.vars) {
+            if (m_occ_cnt[v2] == 0) {
+                for (const auto& occ : m_occ)
+                    m_occ_cnt[occ] = 0;
+                m_occ.clear();
+                return can_multiple; // p2 contains more v2 than p1; we need more information
+            }
+            m_occ_cnt[v2]--;
+        }
+        
+        out = p1.manager().mk_val(inv);
+        for (const auto& occ : m_occ) {
+            for (unsigned i = 0; i < m_occ_cnt[occ]; i++)
+                out *= s.var(occ);
+            m_occ_cnt[occ] = 0;
+        }
+        m_occ.clear();
+        LOG("Found multiple: " << out);
+        return is_multiple;
+    }
 
 }

src/math/polysat/variable_elimination.h

@@ -21,14 +21,35 @@ namespace polysat {
     class conflict;
 
     class free_variable_elimination {
+
+        enum get_multiple_result {
+          is_multiple, can_multiple, cannot_multiple
+        };
+
         solver& s;
+        unsigned_vector m_has_validation_of_range; // TODO: Find a better name
+        unsigned_vector m_pv_constants;
+        unsigned_vector m_pv_power_constants;
+        unsigned_vector m_inverse_constants;
+        unsigned_vector m_rest_constants;
+        
+        unsigned_vector m_occ;
+        unsigned_vector m_occ_cnt;
+        
+        pdd get_hamming_distance(pdd p);
+        pdd get_odd(pdd p); // add lemma "2^pv(v) * v' = v"
+        optional<pdd> get_inverse(pdd v); // add lemma "v' * v'^-1 = 1 (where v' is the odd part of v)"
+        void add_dyadic_valuation(pvar v, unsigned k); // add lemma "pv(v) = k" ==> "pv_v = k"
+        std::pair<pdd, pdd> get_dyadic_valuation(pdd p, unsigned short lower, unsigned short upper); // lower bound inclusive; upper exclusive
+        std::pair<pdd, pdd> get_dyadic_valuation(pdd p);
         void find_lemma(pvar v, conflict& core);
         void find_lemma(pvar v, signed_constraint c, conflict& core);
         pdd eval(pdd const& p, conflict& core, substitution& out_sub);
         bool inv(pdd const& p, pdd& out_p_inv);
+        get_multiple_result get_multiple(const pdd& p1, const pdd& p2, pdd &out);
     public:
         free_variable_elimination(solver& s): s(s) {}
         void find_lemma(conflict& core);
-    };
+};
 
 }