mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 08:51:55 +00:00
Code Activity

updates to model generation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-01-11 11:20:23 -08:00
parent c80f34102f
commit 1c2966f8e9
6 changed files with 21 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_solver.h
View file

@ -279,6 +279,7 @@ namespace sat {
unsigned lvl(bool_var v) const { return m_level[v]; }
unsigned lvl(literal l) const { return m_level[l.var()]; }
unsigned init_trail_size() const { return at_base_lvl() ? m_trail.size() : m_scopes[0].m_trail_lim; }
literal trail_literal(unsigned i) const { return m_trail[i]; }
void assign(literal l, justification j) {
TRACE("sat_assign", tout << l << " previous value: " << value(l) << "\n";);
switch (value(l)) {

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

@ -787,21 +787,23 @@ private:
}
m_model = md;
if (m_sat_mc) {
(*m_sat_mc)(m_model);
}
if (m_bb_rewriter.get() && !m_bb_rewriter->const2bits().empty()) {
m_mc0 = concat(m_mc0.get(), mk_bit_blaster_model_converter(m, m_bb_rewriter->const2bits()));
}
if (m_mc0) {
if (m_mc0) {
(*m_mc0)(m_model);
}
SASSERT(m_model);
DEBUG_CODE(
for (unsigned i = 0; i < m_fmls.size(); ++i) {
for (expr * f : m_fmls) {
expr_ref tmp(m);
if (m_model->eval(m_fmls[i].get(), tmp, true)) {
if (m_model->eval(f, tmp, true)) {
CTRACE("sat", !m.is_true(tmp),
tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m)
<< " to " << tmp << "\n";
tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n";
model_smt2_pp(tout, m, *(m_model.get()), 0););
SASSERT(m.is_true(tmp));
}

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

@ -1139,20 +1139,12 @@ struct sat2goal::imp {
if (mc) mc->flush_smc(s);
init_lit2expr(s, map, mc);
// collect units
unsigned num_vars = s.num_vars();
for (sat::bool_var v = 0; v < num_vars; v++) {
unsigned trail_sz = s.init_trail_size();
for (unsigned i = 0; i < trail_sz; ++i) {
checkpoint();
switch (s.value(v)) {
case l_true:
r.assert_expr(lit2expr(mc, sat::literal(v, false)));
break;
case l_false:
r.assert_expr(lit2expr(mc, sat::literal(v, true)));
break;
case l_undef:
break;
}
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);