mirror of
https://github.com/Z3Prover/z3
synced 2025-11-04 13:29:11 +00:00
add basic string factory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
75c935a4cb
commit
a8e366aa24
4 changed files with 150 additions and 5 deletions
|
|
@ -352,6 +352,6 @@ bool seq_decl_plugin::is_value(app* e) const {
|
|||
return false;
|
||||
}
|
||||
|
||||
app* seq_util::mk_string(symbol const& s) {
|
||||
return seq.mk_string(s);
|
||||
app* seq_util::str::mk_string(symbol const& s) {
|
||||
return u.seq.mk_string(s);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -156,14 +156,99 @@ public:
|
|||
class seq_util {
|
||||
ast_manager& m;
|
||||
seq_decl_plugin& seq;
|
||||
family_id m_fid;
|
||||
public:
|
||||
|
||||
class str {
|
||||
seq_util& u;
|
||||
ast_manager& m;
|
||||
family_id m_fid;
|
||||
public:
|
||||
str(seq_util& u):u(u), m(u.m), m_fid(u.m_fid) {}
|
||||
|
||||
app* mk_string(symbol const& s);
|
||||
app* mk_string(char const* s) { return mk_string(symbol(s)); }
|
||||
app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_CONCAT, 2, es); }
|
||||
app* mk_length(expr* a) { return m.mk_app(m_fid, OP_STRING_LENGTH, 1, &a); }
|
||||
app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_STRING_SUBSTR, 3, es); }
|
||||
app* mk_strctn(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_STRCTN, 2, es); }
|
||||
|
||||
bool is_const(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
|
||||
|
||||
bool is_const(expr const* n, std::string& s) const {
|
||||
return is_const(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol().str(), true);
|
||||
}
|
||||
|
||||
bool is_string(sort* s) const { return is_sort_of(s, m_fid, STRING_SORT); }
|
||||
bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_CONCAT); }
|
||||
bool is_length(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_LENGTH); }
|
||||
bool is_substr(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_SUBSTR); }
|
||||
bool is_strctn(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STRCTN); }
|
||||
bool is_charat(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_CHARAT); }
|
||||
bool is_stridof(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STRIDOF); }
|
||||
bool is_repl(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STRREPL); }
|
||||
bool is_prefix(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_PREFIX); }
|
||||
bool is_suffix(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_SUFFIX); }
|
||||
bool is_itos(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_ITOS); }
|
||||
bool is_stoi(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STOI); }
|
||||
bool is_in_regexp(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_IN_REGEXP); }
|
||||
|
||||
|
||||
MATCH_BINARY(is_concat);
|
||||
MATCH_UNARY(is_length);
|
||||
MATCH_TERNARY(is_substr);
|
||||
MATCH_BINARY(is_strctn);
|
||||
MATCH_BINARY(is_charat);
|
||||
MATCH_BINARY(is_stridof);
|
||||
MATCH_BINARY(is_repl);
|
||||
MATCH_BINARY(is_prefix);
|
||||
MATCH_BINARY(is_suffix);
|
||||
MATCH_UNARY(is_itos);
|
||||
MATCH_UNARY(is_stoi);
|
||||
MATCH_BINARY(is_in_regexp);
|
||||
};
|
||||
|
||||
class re {
|
||||
seq_util& u;
|
||||
ast_manager& m;
|
||||
family_id m_fid;
|
||||
public:
|
||||
re(seq_util& u):u(u), m(u.m), m_fid(u.m_fid) {}
|
||||
|
||||
bool is_to_regexp(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_TO_REGEXP); }
|
||||
bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_CONCAT); }
|
||||
bool is_union(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_UNION); }
|
||||
bool is_inter(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_INTER); }
|
||||
bool is_star(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_STAR); }
|
||||
bool is_plus(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_PLUS); }
|
||||
bool is_opt(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_OPT); }
|
||||
bool is_range(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_RANGE); }
|
||||
bool is_loop(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_LOOP); }
|
||||
|
||||
MATCH_UNARY(is_to_regexp);
|
||||
MATCH_BINARY(is_concat);
|
||||
MATCH_BINARY(is_union);
|
||||
MATCH_BINARY(is_inter);
|
||||
MATCH_UNARY(is_star);
|
||||
MATCH_UNARY(is_plus);
|
||||
MATCH_UNARY(is_opt);
|
||||
|
||||
};
|
||||
str str;
|
||||
re re;
|
||||
|
||||
seq_util(ast_manager& m):
|
||||
m(m),
|
||||
seq(*static_cast<seq_decl_plugin*>(m.get_plugin(m.mk_family_id("seq")))) {
|
||||
seq(*static_cast<seq_decl_plugin*>(m.get_plugin(m.mk_family_id("seq")))),
|
||||
m_fid(seq.get_family_id()),
|
||||
str(*this),
|
||||
re(*this) {
|
||||
}
|
||||
|
||||
~seq_util() {}
|
||||
|
||||
app* mk_string(symbol const& s);
|
||||
family_id get_family_id() const { return m_fid; }
|
||||
|
||||
};
|
||||
|
||||
#endif /* SEQ_DECL_PLUGIN_H_ */
|
||||
|
|
|
|||
|
|
@ -1069,7 +1069,7 @@ namespace smt2 {
|
|||
|
||||
void parse_string_const() {
|
||||
SASSERT(curr() == scanner::STRING_TOKEN);
|
||||
expr_stack().push_back(sutil().mk_string(curr_id()));
|
||||
expr_stack().push_back(sutil().str.mk_string(curr_id()));
|
||||
TRACE("smt2parser", tout << "new string: " << mk_pp(expr_stack().back(), m()) << "\n";);
|
||||
next();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -20,8 +20,64 @@ Revision History:
|
|||
#define THEORY_SEQ_EMPTY_H_
|
||||
|
||||
#include "smt_theory.h"
|
||||
#include "seq_decl_plugin.h"
|
||||
|
||||
namespace smt {
|
||||
class seq_factory : public value_factory {
|
||||
typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
|
||||
proto_model& m_model;
|
||||
seq_util u;
|
||||
symbol_set m_strings;
|
||||
unsigned m_next;
|
||||
public:
|
||||
seq_factory(ast_manager & m, family_id fid, proto_model & md):
|
||||
value_factory(m, fid),
|
||||
m_model(md),
|
||||
u(m),
|
||||
m_next(0)
|
||||
{
|
||||
m_strings.insert(symbol(""));
|
||||
m_strings.insert(symbol("a"));
|
||||
m_strings.insert(symbol("b"));
|
||||
}
|
||||
|
||||
virtual expr* get_some_value(sort* s) {
|
||||
if (u.str.is_string(s))
|
||||
return u.str.mk_string(symbol(""));
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
}
|
||||
virtual bool get_some_values(sort* s, expr_ref& v1, expr_ref& v2) {
|
||||
if (u.str.is_string(s)) {
|
||||
v1 = u.str.mk_string("a");
|
||||
v2 = u.str.mk_string("b");
|
||||
return true;
|
||||
}
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return false;
|
||||
}
|
||||
virtual expr* get_fresh_value(sort* s) {
|
||||
if (u.str.is_string(s)) {
|
||||
while (true) {
|
||||
std::ostringstream strm;
|
||||
strm << "S" << m_next++;
|
||||
symbol sym(strm.str().c_str());
|
||||
if (m_strings.contains(sym)) continue;
|
||||
m_strings.insert(sym);
|
||||
return u.str.mk_string(sym);
|
||||
}
|
||||
}
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
}
|
||||
virtual void register_value(expr* n) {
|
||||
std::string sym;
|
||||
if (u.str.is_const(n, sym)) {
|
||||
m_strings.insert(symbol(sym.c_str()));
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
class theory_seq_empty : public theory {
|
||||
bool m_used;
|
||||
virtual final_check_status final_check_eh() { return m_used?FC_GIVEUP:FC_DONE; }
|
||||
|
|
@ -33,6 +89,10 @@ namespace smt {
|
|||
virtual char const * get_name() const { return "seq-empty"; }
|
||||
public:
|
||||
theory_seq_empty(ast_manager& m):theory(m.mk_family_id("seq")), m_used(false) {}
|
||||
virtual void init_model(model_generator & mg) {
|
||||
mg.register_factory(alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()));
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue