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

Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-01-12 08:23:27 -08:00
parent 9635a74e52 4b112d52df
commit 5a90aa9860
6 changed files with 21 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_solver.h
View file

@ -280,6 +280,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);

7
src/tactic/generic_model_converter.cpp
View file

@ -28,6 +28,13 @@ Notes:
#include "model/model_evaluator.h"
void generic_model_converter::add(func_decl * d, expr* e) {
struct entry et(d, e, m, ADD);
VERIFY(d->get_range() == m.get_sort(e));
m_first_idx.insert_if_not_there(et.m_f, m_add_entries.size());
m_add_entries.push_back(et);
}
void generic_model_converter::operator()(model_ref & md) {
TRACE("model_converter", tout << "before generic_model_converter\n"; model_v2_pp(tout, *md); display(tout););
model_evaluator ev(*(md.get()));

6
src/tactic/generic_model_converter.h
View file

@ -47,11 +47,7 @@ public:
void hide(func_decl * f) { m_hide_entries.push_back(entry(f, 0, m, HIDE)); }
void add(func_decl * d, expr* e) {
struct entry et(d, e, m, ADD);
m_first_idx.insert_if_not_there(et.m_f, m_add_entries.size());
m_add_entries.push_back(et);
}
void add(func_decl * d, expr* e);
void add(expr * d, expr* e) { SASSERT(is_app(d) && to_app(d)->get_num_args() == 0); add(to_app(d)->get_decl(), e); }

1
src/tactic/model_converter.cpp
View file

@ -26,6 +26,7 @@ Notes:
void model_converter::display_add(std::ostream& out, ast_manager& m, func_decl* f, expr* e) const {
smt2_pp_environment_dbg env(m);
smt2_pp_environment* _env = m_env ? m_env : &env;
VERIFY(f->get_range() == m.get_sort(e));
ast_smt2_pp(out, f, e, *_env, params_ref(), 0, "model-add") << "\n";
}