From 1758799ef49403c7edf5c95d66ccfea9863057d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Nov 2015 10:00:14 -0800 Subject: [PATCH] add translate facility to inc_sat_solver. Limit lemma copying to unit lemmas Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 20 ++++++-- src/smt/smt_context.cpp | 67 +++++++++++++++------------ src/smt/smt_context.h | 5 ++ src/smt/smt_kernel.h | 1 - 4 files changed, 60 insertions(+), 33 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 4f3e1f7db..b0d771ba8 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -32,6 +32,7 @@ Notes: #include "model_smt2_pp.h" #include "filter_model_converter.h" #include "bit_blaster_model_converter.h" +#include "ast_translation.h" // incremental SAT solver. class inc_sat_solver : public solver { @@ -94,9 +95,22 @@ public: virtual ~inc_sat_solver() {} - virtual solver* translate(ast_manager& m, params_ref const& p) { - UNREACHABLE(); - return 0; + virtual solver* translate(ast_manager& dst_m, params_ref const& p) { + ast_translation tr(m, dst_m); + if (m_num_scopes > 0) { + throw default_exception("Cannot translate sat solver at non-base level"); + } + inc_sat_solver* result = alloc(inc_sat_solver, dst_m, p); + expr_ref fml(dst_m); + for (unsigned i = 0; i < m_fmls.size(); ++i) { + fml = tr(m_fmls[i].get()); + result->m_fmls.push_back(fml); + } + for (unsigned i = 0; i < m_asmsf.size(); ++i) { + fml = tr(m_asmsf[i].get()); + result->m_asmsf.push_back(fml); + } + return result; } virtual void set_progress_callback(progress_callback * callback) {} diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index c55243cfd..39ccbdbb2 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -99,6 +99,36 @@ namespace smt { m_model_generator->set_context(this); } + literal context::translate_literal( + literal lit, context& src_ctx, context& dst_ctx, + vector b2v, ast_translation& tr) { + ast_manager& dst_m = dst_ctx.get_manager(); + ast_manager& src_m = src_ctx.get_manager(); + expr_ref dst_f(dst_m); + + SASSERT(lit != false_literal && lit != true_literal); + bool_var v = b2v.get(lit.var(), null_bool_var); + if (v == null_bool_var) { + expr* e = src_ctx.m_bool_var2expr.get(lit.var(), 0); + SASSERT(e); + dst_f = tr(e); + v = dst_ctx.get_bool_var_of_id_option(dst_f->get_id()); + if (v != null_bool_var) { + } + else if (src_m.is_not(e) || src_m.is_and(e) || src_m.is_or(e) || + src_m.is_iff(e) || src_m.is_ite(e)) { + v = dst_ctx.mk_bool_var(dst_f); + } + else { + dst_ctx.internalize_formula(dst_f, false); + v = dst_ctx.get_bool_var(dst_f); + } + b2v.setx(lit.var(), v, null_bool_var); + } + return literal(v, lit.sign()); + } + + void context::copy(context& src_ctx, context& dst_ctx) { ast_manager& dst_m = dst_ctx.get_manager(); ast_manager& src_m = src_ctx.get_manager(); @@ -136,36 +166,15 @@ namespace smt { dst_ctx.internalize_assertions(); vector b2v; - expr_ref dst_f(dst_m); -#define TRANSLATE(_lin, _lout) { \ - SASSERT(_lin != false_literal && _lin != true_literal); \ - bool_var v = b2v.get(_lin.var(), null_bool_var); \ - if (v == null_bool_var) { \ - expr* e = src_ctx.m_bool_var2expr.get(_lin.var(), 0); \ - SASSERT(e); \ - dst_f = tr(e); \ - v = dst_ctx.get_bool_var_of_id_option(dst_f->get_id()); \ - if (v != null_bool_var) { \ - } \ - else if (src_m.is_not(e) || src_m.is_and(e) || src_m.is_or(e) || \ - src_m.is_iff(e) || src_m.is_ite(e)) { \ - v = dst_ctx.mk_bool_var(dst_f); \ - } \ - else { \ - dst_ctx.internalize_formula(dst_f, false); \ - v = dst_ctx.get_bool_var(dst_f); \ - } \ - b2v.setx(_lin.var(), v, null_bool_var); \ - } \ - _lout = literal(v, _lin.sign()); \ - } \ +#define TRANSLATE(_lit) translate_literal(_lit, src_ctx, dst_ctx, b2v, tr) for (unsigned i = 0; i < src_ctx.m_assigned_literals.size(); ++i) { literal lit; - TRANSLATE(src_ctx.m_assigned_literals[i], lit); + lit = TRANSLATE(src_ctx.m_assigned_literals[i]); dst_ctx.mk_clause(1, &lit, 0, CLS_AUX, 0); } +#if 0 literal_vector lits; expr_ref_vector cls(src_m); for (unsigned i = 0; i < src_ctx.m_lemmas.size(); ++i) { @@ -174,9 +183,8 @@ namespace smt { clause& src_cls = *src_ctx.m_lemmas[i]; unsigned sz = src_cls.get_num_literals(); for (unsigned j = 0; j < sz; ++j) { - literal lit = src_cls.get_literal(j), lout; - TRANSLATE(lit, lout); - lits.push_back(lout); + literal lit = TRANSLATE(src_cls.get_literal(j)); + lits.push_back(lit); } dst_ctx.mk_clause(lits.size(), lits.c_ptr(), 0, src_cls.get_kind(), 0); } @@ -192,12 +200,13 @@ namespace smt { for (; it2 != end2; ++it2) { literal l2 = *it2; if (l1.index() < l2.index()) { - TRANSLATE(neg_l1, ls[0]); - TRANSLATE(l2, ls[1]); + ls[0] = TRANSLATE(neg_l1); + ls[1] = TRANSLATE(l2); dst_ctx.mk_clause(2, ls, 0, CLS_AUX, 0); } } } +#endif TRACE("smt_context", src_ctx.display(tout); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 8fb3504ad..08d68c723 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1329,6 +1329,11 @@ namespace smt { // copy plugins into a fresh context. void copy_plugins(context& src, context& dst); + static literal translate_literal( + literal lit, context& src_ctx, context& dst_ctx, + vector b2v, ast_translation& tr); + + public: context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref()); diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index b2d880532..a7a467964 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -45,7 +45,6 @@ namespace smt { class kernel { struct imp; imp * m_imp; - kernel(): m_imp(0) {} public: kernel(ast_manager & m, smt_params & fp, params_ref const & p = params_ref());