Searched refs:pull_ite (Results 1 – 3 of 3) sorted by relevance
| /dports/math/z3/z3-z3-4.8.13/src/ast/rewriter/ |
| H A D | th_rewriter.cpp | 319 br_status pull_ite(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { in pull_ite() function
348 br_status pull_ite(expr_ref & result) { in pull_ite() function
351 …br_status st = pull_ite(to_app(t)->get_decl(), to_app(t)->get_num_args(), to_app(t)->get_args(), r… in pull_ite()
667 st = pull_ite(f, num, args, result); in reduce_app()
669 st = pull_ite(result); in reduce_app()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/rewriter/ |
| H A D | th_rewriter.cpp | 300 br_status pull_ite(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { in pull_ite() function
329 br_status pull_ite(expr_ref & result) { in pull_ite() function
332 …br_status st = pull_ite(to_app(t)->get_decl(), to_app(t)->get_num_args(), to_app(t)->get_args(), r… in pull_ite()
648 st = pull_ite(f, num, args, result); in reduce_app()
650 st = pull_ite(result); in reduce_app()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | extended_rewrite.cpp | 638 Node pull_ite = nm->mkNode(itek, nite[0], ip.second[0], ip.second[1]); in extendedRewritePullIte() local
639 pull_ite = Rewriter::rewrite(pull_ite); in extendedRewritePullIte()
640 if (pull_ite.getKind() == ITE) in extendedRewritePullIte()
642 Node new_pull_ite = extendedRewriteIte(itek, pull_ite, false); in extendedRewritePullIte()
657 debugExtendedRewrite(n, pull_ite, "ITE pull basic elim"); in extendedRewritePullIte()
658 return pull_ite; in extendedRewritePullIte()
|