mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

remove unused field

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-09 07:09:23 -08:00
parent aebdc8950a
commit b1a1aa5007
2 changed files with 3 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/seq_decl_plugin.cpp
View file

@ -437,10 +437,6 @@ app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort
} }
app* seq_util::str::mk_string(symbol const& s) {
return u.seq.mk_string(s);
}
void seq_util::str::get_concat(expr* e, ptr_vector<expr>& es) const { void seq_util::str::get_concat(expr* e, ptr_vector<expr>& es) const {
expr* e1, *e2; expr* e1, *e2;
while (is_concat(e, e1, e2)) { while (is_concat(e, e1, e2)) {

7
src/ast/seq_decl_plugin.h
View file

@ -167,11 +167,11 @@ public:
ast_manager& m; ast_manager& m;
family_id m_fid; family_id m_fid;
public: public:
str(seq_util& u):u(u), m(u.m), m_fid(u.m_fid) {} str(seq_util& u): u(u), m(u.m), m_fid(u.m_fid) {}
sort* mk_seq(sort* s) { parameter param(s); return m.mk_sort(m_fid, SEQ_SORT, 1, &param); } sort* mk_seq(sort* s) { parameter param(s); return m.mk_sort(m_fid, SEQ_SORT, 1, &param); }
app* mk_empty(sort* s) { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, 0, 0, (expr*const*)0, s)); } app* mk_empty(sort* s) { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, 0, 0, (expr*const*)0, s)); }
app* mk_string(symbol const& s); app* mk_string(symbol const& s) { return u.seq.mk_string(s); }
app* mk_string(char const* s) { return mk_string(symbol(s)); } app* mk_string(char const* s) { return mk_string(symbol(s)); }
app* mk_string(std::string const& s) { return mk_string(symbol(s.c_str())); } app* mk_string(std::string const& s) { return mk_string(symbol(s.c_str())); }
app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); } app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); }
@ -229,11 +229,10 @@ public:
}; };
class re { class re {
seq_util& u;
ast_manager& m; ast_manager& m;
family_id m_fid; family_id m_fid;
public: public:
re(seq_util& u):u(u), m(u.m), m_fid(u.m_fid) {} re(seq_util& u): m(u.m), m_fid(u.m_fid) {}
bool is_to_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); } bool is_to_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); }
bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_RE_CONCAT); } bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_RE_CONCAT); }