1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 datatype_rewriter.cpp
7
8 Abstract:
9
10 Basic rewriting rules for Datatypes.
11
12 Author:
13
14 Leonardo (leonardo) 2011-04-06
15
16 Notes:
17
18 --*/
19 #include "ast/rewriter/datatype_rewriter.h"
20
mk_app_core(func_decl * f,unsigned num_args,expr * const * args,expr_ref & result)21 br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
22 SASSERT(f->get_family_id() == get_fid());
23 switch(f->get_decl_kind()) {
24 case OP_DT_CONSTRUCTOR: return BR_FAILED;
25 case OP_DT_RECOGNISER:
26 SASSERT(num_args == 1);
27 result = m_util.mk_is(m_util.get_recognizer_constructor(f), args[0]);
28 return BR_REWRITE1;
29 case OP_DT_IS:
30 //
31 // simplify is_cons(cons(x,y)) -> true
32 // simplify is_cons(nil) -> false
33 //
34 SASSERT(num_args == 1);
35 if (!is_app(args[0]) || !m_util.is_constructor(to_app(args[0])))
36 return BR_FAILED;
37 if (to_app(args[0])->get_decl() == m_util.get_recognizer_constructor(f))
38 result = m().mk_true();
39 else
40 result = m().mk_false();
41 return BR_DONE;
42 case OP_DT_ACCESSOR: {
43 //
44 // simplify head(cons(x,y)) -> x
45 //
46 SASSERT(num_args == 1);
47 if (!is_app(args[0]) || !m_util.is_constructor(to_app(args[0])))
48 return BR_FAILED;
49
50 app * a = to_app(args[0]);
51 func_decl * c_decl = a->get_decl();
52 if (c_decl != m_util.get_accessor_constructor(f))
53 return BR_FAILED;
54 ptr_vector<func_decl> const & acc = *m_util.get_constructor_accessors(c_decl);
55 SASSERT(acc.size() == a->get_num_args());
56 unsigned num = acc.size();
57 for (unsigned i = 0; i < num; ++i) {
58 if (f == acc[i]) {
59 // found it.
60 result = a->get_arg(i);
61 return BR_DONE;
62 }
63 }
64 UNREACHABLE();
65 break;
66 }
67 case OP_DT_UPDATE_FIELD: {
68 SASSERT(num_args == 2);
69 if (!is_app(args[0]) || !m_util.is_constructor(to_app(args[0])))
70 return BR_FAILED;
71 app * a = to_app(args[0]);
72 func_decl * c_decl = a->get_decl();
73 func_decl * acc = m_util.get_update_accessor(f);
74 if (c_decl != m_util.get_accessor_constructor(acc)) {
75 result = a;
76 return BR_DONE;
77 }
78 ptr_vector<func_decl> const & accs = *m_util.get_constructor_accessors(c_decl);
79 SASSERT(accs.size() == a->get_num_args());
80 unsigned num = accs.size();
81 ptr_buffer<expr> new_args;
82 for (unsigned i = 0; i < num; ++i) {
83
84 if (acc == accs[i]) {
85 new_args.push_back(args[1]);
86 }
87 else {
88 new_args.push_back(a->get_arg(i));
89 }
90 }
91 result = m().mk_app(c_decl, num, new_args.data());
92 return BR_DONE;
93 }
94 default:
95 UNREACHABLE();
96 }
97
98 return BR_FAILED;
99 }
100
mk_eq_core(expr * lhs,expr * rhs,expr_ref & result)101 br_status datatype_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
102 if (!is_app(lhs) || !is_app(rhs) || !m_util.is_constructor(to_app(lhs)) || !m_util.is_constructor(to_app(rhs)))
103 return BR_FAILED;
104 if (to_app(lhs)->get_decl() != to_app(rhs)->get_decl()) {
105 result = m().mk_false();
106 return BR_DONE;
107 }
108
109 // Remark: In datatype_simplifier_plugin, we used
110 // m_basic_simplifier to create '=' and 'and' applications in the
111 // following code. This trick not guarantee that the final expression
112 // will be fully simplified.
113 //
114 // Example:
115 // The assertion
116 // (assert (= (cons a1 (cons a2 (cons a3 (cons (+ a4 1) (cons (+ a5 c5) (cons a6 nil))))))
117 // (cons b1 (cons b2 (cons b3 (cons b4 (cons b5 (cons b6 nil))))))))
118 //
119 // After applying asserted_formulas::reduce(), the following formula was generated.
120 //
121 // (= a1 b1)
122 // (= a2 b2)
123 // (= a3 b3)
124 // (= (+ a4 (* (- 1) b4)) (- 1))
125 // (= (+ c5 a5) b5) <<< NOT SIMPLIFIED WITH RESPECT TO ARITHMETIC
126 // (= (cons a6 nil) (cons b6 nil))) <<< NOT SIMPLIFIED WITH RESPECT TO DATATYPE theory
127 //
128 // Note that asserted_formulas::reduce() applied the simplifier many times.
129 // After the first simplification step we had:
130 // (= a1 b1)
131 // (= (cons a2 (cons a3 (cons (+ a4 1) (cons (+ a5 c5) (cons a6 nil))))))
132 // (cons b2 (cons b3 (cons b4 (cons b5 (cons b6 nil))))))
133
134 ptr_buffer<expr> eqs;
135 unsigned num = to_app(lhs)->get_num_args();
136 SASSERT(num == to_app(rhs)->get_num_args());
137 for (unsigned i = 0; i < num; ++i) {
138 eqs.push_back(m().mk_eq(to_app(lhs)->get_arg(i), to_app(rhs)->get_arg(i)));
139 }
140 result = m().mk_and(eqs.size(), eqs.data());
141 return BR_REWRITE2;
142 }
143