Searched refs:m_register_engine (Results 1 – 10 of 10) sorted by relevance
/dports/math/z3/z3-z3-4.8.13/src/muz/fp/ |
H A D | horn_tactic.cpp | 38 datalog::register_engine m_register_engine; member 46 m_ctx(m, m_register_engine, m_fparams) { in imp()
|
H A D | dl_cmds.cpp | 42 datalog::register_engine m_register_engine; member 81 m_context = alloc(datalog::context, m, m_register_engine, fparams(), m_params_ref); in init()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/fp/ |
H A D | horn_tactic.cpp | 38 datalog::register_engine m_register_engine; member 46 m_ctx(m, m_register_engine, m_fparams) { in imp()
|
H A D | dl_cmds.cpp | 42 datalog::register_engine m_register_engine; member 81 m_context = alloc(datalog::context, m, m_register_engine, fparams(), m_params_ref); in init()
|
/dports/math/z3/z3-z3-4.8.13/src/muz/base/ |
H A D | dl_context.h | 165 register_engine_base& m_register_engine; variable 236 register_engine_base& get_register_engine() { return m_register_engine; } in get_register_engine()
|
H A D | dl_context.cpp | 202 m_register_engine(re), in context() 929 m_engine = m_register_engine.mk_engine(get_engine(e)); in ensure_engine()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/base/ |
H A D | dl_context.h | 165 register_engine_base& m_register_engine; variable 236 register_engine_base& get_register_engine() { return m_register_engine; } in get_register_engine()
|
H A D | dl_context.cpp | 201 m_register_engine(re), in context() 928 m_engine = m_register_engine.mk_engine(get_engine(e)); in ensure_engine()
|
/dports/math/z3/z3-z3-4.8.13/src/api/ |
H A D | api_datalog.cpp | 44 datalog::register_engine m_register_engine; member in api::fixedpoint_context 52 m_context(m, m_register_engine, p), in fixedpoint_context()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/api/ |
H A D | api_datalog.cpp | 44 datalog::register_engine m_register_engine; member in api::fixedpoint_context 52 m_context(m, m_register_engine, p), in fixedpoint_context()
|