Searched refs:m_old_th_var (Results 1 – 6 of 6) sorted by relevance
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/euf/ |
| H A D | euf_egraph.h | 115 unsigned m_old_th_var : 24; member
129 tag(tag_t::is_replace_th_var), r1(n), n1(nullptr), m_th_id(id), m_old_th_var(v) {} in update_record()
|
| H A D | euf_egraph.cpp | 310 p.r1->replace_th_var(p.m_old_th_var, p.m_th_id); in pop()
|
| /dports/math/z3/z3-z3-4.8.13/src/ast/euf/ |
| H A D | euf_egraph.h | 119 unsigned m_old_th_var : 24; member
135 tag(tag_t::is_replace_th_var), r1(n), n1(nullptr), m_th_id(id), m_old_th_var(v) {} in update_record()
|
| H A D | euf_egraph.cpp | 356 p.r1->replace_th_var(p.m_old_th_var, p.m_th_id); in pop()
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | smt_internalizer.cpp | 1721 unsigned m_old_th_var:24; member in smt::replace_th_var_trail
1726 m_old_th_var(old_var) { in replace_th_var_trail()
1731 m_enode->replace_th_var(m_old_th_var, m_th_id); in undo()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | smt_internalizer.cpp | 1715 unsigned m_old_th_var:24; member in smt::replace_th_var_trail
1720 m_old_th_var(old_var) { in replace_th_var_trail()
1725 m_enode->replace_th_var(m_old_th_var, m_th_id); in undo()
|