Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dequality_query.cpp151 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 Dequality_query.h116 int getRepScore( Node n, Node f, int index, TypeNode v_tn );
/dports/math/z3/z3-z3-4.8.13/src/ast/fpa/
H A Dfpa2bv_converter.cpp2708 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 Dfpa2bv_converter.cpp2702 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);