z3-src 500.0.0

/*++
Copyright (c) 2015 Microsoft Corporation

Module Name:

    seq_rewriter.h

Abstract:

    Basic rewriting rules for sequences constraints.

Author:

    Nikolaj Bjorner (nbjorner) 2015-12-5

Notes:

--*/
#pragma once

#include "seq_split.h"
#include "ast/seq_decl_plugin.h"
#include "ast/rewriter/seq_derive.h"
#include "ast/ast_pp.h"
#include "ast/arith_decl_plugin.h"
#include "ast/rewriter/rewriter_types.h"
#include "ast/rewriter/bool_rewriter.h"
#include "ast/rewriter/seq_subset.h"
#include "util/params.h"
#include "util/lbool.h"
#include "util/sign.h"


inline std::ostream& operator<<(std::ostream& out, expr_ref_pair_vector const& es) {
    for (auto const& p : es) {
        out << expr_ref(p.first, es.get_manager()) << "; " << expr_ref(p.second, es.get_manager()) << "\n";
    }
    return out;
}

class sym_expr {
    enum ty {
        t_char,
        t_pred,
        t_not,
        t_range
    };
    ty        m_ty;
    sort*     m_sort;
    sym_expr* m_expr;
    expr_ref  m_t;
    expr_ref  m_s;
    unsigned  m_ref;
    sym_expr(ty ty, expr_ref& t, expr_ref& s, sort* srt, sym_expr* e) : 
        m_ty(ty), m_sort(srt), m_expr(e), m_t(t), m_s(s), m_ref(0) {}
public:
    ~sym_expr() { if (m_expr) m_expr->dec_ref(); }
    expr_ref accept(expr* e);
    static sym_expr* mk_char(expr_ref& t) { return alloc(sym_expr, t_char, t, t, t->get_sort(), nullptr); }
    static sym_expr* mk_char(ast_manager& m, expr* t) { expr_ref tr(t, m); return mk_char(tr); }
    static sym_expr* mk_pred(expr_ref& t, sort* s) { return alloc(sym_expr, t_pred, t, t, s, nullptr); }
    static sym_expr* mk_range(expr_ref& lo, expr_ref& hi) { return alloc(sym_expr, t_range, lo, hi, hi->get_sort(), nullptr); }
    static sym_expr* mk_not(ast_manager& m, sym_expr* e) { expr_ref f(m); e->inc_ref(); return alloc(sym_expr, t_not, f, f, e->get_sort(), e); }
    void inc_ref() { ++m_ref;  }
    void dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); }
    std::ostream& display(std::ostream& out) const;
    bool is_char() const { return m_ty == t_char; }
    bool is_pred() const { return !is_char(); }
    bool is_range() const { return m_ty == t_range; }
    bool is_not() const { return m_ty == t_not; }
    sort* get_sort() const { return m_sort; }
    expr* get_char() const { SASSERT(is_char()); return m_t; }
    expr* get_pred() const { SASSERT(is_pred()); return m_t; }
    expr* get_lo() const { SASSERT(is_range()); return m_t; }
    expr* get_hi() const { SASSERT(is_range()); return m_s; }
    sym_expr* get_arg() const { SASSERT(is_not()); return m_expr; }
};

class sym_expr_manager {
public:
    void inc_ref(sym_expr* s) { if (s) s->inc_ref(); }
    void dec_ref(sym_expr* s) { if (s) s->dec_ref(); }
};

#if 0

class expr_solver {
public:
    virtual ~expr_solver() = default;
    virtual lbool check_sat(expr* e) = 0;
};
#endif


/**
   \brief Cheap rewrite rules for seq constraints
*/
class seq_rewriter {

    class op_cache {
        struct op_entry {
            decl_kind k;
            expr* a, *b, *c, *r;
            op_entry(decl_kind k, expr* a, expr* b, expr* c, expr* r): k(k), a(a), b(b), c(c), r(r) {}
            op_entry():k(0), a(nullptr), b(nullptr), c(nullptr), r(nullptr) {}
        };

