na

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

src/math/polysat/conflict.cpp

@@ -296,11 +296,8 @@ namespace polysat {
             return false;
         }
 
-        if (conflict_var() == v) {
+        if (conflict_var() == v && s.m_forbidden_intervals.perform(v, cjust_v, *this))
-            forbidden_intervals fi(s);
-            if (fi.perform(v, cjust_v, *this))
             return true;        
-        }
         
         m_vars.remove(v);
 

src/math/polysat/forbidden_intervals.cpp

@@ -17,6 +17,7 @@ Author:
 --*/
 #include "math/polysat/forbidden_intervals.h"
 #include "math/polysat/interval.h"
+#include "math/polysat/solver.h"
 #include "math/polysat/log.h"
 
 namespace polysat {
@@ -219,6 +220,8 @@ namespace polysat {
             return true;
         if (match_linear4(c, a1, b1, e1, a2, b2, e2, out_interval, out_side_cond))
             return true;
+        if (match_linear5(c, a1, b1, e1, a2, b2, e2, out_interval, out_side_cond))
+            return true;
 
         _backtrack.released = false;
         return false;
@@ -386,16 +389,27 @@ namespace polysat {
     }
 
     /**
+     * Ad-hoc linear forbidden intervals 
      * ax <= b, b != -1, a < b:     x not in [ceil((b+1)/a) .. floor((2^K-1)/a)]
      * b <= ax, 0 < a < b:          x not in [0 .. floor((b-1)/a)] 
      * ax < b, a < b:               x not in [ceil(b/a) .. floor((2^K-1)/a)]
      * b < ax, 0 < a <= b:          x not in [0 .. floor(b/a)]     
+     * 
+     * TODO: generalize to ax + b <= c scenarios where ax does not overflow 
+     * and ax+b does not overflow, but is larger than c
+     * Scenarios:
+     *  - ax + b <= c
+     *  - ax + b < c
+     *  - c <= ax + b
+     *  - c < ax + b
      */
     bool forbidden_intervals::match_linear5(signed_constraint const& c,
         rational const& a1, pdd const& b1, pdd const& e1,
         rational const& a2, pdd const& b2, pdd const& e2,
         eval_interval& interval, vector<signed_constraint>& side_cond) {
         auto& m = e1.manager();
+
+        // ax <= b, b != -1, a < b:     x not in [ceil((b+1)/a) .. floor((2^K-1)/a)]
         if (c.is_positive() && 
             !a1.is_zero() && !a1.is_one() && 
             a2.is_zero() && b1.is_zero() && e2.is_val() && 
@@ -404,11 +418,14 @@ namespace polysat {
                 side_cond.push_back(s.eq(e1));
             auto lo_val = ceil((b2.val() + 1) / a1);
             auto hi_val = floor(m.max_value() / a1) + 1;
+            SASSERT(lo_val < hi_val);
             auto lo = m.mk_val(lo_val);
             auto hi = m.mk_val(hi_val);
             interval = eval_interval::proper(lo, lo_val, hi, hi_val);
             return true;            
         }
+
+        // b <= ax, 0 < a < b:          x not in [0 .. floor((b-1)/a)] 
         if (c.is_positive() && 
             !a2.is_zero() && !a2.is_one() && 
             a1.is_zero() && b2.is_zero() &&
@@ -417,15 +434,39 @@ namespace polysat {
                 side_cond.push_back(s.eq(e2));
             auto lo_val = rational::zero();
             auto hi_val = floor((b1.val() - 1) / a2) + 1;
+            SASSERT(lo_val < hi_val);
             auto lo = m.mk_val(lo_val);
             auto hi = m.mk_val(hi_val);
             interval = eval_interval::proper(lo, lo_val, hi, hi_val);
             return true;
         }
-        if (c.is_negative() && 
-            !a2.is_zero() && !a2.is_one() && 
-            a1.is_zero() && false) {
 
+        // ax < b, a < b:               x not in [ceil(b/a) .. floor((2^K-1)/a)]
+        if (c.is_negative() && 
+            !a2.is_zero() && !a2.is_one() && b2.is_zero() && 
+            a1.is_zero() && e1.is_val() && a2 < b1.val()) {
+            if (!e2.is_val())
+                side_cond.push_back(s.eq(e2));
+            auto lo_val = ceil(b1.val() / a2);
+            auto hi_val = floor(m.max_value() / a2) + 1;
+            auto lo = m.mk_val(lo_val);
+            auto hi = m.mk_val(hi_val);
+            interval = eval_interval::proper(lo, lo_val, hi, hi_val);
+            return true;
+        }
+
+        // b < ax, 0 < a <= b:          x not in [0 .. floor(b/a)]     
+        if (c.is_negative() &&
+            !a1.is_zero() && !a1.is_one() && b1.is_zero() &&
+            a2.is_zero() && e2.is_val() && a1 <= b2.val()) { 
+            if (!e1.is_val())
+                side_cond.push_back(s.eq(e2));
+            auto lo_val = rational::zero();
+            auto hi_val = floor(b2.val() / a1) + 1;
+            auto lo = m.mk_val(lo_val);
+            auto hi = m.mk_val(hi_val);
+            interval = eval_interval::proper(lo, lo_val, hi, hi_val);
+            return true;
         }
         return false;
     }

src/math/polysat/forbidden_intervals.h

@@ -14,11 +14,12 @@ Author:
 
 --*/
 #pragma once
-#include "math/polysat/constraint.h"
+#include "math/polysat/conflict.h"
-#include "math/polysat/solver.h"
 
 namespace polysat {
 
+    class solver;
+
     class forbidden_intervals {
         solver& s;
         void revert_core(conflict& core);

src/math/polysat/saturation.cpp

@@ -367,7 +367,7 @@ namespace polysat {
     /// [z] z <= y' /\ zx > yx  ==>  Ω*(x,y') \/ y'x > yx
     /// [z] z <= y' /\ yx <= zx  ==>  Ω*(x,y') \/ yx <= y'x
     bool inf_saturate::try_ugt_z(pvar z, conflict& core, inequality const& yx_l_zx) {
-        set_rule("[z] z <= y' /\ zx > yx");
+        set_rule("[z] z <= y' && zx > yx");
         pdd y = s.var(z);
         pdd x = y;
         if (!is_YX_l_zX(z, yx_l_zx, x, y))

src/math/polysat/solver.cpp

@@ -19,7 +19,6 @@ Author:
 #include "math/polysat/solver.h"
 #include "math/polysat/explain.h"
 #include "math/polysat/log.h"
-#include "math/polysat/forbidden_intervals.h"
 #include "math/polysat/variable_elimination.h"
 
 // For development; to be removed once the linear solver works well enough
@@ -39,6 +38,7 @@ namespace polysat {
         m_viable(*this),
         m_linear_solver(*this),
         m_conflict(*this),
+        m_forbidden_intervals(*this),
         m_bvars(),
         m_free_pvars(m_activity),
         m_constraints(m_bvars) {

src/math/polysat/solver.h

@@ -29,6 +29,7 @@ Author:
 #include "math/polysat/justification.h"
 #include "math/polysat/linear_solver.h"
 #include "math/polysat/search_state.h"
+#include "math/polysat/forbidden_intervals.h"
 #include "math/polysat/trail.h"
 #include "math/polysat/viable.h"
 #include "math/polysat/log.h"
@@ -71,6 +72,7 @@ namespace polysat {
         scoped_ptr_vector<dd::pdd_manager> m_pdd;
         linear_solver            m_linear_solver;
         conflict                 m_conflict;        
+        forbidden_intervals      m_forbidden_intervals;
         bool_var_manager         m_bvars;       // Map boolean variables to constraints
         var_queue                m_free_pvars;  // free poly vars
         stats                    m_stats;

src/math/polysat/viable.h

@@ -168,8 +168,6 @@ namespace polysat {
          */
         bool has_viable(pvar v);
 
-        bool is_false(pvar v) { return !has_viable(v); }
-
         /**
          * check if value is viable according to m_viable.
          */