From 06e3b6cfb87c7ce86be13b4cc5464411d814ee82 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 29 Mar 2013 08:13:07 -0700 Subject: [PATCH] remove model converter from transformer operators. Rely on reference in context Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_context.cpp | 2 +- src/muz_qe/dl_context.h | 1 + src/muz_qe/dl_mk_array_blast.cpp | 2 +- src/muz_qe/dl_mk_array_blast.h | 2 +- src/muz_qe/dl_mk_bit_blast.cpp | 10 +++++----- src/muz_qe/dl_mk_bit_blast.h | 2 +- src/muz_qe/dl_mk_coalesce.cpp | 2 +- src/muz_qe/dl_mk_coalesce.h | 2 +- src/muz_qe/dl_mk_coi_filter.cpp | 10 ++++------ src/muz_qe/dl_mk_coi_filter.h | 4 +--- src/muz_qe/dl_mk_explanations.cpp | 8 ++------ src/muz_qe/dl_mk_explanations.h | 2 +- src/muz_qe/dl_mk_extract_quantifiers.cpp | 2 +- src/muz_qe/dl_mk_extract_quantifiers.h | 2 +- src/muz_qe/dl_mk_filter_rules.cpp | 2 +- src/muz_qe/dl_mk_filter_rules.h | 2 +- src/muz_qe/dl_mk_interp_tail_simplifier.cpp | 2 +- src/muz_qe/dl_mk_interp_tail_simplifier.h | 2 +- src/muz_qe/dl_mk_karr_invariants.cpp | 6 +++--- src/muz_qe/dl_mk_karr_invariants.h | 2 +- src/muz_qe/dl_mk_magic_sets.cpp | 4 ++-- src/muz_qe/dl_mk_magic_sets.h | 2 +- src/muz_qe/dl_mk_partial_equiv.cpp | 2 +- src/muz_qe/dl_mk_partial_equiv.h | 2 +- src/muz_qe/dl_mk_rule_inliner.cpp | 14 +++++++------- src/muz_qe/dl_mk_rule_inliner.h | 2 +- src/muz_qe/dl_mk_similarity_compressor.cpp | 2 +- src/muz_qe/dl_mk_similarity_compressor.h | 2 +- src/muz_qe/dl_mk_simple_joins.cpp | 3 +-- src/muz_qe/dl_mk_simple_joins.h | 2 +- src/muz_qe/dl_mk_slice.cpp | 6 +++--- src/muz_qe/dl_mk_slice.h | 2 +- src/muz_qe/dl_mk_subsumption_checker.cpp | 2 +- src/muz_qe/dl_mk_subsumption_checker.h | 2 +- src/muz_qe/dl_mk_unbound_compressor.cpp | 2 +- src/muz_qe/dl_mk_unbound_compressor.h | 2 +- src/muz_qe/dl_mk_unfold.cpp | 2 +- src/muz_qe/dl_mk_unfold.h | 2 +- src/muz_qe/dl_rule_transformer.cpp | 4 ++-- src/muz_qe/dl_rule_transformer.h | 6 ++---- src/muz_qe/hilbert_basis.cpp | 3 --- 41 files changed, 61 insertions(+), 74 deletions(-) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 592cfaccd..71ef7ad20 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -860,7 +860,7 @@ namespace datalog { 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, m_mc)) { + if (transf(m_rule_set)) { //we have already ensured the negation is stratified and transformations //should not break the stratification m_rule_set.ensure_closed(); diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index ddf200b70..0c4558a28 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -319,6 +319,7 @@ namespace datalog { void ensure_opened(); model_converter_ref& get_model_converter() { return m_mc; } + void add_model_converter(model_converter* mc) { m_mc = concat(m_mc.get(), mc); } proof_converter_ref& get_proof_converter() { return m_pc; } void add_proof_converter(proof_converter* pc) { m_pc = concat(m_pc.get(), pc); } diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp index 048269c5a..1182a2756 100644 --- a/src/muz_qe/dl_mk_array_blast.cpp +++ b/src/muz_qe/dl_mk_array_blast.cpp @@ -208,7 +208,7 @@ namespace datalog { return true; } - rule_set * mk_array_blast::operator()(rule_set const & source, model_converter_ref& mc) { + rule_set * mk_array_blast::operator()(rule_set const & source) { rule_set* rules = alloc(rule_set, m_ctx); rule_set::iterator it = source.begin(), end = source.end(); diff --git a/src/muz_qe/dl_mk_array_blast.h b/src/muz_qe/dl_mk_array_blast.h index 94eb64601..c27bb32b3 100644 --- a/src/muz_qe/dl_mk_array_blast.h +++ b/src/muz_qe/dl_mk_array_blast.h @@ -54,7 +54,7 @@ namespace datalog { virtual ~mk_array_blast(); - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); }; diff --git a/src/muz_qe/dl_mk_bit_blast.cpp b/src/muz_qe/dl_mk_bit_blast.cpp index 338eed0b4..d14080498 100644 --- a/src/muz_qe/dl_mk_bit_blast.cpp +++ b/src/muz_qe/dl_mk_bit_blast.cpp @@ -255,7 +255,7 @@ namespace datalog { m_blaster.updt_params(m_params); } - rule_set * operator()(rule_set const & source, model_converter_ref& mc) { + rule_set * operator()(rule_set const & source) { // TODO pc if (!m_context.get_params().bit_blast()) { return 0; @@ -284,7 +284,7 @@ namespace datalog { result->add_rule(m_rules.get(i)); } - if (mc) { + if (m_context.get_model_converter()) { filter_model_converter* fmc = alloc(filter_model_converter, m); bit_blast_model_converter* bvmc = alloc(bit_blast_model_converter, m); func_decl_ref_vector const& old_funcs = m_rewriter.m_cfg.old_funcs(); @@ -293,7 +293,7 @@ namespace datalog { fmc->insert(new_funcs[i]); bvmc->insert(old_funcs[i], new_funcs[i]); } - mc = concat(mc.get(), concat(bvmc, fmc)); + m_context.add_model_converter(concat(bvmc, fmc)); } return result; @@ -308,8 +308,8 @@ namespace datalog { dealloc(m_impl); } - rule_set * mk_bit_blast::operator()(rule_set const & source, model_converter_ref& mc) { - return (*m_impl)(source, mc); + rule_set * mk_bit_blast::operator()(rule_set const & source) { + return (*m_impl)(source); } }; diff --git a/src/muz_qe/dl_mk_bit_blast.h b/src/muz_qe/dl_mk_bit_blast.h index 3a6de75e3..60c83f6cb 100644 --- a/src/muz_qe/dl_mk_bit_blast.h +++ b/src/muz_qe/dl_mk_bit_blast.h @@ -44,7 +44,7 @@ namespace datalog { mk_bit_blast(context & ctx, unsigned priority = 35000); ~mk_bit_blast(); - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); }; }; diff --git a/src/muz_qe/dl_mk_coalesce.cpp b/src/muz_qe/dl_mk_coalesce.cpp index de5388312..94c42e33b 100644 --- a/src/muz_qe/dl_mk_coalesce.cpp +++ b/src/muz_qe/dl_mk_coalesce.cpp @@ -171,7 +171,7 @@ namespace datalog { return true; } - rule_set * mk_coalesce::operator()(rule_set const & source, model_converter_ref& mc) { + rule_set * mk_coalesce::operator()(rule_set const & source) { rule_set* rules = alloc(rule_set, m_ctx); rule_set::decl2rules::iterator it = source.begin_grouped_rules(), end = source.end_grouped_rules(); for (; it != end; ++it) { diff --git a/src/muz_qe/dl_mk_coalesce.h b/src/muz_qe/dl_mk_coalesce.h index ab0b74479..4a4065174 100644 --- a/src/muz_qe/dl_mk_coalesce.h +++ b/src/muz_qe/dl_mk_coalesce.h @@ -52,7 +52,7 @@ namespace datalog { */ mk_coalesce(context & ctx); - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); }; }; diff --git a/src/muz_qe/dl_mk_coi_filter.cpp b/src/muz_qe/dl_mk_coi_filter.cpp index 915dd4306..6aa688a3c 100644 --- a/src/muz_qe/dl_mk_coi_filter.cpp +++ b/src/muz_qe/dl_mk_coi_filter.cpp @@ -33,9 +33,7 @@ namespace datalog { // ----------------------------------- - rule_set * mk_coi_filter::operator()( - rule_set const & source, - model_converter_ref& mc) + rule_set * mk_coi_filter::operator()(rule_set const & source) { if (source.get_num_rules()==0) { return 0; @@ -80,7 +78,7 @@ namespace datalog { if (interesting_preds.contains(pred)) { res->add_rule(r); } - else if (mc.get()) { + else if (m_context.get_model_converter()) { pruned_preds.insert(pred); } } @@ -89,14 +87,14 @@ namespace datalog { res = 0; } - if (res && mc) { + if (res && m_context.get_model_converter()) { decl_set::iterator end = pruned_preds.end(); decl_set::iterator it = pruned_preds.begin(); extension_model_converter* mc0 = alloc(extension_model_converter, m); for (; it != end; ++it) { mc0->insert(*it, m.mk_true()); } - mc = concat(mc.get(), mc0); + m_context.add_model_converter(mc0); } return res.detach(); diff --git a/src/muz_qe/dl_mk_coi_filter.h b/src/muz_qe/dl_mk_coi_filter.h index 2191048d3..b02bed9ec 100644 --- a/src/muz_qe/dl_mk_coi_filter.h +++ b/src/muz_qe/dl_mk_coi_filter.h @@ -38,9 +38,7 @@ namespace datalog { m(ctx.get_manager()), m_context(ctx) {} - - rule_set * operator()(rule_set const & source, - model_converter_ref& mc); + rule_set * operator()(rule_set const & source); }; }; diff --git a/src/muz_qe/dl_mk_explanations.cpp b/src/muz_qe/dl_mk_explanations.cpp index af5b1d97a..646a0bcbe 100644 --- a/src/muz_qe/dl_mk_explanations.cpp +++ b/src/muz_qe/dl_mk_explanations.cpp @@ -174,11 +174,9 @@ namespace datalog { } } -#if 1 virtual void deallocate() { get_plugin().recycle(this); } -#endif public: @@ -875,14 +873,12 @@ namespace datalog { } } - rule_set * mk_explanations::operator()(rule_set const & source, model_converter_ref& mc) { - SASSERT(!mc); + rule_set * mk_explanations::operator()(rule_set const & source) { + if(source.get_num_rules()==0) { return 0; } - m_context.collect_predicates(m_original_preds); - rule_set * res = alloc(rule_set, m_context); transform_facts(m_context.get_rel_context().get_rmanager()); transform_rules(source, *res); diff --git a/src/muz_qe/dl_mk_explanations.h b/src/muz_qe/dl_mk_explanations.h index 40606f8df..4e7e23e98 100644 --- a/src/muz_qe/dl_mk_explanations.h +++ b/src/muz_qe/dl_mk_explanations.h @@ -82,7 +82,7 @@ namespace datalog { return get_union_decl(m_context); } - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); static expr* get_explanation(relation_base const& r); }; diff --git a/src/muz_qe/dl_mk_extract_quantifiers.cpp b/src/muz_qe/dl_mk_extract_quantifiers.cpp index a3d5cc2ab..76e329d79 100644 --- a/src/muz_qe/dl_mk_extract_quantifiers.cpp +++ b/src/muz_qe/dl_mk_extract_quantifiers.cpp @@ -355,7 +355,7 @@ namespace datalog { m_quantifiers.reset(); } - rule_set * mk_extract_quantifiers::operator()(rule_set const & source, model_converter_ref& mc) { + rule_set * mk_extract_quantifiers::operator()(rule_set const & source) { reset(); rule_set::iterator it = source.begin(), end = source.end(); for (; !m_has_quantifiers && it != end; ++it) { diff --git a/src/muz_qe/dl_mk_extract_quantifiers.h b/src/muz_qe/dl_mk_extract_quantifiers.h index 7d2f7b149..27b13cd71 100644 --- a/src/muz_qe/dl_mk_extract_quantifiers.h +++ b/src/muz_qe/dl_mk_extract_quantifiers.h @@ -77,7 +77,7 @@ namespace datalog { void set_query(func_decl* q); - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); bool has_quantifiers() { return m_has_quantifiers; } diff --git a/src/muz_qe/dl_mk_filter_rules.cpp b/src/muz_qe/dl_mk_filter_rules.cpp index 46fde4bc2..62abd78c4 100644 --- a/src/muz_qe/dl_mk_filter_rules.cpp +++ b/src/muz_qe/dl_mk_filter_rules.cpp @@ -150,7 +150,7 @@ namespace datalog { } } - rule_set * mk_filter_rules::operator()(rule_set const & source, model_converter_ref& mc) { + rule_set * mk_filter_rules::operator()(rule_set const & source) { // TODO mc, pc m_tail2filter.reset(); m_result = alloc(rule_set, m_context); diff --git a/src/muz_qe/dl_mk_filter_rules.h b/src/muz_qe/dl_mk_filter_rules.h index daa72e36f..4a247fdb5 100644 --- a/src/muz_qe/dl_mk_filter_rules.h +++ b/src/muz_qe/dl_mk_filter_rules.h @@ -72,7 +72,7 @@ namespace datalog { /** \brief Return a new rule set where only filter rules contain atoms with repeated variables and/or values. */ - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); }; }; diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp index a48b7b32f..27b99cf98 100644 --- a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp @@ -572,7 +572,7 @@ namespace datalog { return modified; } - rule_set * mk_interp_tail_simplifier::operator()(rule_set const & source, model_converter_ref& mc) { + rule_set * mk_interp_tail_simplifier::operator()(rule_set const & source) { if (source.get_num_rules() == 0) { return 0; } diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.h b/src/muz_qe/dl_mk_interp_tail_simplifier.h index 4cb14914a..247b20755 100644 --- a/src/muz_qe/dl_mk_interp_tail_simplifier.h +++ b/src/muz_qe/dl_mk_interp_tail_simplifier.h @@ -93,7 +93,7 @@ namespace datalog { */ bool transform_rule(rule * r, rule_ref& res); - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); }; }; diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp index d44b31979..982bdfd74 100644 --- a/src/muz_qe/dl_mk_karr_invariants.cpp +++ b/src/muz_qe/dl_mk_karr_invariants.cpp @@ -520,7 +520,7 @@ namespace datalog { m_hb.set_cancel(true); } - rule_set * mk_karr_invariants::operator()(rule_set const & source, model_converter_ref& mc) { + rule_set * mk_karr_invariants::operator()(rule_set const & source) { if (!m_ctx.get_params().karr()) { return 0; } @@ -590,7 +590,7 @@ namespace datalog { for (; it != end; ++it) { update_body(*rules, **it); } - if (mc) { + if (m_ctx.get_model_converter()) { add_invariant_model_converter* kmc = alloc(add_invariant_model_converter, m); rule_set::decl2rules::iterator git = source.begin_grouped_rules(); rule_set::decl2rules::iterator gend = source.end_grouped_rules(); @@ -601,7 +601,7 @@ namespace datalog { kmc->add(p, *M); } } - mc = concat(mc.get(), kmc); + m_ctx.add_model_converter(kmc); } TRACE("dl", rules->display(tout);); return rules; diff --git a/src/muz_qe/dl_mk_karr_invariants.h b/src/muz_qe/dl_mk_karr_invariants.h index 7cd26d495..8abab9d7e 100644 --- a/src/muz_qe/dl_mk_karr_invariants.h +++ b/src/muz_qe/dl_mk_karr_invariants.h @@ -69,7 +69,7 @@ namespace datalog { virtual void cancel(); - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); }; diff --git a/src/muz_qe/dl_mk_magic_sets.cpp b/src/muz_qe/dl_mk_magic_sets.cpp index 990040ab8..6885edc4e 100644 --- a/src/muz_qe/dl_mk_magic_sets.cpp +++ b/src/muz_qe/dl_mk_magic_sets.cpp @@ -317,8 +317,8 @@ namespace datalog { m_rules.push_back(r); } - rule_set * mk_magic_sets::operator()(rule_set const & source, model_converter_ref& mc) { - SASSERT(!mc); + rule_set * mk_magic_sets::operator()(rule_set const & source) { + SASSERT(!m_context.get_model_converter()); unsigned init_rule_cnt = source.get_num_rules(); { func_decl_set intentional; diff --git a/src/muz_qe/dl_mk_magic_sets.h b/src/muz_qe/dl_mk_magic_sets.h index 3f50e6713..2dc91c7e8 100644 --- a/src/muz_qe/dl_mk_magic_sets.h +++ b/src/muz_qe/dl_mk_magic_sets.h @@ -121,7 +121,7 @@ namespace datalog { */ mk_magic_sets(context & ctx, rule * goal_rule); - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); }; }; diff --git a/src/muz_qe/dl_mk_partial_equiv.cpp b/src/muz_qe/dl_mk_partial_equiv.cpp index b55f5294e..35f8ff8df 100644 --- a/src/muz_qe/dl_mk_partial_equiv.cpp +++ b/src/muz_qe/dl_mk_partial_equiv.cpp @@ -86,7 +86,7 @@ namespace datalog { } - rule_set * mk_partial_equivalence_transformer::operator()(rule_set const & source, model_converter_ref& mc) { + rule_set * mk_partial_equivalence_transformer::operator()(rule_set const & source) { // TODO mc if (source.get_num_rules() == 0) { diff --git a/src/muz_qe/dl_mk_partial_equiv.h b/src/muz_qe/dl_mk_partial_equiv.h index c44d59e8c..54a70b3c0 100644 --- a/src/muz_qe/dl_mk_partial_equiv.h +++ b/src/muz_qe/dl_mk_partial_equiv.h @@ -35,7 +35,7 @@ namespace datalog { m(ctx.get_manager()), m_context(ctx) {} - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); private: diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp index 047ed768f..91cfbe3fc 100644 --- a/src/muz_qe/dl_mk_rule_inliner.cpp +++ b/src/muz_qe/dl_mk_rule_inliner.cpp @@ -241,8 +241,10 @@ namespace datalog { return false; } - //these conditions are optional, they avoid possible exponential increase - //in the size of the problem + // + // these conditions are optional, they avoid possible exponential increase + // in the size of the problem + // return //m_head_pred_non_empty_tails_ctr.get(pred)<=1 @@ -837,7 +839,7 @@ namespace datalog { return done_something; } - rule_set * mk_rule_inliner::operator()(rule_set const & source, model_converter_ref& mc) { + rule_set * mk_rule_inliner::operator()(rule_set const & source) { bool something_done = false; ref hsmc; @@ -854,7 +856,7 @@ namespace datalog { } - if (mc) { + if (m_context.get_model_converter()) { hsmc = alloc(horn_subsume_model_converter, m); } m_mc = hsmc.get(); @@ -881,9 +883,7 @@ namespace datalog { res = 0; } else { - if (mc) { - mc = concat(mc.get(), hsmc.get()); - } + m_context.add_model_converter(hsmc.get()); } return res.detach(); diff --git a/src/muz_qe/dl_mk_rule_inliner.h b/src/muz_qe/dl_mk_rule_inliner.h index a58b3b473..5ef8db7eb 100644 --- a/src/muz_qe/dl_mk_rule_inliner.h +++ b/src/muz_qe/dl_mk_rule_inliner.h @@ -196,7 +196,7 @@ namespace datalog { {} virtual ~mk_rule_inliner() { } - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); }; }; diff --git a/src/muz_qe/dl_mk_similarity_compressor.cpp b/src/muz_qe/dl_mk_similarity_compressor.cpp index dfd0a4d81..9868c82f6 100644 --- a/src/muz_qe/dl_mk_similarity_compressor.cpp +++ b/src/muz_qe/dl_mk_similarity_compressor.cpp @@ -500,7 +500,7 @@ namespace datalog { } } - rule_set * mk_similarity_compressor::operator()(rule_set const & source, model_converter_ref& mc) { + rule_set * mk_similarity_compressor::operator()(rule_set const & source) { // TODO mc m_modified = false; unsigned init_rule_cnt = source.get_num_rules(); diff --git a/src/muz_qe/dl_mk_similarity_compressor.h b/src/muz_qe/dl_mk_similarity_compressor.h index d1ded01e7..6e0ca9db5 100644 --- a/src/muz_qe/dl_mk_similarity_compressor.h +++ b/src/muz_qe/dl_mk_similarity_compressor.h @@ -69,7 +69,7 @@ namespace datalog { public: mk_similarity_compressor(context & ctx, unsigned threshold_count); - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); }; }; diff --git a/src/muz_qe/dl_mk_simple_joins.cpp b/src/muz_qe/dl_mk_simple_joins.cpp index f19e34fec..3a3f96acf 100644 --- a/src/muz_qe/dl_mk_simple_joins.cpp +++ b/src/muz_qe/dl_mk_simple_joins.cpp @@ -718,8 +718,7 @@ namespace datalog { } }; - rule_set * mk_simple_joins::operator()(rule_set const & source, model_converter_ref& mc) { - // TODO mc + rule_set * mk_simple_joins::operator()(rule_set const & source) { rule_set rs_aux_copy(m_context); rs_aux_copy.add_rules(source); if(!rs_aux_copy.is_closed()) { diff --git a/src/muz_qe/dl_mk_simple_joins.h b/src/muz_qe/dl_mk_simple_joins.h index df8d3f55c..89832626f 100644 --- a/src/muz_qe/dl_mk_simple_joins.h +++ b/src/muz_qe/dl_mk_simple_joins.h @@ -53,7 +53,7 @@ namespace datalog { public: mk_simple_joins(context & ctx); - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); }; }; diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz_qe/dl_mk_slice.cpp index 0adab78ce..c98d6503e 100644 --- a/src/muz_qe/dl_mk_slice.cpp +++ b/src/muz_qe/dl_mk_slice.cpp @@ -802,7 +802,7 @@ namespace datalog { } } - rule_set * mk_slice::operator()(rule_set const & src, model_converter_ref& mc) { + rule_set * mk_slice::operator()(rule_set const & src) { for (unsigned i = 0; i < src.get_num_rules(); ++i) { if (src.get_rule(i)->has_quantifiers()) { return 0; @@ -813,7 +813,7 @@ namespace datalog { if (m_ctx.generate_proof_trace()) { spc = alloc(slice_proof_converter, m_ctx); } - if (mc) { + if (m_ctx.get_model_converter()) { smc = alloc(slice_model_converter, *this, m); } m_pc = spc.get(); @@ -836,7 +836,7 @@ namespace datalog { } } m_ctx.add_proof_converter(spc.get()); - mc = concat(mc.get(), smc.get()); + m_ctx.add_model_converter(smc.get()); return result; } diff --git a/src/muz_qe/dl_mk_slice.h b/src/muz_qe/dl_mk_slice.h index 4290ee4b9..1b4312e77 100644 --- a/src/muz_qe/dl_mk_slice.h +++ b/src/muz_qe/dl_mk_slice.h @@ -102,7 +102,7 @@ namespace datalog { virtual ~mk_slice() { } - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); func_decl* get_predicate(func_decl* p) { func_decl* q = p; m_predicates.find(p, q); return q; } diff --git a/src/muz_qe/dl_mk_subsumption_checker.cpp b/src/muz_qe/dl_mk_subsumption_checker.cpp index 2f0d56475..fb55a377c 100644 --- a/src/muz_qe/dl_mk_subsumption_checker.cpp +++ b/src/muz_qe/dl_mk_subsumption_checker.cpp @@ -332,7 +332,7 @@ namespace datalog { } } - rule_set * mk_subsumption_checker::operator()(rule_set const & source, model_converter_ref& mc) { + rule_set * mk_subsumption_checker::operator()(rule_set const & source) { // TODO mc m_have_new_total_rule = false; diff --git a/src/muz_qe/dl_mk_subsumption_checker.h b/src/muz_qe/dl_mk_subsumption_checker.h index a95f08c5d..59904b3ef 100644 --- a/src/muz_qe/dl_mk_subsumption_checker.h +++ b/src/muz_qe/dl_mk_subsumption_checker.h @@ -84,7 +84,7 @@ namespace datalog { reset_dealloc_values(m_ground_unconditional_rule_heads); } - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); }; }; diff --git a/src/muz_qe/dl_mk_unbound_compressor.cpp b/src/muz_qe/dl_mk_unbound_compressor.cpp index 54b6f4ebe..40926c2a8 100644 --- a/src/muz_qe/dl_mk_unbound_compressor.cpp +++ b/src/muz_qe/dl_mk_unbound_compressor.cpp @@ -334,7 +334,7 @@ namespace datalog { } } - rule_set * mk_unbound_compressor::operator()(rule_set const & source, model_converter_ref& mc) { + rule_set * mk_unbound_compressor::operator()(rule_set const & source) { // TODO mc m_modified = false; diff --git a/src/muz_qe/dl_mk_unbound_compressor.h b/src/muz_qe/dl_mk_unbound_compressor.h index 256be180d..cad953783 100644 --- a/src/muz_qe/dl_mk_unbound_compressor.h +++ b/src/muz_qe/dl_mk_unbound_compressor.h @@ -82,7 +82,7 @@ namespace datalog { public: mk_unbound_compressor(context & ctx); - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); }; }; diff --git a/src/muz_qe/dl_mk_unfold.cpp b/src/muz_qe/dl_mk_unfold.cpp index 7af82110a..dfbd87122 100644 --- a/src/muz_qe/dl_mk_unfold.cpp +++ b/src/muz_qe/dl_mk_unfold.cpp @@ -50,7 +50,7 @@ namespace datalog { } } - rule_set * mk_unfold::operator()(rule_set const & source, model_converter_ref& mc) { + rule_set * mk_unfold::operator()(rule_set const & source) { rule_set* rules = alloc(rule_set, m_ctx); rule_set::iterator it = source.begin(), end = source.end(); for (; it != end; ++it) { diff --git a/src/muz_qe/dl_mk_unfold.h b/src/muz_qe/dl_mk_unfold.h index 90aefa86e..26f64926d 100644 --- a/src/muz_qe/dl_mk_unfold.h +++ b/src/muz_qe/dl_mk_unfold.h @@ -44,7 +44,7 @@ namespace datalog { */ mk_unfold(context & ctx); - rule_set * operator()(rule_set const & source, model_converter_ref& mc); + rule_set * operator()(rule_set const & source); }; }; diff --git a/src/muz_qe/dl_rule_transformer.cpp b/src/muz_qe/dl_rule_transformer.cpp index 5ecbf2b45..50a3f3310 100644 --- a/src/muz_qe/dl_rule_transformer.cpp +++ b/src/muz_qe/dl_rule_transformer.cpp @@ -73,7 +73,7 @@ namespace datalog { m_dirty=true; } - bool rule_transformer::operator()(rule_set & rules, model_converter_ref& mc) { + bool rule_transformer::operator()(rule_set & rules) { ensure_ordered(); bool modified = false; @@ -87,7 +87,7 @@ namespace datalog { for(; it!=end && !m_cancel; ++it) { plugin & p = **it; - rule_set * new_rules = p(rules, mc); + rule_set * new_rules = p(rules); if (!new_rules) { continue; } diff --git a/src/muz_qe/dl_rule_transformer.h b/src/muz_qe/dl_rule_transformer.h index 3b2140caf..2dbf25118 100644 --- a/src/muz_qe/dl_rule_transformer.h +++ b/src/muz_qe/dl_rule_transformer.h @@ -23,7 +23,6 @@ Revision History: #include"vector.h" #include"dl_rule.h" #include"dl_rule_set.h" -#include"model_converter.h" namespace datalog { @@ -68,7 +67,7 @@ namespace datalog { \brief Transform the rule set using the registered transformation plugins. If the rule set has changed, return true; otherwise return false. */ - bool operator()(rule_set & rules, model_converter_ref& mc); + bool operator()(rule_set & rules); }; class rule_transformer::plugin { @@ -104,8 +103,7 @@ namespace datalog { The caller takes ownership of the returned \c rule_set object. */ - virtual rule_set * operator()(rule_set const & source, - model_converter_ref& mc) = 0; + virtual rule_set * operator()(rule_set const & source) = 0; virtual void cancel() { m_cancel = true; } diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp index 9fbd8cc2e..0b6b664ec 100644 --- a/src/muz_qe/hilbert_basis.cpp +++ b/src/muz_qe/hilbert_basis.cpp @@ -997,11 +997,9 @@ void hilbert_basis::select_inequality() { unsigned best = m_current_ineq; unsigned non_zeros = get_num_nonzeros(m_ineqs[best]); unsigned prod = get_ineq_product(m_ineqs[best]); - //numeral diff = get_ineq_diff(m_ineqs[best]); for (unsigned j = best+1; prod != 0 && j < m_ineqs.size(); ++j) { unsigned non_zeros2 = get_num_nonzeros(m_ineqs[j]); unsigned prod2 = get_ineq_product(m_ineqs[j]); - //numeral diff2 = get_ineq_diff(m_ineqs[j]); if (prod2 == 0) { prod = prod2; non_zeros = non_zeros2; @@ -1010,7 +1008,6 @@ void hilbert_basis::select_inequality() { } if (non_zeros2 < non_zeros || (non_zeros2 == non_zeros && prod2 < prod)) { prod = prod2; - // diff = diff2; non_zeros = non_zeros2; best = j; }