/dports/math/z3/z3-z3-4.8.13/src/math/interval/ |
H A D | dep_intervals.cpp | 134 if (m_num_manager.lt(r.to_mpq(), lower(i))) in is_above() 136 if (m_num_manager.eq(lower(i), r.to_mpq()) && m_config.lower_is_open(i)) in is_above() 144 if (m_num_manager.lt(upper(i), r.to_mpq())) in is_below() 146 if (m_num_manager.eq(upper(i), r.to_mpq()) && m_config.upper_is_open(i)) in is_below()
|
H A D | dep_intervals.h | 98 void set_lower(interval& a, rational const& n) const { set_lower(a, n.to_mpq()); } in set_lower() 99 void set_upper(interval& a, rational const& n) const { set_upper(a, n.to_mpq()); } in set_upper() 167 void set_lower(interval& a, rational const& n) const { m_config.set_lower(a, n.to_mpq()); } in set_lower() 168 void set_upper(interval& a, rational const& n) const { m_config.set_upper(a, n.to_mpq()); } in set_upper() 226 m_imanager.mul(r.to_mpq(), a, b); in mul()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/interval/ |
H A D | dep_intervals.cpp | 134 if (m_num_manager.lt(r.to_mpq(), lower(i))) in is_above() 136 if (m_num_manager.eq(lower(i), r.to_mpq()) && m_config.lower_is_open(i)) in is_above() 144 if (m_num_manager.lt(upper(i), r.to_mpq())) in is_below() 146 if (m_num_manager.eq(upper(i), r.to_mpq()) && m_config.upper_is_open(i)) in is_below()
|
H A D | dep_intervals.h | 98 void set_lower(interval& a, rational const& n) const { set_lower(a, n.to_mpq()); } in set_lower() 99 void set_upper(interval& a, rational const& n) const { set_upper(a, n.to_mpq()); } in set_upper() 167 void set_lower(interval& a, rational const& n) const { m_config.set_lower(a, n.to_mpq()); } in set_lower() 168 void set_upper(interval& a, rational const& n) const { m_config.set_upper(a, n.to_mpq()); } in set_upper() 226 m_imanager.mul(r.to_mpq(), a, b); in mul()
|
/dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/ |
H A D | fpa_rewriter.cpp | 128 const mpq & q = r1.to_mpq(); in mk_to_fp() 162 m_fm.set(v, ebits, sbits, rmv, r1.to_mpq()); in mk_to_fp() 181 m_fm.set(v, ebits, sbits, rmv, r1.to_mpq()); in mk_to_fp() 197 m_fm.set(v, ebits, sbits, rmv, r2.to_mpq().numerator(), r1.to_mpq()); in mk_to_fp() 211 m_fm.set(v, ebits, sbits, rmv, r1.to_mpq().numerator(), r2.to_mpq()); in mk_to_fp() 219 SASSERT(m_fm.mpz_manager().is_one(r2.to_mpq().denominator())); in mk_to_fp() 226 r3.to_mpq().numerator()); in mk_to_fp() 249 m_fm.set(v, ebits, sbits, rmv, r.to_mpq()); in mk_to_fp_unsigned() 693 SASSERT(mpzm.is_one(rexp.to_mpq().denominator())); in mk_fp() 694 SASSERT(mpzm.is_one(rsig.to_mpq().denominator())); in mk_fp() [all …]
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/rewriter/ |
H A D | fpa_rewriter.cpp | 127 const mpq & q = r1.to_mpq(); in mk_to_fp() 161 m_fm.set(v, ebits, sbits, rmv, r1.to_mpq()); in mk_to_fp() 180 m_fm.set(v, ebits, sbits, rmv, r1.to_mpq()); in mk_to_fp() 196 m_fm.set(v, ebits, sbits, rmv, r2.to_mpq().numerator(), r1.to_mpq()); in mk_to_fp() 210 m_fm.set(v, ebits, sbits, rmv, r1.to_mpq().numerator(), r2.to_mpq()); in mk_to_fp() 218 SASSERT(m_fm.mpz_manager().is_one(r2.to_mpq().denominator())); in mk_to_fp() 225 r3.to_mpq().numerator()); in mk_to_fp() 248 m_fm.set(v, ebits, sbits, rmv, r.to_mpq()); in mk_to_fp_unsigned() 692 SASSERT(mpzm.is_one(rexp.to_mpq().denominator())); in mk_fp() 693 SASSERT(mpzm.is_one(rsig.to_mpq().denominator())); in mk_fp() [all …]
|
/dports/math/z3/z3-z3-4.8.13/src/math/simplex/ |
H A D | simplex.cpp | 64 inf_mgr.set(q, fin.to_mpq(), inf.to_mpq()); in ensure_rational_solution()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/simplex/ |
H A D | simplex.cpp | 64 inf_mgr.set(q, fin.to_mpq(), inf.to_mpq());
|
/dports/math/z3/z3-z3-4.8.13/src/api/ |
H A D | api_algebraic.cpp | 134 _am.set(_av, av.to_mpq()); \ 145 _am.set(_bv, bv.to_mpq()); \ 222 _am.set(av, get_rational(c, a).to_mpq()); in Z3_algebraic_root() 244 _am.set(av, get_rational(c, a).to_mpq()); in Z3_algebraic_power() 269 _am.set(_av, av.to_mpq()); \ 278 _am.set(_bv, bv.to_mpq()); \ 330 _am.set(tmp, get_rational(c, a[i]).to_mpq()); in to_anum_vector()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/api/ |
H A D | api_algebraic.cpp | 134 _am.set(_av, av.to_mpq()); \ 145 _am.set(_bv, bv.to_mpq()); \ 222 _am.set(av, get_rational(c, a).to_mpq()); in Z3_algebraic_root() 244 _am.set(av, get_rational(c, a).to_mpq()); in Z3_algebraic_power() 269 _am.set(_av, av.to_mpq()); \ 278 _am.set(_bv, bv.to_mpq()); \ 330 _am.set(tmp, get_rational(c, a[i]).to_mpq()); in to_anum_vector()
|
/dports/math/z3/z3-z3-4.8.13/src/smt/ |
H A D | theory_wmaxsat.cpp | 146 mgr.set(q, m_zcost, m_den.to_mpq().numerator()); in get_cost() 152 m_zmin_cost = (m_rmin_cost * m_den).to_mpq().numerator(); in init_min_cost() 352 mpq const& q = r.to_mpq(); in normalize() 362 m_zmin_cost = r.to_mpq().numerator(); in normalize()
|
H A D | theory_fpa.cpp | 90 mpzm.set(all_z, all_r.to_mpq().numerator()); in mk_value() 111 SASSERT(mpzm.is_one(sgn_r.to_mpq().denominator())); in mk_value() 112 SASSERT(mpzm.is_one(exp_r.to_mpq().denominator())); in mk_value() 113 SASSERT(mpzm.is_one(sig_r.to_mpq().denominator())); in mk_value() 115 mpzm.set(sgn_z, sgn_r.to_mpq().numerator()); in mk_value() 116 mpzm.set(exp_z, exp_r.to_mpq().numerator()); in mk_value() 117 mpzm.set(sig_z, sig_r.to_mpq().numerator()); in mk_value()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
H A D | theory_wmaxsat.cpp | 146 mgr.set(q, m_zcost, m_den.to_mpq().numerator()); in mtd_probe() 152 m_zmin_cost = (m_rmin_cost * m_den).to_mpq().numerator(); in mtd_probe() 352 mpq const& q = r.to_mpq(); in mtd_probe() 362 m_zmin_cost = r.to_mpq().numerator(); in mtd_probe()
|
H A D | theory_fpa.cpp | 90 mpzm.set(all_z, all_r.to_mpq().numerator()); in mk_value() 111 SASSERT(mpzm.is_one(sgn_r.to_mpq().denominator())); in mk_value() 112 SASSERT(mpzm.is_one(exp_r.to_mpq().denominator())); in mk_value() 113 SASSERT(mpzm.is_one(sig_r.to_mpq().denominator())); in mk_value() 115 mpzm.set(sgn_z, sgn_r.to_mpq().numerator()); in mk_value() 116 mpzm.set(exp_z, exp_r.to_mpq().numerator()); in mk_value() 117 mpzm.set(sig_z, sig_r.to_mpq().numerator()); in mk_value()
|
/dports/math/z3/z3-z3-4.8.13/src/math/lp/ |
H A D | nla_intervals.h | 44 … void set_lower(interval& a, rational const& n) const { m_dep_intervals.set_lower(a, n.to_mpq()); } in set_lower() 45 … void set_upper(interval& a, rational const& n) const { m_dep_intervals.set_upper(a, n.to_mpq()); } in set_upper()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/lp/ |
H A D | nla_intervals.h | 44 … void set_lower(interval& a, rational const& n) const { m_dep_intervals.set_lower(a, n.to_mpq()); } in set_lower() 45 … void set_upper(interval& a, rational const& n) const { m_dep_intervals.set_upper(a, n.to_mpq()); } in set_upper()
|
/dports/math/z3/z3-z3-4.8.13/src/math/subpaving/tactic/ |
H A D | expr2subpaving.cpp | 144 qm().set(n, k.to_mpq().numerator()); in process_num() 145 qm().set(d, k.to_mpq().denominator()); in process_num() 176 qm().set(n, k.to_mpq().numerator()); in process_mul() 177 qm().set(d, k.to_mpq().denominator()); in process_mul()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/subpaving/tactic/ |
H A D | expr2subpaving.cpp | 143 qm().set(n, k.to_mpq().numerator()); 144 qm().set(d, k.to_mpq().denominator()); 175 qm().set(n, k.to_mpq().numerator()); 176 qm().set(d, k.to_mpq().denominator());
|
/dports/math/z3/z3-z3-4.8.13/src/test/ |
H A D | simplex.cpp | 75 coeffs.push_back(v[i].to_mpq().numerator()); in add_row() 83 coeffs.push_back(b.to_mpq().numerator()); in add_row()
|
H A D | mpff.cpp | 130 fm.to_mpq(fa, qm, qa); \ 133 fm.to_mpq(fb, qm, qb); \ 138 fm.to_mpq(fc1, qm, qt); \ 144 fm.to_mpq(fc2, qm, qt); \ 185 fm.to_mpq(a, qm, c); in MK_BIN_RANDOM_TST()
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/test/ |
H A D | simplex.cpp | 75 coeffs.push_back(v[i].to_mpq().numerator()); in add_row() 83 coeffs.push_back(b.to_mpq().numerator()); in add_row()
|
/dports/math/z3/z3-z3-4.8.13/src/math/realclosure/ |
H A D | realclosure.cpp | 1034 static mpq & to_mpq(value * v) { in to_mpq() function 2586 ::to_mpq(qm(), v, v_q); in mk_rational() 2597 qm().set(to_mpq(a), v); in update_mpq_value() 3064 return qm().eq(to_mpq(a), to_mpq(b)); in struct_eq() 5059 qm().add(to_mpq(a), to_mpq(b), v); in add() 5088 qm().sub(to_mpq(a), to_mpq(b), v); in sub() 5124 qm().set(v, to_mpq(a)); in neg() 5270 qm().mul(to_mpq(a), to_mpq(b), v); in mul() 5305 qm().div(to_mpq(a), to_mpq(b), v); in div() 5693 if (qm().eq(to_mpq(a), to_mpq(b))) in compare() [all …]
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/realclosure/ |
H A D | realclosure.cpp | 1034 static mpq & to_mpq(value * v) { in to_mpq() function 2586 ::to_mpq(qm(), v, v_q); in mk_rational() 2597 qm().set(to_mpq(a), v); in update_mpq_value() 3064 return qm().eq(to_mpq(a), to_mpq(b)); in struct_eq() 5059 qm().add(to_mpq(a), to_mpq(b), v); in add() 5088 qm().sub(to_mpq(a), to_mpq(b), v); in sub() 5124 qm().set(v, to_mpq(a)); in neg() 5270 qm().mul(to_mpq(a), to_mpq(b), v); in mul() 5305 qm().div(to_mpq(a), to_mpq(b), v); in div() 5693 if (qm().eq(to_mpq(a), to_mpq(b))) in compare() [all …]
|
/dports/math/z3/z3-z3-4.8.13/src/math/polynomial/ |
H A D | algebraic_numbers.cpp | 797 to_mpq(qm(), lower(c), r); in refine() 818 to_mpq(qm(), lower(c), r); in refine_until_prec() 1461 to_mpq(qm(), i.lower(), il); in add() 1462 to_mpq(qm(), i.upper(), iu); in add() 1569 to_mpq(qm(), i.lower(), il); in mul() 2541 to_mpq(qm(), v, qv); in eval_at_mpbq() 2628 to_mpq(qm(), w, qw); in select() 2841 to_mpq(qm(), _l, l); in get_lower() 2852 to_mpq(qm(), _u, u); in get_upper() 3085 to_mpq(qm(), bq, l); in get_lower() [all …]
|
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/polynomial/ |
H A D | algebraic_numbers.cpp | 797 to_mpq(qm(), lower(c), r); in refine() 818 to_mpq(qm(), lower(c), r); in refine_until_prec() 1461 to_mpq(qm(), i.lower(), il); in add() 1462 to_mpq(qm(), i.upper(), iu); in add() 1569 to_mpq(qm(), i.lower(), il); in mul() 2523 to_mpq(qm(), v, qv); in eval_at_mpbq() 2610 to_mpq(qm(), w, qw); in select() 2823 to_mpq(qm(), _l, l); in get_lower() 2834 to_mpq(qm(), _u, u); in get_upper() 3067 to_mpq(qm(), bq, l); in get_lower() [all …]
|