1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3 
4 Module Name:
5 
6     seq_skolem.h
7 
8 Abstract:
9 
10     Skolem function support for sequences.
11     Skolem functions are auxiliary funcions useful for axiomatizing sequence
12     operations.
13 
14 Author:
15 
16     Nikolaj Bjorner (nbjorner) 2020-4-16
17 
18 --*/
19 #pragma once
20 
21 #include "ast/seq_decl_plugin.h"
22 #include "ast/arith_decl_plugin.h"
23 #include "ast/rewriter/th_rewriter.h"
24 
25 namespace seq {
26 
27     class skolem {
28         ast_manager&   m;
29         th_rewriter&   m_rewrite; // NB: would be nicer not to have this dependency
30         seq_util       seq;
31         arith_util     a;
32 
33         symbol         m_prefix, m_suffix;
34         symbol         m_tail;
35         symbol         m_seq_first, m_seq_last;
36         symbol         m_indexof_left, m_indexof_right;   // inverse of indexof: (indexof_left s t) + s + (indexof_right s t) = t, for s in t.
37         symbol         m_aut_step;                        // regex unfolding state
38         symbol         m_accept;                          // regex
39         symbol         m_is_empty, m_is_non_empty;        // regex emptiness check
40         symbol         m_pre, m_post;                     // inverse of at: (pre s i) + (at s i) + (post s i) = s if 0 <= i < (len s)
41         symbol         m_eq;                              // equality atom
42         symbol         m_max_unfolding, m_length_limit;
43 
44     public:
45 
46         skolem(ast_manager& m, th_rewriter& r);
47 
mk(symbol const & s,sort * range)48         expr_ref mk(symbol const& s, sort* range) { return mk(s, nullptr, nullptr, nullptr, nullptr, range); }
mk(symbol const & s,expr * e,sort * range)49         expr_ref mk(symbol const& s, expr* e, sort* range) { return mk(s, e, nullptr, nullptr, nullptr, range); }
mk(symbol const & s,expr * e1,expr * e2,sort * range)50         expr_ref mk(symbol const& s, expr* e1, expr* e2, sort* range) { return mk(s, e1, e2, nullptr, nullptr, range); }
51         expr_ref mk(symbol const& s, expr* e1, expr* e2, expr* e3, sort* range, bool rw = true) { return mk(s, e1, e2, e3, nullptr, range, rw); }
52         expr_ref mk(symbol const& s, expr* e1, expr* e2 = nullptr, expr* e3 = nullptr, expr* e4 = nullptr, sort* range = nullptr, bool rw = true);
53 
mk(char const * s,sort * range)54         expr_ref mk(char const* s, sort* range) { return mk(s, nullptr, nullptr, nullptr, nullptr, range); }
mk(char const * s,expr * e,sort * range)55         expr_ref mk(char const* s, expr* e, sort* range) { return mk(s, e, nullptr, nullptr, nullptr, range); }
mk(char const * s,expr * e1,expr * e2,sort * range)56         expr_ref mk(char const* s, expr* e1, expr* e2, sort* range) { return mk(s, e1, e2, nullptr, nullptr, range); }
mk(char const * s,expr * e1,expr * e2,expr * e3,sort * range)57         expr_ref mk(char const* s, expr* e1, expr* e2, expr* e3, sort* range) { return mk(s, e1, e2, e3, nullptr, range); }
58         expr_ref mk(char const* s , expr* e1, expr* e2 = nullptr, expr* e3 = nullptr, expr* e4 = nullptr, sort* range = nullptr) {
59             return mk(symbol(s), e1, e2, e3, e4, range);
60         }
61 
mk_align(expr * e1,expr * e2,expr * e3,expr * e4)62         expr_ref mk_align(expr* e1, expr* e2, expr* e3, expr* e4) { return mk("seq.align", e1, e2, e3, e4); }
mk_align_l(expr * e1,expr * e2,expr * e3,expr * e4)63         expr_ref mk_align_l(expr* e1, expr* e2, expr* e3, expr* e4) { return mk("seq.align.l", e1, e2, e3, e4); }
mk_align_r(expr * e1,expr * e2,expr * e3,expr * e4)64         expr_ref mk_align_r(expr* e1, expr* e2, expr* e3, expr* e4) { return mk("seq.align.r", e1, e2, e3, e4); }
mk_align_m(expr * e1,expr * e2,expr * e3,expr * e4)65         expr_ref mk_align_m(expr* e1, expr* e2, expr* e3, expr* e4) {
66             expr* x1 = nullptr, *x2 = nullptr, *y1 = nullptr, *y2 = nullptr;
67             if (is_align(e1, x1, x2) && is_align(e2, y1, y2)) {
68                 if (x2 == y2 && x1 != y1)
69                     return mk_align_m(x1, y1, e3, e4);
70             }
71             return mk("seq.align.m", e1, e2, e3, e4);
72         }
mk_accept(expr_ref_vector const & args)73         expr_ref mk_accept(expr_ref_vector const& args) { return expr_ref(seq.mk_skolem(m_accept, args.size(), args.data(), m.mk_bool_sort()), m); }
mk_accept(expr * s,expr * i,expr * r)74         expr_ref mk_accept(expr* s, expr* i, expr* r) { return mk(m_accept, s, i, r, nullptr, m.mk_bool_sort()); }
mk_is_non_empty(expr * r,expr * u,expr * n)75         expr_ref mk_is_non_empty(expr* r, expr* u, expr* n) { return mk(m_is_non_empty, r, u, n, m.mk_bool_sort(), false); }
mk_is_empty(expr * r,expr * u,expr * n)76         expr_ref mk_is_empty(expr* r, expr* u, expr* n) { return mk(m_is_empty, r, u, n, m.mk_bool_sort(), false); }
77 
78         expr_ref mk_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk(m_indexof_left, t, s, offset); }
79         expr_ref mk_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk(m_indexof_right, t, s, offset); }
80         expr_ref mk_contains_left(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.cnt.l", t, s, offset); }
81         expr_ref mk_contains_right(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.cnt.r", t, s, offset); }
82         expr_ref mk_last_indexof_left(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.lidx.l", t, s, offset); }
83         expr_ref mk_last_indexof_right(expr* t, expr* s, expr* offset = nullptr) { return mk("seq.lidx.r", t, s, offset); }
84 
mk_tail(expr * s,expr * i)85         expr_ref mk_tail(expr* s, expr* i) { return mk(m_tail, s, i); }
mk_post(expr * s,expr * i)86         expr_ref mk_post(expr* s, expr* i) { return mk(m_post, s, i); }
mk_ite(expr * c,expr * t,expr * e)87         expr_ref mk_ite(expr* c, expr* t, expr* e) { return mk(symbol("seq.if"), c, t, e, nullptr, t->get_sort()); }
88         expr_ref mk_last(expr* s);
89         expr_ref mk_first(expr* s);
mk_pre(expr * s,expr * i)90         expr_ref mk_pre(expr* s, expr* i) { return mk(m_pre, s, i); }
mk_eq(expr * a,expr * b)91         expr_ref mk_eq(expr* a, expr* b) { return mk(m_eq, a, b, nullptr, nullptr, m.mk_bool_sort()); }
mk_prefix_inv(expr * s,expr * t)92         expr_ref mk_prefix_inv(expr* s, expr* t) { return mk(m_prefix, s, t); }
mk_suffix_inv(expr * s,expr * t)93         expr_ref mk_suffix_inv(expr* s, expr* t) { return mk(m_suffix, s, t); }
94         expr_ref mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned j, expr* t);
mk_is_digit(expr * ch)95         expr_ref mk_is_digit(expr* ch) { return mk(symbol("seq.is_digit"), ch, nullptr, nullptr, nullptr, m.mk_bool_sort()); }
96         expr_ref mk_unit_inv(expr* n);
mk_digit2int(expr * ch)97         expr_ref mk_digit2int(expr* ch) { return mk(symbol("seq.digit2int"), ch, nullptr, nullptr, nullptr, a.mk_int()); }
98         expr_ref mk_digit2bv(expr* ch, sort* bv_sort);
mk_ubv2ch(expr * b)99         expr_ref mk_ubv2ch(expr* b) { return mk(symbol("seq.ubv2ch"), b, nullptr, nullptr, nullptr, seq.mk_char_sort()); }
100         expr_ref mk_left(expr* x, expr* y, expr* z = nullptr) { return mk("seq.left", x, y, z); }
101         expr_ref mk_right(expr* x, expr* y, expr* z = nullptr) { return mk("seq.right", x, y, z); }
102         expr_ref mk_max_unfolding_depth(unsigned d);
103         expr_ref mk_length_limit(expr* e, unsigned d);
104 
105 
106         bool is_skolem(symbol const& s, expr const* e) const;
is_skolem(expr const * e)107         bool is_skolem(expr const* e) const { return seq.is_skolem(e); }
108 
is_first(expr * e,expr * & u)109         bool is_first(expr* e, expr*& u) { return is_skolem(m_seq_first, e) && (u = to_app(e)->get_arg(0), true); }
is_last(expr * e,expr * & u)110         bool is_last(expr* e, expr*& u) { return is_skolem(m_seq_last, e) && (u = to_app(e)->get_arg(0), true); }
is_unit_inv(expr * e)111         bool is_unit_inv(expr* e) const { return is_skolem(symbol("seq.unit-inv"), e); }
is_unit_inv(expr * e,expr * & u)112         bool is_unit_inv(expr* e, expr*& u) const { return is_unit_inv(e) && (u = to_app(e)->get_arg(0), true); }
is_tail(expr * e)113         bool is_tail(expr* e) const { return is_skolem(m_tail, e); }
is_seq_first(expr * e)114         bool is_seq_first(expr* e) const { return is_skolem(m_seq_first, e); }
is_indexof_left(expr * e)115         bool is_indexof_left(expr* e) const { return is_skolem(m_indexof_left, e); }
is_indexof_right(expr * e)116         bool is_indexof_right(expr* e) const { return is_skolem(m_indexof_right, e); }
is_indexof_left(expr * e,expr * & x,expr * & y)117         bool is_indexof_left(expr* e, expr*& x, expr*& y) const {
118             return is_indexof_left(e) && (x = to_app(e)->get_arg(0), y = to_app(e)->get_arg(1), true);
119         }
is_indexof_right(expr * e,expr * & x,expr * & y)120         bool is_indexof_right(expr* e, expr*& x, expr*& y) const {
121             return is_indexof_right(e) && (x = to_app(e)->get_arg(0), y = to_app(e)->get_arg(1), true);
122         }
123 
is_step(expr * e)124         bool is_step(expr* e) const { return is_skolem(m_aut_step, e); }
125         bool is_step(expr* e, expr*& s, expr*& idx, expr*& re, expr*& i, expr*& j, expr*& t) const;
is_accept(expr * acc)126         bool is_accept(expr* acc) const {  return is_skolem(m_accept, acc); }
is_accept(expr * a,expr * & s,expr * & i,expr * & r,expr * & n)127         bool is_accept(expr* a, expr*& s, expr*& i, expr*& r, expr*& n) const {
128             return is_accept(a) && to_app(a)->get_num_args() == 4 &&
129                 (s = to_app(a)->get_arg(0), i = to_app(a)->get_arg(1),
130                  r = to_app(a)->get_arg(2), n = to_app(a)->get_arg(3),
131                  true);
132         }
is_accept(expr * e,expr * & s,expr * & i,unsigned & idx,expr * & r)133         bool is_accept(expr* e, expr*& s, expr*& i, unsigned& idx, expr*& r) const {
134             return is_accept(e) && to_app(e)->get_num_args() == 3 &&
135                 (s = to_app(e)->get_arg(0), i = to_app(e)->get_arg(1),
136                  r = to_app(e)->get_arg(2), true) &&
137                 a.is_unsigned(i, idx);
138         }
is_align(expr const * e)139         bool is_align(expr const* e) const { return is_skolem(symbol("seq.align.m"), e); }
is_align_l(expr const * e)140         bool is_align_l(expr const* e) const { return is_skolem(symbol("seq.align.l"), e); }
is_align_r(expr const * e)141         bool is_align_r(expr const* e) const { return is_skolem(symbol("seq.align.r"), e); }
142         MATCH_BINARY(is_align);
143         bool is_post(expr* e, expr*& s, expr*& start);
144         bool is_pre(expr* e, expr*& s, expr*& i);
145         bool is_eq(expr* e, expr*& a, expr*& b) const;
146         bool is_tail(expr* e, expr*& s, expr*& idx) const;
147         bool is_tail_u(expr* e, expr*& s, unsigned& idx) const;
148         bool is_tail(expr* e, expr*& s) const;
is_digit(expr * e)149         bool is_digit(expr* e) const { return is_skolem(symbol("seq.is_digit"), e); }
is_max_unfolding(expr * e)150         bool is_max_unfolding(expr* e) const { return is_skolem(m_max_unfolding, e); }
is_length_limit(expr * e)151         bool is_length_limit(expr* e) const { return is_skolem(m_length_limit, e); }
152         bool is_length_limit(expr* p, unsigned& lim, expr*& s) const;
is_is_empty(expr * e)153         bool is_is_empty(expr* e) const { return is_skolem(m_is_empty, e); }
is_is_non_empty(expr * e)154         bool is_is_non_empty(expr* e) const { return is_skolem(m_is_non_empty, e); }
is_is_empty(expr * e,expr * & r,expr * & u,expr * & n)155         bool is_is_empty(expr* e, expr*& r, expr*& u, expr*& n) const {
156             return is_skolem(m_is_empty, e) && (r = to_app(e)->get_arg(0), u = to_app(e)->get_arg(1), n = to_app(e)->get_arg(2), true);
157         }
is_is_non_empty(expr * e,expr * & r,expr * & u,expr * & n)158         bool is_is_non_empty(expr* e, expr*& r, expr*& u, expr*& n) const {
159             return is_skolem(m_is_non_empty, e) && (r = to_app(e)->get_arg(0), u = to_app(e)->get_arg(1), n = to_app(e)->get_arg(2), true);
160         }
161 
162         void decompose(expr* e, expr_ref& head, expr_ref& tail);
163 
164     };
165 
166 };
167 
168