        struct hash_entry {
            unsigned operator()(op_entry const& e) const { 
                return combine_hash(mk_mix(e.k, e.a ? e.a->get_id() : 0, e.b ? e.b->get_id() : 0), e.c ? e.c->get_id() : 0);
            }
        };

        struct eq_entry {
            bool operator()(op_entry const& a, op_entry const& b) const {
                return a.k == b.k && a.a == b.a && a.b == b.b && a.c == b.c;
            }
        };

        typedef hashtable<op_entry, hash_entry, eq_entry> op_table;

        unsigned        m_max_cache_size { 10000 };
        expr_ref_vector m_trail;
        op_table        m_table;
        void cleanup();

    public:
        op_cache(ast_manager& m);
        expr* find(decl_kind op, expr* a, expr* b, expr* c);
        void insert(decl_kind op, expr* a, expr* b, expr* c, expr* r);
    };

    friend class seq::derive;

    seq_util       m_util;
    seq_subset     m_subset;
    seq_split      m_split;
    arith_util     m_autil;
    bool_rewriter  m_br;
    seq::derive    m_derive;
    // re2automaton   m_re2aut;
    op_cache       m_op_cache;
    expr_ref_vector m_es, m_lhs, m_rhs;
    bool m_coalesce_chars = true;
    bool           m_in_bisim { false };   
    unsigned       m_re_deriv_depth { 0 };
    static const unsigned m_max_re_deriv_depth = 512;

    enum length_comparison {
        shorter_c, 
        longer_c,
        same_length_c,
        unknown_c
    };



    length_comparison compare_lengths(expr_ref_vector const& as, expr_ref_vector const& bs) {
        return compare_lengths(as.size(), as.data(), bs.size(), bs.data());
    }
    length_comparison compare_lengths(unsigned sza, expr* const* as, unsigned szb, expr* const* bs);


    bool get_head_tail(expr* e, expr_ref& head, expr_ref& tail);
    bool get_head_tail_reversed(expr* e, expr_ref& head, expr_ref& tail);
    bool get_re_head_tail(expr* e, expr_ref& head, expr_ref& tail);
    bool get_re_head_tail_reversed(expr* e, expr_ref& head, expr_ref& tail);

    expr_ref re_and(expr* cond, expr* r);
    expr_ref re_predicate(expr* cond, sort* seq_sort);

    expr_ref mk_seq_concat(expr* a, expr* b);    

    // Construct the expressions for taking the first element, the last element, the rest, and the butlast element
    expr_ref mk_seq_first(expr* s);
    expr_ref mk_seq_rest(expr* s);
    expr_ref mk_seq_last(expr* s);
    expr_ref mk_seq_butlast(expr* s);

    bool try_get_unit_values(expr* s, expr_ref_vector& result);
    //replace b in a by c into result
    void replace_all_subvectors(expr_ref_vector const& as, expr_ref_vector const& bs, expr* c, expr_ref_vector& result);

    // For replace_all(x, a, b) in R: transform R so that
    // - occurrences of b_ch are replaced by union(to_re(a_str), to_re(b_str))
    // - occurrences of a_ch are replaced by empty (replace_all never outputs a)
    expr_ref re_replace_char(expr *r, unsigned a_ch, unsigned b_ch, expr *a_str, expr *b_str);


    expr_ref merge_regex_sets(expr* r1, expr* r2, expr* unit, std::function<bool(expr*, expr*&, expr*&)>& decompose, std::function<expr* (expr*, expr*)>& compose);

    // elem is (:var 0) and path a condition that may have (:var 0) as a free variable
    // simplify path, e.g., (:var 0) = 'a' & (:var 0) = 'b' is simplified to false
    // expr_ref simplify_path(expr* elem, expr* path);

