mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-18 02:16:40 +00:00
Code Activity

remove unused code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-25 03:36:30 -07:00
parent f8b8d5b870
commit 1e751422e1
2 changed files with 17 additions and 105 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/theory_special_relations.h
View file

@ -112,22 +112,10 @@ namespace smt {
typedef u_map<atom*> bool_var2atom;
special_relations_util m_util;
arith_util m_autil;
atoms m_atoms;
unsigned_vector m_atoms_lim;
obj_map<func_decl, relation*> m_relations;
bool_var2atom m_bool_var2atom;
scoped_ptr<solver> m_nested_solver;
struct atom_hash {
size_t operator()(atom const& a) const {
return std::hash<int>()(a.v1()) ^ std::hash<int>()(a.v2()) ^ std::hash<bool>()(a.phase());
}
};
u_map<expr*> expr_cache;
u_map<atom*> atom_cache;
sort* m_int_sort;
void del_atoms(unsigned old_size);
lbool final_check(relation& r);