Searched refs:v_tn (Results 1 – 4 of 4) sorted by relevance
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
H A D | equality_query.cpp | 151 TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType(); in getInternalRepresentative() local 152 std::map<Node, Node>& v_int_rep = d_int_rep[v_tn]; in getInternalRepresentative() 179 Trace("internal-rep-select") << " }, type = " << v_tn << std::endl; in getInternalRepresentative() 182 int score = getRepScore(eqc[i], q, index, v_tn); in getInternalRepresentative() 202 Assert( r_best.getType().isSubtypeOf( v_tn ) ); in getInternalRepresentative() 260 TypeNode v_tn) in getRepScore() argument 264 }else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type in getRepScore()
|
H A D | equality_query.h | 116 int getRepScore( Node n, Node f, int index, TypeNode v_tn );
|
/dports/math/z3/z3-z3-4.8.13/src/ast/fpa/ |
H A D | fpa2bv_converter.cpp | 2708 scoped_mpf v_tn(m_mpf_manager), v_tz(m_mpf_manager); in mk_to_fp_real() local 2712 m_util.fm().set(v_tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq()); in mk_to_fp_real() 2736 sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tn)) ? 1 : 0, 1); in mk_to_fp_real() 2737 sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1); in mk_to_fp_real() 2738 unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tn), ebits); in mk_to_fp_real()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/fpa/ |
H A D | fpa2bv_converter.cpp | 2702 scoped_mpf v_tn(m_mpf_manager), v_tz(m_mpf_manager); 2706 m_util.fm().set(v_tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq()); 2730 sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tn)) ? 1 : 0, 1); 2731 sig = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1); 2732 unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tn), ebits);
|