mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

fix(datatype): only use pointer equality for enode_tbl

Browse source
This commit is contained in:
Simon Cruanes 2018-04-03 11:53:29 -05:00
parent 9df140343a
commit fa10e510bb
2 changed files with 1 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/smt_enode.h
View file

@ -171,9 +171,6 @@ namespace smt {
m_interpreted = true;
}
inline bool equal(const enode & other) const {
return m_owner == other.m_owner;
}
void del_eh(ast_manager & m, bool update_children_parent = true);
@ -426,9 +423,5 @@ namespace smt {
};
inline bool operator==(const smt::enode & e1, const smt::enode & e2) {
return e1.equal(e2);
}
#endif /* SMT_ENODE_H_ */

2
src/smt/theory_datatype.h
View file

@ -73,7 +73,7 @@ namespace smt {
void sign_recognizer_conflict(enode * c, enode * r);
typedef enum { ENTER, EXIT } stack_op;
typedef map<enode*, enode*, obj_ptr_hash<enode>, deref_eq<enode> > parent_tbl;
typedef map<enode*, enode*, obj_ptr_hash<enode>, ptr_eq<enode> > parent_tbl;
typedef std::pair<stack_op, enode*> stack_entry;
ptr_vector<enode> m_to_unmark;