Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt

src/ackermannization/ackr_model_converter.cpp

@@ -39,6 +39,8 @@ public:
 
     virtual ~ackr_model_converter() { }
 
+    virtual void get_units(obj_map<expr, bool>& units) { units.reset(); }
+
     virtual void operator()(model_ref & md, unsigned goal_idx) {
         SASSERT(goal_idx == 0);
         SASSERT(!fixed_model || md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions()));

src/ackermannization/lackr_model_converter_lazy.cpp

@@ -43,6 +43,8 @@ public:
         operator()(md, 0);
     }
 
+    virtual void get_units(obj_map<expr, bool>& units) { units.reset(); }
+
     //void display(std::ostream & out);
 
     virtual model_converter * translate(ast_translation & translator) {

src/api/api_solver.cpp

@@ -347,6 +347,22 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+
+    Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s) {
+        Z3_TRY;
+        LOG_Z3_solver_get_units(c, s);
+        RESET_ERROR_CODE();
+        init_solver(c, s);
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
+        mk_c(c)->save_object(v);
+        expr_ref_vector fmls = to_solver_ref(s)->get_units(mk_c(c)->m());
+        for (expr* f : fmls) {
+            v->m_ast_vector.push_back(f);
+        }
+        RETURN_Z3(of_ast_vector(v));
+        Z3_CATCH_RETURN(0);
+    }
+
     static Z3_lbool _solver_check(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) {
         for (unsigned i = 0; i < num_assumptions; i++) {
             if (!is_expr(to_ast(assumptions[i]))) {

src/api/dotnet/Solver.cs

@@ -265,6 +265,20 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Currently inferred units.
+        /// </summary>
+        public BoolExpr[] Units
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
+
+                ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_units(Context.nCtx, NativeObject));
+                return assertions.ToBoolExprArray();
+            }
+        }
+
         /// <summary>
         /// Checks whether the assertions in the solver are consistent or not.
         /// </summary>

src/api/python/z3/z3.py

@@ -6369,6 +6369,11 @@ class Solver(Z3PPObject):
         """
         return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
 
+    def units(self):
+        """Return an AST vector containing all currently inferred units.
+        """
+        return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
+
     def statistics(self):
         """Return statistics for the last `check()`.
 

src/api/z3_api.h

@@ -6163,6 +6163,13 @@ extern "C" {
     */
     Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s);
 
