CNF conversion refactoring (#5547)

* split sat2goal out of goal2sat

These two classes need different things out of the sat::solver class,
and separating them makes it easier to fiddle with their dependencies
independently.

I also fiddled with some headers to make it possible to include
sat_solver_core.h instead of sat_solver.h.

* limit solver_core methods to those needed by goal2sat

And switch sat2goal and sat_tactic over to relying on the derived
sat::solver class instead. There were no other uses of solver_core.

I'm hoping this makes it feasible to reuse goal2sat's CNF conversion
from places like the tseitin-cnf tactic, so they can be unified into a
single implementation.

src/api/api_solver.cpp

@@ -42,6 +42,7 @@ Revision History:
 #include "sat/dimacs.h"
 #include "sat/sat_solver.h"
 #include "sat/tactic/goal2sat.h"
+#include "sat/tactic/sat2goal.h"
 
 
 extern "C" {

src/sat/sat_solver.h

@@ -244,12 +244,13 @@ namespace sat {
         // Misc
         //
         // -----------------------
-        void updt_params(params_ref const & p) override;        
+        void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);
 
-        void collect_statistics(statistics & st) const override;
+        // collect statistics from sat solver
+        void collect_statistics(statistics & st) const;
         void reset_statistics();
-        void display_status(std::ostream & out) const override;
+        void display_status(std::ostream & out) const;
         
         /**
            \brief Copy (non learned) clauses from src to this solver.
@@ -351,14 +352,19 @@ namespace sat {
         //
         // -----------------------
     public:
-        bool inconsistent() const override { return m_inconsistent; }
+        // is the state inconsistent?
-        unsigned num_vars() const override { return m_justification.size(); }
+        bool inconsistent() const { return m_inconsistent; }
-        unsigned num_clauses() const override;
+
+        // number of variables and clauses
+        unsigned num_vars() const { return m_justification.size(); }
+        unsigned num_clauses() const;
+
         void num_binary(unsigned& given, unsigned& learned) const;
         unsigned num_restarts() const { return m_restarts; }
-        bool is_external(bool_var v) const override { return m_external[v]; }
+        bool is_external(bool_var v) const { return m_external[v]; }
+        bool is_external(literal l) const { return is_external(l.var()); }
         void set_external(bool_var v) override;
-        void set_non_external(bool_var v) override;
+        void set_non_external(bool_var v);
         bool was_eliminated(bool_var v) const { return m_eliminated[v]; }
         void set_eliminated(bool_var v, bool f) override;
         bool was_eliminated(literal l) const { return was_eliminated(l.var()); }
@@ -368,16 +374,14 @@ namespace sat {
         unsigned scope_lvl() const { return m_scope_lvl; }
         unsigned search_lvl() const { return m_search_lvl; }
         bool  at_search_lvl() const { return m_scope_lvl == m_search_lvl; }
-        bool  at_base_lvl() const override { return m_scope_lvl == 0; }
+        bool  at_base_lvl() const { return m_scope_lvl == 0; }
         lbool value(literal l) const { return m_assignment[l.index()]; }
         lbool value(bool_var v) const { return m_assignment[literal(v, false).index()]; }
         justification get_justification(literal l) const { return m_justification[l.var()]; }
         justification get_justification(bool_var v) const { return m_justification[v]; }
         unsigned lvl(bool_var v) const { return m_justification[v].level(); }
         unsigned lvl(literal l) const { return m_justification[l.var()].level(); }
-        unsigned init_trail_size() const override { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; }
         unsigned trail_size() const { return m_trail.size(); }
-        literal  trail_literal(unsigned i) const override { return m_trail[i]; }
         literal  scope_literal(unsigned n) const { return m_trail[m_scopes[n].m_trail_lim]; }
         void assign(literal l, justification j) {
             TRACE("sat_assign", tout << l << " previous value: " << value(l) << " j: " << j << "\n";);
@@ -430,7 +434,7 @@ namespace sat {
         bool canceled() { return !m_rlimit.inc(); }
         config const& get_config() const { return m_config; }
         drat& get_drat() { return m_drat; }
-        drat* get_drat_ptr() override { return &m_drat;  }
+        drat* get_drat_ptr() { return &m_drat;  }
         void set_incremental(bool b) { m_config.m_incremental = b; }
         bool is_incremental() const { return m_config.m_incremental; }
         extension* get_extension() const override { return m_ext.get(); }
@@ -472,15 +476,37 @@ namespace sat {
         //
         // -----------------------
     public:
-        lbool check(unsigned num_lits = 0, literal const* lits = nullptr) override;
+        lbool check(unsigned num_lits = 0, literal const* lits = nullptr);
 
-        model const & get_model() const override { return m_model; }
+        // retrieve model if solver return sat
+        model const & get_model() const { return m_model; }
         bool model_is_current() const { return m_model_is_current; }
-        literal_vector const& get_core() const override { return m_core; }
+
+        // retrieve core from assumptions
+        literal_vector const& get_core() const { return m_core; }
+
         model_converter const & get_model_converter() const { return m_mc; }
-        void flush(model_converter& mc) override { mc.flush(m_mc); }
+
+        // The following methods are used when converting the state from the SAT solver back
+        // to a set of assertions.
+
+        // retrieve model converter that handles variable elimination and other transformations
+        void flush(model_converter& mc) { mc.flush(m_mc); }
+
+        // size of initial trail containing unit clauses
+        unsigned init_trail_size() const { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; }
+
+        // literal at trail index i
+        literal  trail_literal(unsigned i) const { return m_trail[i]; }
+
+        // collect n-ary clauses
+        clause_vector const& clauses() const { return m_clauses; }
+
+        // collect binary clauses
+        void collect_bin_clauses(svector<bin_clause> & r, bool learned, bool learned_only) const;
+
         void set_model(model const& mdl, bool is_current);
-        char const* get_reason_unknown() const override { return m_reason_unknown.c_str(); }
+        char const* get_reason_unknown() const { return m_reason_unknown.c_str(); }
         bool check_clauses(model const& m) const;
         bool is_assumption(bool_var v) const;
         void set_activity(bool_var v, unsigned act);
@@ -688,7 +714,7 @@ namespace sat {
     public:
         void user_push() override;
         void user_pop(unsigned num_scopes) override;
-        void pop_to_base_level() override;
+        void pop_to_base_level();
         unsigned num_user_scopes() const override { return m_user_scope_literals.size(); }
         unsigned num_scopes() const override { return m_scopes.size(); }
         reslimit& rlimit() { return m_rlimit; }
@@ -788,8 +814,6 @@ namespace sat {
         clause * const * begin_learned() const { return m_learned.begin(); }
         clause * const * end_learned() const { return m_learned.end(); }
         clause_vector const& learned() const { return m_learned; }
-        clause_vector const& clauses() const override { return m_clauses; }
-        void collect_bin_clauses(svector<bin_clause> & r, bool learned, bool learned_only) const override;
 
 
         // -----------------------
@@ -798,11 +822,11 @@ namespace sat {
         //
         // -----------------------
     public:
-        bool check_invariant() const override;
+        bool check_invariant() const;
         void display(std::ostream & out) const;
         void display_watches(std::ostream & out) const;
         void display_watches(std::ostream & out, literal lit) const;
-        void display_dimacs(std::ostream & out) const override;
+        void display_dimacs(std::ostream & out) const;
         std::ostream& display_model(std::ostream& out) const;
         void display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const;
         void display_assignment(std::ostream & out) const;

src/sat/sat_solver/inc_sat_solver.cpp

@@ -42,6 +42,7 @@ Notes:
 #include "sat/sat_params.hpp"
 #include "sat/smt/euf_solver.h"
 #include "sat/tactic/goal2sat.h"
+#include "sat/tactic/sat2goal.h"
 #include "sat/tactic/sat_tactic.h"
 #include "sat/sat_simplifier_params.hpp"
 

src/sat/sat_solver_core.h

@@ -18,14 +18,13 @@ Revision History:
 --*/
 #pragma once
 
-
+#include "sat/sat_model_converter.h"
 #include "sat/sat_types.h"
 
 namespace sat {
 
     class cut_simplifier;
     class extension;
-    class drat;
 
     class solver_core {
     protected:
@@ -34,27 +33,6 @@ namespace sat {
         solver_core(reslimit& l) : m_rlimit(l) {}
         virtual ~solver_core() {}
 
-        virtual void pop_to_base_level() {}
-        virtual bool at_base_lvl() const { return true; }
-
-        // retrieve model if solver return sat
-        virtual model const & get_model() const = 0;
-
-        // retrieve core from assumptions
-        virtual literal_vector const& get_core() const = 0;
-
-        // is the state inconsistent?
-        virtual bool inconsistent() const = 0;
-
-        // number of variables and clauses
-        virtual unsigned num_vars() const = 0;
-        virtual unsigned num_clauses() const = 0;
-
-        // check satisfiability
-        virtual lbool check(unsigned num_lits = 0, literal const* lits = nullptr) = 0;
-
-        virtual char const* get_reason_unknown() const { return "reason unavailable"; }
-
         // add clauses
         virtual void add_clause(unsigned n, literal* lits, status st) = 0;
         void add_clause(literal l1, literal l2, status st) {
@@ -68,18 +46,7 @@ namespace sat {
         // create boolean variable, tagged as external (= true) or internal (can be eliminated).
         virtual bool_var add_var(bool ext) = 0;
 
-        // update parameters
-        virtual void updt_params(params_ref const& p) {}
-        
-
-        virtual bool check_invariant() const { return true; }
-        virtual void display_status(std::ostream& out) const {}
-        virtual void display_dimacs(std::ostream& out) const {}
-
-        virtual bool is_external(bool_var v) const { return true; }
-        bool is_external(literal l) const { return is_external(l.var()); }
         virtual void set_external(bool_var v) {}
-        virtual void set_non_external(bool_var v) {}
         virtual void set_eliminated(bool_var v, bool f) {}
         virtual void set_phase(literal l) { }
 
@@ -96,32 +63,6 @@ namespace sat {
         virtual void       set_extension(extension* e) { if (e) throw default_exception("optional API not supported"); }
 
         virtual cut_simplifier* get_cut_simplifier() { return nullptr; }
-
-        virtual drat* get_drat_ptr() { return nullptr;  }
-
-
-        // The following methods are used when converting the state from the SAT solver back
-        // to a set of assertions. 
-
-        // retrieve model converter that handles variable elimination and other transformations
-        virtual void flush(model_converter& mc) {}
-
-        // size of initial trail containing unit clauses
-        virtual unsigned init_trail_size() const = 0;
-
-        // literal at trail index i
-        virtual literal trail_literal(unsigned i) const = 0;
-
-        // collect n-ary clauses
-        virtual clause_vector const& clauses() const = 0;
-
-        // collect binary clauses
-        typedef std::pair<literal, literal> bin_clause;
-        virtual void collect_bin_clauses(svector<bin_clause> & r, bool learned, bool learned_only) const = 0;
-
-        // collect statistics from sat solver
-        virtual void collect_statistics(statistics & st) const {}
-
     };
 };
 

src/sat/smt/sat_internalizer.h

@@ -0,0 +1,35 @@
+/*++
+Copyright (c) 2020 Microsoft Corporation
+
+Module Name:
+
+    sat_internalizer.h
+
+Abstract:
+
+    Header for SMT theories over SAT solver
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2020-08-25
+
+--*/
+#pragma once
+
+#include "util/sat_literal.h"
+
+namespace sat {
+    class sat_internalizer {
+    public:
+        virtual ~sat_internalizer() {}
+        virtual bool is_bool_op(expr* e) const = 0;
+        virtual literal internalize(expr* e, bool learned) = 0;
+        virtual bool_var to_bool_var(expr* e) = 0;
+        virtual bool_var add_bool_var(expr* e)  = 0;
+        virtual void cache(app* t, literal l) = 0;
+        virtual void uncache(literal l) = 0;
+        virtual void push() = 0;
+        virtual void pop(unsigned n) = 0;
+        virtual void set_expr2var_replay(obj_map<expr, sat::bool_var>* r) = 0;
+    };
+}

src/sat/smt/sat_smt.h

@@ -19,6 +19,7 @@ Author:
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "sat/sat_solver.h"
+#include "sat/smt/sat_internalizer.h"
 
 namespace sat {
     
@@ -28,20 +29,6 @@ namespace sat {
         eframe(expr* e) : m_e(e), m_idx(0) {}
     };
 
-    class sat_internalizer {
-    public:
-        virtual ~sat_internalizer() {}
-        virtual bool is_bool_op(expr* e) const = 0;
-        virtual literal internalize(expr* e, bool learned) = 0;
-        virtual bool_var to_bool_var(expr* e) = 0;
-        virtual bool_var add_bool_var(expr* e)  = 0;
-        virtual void cache(app* t, literal l) = 0;
-        virtual void uncache(literal l) = 0;
-        virtual void push() = 0;
-        virtual void pop(unsigned n) = 0;
-        virtual void set_expr2var_replay(obj_map<expr, sat::bool_var>* r) = 0;
-    };
-    
     class constraint_base {
         extension* m_ex;
         unsigned   m_mem[0];

src/sat/tactic/CMakeLists.txt

@@ -1,6 +1,7 @@
 z3_add_component(sat_tactic
   SOURCES
     goal2sat.cpp
+    sat2goal.cpp
     sat_tactic.cpp
   COMPONENT_DEPENDENCIES
     sat

src/sat/tactic/goal2sat.cpp

@@ -1053,290 +1053,3 @@ sat::sat_internalizer& goal2sat::si(ast_manager& m, params_ref const& p, sat::so
         m_imp = alloc(imp, m, p, t, a2b, dep2asm, default_external);
     return *m_imp;
 }
-
-
-
-sat2goal::mc::mc(ast_manager& m): m(m), m_var2expr(m) {}
-
-void sat2goal::mc::flush_smc(sat::solver_core& s, atom2bool_var const& map) {
-    s.flush(m_smc);
-    m_var2expr.resize(s.num_vars());
-    map.mk_var_inv(m_var2expr);
-    flush_gmc();
-}
-
-void sat2goal::mc::flush_gmc() {
-    sat::literal_vector updates;
-    m_smc.expand(updates);    
-    if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal");
-    // now gmc owns the model converter
-    sat::literal_vector clause;
-    expr_ref_vector tail(m);
-    expr_ref def(m);
-    auto is_literal = [&](expr* e) { expr* r; return is_uninterp_const(e) || (m.is_not(e, r) && is_uninterp_const(r)); };
-    
-    for (unsigned i = 0; i < updates.size(); ++i) {
-        sat::literal l = updates[i];
-        if (l == sat::null_literal) {
-            sat::literal lit0 = clause[0];
-            for (unsigned i = 1; i < clause.size(); ++i) {
-                tail.push_back(lit2expr(~clause[i]));
-            }
-            def = m.mk_or(lit2expr(lit0), mk_and(tail));
-            if (lit0.sign()) {
-                lit0.neg();
-                def = m.mk_not(def);
-            }
-            expr_ref e = lit2expr(lit0);
-            if (is_literal(e))
-                m_gmc->add(e, def);
-            clause.reset();
-            tail.reset();
-        }
-        // short circuit for equivalences:
-        else if (clause.empty() && tail.empty() && 
-                 i + 5 < updates.size() && 
-                 updates[i] == ~updates[i + 3] &&
-                 updates[i + 1] == ~updates[i + 4] && 
-                 updates[i + 2] == sat::null_literal && 
-                 updates[i + 5] == sat::null_literal) {
-            sat::literal r = ~updates[i+1];
-            if (l.sign()) { 
-                l.neg(); 
-                r.neg(); 
-            }
-            
-            expr* a = lit2expr(l);
-            if (is_literal(a))
-                m_gmc->add(a, lit2expr(r));
-            i += 5;
-        }
-        else {
-            clause.push_back(l);
-        }
-    }
-}
- 
-model_converter* sat2goal::mc::translate(ast_translation& translator) {
-    mc* result = alloc(mc, translator.to());
-    result->m_smc.copy(m_smc);
-    result->m_gmc = m_gmc ? dynamic_cast<generic_model_converter*>(m_gmc->translate(translator)) : nullptr;
-    for (expr* e : m_var2expr) {
-        result->m_var2expr.push_back(translator(e));
-    }
-    return result;
-}
-
-void sat2goal::mc::set_env(ast_pp_util* visitor) {
-    flush_gmc();
-    if (m_gmc) m_gmc->set_env(visitor);
-}
-
-void sat2goal::mc::display(std::ostream& out) {
-    flush_gmc();
-    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()(sat::model& md) {
-    m_smc(md);
-}
-
-void sat2goal::mc::operator()(model_ref & md) {
-    // apply externalized model converter
-    CTRACE("sat_mc", m_gmc, m_gmc->display(tout << "before sat_mc\n"); model_v2_pp(tout, *md););
-    if (m_gmc) (*m_gmc)(md);
-    CTRACE("sat_mc", m_gmc, m_gmc->display(tout << "after sat_mc\n"); model_v2_pp(tout, *md););
-}
-
-
-void sat2goal::mc::operator()(expr_ref& fml) {
-    flush_gmc();
-    if (m_gmc) (*m_gmc)(fml);
-}
-
-void sat2goal::mc::insert(sat::bool_var v, expr * atom, bool aux) {
-    SASSERT(!m_var2expr.get(v, nullptr));
-    m_var2expr.reserve(v + 1);
-    m_var2expr.set(v, atom);
-    if (aux) {
-        SASSERT(m.is_bool(atom));
-        if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal");
-        if (is_uninterp_const(atom))
-            m_gmc->hide(to_app(atom)->get_decl());
-    }
-    TRACE("sat_mc", tout << "insert " << v << "\n";);
-}
-
-expr_ref sat2goal::mc::lit2expr(sat::literal l) {
-    sat::bool_var v = l.var();
-    if (!m_var2expr.get(v)) {
-        app* aux = m.mk_fresh_const(nullptr, m.mk_bool_sort());
-        m_var2expr.set(v, aux);
-        if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal");
-        m_gmc->hide(aux->get_decl());
-    }
-    VERIFY(m_var2expr.get(v));
-    expr_ref result(m_var2expr.get(v), m);
-    if (l.sign()) {
-        result = m.mk_not(result);
-    }
-    return result;
-}
-
-
-struct sat2goal::imp {
-
-    typedef mc sat_model_converter;
-
-    ast_manager &           m;
-    expr_ref_vector         m_lit2expr;
-    unsigned long long      m_max_memory;
-    bool                    m_learned;
-    
-    imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m) {
-        updt_params(p);
-    }
-
-    void updt_params(params_ref const & p) {
-        m_learned        = p.get_bool("learned", false);
-        m_max_memory     = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
-    }
-
-    void checkpoint() {
-        if (!m.inc())
-            throw tactic_exception(m.limit().get_cancel_msg());
-        if (memory::get_allocation_size() > m_max_memory)
-            throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
-    }
-
-    expr * lit2expr(ref<mc>& mc, sat::literal l) {
-        if (!m_lit2expr.get(l.index())) {
-            SASSERT(m_lit2expr.get((~l).index()) == 0);
-            expr* aux = mc ? mc->var2expr(l.var()) : nullptr;
-            if (!aux) {
-                aux = m.mk_fresh_const(nullptr, m.mk_bool_sort());
-                if (mc) {
-                    mc->insert(l.var(), aux, true);
-                }
-            }
-            sat::literal lit(l.var(), false);
-            m_lit2expr.set(lit.index(), aux);
-            m_lit2expr.set((~lit).index(), m.mk_not(aux));
-        }        
-        return m_lit2expr.get(l.index());
-    }
-
-    void assert_clauses(ref<mc>& mc, sat::solver_core const & s, sat::clause_vector const& clauses, goal & r, bool asserted) {
-        ptr_buffer<expr> lits;
-        unsigned small_lbd = 3; // s.get_config().m_gc_small_lbd;
-        for (sat::clause* cp : clauses) {
-            checkpoint();
-            lits.reset();
-            sat::clause const & c = *cp;
-            if (asserted || m_learned || c.glue() <= small_lbd) {
-                for (sat::literal l : c) {
-                    lits.push_back(lit2expr(mc, l));
-                }
-                r.assert_expr(m.mk_or(lits));
-            }
-        }
-    }
-
-    void operator()(sat::solver_core & s, atom2bool_var const & map, goal & r, ref<mc> & mc) {
-        if (s.at_base_lvl() && s.inconsistent()) {
-            r.assert_expr(m.mk_false());
-            return;
-        }
-        if (r.models_enabled() && !mc) {
-            mc = alloc(sat_model_converter, m);
-        }
-        if (mc) mc->flush_smc(s, map);
-        m_lit2expr.resize(s.num_vars() * 2);
-        map.mk_inv(m_lit2expr);
-        // collect units
-        unsigned trail_sz = s.init_trail_size();
-        for (unsigned i = 0; i < trail_sz; ++i) {
-            checkpoint();            
-            r.assert_expr(lit2expr(mc, s.trail_literal(i)));
-        }
-        // collect binary clauses
-        svector<sat::solver::bin_clause> bin_clauses;
-        s.collect_bin_clauses(bin_clauses, m_learned, false);
-        for (sat::solver::bin_clause const& bc : bin_clauses) {
-            checkpoint();
-            r.assert_expr(m.mk_or(lit2expr(mc, bc.first), lit2expr(mc, bc.second)));
-        }
-        // collect clauses
-        assert_clauses(mc, s, s.clauses(), r, true);
-
-        auto* ext = s.get_extension();
-        if (ext) {
-            std::function<expr_ref(sat::literal)> l2e = [&](sat::literal lit) {
-                return expr_ref(lit2expr(mc, lit), m);
-            };
-            expr_ref_vector fmls(m);
-            pb::solver* ba = dynamic_cast<pb::solver*>(ext);
-            if (ba) {                
-                ba->to_formulas(l2e, fmls);
-            }
-            else 
-                dynamic_cast<euf::solver*>(ext)->to_formulas(l2e, fmls);            
-            for (expr* f : fmls)
-                r.assert_expr(f);            
-        }
-    }
-
-    void add_clause(ref<mc>& mc, sat::literal_vector const& lits, expr_ref_vector& lemmas) {
-        expr_ref_vector lemma(m);
-        for (sat::literal l : lits) {
-            expr* e = lit2expr(mc, l);
-            if (!e) return;
-            lemma.push_back(e);
-        }
-        lemmas.push_back(mk_or(lemma));
-    }
-
-    void add_clause(ref<mc>& mc, sat::clause const& c, expr_ref_vector& lemmas) {
-        expr_ref_vector lemma(m);
-        for (sat::literal l : c) {
-            expr* e = lit2expr(mc, l);
-            if (!e) return;
-            lemma.push_back(e);
-        }
-        lemmas.push_back(mk_or(lemma));
-    }
-
-};
-
-sat2goal::sat2goal():m_imp(nullptr) {
-}
-
-void sat2goal::collect_param_descrs(param_descrs & r) {
-    insert_max_memory(r);
-    r.insert("learned", CPK_BOOL, "(default: false) collect also learned clauses.");
-}
-
-struct sat2goal::scoped_set_imp {
-    sat2goal * m_owner; 
-    scoped_set_imp(sat2goal * o, sat2goal::imp * i):m_owner(o) {
-        m_owner->m_imp = i;        
-    }
-    ~scoped_set_imp() {
-        m_owner->m_imp = nullptr;
-    }
-};
-
-void sat2goal::operator()(sat::solver_core & t, atom2bool_var const & m, params_ref const & p, 
-                          goal & g, ref<mc> & mc) {
-    imp proc(g.m(), p);
-    scoped_set_imp set(this, &proc);
-    proc(t, m, g, mc);
-}
-
-

src/sat/tactic/goal2sat.h

@@ -29,11 +29,9 @@ Notes:
 #pragma once
 
 #include "tactic/goal.h"
-#include "sat/sat_solver.h"
+#include "sat/sat_solver_core.h"
-#include "tactic/model_converter.h"
-#include "tactic/generic_model_converter.h"
 #include "sat/smt/atom2bool_var.h"
-#include "sat/smt/sat_smt.h"
+#include "sat/smt/sat_internalizer.h"
 
 class goal2sat {
     struct imp;
@@ -77,54 +75,3 @@ public:
     void user_pop(unsigned n);
 
 };
-
-
-class sat2goal {
-    struct imp;
-    imp *  m_imp;
-    struct scoped_set_imp;
-public:
-
-    class mc : public model_converter {
-        ast_manager&            m;
-        sat::model_converter    m_smc;
-        generic_model_converter_ref m_gmc;
-        expr_ref_vector          m_var2expr;
-
-        // flushes from m_smc to m_gmc;
-        void flush_gmc();
-        
-    public:
-        mc(ast_manager& m);
-        ~mc() override {}
-        // flush model converter from SAT solver to this structure.
-        void flush_smc(sat::solver_core& s, atom2bool_var const& map);
-        void operator()(sat::model& m);
-        void operator()(model_ref& md) override;
-        void operator()(expr_ref& fml) override; 
-        model_converter* translate(ast_translation& translator) override;
-        void set_env(ast_pp_util* visitor) override;
-        void display(std::ostream& out) override;
-        void get_units(obj_map<expr, bool>& units) override;
-        expr* var2expr(sat::bool_var v) const { return m_var2expr.get(v, nullptr); }
-        expr_ref lit2expr(sat::literal l);
-        void insert(sat::bool_var v, expr * atom, bool aux);
-    };
-
-    sat2goal();
-
-
-    static void collect_param_descrs(param_descrs & r);
-
-    /**
-       \brief Translate the state of the SAT engine back into a goal.
-       The SAT solver may use variables that are not in \c m. The translator
-       creates fresh boolean AST variables for them. They are stored in fvars.
-       
-       \warning conversion throws a tactic_exception, if it is interrupted (by set_cancel),
-       or memory consumption limit is reached (set with param :max-memory).
-    */
-    void operator()(sat::solver_core & t, atom2bool_var const & m, params_ref const & p, goal & s, ref<mc> & mc);
-    
-};
-

src/sat/tactic/sat2goal.cpp

@@ -0,0 +1,331 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat2goal.cpp
+
+Abstract:
+
+    "Compile" a goal into the SAT engine.
+    Atoms are "abstracted" into boolean variables.
+    The mapping between boolean variables and atoms
+    can be used to convert back the state of the 
+    SAT engine into a goal.
+
+    The idea is to support scenarios such as:
+    1) simplify, blast, convert into SAT, and solve
+    2) convert into SAT, apply SAT for a while, learn new units, and translate back into a goal.
+    3) convert into SAT, apply SAT preprocessor (failed literal propagation, resolution, etc) and translate back into a goal.
+    4) Convert boolean structure into SAT, convert atoms into another engine, combine engines using lazy combination, solve.
+
+Author:
+
+    Leonardo (leonardo) 2011-10-26
+
+Notes:
+
+--*/
+#include "util/ref_util.h"
+#include "ast/ast_smt2_pp.h"
+#include "ast/ast_pp.h"
+#include "ast/ast_smt2_pp.h"
+#include "ast/ast_ll_pp.h"
+#include "ast/pb_decl_plugin.h"
+#include "ast/ast_util.h"
+#include "ast/for_each_expr.h"
+#include "model/model_evaluator.h"
+#include "model/model_v2_pp.h"
+#include "tactic/tactic.h"
+#include "tactic/generic_model_converter.h"
+#include "sat/sat_cut_simplifier.h"
+#include "sat/sat_drat.h"
+#include "sat/tactic/sat2goal.h"
+#include "sat/smt/pb_solver.h"
+#include "sat/smt/euf_solver.h"
+#include "sat/smt/sat_th.h"
+#include "sat/sat_params.hpp"
+#include<sstream>
+
+sat2goal::mc::mc(ast_manager& m): m(m), m_var2expr(m) {}
+
+void sat2goal::mc::flush_smc(sat::solver& s, atom2bool_var const& map) {
+    s.flush(m_smc);
+    m_var2expr.resize(s.num_vars());
+    map.mk_var_inv(m_var2expr);
+    flush_gmc();
+}
+
+void sat2goal::mc::flush_gmc() {
+    sat::literal_vector updates;
+    m_smc.expand(updates);    
+    if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal");
+    // now gmc owns the model converter
+    sat::literal_vector clause;
+    expr_ref_vector tail(m);
+    expr_ref def(m);
+    auto is_literal = [&](expr* e) { expr* r; return is_uninterp_const(e) || (m.is_not(e, r) && is_uninterp_const(r)); };
+    
+    for (unsigned i = 0; i < updates.size(); ++i) {
+        sat::literal l = updates[i];
+        if (l == sat::null_literal) {
+            sat::literal lit0 = clause[0];
+            for (unsigned i = 1; i < clause.size(); ++i) {
+                tail.push_back(lit2expr(~clause[i]));
+            }
+            def = m.mk_or(lit2expr(lit0), mk_and(tail));
+            if (lit0.sign()) {
+                lit0.neg();
+                def = m.mk_not(def);
+            }
+            expr_ref e = lit2expr(lit0);
+            if (is_literal(e))
+                m_gmc->add(e, def);
+            clause.reset();
+            tail.reset();
+        }
+        // short circuit for equivalences:
+        else if (clause.empty() && tail.empty() && 
+                 i + 5 < updates.size() && 
+                 updates[i] == ~updates[i + 3] &&
+                 updates[i + 1] == ~updates[i + 4] && 
+                 updates[i + 2] == sat::null_literal && 
+                 updates[i + 5] == sat::null_literal) {
+            sat::literal r = ~updates[i+1];
+            if (l.sign()) { 
+                l.neg(); 
+                r.neg(); 
+            }
+            
+            expr* a = lit2expr(l);
+            if (is_literal(a))
+                m_gmc->add(a, lit2expr(r));
+            i += 5;
+        }
+        else {
+            clause.push_back(l);
+        }
+    }
+}
+ 
+model_converter* sat2goal::mc::translate(ast_translation& translator) {
+    mc* result = alloc(mc, translator.to());
+    result->m_smc.copy(m_smc);
+    result->m_gmc = m_gmc ? dynamic_cast<generic_model_converter*>(m_gmc->translate(translator)) : nullptr;
+    for (expr* e : m_var2expr) {
+        result->m_var2expr.push_back(translator(e));
+    }
+    return result;
+}
+
+void sat2goal::mc::set_env(ast_pp_util* visitor) {
+    flush_gmc();
+    if (m_gmc) m_gmc->set_env(visitor);
+}
+
+void sat2goal::mc::display(std::ostream& out) {
+    flush_gmc();
+    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()(sat::model& md) {
+    m_smc(md);
+}
+
+void sat2goal::mc::operator()(model_ref & md) {
+    // apply externalized model converter
+    CTRACE("sat_mc", m_gmc, m_gmc->display(tout << "before sat_mc\n"); model_v2_pp(tout, *md););
+    if (m_gmc) (*m_gmc)(md);
+    CTRACE("sat_mc", m_gmc, m_gmc->display(tout << "after sat_mc\n"); model_v2_pp(tout, *md););
+}
+
+
+void sat2goal::mc::operator()(expr_ref& fml) {
+    flush_gmc();
+    if (m_gmc) (*m_gmc)(fml);
+}
+
+void sat2goal::mc::insert(sat::bool_var v, expr * atom, bool aux) {
+    SASSERT(!m_var2expr.get(v, nullptr));
+    m_var2expr.reserve(v + 1);
+    m_var2expr.set(v, atom);
+    if (aux) {
+        SASSERT(m.is_bool(atom));
+        if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal");
+        if (is_uninterp_const(atom))
+            m_gmc->hide(to_app(atom)->get_decl());
+    }
+    TRACE("sat_mc", tout << "insert " << v << "\n";);
+}
+
+expr_ref sat2goal::mc::lit2expr(sat::literal l) {
+    sat::bool_var v = l.var();
+    if (!m_var2expr.get(v)) {
+        app* aux = m.mk_fresh_const(nullptr, m.mk_bool_sort());
+        m_var2expr.set(v, aux);
+        if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal");
+        m_gmc->hide(aux->get_decl());
+    }
+    VERIFY(m_var2expr.get(v));
+    expr_ref result(m_var2expr.get(v), m);
+    if (l.sign()) {
+        result = m.mk_not(result);
+    }
+    return result;
+}
+
+
+struct sat2goal::imp {
+
+    typedef mc sat_model_converter;
+
+    ast_manager &           m;
+    expr_ref_vector         m_lit2expr;
+    unsigned long long      m_max_memory;
+    bool                    m_learned;
+    
+    imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m) {
+        updt_params(p);
+    }
+
+    void updt_params(params_ref const & p) {
+        m_learned        = p.get_bool("learned", false);
+        m_max_memory     = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
+    }
+
+    void checkpoint() {
+        if (!m.inc())
+            throw tactic_exception(m.limit().get_cancel_msg());
+        if (memory::get_allocation_size() > m_max_memory)
+            throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
+    }
+
+    expr * lit2expr(ref<mc>& mc, sat::literal l) {
+        if (!m_lit2expr.get(l.index())) {
+            SASSERT(m_lit2expr.get((~l).index()) == 0);
+            expr* aux = mc ? mc->var2expr(l.var()) : nullptr;
+            if (!aux) {
+                aux = m.mk_fresh_const(nullptr, m.mk_bool_sort());
+                if (mc) {
+                    mc->insert(l.var(), aux, true);
+                }
+            }
+            sat::literal lit(l.var(), false);
+            m_lit2expr.set(lit.index(), aux);
+            m_lit2expr.set((~lit).index(), m.mk_not(aux));
+        }        
+        return m_lit2expr.get(l.index());
+    }
+
+    void assert_clauses(ref<mc>& mc, sat::solver const & s, sat::clause_vector const& clauses, goal & r, bool asserted) {
+        ptr_buffer<expr> lits;
+        unsigned small_lbd = 3; // s.get_config().m_gc_small_lbd;
+        for (sat::clause* cp : clauses) {
+            checkpoint();
+            lits.reset();
+            sat::clause const & c = *cp;
+            if (asserted || m_learned || c.glue() <= small_lbd) {
+                for (sat::literal l : c) {
+                    lits.push_back(lit2expr(mc, l));
+                }
+                r.assert_expr(m.mk_or(lits));
+            }
+        }
+    }
+
+    void operator()(sat::solver & s, atom2bool_var const & map, goal & r, ref<mc> & mc) {
+        if (s.at_base_lvl() && s.inconsistent()) {
+            r.assert_expr(m.mk_false());
+            return;
+        }
+        if (r.models_enabled() && !mc) {
+            mc = alloc(sat_model_converter, m);
+        }
+        if (mc) mc->flush_smc(s, map);
+        m_lit2expr.resize(s.num_vars() * 2);
+        map.mk_inv(m_lit2expr);
+        // collect units
+        unsigned trail_sz = s.init_trail_size();
+        for (unsigned i = 0; i < trail_sz; ++i) {
+            checkpoint();            
+            r.assert_expr(lit2expr(mc, s.trail_literal(i)));
+        }
+        // collect binary clauses
+        svector<sat::solver::bin_clause> bin_clauses;
+        s.collect_bin_clauses(bin_clauses, m_learned, false);
+        for (sat::solver::bin_clause const& bc : bin_clauses) {
+            checkpoint();
+            r.assert_expr(m.mk_or(lit2expr(mc, bc.first), lit2expr(mc, bc.second)));
+        }
+        // collect clauses
+        assert_clauses(mc, s, s.clauses(), r, true);
+
+        auto* ext = s.get_extension();
+        if (ext) {
+            std::function<expr_ref(sat::literal)> l2e = [&](sat::literal lit) {
+                return expr_ref(lit2expr(mc, lit), m);
+            };
+            expr_ref_vector fmls(m);
+            pb::solver* ba = dynamic_cast<pb::solver*>(ext);
+            if (ba) {                
+                ba->to_formulas(l2e, fmls);
+            }
+            else 
+                dynamic_cast<euf::solver*>(ext)->to_formulas(l2e, fmls);            
+            for (expr* f : fmls)
+                r.assert_expr(f);            
+        }
+    }
+
+    void add_clause(ref<mc>& mc, sat::literal_vector const& lits, expr_ref_vector& lemmas) {
+        expr_ref_vector lemma(m);
+        for (sat::literal l : lits) {
+            expr* e = lit2expr(mc, l);
+            if (!e) return;
+            lemma.push_back(e);
+        }
+        lemmas.push_back(mk_or(lemma));
+    }
+
+    void add_clause(ref<mc>& mc, sat::clause const& c, expr_ref_vector& lemmas) {
+        expr_ref_vector lemma(m);
+        for (sat::literal l : c) {
+            expr* e = lit2expr(mc, l);
+            if (!e) return;
+            lemma.push_back(e);
+        }
+        lemmas.push_back(mk_or(lemma));
+    }
+
+};
+
+sat2goal::sat2goal():m_imp(nullptr) {
+}
+
+void sat2goal::collect_param_descrs(param_descrs & r) {
+    insert_max_memory(r);
+    r.insert("learned", CPK_BOOL, "(default: false) collect also learned clauses.");
+}
+
+struct sat2goal::scoped_set_imp {
+    sat2goal * m_owner; 
+    scoped_set_imp(sat2goal * o, sat2goal::imp * i):m_owner(o) {
+        m_owner->m_imp = i;        
+    }
+    ~scoped_set_imp() {
+        m_owner->m_imp = nullptr;
+    }
+};
+
+void sat2goal::operator()(sat::solver & t, atom2bool_var const & m, params_ref const & p,
+                          goal & g, ref<mc> & mc) {
+    imp proc(g.m(), p);
+    scoped_set_imp set(this, &proc);
+    proc(t, m, g, mc);
+}

src/sat/tactic/sat2goal.h

@@ -0,0 +1,84 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat2goal.h
+
+Abstract:
+
+    "Compile" a goal into the SAT engine.
+    Atoms are "abstracted" into boolean variables.
+    The mapping between boolean variables and atoms
+    can be used to convert back the state of the 
+    SAT engine into a goal.
+
+    The idea is to support scenarios such as:
+    1) simplify, blast, convert into SAT, and solve
+    2) convert into SAT, apply SAT for a while, learn new units, and translate back into a goal.
+    3) convert into SAT, apply SAT preprocessor (failed literal propagation, resolution, etc) and translate back into a goal.
+    4) Convert boolean structure into SAT, convert atoms into another engine, combine engines using lazy combination, solve.
+
+Author:
+
+    Leonardo (leonardo) 2011-10-26
+
+Notes:
+
+--*/
+#pragma once
+
+#include "tactic/goal.h"
+#include "sat/sat_model_converter.h"
+#include "sat/sat_solver.h"
+#include "tactic/generic_model_converter.h"
+#include "sat/smt/atom2bool_var.h"
+
+class sat2goal {
+    struct imp;
+    imp *  m_imp;
+    struct scoped_set_imp;
+public:
+
+    class mc : public model_converter {
+        ast_manager&            m;
+        sat::model_converter    m_smc;
+        generic_model_converter_ref m_gmc;
+        expr_ref_vector          m_var2expr;
+
+        // flushes from m_smc to m_gmc;
+        void flush_gmc();
+        
+    public:
+        mc(ast_manager& m);
+        ~mc() override {}
+        // flush model converter from SAT solver to this structure.
+        void flush_smc(sat::solver& s, atom2bool_var const& map);
+        void operator()(sat::model& m);
+        void operator()(model_ref& md) override;
+        void operator()(expr_ref& fml) override; 
+        model_converter* translate(ast_translation& translator) override;
+        void set_env(ast_pp_util* visitor) override;
+        void display(std::ostream& out) override;
+        void get_units(obj_map<expr, bool>& units) override;
+        expr* var2expr(sat::bool_var v) const { return m_var2expr.get(v, nullptr); }
+        expr_ref lit2expr(sat::literal l);
+        void insert(sat::bool_var v, expr * atom, bool aux);
+    };
+
+    sat2goal();
+
+
+    static void collect_param_descrs(param_descrs & r);
+
+    /**
+       \brief Translate the state of the SAT engine back into a goal.
+       The SAT solver may use variables that are not in \c m. The translator
+       creates fresh boolean AST variables for them. They are stored in fvars.
+       
+       \warning conversion throws a tactic_exception, if it is interrupted (by set_cancel),
+       or memory consumption limit is reached (set with param :max-memory).
+    */
+    void operator()(sat::solver & t, atom2bool_var const & m, params_ref const & p, goal & s, ref<mc> & mc);
+    
+};

src/sat/tactic/sat_tactic.cpp

@@ -20,6 +20,7 @@ Notes:
 #include "model/model_v2_pp.h"
 #include "tactic/tactical.h"
 #include "sat/tactic/goal2sat.h"
+#include "sat/tactic/sat2goal.h"
 #include "sat/sat_solver.h"
 #include "sat/sat_params.hpp"
 
@@ -29,7 +30,7 @@ class sat_tactic : public tactic {
         ast_manager &   m;
         goal2sat        m_goal2sat;
         sat2goal        m_sat2goal;
-        scoped_ptr<sat::solver_core>   m_solver;
+        scoped_ptr<sat::solver> m_solver;
         params_ref      m_params;
         
         imp(ast_manager & _m, params_ref const & p):

src/shell/dimacs_frontend.cpp

@@ -26,6 +26,7 @@ Revision History:
 #include "sat/sat_params.hpp"
 #include "sat/sat_solver.h"
 #include "sat/tactic/goal2sat.h"
+#include "sat/tactic/sat2goal.h"
 #include "ast/reg_decl_plugins.h"
 #include "tactic/tactic.h"
 #include "tactic/fd_solver/fd_solver.h"