Home
last modified time | relevance | path

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

/dports/math/z3/z3-z3-4.8.13/src/smt/
H A Dsmt_context.cpp2413 del_clauses(m_lemmas, bs.m_lemmas_lim); in pop_scope_core()
2691 num_del_clauses += simplify_clauses(m_lemmas, bs.m_lemmas_lim); in simplify_clauses()
2725 unsigned start_at = m_base_lvl == 0 ? 0 : m_base_scopes[m_base_lvl - 1].m_lemmas_lim; in del_inactive_lemmas1()
2785 unsigned start_at = m_base_lvl == 0 ? 0 : m_base_scopes[m_base_lvl - 1].m_lemmas_lim; in del_inactive_lemmas2()
2925 bs.m_lemmas_lim = m_lemmas.size(); in push()
H A Dsmt_context.h634 unsigned m_lemmas_lim; member
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/
H A Dsmt_context.cpp2425 del_clauses(m_lemmas, bs.m_lemmas_lim); in pop_scope_core()
2703 num_del_clauses += simplify_clauses(m_lemmas, bs.m_lemmas_lim); in simplify_clauses()
2737 unsigned start_at = m_base_lvl == 0 ? 0 : m_base_scopes[m_base_lvl - 1].m_lemmas_lim; in del_inactive_lemmas1()
2797 unsigned start_at = m_base_lvl == 0 ? 0 : m_base_scopes[m_base_lvl - 1].m_lemmas_lim; in del_inactive_lemmas2()
2937 bs.m_lemmas_lim = m_lemmas.size(); in push()
H A Dsmt_context.h633 unsigned m_lemmas_lim; member