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

minor cleanup

Browse source 
Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
This commit is contained in:
Nuno Lopes 2013-04-23 10:02:44 -07:00
parent d849dbf21f
commit 08eb85fe3d
4 changed files with 0 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/muz_qe/dl_compiler.h
View file

@ -42,7 +42,6 @@ namespace datalog {
typedef u_map<unsigned> int2int;
typedef u_map<unsigned_vector> int2ints;
typedef obj_map<func_decl, reg_idx> pred2idx;
// typedef map<func_decl *, reg_idx, ptr_hash<func_decl>,ptr_eq<func_decl> > pred2idx;
typedef unsigned_vector var_vector;
typedef ptr_vector<func_decl> func_decl_vector;

3
src/muz_qe/dl_rule_transformer.cpp
View file

@ -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);

1
src/muz_qe/fixedpoint_params.pyg
View file

@ -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"),

2
src/muz_qe/rel_context.cpp
View file

@ -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;