Searched refs:m_user_propagator (Results 1 – 8 of 8) sorted by relevance
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/ |
H A D | euf_solver.h | 96 user::solver* m_user_propagator{ nullptr }; 192 if (!m_user_propagator) in check_for_user_propagator() 367 m_user_propagator->register_final(final_eh); in user_propagate_register_final() 371 m_user_propagator->register_fixed(fixed_eh); in user_propagate_register_fixed() 375 m_user_propagator->register_eq(eq_eh); in user_propagate_register_eq() 379 m_user_propagator->register_diseq(diseq_eh); in user_propagate_register_diseq() 383 return m_user_propagator->add_expr(e); in user_propagate_register()
|
H A D | euf_solver.cpp | 790 m_user_propagator = alloc(user::solver, *this); in user_propagate_init() 791 m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh); in user_propagate_init() 793 m_user_propagator->push(); in user_propagate_init() 794 m_solvers.push_back(m_user_propagator); in user_propagate_init() 795 m_id2solver.setx(m_user_propagator->get_id(), m_user_propagator, nullptr); in user_propagate_init() 799 …return m_user_propagator && m_user_propagator->has_fixed() && n->get_th_var(m_user_propagator->get… in watches_fixed() 803 theory_var v = n->get_th_var(m_user_propagator->get_id()); in assign_fixed() 804 m_user_propagator->new_fixed_eh(v, val, sz, explain); in assign_fixed()
|
/dports/math/z3/z3-z3-4.8.13/src/sat/smt/ |
H A D | euf_solver.h | 103 user_solver::solver* m_user_propagator = nullptr; variable 206 if (!m_user_propagator) in check_for_user_propagator() 413 m_user_propagator->register_final(final_eh); in user_propagate_register_final() 417 m_user_propagator->register_fixed(fixed_eh); in user_propagate_register_fixed() 421 m_user_propagator->register_eq(eq_eh); in user_propagate_register_eq() 425 m_user_propagator->register_diseq(diseq_eh); in user_propagate_register_diseq() 429 return m_user_propagator->add_expr(e); in user_propagate_register()
|
H A D | euf_solver.cpp | 1000 m_user_propagator = alloc(user_solver::solver, *this); in user_propagate_init() 1001 m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh); in user_propagate_init() 1003 m_user_propagator->push(); in user_propagate_init() 1004 m_solvers.push_back(m_user_propagator); in user_propagate_init() 1005 m_id2solver.setx(m_user_propagator->get_id(), m_user_propagator, nullptr); in user_propagate_init() 1009 …return m_user_propagator && m_user_propagator->has_fixed() && n->get_th_var(m_user_propagator->get… in watches_fixed() 1013 theory_var v = n->get_th_var(m_user_propagator->get_id()); in assign_fixed() 1014 m_user_propagator->new_fixed_eh(v, val, sz, explain); in assign_fixed()
|
/dports/math/z3/z3-z3-4.8.13/src/smt/ |
H A D | smt_context.h | 91 user_propagator* m_user_propagator; variable 1703 if (!m_user_propagator) in user_propagate_register_final() 1705 m_user_propagator->register_final(final_eh); in user_propagate_register_final() 1709 if (!m_user_propagator) in user_propagate_register_fixed() 1711 m_user_propagator->register_fixed(fixed_eh); in user_propagate_register_fixed() 1715 if (!m_user_propagator) in user_propagate_register_eq() 1717 m_user_propagator->register_eq(eq_eh); in user_propagate_register_eq() 1721 if (!m_user_propagator) in user_propagate_register_diseq() 1723 m_user_propagator->register_diseq(diseq_eh); in user_propagate_register_diseq() 1727 if (!m_user_propagator) in user_propagate_register() [all …]
|
H A D | smt_context.cpp | 58 m_user_propagator(nullptr), in context() 197 if (!src_ctx.m_user_propagator) in copy_user_propagator() 201 m_user_propagator = reinterpret_cast<user_propagator*>(p); in copy_user_propagator() 202 SASSERT(m_user_propagator); in copy_user_propagator() 204 app* e = src_ctx.m_user_propagator->get_expr(i); in copy_user_propagator() 205 m_user_propagator->add_expr(tr(e)); in copy_user_propagator() 2893 m_user_propagator = alloc(user_propagator, *this); in user_propagate_init() 2896 m_user_propagator->push_scope_eh(); in user_propagate_init() 2897 register_plugin(m_user_propagator); in user_propagate_init() 2901 …return m_user_propagator && m_user_propagator->has_fixed() && n->get_th_var(m_user_propagator->get… in watches_fixed() [all …]
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
H A D | smt_context.h | 92 user_propagator* m_user_propagator; variable 1696 if (!m_user_propagator) in user_propagate_register_final() 1698 m_user_propagator->register_final(final_eh); in user_propagate_register_final() 1702 if (!m_user_propagator) in user_propagate_register_fixed() 1704 m_user_propagator->register_fixed(fixed_eh); in user_propagate_register_fixed() 1708 if (!m_user_propagator) in user_propagate_register_eq() 1710 m_user_propagator->register_eq(eq_eh); in user_propagate_register_eq() 1714 if (!m_user_propagator) in user_propagate_register_diseq() 1716 m_user_propagator->register_diseq(diseq_eh); in user_propagate_register_diseq() 1720 if (!m_user_propagator) in user_propagate_register() [all …]
|
H A D | smt_context.cpp | 57 m_user_propagator(nullptr), in context() 210 if (!src_ctx.m_user_propagator) in copy_user_propagator() 214 m_user_propagator = reinterpret_cast<user_propagator*>(p); in copy_user_propagator() 215 SASSERT(m_user_propagator); in copy_user_propagator() 217 app* e = src_ctx.m_user_propagator->get_expr(i); in copy_user_propagator() 218 m_user_propagator->add_expr(tr(e)); in copy_user_propagator() 2905 m_user_propagator = alloc(user_propagator, *this); in user_propagate_init() 2908 m_user_propagator->push_scope_eh(); in user_propagate_init() 2909 register_plugin(m_user_propagator); in user_propagate_init() 2913 …return m_user_propagator && m_user_propagator->has_fixed() && n->get_th_var(m_user_propagator->get… in watches_fixed() [all …]
|