mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Disable a few rule transformations

Browse source 
For this prototype, we need to disable three rule transformations,
namely coi_filter, similarity_compressor, rule_inliner. But
disabling the inliner causes problems with the tracer in the
datalog interpreter. Since a new proprocessor is underway, we
skip the problematic trace outputs for now.

Signed-off-by: Alex Horn <t-alexh@microsoft.com>
This commit is contained in:
Alex Horn 2015-06-11 16:16:47 +01:00
parent 565c0f785f
commit c8a123b7dd
2 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/muz/rel/dl_instruction.cpp
View file

@ -553,7 +553,7 @@ namespace datalog {
if (r.fast_empty()) { if (r.fast_empty()) {
ctx.make_empty(m_reg); ctx.make_empty(m_reg);
} }
TRACE("dl_verbose", r.display(tout <<"post-filter-interpreted:\n");); //TRACE("dl_verbose", r.display(tout <<"post-filter-interpreted:\n"););
return true; return true;
} }
@ -610,7 +610,7 @@ namespace datalog {
if (ctx.reg(m_res)->fast_empty()) { if (ctx.reg(m_res)->fast_empty()) {
ctx.make_empty(m_res); ctx.make_empty(m_res);
} }
TRACE("dl_verbose", reg.display(tout << "post-filter-interpreted-and-project:\n");); //TRACE("dl_verbose", reg.display(tout << "post-filter-interpreted-and-project:\n"););
return true; return true;
} }

6
src/muz/rel/rel_context.cpp
View file

@ -292,17 +292,23 @@ namespace datalog {
void rel_context::transform_rules() { void rel_context::transform_rules() {
rule_transformer transf(m_context); rule_transformer transf(m_context);
#ifdef _MIN_DONE_
transf.register_plugin(alloc(mk_coi_filter, m_context)); transf.register_plugin(alloc(mk_coi_filter, m_context));
#endif
transf.register_plugin(alloc(mk_filter_rules, m_context)); transf.register_plugin(alloc(mk_filter_rules, m_context));
transf.register_plugin(alloc(mk_simple_joins, m_context)); transf.register_plugin(alloc(mk_simple_joins, m_context));
if (m_context.unbound_compressor()) { if (m_context.unbound_compressor()) {
transf.register_plugin(alloc(mk_unbound_compressor, m_context)); transf.register_plugin(alloc(mk_unbound_compressor, m_context));
} }
#ifdef _MIN_DONE_
if (m_context.similarity_compressor()) { if (m_context.similarity_compressor()) {
transf.register_plugin(alloc(mk_similarity_compressor, m_context)); transf.register_plugin(alloc(mk_similarity_compressor, m_context));
} }
#endif
transf.register_plugin(alloc(mk_partial_equivalence_transformer, m_context)); transf.register_plugin(alloc(mk_partial_equivalence_transformer, m_context));
#ifdef _MIN_DONE_
transf.register_plugin(alloc(mk_rule_inliner, m_context)); transf.register_plugin(alloc(mk_rule_inliner, m_context));
#endif
transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context)); transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context));
transf.register_plugin(alloc(mk_separate_negated_tails, m_context)); transf.register_plugin(alloc(mk_separate_negated_tails, m_context));