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