Home
last modified time | relevance | path

Searched refs:m_b_split_vec (Results 1 – 2 of 2) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/math/lp/
H A Dcross_nested.h34 ptr_vector<nex> m_b_split_vec; variable
379 m_b_split_vec.clear(); in pre_split()
385 m_b_split_vec.push_back(const_cast<nex*>(ce)); in pre_split()
390 SASSERT(a->size() >= 2 && m_b_split_vec.size()); in pre_split()
393 if (m_b_split_vec.size() == 1) { in pre_split()
394 b = m_b_split_vec[0]; in pre_split()
397 SASSERT(m_b_split_vec.size() > 1); in pre_split()
398 b = m_nex_creator.mk_sum(m_b_split_vec); in pre_split()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/lp/
H A Dcross_nested.h34 ptr_vector<nex> m_b_split_vec; variable
379 m_b_split_vec.clear(); in pre_split()
385 m_b_split_vec.push_back(const_cast<nex*>(ce)); in pre_split()
390 SASSERT(a->size() >= 2 && m_b_split_vec.size()); in pre_split()
393 if (m_b_split_vec.size() == 1) { in pre_split()
394 b = m_b_split_vec[0]; in pre_split()
397 SASSERT(m_b_split_vec.size() > 1); in pre_split()
398 b = m_nex_creator.mk_sum(m_b_split_vec); in pre_split()