1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 push_app_ite.cpp
7
8 Abstract:
9
10 TODO: Write a better ite lifter
11
12
13 Author:
14
15 Leonardo de Moura (leonardo) 2008-05-14.
16
17 Revision History:
18
19 --*/
20 #include "ast/rewriter/push_app_ite.h"
21 #include "ast/ast_pp.h"
22
23
has_ite_arg(ast_manager & m,unsigned num_args,expr * const * args)24 static int has_ite_arg(ast_manager& m, unsigned num_args, expr * const * args) {
25 for (unsigned i = 0; i < num_args; i++)
26 if (m.is_ite(args[i]))
27 return i;
28 return -1;
29 }
30
31
32 /**
33 \brief Default (conservative) implementation. Return true if there one and only one ite-term argument.
34 */
is_target(func_decl * decl,unsigned num_args,expr * const * args)35 bool push_app_ite_cfg::is_target(func_decl * decl, unsigned num_args, expr * const * args) {
36 if (m.is_ite(decl))
37 return false;
38 bool found_ite = false;
39 for (unsigned i = 0; i < num_args; i++) {
40 if (m.is_ite(args[i]) && !m.is_bool(args[i])) {
41 if (found_ite) {
42 if (m_conservative)
43 return false;
44 }
45 else {
46 found_ite = true;
47 }
48 }
49 }
50 CTRACE("push_app_ite", found_ite, tout << "found target for push app ite:\n";
51 tout << "conservative " << m_conservative << "\n";
52 tout << decl->get_name();
53 for (unsigned i = 0; i < num_args; i++) tout << " " << mk_pp(args[i], m);
54 tout << "\n";);
55 return found_ite;
56 }
57
reduce_app(func_decl * f,unsigned num,expr * const * args,expr_ref & result,proof_ref & result_pr)58 br_status push_app_ite_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
59 if (!is_target(f, num, args)) {
60 return BR_FAILED;
61 }
62 int ite_arg_idx = has_ite_arg(m, num, args);
63 if (ite_arg_idx < 0) {
64 return BR_FAILED;
65 }
66 app * ite = to_app(args[ite_arg_idx]);
67 expr * c = nullptr, * t = nullptr, * e = nullptr;
68 VERIFY(m.is_ite(ite, c, t, e));
69 expr ** args_prime = const_cast<expr**>(args);
70 expr * old = args_prime[ite_arg_idx];
71 args_prime[ite_arg_idx] = t;
72 expr_ref t_new(m.mk_app(f, num, args_prime), m);
73 args_prime[ite_arg_idx] = e;
74 expr_ref e_new(m.mk_app(f, num, args_prime), m);
75 args_prime[ite_arg_idx] = old;
76 result = m.mk_ite(c, t_new, e_new);
77 TRACE("push_app_ite", tout << result << "\n";);
78 if (m.proofs_enabled()) {
79 result_pr = m.mk_rewrite(m.mk_app(f, num, args), result);
80 }
81 return BR_REWRITE2;
82 }
83
is_target(func_decl * decl,unsigned num_args,expr * const * args)84 bool ng_push_app_ite_cfg::is_target(func_decl * decl, unsigned num_args, expr * const * args) {
85 bool r = push_app_ite_cfg::is_target(decl, num_args, args);
86 if (!r)
87 return false;
88 for (unsigned i = 0; i < num_args; i++)
89 if (!is_ground(args[i]))
90 return true;
91 return false;
92 }
93