From babfc701a60fc1cf5c1321b77c194a041490b251 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Mar 2013 10:36:36 -0700 Subject: [PATCH] make model and proof converters a reference Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_bmc_engine.cpp | 6 ++++-- src/muz_qe/dl_context.cpp | 12 ++++++------ src/muz_qe/dl_context.h | 11 ++++++++--- src/muz_qe/horn_tactic.cpp | 6 ++++-- src/muz_qe/pdr_dl_interface.cpp | 12 +++++++----- src/muz_qe/rel_context.cpp | 12 +++--------- src/shell/datalog_frontend.cpp | 4 +--- 7 files changed, 33 insertions(+), 30 deletions(-) diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp index 80fcdea4a..200338b86 100644 --- a/src/muz_qe/dl_bmc_engine.cpp +++ b/src/muz_qe/dl_bmc_engine.cpp @@ -1420,13 +1420,15 @@ namespace datalog { model_converter_ref mc = datalog::mk_skip_model_converter(); m_pc = datalog::mk_skip_proof_converter(); m_ctx.set_output_predicate(m_query_pred); - m_ctx.apply_default_transformation(mc, m_pc); + m_ctx.set_model_converter(mc); + m_ctx.set_proof_converter(m_pc); + m_ctx.apply_default_transformation(); if (m_ctx.get_params().slice()) { datalog::rule_transformer transformer(m_ctx); datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); transformer.register_plugin(slice); - m_ctx.transform_rules(transformer, mc, m_pc); + m_ctx.transform_rules(transformer); m_query_pred = slice->get_predicate(m_query_pred.get()); m_ctx.set_output_predicate(m_query_pred); } diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 53231e7b0..839aa93f9 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -826,7 +826,7 @@ namespace datalog { m_closed = false; } - void context::transform_rules(model_converter_ref& mc, proof_converter_ref& pc) { + void context::transform_rules() { m_transf.reset(); m_transf.register_plugin(alloc(mk_filter_rules,*this)); m_transf.register_plugin(alloc(mk_simple_joins,*this)); @@ -841,13 +841,13 @@ namespace datalog { } m_transf.register_plugin(alloc(datalog::mk_partial_equivalence_transformer, *this)); - transform_rules(m_transf, mc, pc); + transform_rules(m_transf); } - void context::transform_rules(rule_transformer& transf, model_converter_ref& mc, proof_converter_ref& pc) { + void context::transform_rules(rule_transformer& transf) { SASSERT(m_closed); //we must finish adding rules before we start transforming them TRACE("dl", display_rules(tout);); - if (transf(m_rule_set, mc, pc)) { + if (transf(m_rule_set, m_mc, m_pc)) { //we have already ensured the negation is stratified and transformations //should not break the stratification m_rule_set.ensure_closed(); @@ -862,7 +862,7 @@ namespace datalog { m_rule_set.add_rules(rs); } - void context::apply_default_transformation(model_converter_ref& mc, proof_converter_ref& pc) { + void context::apply_default_transformation() { ensure_closed(); m_transf.reset(); m_transf.register_plugin(alloc(datalog::mk_coi_filter, *this)); @@ -890,7 +890,7 @@ namespace datalog { m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000)); m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000)); m_transf.register_plugin(alloc(datalog::mk_karr_invariants, *this, 36010)); - transform_rules(m_transf, mc, pc); + transform_rules(m_transf); } void context::collect_params(param_descrs& p) { diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index b587daf7f..f9a1f1737 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -97,6 +97,8 @@ namespace datalog { expr_ref_vector m_rule_fmls; svector m_rule_names; expr_ref_vector m_background; + model_converter_ref m_mc; + proof_converter_ref m_pc; scoped_ptr m_pdr; scoped_ptr m_bmc; @@ -313,11 +315,14 @@ namespace datalog { void reopen(); void ensure_opened(); - void transform_rules(model_converter_ref& mc, proof_converter_ref& pc); - void transform_rules(rule_transformer& transf, model_converter_ref& mc, proof_converter_ref& pc); + void set_model_converter(model_converter_ref& mc) { m_mc = mc; } + void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; } + + void transform_rules(); // model_converter_ref& mc, proof_converter_ref& pc); + void transform_rules(rule_transformer& transf); // , model_converter_ref& mc, proof_converter_ref& pc); void replace_rules(rule_set & rs); - void apply_default_transformation(model_converter_ref& mc, proof_converter_ref& pc); + void apply_default_transformation(); // model_converter_ref& mc, proof_converter_ref& pc); void collect_params(param_descrs& r); diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp index 633aeaa81..c87874b29 100644 --- a/src/muz_qe/horn_tactic.cpp +++ b/src/muz_qe/horn_tactic.cpp @@ -282,14 +282,16 @@ class horn_tactic : public tactic { func_decl* query_pred = to_app(q)->get_decl(); m_ctx.set_output_predicate(query_pred); + m_ctx.set_model_converter(mc); + m_ctx.set_proof_converter(pc); m_ctx.get_rules(); // flush adding rules. - m_ctx.apply_default_transformation(mc, pc); + m_ctx.apply_default_transformation(); if (m_ctx.get_params().slice()) { datalog::rule_transformer transformer(m_ctx); datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); transformer.register_plugin(slice); - m_ctx.transform_rules(transformer, mc, pc); + m_ctx.transform_rules(transformer); } expr_substitution sub(m); diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index 54a40f8b8..b55f302ed 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -111,13 +111,15 @@ lbool dl_interface::query(expr * query) { pc = datalog::mk_skip_proof_converter(); } m_ctx.set_output_predicate(query_pred); - m_ctx.apply_default_transformation(mc, pc); + m_ctx.set_model_converter(mc); + m_ctx.set_proof_converter(pc); + m_ctx.apply_default_transformation(); if (m_ctx.get_params().slice()) { datalog::rule_transformer transformer(m_ctx); datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); transformer.register_plugin(slice); - m_ctx.transform_rules(transformer, mc, pc); + m_ctx.transform_rules(transformer); query_pred = slice->get_predicate(query_pred.get()); m_ctx.set_output_predicate(query_pred); @@ -137,11 +139,11 @@ lbool dl_interface::query(expr * query) { datalog::rule_transformer transformer1(m_ctx), transformer2(m_ctx); if (m_ctx.get_params().coalesce_rules()) { transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx)); - m_ctx.transform_rules(transformer1, mc, pc); + m_ctx.transform_rules(transformer1); } transformer2.register_plugin(alloc(datalog::mk_unfold, m_ctx)); while (num_unfolds > 0) { - m_ctx.transform_rules(transformer2, mc, pc); + m_ctx.transform_rules(transformer2); --num_unfolds; } } @@ -149,7 +151,7 @@ lbool dl_interface::query(expr * query) { datalog::mk_extract_quantifiers* extract_quantifiers = alloc(datalog::mk_extract_quantifiers, m_ctx); datalog::rule_transformer extract_q_tr(m_ctx); extract_q_tr.register_plugin(extract_quantifiers); - m_ctx.transform_rules(extract_q_tr, mc, pc); + m_ctx.transform_rules(extract_q_tr); IF_VERBOSE(2, m_ctx.display_rules(verbose_stream());); diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp index 00ac51e9f..8e22a704c 100644 --- a/src/muz_qe/rel_context.cpp +++ b/src/muz_qe/rel_context.cpp @@ -103,9 +103,7 @@ namespace datalog { TRACE("dl", m_context.display(tout);); while (true) { - model_converter_ref mc; // Ignored in Datalog mode - proof_converter_ref pc; // Ignored in Datalog mode - m_context.transform_rules(mc, pc); + m_context.transform_rules(); compiler::compile(m_context, m_context.get_rules(), rules_code, termination_code); TRACE("dl", rules_code.display(*this, tout); ); @@ -263,14 +261,12 @@ namespace datalog { reset_negated_tables(); if (m_context.generate_explanations()) { - model_converter_ref mc; // ignored in Datalog mode - proof_converter_ref pc; // ignored in Datalog mode rule_transformer transformer(m_context); //expl_plugin is deallocated when transformer goes out of scope mk_explanations * expl_plugin = alloc(mk_explanations, m_context, m_context.explanations_on_relation_level()); transformer.register_plugin(expl_plugin); - m_context.transform_rules(transformer, mc, pc); + m_context.transform_rules(transformer); //we will retrieve the predicate with explanations instead of the original query predicate query_pred = expl_plugin->get_e_decl(query_pred); @@ -280,11 +276,9 @@ namespace datalog { } if (m_context.magic_sets_for_queries()) { - model_converter_ref mc; // Ignored in Datalog mode - proof_converter_ref pc; // Ignored in Datalog mode rule_transformer transformer(m_context); transformer.register_plugin(alloc(mk_magic_sets, m_context, qrule.get())); - m_context.transform_rules(transformer, mc, pc); + m_context.transform_rules(transformer); } lbool res = saturate(); diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp index 44a9d9b66..07052609e 100644 --- a/src/shell/datalog_frontend.cpp +++ b/src/shell/datalog_frontend.cpp @@ -200,9 +200,7 @@ unsigned read_datalog(char const * file) { timeout = UINT_MAX; } do { - model_converter_ref mc; // ignored - proof_converter_ref pc; // ignored - ctx.transform_rules(mc, pc); + ctx.transform_rules(); datalog::compiler::compile(ctx, ctx.get_rules(), rules_code, termination_code);