From a8e366aa246c2262523eacf09f89f14f7367f270 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 4 Dec 2015 15:24:29 -0800 Subject: [PATCH] add basic string factory Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 4 +- src/ast/seq_decl_plugin.h | 89 ++++++++++++++++++++++++++++++++- src/parsers/smt2/smt2parser.cpp | 2 +- src/smt/theory_seq_empty.h | 60 ++++++++++++++++++++++ 4 files changed, 150 insertions(+), 5 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 612ffc9db..65df99c5a 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -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); } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 3d1faba42..0cdfbd5a8 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -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(m.get_plugin(m.mk_family_id("seq")))) { + seq(*static_cast(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_ */ diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 62751c025..2f16f01d7 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -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(); } diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index 60350017f..b99336b29 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -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_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())); + } + }; };