+    /**
+       \brief Return the set of units modulo model conversion.
+
+       def_API('Z3_solver_get_units', AST_VECTOR, (_in(CONTEXT), _in(SOLVER)))
+    */
+    Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s);
+
     /**
        \brief Check whether the assertions in a given solver are consistent or not.
 

src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp

@@ -181,6 +181,17 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
         }
     }
 
+    unsigned m_keypos;
+
+    void start_rewrite() {
+        m_keypos = m_keys.size();
+    }
+    void end_rewrite(obj_map<func_decl, expr*>& const2bits) {
+        for (unsigned i = m_keypos; i < m_keys.size(); ++i) {
+            const2bits.insert(m_keys[i].get(), m_values[i].get());
+        }
+    }
+
     template<typename V>
     app * mk_mkbv(V const & bits) {
         return m().mk_app(butil().get_family_id(), OP_MKBV, bits.size(), bits.c_ptr());
@@ -635,6 +646,8 @@ struct bit_blaster_rewriter::imp : public rewriter_tpl<blaster_rewriter_cfg> {
     }
     void push() { m_cfg.push(); }
     void pop(unsigned s) { m_cfg.pop(s); }
+    void start_rewrite() { m_cfg.start_rewrite(); }
+    void end_rewrite(obj_map<func_decl, expr*>& const2bits) { m_cfg.end_rewrite(const2bits); }
     unsigned get_num_scopes() const { return m_cfg.get_num_scopes(); }
 };
 
@@ -683,3 +696,10 @@ unsigned bit_blaster_rewriter::get_num_scopes() const {
     return m_imp->get_num_scopes();
 }
 
+void bit_blaster_rewriter::start_rewrite() {
+    m_imp->start_rewrite();
+}
+
+void bit_blaster_rewriter::end_rewrite(obj_map<func_decl, expr*>& const2bits) {
+    m_imp->end_rewrite(const2bits);
+}

src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h

@@ -33,7 +33,9 @@ public:
     ast_manager & m() const;
     unsigned get_num_steps() const;
     void cleanup();
-    obj_map<func_decl, expr*> const& const2bits() const; 
+    obj_map<func_decl, expr*> const& const2bits() const;     
+    void start_rewrite();
+    void end_rewrite(obj_map<func_decl, expr*>& const2bits);
     void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
     void push();
     void pop(unsigned num_scopes);

src/muz/base/dl_util.cpp

@@ -387,6 +387,9 @@ namespace datalog {
         void operator()(model_ref&) override {}
 
         void display(std::ostream & out) override { }
+
+        void get_units(obj_map<expr, bool>& units) override {}
+
     };
 
     model_converter* mk_skip_model_converter() { return alloc(skip_model_converter); }

src/muz/transforms/dl_mk_bit_blast.cpp

@@ -63,6 +63,8 @@ namespace datalog {
             return alloc(bit_blast_model_converter, m);
         }
 
+        virtual void get_units(obj_map<expr, bool>& units)  {}
+
         virtual void display(std::ostream& out) { out << "(bit-blast-model-converter)\n"; }
 
         virtual void operator()(model_ref & model) {

src/muz/transforms/dl_mk_karr_invariants.cpp

@@ -120,6 +120,8 @@ namespace datalog {
             }
         }
 
+        virtual void get_units(obj_map<expr, bool>& units) {}
+
         virtual void operator()(model_ref & mr) {
             for (unsigned i = 0; i < m_funcs.size(); ++i) {
                 func_decl* p = m_funcs[i].get();

src/muz/transforms/dl_mk_quantifier_abstraction.cpp

@@ -55,6 +55,8 @@ namespace datalog {
 
         virtual void display(std::ostream& out) { display_add(out, m); }
 
+        virtual void get_units(obj_map<expr, bool>& units) { units.reset(); }        
+
         void insert(func_decl* old_p, func_decl* new_p, expr_ref_vector& sub, sort_ref_vector& sorts, svector<bool> const& bound) {
             m_old_funcs.push_back(old_p);
             m_new_funcs.push_back(new_p);

src/muz/transforms/dl_mk_scale.cpp

@@ -38,13 +38,13 @@ namespace datalog {
             m_new2old.insert(new_f, old_f);
         }
        
+        virtual void get_units(obj_map<expr, bool>& units) { units.reset(); }
+
         virtual void operator()(model_ref& md) {
             model_ref old_model = alloc(model, m);
-            obj_map<func_decl, func_decl*>::iterator it  = m_new2old.begin();
+            for (auto const& kv : m_new2old) {
-            obj_map<func_decl, func_decl*>::iterator end = m_new2old.end();
+                func_decl* old_p = kv.m_value;
-            for (; it != end; ++it) {
+                func_decl* new_p = kv.m_key;
-                func_decl* old_p = it->m_value;
-                func_decl* new_p = it->m_key;
                 func_interp* old_fi = alloc(func_interp, m, old_p->get_arity());
 
                 if (new_p->get_arity() == 0) {

src/muz/transforms/dl_mk_slice.cpp

@@ -308,6 +308,8 @@ namespace datalog {
             m_sliceable.insert(f, bv);
         }
 
+        void get_units(obj_map<expr, bool>& units) override {}
+
         void operator()(model_ref & md) override {
             if (m_slice2old.empty()) {
                 return;

src/opt/opt_parse.cpp

@@ -670,6 +670,14 @@ private:
         return peek(pos) == "<=" || peek(pos) == "=<";
     }
 
+    bool peek_minus_infty(unsigned pos) {
+        return peek(pos) == "-" && (peek(pos+1) == "inf" || peek(pos+1) == "infinity");
+    }
+
+    bool peek_plus_infty(unsigned pos) {
+        return peek(pos) == "+" && (peek(pos+1) == "inf" || peek(pos+1) == "infinity");
+    }
+
     void parse_indicator(symbol& var, rational& val) {
         if (peek(1) == "=" && tok.peek_num(2) && peek(3) == "->") {
             var = peek(0);
@@ -703,11 +711,15 @@ private:
             v = peek(2);
             update_lower(lhs, v);
             tok.next(3);
-            if (peek_le(0) && tok.peek_num(1)) {
+            parse_upper(v);
-                rational rhs = tok.get_num(1);
+        }
-                update_upper(v, rhs);
+        else if (peek_minus_infty(0) && peek_le(2)) {
-                tok.next(2);
+            v = peek(3);
-            }
+            tok.next(4);
+            parse_upper(v);
+        }
+        else if (peek_plus_infty(2) && peek_le(1)) {
+            tok.next(4);            
         }
         else if (peek_le(1) && tok.peek_num(2)) {
             v = peek(0);
@@ -721,6 +733,18 @@ private:
         }
     }
 
+    void parse_upper(symbol const& v) {
+        if (peek_le(0) && tok.peek_num(1)) {
+            rational rhs = tok.get_num(1);
+            update_upper(v, rhs);
+            tok.next(2);
+        }
+        else if (peek_le(0) && peek_plus_infty(1)) {
+            tok.next(3);            
+        }
+
+    }
+
     void update_lower(rational const& r, symbol const& v) {
         bound b;
         m_bounds.find(v, b);

src/sat/ba_solver.cpp

@@ -47,16 +47,6 @@ namespace sat {
         return static_cast<pb const&>(*this);
     }
 
-    ba_solver::eq& ba_solver::constraint::to_eq() {
-        SASSERT(is_eq());
-        return static_cast<eq&>(*this);
-    }
-
-    ba_solver::eq const& ba_solver::constraint::to_eq() const{
-        SASSERT(is_eq());
-        return static_cast<eq const&>(*this);
-    }
-
     ba_solver::xr& ba_solver::constraint::to_xr() {
         SASSERT(is_xr());
         return static_cast<xr&>(*this);
@@ -95,15 +85,6 @@ namespace sat {
             }            
             break;
         }
-        case ba_solver::eq_t: {
-            ba_solver::eq const& e = cnstr.to_eq();
-            for (ba_solver::eliteral wl : e) {
-                if (wl.weight != 1) out << wl.weight << " * ";
-                out << wl.lit << " ";
-            }
-            out << " = " << e.k();
-            break;
-        }
         default:
             UNREACHABLE();
         }
@@ -205,33 +186,6 @@ namespace sat {
     }
 
 
-    // -----------------------------------
-    // eq
-
-    ba_solver::eq::eq(unsigned id, literal lit, svector<ba_solver::wliteral> const& wlits, unsigned k):
-        constraint(eq_t, id, lit, wlits.size(), eq::get_obj_size(wlits.size())),
-        m_lo(0),
-        m_hi(0),
-        m_max(0),        
-        m_k(k)        
-    {
-        unsigned i = 0;        
-        for (wliteral const& w : wlits) {
-            m_wlits[i++] = eliteral(w.first, w.second);
-            m_max += w.first;
-        }
-        m_hi = m_max;
-        m_trail_sz = 0;
-    }
-
-    unsigned ba_solver::eq::index(literal l) const {
-        for (unsigned i = 0; i < size(); ++i) {
-            if (l.var() == m_wlits[i].lit.var()) return i;
-        }
-        UNREACHABLE();
-        return UINT_MAX;
-    }
-
     // -----------------------------------
     // xr
     
@@ -271,7 +225,7 @@ namespace sat {
         }
         if (root != null_literal) {
             if (!is_watched(root, c)) watch_literal(root, c);
-            if (!is_watched(~root, c)) watch_literal(~root, c);
+            if (!c.is_pure() && !is_watched(~root, c)) watch_literal(~root, c);
         }
         TRACE("ba", display(tout << "init watch: ", c, true););
         SASSERT(root == null_literal || value(root) == l_true);
@@ -925,251 +879,6 @@ namespace sat {
         out << ">= " << p.k()  << "\n";
     }
 
-    // --------------------
-    // eq:
-
-    ba_solver::constraint* ba_solver::add_eq(literal lit, svector<wliteral> const& wlits, unsigned k, bool learned) {
-        void * mem = m_allocator.allocate(eq::get_obj_size(wlits.size()));
-        eq* e = new (mem) eq(next_id(), lit, wlits, k);
-        e->set_learned(learned);
-        add_constraint(e);
-        for (eliteral const& wl : *e) {
-            watch_literal(wl.lit, *e);
-            watch_literal(~(wl.lit), *e);
-        }        
-        return e;
-    }
-
-    void ba_solver::display(std::ostream& out, eq const& e, bool values) const {
-        display_lit(out, e.lit(), e.size(), values);
-        if (values) {
-            if (e.trail_sz() > 0) {
-                out << "trail: ";
-                for (unsigned i = 0; i < e.trail_sz(); ++i) {
-                    out << e[i].tweight << " * " << e[i].tlit << " ";
-                }
-            }
-            out << "[" << e.lo() << ":" << e.hi() << "] ";
-        }
-        for (eliteral wl : e) {
-            literal l = wl.lit;
-            unsigned w = wl.weight;
-            if (w > 1) out << w << " * ";
-            out << l;
-            if (values) {
-                out << "@(" << value(l);
-                if (value(l) != l_undef) {
-                    out << ":" << lvl(l);
-                }
-                out << ") ";
-            }
-            else {
-                out << " ";
-            }
-        }
-        out << "= " << e.k()  << "\n";
-    }
-
-    bool ba_solver::init_watch(eq& e) {
-        return true;
-    }
-
-    void ba_solver::clear_watch(eq& e) {
-        for (eliteral const& wl : e) {
-            unwatch_literal(wl.lit, e);
-            unwatch_literal(~(wl.lit), e);
-        }
-        if (e.lit() != null_literal) {
-            unwatch_literal(e.lit(), e);
-            unwatch_literal(~e.lit(), e);
-        }
-    }
-
-    /*
-     * \update the bounds for [lo,hi] based on what is unassigned on the trail.
-     */
-    void ba_solver::pop_eq(eq& e) {
-        unsigned idx = e.trail_sz() - 1;
-        literal tlit = e[idx].tlit;
-        if (tlit.sign()) {
-            e.inc_hi(e[idx].tweight);
-        }
-        else {
-            e.dec_lo(e[idx].tweight);
-        }
-        e.set_trail_sz(idx);
-    }
-
-    lbool ba_solver::add_assign(eq& e, literal nl) {
-        //IF_VERBOSE(0, verbose_stream() << nl << "@" << lvl(nl) << ": " << e << "\n");
-        SASSERT(value(nl) == l_false);
-        if (nl.var() == e.lit().var()) {
-            // no-op
-        }
-        else {
-            unsigned i = e.index(nl);
-            eliteral wl = e[i];
-            if (wl.lit == nl) {
-                e.dec_hi(wl);
-            }
-            else {
-                SASSERT(wl.lit == ~nl);
-                e.inc_lo(wl);
-            }
-            m_eq_to_pop.push_back(&e);
-        }
-        if (e.lo() > e.k() || e.hi() < e.k()) {
-            if (e.lit() == null_literal || value(e.lit()) == l_true) {
-                set_conflict(e, nl);
-                return l_false;
-            }
-            if (e.lit() != null_literal && value(e.lit()) == l_undef) {
-                assign(e, ~e.lit());
-            }
-        }
-        else if (e.lo() == e.hi()) {
-            SASSERT(e.lo() == e.k());
-            if (e.lit() != null_literal && value(e.lit()) == l_false) {
-                set_conflict(e, nl);
-                return l_false;
-            }
-            if (e.lit() != null_literal && value(e.lit()) == l_undef) {
-                assign(e, e.lit());
-            }
-        }
-        else if ((e.lit() == null_literal || value(e.lit()) == l_true)) {
-            if (e.lo() == e.k()) {
-                for (eliteral el : e) {
-                    if (value(el.lit) == l_undef) {
-                        //IF_VERBOSE(0, display(verbose_stream() << "proapgate " << ~el.lit << " ", e, true));
-                        assign(e, ~el.lit);
-                    }
-                }
-            }
-            else if (e.hi() == e.k()) {
-                for (eliteral el : e) {
-                    if (value(el.lit) == l_undef) {
-                        //IF_VERBOSE(0, display(verbose_stream() << "proapgate " << el.lit << " ", e, true));
-                        assign(e, el.lit);
-                    }
-                }
-            }
-        }
-        return l_true;
-    }
-
-    void ba_solver::simplify(eq& e) {
-        // no-op for now
-    }
-
-    void ba_solver::recompile(eq& e) {
-        for (eliteral const& el : e) {
-            m_weights[el.lit.index()] += el.weight;
-        }
-        unsigned k = e.k(), sz = e.size();
-        unsigned j = 0;
-        bool is_false = false;
-        for (unsigned i = 0; i < sz; ++i) {
-            eliteral el = e[i];
-            unsigned w1 = m_weights[el.lit.index()];
-            unsigned w2 = m_weights[(~el.lit).index()];
-            if (w1 == 0 || w1 < w2) continue;
-            if (k < w2) {
-                is_false = true;
-                break;
-            }            
-            k  -= w2;
-            w1 -= w2;
-            if (w1 == 0) continue;            
-            e[j++] = eliteral(w1, el.lit);            
-        }
-        sz = j;
-        for (eliteral const& el : e) {
-            m_weights[el.lit.index()] = 0;
-            m_weights[(~el.lit).index()] = 0;
-        }        
-        if (is_false) {
-            if (e.lit() == null_literal) {
-                s().mk_clause(0, 0, true);
-            }
-            else {
-                literal lit = ~e.lit();
-                s().mk_clause(1, &lit, true);
-            }
-            remove_constraint(e, "recompiled to false");
-            return;
-        }
-        // update trail
-        e.set_size(sz);
-        e.set_k(k);
-        for (unsigned i = 0; i < sz; ++i) {
-            e[i].tlit = null_literal;
-        }                
-        e.set_trail_sz(0);
-        e.reset_lo();
-        e.reset_hi();
-        for (eliteral const& el : e) {            
-            switch (value(el.lit)) {
-            case l_true:  e.inc_lo(el); break;
-            case l_false: e.dec_hi(el); break;
-            default: break;
-            }
-        }
-    }
-
-    void ba_solver::split_root(eq& e) {
-        NOT_IMPLEMENTED_YET();
-    }
-
-    void ba_solver::get_antecedents(literal l, eq const& e, literal_vector& r) {
-        for (eliteral wl : e) {
-            if (wl.lit.var() == l.var()) continue;
-            switch (value(wl.lit)) {
-            case l_true: r.push_back(wl.lit); break;
-            case l_false: r.push_back(~wl.lit); break;
-            default: break;
-            }
-        }
-        if (e.lit() != null_literal && l.var() != e.lit().var()) {
-            switch (value(e.lit())) {
-            case l_true: r.push_back(e.lit()); break;
-            case l_false: r.push_back(~e.lit()); break;
-            default: break;
-            }            
-        }
-    }
-
-    lbool ba_solver::eval(eq const& e) const {
-        unsigned trues = 0, undefs = 0;
-        for (eliteral wl : e) {
-            switch (value(wl.lit)) {
-            case l_true: trues += wl.weight; break;
-            case l_undef: undefs += wl.weight; break;
-            default: break;
-            }
-        }
-        if (trues + undefs < e.k()) return l_false;
-        if (trues > e.k()) return l_false;
-        if (trues == e.k() && undefs == 0) return l_true;
-        return l_undef;        
-    }
-
-    lbool ba_solver::eval(model const& m, eq const& e) const {
-        unsigned trues = 0, undefs = 0;
-        for (eliteral wl : e) {
-            switch (value(m, wl.lit)) {
-            case l_true: trues += wl.weight; break;
-            case l_undef: undefs += wl.weight; break;
-            default: break;
-            }
-        }
-        if (trues + undefs < e.k()) return l_false;
-        if (trues > e.k()) return l_false;
-        if (trues == e.k() && undefs == 0) return l_true;
-        return l_undef;        
-    }
-
-
     // --------------------
     // xr:
 
@@ -1512,17 +1221,6 @@ namespace sat {
                     for (literal l : m_lemma) process_antecedent(~l, offset);
                     break;
                 }
-                case eq_t: {
-                    eq& e = cnstr.to_eq();
-                    m_lemma.reset();
-                    inc_bound(offset);
-                    inc_coeff(consequent, offset);
-                    get_antecedents(consequent, e, m_lemma);
-                    TRACE("ba", display(tout, e, true); tout << m_lemma << "\n";);
-                    for (literal l : m_lemma) process_antecedent(~l, offset);
-                    break;
-
-                }
                 default:
                     UNREACHABLE();
                     break;
@@ -1888,7 +1586,6 @@ namespace sat {
         case card_t: return init_watch(c.to_card()); 
         case pb_t: return init_watch(c.to_pb());
         case xr_t: return init_watch(c.to_xr()); 
-        case eq_t: return init_watch(c.to_eq());
         }
         UNREACHABLE();
         return false;
@@ -1899,7 +1596,6 @@ namespace sat {
         case card_t: return add_assign(c.to_card(), l); 
         case pb_t: return add_assign(c.to_pb(), l); 
         case xr_t: return add_assign(c.to_xr(), l);
-        case eq_t: return add_assign(c.to_eq(), l);
         }
         UNREACHABLE();
         return l_undef;
@@ -1950,7 +1646,8 @@ namespace sat {
             init_watch(c);
             return true;
         }
