mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 04:41:21 +00:00
Code Activity

fixing templates for broken windows hash functions

Browse source
This commit is contained in:
Ken McMillan 2013-12-15 17:31:46 -08:00
parent 852f53d6a6
commit 1e8c04be8e
5 changed files with 16 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/duality/duality.h
View file

@ -1011,7 +1011,7 @@ private:
// Allow to hash on nodes and edges in deterministic way // Allow to hash on nodes and edges in deterministic way
namespace stl_ext { namespace hash_space {
template <> template <>
class hash<Duality::RPFP::Node *> { class hash<Duality::RPFP::Node *> {
public: public:
@ -1021,7 +1021,7 @@ namespace stl_ext {
}; };
} }
namespace stl_ext { namespace hash_space {
template <> template <>
class hash<Duality::RPFP::Edge *> { class hash<Duality::RPFP::Edge *> {
public: public:

2
src/duality/duality_wrapper.cpp
View file

@ -606,7 +606,7 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
void model::show_hash() const { void model::show_hash() const {
std::ostringstream ss; std::ostringstream ss;
model_smt2_pp(ss, m(), *m_model, 0); model_smt2_pp(ss, m(), *m_model, 0);
stl_ext::hash<std::string> hasher; hash_space::hash<std::string> hasher;
unsigned h = hasher(ss.str()); unsigned h = hasher(ss.str());
std::cout << "model hash: " << h << "\n"; std::cout << "model hash: " << h << "\n";
} }

18
src/interp/iz3base.h
View file

@ -146,14 +146,7 @@ class iz3base : public iz3mgr, public scopes {
ranges(){scope_computed = false;} ranges(){scope_computed = false;}
}; };
// We only use this for sym_range_hash, which has no range destructor stl_ext::hash_map<symb,range> sym_range_hash;
struct symb_hash {
size_t operator()(const symb &s) const {
return (size_t) s;
}
};
stl_ext::hash_map<symb,range,symb_hash> sym_range_hash;
stl_ext::hash_map<ast,ranges> ast_ranges_hash; stl_ext::hash_map<ast,ranges> ast_ranges_hash;
stl_ext::hash_map<ast,ast> simplify_memo; stl_ext::hash_map<ast,ast> simplify_memo;
stl_ext::hash_map<ast,int> frame_map; // map assertions to frames stl_ext::hash_map<ast,int> frame_map; // map assertions to frames
@ -187,6 +180,15 @@ class iz3base : public iz3mgr, public scopes {
}; };
namespace hash_space {
template <>
class hash<iz3mgr::symb> {
public:
size_t operator()(const iz3mgr::symb &s) const {
return (size_t) s;
}
};
}

2
src/interp/iz3foci.cpp
View file

@ -58,7 +58,7 @@ public:
} }
}; };
typedef hash_map<symb,foci2::symb,symb_hash> FuncDeclToSymbol; typedef hash_map<symb,foci2::symb> FuncDeclToSymbol;
FuncDeclToSymbol func_decl_to_symbol; // maps Z3 func decls to symbols FuncDeclToSymbol func_decl_to_symbol; // maps Z3 func decls to symbols
typedef hash_map<foci2::symb,symb> SymbolToFuncDecl; typedef hash_map<foci2::symb,symb> SymbolToFuncDecl;

11
src/interp/iz3translate.cpp
View file

@ -619,14 +619,7 @@ public:
return 1; return 1;
} }
// We only use this for debugging purposes void symbols_out_of_scope_rec(hash_set<ast> &memo, hash_set<symb> &symb_memo, int frame, const ast &t){
struct symb_hash {
size_t operator()(const symb &s) const {
return (size_t) s;
}
};
void symbols_out_of_scope_rec(hash_set<ast> &memo, hash_set<symb,symb_hash> &symb_memo, int frame, const ast &t){
if(memo.find(t) != memo.end()) if(memo.find(t) != memo.end())
return; return;
memo.insert(t); memo.insert(t);
@ -645,7 +638,7 @@ public:
void symbols_out_of_scope(int frame, const ast &t){ void symbols_out_of_scope(int frame, const ast &t){
hash_set<ast> memo; hash_set<ast> memo;
hash_set<symb,symb_hash> symb_memo; hash_set<symb> symb_memo;
symbols_out_of_scope_rec(memo,symb_memo,frame,t); symbols_out_of_scope_rec(memo,symb_memo,frame,t);
} }