mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 19:53:34 +00:00
Code Activity

fix model bugs

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-01-13 16:12:38 -08:00
parent 5a90aa9860
commit d79c33fb21
6 changed files with 43 additions and 46 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/ast/expr2var.cpp
View file

@ -58,11 +58,9 @@ void expr2var::display(std::ostream & out) const {
}
void expr2var::mk_inv(expr_ref_vector & var2expr) const {
obj_map<expr, var>::iterator it = m_mapping.begin();
obj_map<expr, var>::iterator end = m_mapping.end();
for (; it != end; ++it) {
expr * t = it->m_key;
var x = it->m_value;
for (auto & kv : m_mapping) {
expr * t = kv.m_key;
var x = kv.m_value;
if (x >= var2expr.size())
var2expr.resize(x+1, 0);
var2expr.set(x, t);

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

@ -533,11 +533,11 @@ private:
TRACE("sat", g->display_with_dependencies(tout););
// ensure that if goal is already internalized, then import mc from m_solver.
if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m);
m_sat_mc->flush_smc(m_solver);
m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, is_incremental(), is_lemma);
m_goal2sat.get_interpreted_atoms(atoms);
if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m);
m_sat_mc->flush_smc(m_solver, m_map);
if (!atoms.empty()) {
std::stringstream strm;
strm << "interpreted atoms sent to SAT solver " << atoms;
@ -798,16 +798,20 @@ private:
}
SASSERT(m_model);
DEBUG_CODE(
for (expr * f : m_fmls) {
expr_ref tmp(m);
if (m_model->eval(f, tmp, true)) {
CTRACE("sat", !m.is_true(tmp),
tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n";
model_smt2_pp(tout, m, *(m_model.get()), 0););
SASSERT(m.is_true(tmp));
IF_VERBOSE(0, verbose_stream() << "Verifying solution\n";);
for (expr * f : m_fmls) {
expr_ref tmp(m);
if (m_model->eval(f, tmp, true)) {
CTRACE("sat", !m.is_true(tmp),
tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n";
model_smt2_pp(tout, m, *(m_model.get()), 0););
if (!m.is_true(tmp)) {
IF_VERBOSE(0, verbose_stream() << "failed to verify: " << tmp << "\n";);
IF_VERBOSE(0, verbose_stream() << m_params << "\n";);
}
});
VERIFY(m.is_true(tmp));
}
}
}
};

6
src/sat/tactic/atom2bool_var.cpp
View file

@ -31,6 +31,12 @@ void atom2bool_var::mk_inv(expr_ref_vector & lit2expr) const {
}
}
void atom2bool_var::mk_var_inv(app_ref_vector & var2expr) const {
for (auto const& kv : m_mapping) {
var2expr.set(kv.m_value, to_app(kv.m_key));
}
}
sat::bool_var atom2bool_var::to_bool_var(expr * n) const {
sat::bool_var v = sat::null_bool_var;
m_mapping.find(n, v);

1
src/sat/tactic/atom2bool_var.h
View file

@ -31,6 +31,7 @@ public:
void insert(expr * n, sat::bool_var v) { expr2var::insert(n, v); }
sat::bool_var to_bool_var(expr * n) const;
void mk_inv(expr_ref_vector & lit2expr) const;
void mk_var_inv(app_ref_vector & var2expr) const;
// return true if the mapping contains uninterpreted atoms.
bool interpreted_atoms() const { return expr2var::interpreted_vars(); }
};

46
src/sat/tactic/goal2sat.cpp
View file