    bool lt_char(expr* ch1, expr* ch2);
    bool eq_char(expr* ch1, expr* ch2);
    bool neq_char(expr* ch1, expr* ch2);
    bool le_char(expr* ch1, expr* ch2);
    bool are_complements(expr* r1, expr* r2) const;
    bool is_subset(expr* r1, expr* r2) const;

    br_status mk_seq_unit(expr* e, expr_ref& result);
    br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
    br_status mk_seq_length(expr* a, expr_ref& result);
    expr_ref mk_len(rational const& offset, expr_ref_vector const& xs);
    bool extract_pop_suffix(expr_ref_vector const& as, expr* b, expr* c, expr_ref& result);
    bool extract_push_offset(expr_ref_vector const& as, expr* b, expr* c, expr_ref& result);
    bool extract_push_length(expr_ref_vector& as, expr* b, expr* c, expr_ref& result);
    br_status mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result);
    br_status mk_seq_contains(expr* a, expr* b, expr_ref& result);
    br_status mk_seq_at(expr* a, expr* b, expr_ref& result);
    br_status mk_seq_nth(expr* a, expr* b, expr_ref& result);
    br_status mk_seq_nth_i(expr* a, expr* b, expr_ref& result);
    br_status mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result);
    br_status mk_seq_last_index(expr* a, expr* b, expr_ref& result);
    br_status mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result);
    br_status mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref& result);
    br_status mk_seq_replace_re_all(expr* a, expr* b, expr* c, expr_ref& result);
    br_status mk_seq_replace_re(expr* a, expr* b, expr* c, expr_ref& result);
    br_status mk_seq_prefix(expr* a, expr* b, expr_ref& result);
    br_status mk_seq_suffix(expr* a, expr* b, expr_ref& result);
    br_status mk_seq_map(expr* f, expr* s, expr_ref& result);
    br_status mk_seq_mapi(expr* f, expr* i, expr* s, expr_ref& result);
    br_status mk_seq_foldl(expr* f, expr* b, expr* s, expr_ref& result);
    br_status mk_seq_foldli(expr* f, expr* i, expr* b, expr* s, expr_ref& result);
    br_status mk_str_units(func_decl* f, expr_ref& result);
    br_status mk_str_itos(expr* a, expr_ref& result);
    br_status mk_str_stoi(expr* a, expr_ref& result);
    br_status mk_str_ubv2s(expr* a, expr_ref& result);
    br_status mk_str_sbv2s(expr* a, expr_ref& result);
    br_status mk_str_in_regexp(expr* a, expr* b, expr_ref& result);
    br_status mk_str_to_regexp(expr* a, expr_ref& result);
    br_status mk_str_le(expr* a, expr* b, expr_ref& result);
    br_status mk_str_lt(expr* a, expr* b, expr_ref& result);
    br_status mk_str_from_code(expr* a, expr_ref& result);
    br_status mk_str_to_code(expr* a, expr_ref& result);
    br_status mk_str_is_digit(expr* a, expr_ref& result);
    br_status mk_re_concat(expr* a, expr* b, expr_ref& result);
    br_status mk_re_union(expr* a, expr* b, expr_ref& result);
    br_status mk_re_inter(expr* a, expr* b, expr_ref& result);
    br_status mk_re_union0(expr* a, expr* b, expr_ref& result);
    br_status mk_re_inter0(expr* a, expr* b, expr_ref& result);
    br_status mk_re_complement(expr* a, expr_ref& result);
    // Range-set collapse helpers: if the operands form a boolean
    // combination of character-class regexes, materialize the result as a
    // canonical regex over a single range_predicate.  See
    // ast/rewriter/seq_range_collapse.h for the recognized fragment.
    // NOTE: re.complement is intentionally not in this set because it
    // operates at the sequence level, not the character-class level.
    bool try_collapse_re_union(expr* a, expr* b, expr_ref& result);
    bool try_collapse_re_inter(expr* a, expr* b, expr_ref& result);
    br_status mk_re_star(expr* a, expr_ref& result);
    br_status mk_re_diff(expr* a, expr* b, expr_ref& result);
    br_status mk_re_xor(expr* a, expr* b, expr_ref& result);
    br_status mk_re_xor0(expr* a, expr* b, expr_ref& result);
    br_status mk_re_plus(expr* a, expr_ref& result);
    br_status mk_re_opt(expr* a, expr_ref& result);
    br_status mk_re_power(func_decl* f, expr* a, expr_ref& result);
    br_status mk_re_loop(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result);
    br_status mk_re_range(expr* lo, expr* hi, expr_ref& result);
    br_status mk_re_reverse(expr* r, expr_ref& result);
    br_status mk_re_derivative(expr* ele, expr* r, expr_ref& result);

    br_status lift_ites_throttled(func_decl* f, unsigned n, expr* const* args, expr_ref& result);
    bool lift_ites_filter(func_decl* f, expr* ite);

    br_status reduce_re_eq(expr* a, expr* b, expr_ref& result);
    br_status reduce_re_is_empty(expr* r, expr_ref& result);

    bool non_overlap(expr_ref_vector const& p1, expr_ref_vector const& p2) const;
    bool non_overlap(zstring const& p1, zstring const& p2) const;
    bool rewrite_contains_pattern(expr* a, expr* b, expr_ref& result);
    bool has_fixed_length_constraint(expr* a, unsigned& len);
    /* r = ite(c1,ite(c2,to_re(s),to_re(t)),to_re(u)) ==> returns true, result = ite(c1,ite(c2,s,t),u)*/
    bool lift_str_from_to_re_ite(expr * r, expr_ref & result);
    /* same as lift_to_re_from_ite and also: r = to_re(u) ==> returns true, result = u */
    bool lift_str_from_to_re(expr * r, expr_ref & result);

    br_status mk_bool_app_helper(bool is_and, unsigned n, expr* const* args, expr_ref& result);
    br_status mk_eq_helper(expr* a, expr* b, expr_ref& result);

    bool cannot_contain_prefix(expr* a, expr* b);
    bool cannot_contain_suffix(expr* a, expr* b);
    expr_ref zero() { return expr_ref(m_autil.mk_int(0), m()); }
    expr_ref one() { return expr_ref(m_autil.mk_int(1), m()); }
    expr_ref minus_one() { return expr_ref(m_autil.mk_int(-1), m()); }
    expr_ref mk_sub(expr* a, rational const& n);
    expr_ref mk_sub(expr* a, unsigned n) { return mk_sub(a, rational(n)); }

    bool is_suffix(expr* s, expr* offset, expr* len);
    bool is_prefix(expr* s, expr* offset, expr* len);
    bool sign_is_determined(expr* len, sign& s);

    bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_pair_vector& eqs);
    bool reduce_non_overlap(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs);
    bool reduce_subsequence(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs);
    bool reduce_by_length(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs);
    bool reduce_extract(expr* l, expr* r, expr_ref_vector& res);
    bool has_var(expr_ref_vector const& es);
    bool reduce_itos(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& eqs);
    bool reduce_eq_empty(expr* l, expr* r, expr_ref& result);
    bool reduce_arith_eq(expr* l, expr* r, expr_ref_vector& constraints);
    std::pair<bool, unsigned> min_length(expr_ref_vector const& es);
    std::pair<bool, unsigned> min_length(expr* e);
    std::pair<bool, unsigned> min_length(unsigned sz, expr* const* es);
    std::pair<bool, rational> max_length(expr* e);
    bool max_length(expr* e, rational& len) { auto ml = max_length(e); len = ml.second; return ml.first; }
    lbool eq_length(expr* x, expr* y);
    expr* concat_non_empty(expr_ref_vector& es);
    bool reduce_by_char(expr_ref& r, expr* ch, unsigned depth);

    bool is_string(unsigned n, expr* const* es, zstring& s) const;

    void add_next(u_map<expr*>& next, expr_ref_vector& trail, unsigned idx, expr* cond);
    bool is_sequence(expr* e, expr_ref_vector& seq);
