Lines Matching refs:premise
82 for (proof* premise : m.get_parents(pf)) in add_lowest_split_to_core()
83 if (m_ctx.is_b_open(premise)) in add_lowest_split_to_core()
84 todo.push_back(premise); in add_lowest_split_to_core()
150 proof * premise = m.get_parent(step, i); in compute_partial_core() local
152 if (m_ctx.is_b_open (premise)) { in compute_partial_core()
153 SASSERT(!m_ctx.is_a(premise)); in compute_partial_core()
155 if (m_ctx.is_b_pure (premise)) { in compute_partial_core()
158 … coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise))); in compute_partial_core()
167 … coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise))); in compute_partial_core()
174 … coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise))); in compute_partial_core()
197 expr* premise = args[i]; in compute_partial_core() local
200 brw.mk_not(premise, negatedPremise); in compute_partial_core()
264 proof * premise = m.get_parent(step, i); in compute_partial_core() local
266 if (m_ctx.is_b(premise) && !m_ctx.is_closed(premise)) in compute_partial_core()
268 SASSERT(!m_ctx.is_a(premise)); in compute_partial_core()
270 if (m_ctx.is_b_pure(premise)) in compute_partial_core()
274 (std::make_pair(abs(coefficient), to_app(m.get_fact(premise)))); in compute_partial_core()
540 for (proof* premise : m.get_parents(step)) { in advance_to_lowest_partial_cut()
541 if (m_ctx.is_b(premise)) { in advance_to_lowest_partial_cut()
542 todo_subproof.push_back(premise); in advance_to_lowest_partial_cut()
580 for (proof* premise : m.get_parents(current)) { in advance_to_lowest_partial_cut()
581 todo_subproof.push_back(premise); in advance_to_lowest_partial_cut()