update python build dependencies

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

scripts/mk_project.py

@@ -59,7 +59,7 @@ def init_project_def():
     add_lib('proto_model', ['model', 'rewriter', 'smt_params'], 'smt/proto_model')
     add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model', 'solver_assertions',
                     'substitution', 'grobner', 'simplex', 'proofs', 'pattern', 'parser_util', 'fpa', 'lp'])
-    add_lib('sat_smt', ['sat', 'euf', 'smt', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'mbp', 'normal_forms', 'lp', 'pattern', 'qe_lite'], 'sat/smt')
+    add_lib('sat_smt', ['sat', 'ast_sls', 'euf', 'smt', 'tactic', 'solver', 'smt_params', 'bit_blaster', 'fpa', 'mbp', 'normal_forms', 'lp', 'pattern', 'qe_lite'], 'sat/smt')
     add_lib('sat_tactic', ['tactic', 'sat', 'solver', 'sat_smt'], 'sat/tactic')
     add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic')    
     add_lib('bv_tactics', ['tactic', 'bit_blaster', 'core_tactics'], 'tactic/bv')

src/ast/sls/bv_sls_eval.cpp

@@ -983,6 +983,7 @@ namespace bv {
     bool sls_eval::try_repair_bxor(bvval const& e, bvval& a, bvval const& b) {
         for (unsigned i = 0; i < e.nw; ++i)
             m_tmp[i] = e.bits[i] ^ b.bits[i];
+        a.clear_overflow_bits(m_tmp);
         a.set_repair(random_bool(), m_tmp);
         return true;        
     }
@@ -1517,15 +1518,14 @@ namespace bv {
             for (unsigned i = 0; i < a.bw; ++i)
                 a.set(m_tmp, i, e.get(e.bits, i + b.bw));
             a.clear_overflow_bits(m_tmp);
-            a.set_repair(random_bool(), m_tmp);
+            return a.set_repair(random_bool(), m_tmp);
         }
         else {
             for (unsigned i = 0; i < b.bw; ++i)
                 b.set(m_tmp, i, e.get(e.bits, i));
             b.clear_overflow_bits(m_tmp);
-            b.set_repair(random_bool(), m_tmp);
+            return b.set_repair(random_bool(), m_tmp);
         }
-        return true;
     }
 
     bool sls_eval::try_repair_extract(bvval const& e, bvval& a, unsigned lo) {

src/ast/sls/sls_valuation.cpp

@@ -24,7 +24,6 @@ namespace bv {
 
     sls_valuation::sls_valuation(unsigned bw): bw(bw) {
         nw = (bw + sizeof(digit_t) * 8 - 1) / (8 * sizeof(digit_t));
-        unsigned num_bytes = nw * sizeof(digit_t);
         lo.reserve(nw + 1);
         hi.reserve(nw + 1);
         bits.reserve(nw + 1);
@@ -192,14 +191,17 @@ namespace bv {
         return true;
     }
 
-    void sls_valuation::set_repair(bool try_down, svector<digit_t>& dst) {
+    bool sls_valuation::set_repair(bool try_down, svector<digit_t>& dst) {
         for (unsigned i = 0; i < nw; ++i)
             dst[i] = (~fixed[i] & dst[i]) | (fixed[i] & bits[i]);
         bool ok = try_down ? round_down(dst) : round_up(dst);
         if (!ok)
             VERIFY(try_down ? round_up(dst) : round_down(dst));
+        if (eq(bits, dst))
+            return false;
         set(bits, dst);
         SASSERT(!has_overflow(dst));
+        return true;
     }
 
     void sls_valuation::min_feasible(svector<digit_t>& out) const {
@@ -294,8 +296,6 @@ namespace bv {
 
     void sls_valuation::shift_right(svector<digit_t>& out, unsigned shift) const {
         SASSERT(shift < bw);
-        unsigned n = shift / (8 * sizeof(digit_t));
-        unsigned s = shift % (8 * sizeof(digit_t));
         for (unsigned i = 0; i < bw; ++i)
             set(out, i, i + shift < bw ? get(bits, i + shift) : false);
         SASSERT(!has_overflow(out));

src/ast/sls/sls_valuation.h

@@ -66,7 +66,7 @@ namespace bv {
         bool is_ones(svector<digit_t> const& a) const {
             auto bound = bw % (sizeof(digit_t) * 8) == 0 ? nw : nw - 1;
             for (unsigned i = 0; i < bound; ++i)
-                if (a[i] != ~0)
+                if (a[i] != (a[i] ^ 0))
                     return false;
             if (bound < nw) {
                 for (unsigned i = bound * sizeof(digit_t) * 8; i < bw; ++i)
@@ -116,7 +116,7 @@ namespace bv {
         bool get_at_least(svector<digit_t> const& src, svector<digit_t>& dst) const;
         bool round_up(svector<digit_t>& dst) const;
         bool round_down(svector<digit_t>& dst) const;
-        void set_repair(bool try_down, svector<digit_t>& dst);
+        bool set_repair(bool try_down, svector<digit_t>& dst);
 
         bool try_set(svector<digit_t> const& src) {
             if (!can_set(src))