Searched refs:m_assigned_literals_lim (Results 1 – 6 of 6) sorted by relevance
67 SASSERT(n <= s.m_assigned_literals_lim); in display_num_assigned_literals_per_lvl()68 out << (s.m_assigned_literals_lim - n) << " "; in display_num_assigned_literals_per_lvl()69 n = s.m_assigned_literals_lim; in display_num_assigned_literals_per_lvl()
627 unsigned m_assigned_literals_lim; member724 return m_scopes[scope_lvl - 1].m_assigned_literals_lim; in get_decision_literal_pos()
1926 s.m_assigned_literals_lim = m_assigned_literals.size(); in push_scope()2431 unassign_vars(s.m_assigned_literals_lim); in pop_scope_core()3984 unsigned head = m_scope_lvl == 0 ? 0 : m_scopes[m_scope_lvl - 1].m_assigned_literals_lim; in forget_phase_of_vars_in_current_level()4329 unsigned guess_idx = s.m_assigned_literals_lim; in get_guessed_literals()
626 unsigned m_assigned_literals_lim; member723 return m_scopes[scope_lvl - 1].m_assigned_literals_lim; in get_decision_literal_pos()
1938 s.m_assigned_literals_lim = m_assigned_literals.size(); in push_scope()2443 unassign_vars(s.m_assigned_literals_lim); in pop_scope_core()3994 unsigned head = m_scope_lvl == 0 ? 0 : m_scopes[m_scope_lvl - 1].m_assigned_literals_lim; in forget_phase_of_vars_in_current_level()4339 unsigned guess_idx = s.m_assigned_literals_lim; in get_guessed_literals()