remove add_non_viable

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

src/math/polysat/viable.cpp

@@ -90,13 +90,6 @@ namespace polysat {
         return var2bits(v).contains(m_viable[v], val);
     }
 
-    void viable::add_non_viable(pvar v, rational const& val) {
-        LOG("pvar " << v << " /= " << val);
-        SASSERT(is_viable(v, val));
-        auto const& bits = var2bits(v);
-        intersect_viable(v, bits.var() != val);
-    }
-
     void viable::intersect_viable(pvar v, bdd vals) {
         push_viable(v);
         m_viable[v] &= vals;

src/math/polysat/viable.h

@@ -86,11 +86,6 @@ namespace polysat {
          */
         bool is_viable(pvar v, rational const& val);
 
-        /**
-         * register that val is non-viable for var.
-         */
-        void add_non_viable(pvar v, rational const& val);
-
         /*
         * Extract min and max viable values for v
         */

src/math/polysat/viable2.cpp

@@ -170,17 +170,6 @@ namespace polysat {
         return true; 
     }
 
-    void viable2::add_non_viable(pvar v, rational const& lo_val, signed_constraint const& c) { 
-        entry* ne = alloc_entry();
-        rational const& max_value = s.var2pdd(v).max_value();
-        rational hi_val = (lo_val == max_value) ? rational::zero() : lo_val + 1;
-        pdd lo = s.var2pdd(v).mk_val(lo_val);
-        pdd hi = s.var2pdd(v).mk_val(hi_val);
-        ne->interval = eval_interval::proper(lo, lo_val, hi, hi_val); 
-        ne->src = c;     
-        intersect(v, ne);
-    }
-
     rational viable2::min_viable(pvar v) { 
         rational lo(0);
         auto* e = m_viable[v];

src/math/polysat/viable2.h

@@ -83,11 +83,6 @@ namespace polysat {
          */
         bool is_viable(pvar v, rational const& val);
 
-        /**
-         * register that val is non-viable for var.
-         */
-        void add_non_viable(pvar v, rational const& val, signed_constraint const& c);
-
         /*
         * Extract min and max viable values for v
         */