move to hide bits

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

src/ast/sls/bv_sls_eval.cpp

@@ -39,7 +39,8 @@ namespace bv {
                 if (bv.is_bv(e)) {
                     auto& v = wval0(e);
                     for (unsigned i = 0; i < v.bw; ++i)
-                        v.set_bit(i, eval(e, i));
+                        v.set(m_tmp, i, eval(e, i));
+                    v.set(m_tmp);
                 }
                 else if (m.is_bool(e))
                     m_eval.setx(e->get_id(), eval(e, 0), false);

src/ast/sls/sls_valuation.h

@@ -41,7 +41,7 @@ namespace bv {
 
         digit_t bits(unsigned i) const { return m_bits[i]; }
         svector<digit_t> const& bits() const { return m_bits; }
-        void set_bit(unsigned i, bool v) { set(m_bits, i, v); }
+
         bool get_bit(unsigned i) const { return get(m_bits, i); }
 
         void set_value(svector<digit_t>& bits, rational const& r);
@@ -228,6 +228,9 @@ namespace bv {
             return out;
         }
 
+        // TODO move:
+        void set_bit(unsigned i, bool v) { set(m_bits, i, v); }
+
     private:
         static digit_t get_pos_mask(unsigned bit_idx) {
             return (digit_t)1 << (digit_t)(bit_idx % (8 * sizeof(digit_t)));
@@ -246,6 +249,7 @@ namespace bv {
     public:
         sls_pre_valuation(unsigned bw):sls_valuation(bw) {}
         svector<digit_t>& bits() { return m_bits; }
+
     };
 
     inline std::ostream& operator<<(std::ostream& out, sls_valuation const& v) { return v.display(out); }