Home
last modified time | relevance | path

Searched refs:m_num_diff_ineqs (Results 1 – 6 of 6) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/ast/
H A Dstatic_features.cpp94 m_num_diff_ineqs = 0; in reset()
245 m_num_diff_ineqs++; in update_core()
639 out << "NUM_DIFF_INEQS " << m_num_diff_ineqs << "\n"; in display_primitive()
669 …IFF " << (m_num_arith_eqs == m_num_diff_eqs && m_num_arith_ineqs == m_num_diff_ineqs && m_num_arit… in display()
673 …out << "PERC_DIFF_INEQS " << (m_num_arith_ineqs > 0 ? (double) m_num_diff_ineqs / (double) m_num_a… in display()
H A Dstatic_features.h94 unsigned m_num_diff_ineqs; // <= m_num_arith_ineqs member
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/
H A Dstatic_features.cpp94 m_num_diff_ineqs = 0; in reset()
245 m_num_diff_ineqs++; in update_core()
625 out << "NUM_DIFF_INEQS " << m_num_diff_ineqs << "\n"; in display_primitive()
655 …IFF " << (m_num_arith_eqs == m_num_diff_eqs && m_num_arith_ineqs == m_num_diff_ineqs && m_num_arit… in display()
659 …out << "PERC_DIFF_INEQS " << (m_num_arith_ineqs > 0 ? (double) m_num_diff_ineqs / (double) m_num_a… in display()
H A Dstatic_features.h94 unsigned m_num_diff_ineqs; // <= m_num_arith_ineqs member
/dports/math/z3/z3-z3-4.8.13/src/smt/
H A Dsmt_setup.cpp261 st.m_num_arith_ineqs == st.m_num_diff_ineqs; in is_in_diff_logic()
267 (st.m_num_diff_ineqs > 0 || st.m_num_diff_eqs > 0 || st.m_num_diff_terms > 0) in is_diff_logic()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/
H A Dsmt_setup.cpp260 st.m_num_arith_ineqs == st.m_num_diff_ineqs; in is_in_diff_logic()
266 (st.m_num_diff_ineqs > 0 || st.m_num_diff_eqs > 0 || st.m_num_diff_terms > 0) in is_diff_logic()