mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

ctx

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-18 09:02:20 -07:00
parent bd53fa801e
commit 2f5f546990
1 changed files with 8 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/smt/theory_recfun.cpp
View file

@ -106,7 +106,7 @@ namespace smt {
* body-expand it. * body-expand it.
*/ */
void theory_recfun::relevant_eh(app * n) { void theory_recfun::relevant_eh(app * n) {
SASSERT(get_context().relevancy()); SASSERT(ctx().relevancy());
if (u().is_defined(n)) { if (u().is_defined(n)) {
TRACEFN("relevant_eh: (defined) " << mk_pp(n, m())); TRACEFN("relevant_eh: (defined) " << mk_pp(n, m()));
case_expansion e(u(), n); case_expansion e(u(), n);
@ -140,11 +140,10 @@ namespace smt {
} }
void theory_recfun::propagate() { void theory_recfun::propagate() {
context & ctx = get_context();
for (literal_vector & c : m_q_clauses) { for (literal_vector & c : m_q_clauses) {
TRACEFN("add axiom " << pp_lits(ctx, c)); TRACEFN("add axiom " << pp_lits(ctx(), c));
ctx.mk_th_axiom(get_id(), c.size(), c.c_ptr()); ctx().mk_th_axiom(get_id(), c.size(), c.c_ptr());
} }
m_q_clauses.clear(); m_q_clauses.clear();
@ -169,20 +168,19 @@ namespace smt {
void theory_recfun::max_depth_conflict() { void theory_recfun::max_depth_conflict() {
TRACEFN("max-depth conflict"); TRACEFN("max-depth conflict");
context & ctx = get_context();
literal_vector c; literal_vector c;
// make clause `depth_limit => V_{g : guards} ~ g` // make clause `depth_limit => V_{g : guards} ~ g`
{ {
// first literal must be the depth limit one // first literal must be the depth limit one
app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth()); app_ref dlimit = m_util.mk_depth_limit_pred(get_max_depth());
c.push_back(~mk_literal(dlimit)); c.push_back(~mk_literal(dlimit));
SASSERT(ctx.get_assignment(c.back()) == l_true); SASSERT(ctx().get_assignment(c.back()) == l_true);
} }
for (auto& kv : m_guards) { for (auto& kv : m_guards) {
c.push_back(~ mk_literal(&kv.get_key())); c.push_back(~ mk_literal(kv.m_key));
} }
TRACEFN("max-depth limit: add clause " << pp_lits(ctx, c)); TRACEFN("max-depth limit: add clause " << pp_lits(ctx(), c));
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));
} }
@ -222,7 +220,7 @@ namespace smt {
var_subst subst(m(), true); var_subst subst(m(), true);
expr_ref new_body(m()); expr_ref new_body(m());
new_body = subst(e, args.size(), args.c_ptr()); new_body = subst(e, args.size(), args.c_ptr());
get_context().get_rewriter()(new_body); // simplify ctx().get_rewriter()(new_body); // simplify
return new_body; return new_body;
} }