-        else if (c.lit() != null_literal && value(c.lit()) != l_true && c.tag() != eq_t) {
+        else if (c.lit() != null_literal && value(c.lit()) != l_true) {
+        // else if (c.lit() != null_literal && value(c.lit()) == l_false) {
             return true;
         }
         else {
@@ -2005,7 +1702,6 @@ namespace sat {
         case card_t: return get_reward(c.to_card(), occs);
         case pb_t: return get_reward(c.to_pb(), occs); 
         case xr_t: return 0;
-        case eq_t: return 1;
         default: UNREACHABLE(); return 0;
         }
     }
@@ -2259,6 +1955,13 @@ namespace sat {
     }
 
     void ba_solver::get_antecedents(literal l, card const& c, literal_vector& r) {
+        if (l == ~c.lit()) {
+            for (unsigned i = c.k() - 1; i < c.size(); ++i) {
+                VERIFY(value(c[i]) == l_false);
+                r.push_back(~c[i]);
+            }   
+            return;
+        }
         DEBUG_CODE(
             bool found = false;
             for (unsigned i = 0; !found && i < c.k(); ++i) {
@@ -2267,7 +1970,7 @@ namespace sat {
             SASSERT(found););
         
         // IF_VERBOSE(0, if (_debug_conflict) verbose_stream() << "ante " << l << " " << c << "\n");
-        SASSERT(c.lit() == null_literal || value(c.lit()) != l_false);
+        VERIFY(c.lit() == null_literal || value(c.lit()) != l_false);
         if (c.lit() != null_literal) r.push_back(value(c.lit()) == l_true ? c.lit() : ~c.lit());
         for (unsigned i = c.k(); i < c.size(); ++i) {
             SASSERT(value(c[i]) == l_false);
@@ -2310,6 +2013,7 @@ namespace sat {
     }
 
     void ba_solver::watch_literal(literal lit, constraint& c) {
+        if (c.is_pure() && lit == ~c.lit()) return;
         get_wlist(~lit).push_back(watched(c.index()));
     }
 
@@ -2318,7 +2022,6 @@ namespace sat {
         case card_t: get_antecedents(l, c.to_card(), r); break;
         case pb_t: get_antecedents(l, c.to_pb(), r); break;
         case xr_t: get_antecedents(l, c.to_xr(), r); break;
-        case eq_t: get_antecedents(l, c.to_eq(), r); break;
         default: UNREACHABLE(); break;
         }
     }
@@ -2342,9 +2045,6 @@ namespace sat {
         case xr_t:
             clear_watch(c.to_xr());
             break;
-        case eq_t:
-            clear_watch(c.to_eq());
-            break;
         default:
             UNREACHABLE();
         }
@@ -2367,7 +2067,6 @@ namespace sat {
         case card_t:  return validate_unit_propagation(c.to_card(), l); 
         case pb_t: return validate_unit_propagation(c.to_pb(), l);
         case xr_t: return true;
-        case eq_t: return validate_unit_propagation(c.to_eq(), l);
         default: UNREACHABLE(); break;
         }
         return false;
@@ -2383,7 +2082,6 @@ namespace sat {
         case card_t: return eval(v1, eval(c.to_card())); 
         case pb_t:   return eval(v1, eval(c.to_pb()));
         case xr_t:  return eval(v1, eval(c.to_xr()));
-        case eq_t:  return eval(v1, eval(c.to_eq()));
         default: UNREACHABLE(); break;
         }
         return l_undef;        
@@ -2395,7 +2093,6 @@ namespace sat {
         case card_t: return eval(v1, eval(m, c.to_card())); 
         case pb_t:   return eval(v1, eval(m, c.to_pb()));
         case xr_t:   return eval(v1, eval(m, c.to_xr()));
-        case eq_t:   return eval(v1, eval(m, c.to_eq()));
         default: UNREACHABLE(); break;
         }
         return l_undef;        
@@ -2660,7 +2357,7 @@ namespace sat {
             return l_false;
         }
         SASSERT(value(alit) == l_false);
-        SASSERT(c.lit() == null_literal || value(c.lit()) == l_true);
+        VERIFY(c.lit() == null_literal || value(c.lit()) != l_false);
         unsigned index = 0;
         for (index = 0; index <= bound; ++index) {
             if (c[index] == alit) {
@@ -2688,6 +2385,7 @@ namespace sat {
         if (bound != index && value(c[bound]) == l_false) {
             TRACE("ba", tout << "conflict " << c[bound] << " " << alit << "\n";);
             if (c.lit() != null_literal && value(c.lit()) == l_undef) {
+                if (index + 1 < bound) c.swap(index, bound - 1);
                 assign(c, ~c.lit());
                 return inconsistent() ? l_false : l_true;
             }
@@ -2695,14 +2393,15 @@ namespace sat {
             return l_false;
         }
 
+        if (index != bound) {
+            c.swap(index, bound);
+        }        
+
         // TRACE("ba", tout << "no swap " << index << " " << alit << "\n";);
         // there are no literals to swap with,
         // prepare for unit propagation by swapping the false literal into 
         // position bound. Then literals in positions 0..bound-1 have to be
         // assigned l_true.
-        if (index != bound) {
-            c.swap(index, bound);
-        }        
 
         if (c.lit() != null_literal && value(c.lit()) == l_undef) {
             return l_true;
@@ -2730,7 +2429,6 @@ namespace sat {
 
     void ba_solver::push() {
         m_constraint_to_reinit_lim.push_back(m_constraint_to_reinit.size());
-        m_eq_to_pop_lim.push_back(m_eq_to_pop.size());
     }
 
     void ba_solver::pop(unsigned n) {        
@@ -2739,13 +2437,6 @@ namespace sat {
         m_constraint_to_reinit_last_sz = m_constraint_to_reinit_lim[new_lim];
         m_constraint_to_reinit_lim.shrink(new_lim);
         m_num_propagations_since_pop = 0;
-
-        new_lim = m_eq_to_pop_lim.size() - n;
-        for (unsigned i = m_eq_to_pop_lim[new_lim]; i < m_eq_to_pop.size(); ++i) {
-            pop_eq(*m_eq_to_pop[i]);
-        }
-        m_eq_to_pop.shrink(m_eq_to_pop_lim[new_lim]);
-        m_eq_to_pop_lim.shrink(new_lim);
     }
 
     void ba_solver::pop_reinit() {
@@ -2772,9 +2463,6 @@ namespace sat {
         case xr_t:
             simplify(c.to_xr());
             break;
-        case eq_t:
-            simplify(c.to_eq());
-            break;
         default:
             UNREACHABLE();
         }                
@@ -2798,6 +2486,7 @@ namespace sat {
             for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]);
             cleanup_clauses();
             cleanup_constraints();
+            update_pure();
         }        
         while (m_simplify_change || trail_sz < s().init_trail_size());
 
@@ -2814,7 +2503,41 @@ namespace sat {
         // IF_VERBOSE(0, s().display(verbose_stream()));
         // mutex_reduction();
         // if (s().m_clauses.size() < 80000) lp_lookahead_reduction();
+    }
 
+    /*
+     * ~lit does not occur in clauses
+     * ~lit is only in one constraint use list
+     * lit == C 
+     * -> ignore assignemnts to ~lit for C
+     * 
+     * ~lit does not occur in clauses
+     * lit is only in one constraint use list
+     * lit == C
+     * -> negate: ~lit == ~C
+     */
+    void ba_solver::update_pure() {
+        // return;
+        for (constraint* cp : m_constraints) {
+            literal lit = cp->lit();
+            if (lit != null_literal && 
+                !cp->is_pure() &&
+                value(lit) == l_undef && 
+                get_wlist(~lit).size() == 1 &&                 
+                m_clause_use_list.get(lit).empty()) {
+                clear_watch(*cp);
+                cp->negate();
+                lit.neg();
+            }
+            if (lit != null_literal && 
+                !cp->is_pure() &&
+                m_cnstr_use_list[(~lit).index()].size() == 1 &&
+                get_wlist(lit).size() == 1 && 
+                m_clause_use_list.get(~lit).empty()) { 
+                cp->set_pure();
+                get_wlist(~lit).erase(watched(cp->index())); // just ignore assignments to false
+            }
+        }
     }
 
     void ba_solver::mutex_reduction() {
@@ -2930,9 +2653,6 @@ namespace sat {
         case pb_t:
             recompile(c.to_pb());
             break;
-        case eq_t:
-            recompile(c.to_eq());
-            break;            
         case xr_t:
             NOT_IMPLEMENTED_YET();
             break;
@@ -3144,7 +2864,6 @@ namespace sat {
         case card_t: split_root(c.to_card()); break;
         case pb_t: split_root(c.to_pb()); break;
         case xr_t: NOT_IMPLEMENTED_YET(); break;
-        case eq_t: split_root(c.to_eq()); break;
         }
     }
 
@@ -3265,15 +2984,6 @@ namespace sat {
                 }             
                 break;
             }
-            case eq_t: {
-                eq& e = cp->to_eq();
-                for (eliteral wl : e) {
-                    literal l = wl.lit;
-                    m_cnstr_use_list[l.index()].push_back(&e);
-                    m_cnstr_use_list[(~l).index()].push_back(&e);
-                }
-                break;
-            }
             }
         }
     }
@@ -3296,8 +3006,6 @@ namespace sat {
                 }
                 break;
             }
-            case eq_t: 
-                break;
             default:
                 break;
             }
@@ -3372,8 +3080,6 @@ namespace sat {
             if (p.k() > 1) subsumption(p);
             break;
         }
-        case eq_t: 
-            break;
         default:
             break;                
         }
@@ -3464,30 +3170,32 @@ namespace sat {
         return c1_exclusive + c2.k() + comp.size() <= c1.k();
     }
 
-    bool ba_solver::subsumes(card& c1, clause& c2, literal_vector & comp) {
+    /*
-        unsigned c2_exclusive = 0;
+      \brief L + A >= k subsumes L + C if |A| < k
-        unsigned common = 0;
+             A + L + B >= k self-subsumes A + ~L + C >= 1
-        comp.reset();
+             if k + 1 - |B| - |C| - |L| > 0
+     */
+    bool ba_solver::subsumes(card& c1, clause& c2, bool& self) {
+        unsigned common = 0, complement = 0, c2_exclusive = 0;
+        self = false;
+        
         for (literal l : c2) {
             if (is_marked(l)) {
                 ++common;
             }
             else if (is_marked(~l)) {
-                comp.push_back(l);
+                ++complement;
             }
             else {
                 ++c2_exclusive;
             }
         }
-
+        unsigned c1_exclusive = c1.size() - common - complement;
-        unsigned c1_exclusive = c1.size() - common - comp.size();
+        if (complement > 0 && c1.k() + 1 > c1_exclusive + c2_exclusive + common) {
-        bool result = c1_exclusive + 1 <= c1.k();
+            self = true;
-
+            return true; 
-        if (!comp.empty() && result) {
-            IF_VERBOSE(10, verbose_stream() << "self-subsume clause " << c2 << " is TBD\n";);
-            return false;
         }
-        return result;
+        return c1.size() - common < c1.k();
     }
 
     /*
@@ -3517,8 +3225,6 @@ namespace sat {
             case pb_t: 
                 s = subsumes(p1, c->to_pb()); 
                 break;
-            case eq_t:
-                break;
             default: 
                 break;
             }
@@ -3582,23 +3288,22 @@ namespace sat {
 
     void ba_solver::clause_subsumption(card& c1, literal lit, clause_vector& removed_clauses) {
         SASSERT(!c1.was_removed());
-        literal_vector slit;
+        clause_use_list& occurs = m_clause_use_list.get(lit);
-        clause_use_list::iterator it = m_clause_use_list.get(lit).mk_iterator();
+        clause_use_list::iterator it = occurs.mk_iterator();
         while (!it.at_end()) {
             clause& c2 = it.curr();
-            if (!c2.was_removed() && subsumes(c1, c2, slit)) {
+            bool self;
-                if (slit.empty()) {
+            if (!c2.was_removed() && subsumes(c1, c2, self)) {
+                if (self) {
+                    // self-subsumption is TBD
+                }
+                else {
                     TRACE("ba", tout << "remove\n" << c1 << "\n" << c2 << "\n";);
                     removed_clauses.push_back(&c2);
                     ++m_stats.m_num_clause_subsumes;
                     c1.set_learned(false);
-                }
+                }            
-                else {
+            }
-                    IF_VERBOSE(11, verbose_stream() << "self-subsume clause is TBD\n";);
-                    // remove literal slit from c2.
-                    TRACE("ba", tout << "TBD remove literals " << slit << " from " << c2 << "\n";);
-                }
-            }            
             it.next();
         }
     }
@@ -3615,7 +3320,7 @@ namespace sat {
             watched w = *it;
             if (w.is_binary_clause() && is_marked(w.get_literal())) {
                 ++m_stats.m_num_bin_subsumes;
-                // IF_VERBOSE(10, verbose_stream() << c1 << " subsumes (" << lit << " " << w.get_literal() << ")\n";);
+                IF_VERBOSE(10, verbose_stream() << c1 << " subsumes (" << lit << " " << w.get_literal() << ")\n";);
                 if (!w.is_learned()) {
                     c1.set_learned(false);
                 }
@@ -3745,15 +3450,6 @@ namespace sat {
                 result->add_xr(lits, x.learned());        
                 break;
             }
-            case eq_t: {
-                eq const& e = cp->to_eq();
-                wlits.reset();
-                for (eliteral w : e) {
-                    wlits.push_back(wliteral(w.weight, w.lit));
-                }
-                result->add_eq(e.lit(), wlits, e.k(), e.learned());
-                break;
-            }
             default:
                 UNREACHABLE();
             }                
@@ -3791,14 +3487,6 @@ namespace sat {
                 }
                 break;
             }
-            case eq_t: {
-                eq const& e = cp->to_eq();
-                for (eliteral w : e) {
-                    ul.insert(w.lit, idx);
-                    ul.insert(~(w.lit), idx);
-                }
-                break;
-            }
             default:
                 UNREACHABLE();
             }                            
@@ -3840,8 +3528,6 @@ namespace sat {
             }
             return weight >= p.k();
         }
-        case eq_t:
-            break;
         default:
             break;
         }
@@ -3963,7 +3649,6 @@ namespace sat {
         case card_t: display(out, c.to_card(), values); break;
         case pb_t: display(out, c.to_pb(), values); break;
         case xr_t: display(out, c.to_xr(), values); break;
-        case eq_t: display(out, c.to_eq(), values); break;
         default: UNREACHABLE(); break;
         }
     }
@@ -4280,13 +3965,6 @@ namespace sat {
                 if (lxr != null_literal) ineq.push(~lxr, offset);
                 break;
             }
-            case eq_t: {
-                eq& e = cnstr.to_eq();
-                ineq.reset(e.k());
-                for (eliteral wl : e) ineq.push(wl.lit, wl.weight);
-                if (e.lit() != null_literal) ineq.push(~e.lit(), e.k());
-                break;
-            }
             default:
                 UNREACHABLE();
                 break;

src/sat/ba_solver.h

@@ -51,14 +51,12 @@ namespace sat {
         enum tag_t {
             card_t,
             pb_t,
-            xr_t,
+            xr_t
-            eq_t
         };
 
         class card;
         class pb;
         class xr;
-        class eq;
 
         class constraint {
         protected:
@@ -72,9 +70,10 @@ namespace sat {
             size_t         m_obj_size;
             bool           m_learned;
             unsigned       m_id;
+            bool           m_pure;        // is the constraint pure (only positive occurrences)
         public:
             constraint(tag_t t, unsigned id, literal l, unsigned sz, size_t osz): 
-            m_tag(t), m_removed(false), m_lit(l), m_watch(null_literal), m_glue(0), m_psm(0), m_size(sz), m_obj_size(osz), m_learned(false), m_id(id) {}
+            m_tag(t), m_removed(false), m_lit(l), m_watch(null_literal), m_glue(0), m_psm(0), m_size(sz), m_obj_size(osz), m_learned(false), m_id(id), m_pure(false) {}
             ext_constraint_idx index() const { return reinterpret_cast<ext_constraint_idx>(this); }
             unsigned id() const { return m_id; }
             tag_t tag() const { return m_tag; }
@@ -95,20 +94,19 @@ namespace sat {
             void set_watch() { m_watch = m_lit; }
             void clear_watch() { m_watch = null_literal; }
             bool is_clear() const { return m_watch == null_literal && m_lit != null_literal; }
+            bool is_pure() const { return m_pure; }
+            void set_pure() { m_pure = true; }
 
             size_t obj_size() const { return m_obj_size; }
             card& to_card();
             pb&  to_pb();
             xr& to_xr();
-            eq& to_eq();
             card const& to_card() const;
             pb const&  to_pb() const;
             xr const& to_xr() const;
-            eq const& to_eq() const;
             bool is_card() const { return m_tag == card_t; }
             bool is_pb() const { return m_tag == pb_t; }
             bool is_xr() const { return m_tag == xr_t; }
-            bool is_eq() const { return m_tag == eq_t; }
             
             virtual bool is_watching(literal l) const { UNREACHABLE(); return false; };
             virtual literal_vector literals() const { UNREACHABLE(); return literal_vector(); }
@@ -185,60 +183,6 @@ namespace sat {
             virtual unsigned get_coeff(unsigned i) const { return m_wlits[i].first; }
         };
 
-        struct eliteral {
-            unsigned weight;
-            literal  lit;
-            unsigned tweight;
-            literal  tlit;
-            eliteral(unsigned w, literal lit):
-                weight(w), lit(lit), tweight(0), tlit(null_literal)
-            {}
-            eliteral(): weight(0), lit(null_literal), tweight(0), tlit(null_literal) {}
-        };
-        class eq : public constraint {
-            unsigned       m_lo, m_hi, m_max, m_k, m_trail_sz;
-            eliteral       m_wlits[0];
-        public:
-            static size_t get_obj_size(unsigned num_lits) { return sizeof(eq) + num_lits * sizeof(eliteral); }
-            eq(unsigned id, literal lit, svector<wliteral> const& wlits, unsigned k);
-            literal lit() const { return m_lit; }
-            eliteral operator[](unsigned i) const { return m_wlits[i]; }
-            eliteral& operator[](unsigned i) { return m_wlits[i]; }
-            eliteral const* begin() const { return m_wlits; }
-            eliteral const* end() const { return begin() + m_size; }
-            unsigned index(literal l) const;            
-            unsigned k() const { return m_k; }
-            void reset_lo() { m_lo = 0; }
-            void reset_hi() { m_hi = m_max; }
-            unsigned lo() const { return m_lo; }
-            unsigned hi() const { return m_hi; }
-            void inc_hi(unsigned d) { m_hi += d; }
-            void dec_lo(unsigned d) { SASSERT(d <= m_lo); m_lo -= d; }
-            // increment/decrement lo/hi save delta and variable in a trail.
-            void inc_lo(eliteral const& e) { 
-                m_lo += e.weight; 
-                m_wlits[m_trail_sz].tlit = literal(e.lit.var(), false); 
-                m_wlits[m_trail_sz++].tweight = e.weight; 
-            }
-            void dec_hi(eliteral const& e) { 
-                m_hi -= e.weight; 
-                m_wlits[m_trail_sz].tlit = literal(e.lit.var(), true); 
-                m_wlits[m_trail_sz++].tweight = e.weight; 
-            }
-            unsigned trail_sz() const { return m_trail_sz; }
-            void set_trail_sz(unsigned sz) { m_trail_sz = sz; }
-
-            virtual void negate() { SASSERT(lit() != null_literal); m_lit.neg(); }
-            virtual void set_k(unsigned k) { m_k = k; }
-            virtual void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); }
-            virtual literal_vector literals() const { literal_vector lits; for (auto wl : *this) lits.push_back(wl.lit); return lits; }
-            virtual bool is_watching(literal l) const { return true; }
-            virtual literal get_lit(unsigned i) const { return m_wlits[i].lit; }
-            virtual void set_lit(unsigned i, literal l) { m_wlits[i].lit = l; }
-            virtual unsigned get_coeff(unsigned i) const { return m_wlits[i].weight; }
-            
-        };
-
         class xr : public constraint {
             literal        m_lits[0];
         public:
@@ -281,8 +225,6 @@ namespace sat {
         unsigned_vector        m_constraint_to_reinit_lim;
         unsigned               m_constraint_to_reinit_last_sz;
         unsigned               m_constraint_id;
-        ptr_vector<eq>         m_eq_to_pop;
-        unsigned_vector        m_eq_to_pop_lim;
 
         // conflict resolution
         unsigned          m_num_marks;
@@ -340,7 +282,7 @@ namespace sat {
         unsigned_vector           m_weights;
         svector<wliteral>         m_wlits;
         bool subsumes(card& c1, card& c2, literal_vector& comp);
-        bool subsumes(card& c1, clause& c2, literal_vector& comp);
+        bool subsumes(card& c1, clause& c2, bool& self);
         bool subsumed(card& c1, literal l1, literal l2);
         bool subsumes(pb const& p1, pb_base const& p2);
         void subsumes(pb& p1, literal lit);
@@ -363,6 +305,7 @@ namespace sat {
         void gc_half(char const* _method);
         void update_psm(constraint& c) const;
         void mutex_reduction();
+        void update_pure();
 
         unsigned use_count(literal lit) const { return m_cnstr_use_list[lit.index()].size() + m_clause_use_list.get(lit).size(); }
 
@@ -451,19 +394,6 @@ namespace sat {
         lbool eval(model const& m, pb const& p) const;
         double get_reward(pb const& p, literal_occs_fun& occs) const;
 
-        // eq functionality
-        void pop_eq(eq& e);
-        bool init_watch(eq& e);
-        void clear_watch(eq& e);
-        lbool add_assign(eq& e, literal alit);
-        void get_antecedents(literal l, eq const& e, literal_vector& r);
-        void simplify(eq& e);
-        void recompile(eq& e);
-        void split_root(eq& e);
-        void calibrate(eq& e);
-        lbool eval(eq const& e) const;
-        lbool eval(model const& m, eq const& e) const;
-
         // access solver
         inline lbool value(bool_var v) const { return value(literal(v, false)); }
         inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); }
@@ -541,13 +471,11 @@ namespace sat {
         void display(std::ostream& out, card const& c, bool values) const;
         void display(std::ostream& out, pb const& p, bool values) const;
         void display(std::ostream& out, xr const& c, bool values) const;
-        void display(std::ostream& out, eq const& e, bool values) const;
         void display_lit(std::ostream& out, literal l, unsigned sz, bool values) const;
 
         constraint* add_at_least(literal l, literal_vector const& lits, unsigned k, bool learned);
         constraint* add_pb_ge(literal l, svector<wliteral> const& wlits, unsigned k, bool learned);
         constraint* add_xr(literal_vector const& lits, bool learned);
-        constraint* add_eq(literal l, svector<wliteral> const& wlits, unsigned k, bool learned);
 
         void copy_core(ba_solver* result, bool learned);
         void copy_constraints(ba_solver* result, ptr_vector<constraint> const& constraints);
@@ -561,7 +489,6 @@ namespace sat {
         void    add_at_least(bool_var v, literal_vector const& lits, unsigned k);
         void    add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k);
         void    add_xr(literal_vector const& lits);
-        void    add_eq(literal l, svector<wliteral> const& wlits, unsigned k) { add_eq(l, wlits, k, false); }
 
         virtual bool propagate(literal l, ext_constraint_idx idx);
         virtual lbool resolve_conflict();

src/sat/sat_asymm_branch.cpp

@@ -87,8 +87,6 @@ namespace sat {
             IF_VERBOSE(1, verbose_stream() << "(sat-asymm-branch-step :elim " << num_elim << ")\n";);
             if (num_elim == 0)
                 break;
-            if (false && num_elim > 1000) 
-                i = 0;
         }        
         IF_VERBOSE(1, if (m_elim_learned_literals > eliml0) 
                           verbose_stream() << "(sat-asymm-branch :elim " << m_elim_learned_literals - eliml0 << ")\n";);

src/sat/sat_asymm_branch_params.pyg

@@ -2,7 +2,7 @@ def_module_params(module_name='sat',
                   class_name='sat_asymm_branch_params',
                   export=True,
                   params=(('asymm_branch', BOOL, True, 'asymmetric branching'),
-                          ('asymm_branch.rounds', UINT, 10, 'maximal number of rounds to run asymmetric branch simplifications if progress is made'),
+                          ('asymm_branch.rounds', UINT, 2, 'maximal number of rounds to run asymmetric branch simplifications if progress is made'),
                           ('asymm_branch.delay', UINT, 1, 'number of simplification rounds to wait until invoking asymmetric branch simplification'),
                           ('asymm_branch.sampled', BOOL, True, 'use sampling based asymmetric branching based on binary implication graph'),
                           ('asymm_branch.limit', UINT, 100000000, 'approx. maximum number of literals visited during asymmetric branching'),

src/sat/sat_big.cpp

@@ -169,6 +169,7 @@ namespace sat {
         unsigned idx = 0;
         unsigned elim = 0;
         for (watch_list & wlist : s.m_watches) {
+            if (s.inconsistent()) break;
             literal u = to_literal(idx++);
             watch_list::iterator it     = wlist.begin();
             watch_list::iterator itprev = it;
@@ -179,6 +180,10 @@ namespace sat {
                     literal v = w.get_literal();
                     if (reaches(u, v) && u != get_parent(v)) {
                         ++elim;
+                        if (find_binary_watch(wlist, ~v)) {
+                            IF_VERBOSE(10, verbose_stream() << "binary: " << ~u << "\n");
+                            s.assign(~u, justification());
+                        }
                         // could turn non-learned non-binary tautology into learned binary.
                         s.get_wlist(~v).erase(watched(~u, w.is_learned()));
                         continue;
@@ -189,6 +194,7 @@ namespace sat {
             }
             wlist.set_end(itprev);
         }
+        s.propagate(false);
         return elim;
     }
 

src/sat/sat_config.cpp

@@ -72,6 +72,10 @@ namespace sat {
         m_num_threads     = p.threads();
         m_local_search    = p.local_search();
         m_local_search_threads = p.local_search_threads();
+        if (p.local_search_mode() == symbol("gsat"))
+            m_local_search_mode = local_search_mode::gsat;
+        else
+            m_local_search_mode = local_search_mode::wsat;
         m_unit_walk       = p.unit_walk();
         m_unit_walk_threads = p.unit_walk_threads();
         m_lookahead_simplify = p.lookahead_simplify();

src/sat/sat_config.h

@@ -73,6 +73,11 @@ namespace sat {
         adaptive_psat_cutoff
     };
 
+    enum local_search_mode {
+        gsat,
+        wsat
+    };
+
     struct config {
         unsigned long long m_max_memory;
         phase_selection    m_phase;
@@ -90,6 +95,7 @@ namespace sat {
         unsigned           m_num_threads;
         unsigned           m_local_search_threads;
         bool               m_local_search;
+        local_search_mode  m_local_search_mode;
         unsigned           m_unit_walk_threads;
         bool               m_unit_walk;
         bool               m_lookahead_simplify;

src/sat/sat_elim_eqs.cpp

@@ -223,6 +223,7 @@ namespace sat {
     }
 
     void elim_eqs::operator()(literal_vector const & roots, bool_var_vector const & to_elim) {
+        TRACE("elim_eqs", tout << "before bin cleanup\n"; m_solver.display(tout););
         cleanup_bin_watches(roots);
         TRACE("elim_eqs", tout << "after bin cleanup\n"; m_solver.display(tout););
         cleanup_clauses(roots, m_solver.m_clauses);
@@ -232,5 +233,6 @@ namespace sat {
         save_elim(roots, to_elim);
         m_solver.propagate(false);
         SASSERT(check_clauses(roots));
+        TRACE("elim_eqs", tout << "after full cleanup\n"; m_solver.display(tout););
     }
 };

src/sat/sat_local_search.cpp

@@ -72,9 +72,12 @@ namespace sat {
     void local_search::init_cur_solution() {
         for (unsigned v = 0; v < num_vars(); ++v) {
             // use bias with a small probability
-            if (m_rand() % 100 < 2) {
+            if (m_rand() % 10 < 5) {
                 m_vars[v].m_value = ((unsigned)(m_rand() % 100) < m_vars[v].m_bias);
             }
+            else {
+                m_vars[v].m_value = (m_rand() % 2) == 0;
+            }
         }
     }
 
@@ -449,7 +452,6 @@ namespace sat {
         m_best_unsat_rate = 1;
         m_last_best_unsat_rate = 1;
 
-
         reinit();
         timer timer;
         timer.start();
@@ -457,20 +459,23 @@ namespace sat {
         PROGRESS(tries, total_flips);
         
         for (tries = 1; !m_unsat_stack.empty() && m_limit.inc(); ++tries) {
-            if (m_unsat_stack.size() < m_best_unsat) {
-                m_best_unsat = m_unsat_stack.size();
-                m_last_best_unsat_rate = m_best_unsat_rate;
-                m_best_unsat_rate = (double)m_unsat_stack.size() / num_constraints();
-            }
             for (step = 0; step < m_max_steps && !m_unsat_stack.empty(); ++step) {
                 pick_flip_walksat();
+                if (m_unsat_stack.size() < m_best_unsat) {
+                    m_best_unsat = m_unsat_stack.size();
+                    m_last_best_unsat_rate = m_best_unsat_rate;
+                    m_best_unsat_rate = (double)m_unsat_stack.size() / num_constraints();                                        
+                }
             }
             total_flips += step;
             PROGRESS(tries, total_flips);
-            if (m_par && tries % 1 == 0) {
+            if (m_par && m_par->get_phase(*this)) {
-                m_par->get_phase(*this);
                 reinit();
             }
+            if (tries % 10 == 0 && !m_unsat_stack.empty()) {
+                reinit();
+            }
+            
         }
     }
 
@@ -490,7 +495,10 @@ namespace sat {
                     if (m_best_objective_value >= m_best_known_value) {
                         break;
                     }
-                }                
+                }          
+                if (m_unsat_stack.size() < m_best_unsat) {
+                    m_best_unsat = m_unsat_stack.size();
+                }
                 flipvar = pick_var_gsat();
                 flip_gsat(flipvar);
                 m_vars[flipvar].m_time_stamp = step++;
@@ -563,6 +571,9 @@ namespace sat {
         unsigned num_unsat = m_unsat_stack.size();
         constraint const& c = m_constraints[m_unsat_stack[m_rand() % m_unsat_stack.size()]];
         SASSERT(c.m_k < constraint_value(c));
+        unsigned reflipped = 0;
+        bool is_core = m_unsat_stack.size() <= 10;
+    reflip:
         // TBD: dynamic noise strategy 
         //if (m_rand() % 100 < 98) {
         if (m_rand() % 10000 <= m_noise) {
@@ -635,6 +646,10 @@ namespace sat {
             }
         }
         flip_walksat(best_var);
+        if (false && is_core && c.m_k < constraint_value(c)) {
+            ++reflipped;
+            goto reflip;
+        }
     }
 
     void local_search::flip_walksat(bool_var flipvar) {

src/sat/sat_local_search.h

@@ -21,17 +21,13 @@
 
 #include "util/vector.h"
 #include "sat/sat_types.h"
+#include "sat/sat_config.h"
 #include "util/rlimit.h"
 
 namespace sat {
 
     class parallel;
 
-    enum local_search_mode {
-        gsat,
-        wsat
-    };
-
     class local_search_config {
         unsigned m_seed;
         unsigned m_strategy_id;

src/sat/sat_parallel.cpp

@@ -229,7 +229,6 @@ namespace sat {
                     break;
                 }
             }
-            IF_VERBOSE(1, verbose_stream() << "set phase: " << m_num_clauses << " " << s.m_clauses.size() << " " << m_solver_copy << "\n";);
         }
         if (m_consumer_ready && (m_num_clauses == 0 || (m_num_clauses > s.m_clauses.size()))) {
             // time to update local search with new clauses.
@@ -268,10 +267,13 @@ namespace sat {
         }
     }
 
-   void parallel::get_phase(local_search& s) {
+    bool parallel::get_phase(local_search& s) {
+        bool copied = false;
         #pragma omp critical (par_solver)
         {
+            m_consumer_ready = true;
             if (m_solver_copy && s.num_non_binary_clauses() > m_solver_copy->m_clauses.size()) {
+                copied = true;
                 s.import(*m_solver_copy.get(), true);
             }
             for (unsigned i = 0; i < m_phase.size(); ++i) {
@@ -280,6 +282,7 @@ namespace sat {
             }
             m_phase.reserve(s.num_vars(), l_undef);
         }
+        return copied;
     }
 
     void parallel::set_phase(local_search& s) {

src/sat/sat_parallel.h

@@ -106,7 +106,7 @@ namespace sat {
         
         void set_phase(local_search& s);
 
-        void get_phase(local_search& s);
+        bool get_phase(local_search& s);
 
         bool copy_solver(solver& s);
     };

src/sat/sat_params.pyg

@@ -38,6 +38,7 @@ def_module_params('sat',
                           ('atmost1_encoding', SYMBOL, 'grouped', 'encoding used for at-most-1 constraints grouped, bimander, ordered'),
                           ('local_search', BOOL, False, 'use local search instead of CDCL'),
                           ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
+                          ('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'),
 	                  ('unit_walk', BOOL, False, 'use unit-walk search instead of CDCL'),
                           ('unit_walk_threads', UINT, 0, 'number of unit-walk search threads to find satisfiable solution'),
                           ('lookahead.cube.cutoff', SYMBOL, 'adaptive_freevars', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'),

src/sat/sat_scc.cpp

@@ -232,6 +232,7 @@ namespace sat {
         if (m_scc_tr) {
             reduce_tr();
         }
+        TRACE("scc_detail", m_solver.display(tout););
         return to_elim.size();
     }
 

src/sat/sat_simplifier.cpp

@@ -198,7 +198,7 @@ namespace sat {
         initialize();
 
         CASSERT("sat_solver", s.check_invariant());
-        TRACE("before_simplifier", s.display(tout););
+        TRACE("sat_simplifier", s.display(tout););
 
         s.m_cleaner(true);
         TRACE("after_cleanup", s.display(tout););
@@ -254,7 +254,7 @@ namespace sat {
         }
 
         CASSERT("sat_solver", s.check_invariant());
-        TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
+        TRACE("sat_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
 
         finalize();
 

src/sat/sat_solver.cpp

@@ -332,6 +332,14 @@ namespace sat {
     }
 
     void solver::mk_bin_clause(literal l1, literal l2, bool learned) {
+        if (find_binary_watch(get_wlist(~l1), ~l2)) {
+            assign(l1, justification());
+            return;
+        }
+        if (find_binary_watch(get_wlist(~l2), ~l1)) {
+            assign(l2, justification());
+            return;
+        }
         watched* w0 = find_binary_watch(get_wlist(~l1), l2);
         if (w0) {
             if (w0->is_learned() && !learned) {
@@ -355,7 +363,7 @@ namespace sat {
         }
         m_stats.m_mk_bin_clause++;
         get_wlist(~l1).push_back(watched(l2, learned));
-        get_wlist(~l2).push_back(watched(l1, learned));        
+        get_wlist(~l2).push_back(watched(l1, learned));
     }
 
     bool solver::propagate_bin_clause(literal l1, literal l2) {
@@ -1023,6 +1031,7 @@ namespace sat {
         scoped_limits scoped_rl(rlimit());
         local_search srch;
         srch.config().set_seed(m_config.m_random_seed);
+        srch.config().set_mode(m_config.m_local_search_mode);
         srch.import(*this, false);
         scoped_rl.push_child(&srch.rlimit());
         lbool r = srch.check(num_lits, lits, 0);
@@ -1047,6 +1056,7 @@ namespace sat {
         for (int i = 0; i < num_local_search; ++i) {
             local_search* l = alloc(local_search);
             l->config().set_seed(m_config.m_random_seed + i);
+            l->config().set_mode(m_config.m_local_search_mode);
             l->import(*this, false);
             ls.push_back(l);
         }
@@ -1095,7 +1105,7 @@ namespace sat {
                     r = par.get_solver(i).check(num_lits, lits);
                 }
                 else if (IS_LOCAL_SEARCH(i)) {
-                    r = ls[i-local_search_offset]->check(num_lits, lits);
+                    r = ls[i-local_search_offset]->check(num_lits, lits, &par);
                 }
                 else if (IS_UNIT_WALK(i)) {
                     r = uw[i-unit_walk_offset]->check(num_lits, lits);
@@ -1519,9 +1529,9 @@ namespace sat {
 
         m_scc();
         CASSERT("sat_simplify_bug", check_invariant());
-        
+      
-
         m_simplifier(false);
+
         CASSERT("sat_simplify_bug", check_invariant());
         CASSERT("sat_missed_prop", check_missed_propagation());
         if (!m_learned.empty()) {
@@ -1536,6 +1546,7 @@ namespace sat {
         CASSERT("sat_missed_prop", check_missed_propagation());
         CASSERT("sat_simplify_bug", check_invariant());
         m_asymm_branch(false);
+
         CASSERT("sat_missed_prop", check_missed_propagation());
         CASSERT("sat_simplify_bug", check_invariant());
         if (m_ext) {

src/sat/sat_solver/inc_sat_solver.cpp

@@ -60,7 +60,8 @@ class inc_sat_solver : public solver {
     sat::literal_vector m_asms;
     goal_ref_buffer     m_subgoals;
     proof_converter_ref m_pc;
-    mutable model_converter_ref m_mc0;
+    sref_vector<model_converter> m_mcs;
+    mutable model_converter_ref m_mc0;         // TBD: should be saved/retained under push/pop
     mutable obj_hashtable<func_decl>  m_inserted_const2bits;
     mutable ref<sat2goal::mc>   m_sat_mc;
     mutable model_converter_ref m_cached_mc;
@@ -88,6 +89,7 @@ public:
         m_internalized_converted(false), 
         m_internalized_fmls(m) {
         updt_params(p);
+        m_mcs.push_back(nullptr);
         init_preprocess();
         m_solver.set_incremental(incremental_mode && !override_incremental());
     }
@@ -119,7 +121,7 @@ public:
         for (unsigned a : m_asms_lim) result->m_asms_lim.push_back(a);
         for (unsigned h : m_fmls_head_lim) result->m_fmls_head_lim.push_back(h);
         for (expr* f : m_internalized_fmls) result->m_internalized_fmls.push_back(tr(f));
-        if (m_mc0) result->m_mc0 = m_mc0->translate(tr);
+        if (m_mcs.back()) result->m_mcs.push_back(m_mcs.back()->translate(tr));
         if (m_sat_mc) result->m_sat_mc = dynamic_cast<sat2goal::mc*>(m_sat_mc->translate(tr));
         // copy m_bb_rewriter?
         result->m_internalized_converted = m_internalized_converted;
@@ -186,6 +188,7 @@ public:
         if (r != l_true) return r;
 
         init_reason_unknown();
+        m_internalized_converted = false;
         try {
             // IF_VERBOSE(0, m_solver.display(verbose_stream()));
             r = m_solver.check(m_asms.size(), m_asms.c_ptr());
@@ -217,6 +220,7 @@ public:
         internalize_formulas();
         m_solver.user_push();
         ++m_num_scopes;
+        m_mcs.push_back(m_mcs.back());
         m_fmls_lim.push_back(m_fmls.size());
         m_asms_lim.push_back(m_asmsf.size());
         m_fmls_head_lim.push_back(m_fmls_head);
@@ -234,7 +238,9 @@ public:
         SASSERT(n <= m_num_scopes);
         m_solver.user_pop(n);
         m_num_scopes -= n;
+        // ? m_internalized_converted = false;
         while (n > 0) {
+            m_mcs.pop_back();
             m_fmls_head = m_fmls_head_lim.back();
             m_fmls.resize(m_fmls_lim.back());
             m_fmls_lim.pop_back();
@@ -448,12 +454,10 @@ public:
         if (m_cached_mc)
             return m_cached_mc;
         if (is_internalized() && m_internalized_converted) {            
-            insert_const2bits();
             m_sat_mc->flush_smc(m_solver, m_map);
-            m_cached_mc = m_mc0.get();
+            m_cached_mc = m_mcs.back();
             m_cached_mc = concat(solver::get_model_converter().get(), m_cached_mc.get());
             m_cached_mc = concat(m_cached_mc.get(), m_sat_mc.get());
-            // IF_VERBOSE(0, m_cached_mc->display(verbose_stream() << "get-model-converter\n"););
             return m_cached_mc;
         }
         else {
@@ -493,12 +497,10 @@ public:
         simp2_p.set_bool("elim_and", true);
         simp2_p.set_bool("blast_distinct", true);
         m_preprocess =
-            and_then(mk_card2bv_tactic(m, m_params),
+            and_then(mk_card2bv_tactic(m, m_params),                  // updates model converter
                      using_params(mk_simplify_tactic(m), simp2_p),
                      mk_max_bv_sharing_tactic(m),
-                     mk_bit_blaster_tactic(m, m_bb_rewriter.get()),
+                     mk_bit_blaster_tactic(m, m_bb_rewriter.get()),   // updates model converter
-                     //mk_aig_tactic(),
-                     //mk_propagate_values_tactic(m, simp2_p),
                      using_params(mk_simplify_tactic(m), simp2_p));
         while (m_bb_rewriter->get_num_scopes() < m_num_scopes) {
             m_bb_rewriter->push();
@@ -508,22 +510,6 @@ public:
 
 private:
 
-    void insert_const2bits() const {
-        if (!m_bb_rewriter) return;
-        obj_map<func_decl, expr*> to_insert;
-        obj_map<func_decl, expr*> const& const2bits = m_bb_rewriter->const2bits();
-        for (auto const& kv : const2bits) {
-            if (!m_inserted_const2bits.contains(kv.m_key)) {
-                m_inserted_const2bits.insert(kv.m_key);
-                to_insert.insert(kv.m_key, kv.m_value);
-            }
-        }
-        if (!to_insert.empty()) {
-            m_mc0 = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, to_insert));
-        }
-    }
-
-
     lbool internalize_goal(goal_ref& g, dep2asm_t& dep2asm, bool is_lemma) {
         m_pc.reset();
         m_subgoals.reset();
@@ -543,15 +529,15 @@ private:
             m_preprocess = 0;
             m_bb_rewriter = 0;
             return l_undef;
-        }
+        }        
         if (m_subgoals.size() != 1) {
-            IF_VERBOSE(0, verbose_stream() << "size of subgoals is not 1, it is: " << m_subgoals.size() << "\n";);
+            IF_VERBOSE(0, verbose_stream() << "size of subgoals is not 1, it is: " << m_subgoals.size() << "\n");
             return l_undef;
         }
         g = m_subgoals[0];
         expr_ref_vector atoms(m);
         m_pc = g->pc();
-        m_mc0 = concat(m_mc0.get(), g->mc());
+        m_mcs.set(m_mcs.size()-1, concat(m_mcs.back(), g->mc()));
         TRACE("sat", g->display_with_dependencies(tout););
 
         // ensure that if goal is already internalized, then import mc from m_solver.
@@ -591,8 +577,8 @@ private:
     }
 
     lbool internalize_vars(expr_ref_vector const& vars, sat::bool_var_vector& bvars) {
-        for (unsigned i = 0; i < vars.size(); ++i) {
+        for (expr* v : vars) {
-            internalize_var(vars[i], bvars);
+            internalize_var(v, bvars);
         }
         return l_true;
     }
@@ -604,7 +590,6 @@ private:
         bool internalized = false;
         if (is_uninterp_const(v) && m.is_bool(v)) {
             sat::bool_var b = m_map.to_bool_var(v);
-
             if (b != sat::null_bool_var) {
                 bvars.push_back(b);
                 internalized = true;
@@ -614,10 +599,9 @@ private:
             SASSERT(bvutil.is_bv(bv));
             app* abv = to_app(bv);
             internalized = true;
-            unsigned sz = abv->get_num_args();
+            for (expr* arg : *abv) {
-            for (unsigned j = 0; j < sz; ++j) {
+                SASSERT(is_uninterp_const(arg));
-                SASSERT(is_uninterp_const(abv->get_arg(j)));
+                sat::bool_var b = m_map.to_bool_var(arg);
-                sat::bool_var b = m_map.to_bool_var(abv->get_arg(j));
                 if (b == sat::null_bool_var) {
                     internalized = false;
                 }
@@ -625,7 +609,7 @@ private:
                     bvars.push_back(b);
                 }
             }
-            CTRACE("sat", internalized, tout << "var: "; for (unsigned j = 0; j < sz; ++j) tout << bvars[bvars.size()-sz+j] << " "; tout << "\n";);
+            CTRACE("sat", internalized, tout << "var: " << bvars << "\n";);
         }
         else if (is_uninterp_const(v) && bvutil.is_bv(v)) {
             // variable does not occur in assertions, so is unconstrained.
@@ -813,18 +797,18 @@ private:
             //IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "satmc\n"););
             (*m_sat_mc)(mdl);
         }
-        insert_const2bits();
+        if (m_mcs.back()) {            
-        if (m_mc0) {            
             //IF_VERBOSE(0, m_mc0->display(verbose_stream() << "mc0\n"););
-            (*m_mc0)(mdl);
+            (*m_mcs.back())(mdl);
         }
         TRACE("sat", model_smt2_pp(tout, m, *mdl, 0););
         
         // IF_VERBOSE(0, model_smt2_pp(verbose_stream() << "after\n", m, *mdl, 0););
 
 #if 0
-        IF_VERBOSE(0, verbose_stream() << "Verifying solution\n";);
+        IF_VERBOSE(0, verbose_streamm() << "Verifying solution\n";);
         model_evaluator eval(*mdl);
+        bool all_true = true;
         for (expr * f : m_fmls) {
             expr_ref tmp(m);
             eval(f, tmp);
@@ -833,13 +817,20 @@ private:
                    model_smt2_pp(tout, m, *(mdl.get()), 0););
             if (!m.is_true(tmp)) {
                 IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(f, m) << "\n";);
-                IF_VERBOSE(0, verbose_stream() << m_params << "\n";);
+                all_true = false;
-                IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "sat mc\n"););
+            }
-                IF_VERBOSE(0, if (m_mc0) m_mc0->display(verbose_stream() << "mc0\n"););
+            else {
-                break;
+                VERIFY(m.is_true(tmp));                                
             }
-            VERIFY(m.is_true(tmp));                                
         }
+        if (!all_true) {
+            IF_VERBOSE(0, verbose_stream() << m_params << "\n";);
+            IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "sat mc\n"););
+            IF_VERBOSE(0, if (m_mcs.back()) m_mcs.back()->display(verbose_stream() << "mc0\n"););
+            //IF_VERBOSE(0, m_solver.display(verbose_stream()));
+            IF_VERBOSE(0, for (auto const& kv : m_map) verbose_stream() << mk_pp(kv.m_key, m) << " |-> " << kv.m_value << "\n";);
+        }
+
 #endif
     }
 };

src/sat/tactic/goal2sat.cpp

@@ -573,28 +573,6 @@ struct goal2sat::imp {
 
     void convert_eq_k(app* t, rational const& k, bool root, bool sign) {
         SASSERT(k.is_unsigned());
-#if 0
-        IF_VERBOSE(0, verbose_stream() << t->get_id() << ": " << mk_pp(t, m) << "\n";);
-        svector<wliteral> wlits;
-        convert_pb_args(t, wlits);
-        if (root && !sign) {
-            m_ext->add_eq(sat::null_literal, wlits, k.get_unsigned());
-            m_result_stack.reset();
-        }
-        else {
-            sat::bool_var v = m_solver.mk_var();
-            sat::literal l(v, false);
-            m_ext->add_eq(l, wlits, k.get_unsigned());
-            m_result_stack.shrink(m_result_stack.size() - t->get_num_args());
-            m_cache.insert(t, l);
-            if (sign) l.neg();
-            m_result_stack.push_back(l);
-            if (root) {
-                mk_clause(l);
-                m_result_stack.reset();
-            }
-        }
-#else
         sat::literal_vector lits;
         convert_pb_args(t->get_num_args(), lits);
         sat::bool_var v1 = (root && !sign) ? sat::null_bool_var : m_solver.mk_var(true);
@@ -625,7 +603,6 @@ struct goal2sat::imp {
                 m_result_stack.reset();
             }
         }
-#endif
     }
 
     void ensure_extension() {
@@ -1004,6 +981,12 @@ void sat2goal::mc::display(std::ostream& out) {
     if (m_gmc) m_gmc->display(out);
 }
 
+void sat2goal::mc::get_units(obj_map<expr, bool>& units) {
+    flush_gmc();
+    if (m_gmc) m_gmc->get_units(units);
+}
+
+
 void sat2goal::mc::operator()(model_ref & md) {
     model_evaluator ev(*md);
     ev.set_model_completion(false);

src/sat/tactic/goal2sat.h

@@ -94,7 +94,7 @@ public:
         model_converter* translate(ast_translation& translator) override;
         void collect(ast_pp_util& visitor) override;
         void display(std::ostream& out) override;
-        
+        void get_units(obj_map<expr, bool>& units) override;
         app* var2expr(sat::bool_var v) const { return m_var2expr.get(v, nullptr); }
         expr_ref lit2expr(sat::literal l);
         void insert(sat::bool_var v, app * atom, bool aux);

src/solver/solver.cpp

@@ -211,7 +211,35 @@ void solver::updt_params(params_ref const & p) {
     m_enforce_model_conversion = m_params.get_bool("solver.enforce_model_conversion", false);
 }
 
-void solver::hoist_converter(model_converter_ref& mc) {
-    
-}
 
+expr_ref_vector solver::get_units(ast_manager& m) {
+    expr_ref_vector fmls(m), result(m), tmp(m);
+    get_assertions(fmls);
+    obj_map<expr, bool> units;
+    for (expr* f : fmls) {
+        if (m.is_not(f, f) && is_literal(m, f)) {
+            m.inc_ref(f);
+            units.insert(f, false);
+        }
+        else if (is_literal(m, f)) {
+            m.inc_ref(f);
+            units.insert(f, true);
+        }
+    }
+    model_converter_ref mc = get_model_converter();
+    if (mc) {
+        mc->get_units(units);
+    }
+    for (auto const& kv : units) {
+        tmp.push_back(kv.m_key);
+        if (kv.m_value) 
+            result.push_back(kv.m_key); 
+        else 
+            result.push_back(m.mk_not(kv.m_key));
+    }
+    for (expr* e : tmp) {
+        m.dec_ref(e);
+    }
+
+    return result;
+}

src/solver/solver.h

@@ -203,6 +203,11 @@ public:
 
     virtual model_converter_ref get_model_converter() const { return m_mc0; }
 
+    /**
+       \brief extract units from solver.
+    */
+    expr_ref_vector get_units(ast_manager& m);
+
     class scoped_push {
         solver& s;
         bool    m_nopop;
@@ -220,7 +225,6 @@ protected:
 
     bool is_literal(ast_manager& m, expr* e);
 
-    void hoist_converter(model_converter_ref& mc);
 };
 
 typedef ref<solver> solver_ref;

src/tactic/arith/eq2bv_tactic.cpp

@@ -119,6 +119,8 @@ class eq2bv_tactic : public tactic {
             }
         }
 
+        virtual void get_units(obj_map<expr, bool>& units) { units.reset(); }
+
     };
 
 public:

src/tactic/arith/fm_tactic.cpp

@@ -180,6 +180,8 @@ class fm_tactic : public tactic {
             m_clauses.back().swap(c);
         }
 
+        virtual void get_units(obj_map<expr, bool>& units) { units.reset(); }
+
         virtual void operator()(model_ref & md) {
             TRACE("fm_mc", model_v2_pp(tout, *md); display(tout););
             model_evaluator ev(*(md.get()));

src/tactic/arith/pb2bv_model_converter.cpp

@@ -50,6 +50,10 @@ pb2bv_model_converter::~pb2bv_model_converter() {
     }
 }
 
+void pb2bv_model_converter::get_units(obj_map<expr, bool>& units) { 
+    if (!m_c2bit.empty()) units.reset(); 
+}
+
 
 void pb2bv_model_converter::operator()(model_ref & md) {
     TRACE("pb2bv", tout << "converting model:\n"; model_v2_pp(tout, *md); display(tout););

src/tactic/arith/pb2bv_model_converter.h

@@ -33,6 +33,7 @@ public:
     virtual ~pb2bv_model_converter();
     void operator()(model_ref & md) override;
     void display(std::ostream & out) override;
+    void get_units(obj_map<expr, bool>& units) override;
     model_converter * translate(ast_translation & translator) override;
 };
 

src/tactic/bv/bit_blaster_model_converter.cpp

@@ -206,6 +206,10 @@ struct bit_blaster_model_converter : public model_converter {
         }
     }
 
+    void get_units(obj_map<expr, bool>& units) override {
+        // no-op
+    }
+
 protected:
     bit_blaster_model_converter(ast_manager & m):m_vars(m), m_bits(m) { }
 public:

src/tactic/bv/bit_blaster_tactic.cpp

@@ -62,6 +62,7 @@ class bit_blaster_tactic : public tactic {
             TRACE("before_bit_blaster", g->display(tout););
             m_num_steps = 0;
             
+            m_rewriter->start_rewrite();
             expr_ref   new_curr(m());
             proof_ref  new_pr(m());
             unsigned size = g->size();
@@ -78,13 +79,16 @@ class bit_blaster_tactic : public tactic {
                 }
                 if (curr != new_curr) {
                     change = true;                    
-                    TRACE("bit_blaster", tout << mk_pp(curr, m()) << " -> " << mk_pp(new_curr, m()) << "\n";);
+                    TRACE("bit_blaster", tout << mk_pp(curr, m()) << " -> " << new_curr << "\n";);
                     g->update(idx, new_curr, new_pr, g->dep(idx));
                 }
             }
             
-            if (change && g->models_enabled())  
+            if (change && g->models_enabled()) {
-                g->add(mk_bit_blaster_model_converter(m(), m_rewriter->const2bits()));
+                obj_map<func_decl, expr*> const2bits;
+                m_rewriter->end_rewrite(const2bits);
+                g->add(mk_bit_blaster_model_converter(m(), const2bits));
+            }
             g->inc_depth();
             result.push_back(g.get());
             TRACE("after_bit_blaster", g->display(tout); if (g->mc()) g->mc()->display(tout); tout << "\n";);
@@ -148,6 +152,7 @@ public:
         return m_imp->get_num_steps();
     }
 
+
 };
 
 
@@ -158,3 +163,4 @@ tactic * mk_bit_blaster_tactic(ast_manager & m, params_ref const & p) {
 tactic * mk_bit_blaster_tactic(ast_manager & m, bit_blaster_rewriter* rw, params_ref const & p) {
     return clean(alloc(bit_blaster_tactic, m, rw, p));
 }
+

src/tactic/core/pb_preprocess_tactic.cpp

@@ -33,60 +33,13 @@ Notes:
 --*/
 #include "tactic/core/pb_preprocess_tactic.h"
 #include "tactic/tactical.h"
+#include "tactic/generic_model_converter.h"
 #include "ast/for_each_expr.h"
 #include "ast/pb_decl_plugin.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/expr_substitution.h"
 #include "ast/ast_pp.h"
 
-class pb_preproc_model_converter : public model_converter {
-    ast_manager& m;
-    pb_util      pb;
-    expr_ref_vector                  m_refs;
-    svector<std::pair<app*, expr*> > m_const;
-
-public:
-    pb_preproc_model_converter(ast_manager& m):m(m), pb(m), m_refs(m) {}
-
-    virtual void operator()(model_ref & mdl) {
-        for (auto const& kv : m_const) {
-            mdl->register_decl(kv.first->get_decl(), kv.second);
-        }
-    }
-
-    void set_value(expr* e, bool p) {
-        while (m.is_not(e, e)) {
-            p = !p;
-        }
-        SASSERT(is_app(e));
-        set_value_p(to_app(e), p?m.mk_true():m.mk_false());        
-    }
-
-    virtual model_converter * translate(ast_translation & translator) {
-        pb_preproc_model_converter* mc = alloc(pb_preproc_model_converter, translator.to());
-        for (auto const& kv : m_const) {
-            mc->set_value_p(translator(kv.first), translator(kv.second));
-        }
-        return mc;
-    }
-
-    virtual void display(std::ostream & out) {
-        for (auto const& kv : m_const) {
-            out << "(model-set " << mk_pp(kv.first, m) << " " << mk_pp(kv.second, m) << ")\n";
-        }
-    }
-
-private:
-    void set_value_p(app* e, expr* v) {
-        SASSERT(e->get_num_args() == 0);  
-        SASSERT(is_uninterp_const(e));
-        m_const.push_back(std::make_pair(e, v));
-        m_refs.push_back(e);
-        m_refs.push_back(v);
-    }
-
-};
-
 class pb_preprocess_tactic : public tactic {
     struct rec { unsigned_vector pos, neg; rec() { } };
     typedef obj_map<app, rec> var_map;
@@ -119,24 +72,31 @@ class pb_preprocess_tactic : public tactic {
         for (unsigned i = 0; i < m_other.size(); ++i) {
             out << "ot " << m_other[i] << ": " << mk_pp(g->form(m_other[i]), m) << "\n";
         }
-                
+         
-        var_map::iterator it  = m_vars.begin();
+        for (auto const& kv : m_vars) {
-        var_map::iterator end = m_vars.end();
+            app* e = kv.m_key;
-        for (; it != end; ++it) {
+            unsigned_vector const& pos = kv.m_value.pos;
-            app* e = it->m_key;
+            unsigned_vector const& neg = kv.m_value.neg;
-            unsigned_vector const& pos = it->m_value.pos;
-            unsigned_vector const& neg = it->m_value.neg;
             out << mk_pp(e, m) << ": ";
-            for (unsigned i = 0; i < pos.size(); ++i) {
+            for (unsigned p : pos) {
-                out << "p: " << pos[i] << " ";
+                out << "p: " << p << " ";
             }
-            for (unsigned i = 0; i < neg.size(); ++i) {
+            for (unsigned n : neg) {
-                out << "n: " << neg[i] << " ";
+                out << "n: " << n << " ";
             }
             out << "\n";
         }
     }
 
+    void set_value(generic_model_converter& mc, expr* e, bool p) {
+        while (m.is_not(e, e)) {
+            p = !p;
+        }
+        SASSERT(is_app(e));
+        mc.add(to_app(e), p?m.mk_true():m.mk_false());        
+    }
+
+
 public:
     pb_preprocess_tactic(ast_manager& m, params_ref const& p = params_ref()): 
         m(m), pb(m), m_r(m) {}
@@ -156,7 +116,7 @@ public:
             throw tactic_exception("pb-preprocess does not support proofs");
         }
 
-        pb_preproc_model_converter* pp = alloc(pb_preproc_model_converter, m);
+        generic_model_converter* pp = alloc(generic_model_converter, m, "pb-preprocess");
         g->add(pp);
 
         g->inc_depth();        
@@ -165,7 +125,7 @@ public:
         // decompose(g);
     }
 
-    bool simplify(goal_ref const& g, pb_preproc_model_converter& mc) {
+    bool simplify(goal_ref const& g, generic_model_converter& mc) {
         reset();
         normalize(g);
         if (g->inconsistent()) {
@@ -203,11 +163,11 @@ public:
             TRACE("pb", tout << mk_pp(e, m) << " " << r.pos.size() << " " << r.neg.size() << "\n";);
             if (r.pos.empty()) {                
                 replace(r.neg, e, m.mk_false(), g);
-                mc.set_value(e, false);
+                set_value(mc, e, false);
             }
             else if (r.neg.empty()) {
                 replace(r.pos, e, m.mk_true(), g);
-                mc.set_value(e, true);
+                set_value(mc, e, true);
             }
             if (g->inconsistent()) return false;
             ++it;
@@ -509,7 +469,7 @@ private:
 
     // Implement very special case of resolution.
     
-    void resolve(pb_preproc_model_converter& mc, unsigned idx1, 
+    void resolve(generic_model_converter& mc, unsigned idx1, 
                  unsigned_vector const& positions, app* e, bool pos, goal_ref const& g) {
         if (positions.size() != 1) return;
         unsigned idx2 = positions[0];
@@ -558,7 +518,7 @@ private:
             else {
                 args2[j] = m.mk_true();
             }
-            mc.set_value(arg, j != min_index);
+            set_value(mc, arg, j != min_index);
         }
         
         tmp1 = pb.mk_ge(args2.size(), coeffs2.c_ptr(), args2.c_ptr(), k2);

src/tactic/generic_model_converter.cpp

@@ -181,6 +181,53 @@ void generic_model_converter::operator()(expr_ref& fml) {
     fml = mk_and(fmls);
 }
 
+void generic_model_converter::get_units(obj_map<expr, bool>& units) {
+    th_rewriter rw(m);
+    expr_safe_replace rep(m);
+    expr_ref tmp(m);
+    bool val = false;
+    expr* f = nullptr;
+    for (auto const& kv : units) {
+        rep.insert(kv.m_key, kv.m_value ? m.mk_true() : m.mk_false());
+    }
+    for (unsigned i = m_entries.size(); i-- > 0;) {
+        entry const& e = m_entries[i];
+        switch (e.m_instruction) {
+        case HIDE: 
+            tmp = m.mk_const(e.m_f);
+            if (units.contains(tmp)) {
+                m.dec_ref(tmp);
+                units.remove(tmp);
+            }
+            break;
+        case ADD:
+            if (e.m_f->get_arity() == 0 && m.is_bool(e.m_f->get_range())) {
+                tmp = m.mk_const(e.m_f);
+                if (units.contains(tmp)) {
+                    break;
+                }
+                tmp = e.m_def;
+                rep(tmp);
+                rw(tmp);
+                if (m.is_true(tmp)) {
+                    tmp = m.mk_const(e.m_f);
+                    m.inc_ref(tmp);
+                    units.insert(tmp, true);
+                    rep.insert(tmp, m.mk_true());
+                }
+                else if (m.is_false(tmp)) {
+                    tmp = m.mk_const(e.m_f);
+                    m.inc_ref(tmp);
+                    units.insert(tmp, false);
+                    rep.insert(tmp, m.mk_false());
+                }
+            }
+            break;
+        }
+    }
+}
+
+
 /*
  \brief simplify definition expansion from model converter in the case they come from blocked clauses.
  In this case the definitions are of the form:

src/tactic/generic_model_converter.h

@@ -71,6 +71,8 @@ public:
     void collect(ast_pp_util& visitor) override;
 
     void operator()(expr_ref& fml) override; 
+
+    void get_units(obj_map<expr, bool>& units) override;
 };
 
 typedef ref<generic_model_converter> generic_model_converter_ref;

src/tactic/horn_subsume_model_converter.h

@@ -80,6 +80,9 @@ public:
     ast_manager& get_manager() { return m; }
 
     void display(std::ostream & out) override {}
+
+    void get_units(obj_map<expr, bool>& units) override { units.reset(); }
+
 };
 
 #endif

src/tactic/model_converter.cpp

@@ -71,14 +71,19 @@ public:
     }
 
     void operator()(expr_ref & fml) override {
-        this->m_c1->operator()(fml);
         this->m_c2->operator()(fml);
+        this->m_c1->operator()(fml);
     }
     
     void operator()(labels_vec & r) override {
         this->m_c2->operator()(r);
         this->m_c1->operator()(r);
     }
+
+    void get_units(obj_map<expr, bool>& fmls) override {
+        m_c2->get_units(fmls);
+        m_c1->get_units(fmls);
+    }
   
     char const * get_name() const override { return "concat-model-converter"; }
 
@@ -125,6 +130,10 @@ public:
         fml = r;
     }
 
+    void get_units(obj_map<expr, bool>& fmls) override {
+        // no-op
+    }
+
     void cancel() override {
     }
     

src/tactic/model_converter.h

@@ -88,6 +88,8 @@ public:
        formula and removing these definitions from the model converter.
      */
     virtual void operator()(expr_ref& formula) { UNREACHABLE(); }
+
+    virtual void get_units(obj_map<expr, bool>& fmls) { UNREACHABLE(); }
 };
 
 typedef ref<model_converter> model_converter_ref;