# z3 / src / ast / rewriter / bool_rewriter.h

  1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 /*++ Copyright (c) 2011 Microsoft Corporation Module Name: bool_rewriter.h Abstract: Basic rewriting rules for Boolean operators. Author: Leonardo (leonardo) 2011-04-04 Notes: --*/ #ifndef _BOOL_REWRITER_H_ #define _BOOL_REWRITER_H_ #include"ast.h" #include"rewriter.h" #include"params.h" /** \brief Apply basic Boolean rewriting operations. Only depth 1 simplifications are performed. Note: there are no recursive calls. Note: arguments of AC operators are not sorted. Note: arguments of = and xor are also not sorted. Note: By default, (AND A B) is not rewritten as (NOT (OR (NOT A) (NOT B))) Note: AND OR operators are flattened only if mk_flat_app, mk_flat_or, mk_flat_and are used. The following operators are expanded: - => (implies) - xor - nand - nor - iff All methods run in time almost linear on the number of arguments. Actually, this is not true when flattening is enabled. A better approximation is O(Sum_{t \in args} size1(t)). Where size1(t) = max{t->get_num_args(), 1}. */ class bool_rewriter { ast_manager & m_manager; bool m_flat; bool m_local_ctx; bool m_elim_and; bool m_blast_distinct; bool m_ite_extra_rules; unsigned m_local_ctx_limit; unsigned m_local_ctx_cost; br_status mk_flat_and_core(unsigned num_args, expr * const * args, expr_ref & result); br_status mk_flat_or_core(unsigned num_args, expr * const * args, expr_ref & result); br_status mk_nflat_and_core(unsigned num_args, expr * const * args, expr_ref & result); br_status mk_nflat_or_core(unsigned num_args, expr * const * args, expr_ref & result); void mk_and_as_or(unsigned num_args, expr * const * args, expr_ref & result); expr * mk_or_app(unsigned num_args, expr * const * args); bool simp_nested_not_or(unsigned num_args, expr * const * args, expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, expr_ref & result); expr * simp_arg(expr * arg, expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, bool & modified); void mk_nested_ite(expr * new_c, expr * new_t, expr * new_e, expr_ref & result); bool simp_nested_eq_ite(expr * t, expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, expr_ref & result); bool local_ctx_simp(unsigned num_args, expr * const * args, expr_ref & result); br_status try_ite_value(app * ite, app * val, expr_ref & result); public: bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0) { updt_params(p); } ast_manager & m() const { return m_manager; } family_id get_fid() const { return m().get_basic_family_id(); } bool is_eq(expr * t) const { return m().is_eq(t) || m().is_iff(t); } bool flat() const { return m_flat; } void set_flat(bool f) { m_flat = f; } bool elim_and() const { return m_elim_and; } void set_elim_and(bool f) { m_elim_and = f; } void reset_local_ctx_cost() { m_local_ctx_cost = 0; } void updt_params(params_ref const & p); static void get_param_descrs(param_descrs & r); // The core methods return true if a rewrite-step/simplification was applied // to the arguments, and the result is stored in 'result'. Otherwise, they return false // and result.get == 0. br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); void mk_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { if (mk_app_core(f, num_args, args, result) == BR_FAILED) result = m().mk_app(f, num_args, args); } br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); br_status mk_distinct_core(unsigned num_args, expr * const * args, expr_ref & result); br_status mk_iff_core(expr * lhs, expr * rhs, expr_ref & result) { return mk_eq_core(lhs, rhs, result); } br_status mk_and_core(unsigned num_args, expr * const * args, expr_ref & result) { if (m_elim_and) { mk_and_as_or(num_args, args, result); return BR_DONE; } else if (m_flat) { return mk_flat_and_core(num_args, args, result); } else { return mk_nflat_and_core(num_args, args, result); } } br_status mk_or_core(unsigned num_args, expr * const * args, expr_ref & result) { return m_flat ? mk_flat_or_core(num_args, args, result) : mk_nflat_or_core(num_args, args, result); } br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result); br_status mk_not_core(expr * t, expr_ref & result); void mk_eq(expr * lhs, expr * rhs, expr_ref & result) { if (mk_eq_core(lhs, rhs, result) == BR_FAILED) result = m().mk_eq(lhs, rhs); } void mk_iff(expr * lhs, expr * rhs, expr_ref & result) { mk_eq(lhs, rhs, result); } void mk_xor(expr * lhs, expr * rhs, expr_ref & result); void mk_and(unsigned num_args, expr * const * args, expr_ref & result) { if (mk_and_core(num_args, args, result) == BR_FAILED) { SASSERT(!m_elim_and); result = m().mk_and(num_args, args); } } void mk_or(unsigned num_args, expr * const * args, expr_ref & result) { if (mk_or_core(num_args, args, result) == BR_FAILED) result = m().mk_or(num_args, args); } void mk_and(expr * arg1, expr * arg2, expr_ref & result) { expr * args[2] = {arg1, arg2}; mk_and(2, args, result); } void mk_or(expr * arg1, expr * arg2, expr_ref & result) { expr * args[2] = {arg1, arg2}; mk_or(2, args, result); } void mk_and(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { expr * args[3] = {arg1, arg2, arg3}; mk_and(3, args, result); } void mk_or(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { expr * args[3] = {arg1, arg2, arg3}; mk_or(3, args, result); } void mk_implies(expr * lhs, expr * rhs, expr_ref & result); void mk_ite(expr * c, expr * t, expr * e, expr_ref & result) { if (mk_ite_core(c, t, e, result) == BR_FAILED) result = m().mk_ite(c, t, e); } void mk_distinct(unsigned num_args, expr * const * args, expr_ref & result) { if (mk_distinct_core(num_args, args, result) == BR_FAILED) result = m().mk_distinct(num_args, args); } void mk_not(expr * t, expr_ref & result) { if (mk_not_core(t, result) == BR_FAILED) result = m().mk_not(t); } void mk_nand(unsigned num_args, expr * const * args, expr_ref & result); void mk_nor(unsigned num_args, expr * const * args, expr_ref & result); void mk_nand(expr * arg1, expr * arg2, expr_ref & result); void mk_nor(expr * arg1, expr * arg2, expr_ref & result); }; struct bool_rewriter_cfg : public default_rewriter_cfg { bool_rewriter m_r; bool flat_assoc(func_decl * f) const { return m_r.flat() && (m_r.m().is_and(f) || m_r.m().is_or(f)); } bool rewrite_patterns() const { return false; } br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { result_pr = 0; if (f->get_family_id() != m_r.get_fid()) return BR_FAILED; return m_r.mk_app_core(f, num, args, result); } bool_rewriter_cfg(ast_manager & m, params_ref const & p):m_r(m, p) {} }; class bool_rewriter_star : public rewriter_tpl { bool_rewriter_cfg m_cfg; public: bool_rewriter_star(ast_manager & m, params_ref const & p): rewriter_tpl(m, false, m_cfg), m_cfg(m, p) {} }; #endif 
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.