add notes and tangent lemma

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

src/math/polysat/saturation.cpp

@@ -42,6 +42,8 @@ namespace polysat {
                 return true;
             if (try_y_l_ax_and_x_l_z(v, core, c))
                 return true;
+            if (try_tangent(v, core, c))
+                return true;
         }
         return false;
     }
@@ -380,4 +382,27 @@ namespace polysat {
         return propagate(core, z_l_y, yx_l_zx, z_l_y.is_strict || yx_l_zx.is_strict, y * x, y_prime * x, new_constraints);
     }
 
+    // [x] p(x) <= q(x) where value(p) > value(q)
+    //     ==> q <= value(q) => p <= value(q)
+
+    bool inf_saturate::try_tangent(pvar v, conflict& core, inequality const& c) {
+        if (!c.src->contains_var(v))
+            return false;
+        if (c.lhs.is_val() || c.rhs.is_val())
+            return false;
+        if (!c.as_signed_constraint().is_currently_false(s()))
+            return false;
+        rational l_val, r_val;
+        if (!s().try_eval(c.lhs, l_val))
+            return false;
+        if (!s().try_eval(c.rhs, r_val))
+            return false;
+        SASSERT(c.is_strict || l_val > r_val);
+        SASSERT(!c.is_strict || l_val >= r_val);
+        vector<signed_constraint> new_constraints;
+        new_constraints.push_back(c.as_signed_constraint());
+        new_constraints.push_back(s().ule(c.rhs, r_val));
+        return propagate(core, c, c, c.is_strict ? s().ult(c.lhs, r_val) : s().ule(c.lhs, r_val), new_constraints);
+    }
+
 }

src/math/polysat/saturation.h

@@ -54,6 +54,8 @@ namespace polysat {
         bool try_ugt_z(pvar z, conflict& core, inequality const& c);
         bool try_ugt_z(pvar z, conflict& core, inequality const& x_l_z0, inequality const& yz_l_xz, pdd const& y, pdd const& x);
 
+        bool try_tangent(pvar v, conflict& core, inequality const& c);
+
         // c := lhs ~ v 
         //  where ~ is < or <=         
         bool is_l_v(pvar v, inequality const& c);

src/math/polysat/solver.cpp

@@ -640,8 +640,6 @@ namespace polysat {
         }
         m_conflict.reset();
 
-        std::cout << "reason " << *reason << "\n";
-
         // The lemma where 'lit' comes from.
         // Currently, boolean decisions always come from guessing a literal of a learned non-unit lemma.
         clause* lemma = m_bvars.lemma(var);  // need to grab this while 'lit' is still assigned

src/math/polysat/solver.h

@@ -267,7 +267,9 @@ namespace polysat {
         signed_constraint eq(pdd const& p, rational const& q) { return eq(p - q); }
         signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); }
         signed_constraint ule(pdd const& p, pdd const& q) { return m_constraints.ule(p, q); }
+        signed_constraint ule(pdd const& p, rational const& q) { return m_constraints.ule(p, p.manager().mk_val(q)); }
         signed_constraint ult(pdd const& p, pdd const& q) { return m_constraints.ult(p, q); }
+        signed_constraint ult(pdd const& p, rational const& q) { return m_constraints.ult(p, p.manager().mk_val(q)); }
         signed_constraint sle(pdd const& p, pdd const& q) { return m_constraints.sle(p, q); }
         signed_constraint slt(pdd const& p, pdd const& q) { return m_constraints.slt(p, q); }
 

src/math/polysat/ule_constraint.cpp

@@ -12,16 +12,17 @@ Author:
 
 Notes:
 
-    TODO: Maybe we want to rewrite some of the following into equalities? (i.e., into p<=0)
+   TODO: add rewrite rules to simplify expressions
   
-         p <= 0   <==>  p = 0
+   - k1 <= k2   ==> 0 <= 0 if k1 <= k2
-         -1 <= p  <==>  p = -1
+   - k1 <= k2   ==> 1 <= 0 if k1 >  k2
-         1 <= p   <==>  p != 0
+   - 0 <= p     ==> 0 <= 0
-         p <= -2  <==>  p != -1
+   - p <= -1    ==> 0 <= 0
+   - k*p <= 0   ==> p <= 0 if k is odd
 
-         e.g.
+   - k <= p     ==> p - k <= k - 1
-         x - 2 >= 1   <==>  x != 2
+   - p <= p + q ==> p <= -q - 1
-         2 - x >= -1  <==>  x = 3
+   - p + k <= p ==> p + k <= k - 1   for k > 0
 
 --*/
 
@@ -33,10 +34,17 @@ namespace polysat {
 
     ule_constraint::ule_constraint(constraint_manager& m, pdd const& l, pdd const& r) :
         constraint(m, ckind_t::ule_t), m_lhs(l), m_rhs(r) {
-        m_vars.append(l.free_vars());
+
-        for (auto v : r.free_vars())
+        simplify();
+
+        m_vars.append(m_lhs.free_vars());
+        for (auto v : m_rhs.free_vars())
             if (!m_vars.contains(v))
                 m_vars.push_back(v);
+
+    }
+
+    void ule_constraint::simplify() {
         if (m_lhs.is_val() && m_rhs.is_val()) {
             if (m_lhs.val() <= m_rhs.val())
                 m_lhs = m_rhs = 0;

src/math/polysat/ule_constraint.h

@@ -24,6 +24,7 @@ namespace polysat {
         pdd m_rhs;
 
         ule_constraint(constraint_manager& m, pdd const& l, pdd const& r);
+        void simplify();
 
     public:
         ~ule_constraint() override {}