Searched refs:m_lemmas_lim (Results 1 – 4 of 4) sorted by relevance
2413 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()
634 unsigned m_lemmas_lim; member
2425 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()
633 unsigned m_lemmas_lim; member