| /dports/math/py-z3-solver/z3-z3-4.8.10/src/util/ |
| H A D | mpf.cpp | 298 mk_inf(ebits, sbits, o.sign, o); in set()
340 mk_inf(ebits, sbits, x.sign, o); in set()
605 mk_inf(x.ebits, x.sbits, y.sign, o); in mul()
611 mk_inf(x.ebits, x.sbits, x.sign, o); in mul()
617 mk_inf(x.ebits, x.sbits, !y.sign, o); in mul()
623 mk_inf(x.ebits, x.sbits, !x.sign, o); in mul()
680 mk_inf(x.ebits, x.sbits, y.sign, o); in div()
763 mk_inf(x.ebits, x.sbits, y.sign, o); in fma()
771 mk_inf(x.ebits, x.sbits, x.sign, o); in fma()
1917 mk_inf(ebits, sbits, false, o); in mk_pinf()
[all …]
|
| H A D | hwf.h | 148 void mk_inf(bool sign, hwf & o);
|
| H A D | mpf.h | 183 void mk_inf(unsigned ebits, unsigned sbits, bool sign, mpf & o);
|
| H A D | hwf.cpp | 519 void hwf_manager::mk_inf(bool sign, hwf & o) { in mk_inf() function in hwf_manager
|
| /dports/math/z3/z3-z3-4.8.13/src/util/ |
| H A D | mpf.cpp | 298 mk_inf(ebits, sbits, o.sign, o); in set()
340 mk_inf(ebits, sbits, x.sign, o); in set()
605 mk_inf(x.ebits, x.sbits, y.sign, o); in mul()
611 mk_inf(x.ebits, x.sbits, x.sign, o); in mul()
617 mk_inf(x.ebits, x.sbits, !y.sign, o); in mul()
623 mk_inf(x.ebits, x.sbits, !x.sign, o); in mul()
680 mk_inf(x.ebits, x.sbits, y.sign, o); in div()
763 mk_inf(x.ebits, x.sbits, y.sign, o); in fma()
771 mk_inf(x.ebits, x.sbits, x.sign, o); in fma()
1917 mk_inf(ebits, sbits, false, o); in mk_pinf()
[all …]
|
| H A D | hwf.h | 148 void mk_inf(bool sign, hwf & o);
|
| H A D | mpf.h | 183 void mk_inf(unsigned ebits, unsigned sbits, bool sign, mpf & o);
|
| H A D | hwf.cpp | 519 void hwf_manager::mk_inf(bool sign, hwf & o) { in mk_inf() function in hwf_manager
|
| /dports/math/z3/z3-z3-4.8.13/src/qe/ |
| H A D | nlarith_util.cpp | 470 expr* mk_inf() { in mk_inf() function in nlarith::util::imp
491 expr* mk_inf(branch_conditions const& bc) { in mk_inf() function in nlarith::util::imp
492 return mk_inf(); in mk_inf()
531 … bc.add_branch(mk_and(es.size(), es.data()), m().mk_true(), subst, mk_inf(bc), z(), z(), z()); in inf_branch()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/qe/ |
| H A D | nlarith_util.cpp | 470 expr* mk_inf() { in mk_inf() function in nlarith::util::imp
491 expr* mk_inf(branch_conditions const& bc) { in mk_inf() function in nlarith::util::imp
492 return mk_inf(); in mk_inf()
531 … bc.add_branch(mk_and(es.size(), es.c_ptr()), m().mk_true(), subst, mk_inf(bc), z(), z(), z()); in inf_branch()
|
| /dports/math/z3/z3-z3-4.8.13/src/api/ml/ |
| H A D | z3.ml | 1310 let mk_inf = Z3native.mk_fpa_inf var
|
| H A D | z3.mli | 2041 val mk_inf : context -> Sort.sort -> bool -> Expr.expr val
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/api/ml/ |
| H A D | z3.ml | 1308 let mk_inf = Z3native.mk_fpa_inf var
|
| H A D | z3.mli | 2035 val mk_inf : context -> Sort.sort -> bool -> Expr.expr val
|