enable exposing internal solver state on interrupted solvers

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

src/api/api_model.cpp

@@ -349,10 +349,10 @@ extern "C" {
     //
     // ----------------------------
 
+#if 0
     void Z3_API Z3_del_model(Z3_context c, Z3_model  m) {
         Z3_model_dec_ref(c, m);
     }
-
     unsigned Z3_API Z3_get_model_num_constants(Z3_context c, Z3_model m) {
         return Z3_model_get_num_consts(c, m);
     }
@@ -368,6 +368,7 @@ extern "C" {
     Z3_func_decl Z3_API Z3_get_model_func_decl(Z3_context c, Z3_model m, unsigned i) {
         return Z3_model_get_func_decl(c, m, i);
     }
+#endif
     
 
     unsigned get_model_func_num_entries_core(Z3_context c, Z3_model m, unsigned i) {

src/ast/rewriter/pb2bv_rewriter.cpp

@@ -822,8 +822,7 @@ struct pb2bv_rewriter::imp {
             p.get_bool("keep_cardinality_constraints", false) ||
             p.get_bool("sat.cardinality.solver", false) ||
             p.get_bool("cardinality.solver", false) || 
-            gparams::get_module("sat").get_bool("cardinality.solver", false) ||
+            gparams::get_module("sat").get_bool("cardinality.solver", false);
-            keep_pb();
     }
 
     bool keep_pb() const {

src/sat/card_extension.h

@@ -42,7 +42,8 @@ namespace sat {
             stats() { reset(); }
             void reset() { memset(this, 0, sizeof(*this)); }
         };
-        
+
+    public:        
         class card {
             unsigned       m_index;
             literal        m_lit;
@@ -105,6 +106,7 @@ namespace sat {
             void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); }
             void negate() { m_lits[0].neg(); }
         };
+    protected:
 
         struct ineq {
             literal_vector  m_lits;
@@ -304,6 +306,13 @@ 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_xor(bool_var v, literal_vector const& lits);
+        unsigned num_pb() const { return m_pbs.size(); }
+        pb const&      get_pb(unsigned i) const { return *m_pbs[i]; }
+        unsigned num_card() const { return m_cards.size(); }
+        card const&    get_card(unsigned i) const { return *m_cards[i]; }
+        unsigned num_xor() const { return m_xors.size(); }
+        xor const&     get_xor(unsigned i) const { return *m_xors[i]; }
+
         virtual void propagate(literal l, ext_constraint_idx idx, bool & keep);
         virtual bool resolve_conflict();
         virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r);

src/sat/sat_extension.h

@@ -46,7 +46,7 @@ namespace sat {
         virtual std::ostream& display(std::ostream& out) const = 0;
         virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const = 0;
         virtual void collect_statistics(statistics& st) const = 0;
-        virtual extension* copy(solver* s) = 0;
+        virtual extension* copy(solver* s) = 0;       
         virtual void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) = 0;
     };
 

src/sat/sat_solver.h

@@ -309,7 +309,7 @@ namespace sat {
         }
         void set_par(parallel* p, unsigned id);
         bool canceled() { return !m_rlimit.inc(); }
-        config const& get_config() { return m_config; }
+        config const& get_config() const { return m_config; }
         extension* get_extension() const { return m_ext.get(); }
         void       set_extension(extension* e);
         typedef std::pair<literal, literal> bin_clause;

src/sat/sat_solver/inc_sat_solver.cpp

@@ -66,7 +66,11 @@ class inc_sat_solver : public solver {
     expr_dependency_ref m_dep_core;
     svector<double>     m_weights;
     std::string         m_unknown;
-
+    // access formulas after they have been pre-processed and handled by the sat solver.
+    // this allows to access the internal state of the SAT solver and carry on partial results.
+    bool                m_internalized;           // are formulas internalized?
+    bool                m_internalized_converted; // have internalized formulas been converted back
+    expr_ref_vector     m_internalized_fmls;      // formulas in internalized format
 
     typedef obj_map<expr, sat::literal> dep2asm_t;
 public:
@@ -81,7 +85,10 @@ public:
         m_map(m),
         m_num_scopes(0),
         m_dep_core(m),
-        m_unknown("no reason given") {
+        m_unknown("no reason given"),
+        m_internalized(false), 
+        m_internalized_converted(false), 
+        m_internalized_fmls(m) {
         updt_params(p);
         init_preprocess();
     }
@@ -141,6 +148,8 @@ public:
         if (r != l_true) return r;
         r = internalize_assumptions(sz, assumptions, dep2asm);
         if (r != l_true) return r;
+        m_internalized = true;
+        m_internalized_converted = false;
 
         r = m_solver.check(m_asms.size(), m_asms.c_ptr());
         
@@ -170,8 +179,11 @@ public:
         m_fmls_head_lim.push_back(m_fmls_head);
         if (m_bb_rewriter) m_bb_rewriter->push();
         m_map.push();
+        m_internalized = true;
+        m_internalized_converted = false;
     }
     virtual void pop(unsigned n) {
+        m_internalized = false;
         if (n > m_num_scopes) {   // allow inc_sat_solver to
             n = m_num_scopes;     // take over for another solver.
         }
@@ -204,6 +216,7 @@ public:
     }
     virtual ast_manager& get_manager() const { return m; }
     virtual void assert_expr(expr * t) {
+        m_internalized = false;
         TRACE("goal2sat", tout << mk_pp(t, m) << "\n";);
         m_fmls.push_back(t);
     }
@@ -320,9 +333,18 @@ public:
     virtual void get_labels(svector<symbol> & r) {
     }
     virtual unsigned get_num_assertions() const {
-        return m_fmls.size();
+        const_cast<inc_sat_solver*>(this)->convert_internalized();
+        if (m_internalized && m_internalized_converted) {            
+            return m_internalized_fmls.size();
+        }
+        else {
+            return m_fmls.size();
+        }
     }
     virtual expr * get_assertion(unsigned idx) const {
+        if (m_internalized && m_internalized_converted) {
+            return m_internalized_fmls[idx];
+        }
         return m_fmls[idx];
     }
     virtual unsigned get_num_assumptions() const {
@@ -332,6 +354,32 @@ public:
         return m_asmsf[idx];
     }
 
+    void convert_internalized() {
+        if (!m_internalized) return;
+        sat2goal s2g;
+        model_converter_ref mc;
+        goal g(m, false, false, false);
+        s2g(m_solver, m_map, m_params, g, mc);
+        extract_model();
+        if (!m_model) {
+            m_model = alloc(model, m);
+        }
+        model_ref mdl = m_model;
+        if (m_mc) (*m_mc)(mdl);
+        for (unsigned i = 0; i < mdl->get_num_constants(); ++i) {
+            func_decl* c = mdl->get_constant(i);
+            expr_ref eq(m.mk_eq(m.mk_const(c), mdl->get_const_interp(c)), m);
+            g.assert_expr(eq);
+        }
+        m_internalized_fmls.reset();
+        g.get_formulas(m_internalized_fmls);
+        // g.display(std::cout);
+        m_internalized_converted = true;
+ //       if (mc) mc->display(std::cout << "mc");
+ //       if (m_mc) m_mc->display(std::cout << "m_mc\n");
+ //       if (m_mc0) m_mc0->display(std::cout << "m_mc0\n");
+    }
+
     void init_preprocess() {
         if (m_preprocess) {
             m_preprocess->reset();
@@ -374,7 +422,7 @@ private:
         init_preprocess();
         SASSERT(g->models_enabled());
         SASSERT(!g->proofs_enabled());
-        TRACE("goal2sat", g->display(tout););
+        TRACE("sat", g->display(tout););
         try {
             (*m_preprocess)(g, m_subgoals, m_mc, m_pc, m_dep_core);
         }
@@ -391,7 +439,7 @@ private:
         }
         g = m_subgoals[0];
         expr_ref_vector atoms(m);
-        TRACE("goal2sat", g->display_with_dependencies(tout););
+        TRACE("sat", g->display_with_dependencies(tout););
         m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
         m_goal2sat.get_interpreted_atoms(atoms);
         if (!atoms.empty()) {

src/sat/tactic/goal2sat.cpp

@@ -137,7 +137,7 @@ struct goal2sat::imp {
                 sat::bool_var v = m_solver.mk_var(ext);
                 m_map.insert(t, v);
                 l = sat::literal(v, sign);
-                TRACE("goal2sat", tout << "new_var: " << v << "\n" << mk_ismt2_pp(t, m) << "\n";);
+                TRACE("sat", tout << "new_var: " << v << ": " << mk_ismt2_pp(t, m) << "\n";);
                 if (ext && !is_uninterp_const(t)) {
                     m_interpreted_atoms.push_back(t);
                 }
@@ -993,6 +993,7 @@ struct sat2goal::imp {
     expr_ref_vector         m_lit2expr;
     unsigned long long      m_max_memory;
     bool                    m_learned;
+    unsigned                m_glue;
     
     imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m) {
         updt_params(p);
@@ -1000,6 +1001,7 @@ struct sat2goal::imp {
 
     void updt_params(params_ref const & p) {
         m_learned        = p.get_bool("learned", false);
+        m_glue           = p.get_uint("glue", UINT_MAX);
         m_max_memory     = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
     }
 
@@ -1042,20 +1044,71 @@ struct sat2goal::imp {
         return m_lit2expr.get(l.index());
     }
 
-    void assert_clauses(sat::clause * const * begin, sat::clause * const * end, goal & r) {
+    void assert_pb(goal& r, sat::card_extension::pb const& p) {
+        pb_util pb(m);
+        ptr_buffer<expr> lits;
+        vector<rational> coeffs;
+        for (unsigned i = 0; i < p.size(); ++i) {
+            lits.push_back(lit2expr(p[i].second));
+            coeffs.push_back(rational(p[i].first));
+        }
+        rational k(p.k());
+        expr_ref fml(pb.mk_ge(p.size(), coeffs.c_ptr(), lits.c_ptr(), k), m);
+        
+        if (p.lit() != sat::null_literal) {
+            fml = m.mk_eq(lit2expr(p.lit()), fml);            
+        }
+        r.assert_expr(fml);
+    }
+
+    void assert_card(goal& r, sat::card_extension::card const& c) {
+        pb_util pb(m);
+        ptr_buffer<expr> lits;
+        for (unsigned i = 0; i < c.size(); ++i) {
+            lits.push_back(lit2expr(c[i]));
+        }
+        expr_ref fml(pb.mk_at_most_k(c.size(), lits.c_ptr(), c.k()), m);
+        
+        if (c.lit() != sat::null_literal) {
+            fml = m.mk_eq(lit2expr(c.lit()), fml);            
+        }
+        r.assert_expr(fml);
+    }
+
+    void assert_xor(goal & r, sat::card_extension::xor const& x) {
+        ptr_buffer<expr> lits;
+        for (unsigned i = 0; i < x.size(); ++i) {
+            lits.push_back(lit2expr(x[i]));
+        }
+        expr_ref fml(m.mk_xor(x.size(), lits.c_ptr()), m);
+        
+        if (x.lit() != sat::null_literal) {
+            fml = m.mk_eq(lit2expr(x.lit()), fml);            
+        }
+        r.assert_expr(fml);
+    }
+
+    void assert_clauses(sat::solver const & s, sat::clause * const * begin, sat::clause * const * end, goal & r, bool asserted) {
         ptr_buffer<expr> lits;
         for (sat::clause * const * it = begin; it != end; it++) {
             checkpoint();
             lits.reset();
             sat::clause const & c = *(*it);
             unsigned sz = c.size();
-            for (unsigned i = 0; i < sz; i++) {
+            if (asserted || m_learned || c.glue() <= s.get_config().m_gc_small_lbd) {
-                lits.push_back(lit2expr(c[i]));
+                for (unsigned i = 0; i < sz; i++) {
+                    lits.push_back(lit2expr(c[i]));
+                }
+                r.assert_expr(m.mk_or(lits.size(), lits.c_ptr()));
             }
-            r.assert_expr(m.mk_or(lits.size(), lits.c_ptr()));
         }
     }
 
+    sat::card_extension* get_card_extension(sat::solver const& s) {
+        sat::extension* ext = s.get_extension();
+        return dynamic_cast<sat::card_extension*>(ext);
+    }
+
     void operator()(sat::solver const & s, atom2bool_var const & map, goal & r, model_converter_ref & mc) {
         if (s.inconsistent()) {
             r.assert_expr(m.mk_false());
@@ -1087,9 +1140,22 @@ struct sat2goal::imp {
             r.assert_expr(m.mk_or(lit2expr(it->first), lit2expr(it->second)));
         }
         // collect clauses
-        assert_clauses(s.begin_clauses(), s.end_clauses(), r);
+        assert_clauses(s, s.begin_clauses(), s.end_clauses(), r, true);
-        if (m_learned)
+        assert_clauses(s, s.begin_learned(), s.end_learned(), r, false);
-            assert_clauses(s.begin_learned(), s.end_learned(), r);
+
+        // TBD: collect assertions from plugin
+        sat::card_extension* ext = get_card_extension(s);
+        if (ext) {
+            for (unsigned i = 0; i < ext->num_pb(); ++i) {
+                assert_pb(r, ext->get_pb(i));
+            }
+            for (unsigned i = 0; i < ext->num_card(); ++i) {
+                assert_card(r, ext->get_card(i));
+            }
+            for (unsigned i = 0; i < ext->num_xor(); ++i) {
+                assert_xor(r, ext->get_xor(i));
+            }
+        }
     }
 
 };
@@ -1100,6 +1166,7 @@ sat2goal::sat2goal():m_imp(0) {
 void sat2goal::collect_param_descrs(param_descrs & r) {
     insert_max_memory(r);
     r.insert("learned", CPK_BOOL, "(default: false) collect also learned clauses.");
+    r.insert("glue", CPK_UINT, "(default: max-int) collect learned clauses with glue level below parameter.");
 }
 
 struct sat2goal::scoped_set_imp {

src/solver/solver2tactic.cpp

@@ -150,7 +150,21 @@ public:
             if (m.canceled()) {
                 throw tactic_exception(Z3_CANCELED_MSG);
             }
-            throw tactic_exception(local_solver->reason_unknown().c_str());
+            if (in->models_enabled()) {
+                model_ref mdl;
+                local_solver->get_model(mdl);
+                if (mdl) {
+                    mc = model2model_converter(mdl.get());
+                    mc = concat(fmc.get(), mc.get());
+                }
+            }
+            in->reset();
+            unsigned sz = local_solver->get_num_assertions();
+            for (unsigned i = 0; i < sz; ++i) {
+                in->assert_expr(local_solver->get_assertion(i));
+            }
+            result.push_back(in.get());
+            break;
         }
         local_solver->collect_statistics(m_st);
     }

src/tactic/bv/bit_blaster_model_converter.cpp

@@ -117,8 +117,10 @@ struct bit_blaster_model_converter : public model_converter {
                     SASSERT(is_uninterp_const(bit));
                     func_decl * bit_decl = to_app(bit)->get_decl();
                     expr * bit_val = old_model->get_const_interp(bit_decl);
-                    // remark: if old_model does not assign bit_val, then assume it is false.
+                    if (bit_val == 0) {
-                    if (bit_val != 0 && m().is_true(bit_val))
+                        goto bail;
+                    }
+                    if (m().is_true(bit_val))
                         val++;
                 }
             }
@@ -133,15 +135,50 @@ struct bit_blaster_model_converter : public model_converter {
                     func_decl * bit_decl = to_app(bit)->get_decl();
                     expr * bit_val = old_model->get_const_interp(bit_decl);
                     // remark: if old_model does not assign bit_val, then assume it is false.
-                    if (bit_val != 0 && !util.is_zero(bit_val))
+                    if (bit_val == 0) {
+                        goto bail;
+                    }
+                    if (!util.is_zero(bit_val))
                         val++;
                 }
             }
             new_val = util.mk_numeral(val, bv_sz);
             new_model->register_decl(m_vars.get(i), new_val);
+            continue;
+        bail:
+            new_model->register_decl(m_vars.get(i), mk_bv(bs, *old_model));                                    
         }
     }
 
+    app_ref mk_bv(expr* bs, model& old_model) {
+        bv_util util(m());
+        unsigned bv_sz = to_app(bs)->get_num_args();
+        expr_ref_vector args(m());
+        app_ref result(m());
+        for (unsigned j = 0; j < bv_sz; ++j) {
+            expr * bit = to_app(bs)->get_arg(j);
+            SASSERT(is_uninterp_const(bit));
+            func_decl * bit_decl = to_app(bit)->get_decl();
+            expr * bit_val = old_model.get_const_interp(bit_decl);
+            if (bit_val != 0) {
+                args.push_back(bit_val);
+            }
+            else {
+                args.push_back(bit);
+            }
+        }
+
+        if (TO_BOOL) {
+            SASSERT(is_app_of(bs, m().get_family_id("bv"), OP_MKBV));
+            result = util.mk_bv(bv_sz, args.c_ptr());
+        }
+        else {
+            SASSERT(is_app_of(bs, m().get_family_id("bv"), OP_CONCAT));
+            result = util.mk_concat(bv_sz, args.c_ptr());
+        }
+        return result;
+    }
+
     virtual void operator()(model_ref & md, unsigned goal_idx) {
         SASSERT(goal_idx == 0);
         model * new_model = alloc(model, m());

src/tactic/goal.cpp

@@ -262,6 +262,13 @@ void goal::get_formulas(ptr_vector<expr> & result) {
     }
 }
 
+void goal::get_formulas(expr_ref_vector & result) {
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        result.push_back(form(i));
+    }
+}
+
 void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
     // KLM: don't know why this assertion is no longer true
     // SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));

src/tactic/goal.h

@@ -120,6 +120,7 @@ public:
     void update(unsigned i, expr * f, proof * pr = 0, expr_dependency * dep = 0);
 
     void get_formulas(ptr_vector<expr> & result);
+    void get_formulas(expr_ref_vector & result);
     
     void elim_true();
     void elim_redundancies();

src/tactic/portfolio/default_tactic.cpp

@@ -30,7 +30,6 @@ Notes:
 #include"qffp_tactic.h"
 #include"qfaufbv_tactic.h"
 #include"qfauflia_tactic.h"
-#include"qfufnra_tactic.h"
 
 tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
     tactic * st = using_params(and_then(mk_simplify_tactic(m),
@@ -44,7 +43,6 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
                                         cond(mk_is_nra_probe(),   mk_nra_tactic(m),
                                         cond(mk_is_lira_probe(),  mk_lira_tactic(m, p),
                                         cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p),
-                                        //cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p),
                                              mk_smt_tactic()))))))))))),
                                p);
     return st;

