mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

simplify and strenghten some code

Browse source
This commit is contained in:
Simon Cruanes 2017-12-25 17:01:53 +01:00
parent 0c753aa86a
commit 35c802d869
1 changed files with 12 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/smt/theory_recfun.cpp
View file

@ -193,14 +193,14 @@ namespace smt {
app_ref dlimit = m_util->mk_depth_limit_pred(get_max_depth()); app_ref dlimit = m_util->mk_depth_limit_pred(get_max_depth());
ctx.internalize(dlimit, false); ctx.internalize(dlimit, false);
c.push_back(~ ctx.get_literal(dlimit)); c.push_back(~ ctx.get_literal(dlimit));
SASSERT(ctx.get_assignment(ctx.get_literal(dlimit)) == l_true); //SASSERT(ctx.get_assignment(ctx.get_literal(dlimit)) == l_true);
} }
for (auto& kv : m_guards) { for (auto& kv : m_guards) {
expr * g = & kv.get_key(); expr * g = & kv.get_key();
c.push_back(~ ctx.get_literal(g)); c.push_back(~ ctx.get_literal(g));
} }
DEBUG("max-depth limit: add clause " << pp_lits(ctx, c.size(), c.c_ptr())); DEBUG("max-depth limit: add clause " << pp_lits(ctx, c.size(), c.c_ptr()));
SASSERT(std::all_of(c.begin(), c.end(), [&](literal & l) { return ctx.get_assignment(l) == l_false; })); // conflict //SASSERT(std::all_of(c.begin(), c.end(), [&](literal & l) { return ctx.get_assignment(l) == l_false; })); // conflict
m_q_clauses.push_back(std::move(c)); m_q_clauses.push_back(std::move(c));
} }
@ -254,30 +254,21 @@ namespace smt {
void theory_recfun::assert_macro_axiom(case_expansion & e) { void theory_recfun::assert_macro_axiom(case_expansion & e) {
DEBUG("assert_macro_axiom " << pp_case_expansion(e,m())); DEBUG("assert_macro_axiom " << pp_case_expansion(e,m()));
SASSERT(e.m_def->is_fun_macro()); SASSERT(e.m_def->is_fun_macro());
expr * lhs = e.m_lhs; expr_ref lhs(e.m_lhs, m());
context & ctx = get_context(); context & ctx = get_context();
auto & vars = e.m_def->get_vars(); auto & vars = e.m_def->get_vars();
// substitute `e.args` into the macro RHS // substitute `e.args` into the macro RHS
expr * rhs = apply_args(vars, e.m_args, e.m_def->get_macro_rhs()); expr_ref rhs(apply_args(vars, e.m_args, e.m_def->get_macro_rhs()), m());
DEBUG("macro expansion yields" << mk_pp(rhs,m())); DEBUG("macro expansion yields" << mk_pp(rhs,m()));
// now build the axiom `lhs = rhs` // now build the axiom `lhs = rhs`
ctx.internalize(rhs, false); ctx.internalize(rhs, false);
DEBUG("adding axiom: " << mk_pp(lhs, m()) << " = " << mk_pp(rhs, m())); // add unit clause `lhs=rhs`
if (m().proofs_enabled()) { literal l(mk_eq(lhs, rhs, true));
// add unit clause `lhs=rhs` ctx.mark_as_relevant(l);
literal l(mk_eq(lhs, rhs, true)); literal_vector lits;
ctx.mark_as_relevant(l); lits.push_back(l);
literal lits[1] = {l}; DEBUG("assert_macro_axiom: " << pp_lits(ctx, lits.size(), lits.c_ptr()));
ctx.mk_th_axiom(get_id(), 1, lits); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
}
else {
//region r;
enode * e_lhs = ctx.get_enode(lhs);
enode * e_rhs = ctx.get_enode(rhs);
// TODO: proper justification
//justification * js = ctx.mk_justification(
ctx.assign_eq(e_lhs, e_rhs, eq_justification());
}
} }
void theory_recfun::assert_case_axioms(case_expansion & e) { void theory_recfun::assert_case_axioms(case_expansion & e) {
@ -368,7 +359,7 @@ namespace smt {
literal l(mk_eq(lhs, rhs, true)); literal l(mk_eq(lhs, rhs, true));
ctx.mark_as_relevant(l); ctx.mark_as_relevant(l);
clause.push_back(l); clause.push_back(l);
DEBUG("assert_body_axiom " << pp_lits(get_context(), clause.size(), clause.c_ptr())); DEBUG("assert_body_axiom " << pp_lits(ctx, clause.size(), clause.c_ptr()));
ctx.mk_th_axiom(get_id(), clause.size(), clause.c_ptr()); ctx.mk_th_axiom(get_id(), clause.size(), clause.c_ptr());
} }