Searched refs:m_ackerman (Results 1 – 12 of 12) sorted by relevance
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/ |
| H A D | euf_solver.cpp | 352 if (s().value(lit) == l_false && m_ackerman) in propagate_literals()
353 m_ackerman->cg_conflict_eh(a, b); in propagate_literals()
551 if (m_ackerman) in simplify()
552 m_ackerman->propagate(); in simplify()
643 st.update("euf ackerman", m_stats.m_ackerman); in collect_statistics()
750 if (m_ackerman) in init_ackerman()
754 m_ackerman = alloc(ackerman, *this, m); in init_ackerman()
756 m_ackerman->used_eq_eh(a, b, lca); in init_ackerman()
759 m_ackerman->used_cc_eh(a, b); in init_ackerman()
|
| H A D | bv_solver.cpp | 55 m_ackerman(*this), in solver()
91 m_ackerman.used_eq_eh(v1, v2); in add_fixed_eq()
255 m_ackerman.used_diseq_eh(v1, v2); in new_diseq_eh()
547 m_ackerman.propagate(); in simplify()
664 st.update("bv ackerman", m_stats.m_ackerman); in collect_statistics()
|
| H A D | euf_solver.h | 60 unsigned m_ackerman; member
94 scoped_ptr<euf::ackerman> m_ackerman; variable
|
| H A D | bv_solver.h | 48 unsigned m_ackerman; member
194 ackerman m_ackerman; variable
|
| H A D | euf_ackerman.cpp | 164 ++s.m_stats.m_ackerman; in propagate()
|
| H A D | bv_internalize.cpp | 722 ++m_stats.m_ackerman; in assert_ackerman()
|
| /dports/math/z3/z3-z3-4.8.13/src/sat/smt/ |
| H A D | euf_solver.cpp | 385 if (s().value(lit) == l_false && m_ackerman) in propagate_literals()
386 m_ackerman->cg_conflict_eh(a, b); in propagate_literals()
732 if (m_ackerman) in simplify()
733 m_ackerman->propagate(); in simplify()
844 st.update("euf ackerman", m_stats.m_ackerman); in collect_statistics()
960 if (m_ackerman) in init_ackerman()
964 m_ackerman = alloc(ackerman, *this, m); in init_ackerman()
966 m_ackerman->used_eq_eh(a, b, lca); in init_ackerman()
969 m_ackerman->used_cc_eh(a, b); in init_ackerman()
|
| H A D | bv_solver.cpp | 55 m_ackerman(*this), in solver()
92 m_ackerman.used_eq_eh(v1, v2); in add_fixed_eq()
262 m_ackerman.used_diseq_eh(v1, v2); in new_diseq_eh()
538 m_ackerman.propagate(); in simplify()
655 st.update("bv ackerman", m_stats.m_ackerman); in collect_statistics()
|
| H A D | euf_ackerman.cpp | 165 ++s.m_stats.m_ackerman; in propagate()
|
| H A D | bv_solver.h | 48 unsigned m_ackerman; member
198 ackerman m_ackerman; variable
|
| H A D | euf_solver.h | 68 unsigned m_ackerman; member
102 scoped_ptr<euf::ackerman> m_ackerman; variable
|
| H A D | bv_internalize.cpp | 753 ++m_stats.m_ackerman; in assert_ackerman()
|