src/tactic/portfolio/fd_solver.cpp

@@ -18,11 +18,13 @@ Notes:
 --*/
 
 #include "fd_solver.h"
+#include "fd_tactic.h"
 #include "tactic.h"
 #include "inc_sat_solver.h"
 #include "enum2bv_solver.h"
 #include "pb2bv_solver.h"
 #include "bounded_int2bv_solver.h"
+#include "solver/solver2tactic.h"
 
 solver * mk_fd_solver(ast_manager & m, params_ref const & p) {
     solver* s = mk_inc_sat_solver(m, p);
@@ -31,3 +33,7 @@ solver * mk_fd_solver(ast_manager & m, params_ref const & p) {
     s = mk_bounded_int2bv_solver(m, p, s);
     return s;
 }
+
+tactic * mk_fd_tactic(ast_manager & m, params_ref const& p) {
+    return mk_solver2tactic(mk_fd_solver(m, p));
+}

src/tactic/portfolio/fd_solver.h

@@ -26,4 +26,5 @@ class solver;
 
 solver * mk_fd_solver(ast_manager & m, params_ref const & p);
 
+
 #endif

src/tactic/portfolio/smt_strategic_solver.cpp

@@ -34,11 +34,11 @@ Notes:
 #include"default_tactic.h"
 #include"ufbv_tactic.h"
 #include"qffp_tactic.h"
-#include"qfufnra_tactic.h"
 #include"horn_tactic.h"
 #include"smt_solver.h"
 #include"inc_sat_solver.h"
 #include"fd_solver.h"
+#include"fd_tactic.h"
 #include"bv_rewriter.h"
 #include"solver2tactic.h"
 
@@ -91,9 +91,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
     else if (logic=="HORN")
         return mk_horn_tactic(m, p);
     else if (logic == "QF_FD")
-        return mk_solver2tactic(mk_fd_solver(m, p));
+        return mk_fd_tactic(m, p);
-    //else if (logic=="QF_UFNRA")
-    //    return mk_qfufnra_tactic(m, p);
     else 
         return mk_default_tactic(m, p);
 }