mirror of
https://github.com/Z3Prover/z3
synced 2025-08-19 01:32:17 +00:00
259 lines
9.5 KiB
C++
259 lines
9.5 KiB
C++
/*++
|
|
Copyright (c) 2011 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
bool_rewriter.h
|
|
|
|
Abstract:
|
|
|
|
Basic rewriting rules for Boolean operators.
|
|
|
|
Author:
|
|
|
|
Leonardo (leonardo) 2011-04-04
|
|
|
|
Notes:
|
|
|
|
--*/
|
|
#pragma once
|
|
|
|
#include "ast/ast.h"
|
|
#include "ast/rewriter/rewriter.h"
|
|
#include "ast/rewriter/hoist_rewriter.h"
|
|
#include "util/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;
|
|
hoist_rewriter m_hoist;
|
|
bool m_flat_and_or = false;
|
|
bool m_local_ctx = false;
|
|
bool m_elim_and = false;
|
|
bool m_blast_distinct = false;
|
|
bool m_order_eq = false;
|
|
unsigned m_blast_distinct_threshold;
|
|
bool m_ite_extra_rules;
|
|
unsigned m_local_ctx_limit;
|
|
unsigned m_local_ctx_cost;
|
|
bool m_elim_ite;
|
|
|
|
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);
|
|
|
|
void push_new_arg(expr* arg, expr_ref_vector& new_args, expr_fast_mark1& neg_lits, expr_fast_mark2& pos_lits);
|
|
|
|
public:
|
|
bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_hoist(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); }
|
|
|
|
bool flat_and_or() const { return m_flat_and_or; }
|
|
void set_flat_and_or(bool f) { m_flat_and_or = 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 set_order_eq(bool f) { m_order_eq = f; }
|
|
|
|
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_and_or) {
|
|
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_and_or ?
|
|
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);
|
|
|
|
app* mk_eq(expr* lhs, expr* rhs);
|
|
|
|
void mk_eq(expr * lhs, expr * rhs, expr_ref & result) {
|
|
if (mk_eq_core(lhs, rhs, result) == BR_FAILED)
|
|
result = mk_eq(lhs, rhs);
|
|
}
|
|
expr_ref mk_eq_rw(expr* lhs, expr* rhs) {
|
|
expr_ref r(m()), _lhs(lhs, m()), _rhs(rhs, m());
|
|
mk_eq(lhs, rhs, r);
|
|
return r;
|
|
}
|
|
expr_ref mk_xor(expr* a, expr* b) {
|
|
expr_ref result(m());
|
|
mk_xor(a, b, result);
|
|
return result;
|
|
}
|
|
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);
|
|
}
|
|
expr_ref mk_or(unsigned num_args, expr * const * args) {
|
|
expr_ref result(m());
|
|
mk_or(num_args, args, result);
|
|
return result;
|
|
}
|
|
expr_ref mk_and(unsigned num_args, expr * const * args) {
|
|
expr_ref result(m());
|
|
mk_and(num_args, args, result);
|
|
return result;
|
|
}
|
|
expr_ref mk_or(expr_ref_vector const& args) {
|
|
expr_ref result(m());
|
|
mk_or(args.size(), args.data(), result);
|
|
return result;
|
|
}
|
|
expr_ref mk_and(expr_ref_vector const& args) {
|
|
expr_ref result(m());
|
|
mk_and(args.size(), args.data(), result);
|
|
return result;
|
|
}
|
|
expr_ref mk_and(expr* a, expr* b) {
|
|
expr_ref result(m());
|
|
mk_and(a, b, result);
|
|
return result;
|
|
}
|
|
expr_ref mk_or(expr* a, expr* b) {
|
|
expr_ref result(m());
|
|
mk_or(a, b, result);
|
|
return result;
|
|
}
|
|
|
|
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);
|
|
}
|
|
expr_ref mk_ite(expr * c, expr * t, expr * e) {
|
|
expr_ref r(m());
|
|
mk_ite(c, t, e, r);
|
|
return r;
|
|
}
|
|
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);
|
|
}
|
|
expr_ref mk_not(expr* t) {
|
|
expr_ref r(m());
|
|
mk_not(t, r);
|
|
return r;
|
|
}
|
|
|
|
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);
|
|
void mk_ge2(expr* a, expr* b, expr* c, 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_and_or() && (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 = nullptr;
|
|
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> {
|
|
bool_rewriter_cfg m_cfg;
|
|
public:
|
|
bool_rewriter_star(ast_manager & m, params_ref const & p):
|
|
rewriter_tpl<bool_rewriter_cfg>(m, false, m_cfg),
|
|
m_cfg(m, p) {}
|
|
};
|
|
|