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

coallesce lambda/quant tracing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-29 08:02:56 -07:00
parent 64e570f159
commit 5509bf248a
2 changed files with 11 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/ast/ast.cpp
View file

@ -2369,6 +2369,15 @@ bool ast_manager::is_pattern(expr const * n, ptr_vector<expr> &args) {
return true;
}
static void trace_quant(std::ostream& strm, quantifier* q) {
strm << (is_lambda(q) ? "[mk-lambda]" : "[mk-quant]")
<< " #" << q->get_id() << " " << q->get_qid();
for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
strm << " #" << q->get_pattern(i)->get_id();
}
strm << " #" << q->get_expr()->get_id() << "\n";
}
quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names,
expr * body, int weight , symbol const & qid, symbol const & skid,
@ -2401,11 +2410,7 @@ quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, s
quantifier * r = register_node(new_node);
if (m_trace_stream && r == new_node) {
*m_trace_stream << "[mk-quant] #" << r->get_id() << " " << qid;
for (unsigned i = 0; i < num_patterns; ++i) {
*m_trace_stream << " #" << patterns[i]->get_id();
}
*m_trace_stream << " #" << body->get_id() << "\n";
trace_quant(*m_trace_stream, r);
}
return r;
@ -2420,7 +2425,7 @@ quantifier * ast_manager::mk_lambda(unsigned num_decls, sort * const * decl_sort
quantifier * new_node = new (mem) quantifier(num_decls, decl_sorts, decl_names, body, s);
quantifier * r = register_node(new_node);
if (m_trace_stream && r == new_node) {
*m_trace_stream << "[mk-lambda] #" << r->get_id() << ": #" << body->get_id() << "\n";
trace_quant(*m_trace_stream, r);
}
return r;
}

2
src/smt/theory_seq.cpp
View file

@ -4581,7 +4581,6 @@ bool theory_seq::lower_bound(expr* _e, rational& lo) const {
if (thi && thi->get_lower(ctx.get_enode(e), _lo)) break;
theory_lra* thr = get_th_arith<theory_lra>(ctx, afid, e);
if (thr && thr->get_lower(ctx.get_enode(e), _lo)) break;
TRACE("seq", tout << "no lower bound " << mk_pp(_e, m) << "\n";);
return false;
}
while (false);
@ -4639,7 +4638,6 @@ bool theory_seq::upper_bound(expr* _e, rational& hi) const {
if (thi && thi->get_upper(ctx.get_enode(e), _hi)) break;
theory_lra* thr = get_th_arith<theory_lra>(ctx, afid, e);
if (thr && thr->get_upper(ctx.get_enode(e), _hi)) break;
TRACE("seq", tout << "no upper bound " << mk_pp(_e, m) << "\n";);
return false;
}
while (false);