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

ported VCC trace streams

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-02 09:08:47 -08:00
parent 80405dbd62
commit 288a96610f
21 changed files with 149 additions and 160 deletions
Download patch file Download diff file Expand all files Collapse all files

33
src/smt/mam.cpp
View file

@ -1824,7 +1824,6 @@ namespace smt {
backtrack_stack m_backtrack_stack;
unsigned m_top;
const instruction * m_pc;
std::ostream* m_trace_stream;
// auxiliary temporary variables
unsigned m_max_generation; // the maximum generation of an app enode processed.
@ -1855,10 +1854,9 @@ namespace smt {
void update_max_generation(enode * n) {
m_max_generation = std::max(m_max_generation, n->get_generation());
#ifndef SMTCOMP
if (m_trace_stream != NULL)
if (m_ast_manager.has_trace_stream())
m_used_enodes.push_back(n);
#endif
}
// We have to provide the number of expected arguments because we have flat-assoc applications such as +.
@ -1965,12 +1963,11 @@ namespace smt {
#define INIT_ARGS_SIZE 16
public:
interpreter(context & ctx, mam & m, bool use_filters, std::ostream *trace_stream):
interpreter(context & ctx, mam & m, bool use_filters):
m_context(ctx),
m_ast_manager(ctx.get_manager()),
m_mam(m),
m_use_filters(use_filters),
m_trace_stream(trace_stream) {
m_use_filters(use_filters) {
m_args.resize(INIT_ARGS_SIZE, 0);
}
@ -2266,12 +2263,12 @@ namespace smt {
m_pattern_instances.reset();
m_pattern_instances.push_back(n);
m_max_generation = n->get_generation();
#ifndef SMTCOMP
if (m_trace_stream != NULL) {
if (m_ast_manager.has_trace_stream()) {
m_used_enodes.reset();
m_used_enodes.push_back(n);
}
#endif
m_pc = t->get_root();
m_registers[0] = n;
m_top = 0;
@ -2638,10 +2635,10 @@ namespace smt {
}
backtrack_point & bp = m_backtrack_stack[m_top - 1];
m_max_generation = bp.m_old_max_generation;
#ifndef SMTCOMP
if (m_trace_stream != NULL)
if (m_ast_manager.has_trace_stream())
m_used_enodes.shrink(bp.m_old_used_enodes_size);
#endif
TRACE("mam_int", tout << "backtrack top: " << bp.m_instr << " " << *(bp.m_instr) << "\n";);
#ifdef _PROFILE_MAM
if (bp.m_instr->m_opcode != CHOOSE) // CHOOSE has a different status. It is a control flow backtracking.
@ -3759,14 +3756,14 @@ namespace smt {
}
public:
mam_impl(context & ctx, bool use_filters, std::ostream *trace):
mam(ctx, trace),
mam_impl(context & ctx, bool use_filters):
mam(ctx),
m_ast_manager(ctx.get_manager()),
m_use_filters(use_filters),
m_trail_stack(*this),
m_ct_manager(m_lbl_hasher, m_trail_stack),
m_compiler(ctx, m_ct_manager, m_lbl_hasher, use_filters),
m_interpreter(ctx, *this, use_filters, trace),
m_interpreter(ctx, *this, use_filters),
m_trees(m_ast_manager, m_compiler, m_trail_stack),
m_region(m_trail_stack.get_region()),
m_r1(0),
@ -3980,8 +3977,8 @@ namespace smt {
}
};
mam * mk_mam(context & ctx, std::ostream *trace) {
return alloc(mam_impl, ctx, true, trace);
mam * mk_mam(context & ctx) {
return alloc(mam_impl, ctx, true);
}
};

8
src/smt/mam.h
View file

@ -29,11 +29,9 @@ namespace smt {
class mam {
protected:
context & m_context;
std::ostream * m_trace_stream;
public:
mam(context & ctx, std::ostream *trace):
m_context(ctx),
m_trace_stream(trace) {
mam(context & ctx):
m_context(ctx) {
}
virtual ~mam() {
@ -68,7 +66,7 @@ namespace smt {
#endif
};
mam * mk_mam(context & ctx, std::ostream *trace);
mam * mk_mam(context & ctx);
};
#endif /* _MAM_H_ */

35
src/smt/qi_queue.cpp
View file

@ -26,7 +26,7 @@ Revision History:
namespace smt {
qi_queue::qi_queue(quantifier_manager & qm, context & ctx, qi_params & params, std::ostream *trace_stream):
qi_queue::qi_queue(quantifier_manager & qm, context & ctx, qi_params & params):
m_qm(qm),
m_context(ctx),
m_manager(m_context.get_manager()),
@ -37,7 +37,6 @@ namespace smt {
m_parser(m_manager),
m_evaluator(m_manager),
m_subst(m_manager),
m_trace_stream(trace_stream),
m_instances(m_manager) {
init_parser_vars();
m_vals.resize(15, 0.0f);
@ -173,25 +172,23 @@ namespace smt {
}
void qi_queue::display_instance_profile(fingerprint * f, quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned proof_id, unsigned generation) {
#ifndef SMTCOMP
if (m_trace_stream != NULL) {
*m_trace_stream << "[instance] ";
if (m_manager.has_trace_stream()) {
m_manager.trace_stream() << "[instance] ";
#if 1
*m_trace_stream << static_cast<void*>(f);
m_manager.trace_stream() << static_cast<void*>(f);
#else
for (unsigned i = 0; i < num_bindings; i++) {
// I don't want to use mk_pp because it creates expressions for pretty printing.
// This nasty side-effect may change the behavior of Z3.
*m_trace_stream << " #" << bindings[i]->get_owner_id();
m_manager.trace_stream() << " #" << bindings[i]->get_owner_id();
}
#endif
if (m_manager.proofs_enabled())
*m_trace_stream << " #" << proof_id;
*m_trace_stream << " ; " << generation;
*m_trace_stream << "\n";
m_manager.trace_stream() << " #" << proof_id;
m_manager.trace_stream() << " ; " << generation;
m_manager.trace_stream() << "\n";
}
#endif
}
void qi_queue::instantiate(entry & ent) {
@ -224,10 +221,10 @@ namespace smt {
TRACE("qi_queue_bug", tout << "new instance after simplification:\n" << mk_pp(s_instance, m_manager) << "\n";);
if (m_manager.is_true(s_instance)) {
TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m_manager););
#ifndef SMTCOMP
if (m_trace_stream != NULL)
*m_trace_stream << "[end-of-instance]\n";
#endif
if (m_manager.has_trace_stream())
m_manager.trace_stream() << "[end-of-instance]\n";
return;
}
quantifier_stat * stat = m_qm.get_stat(q);
@ -308,10 +305,10 @@ namespace smt {
}
}
});
#ifndef SMTCOMP
if (m_trace_stream != NULL)
*m_trace_stream << "[end-of-instance]\n";
#endif
if (m_manager.has_trace_stream())
m_manager.trace_stream() << "[end-of-instance]\n";
}
void qi_queue::push_scope() {

3
src/smt/qi_queue.h
View file

@ -53,7 +53,6 @@ namespace smt {
cached_var_subst m_subst;
svector<float> m_vals;
double m_eager_cost_threshold;
std::ostream * m_trace_stream;
struct entry {
fingerprint * m_qb;
float m_cost;
@ -81,7 +80,7 @@ namespace smt {
void display_instance_profile(fingerprint * f, quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned proof_id, unsigned generation);
public:
qi_queue(quantifier_manager & qm, context & ctx, qi_params & params, std::ostream *trace);
qi_queue(quantifier_manager & qm, context & ctx, qi_params & params);
~qi_queue();
void setup();
/**

13
src/smt/smt_case_split_queue.cpp
View file

@ -395,8 +395,8 @@ namespace smt {
if ((is_or && val == l_true) || (is_and && val == l_false)) {
expr * undef_child = 0;
if (!has_child_assigned_to(m_context, to_app(curr), val, undef_child, m_params.m_rel_case_split_order)) {
if (m_params.m_trace_stream != NULL) {
*m_params.m_trace_stream << "[decide-and-or] #" << curr->get_id() << " #" << undef_child->get_id() << "\n";
if (m_manager.has_trace_stream()) {
m_manager.trace_stream() << "[decide-and-or] #" << curr->get_id() << " #" << undef_child->get_id() << "\n";
}
TRACE("case_split", tout << "found AND/OR candidate: #" << curr->get_id() << " #" << undef_child->get_id() << "\n";);
literal l = m_context.get_literal(undef_child);
@ -851,8 +851,8 @@ namespace smt {
if ((is_or && val == l_true) || (is_and && val == l_false)) {
expr * undef_child = 0;
if (!has_child_assigned_to(m_context, to_app(curr), val, undef_child, m_params.m_rel_case_split_order)) {
if (m_params.m_trace_stream != NULL) {
*m_params.m_trace_stream << "[decide-and-or] #" << curr->get_id() << " #" << undef_child->get_id() << "\n";
if (m_manager.has_trace_stream()) {
m_manager.trace_stream() << "[decide-and-or] #" << curr->get_id() << " #" << undef_child->get_id() << "\n";
}
TRACE("case_split", tout << "found AND/OR candidate: #" << curr->get_id() << " #" << undef_child->get_id() << "\n";);
literal l = m_context.get_literal(undef_child);
@ -900,11 +900,6 @@ namespace smt {
// does the push after calling us
m_priority_queue2.insert(idx);
e.m_last_decided = -1;
/*
if (m_params.m_trace_stream != NULL) {
*m_params.m_trace_stream << "[generation] #" << e.m_expr->get_id() << " " << e.m_generation << "\n";
}
*/
return;
}
}

23
src/smt/smt_conflict_resolution.cpp
View file

@ -304,13 +304,13 @@ namespace smt {
if (th)
th->conflict_resolution_eh(to_app(n), var);
}
#ifndef SMTCOMP
if (m_params.m_trace_stream != NULL) {
*m_params.m_trace_stream << "[resolve-lit] " << m_conflict_lvl - lvl << " ";
m_ctx.display_literal(*m_params.m_trace_stream, ~antecedent);
*m_params.m_trace_stream << "\n";
if (get_manager().has_trace_stream()) {
get_manager().trace_stream() << "[resolve-lit] " << m_conflict_lvl - lvl << " ";
m_ctx.display_literal(get_manager().trace_stream(), ~antecedent);
get_manager().trace_stream() << "\n";
}
#endif
if (lvl == m_conflict_lvl) {
num_marks++;
}
@ -478,13 +478,12 @@ namespace smt {
}
do {
#ifndef SMTCOMP
if (m_params.m_trace_stream != NULL) {
*m_params.m_trace_stream << "[resolve-process] ";
m_ctx.display_literal(*m_params.m_trace_stream, ~consequent);
*m_params.m_trace_stream << "\n";
if (get_manager().has_trace_stream()) {
get_manager().trace_stream() << "[resolve-process] ";
m_ctx.display_literal(get_manager().trace_stream(), ~consequent);
get_manager().trace_stream() << "\n";
}
#endif
TRACE("conflict", tout << "processing consequent: "; m_ctx.display_literal(tout, consequent); tout << "\n";
tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << "\n";);

39
src/smt/smt_context.cpp
View file

@ -190,11 +190,10 @@ namespace smt {
TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";);
if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(bool_var2expr(l.var()))))
m_atom_propagation_queue.push_back(l);
#ifndef SMTCOMP
if (m_fparams.m_trace_stream != NULL)
if (m_manager.has_trace_stream())
trace_assign(l, j, decision);
m_case_split_queue->assign_lit_eh(l);
#endif
}
bool context::bcp() {
@ -1789,10 +1788,10 @@ namespace smt {
\brief Create an internal backtracking point
*/
void context::push_scope() {
#ifndef SMTCOMP
if (m_fparams.m_trace_stream != NULL)
*m_fparams.m_trace_stream << "[push] " << m_scope_lvl << "\n";
#endif
if (m_manager.has_trace_stream())
m_manager.trace_stream() << "[push] " << m_scope_lvl << "\n";
m_scope_lvl++;
m_region.push_scope();
m_scopes.push_back(scope());
@ -2237,10 +2236,10 @@ namespace smt {
\warning This method will not invoke reset_cache_generation.
*/
unsigned context::pop_scope_core(unsigned num_scopes) {
#ifndef SMTCOMP
if (m_fparams.m_trace_stream != NULL)
*m_fparams.m_trace_stream << "[pop] " << num_scopes << " " << m_scope_lvl << "\n";
#endif
if (m_manager.has_trace_stream())
m_manager.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n";
TRACE("context", tout << "backtracking: " << num_scopes << "\n";);
TRACE("pop_scope_detail", display(tout););
SASSERT(num_scopes > 0);
@ -2927,10 +2926,8 @@ namespace smt {
Return true if succeeded.
*/
bool context::check_preamble(bool reset_cancel) {
#ifndef SMTCOMP
if (m_fparams.m_trace_stream != NULL)
*m_fparams.m_trace_stream << "[begin-check] " << m_scope_lvl << "\n";
#endif
if (m_manager.has_trace_stream())
m_manager.trace_stream() << "[begin-check] " << m_scope_lvl << "\n";
if (reset_cancel) {
m_cancel_flag = false;
@ -3534,13 +3531,13 @@ namespace smt {
tout << ", ilvl: " << get_intern_level(l.var()) << "\n"
<< mk_pp(bool_var2expr(l.var()), m_manager) << "\n";
});
#ifndef SMTCOMP
if (m_fparams.m_trace_stream != NULL) {
*m_fparams.m_trace_stream << "[conflict] ";
display_literals(*m_fparams.m_trace_stream, num_lits, lits);
*m_fparams.m_trace_stream << "\n";
if (m_manager.has_trace_stream()) {
m_manager.trace_stream() << "[conflict] ";
display_literals(m_manager.trace_stream(), num_lits, lits);
m_manager.trace_stream() << "\n";
}
#endif
#ifdef Z3DEBUG
expr_ref_vector expr_lits(m_manager);
svector<bool> expr_signs;

3
src/smt/smt_context_pp.cpp
View file

@ -583,7 +583,8 @@ namespace smt {
}
void context::trace_assign(literal l, b_justification j, bool decision) const {
std::ostream & out = *m_fparams.m_trace_stream;
SASSERT(m_manager.has_trace_stream());
std::ostream & out = m_manager.trace_stream();
out << "[assign] ";
display_literal(out, l);
if (decision)

8
src/smt/smt_internalizer.cpp
View file

@ -952,10 +952,10 @@ namespace smt {
tout << "is_true_eq: " << e->is_true_eq() << " in cg_table: " << m_cg_table.contains_ptr(e) << " is_cgr: "
<< e->is_cgr() << "\n";
});
#ifndef SMTCOMP
if (m_fparams.m_trace_stream != NULL)
*m_fparams.m_trace_stream << "[attach-enode] #" << n->get_id() << " " << m_generation << "\n";
#endif
if (m_manager.has_trace_stream())
m_manager.trace_stream() << "[attach-enode] #" << n->get_id() << " " << m_generation << "\n";
return e;
}

13
src/smt/smt_quantifier.cpp
View file

@ -45,13 +45,16 @@ namespace smt {
m_wrapper(wrapper),
m_context(ctx),
m_params(p),
m_qi_queue(m_wrapper, ctx, p, p.m_trace_stream),
m_qi_queue(m_wrapper, ctx, p),
m_qstat_gen(ctx.get_manager(), ctx.get_region()),
m_plugin(plugin) {
m_num_instances = 0;
m_qi_queue.setup();
}
bool has_trace_stream() const { return m_context.get_manager().has_trace_stream(); }
std::ostream & trace_stream() { return m_context.get_manager().trace_stream(); }
quantifier_stat * get_stat(quantifier * q) const {
return m_quantifier_stat.find(q);
}
@ -112,8 +115,8 @@ namespace smt {
get_stat(q)->update_max_generation(max_generation);
fingerprint * f = m_context.add_fingerprint(q, q->get_id(), num_bindings, bindings);
if (f) {
if (m_params.m_trace_stream != NULL) {
std::ostream & out = *m_params.m_trace_stream;
if (has_trace_stream()) {
std::ostream & out = trace_stream();
out << "[new-match] " << static_cast<void*>(f) << " #" << q->get_id();
for (unsigned i = 0; i < num_bindings; i++) {
// I don't want to use mk_pp because it creates expressions for pretty printing.
@ -418,8 +421,8 @@ namespace smt {
m_fparams = &(m_context->get_fparams());
ast_manager & m = m_context->get_manager();
m_mam = mk_mam(*m_context, m_fparams->m_trace_stream);
m_lazy_mam = mk_mam(*m_context, m_fparams->m_trace_stream);
m_mam = mk_mam(*m_context);
m_lazy_mam = mk_mam(*m_context);
m_model_finder = alloc(model_finder, m, m_context->get_simplifier());
m_model_checker = alloc(model_checker, m, *m_fparams, *(m_model_finder.get()));