push outline of using cjust for overflow premise

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

src/math/dd/dd_fdd.cpp

@@ -332,5 +332,35 @@ namespace dd {
         return true;
     }
 
+    rational fdd::max(bdd b) const {
+        SASSERT(!b.is_false());
+        rational result(0);
+        for (unsigned i = num_bits(); i-- > 0; ) {
+            unsigned v = m_pos2var[i];
+            bdd w = m->mk_var(v);
+            bdd hi = b.cofactor(w);
+            if (!hi.is_false()) {
+                b = hi;
+                result += rational::power_of_two(i);
+            }
+        }
+        return result;
+    }
+
+    rational fdd::min(bdd b) const {
+        SASSERT(!b.is_false());
+        rational result(0);
+        for (unsigned i = num_bits(); i-- > 0; ) {
+            unsigned v = m_pos2var[i];
+            bdd nw = m->mk_nvar(v);
+            bdd lo = b.cofactor(nw);
+            if (lo.is_false())
+                result += rational::power_of_two(i);
+            else
+                b = lo;
+        }
+        return result;
+    }
+
 
 }

src/math/dd/dd_fdd.h

@@ -78,26 +78,31 @@ namespace dd {
         /** Like find, but returns hint if it is contained in the BDD. */
         find_t find_hint(bdd b, rational const& hint, rational& out_val) const;
 
+        /*
+         * find largest value at lo or above such that bdd b evaluates to true
+         * at lo and all values between.
+         * dually, find smallest value below hi that evaluates b to true
+         * and all values between the value and hi also evaluate b to true.
+         * \param b - a bdd using variables from this
+         * \param lo/hi - bound to be traversed.
+         * \return false if b is false at lo/hi
+         * \pre variables in b are a subset of variables from the fdd
+         */
+        bool sup(bdd const& b, bool_vector& lo) const;
 
-
-	/*
-	 * find largest value at lo or above such that bdd b evaluates to true
-	 * at lo and all values between.
-	 * dually, find smallest value below hi that evaluates b to true
-	 * and all values between the value and hi also evaluate b to true.
-	 * \param b - a bdd using variables from this
-	 * \param lo/hi - bound to be traversed.
-	 * \return false if b is false at lo/hi
-	 * \pre variables in b are a subset of variables from the fdd
-	 */ 
-	bool sup(bdd const& b, bool_vector& lo) const;
-      
-	bool inf(bdd const& b, bool_vector& hi) const; 
+        bool inf(bdd const& b, bool_vector& hi) const;
 
         bool sup(bdd const& b, rational& lo) const;
 
         bool inf(bdd const& b, rational& hi) const;
-      
+
+        /*
+        * Find the min-max satisfying assignment.
+        * \pre b is not false.
+        */
+        rational max(bdd b) const;
+
+        rational min(bdd b) const;
     };
 
 }

src/math/dd/dd_pdd.h

@@ -246,6 +246,7 @@ namespace dd {
         inline bool is_one(PDD p) const { return p == one_pdd; } 
         inline bool is_val(PDD p) const { return m_nodes[p].is_val(); }
         inline bool is_internal(PDD p) const { return m_nodes[p].is_internal(); }
+        inline bool is_var(PDD p) const { return !is_val(p) && is_zero(lo(p)) && is_one(hi(p)); }
         bool is_never_zero(PDD p);
         inline unsigned level(PDD p) const { return m_nodes[p].m_level; }
         inline unsigned var(PDD p) const { return m_level2var[level(p)]; }
@@ -388,6 +389,7 @@ namespace dd {
         bool is_one() const { return m.is_one(root); }
         bool is_zero() const { return m.is_zero(root); }
         bool is_linear() const { return m.is_linear(root); }
+        bool is_var() const { return m.is_var(root); }
         /** Polynomial is of the form: a * x + b */
         bool is_unilinear() const { return !is_val() && lo().is_val() && hi().is_val(); }
         bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); } 

src/math/polysat/saturation.cpp

@@ -87,6 +87,7 @@ namespace polysat {
         return best_bound != -1;
     }
 
+
     /// Add Ω*(x, y) to the conflict state.
     ///
     /// @param[in] p    bit width
@@ -160,6 +161,37 @@ namespace polysat {
         return true;
     }
 
+    // special case viable sets.
+    bool inf_saturate::push_omega_viable(conflict_core& core, clause_builder& reason, unsigned level, pdd const& px, pdd const& py) {
+        if (!px.is_var() || !py.is_var())
+            return false;
+        pvar x = px.var();
+        pvar y = py.var();
+        rational x_max = s().m_viable.max_viable(x);
+        rational y_max = s().m_viable.max_viable(y);
+        auto& pddm = px.manager();
+        unsigned bit_size = pddm.power_of_2();
+        if (x_max * y_max < rational::power_of_two(bit_size)) {
+            // max values don't overflow, we can justify no-overflow using cjust for x, y
+            for (auto c : s().m_cjust[x])
+                reason.push(c);
+            for (auto c : s().m_cjust[y])
+                reason.push(c);
+            return true;
+        }
+        
+        rational x_val = s().get_value(x);
+        rational y_val = s().get_value(y);
+
+        if (x_val * y_val >= rational::power_of_two(bit_size))
+            return false;
+
+        // TODO: try bisection approach to find values between x_val and y_val and x_max, y_max
+        // find x_mid, y_mid that doesn't overflow.
+
+        return false;
+    }
+
     /*
     * Match [v] .. <= v 
     */

src/math/polysat/saturation.h

@@ -38,6 +38,7 @@ namespace polysat {
     class inf_saturate : public inference_engine {
         bool find_upper_bound(pvar x, signed_constraint& c, rational& bound);
 
+        bool push_omega_viable(conflict_core& core, clause_builder& reason, unsigned level, pdd const& x, pdd const& y);
         bool push_omega_mul(conflict_core& core, clause_builder& reason, unsigned level, pdd const& x, pdd const& y);
         signed_constraint ineq(unsigned level, bool strict, pdd const& lhs, pdd const& rhs);
         void push_c(conflict_core& core, signed_constraint const& c, clause_builder& reason);

src/math/polysat/solver.h

@@ -228,6 +228,8 @@ namespace polysat {
         void new_constraint(signed_constraint c, unsigned dep, bool activate);
         static void insert_constraint(signed_constraints& cs, signed_constraint c);
 
+        viable& get_viable() { return m_viable; }
+
         bool invariant();
         static bool invariant(signed_constraints const& cs);
         bool wlist_invariant();

src/math/polysat/viable.cpp

@@ -241,6 +241,14 @@ namespace polysat {
 #endif
     }
 
+    rational viable::min_viable(pvar v) {
+        return var2bits(v).min(m_viable[v]);
+    }
+
+    rational viable::max_viable(pvar v) {
+        return var2bits(v).max(m_viable[v]);
+    }
+
     dd::fdd const& viable::sz2bits(unsigned sz) {
         m_bits.reserve(sz + 1);
         auto* bits = m_bits[sz];

src/math/polysat/viable.h

@@ -180,6 +180,12 @@ namespace polysat {
          */
         void add_non_viable(pvar v, rational const& val);
 
+        /*
+        * Extract min and max viable values for v
+        */
+        rational min_viable(pvar v);
+
+        rational max_viable(pvar v);
 
         /**
          * Find a next viable value for variable.