Home
last modified time | relevance | path

Searched refs:res_sgn_c3 (Results 1 – 2 of 2) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/ast/fpa/
H A Dfpa2bv_converter.cpp522 expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m); in add_core() local
529 res_sgn_c3 = m.mk_app(bvfid, OP_BAND, c_sgn, d_sgn); in add_core()
530 expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 }; in add_core()
1681 expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m); in mk_fma() local
1688 res_sgn_c3 = m.mk_app(bvfid, OP_BAND, e_sgn, f_sgn); in mk_fma()
1689 expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 }; in mk_fma()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/fpa/
H A Dfpa2bv_converter.cpp521 expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m);
528 res_sgn_c3 = m.mk_app(bvfid, OP_BAND, c_sgn, d_sgn);
529 expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 };
1670 expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m);
1677 res_sgn_c3 = m.mk_app(bvfid, OP_BAND, e_sgn, f_sgn);
1678 expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 };