diff --git a/src/muz_qe/dl_compiler.h b/src/muz_qe/dl_compiler.h index 8f40f814a..78b4623de 100644 --- a/src/muz_qe/dl_compiler.h +++ b/src/muz_qe/dl_compiler.h @@ -42,7 +42,6 @@ namespace datalog { typedef u_map int2int; typedef u_map int2ints; typedef obj_map pred2idx; -// typedef map,ptr_eq > pred2idx; typedef unsigned_vector var_vector; typedef ptr_vector func_decl_vector; diff --git a/src/muz_qe/dl_rule_transformer.cpp b/src/muz_qe/dl_rule_transformer.cpp index 21021ca43..0cad08cb4 100644 --- a/src/muz_qe/dl_rule_transformer.cpp +++ b/src/muz_qe/dl_rule_transformer.cpp @@ -107,9 +107,6 @@ namespace datalog { tout << typeid(p).name()<<":\n"; new_rules->display(tout); ); - IF_VERBOSE(1, new_rules->get_rule(0)->display(m_context, verbose_stream() << typeid(p).name() <<"\n");); - IF_VERBOSE(1, verbose_stream() << new_rules->get_dependencies().begin()->m_key->get_name() << "\n";); - } if (modified) { rules.replace_rules(*new_rules); diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg index fd7dbdcae..774559cdb 100644 --- a/src/muz_qe/fixedpoint_params.pyg +++ b/src/muz_qe/fixedpoint_params.pyg @@ -13,7 +13,6 @@ def_module_params('fixedpoint', ('unbound_compressor', BOOL, True, "auxiliary relations will be introduced to avoid unbound variables in rule heads"), ('similarity_compressor', BOOL, True, "(DATALOG) rules that differ only in values of constants will be merged into a single rule"), ('similarity_compressor_threshold', UINT, 11, "(DATALOG) if similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged"), - ('filter_rules', BOOL, True, "(DATALOG) apply filter compression on rules"), ('all_or_nothing_deltas', BOOL, False, "(DATALOG) compile rules so that it is enough for the delta relation in union and widening operations to determine only whether the updated relation was modified or not"), ('compile_with_widening', BOOL, False, "(DATALOG) widening will be used to compile recursive rules"), ('eager_emptiness_checking', BOOL, True, "(DATALOG) emptiness of affected relations will be checked after each instruction, so that we may ommit unnecessary instructions"), diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp index be6d999b6..ef5639279 100644 --- a/src/muz_qe/rel_context.cpp +++ b/src/muz_qe/rel_context.cpp @@ -113,12 +113,10 @@ namespace datalog { TRACE("dl", m_context.display(tout);); while (true) { - m_ectx.reset(); m_code.reset(); termination_code.reset(); m_context.ensure_closed(); - IF_VERBOSE(1, verbose_stream() << "num rules: " << m_context.get_rules().get_num_rules() << "\n";); m_context.transform_rules(); if (m_context.canceled()) { result = l_undef;