Home
last modified time | relevance | path

Searched refs:arith_k_sum_is_small (Results 1 – 4 of 4) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/smt/
H A Dsmt_setup.cpp320 if (!st.m_has_rational && !m_params.m_model && st.arith_k_sum_is_small()) in setup_QF_RDL()
379 if (st.arith_k_sum_is_small()) in setup_QF_IDL()
429 else if (st.arith_k_sum_is_small()) in setup_QF_UFIDL()
786 bool fixnum = st.arith_k_sum_is_small() && m_params.m_arith_fixnum; in setup_arith()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/
H A Dsmt_setup.cpp319 if (!st.m_has_rational && !m_params.m_model && st.arith_k_sum_is_small()) in setup_QF_RDL()
378 if (st.arith_k_sum_is_small()) in setup_QF_IDL()
428 else if (st.arith_k_sum_is_small()) in setup_QF_UFIDL()
779 bool fixnum = st.arith_k_sum_is_small() && m_params.m_arith_fixnum; in setup_arith()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/
H A Dstatic_features.h154 bool arith_k_sum_is_small() const { return m_arith_k_sum < rational(INT_MAX / 8); } in arith_k_sum_is_small() function
/dports/math/z3/z3-z3-4.8.13/src/ast/
H A Dstatic_features.h154 bool arith_k_sum_is_small() const { return m_arith_k_sum < rational(INT_MAX / 8); } in arith_k_sum_is_small() function