mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

[datalog] improve performance of smt2 frontend

Browse source 
- delay calls to make_annotations and process_costs untill needed
 - remove debug exception handler in join()

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
This commit is contained in:
Nuno Lopes 2013-04-23 12:01:50 -07:00
parent 1917c909d8
commit 9c230941cc
3 changed files with 7 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/muz_qe/dl_instruction.cpp
View file

@ -359,21 +359,7 @@ namespace datalog {
r2.get_signature().output(ctx.get_rel_context().get_manager(), tout);
tout<<":"<<r2.get_size_estimate_rows()<<" ->\n";);
try {
ctx.set_reg(m_res, (*fn)(r1, r2));
}
catch(...)
{
std::string annotation;
unsigned sz;
ctx.get_register_annotation(m_rel1, annotation);
sz = ctx.reg(m_rel1)?ctx.reg(m_rel1)->get_size_estimate_rows():0;
std::cout << m_rel1 << "\t" << sz << "\t" << annotation << "\n";
ctx.get_register_annotation(m_rel2, annotation);
sz = ctx.reg(m_rel2)?ctx.reg(m_rel2)->get_size_estimate_rows():0;
std::cout << m_rel2 << "\t" << sz << "\t" << annotation << "\n";
throw;
}
ctx.set_reg(m_res, (*fn)(r1, r2));
TRACE("dl",
ctx.reg(m_res)->get_signature().output(ctx.get_rel_context().get_manager(), tout);

9
src/muz_qe/rel_context.cpp
View file

@ -179,9 +179,7 @@ namespace datalog {
scoped_query.reset();
}
m_context.record_transformed_rules();
TRACE("dl", m_ectx.report_big_relations(100, tout););
m_code.process_all_costs();
m_code.make_annotations(m_ectx);
TRACE("dl", display_profile(tout););
return result;
}
@ -480,7 +478,10 @@ namespace datalog {
get_rmanager().display(out);
}
void rel_context::display_profile(std::ostream& out) const {
void rel_context::display_profile(std::ostream& out) {
m_code.make_annotations(m_ectx);
m_code.process_all_costs();
out << "\n--------------\n";
out << "Instructions\n";
m_code.display(*this, out);

2
src/muz_qe/rel_context.h
View file

@ -105,7 +105,7 @@ namespace datalog {
void display_output_facts(rule_set const& rules, std::ostream & out) const;
void display_facts(std::ostream & out) const;
void display_profile(std::ostream& out) const;
void display_profile(std::ostream& out);
lbool saturate();