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

remove pointer comparisons/hash

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-04-23 00:22:14 -07:00 • committed by Nuno Lopes
parent eead1bbc48
commit d849dbf21f
18 changed files with 81 additions and 37 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/muz_qe/dl_base.h
View file

@ -656,6 +656,7 @@ namespace datalog {
typedef sort * relation_sort;
typedef ptr_vector<sort> relation_signature_base0;
typedef ptr_hash<sort> relation_sort_hash;
typedef app * relation_element;
typedef app_ref relation_element_ref;
@ -739,8 +740,8 @@ namespace datalog {
struct hash {
unsigned operator()(relation_signature const& s) const {
relation_sort const* sorts = s.c_ptr();
return string_hash(reinterpret_cast<char const*>(sorts), sizeof(*sorts)*s.size(), 12); }
return obj_vector_hash<relation_signature>(s);
}
};
struct eq {
@ -816,9 +817,11 @@ namespace datalog {
typedef uint64 table_sort;
typedef svector<table_sort> table_signature_base0;
typedef uint64_hash table_sort_hash;
typedef uint64 table_element;
typedef svector<table_element> table_fact;
typedef uint64_hash table_element_hash;
struct table_traits {
typedef table_plugin plugin;
@ -881,8 +884,8 @@ namespace datalog {
public:
struct hash {
unsigned operator()(table_signature const& s) const {
table_sort const* sorts = s.c_ptr();
return string_hash(reinterpret_cast<char const*>(sorts), sizeof(*sorts)*s.size(), 12); }
return svector_hash<table_sort_hash>()(s);
}
};
struct eq {

2
src/muz_qe/dl_compiler.cpp
View file

@ -36,7 +36,7 @@ namespace datalog {
}
void compiler::ensure_predicate_loaded(func_decl * pred, instruction_block & acc) {
pred2idx::entry * e = m_pred_regs.insert_if_not_there2(pred, UINT_MAX);
pred2idx::obj_map_entry * e = m_pred_regs.insert_if_not_there2(pred, UINT_MAX);
if(e->get_data().m_value!=UINT_MAX) {
//predicate is already loaded
return;

3
src/muz_qe/dl_compiler.h
View file

@ -41,7 +41,8 @@ namespace datalog {
typedef hashtable<unsigned, u_hash, u_eq> int_set;
typedef u_map<unsigned> int2int;
typedef u_map<unsigned_vector> int2ints;
typedef map<func_decl *, reg_idx, ptr_hash<func_decl>,ptr_eq<func_decl> > pred2idx;
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;

4
src/muz_qe/dl_context.cpp
View file

@ -813,9 +813,7 @@ namespace datalog {
void context::transform_rules() {
m_transf.reset();
if (get_params().filter_rules()) {
m_transf.register_plugin(alloc(mk_filter_rules, *this));
}
m_transf.register_plugin(alloc(mk_filter_rules, *this));
m_transf.register_plugin(alloc(mk_simple_joins, *this));
if (unbound_compressor()) {
m_transf.register_plugin(alloc(mk_unbound_compressor, *this));

2
src/muz_qe/dl_finite_product_relation.h
View file

@ -47,7 +47,7 @@ namespace datalog {
}
struct hash {
unsigned operator()(const rel_spec & o) const {
return o.m_inner_kind^int_vector_hash(o.m_table_cols);
return o.m_inner_kind^svector_hash<bool_hash>()(o.m_table_cols);
}
};
};

8
src/muz_qe/dl_mk_filter_rules.h
View file

@ -45,14 +45,18 @@ namespace datalog {
filter_key(ast_manager & m) : new_pred(m), filter_args(m) {}
unsigned hash() const {
return new_pred->hash() ^ int_vector_hash(filter_args);
unsigned r = new_pred->hash();
for (unsigned i = 0; i < filter_args.size(); ++i) {
r ^= filter_args[i]->hash();
}
return r;
}
bool operator==(const filter_key & o) const {
return o.new_pred==new_pred && vectors_equal(o.filter_args, filter_args);
}
};
typedef map<filter_key*, func_decl*, obj_ptr_hash<filter_key>, deref_eq<filter_key> > filter_cache;
typedef obj_map<filter_key, func_decl*> filter_cache;
context & m_context;
ast_manager & m_manager;

7
src/muz_qe/dl_mk_magic_sets.h
View file

@ -47,6 +47,11 @@ namespace datalog {
AD_BOUND
};
struct a_flag_hash {
typedef a_flag data;
unsigned operator()(a_flag x) const { return x; }
};
struct adornment : public svector<a_flag> {
void populate(app * lit, const var_idx_set & bound_vars);
@ -71,7 +76,7 @@ namespace datalog {
return m_pred==o.m_pred && m_adornment==o.m_adornment;
}
unsigned hash() const {
return m_pred->hash()^int_vector_hash(m_adornment);
return m_pred->hash()^svector_hash<a_flag_hash>()(m_adornment);
}
};

10
src/muz_qe/dl_mk_similarity_compressor.cpp
View file

@ -29,6 +29,7 @@ namespace datalog {
m_manager(ctx.get_manager()),
m_threshold_count(ctx.similarity_compressor_threshold()),
m_result_rules(ctx.get_rule_manager()),
m_modified(false),
m_pinned(m_manager) {
SASSERT(m_threshold_count>1);
}
@ -55,6 +56,9 @@ namespace datalog {
return (a>b) ? 1 : ( (a==b) ? 0 : -1);
}
template<typename T>
static int aux_compare(T* a, T* b);
static int compare_var_args(app* t1, app* t2) {
SASSERT(t1->get_num_args()==t2->get_num_args());
int res;
@ -88,7 +92,7 @@ namespace datalog {
if ((skip_countdown--) == 0) {
continue;
}
res = aux_compare(t1->get_arg(i), t2->get_arg(i));
res = aux_compare(t1->get_arg(i)->get_id(), t2->get_arg(i)->get_id());
if (res!=0) { return res; }
}
return 0;
@ -113,7 +117,7 @@ namespace datalog {
for (int i=-1; i<pos_tail_sz; i++) {
app * t1 = get_by_tail_index(r1, i);
app * t2 = get_by_tail_index(r2, i);
res = aux_compare(t1->get_decl(), t2->get_decl());
res = aux_compare(t1->get_decl()->get_id(), t2->get_decl()->get_id());
if (res!=0) { return res; }
res = compare_var_args(t1, t2);
if (res!=0) { return res; }
@ -121,7 +125,7 @@ namespace datalog {
unsigned tail_sz = r1->get_tail_size();
for (unsigned i=pos_tail_sz; i<tail_sz; i++) {
res = aux_compare(r1->get_tail(i), r2->get_tail(i));
res = aux_compare(r1->get_tail(i)->get_id(), r2->get_tail(i)->get_id());
if (res!=0) { return res; }
}

6
src/muz_qe/dl_product_relation.h
View file

@ -40,8 +40,12 @@ namespace datalog {
class filter_equal_fn;
class filter_identical_fn;
class filter_interpreted_fn;
struct fid_hash {
typedef family_id data;
unsigned operator()(data x) const { return static_cast<unsigned>(x); }
};
rel_spec_store<rel_spec> m_spec_store;
rel_spec_store<rel_spec, svector_hash<fid_hash> > m_spec_store;
family_id get_relation_kind(const product_relation & r);

2
src/muz_qe/dl_relation_manager.h
View file

@ -605,7 +605,7 @@ namespace datalog {
/**
This is a helper class for relation_plugins whose relations can be of various kinds.
*/
template<class Spec, class Hash=int_vector_hash_proc<Spec>, class Eq=vector_eq_proc<Spec> >
template<class Spec, class Hash, class Eq=vector_eq_proc<Spec> >
class rel_spec_store {
typedef relation_signature::hash r_hash;
typedef relation_signature::eq r_eq;

3
src/muz_qe/dl_rule_transformer.cpp
View file

@ -107,6 +107,9 @@ 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);

2
src/muz_qe/dl_sieve_relation.h
View file

@ -52,7 +52,7 @@ namespace datalog {
struct hash {
unsigned operator()(const rel_spec & s) const {
return int_vector_hash(s.m_inner_cols)^s.m_inner_kind;
return svector_hash<bool_hash>()(s.m_inner_cols)^s.m_inner_kind;
}
};
};

2
src/muz_qe/dl_sparse_table.h
View file

@ -359,7 +359,7 @@ namespace datalog {
typedef svector<unsigned> key_spec; //sequence of columns in a key
typedef svector<table_element> key_value; //values of key columns
typedef map<key_spec, key_indexer*, int_vector_hash_proc<key_spec>,
typedef map<key_spec, key_indexer*, svector_hash_proc<unsigned_hash>,
vector_eq_proc<key_spec> > key_index_map;
static const store_offset NO_RESERVE = UINT_MAX;

2
src/muz_qe/dl_table.h
View file

@ -73,7 +73,7 @@ namespace datalog {
class our_iterator_core;
typedef hashtable<table_fact, int_vector_hash_proc<table_fact>,
typedef hashtable<table_fact, svector_hash_proc<table_element_hash>,
vector_eq_proc<table_fact> > storage;
storage m_data;

29
src/muz_qe/dl_util.h
View file

@ -587,17 +587,31 @@ namespace datalog {
}
template<class T>
unsigned int_vector_hash(const T & cont) {
return string_hash(reinterpret_cast<const char *>(cont.c_ptr()),
cont.size()*sizeof(typename T::data), 0);
struct default_obj_chash {
unsigned operator()(T const& cont, unsigned i) const {
return cont[i]->hash();
}
};
template<class T>
unsigned obj_vector_hash(const T & cont) {
return get_composite_hash(cont, cont.size(),default_kind_hash_proc<T>(), default_obj_chash<T>());
}
template<class T>
struct int_vector_hash_proc {
struct obj_vector_hash_proc {
unsigned operator()(const T & cont) const {
return int_vector_hash(cont);
return obj_vector_hash(cont);
}
};
template<class T>
struct svector_hash_proc {
unsigned operator()(const svector<typename T::data> & cont) const {
return svector_hash<T>()(cont);
}
};
template<class T>
struct vector_eq_proc {
bool operator()(const T & c1, const T & c2) const { return vectors_equal(c1, c2); }
@ -765,11 +779,6 @@ namespace datalog {
//
// -----------------------------------
struct uint64_hash {
typedef uint64 data;
unsigned operator()(uint64 x) const { return hash_ull(x); }
};
template<class T>
void universal_delete(T* ptr) {
dealloc(ptr);

2
src/muz_qe/rel_context.cpp
View file

@ -113,10 +113,12 @@ 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;

6
src/util/hash.h
View file

@ -20,6 +20,7 @@ Revision History:
#define _HASH_H_
#include<algorithm>
#include"util.h"
#ifndef __fallthrough
#define __fallthrough
@ -142,6 +143,11 @@ struct size_t_hash {
unsigned operator()(size_t x) const { return static_cast<unsigned>(x); }
};
struct uint64_hash {
typedef uint64 data;
unsigned operator()(uint64 x) const { return static_cast<unsigned>(x); }
};
struct bool_hash {
typedef bool data;
unsigned operator()(bool x) const { return static_cast<unsigned>(x); }

17
src/util/vector.h
View file

@ -432,24 +432,29 @@ typedef svector<unsigned> unsigned_vector;
typedef svector<char> char_vector;
typedef svector<double> double_vector;
template<typename Hash>
struct vector_hash {
template<typename Hash, typename Vec>
struct vector_hash_tpl {
Hash m_hash;
typedef vector<typename Hash::data> data;
typedef Vec data;
unsigned operator()(data const& v, unsigned idx) const { return m_hash(v[idx]); }
vector_hash(Hash const& h = Hash()):m_hash(h) {}
vector_hash_tpl(Hash const& h = Hash()):m_hash(h) {}
unsigned operator()(data const& v) const {
if (v.empty()) {
return 778;
}
return get_composite_hash<data, default_kind_hash_proc<data>, vector_hash>(v, v.size());
return get_composite_hash<data, default_kind_hash_proc<data>, vector_hash_tpl>(v, v.size());
}
};
template<typename Hash>
struct vector_hash : public vector_hash_tpl<Hash, vector<typename Hash::data> > {};
template<typename Hash>
struct svector_hash : public vector_hash_tpl<Hash, svector<typename Hash::data> > {};
#endif /* _VECTOR_H_ */