mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

add translate facility to inc_sat_solver. Limit lemma copying to unit lemmas

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-11-07 10:00:14 -08:00
parent 3d993a4ee1
commit 1758799ef4
4 changed files with 60 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -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) {}

67
src/smt/smt_context.cpp
View file

@ -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<bool_var> 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<bool_var> 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);

5
src/smt/smt_context.h
View file

@ -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<bool_var> b2v, ast_translation& tr);
public:
context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref());

1
src/smt/smt_kernel.h
View file

@ -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());