1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3 
4 Module Name:
5 
6     bool_rewriter.h
7 
8 Abstract:
9 
10     Basic rewriting rules for Boolean operators.
11 
12 Author:
13 
14     Leonardo (leonardo) 2011-04-04
15 
16 Notes:
17 
18 --*/
19 #pragma once
20 
21 #include "ast/ast.h"
22 #include "ast/rewriter/rewriter.h"
23 #include "util/params.h"
24 
25 /**
26    \brief Apply basic Boolean rewriting operations.
27 
28    Only depth 1 simplifications are performed.
29 
30    Note: there are no recursive calls.
31 
32    Note: arguments of AC operators are not sorted.
33    Note: arguments of = and xor are also not sorted.
34 
35    Note: By default, (AND A B) is not rewritten as (NOT (OR (NOT A) (NOT B)))
36 
37    Note: AND OR operators are flattened only if mk_flat_app, mk_flat_or, mk_flat_and are used.
38 
39    The following operators are expanded:
40    - => (implies)
41    - xor
42    - nand
43    - nor
44    - iff
45 
46    All methods run in time almost linear on the number of arguments.
47    Actually, this is not true when flattening is enabled.
48    A better approximation is O(Sum_{t \in args} size1(t)).
49    Where size1(t) = max{t->get_num_args(), 1}.
50 */
51 class bool_rewriter {
52     ast_manager &  m_manager;
53     bool           m_flat;
54     bool           m_local_ctx;
55     bool           m_elim_and;
56     bool           m_blast_distinct;
57     unsigned       m_blast_distinct_threshold;
58     bool           m_ite_extra_rules;
59     unsigned       m_local_ctx_limit;
60     unsigned       m_local_ctx_cost;
61     bool           m_elim_ite;
62 
63     br_status mk_flat_and_core(unsigned num_args, expr * const * args, expr_ref & result);
64     br_status mk_flat_or_core(unsigned num_args, expr * const * args, expr_ref & result);
65     br_status mk_nflat_and_core(unsigned num_args, expr * const * args, expr_ref & result);
66     br_status mk_nflat_or_core(unsigned num_args, expr * const * args, expr_ref & result);
67 
68     void mk_and_as_or(unsigned num_args, expr * const * args, expr_ref & result);
69 
70     expr * mk_or_app(unsigned num_args, expr * const * args);
71     bool simp_nested_not_or(unsigned num_args, expr * const * args, expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, expr_ref & result);
72     expr * simp_arg(expr * arg, expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, bool & modified);
73     void mk_nested_ite(expr * new_c, expr * new_t, expr * new_e, expr_ref & result);
74     bool simp_nested_eq_ite(expr * t, expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, expr_ref & result);
75     bool local_ctx_simp(unsigned num_args, expr * const * args, expr_ref & result);
76     br_status try_ite_value(app * ite, app * val, expr_ref & result);
77 
78     void push_new_arg(expr* arg, expr_ref_vector& new_args, expr_fast_mark1& neg_lits, expr_fast_mark2& pos_lits);
79 
80 public:
m_manager(m)81     bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0) { updt_params(p); }
m()82     ast_manager & m() const { return m_manager; }
get_fid()83     family_id get_fid() const { return m().get_basic_family_id(); }
is_eq(expr * t)84     bool is_eq(expr * t) const { return m().is_eq(t); }
85 
flat()86     bool flat() const { return m_flat; }
set_flat(bool f)87     void set_flat(bool f) { m_flat = f; }
elim_and()88     bool elim_and() const { return m_elim_and; }
set_elim_and(bool f)89     void set_elim_and(bool f) { m_elim_and = f; }
reset_local_ctx_cost()90     void reset_local_ctx_cost() { m_local_ctx_cost = 0; }
91 
92     void updt_params(params_ref const & p);
93 
94     static void get_param_descrs(param_descrs & r);
95 
96     // The core methods return true if a rewrite-step/simplification was applied
97     // to the arguments, and the result is stored in 'result'. Otherwise, they return false
98     // and result.get == 0.
99 
100     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
mk_app(func_decl * f,unsigned num_args,expr * const * args,expr_ref & result)101     void mk_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
102         if (mk_app_core(f, num_args, args, result) == BR_FAILED)
103             result = m().mk_app(f, num_args, args);
104     }
105 
106     br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
107     br_status mk_distinct_core(unsigned num_args, expr * const * args, expr_ref & result);
mk_iff_core(expr * lhs,expr * rhs,expr_ref & result)108     br_status mk_iff_core(expr * lhs, expr * rhs, expr_ref & result) { return mk_eq_core(lhs, rhs, result); }
mk_and_core(unsigned num_args,expr * const * args,expr_ref & result)109     br_status mk_and_core(unsigned num_args, expr * const * args, expr_ref & result) {
110         if (m_elim_and) {
111             mk_and_as_or(num_args, args, result);
112             return BR_DONE;
113         }
114         else if (m_flat) {
115             return mk_flat_and_core(num_args, args, result);
116         }
117         else {
118             return mk_nflat_and_core(num_args, args, result);
119         }
120     }
mk_or_core(unsigned num_args,expr * const * args,expr_ref & result)121     br_status mk_or_core(unsigned num_args, expr * const * args, expr_ref & result) {
122         return m_flat ?
123             mk_flat_or_core(num_args, args, result) :
124             mk_nflat_or_core(num_args, args, result);
125     }
126     br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result);
127     br_status mk_not_core(expr * t, expr_ref & result);
128 
129     app* mk_eq(expr* lhs, expr* rhs);
130 
mk_eq(expr * lhs,expr * rhs,expr_ref & result)131     void mk_eq(expr * lhs, expr * rhs, expr_ref & result) {
132         if (mk_eq_core(lhs, rhs, result) == BR_FAILED)
133             result = mk_eq(lhs, rhs);
134     }
mk_eq_rw(expr * lhs,expr * rhs)135     expr_ref mk_eq_rw(expr* lhs, expr* rhs) {
136         expr_ref r(m()), _lhs(lhs, m()), _rhs(rhs, m());
137         mk_eq(lhs, rhs, r);
138         return r;
139     }
mk_xor(expr * a,expr * b)140     expr_ref mk_xor(expr* a, expr* b) {
141        expr_ref result(m());
142        mk_xor(a, b, result);
143        return result;
144     }
mk_iff(expr * lhs,expr * rhs,expr_ref & result)145     void mk_iff(expr * lhs, expr * rhs, expr_ref & result) { mk_eq(lhs, rhs, result); }
146     void mk_xor(expr * lhs, expr * rhs, expr_ref & result);
mk_and(unsigned num_args,expr * const * args,expr_ref & result)147     void mk_and(unsigned num_args, expr * const * args, expr_ref & result) {
148         if (mk_and_core(num_args, args, result) == BR_FAILED) {
149             SASSERT(!m_elim_and);
150             result = m().mk_and(num_args, args);
151         }
152     }
mk_or(unsigned num_args,expr * const * args,expr_ref & result)153     void mk_or(unsigned num_args, expr * const * args, expr_ref & result) {
154         if (mk_or_core(num_args, args, result) == BR_FAILED)
155             result = m().mk_or(num_args, args);
156     }
mk_or(unsigned num_args,expr * const * args)157     expr_ref mk_or(unsigned num_args, expr * const * args) {
158         expr_ref result(m());
159         mk_or(num_args, args, result);
160         return result;
161     }
mk_and(unsigned num_args,expr * const * args)162     expr_ref mk_and(unsigned num_args, expr * const * args) {
163         expr_ref result(m());
164         mk_and(num_args, args, result);
165         return result;
166     }
mk_or(expr_ref_vector const & args)167     expr_ref mk_or(expr_ref_vector const& args) {
168         expr_ref result(m());
169         mk_or(args.size(), args.data(), result);
170         return result;
171     }
mk_and(expr_ref_vector const & args)172     expr_ref mk_and(expr_ref_vector const& args) {
173         expr_ref result(m());
174         mk_and(args.size(), args.data(), result);
175         return result;
176     }
mk_and(expr * a,expr * b)177     expr_ref mk_and(expr* a, expr* b) {
178         expr_ref result(m());
179         mk_and(a, b, result);
180         return result;
181     }
mk_or(expr * a,expr * b)182     expr_ref mk_or(expr* a, expr* b) {
183         expr_ref result(m());
184         mk_or(a, b, result);
185         return result;
186     }
187 
mk_and(expr * arg1,expr * arg2,expr_ref & result)188     void mk_and(expr * arg1, expr * arg2, expr_ref & result) {
189         expr * args[2] = {arg1, arg2};
190         mk_and(2, args, result);
191     }
mk_or(expr * arg1,expr * arg2,expr_ref & result)192     void mk_or(expr * arg1, expr * arg2, expr_ref & result) {
193         expr * args[2] = {arg1, arg2};
194         mk_or(2, args, result);
195     }
mk_and(expr * arg1,expr * arg2,expr * arg3,expr_ref & result)196     void mk_and(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
197         expr * args[3] = {arg1, arg2, arg3};
198         mk_and(3, args, result);
199     }
mk_or(expr * arg1,expr * arg2,expr * arg3,expr_ref & result)200     void mk_or(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
201         expr * args[3] = {arg1, arg2, arg3};
202         mk_or(3, args, result);
203     }
204     void mk_implies(expr * lhs, expr * rhs, expr_ref & result);
mk_ite(expr * c,expr * t,expr * e,expr_ref & result)205     void mk_ite(expr * c, expr * t, expr * e, expr_ref & result) {
206         if (mk_ite_core(c, t, e, result) == BR_FAILED)
207             result = m().mk_ite(c, t, e);
208     }
mk_ite(expr * c,expr * t,expr * e)209     expr_ref mk_ite(expr * c, expr * t, expr * e) {
210         expr_ref r(m());
211         mk_ite(c, t, e, r);
212         return r;
213     }
mk_distinct(unsigned num_args,expr * const * args,expr_ref & result)214     void mk_distinct(unsigned num_args, expr * const * args, expr_ref & result) {
215         if (mk_distinct_core(num_args, args, result) == BR_FAILED)
216             result = m().mk_distinct(num_args, args);
217     }
mk_not(expr * t,expr_ref & result)218     void mk_not(expr * t, expr_ref & result) {
219         if (mk_not_core(t, result) == BR_FAILED)
220             result = m().mk_not(t);
221     }
mk_not(expr * t)222     expr_ref mk_not(expr* t) {
223         expr_ref r(m());
224         mk_not(t, r);
225         return r;
226     }
227 
228     void mk_nand(unsigned num_args, expr * const * args, expr_ref & result);
229     void mk_nor(unsigned num_args, expr * const * args, expr_ref & result);
230     void mk_nand(expr * arg1, expr * arg2, expr_ref & result);
231     void mk_nor(expr * arg1, expr * arg2, expr_ref & result);
232     void mk_ge2(expr* a, expr* b, expr* c, expr_ref& result);
233 };
234 
235 struct bool_rewriter_cfg : public default_rewriter_cfg {
236     bool_rewriter m_r;
flat_assocbool_rewriter_cfg237     bool flat_assoc(func_decl * f) const { return m_r.flat() && (m_r.m().is_and(f) || m_r.m().is_or(f)); }
rewrite_patternsbool_rewriter_cfg238     bool rewrite_patterns() const { return false; }
reduce_appbool_rewriter_cfg239     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
240         result_pr = nullptr;
241         if (f->get_family_id() != m_r.get_fid())
242             return BR_FAILED;
243         return m_r.mk_app_core(f, num, args, result);
244     }
bool_rewriter_cfgbool_rewriter_cfg245     bool_rewriter_cfg(ast_manager & m, params_ref const & p):m_r(m, p) {}
246 };
247 
248 class bool_rewriter_star : public rewriter_tpl<bool_rewriter_cfg> {
249     bool_rewriter_cfg m_cfg;
250 public:
bool_rewriter_star(ast_manager & m,params_ref const & p)251     bool_rewriter_star(ast_manager & m, params_ref const & p):
252         rewriter_tpl<bool_rewriter_cfg>(m, false, m_cfg),
253         m_cfg(m, p) {}
254 };
255 
256