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