//    bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
    bool get_lengths(expr* e, expr_ref_vector& lens, rational& pos);
    bool reduce_value_clash(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs);
    bool reduce_back(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs);
    bool reduce_front(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs);
    void remove_empty_and_concats(expr_ref_vector& es);
    void remove_leading(unsigned n, expr_ref_vector& es);

    class seq_util::rex& re() { return u().re; }
    class seq_util::rex const& re() const { return u().re; }
    class seq_util::str& str() { return u().str; }
    class seq_util::str const& str() const { return u().str; }

    void intersect(unsigned lo, unsigned hi, svector<std::pair<unsigned, unsigned>>& ranges);

    bool get_bounds(expr* e, unsigned& low, unsigned& high);
    lbool some_string_in_re(expr_mark& visited, expr* r, unsigned_vector& str);

public:
    seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
        m_util(m), m_subset(m_util.re), m_split(*this), m_autil(m), m_br(m, p), m_derive(m, *this), // m_re2aut(m),
        m_op_cache(m), m_es(m), 
        m_lhs(m), m_rhs(m) {
    }
    ast_manager & m() const { return m_util.get_manager(); }
    family_id get_fid() const { return m_util.get_family_id(); }
    seq_util const& u() const { return m_util; }
    seq_util& u() { return m_util; }

    void updt_params(params_ref const & p);
    static void get_param_descrs(param_descrs & r);


    // bool coalesce_chars() const { return m_coalesce_chars; }

    br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
    br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
    br_status mk_le_core(expr* lhs, expr* rhs, expr_ref& result);
    br_status mk_bool_app(func_decl* f, unsigned n, expr* const* args, expr_ref& result);

    expr_ref mk_app(func_decl* f, expr_ref_vector const& args) { return mk_app(f, args.size(), args.data()); }
    expr_ref mk_app(func_decl* f, unsigned n, expr* const* args) { 
        expr_ref result(m());
        if (f->get_family_id() != u().get_family_id() || 
            BR_FAILED == mk_app_core(f, n, args, result))
            result = m().mk_app(f, n, args);
        return result;
    }

    expr_ref mk_xor0(expr *a, expr *b) {
        expr_ref result(m());
        if (mk_re_xor0(a, b, result) == BR_FAILED)
            result = re().mk_xor(a, b);
        return result;
    }

    expr_ref mk_union(expr *a, expr *b) {
        expr_ref result(m());
        if (mk_re_union(a, b, result) == BR_FAILED)
            result = re().mk_union(a, b);
        return result;
    }

    expr_ref mk_inter(expr *a, expr *b) {
        expr_ref result(m());
        if (mk_re_inter(a, b, result) == BR_FAILED)
            result = re().mk_inter(a, b);
        return result;
    }

    expr_ref mk_complement(expr *a) {
        expr_ref result(m());
        if (mk_re_complement(a, result) == BR_FAILED)
            result = re().mk_complement(a);
        return result;
    }

    /*
    * makes concat and simplifies
    */
    expr_ref mk_re_append(expr* r1, expr* r2) {
        expr_ref result(m());
        if (mk_re_concat(r1, r2, result) == BR_FAILED)
            result = re().mk_concat(r1, r2);
        return result;
    }

    /*
     * Construct r1 XOR r2 applying the structural rewrites in
     * mk_re_xor (r XOR r = empty, comp/empty/full normalisation, AC
     * ordering). Used by the bisimulation procedure.
     */
    expr_ref mk_re_xor_simplified(expr* r1, expr* r2) {
        expr_ref result(m());
        if (mk_re_xor(r1, r2, result) == BR_FAILED)
            result = re().mk_xor(r1, r2);
        return result;
    }

    // Split decomposition (sigma) of a regex; see seq_split.h.  `oracle` (optional)
    // prunes non-viable splits during generation.
    bool split(expr* r, split_set& out, unsigned threshold,
        const split_mode mode = split_mode::strong, split_oracle const& oracle = {}) {
        return m_split.compute(r, out, threshold, mode, oracle);
    }

    void simplify_split(split_set& s) { m_split.simplify(s); }

    // decompose a membership constraint into a set of pairs of regex splits
    std::pair<expr_ref, expr_ref> split_membership(expr* str, expr* regex, unsigned threshold, split_set& result) const {
        return m_split.split_membership(str, regex, threshold, result);
    }

    /**
     * check if regular expression is of the form all ++ s ++ all ++ t + u ++ all, where, s, t, u are sequences
     */
    bool is_re_contains_pattern(expr* r, vector<expr_ref_vector>& patterns);
        
    bool reduce_eq(expr* l, expr* r, expr_ref_pair_vector& new_eqs, bool& change);

    bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs, bool& change);

    bool reduce_contains(expr* a, expr* b, expr_ref_vector& disj);

    expr_ref mk_length(expr* s);

    void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_pair_vector& new_eqs);

    /*
    create the nullability check for r
    */
    expr_ref is_nullable(expr* r);
    /*
    make the derivative of r wrt the given element ele
    */
    expr_ref mk_derivative(expr* ele, expr* r);
    /*
    make the derivative of r wrt the canonical variable v0 = (:var 0), 
    for example mk_derivative(a+) = (if (v0 = 'a') then a* else [])
    */
    expr_ref mk_derivative(expr* r);

    /*
    Classical (non-antimirov) Brzozowski derivative wrt the canonical
    variable v0 = (:var 0). Unlike `mk_derivative` this entry point keeps
    the symbolic derivative as a single transition regex (TRegex): boolean
    operators are pushed into the ITE leaves rather than lifted to the top
    as a union. Used by the regex_bisim equivalence
    procedure which relies on each leaf of D(p XOR q) being a coherent
    XOR pair (D_v p) XOR (D_v q).
    */
    expr_ref mk_brz_derivative(expr *r) {
        return mk_derivative(r);
    }

    /*
    Enumerate the cofactors (min-terms) of a transition regex r taken with
    respect to ele. Produces (path_condition, leaf_regex) pairs for every
    feasible path through the ITE-tree, pruning infeasible character ranges.
    Delegates to the derivative engine so the same path/interval context used
    while hoisting ITEs is reused for the leaf simplification.
    */
    void get_cofactors(expr* ele, expr* r, expr_ref_pair_vector& result) {
        m_derive.get_cofactors(ele, r, result);
    }

    /*
    Compute the symbolic derivative of r and enumerate its reachable leaves
    in fully ITE-hoisted normal form: a list of (path_condition, target)
    pairs where every target is free of (:var 0) (so nullability is always
    decidable) and unions are kept intact as single states. Used by
    regex_bisim, which consumes the targets and ignores the path conditions.
    */
    void brz_derivative_cofactors(expr* r, expr_ref_pair_vector& result) {
        m_derive.derivative_cofactors(r, result);
    }

    // heuristic elimination of element from condition that comes form a derivative.
    // special case optimization for conjunctions of equalities, disequalities and ranges.
    void elim_condition(expr* elem, expr_ref& cond);

    /* Apply simplifications to the union to keep the union normalized (r1 and r2 are not normalized)*/
    expr_ref mk_regex_union_normalize(expr* r1, expr* r2);
    /* Apply simplifications to the intersection to keep it normalized (r1 and r2 are not normalized)*/
    expr_ref mk_regex_inter_normalize(expr* r1, expr* r2);

    expr_ref mk_regex_concat(expr *r1, expr *r2);

    /*
    * Extract some string that is a member of r. 
    * Return true if a valid string was extracted.
    * Return false when giving up or the regular expression is empty.
    */
    lbool some_string_in_re(expr* r, zstring& s);
};