Home
last modified time | relevance | path

Searched refs:m_unhandled_functions (Results 1 – 4 of 4) sorted by relevance

/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/
H A Deuf_solver.cpp40 m_unhandled_functions(m), in solver()
139 if (m_unhandled_functions.contains(f)) in unhandled_function()
143 m_unhandled_functions.push_back(f); in unhandled_function()
144 m_trail.push(push_back_vector<solver, func_decl_ref_vector>(m_unhandled_functions)); in unhandled_function()
H A Deuf_solver.h90 func_decl_ref_vector m_unhandled_functions; variable
352 func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; } in unhandled_functions()
/dports/math/z3/z3-z3-4.8.13/src/sat/smt/
H A Deuf_solver.cpp47 m_unhandled_functions(m), in solver()
149 if (m_unhandled_functions.contains(f)) in unhandled_function()
153 m_unhandled_functions.push_back(f); in unhandled_function()
154 m_trail.push(push_back_vector<func_decl_ref_vector>(m_unhandled_functions)); in unhandled_function()
H A Deuf_solver.h98 func_decl_ref_vector m_unhandled_functions; variable
398 func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; } in unhandled_functions()