@ -880,8 +880,10 @@ void goal2sat::get_interpreted_atoms(expr_ref_vector& atoms) {
sat2goal::mc::mc(ast_manager& m): m(m), m_var2expr(m) {}
void sat2goal::mc::flush_smc(sat::solver& s) {
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);
}
void sat2goal::mc::flush_gmc() {
@ -941,6 +943,7 @@ void sat2goal::mc::operator()(model_ref & md) {
// create a SAT model using md
sat::model sat_md;
expr_ref val(m);
VERIFY(!m_var2expr.empty());
for (expr * atom : m_var2expr) {
if (!atom) {
sat_md.push_back(l_undef);
@ -1011,7 +1014,6 @@ expr_ref sat2goal::mc::lit2expr(sat::literal l) {
struct sat2goal::imp {
typedef mc sat_model_converter;
typedef ref<sat_model_converter> sat_model_converter_ref;
ast_manager & m;
expr_ref_vector m_lit2expr;
@ -1034,23 +1036,7 @@ struct sat2goal::imp {
throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
}
void init_lit2expr(sat::solver const & s, atom2bool_var const & map, sat_model_converter_ref & mc) {
unsigned num_vars = s.num_vars();
m_lit2expr.resize(num_vars * 2);
map.mk_inv(m_lit2expr);
if (mc) {
for (sat::bool_var v = 0; v < num_vars; v++) {
checkpoint();
sat::literal l(v, false);
if (m_lit2expr.get(l.index()) && !mc->var2expr(v)) {
mc->insert(v, to_app(m_lit2expr.get(l.index())), false);
SASSERT(m_lit2expr.get((~l).index()));
}
}
}
}
expr * lit2expr(sat_model_converter_ref& mc, sat::literal l) {
expr * lit2expr(ref<mc>& mc, sat::literal l) {
if (!m_lit2expr.get(l.index())) {
SASSERT(m_lit2expr.get((~l).index()) == 0);
app* aux = mc ? mc->var2expr(l.var()) : nullptr;
@ -1059,13 +1045,14 @@ struct sat2goal::imp {
if (mc)
mc->insert(l.var(), aux, true);
}
m_lit2expr.set(l.index(), aux);
m_lit2expr.set((~l).index(), m.mk_not(aux));
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_pb(sat_model_converter_ref& mc, goal& r, sat::ba_solver::pb const& p) {
void assert_pb(ref<mc>& mc, goal& r, sat::ba_solver::pb const& p) {
pb_util pb(m);
ptr_buffer<expr> lits;
vector<rational> coeffs;
@ -1082,7 +1069,7 @@ struct sat2goal::imp {
r.assert_expr(fml);
}
void assert_card(sat_model_converter_ref& mc, goal& r, sat::ba_solver::card const& c) {
void assert_card(ref<mc>& mc, goal& r, sat::ba_solver::card const& c) {
pb_util pb(m);
ptr_buffer<expr> lits;
for (sat::literal l : c) {
@ -1096,7 +1083,7 @@ struct sat2goal::imp {
r.assert_expr(fml);
}
void assert_xor(sat_model_converter_ref& mc, goal & r, sat::ba_solver::xor const& x) {
void assert_xor(ref<mc>& mc, goal & r, sat::ba_solver::xor const& x) {
ptr_buffer<expr> lits;
for (sat::literal l : x) {
lits.push_back(lit2expr(mc, l));
@ -1109,7 +1096,7 @@ struct sat2goal::imp {
r.assert_expr(fml);
}
void assert_clauses(sat_model_converter_ref& mc, sat::solver const & s, sat::clause_vector const& clauses, goal & r, bool asserted) {
void assert_clauses(ref<mc>& mc, sat::solver const & s, sat::clause_vector const& clauses, goal & r, bool asserted) {
ptr_buffer<expr> lits;
for (sat::clause* cp : clauses) {
checkpoint();
@ -1136,8 +1123,9 @@ struct sat2goal::imp {
if (r.models_enabled() && !mc) {
mc = alloc(sat_model_converter, m);
}
if (mc) mc->flush_smc(s);
init_lit2expr(s, map, mc);
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) {
@ -1173,7 +1161,7 @@ struct sat2goal::imp {
}
}
void add_clause(sat_model_converter_ref& mc, sat::literal_vector const& lits, expr_ref_vector& lemmas) {
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);
@ -1183,7 +1171,7 @@ struct sat2goal::imp {
lemmas.push_back(mk_or(lemma));
}
void add_clause(sat_model_converter_ref& mc, sat::clause const& c, expr_ref_vector& lemmas) {
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);

2
src/sat/tactic/goal2sat.h
View file

@ -88,7 +88,7 @@ public:
mc(ast_manager& m);
virtual ~mc() {}
// flush model converter from SAT solver to this structure.
void flush_smc(sat::solver& s);
void flush_smc(sat::solver& s, atom2bool_var const& map);
void operator()(model_ref& md) override;
void operator()(expr_ref& fml) override;
model_converter* translate(ast_translation& translator) override;