z3-src 500.0.0

/*++
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/expr_safe_replace.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;
    bool           m_flat_and_or = false;
    bool           m_sort_disjunctions = true;
    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;
    ptr_vector<expr> m_todo1, m_todo2;
    unsigned_vector m_counts1, m_counts2;
    expr_mark       m_marked;
    expr_safe_replace m_rep1, m_rep2;

    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);

    bool try_ite_eq(expr* lhs, expr* rhs, expr_ref& r);

    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);

    expr_ref simplify_eq_ite(expr* value, expr* ite);

public:
    bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0), m_rep1(m), m_rep2(m) { 
        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_plain(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_plain(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(std::span<expr* const>(args, num_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);

    // If r is, or contains, an if-then-else, decompose it into a top-level
    // ite by hoisting the (first) inner ite condition: returns c, th, el such
    // that r is equivalent to (ite c th el). Returns false if r has no ite.
    bool decompose_ite(expr *r, expr_ref &c, expr_ref &th, expr_ref &el);
};

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) {}
};