mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

refactoring theory_str

Browse source
This commit is contained in:
Murphy Berzish 2017-02-27 13:22:56 -05:00
parent 7e3e434147
commit 725352234d
17 changed files with 87 additions and 390 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/api/api_ast.cpp
View file

@ -647,12 +647,6 @@ extern "C" {
else if (fid == mk_c(c)->get_seq_fid() && k == RE_SORT) {
return Z3_RE_SORT;
}
else if (fid == mk_c(c)->get_str_fid() && k == STRING_SORT) {
return Z3_STRING_SORT;
}
else if (fid == mk_c(c)->get_str_fid() && k == REGEX_SORT) {
return Z3_REGEX_SORT;
}
else {
return Z3_UNKNOWN_SORT;
}
@ -1147,16 +1141,6 @@ extern "C" {
}
}
if (mk_c(c)->get_str_fid() == _d->get_family_id()) {
switch (_d->get_decl_kind()) {
// TODO(z3str2) add others
case OP_STRCAT: return Z3_OP_STR_CONCAT;
case OP_STRLEN: return Z3_OP_STR_LENGTH;
default:
return Z3_OP_UNINTERPRETED;
}
}
if (mk_c(c)->get_fpa_fid() == _d->get_family_id()) {
switch (_d->get_decl_kind()) {
case OP_FPA_RM_NEAREST_TIES_TO_EVEN: return Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN;

2
src/api/api_context.cpp
View file

@ -81,7 +81,6 @@ namespace api {
m_fpa_util(m()),
m_dtutil(m()),
m_sutil(m()),
m_strutil(m()),
m_last_result(m()),
m_ast_trail(m()),
m_pmanager(m_limit) {
@ -105,7 +104,6 @@ namespace api {
m_datalog_fid = m().mk_family_id("datalog_relation");
m_fpa_fid = m().mk_family_id("fpa");
m_seq_fid = m().mk_family_id("seq");
m_str_fid = m().mk_family_id("str");
m_dt_plugin = static_cast<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
install_tactics(*this);

4
src/api/api_context.h
View file

@ -26,7 +26,6 @@ Revision History:
#include"arith_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"seq_decl_plugin.h"
#include"str_decl_plugin.h"
#include"datatype_decl_plugin.h"
#include"dl_decl_plugin.h"
#include"fpa_decl_plugin.h"
@ -63,8 +62,6 @@ namespace api {
datatype_util m_dtutil;
seq_util m_sutil;
str_util m_strutil;
// Support for old solver API
smt_params m_fparams;
// -------------------------------
@ -130,7 +127,6 @@ namespace api {
fpa_util & fpautil() { return m_fpa_util; }
datatype_util& dtutil() { return m_dtutil; }
seq_util& sutil() { return m_sutil; }
str_util& strutil() { return m_strutil; }
family_id get_basic_fid() const { return m_basic_fid; }
family_id get_array_fid() const { return m_array_fid; }
family_id get_arith_fid() const { return m_arith_fid; }

160
src/api/api_str.cpp
View file

@ -1,160 +0,0 @@
/*++
Copyright (c) 2016 Microsoft Corporation
Module Name:
api_str.cpp
Abstract:
API for strings and regular expressions (Z3str2 implementation).
Author:
Murphy Berzish (mtrberzi) 2016-10-03.
Revision History:
--*/
#include<iostream>
#include"z3.h"
#include"api_log_macros.h"
#include"api_context.h"
#include"api_util.h"
#include"ast_pp.h"
extern "C" {
Z3_sort Z3_API Z3_mk_str_sort(Z3_context c) {
Z3_TRY;
LOG_Z3_mk_str_sort(c);
RESET_ERROR_CODE();
sort * ty = mk_c(c)->strutil().mk_string_sort();
mk_c(c)->save_ast_trail(ty);
RETURN_Z3(of_sort(ty));
Z3_CATCH_RETURN(0);
}
Z3_bool Z3_API Z3_is_str_sort(Z3_context c, Z3_sort s) {
Z3_TRY;
LOG_Z3_is_str_sort(c, s);
RESET_ERROR_CODE();
bool result = mk_c(c)->strutil().is_str_sort(to_sort(s));
return result?Z3_TRUE:Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_is_str(Z3_context c, Z3_ast s) {
Z3_TRY;
LOG_Z3_is_str(c, s);
RESET_ERROR_CODE();
bool result = mk_c(c)->strutil().is_string(to_expr(s));
return result ? Z3_TRUE : Z3_FALSE;
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_string Z3_API Z3_get_str(Z3_context c, Z3_ast s) {
Z3_TRY;
LOG_Z3_get_str(c, s);
RESET_ERROR_CODE();
if (!mk_c(c)->strutil().is_string(to_expr(s))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return "";
}
std::string result = mk_c(c)->strutil().get_string_constant_value(to_expr(s));
return mk_c(c)->mk_external_string(result);
Z3_CATCH_RETURN("");
}
Z3_ast Z3_API Z3_mk_str(Z3_context c, Z3_string str) {
Z3_TRY;
LOG_Z3_mk_str(c, str);
RESET_ERROR_CODE();
std::string s(str);
app * a = mk_c(c)->strutil().mk_string(str);
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(0);
}
MK_BINARY(Z3_mk_str_concat, mk_c(c)->get_str_fid(), OP_STRCAT, SKIP);
MK_UNARY(Z3_mk_str_length, mk_c(c)->get_str_fid(), OP_STRLEN, SKIP);
MK_BINARY(Z3_mk_str_at, mk_c(c)->get_str_fid(), OP_STR_CHARAT, SKIP);
// translate prefixof/suffixof to StartsWith/EndsWith
Z3_ast Z3_API Z3_mk_str_prefixof(Z3_context c, Z3_ast pre, Z3_ast full) {
LOG_Z3_mk_str_prefixof(c, pre, full);
Z3_TRY;
RESET_ERROR_CODE();
expr * args[2] = { to_expr(full), to_expr(pre) }; // reverse args
ast * a = mk_c(c)->m().mk_app(mk_c(c)->get_str_fid(), OP_STR_STARTSWITH, 0, 0, 2, args);
mk_c(c)->save_ast_trail(a);
check_sorts(c, a);
RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_str_suffixof(Z3_context c, Z3_ast suf, Z3_ast full) {
LOG_Z3_mk_str_suffixof(c, suf, full);
Z3_TRY;
RESET_ERROR_CODE();
expr * args[2] = { to_expr(full), to_expr(suf) }; // reverse args
ast * a = mk_c(c)->m().mk_app(mk_c(c)->get_str_fid(), OP_STR_ENDSWITH, 0, 0, 2, args);
mk_c(c)->save_ast_trail(a);
check_sorts(c, a);
RETURN_Z3(of_ast(a));
Z3_CATCH_RETURN(0);
}
MK_BINARY(Z3_mk_str_contains, mk_c(c)->get_str_fid(), OP_STR_CONTAINS, SKIP);
MK_TERNARY(Z3_mk_str_indexof, mk_c(c)->get_str_fid(), OP_STR_INDEXOF, SKIP);
MK_TERNARY(Z3_mk_str_substr, mk_c(c)->get_str_fid(), OP_STR_SUBSTR, SKIP);
MK_TERNARY(Z3_mk_str_replace, mk_c(c)->get_str_fid(), OP_STR_REPLACE, SKIP);
Z3_ast Z3_API Z3_mk_str_to_regex(Z3_context c, Z3_string str) {
LOG_Z3_mk_str_to_regex(c, str);
Z3_TRY;
RESET_ERROR_CODE();
std::string s(str);
app * a = mk_c(c)->strutil().mk_string(str);
mk_c(c)->save_ast_trail(a);
expr * args[1] = { to_expr(a) };
ast * re = mk_c(c)->m().mk_app(mk_c(c)->get_str_fid(), OP_RE_STR2REGEX, 0, 0, 1, args);
mk_c(c)->save_ast_trail(re);
check_sorts(c, re);
RETURN_Z3(of_ast(re));
Z3_CATCH_RETURN(0);
}
MK_BINARY(Z3_mk_str_in_regex, mk_c(c)->get_str_fid(), OP_RE_REGEXIN, SKIP);
MK_BINARY(Z3_mk_regex_concat, mk_c(c)->get_str_fid(), OP_RE_REGEXCONCAT, SKIP);
MK_BINARY(Z3_mk_regex_union, mk_c(c)->get_str_fid(), OP_RE_REGEXUNION, SKIP);
MK_UNARY(Z3_mk_regex_star, mk_c(c)->get_str_fid(), OP_RE_REGEXSTAR, SKIP);
MK_UNARY(Z3_mk_regex_plus, mk_c(c)->get_str_fid(), OP_RE_REGEXPLUS, SKIP);
Z3_ast Z3_API Z3_mk_regex_range(Z3_context c, Z3_string start, Z3_string end) {
LOG_Z3_mk_regex_range(c, start, end);
Z3_TRY;
RESET_ERROR_CODE();
std::string cStart(start);
std::string cEnd(end);
if(cStart.length() != 1 || cEnd.length() != 1) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
app * a1 = mk_c(c)->strutil().mk_string(cStart);
mk_c(c)->save_ast_trail(a1);
app * a2 = mk_c(c)->strutil().mk_string(cEnd);
mk_c(c)->save_ast_trail(a2);
expr * args[2] = { to_expr(a1), to_expr(a2) };
ast * range = mk_c(c)->m().mk_app(mk_c(c)->get_str_fid(), OP_RE_REGEXCHARRANGE, 0, 0, 2, args);
mk_c(c)->save_ast_trail(range);
check_sorts(c, range);
RETURN_Z3(of_ast(range));
Z3_CATCH_RETURN(0);
}
};

2
src/api/z3_api.h
View file

@ -165,8 +165,6 @@ typedef enum
Z3_ROUNDING_MODE_SORT,
Z3_SEQ_SORT,
Z3_RE_SORT,
Z3_STRING_SORT,
Z3_REGEX_SORT,
Z3_UNKNOWN_SORT = 1000
} Z3_sort_kind;

5
src/ast/ast_smt2_pp.h
View file

@ -50,7 +50,6 @@ public:
virtual array_util & get_arutil() = 0;
virtual fpa_util & get_futil() = 0;
virtual seq_util & get_sutil() = 0;
virtual str_util & get_strutil() = 0;
virtual datalog::dl_decl_util& get_dlutil() = 0;
virtual bool uses(symbol const & s) const = 0;
virtual format_ns::format * pp_fdecl(func_decl * f, unsigned & len);
@ -77,17 +76,15 @@ class smt2_pp_environment_dbg : public smt2_pp_environment {
array_util m_arutil;
fpa_util m_futil;
seq_util m_sutil;
str_util m_strutil;
datalog::dl_decl_util m_dlutil;
public:
smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_sutil(m), m_strutil(m), m_dlutil(m) {}
smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_sutil(m), m_dlutil(m) {}
virtual ast_manager & get_manager() const { return m_manager; }
virtual arith_util & get_autil() { return m_autil; }
virtual bv_util & get_bvutil() { return m_bvutil; }
virtual seq_util & get_sutil() { return m_sutil; }
virtual array_util & get_arutil() { return m_arutil; }
virtual fpa_util & get_futil() { return m_futil; }
virtual str_util & get_strutil() { return m_strutil; }
virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
virtual bool uses(symbol const & s) const { return false; }
};

5
src/ast/ast_smt_pp.cpp
View file

@ -165,7 +165,6 @@ class smt_printer {
bv_util m_bvutil;
seq_util m_sutil;
fpa_util m_futil;
str_util m_strutil;
family_id m_basic_fid;
family_id m_bv_fid;
family_id m_str_fid;
@ -473,9 +472,6 @@ class smt_printer {
m_out << ") bv1[1])";
}
}
else if (m_strutil.is_string(n, &str)) {
m_out << "\"" << str << "\"";
}
else if (m_manager.is_label(n, pos, names) && names.size() >= 1) {
if (m_is_smt2) {
m_out << "(! ";
@ -839,7 +835,6 @@ public:
m_bvutil(m),
m_sutil(m),
m_futil(m),
m_strutil(m),
m_logic(logic),
m_AUFLIRA("AUFLIRA"),
// It's much easier to read those testcases with that.

4
src/ast/reg_decl_plugins.cpp
View file

@ -26,7 +26,6 @@ Revision History:
#include"seq_decl_plugin.h"
#include"pb_decl_plugin.h"
#include"fpa_decl_plugin.h"
#include"str_decl_plugin.h"
void reg_decl_plugins(ast_manager & m) {
if (!m.get_plugin(m.mk_family_id(symbol("arith")))) {
@ -53,7 +52,4 @@ void reg_decl_plugins(ast_manager & m) {
if (!m.get_plugin(m.mk_family_id(symbol("pb")))) {
m.register_plugin(symbol("pb"), alloc(pb_decl_plugin));
}
if (!m.get_plugin(m.mk_family_id(symbol("str")))) {
m.register_plugin(symbol("str"), alloc(str_decl_plugin));
}
}

3
src/ast/rewriter/str_rewriter.cpp
View file

@ -17,6 +17,8 @@ Notes:
--*/
#if 0
#include"str_rewriter.h"
#include"arith_decl_plugin.h"
#include"ast_pp.h"
@ -698,3 +700,4 @@ bool str_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
return true;
}
#endif /* disable */

4
src/ast/rewriter/str_rewriter.h
View file

@ -17,6 +17,8 @@ Notes:
--*/
#if 0
#include"str_decl_plugin.h"
#include"arith_decl_plugin.h"
#include"rewriter_types.h"
@ -114,3 +116,5 @@ public:
bool matches(std::string input);
};
#endif /* disable */

5
src/ast/str_decl_plugin.cpp
View file

@ -14,6 +14,9 @@ Author:
Revision History:
--*/
#if 0
#include<sstream>
#include"str_decl_plugin.h"
#include"string_buffer.h"
@ -494,3 +497,5 @@ std::string str_util::get_std_regex_str(expr * regex) {
UNREACHABLE(); return "";
}
}
#endif /* disable */

5
src/ast/str_decl_plugin.h
View file

@ -14,6 +14,9 @@ Author:
Revision History:
--*/
#if 0
#ifndef _STR_DECL_PLUGIN_H_
#define _STR_DECL_PLUGIN_H_
@ -211,3 +214,5 @@ public:
};
#endif /* _STR_DECL_PLUGIN_H_ */
#endif /* disable */

7
src/cmd_context/check_logic.cpp
View file

@ -21,7 +21,6 @@ Revision History:
#include"array_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"seq_decl_plugin.h"
#include"str_decl_plugin.h"
#include"pb_decl_plugin.h"
#include"datatype_decl_plugin.h"
#include"ast_pp.h"
@ -35,7 +34,6 @@ struct check_logic::imp {
bv_util m_bv_util;
array_util m_ar_util;
seq_util m_seq_util;
str_util m_str_util;
datatype_util m_dt_util;
pb_util m_pb_util;
bool m_uf; // true if the logic supports uninterpreted functions
@ -49,7 +47,7 @@ struct check_logic::imp {
bool m_quantifiers; // true if the logic supports quantifiers
bool m_unknown_logic;
imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m), m_seq_util(m), m_str_util(m), m_dt_util(m), m_pb_util(m) {
imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m), m_seq_util(m), m_dt_util(m), m_pb_util(m) {
reset();
}
@ -444,9 +442,6 @@ struct check_logic::imp {
else if (fid == m_seq_util.get_family_id()) {
// nothing to check
}
else if (fid == m_str_util.get_family_id()) {
// nothing to check
}
else if (fid == m_dt_util.get_family_id() && m_logic == "QF_FD") {
// nothing to check
}

8
src/cmd_context/cmd_context.cpp
View file

@ -26,7 +26,6 @@ Notes:
#include"seq_decl_plugin.h"
#include"pb_decl_plugin.h"
#include"fpa_decl_plugin.h"
#include"str_decl_plugin.h"
#include"ast_pp.h"
#include"var_subst.h"
#include"pp.h"
@ -250,7 +249,6 @@ protected:
array_util m_arutil;
fpa_util m_futil;
seq_util m_sutil;
str_util m_strutil;
datalog::dl_decl_util m_dlutil;
@ -272,7 +270,7 @@ protected:
}
public:
pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_sutil(o.m()), m_strutil(o.m()), m_dlutil(o.m()) {}
pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_sutil(o.m()), m_dlutil(o.m()) {}
virtual ~pp_env() {}
virtual ast_manager & get_manager() const { return m_owner.m(); }
virtual arith_util & get_autil() { return m_autil; }
@ -280,7 +278,7 @@ public:
virtual array_util & get_arutil() { return m_arutil; }
virtual fpa_util & get_futil() { return m_futil; }
virtual seq_util & get_sutil() { return m_sutil; }
virtual str_util & get_strutil() { return m_strutil; }
virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
virtual bool uses(symbol const & s) const {
return
@ -561,7 +559,6 @@ void cmd_context::init_manager_core(bool new_manager) {
register_plugin(symbol("pb"), alloc(pb_decl_plugin), logic_has_pb());
register_plugin(symbol("fpa"), alloc(fpa_decl_plugin), logic_has_fpa());
register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic());
register_plugin(symbol("str"), alloc(str_decl_plugin), logic_has_str());
}
else {
// the manager was created by an external module
@ -575,7 +572,6 @@ void cmd_context::init_manager_core(bool new_manager) {
load_plugin(symbol("datatype"), logic_has_datatype(), fids);
load_plugin(symbol("seq"), logic_has_seq(), fids);
load_plugin(symbol("fpa"), logic_has_fpa(), fids);
load_plugin(symbol("str"), logic_has_str(), fids);
load_plugin(symbol("pb"), logic_has_pb(), fids);
svector<family_id>::iterator it = fids.begin();
svector<family_id>::iterator end = fids.end();

27
src/parsers/smt2/smt2parser.cpp
View file

@ -23,7 +23,6 @@ Revision History:
#include"bv_decl_plugin.h"
#include"arith_decl_plugin.h"
#include"seq_decl_plugin.h"
#include"str_decl_plugin.h"
#include"ast_pp.h"
#include"well_sorted.h"
#include"pattern_validation.h"
@ -68,7 +67,6 @@ namespace smt2 {
scoped_ptr<bv_util> m_bv_util;
scoped_ptr<arith_util> m_arith_util;
scoped_ptr<seq_util> m_seq_util;
scoped_ptr<str_util> m_str_util;
scoped_ptr<pattern_validator> m_pattern_validator;
scoped_ptr<var_shifter> m_var_shifter;
@ -286,12 +284,6 @@ namespace smt2 {
return *(m_bv_util.get());
}
str_util & strutil() {
if (m_str_util.get() == 0)
m_str_util = alloc(str_util, m());
return *(m_str_util.get());
}
pattern_validator & pat_validator() {
if (m_pattern_validator.get() == 0) {
m_pattern_validator = alloc(pattern_validator, m());
@ -1086,29 +1078,10 @@ namespace smt2 {
next();
}
// sorry, breaking theory_seq for a bit
/*
void parse_string_const() {
SASSERT(curr() == scanner::STRING_TOKEN);
expr_stack().push_back(sutil().str.mk_string(symbol(m_scanner.get_string())));
TRACE("smt2parser", tout << "new string: " << mk_pp(expr_stack().back(), m()) << "\n";);
next();
}
*/
void parse_string_const() {
parse_string();
}
void parse_string() {
SASSERT(curr() == scanner::STRING_TOKEN);
char const *original_token = m_scanner.get_string();
size_t bufsize = strlen(original_token);
char * buf = alloc_svect(char, bufsize + 1);
strncpy(buf, original_token, bufsize);
buf[bufsize] = '\0';
TRACE("parse_string", tout << "new string constant: " << buf << " length=" << bufsize << "\n";);
expr_stack().push_back(strutil().mk_string_with_escape_characters(buf));
next();
}

137
src/smt/theory_str.cpp
View file

@ -44,7 +44,7 @@ theory_str::theory_str(ast_manager & m, theory_str_params const & params):
/* Internal setup */
search_started(false),
m_autil(m),
m_strutil(m),
u(m),
sLevel(0),
finalCheckProgressIndicator(false),
m_trail(m),
@ -70,36 +70,26 @@ theory_str::~theory_str() {
m_trail_stack.reset();
}
expr * theory_str::mk_string(std::string str) {
expr * theory_str::mk_string(zstring const& str) {
if (m_params.m_StringConstantCache) {
++totalCacheAccessCount;
expr * val;
if (stringConstantCache.find(str, val)) {
// cache hit
++cacheHitCount;
TRACE("t_str_cache", tout << "cache hit: \"" << str << "\" ("
<< cacheHitCount << " hits, " << cacheMissCount << " misses out of "
<< totalCacheAccessCount << " accesses)" << std::endl;);
return val;
} else {
// cache miss
++cacheMissCount;
TRACE("t_str_cache", tout << "cache miss: \"" << str << "\" ("
<< cacheHitCount << " hits, " << cacheMissCount << " misses out of "
<< totalCacheAccessCount << " accesses)" << std::endl;);
val = m_strutil.mk_string(str);
val = u.str.mk_string(str);
m_trail.push_back(val);
stringConstantCache.insert(str, val);
return val;
}
} else {
return m_strutil.mk_string(str);
return u.str.mk_string(str);
}
}
expr * theory_str::mk_string(const char * str) {
std::string valStr(str);
return mk_string(valStr);
symbol sym(str);
return u.str.mk_string(sym);
}
void theory_str::initialize_charset() {
@ -210,25 +200,6 @@ void theory_str::assert_implication(expr * premise, expr * conclusion) {
}
bool theory_str::internalize_atom(app * atom, bool gate_ctx) {
/*
TRACE("t_str", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << std::endl;);
SASSERT(atom->get_family_id() == get_family_id());
context & ctx = get_context();
if (ctx.b_internalized(atom))
return true;
unsigned num_args = atom->get_num_args();
for (unsigned i = 0; i < num_args; i++)
ctx.internalize(atom->get_arg(i), false);
literal l(ctx.mk_bool_var(atom));
ctx.set_var_theory(l.var(), get_id());
return true;
*/
return internalize_term(atom);
}
@ -267,10 +238,9 @@ bool theory_str::internalize_term(app * term) {
theory_var v = mk_var(e);
TRACE("t_str_detail", tout << "term has theory var #" << v << std::endl;);
if (opt_EagerStringConstantLengthAssertions && m_strutil.is_string(term)) {
if (opt_EagerStringConstantLengthAssertions && u.str.is_string(term)) {
TRACE("t_str", tout << "eagerly asserting length of string term " << mk_pp(term, m) << std::endl;);
m_basicstr_axiom_todo.insert(e);
TRACE("t_str_axiom_bug", tout << "add " << mk_pp(e->get_owner(), m) << " to m_basicstr_axiom_todo" << std::endl;);
}
return true;
}
@ -295,7 +265,7 @@ void theory_str::refresh_theory_var(expr * e) {
theory_var theory_str::mk_var(enode* n) {
TRACE("t_str_detail", tout << "mk_var for " << mk_pp(n->get_owner(), get_manager()) << std::endl;);
ast_manager & m = get_manager();
if (!(is_sort_of(m.get_sort(n->get_owner()), m_strutil.get_fid(), STRING_SORT))) {
if (!(is_sort_of(m.get_sort(n->get_owner()), u.get_family_id(), _STRING_SORT))) {
return null_theory_var;
}
if (is_attached_to_var(n)) {
@ -413,7 +383,7 @@ void theory_str::add_cut_info_merge(expr * destNode, int slevel, expr * srcNode)
void theory_str::check_and_init_cut_var(expr * node) {
if (cut_var_map.contains(node)) {
return;
} else if (!m_strutil.is_string(node)) {
} else if (!u.str.is_string(node)) {
add_cut_info_one_node(node, -1, node);
}
}
@ -511,7 +481,7 @@ app * theory_str::mk_str_var(std::string name) {
TRACE("t_str_detail", tout << "creating string variable " << name << " at scope level " << sLevel << std::endl;);
sort * string_sort = m.mk_sort(get_family_id(), STRING_SORT);
sort * string_sort = u.str.mk_string_sort();
app * a = m.mk_fresh_const(name.c_str(), string_sort);
TRACE("t_str_detail", tout << "a->get_family_id() = " << a->get_family_id() << std::endl
@ -538,7 +508,7 @@ app * theory_str::mk_regex_rep_var() {
context & ctx = get_context();
ast_manager & m = get_manager();
sort * string_sort = m.mk_sort(get_family_id(), STRING_SORT);
sort * string_sort = u.str.mk_string_sort();
app * a = m.mk_fresh_const("regex", string_sort);
ctx.internalize(a, false);
@ -590,7 +560,7 @@ app * theory_str::mk_nonempty_str_var() {
TRACE("t_str_detail", tout << "creating nonempty string variable " << name << " at scope level " << sLevel << std::endl;);
sort * string_sort = m.mk_sort(get_family_id(), STRING_SORT);
sort * string_sort = u.str.mk_string_sort();
app * a = m.mk_fresh_const(name.c_str(), string_sort);
ctx.internalize(a, false);
@ -642,8 +612,7 @@ app * theory_str::mk_unroll(expr * n, expr * bound) {
}
app * theory_str::mk_contains(expr * haystack, expr * needle) {
expr * args[2] = {haystack, needle};
app * contains = get_manager().mk_app(get_id(), OP_STR_CONTAINS, 0, 0, 2, args);
app * contains = u.str.mk_contains(haystack, needle); // TODO double-check semantics/argument order
m_trail.push_back(contains);
// immediately force internalization so that axiom setup does not fail
get_context().internalize(contains, false);
@ -652,8 +621,8 @@ app * theory_str::mk_contains(expr * haystack, expr * needle) {
}
app * theory_str::mk_indexof(expr * haystack, expr * needle) {
expr * args[2] = {haystack, needle};
app * indexof = get_manager().mk_app(get_id(), OP_STR_INDEXOF, 0, 0, 2, args);
// TODO check meaning of the third argument here
app * indexof = u.str.mk_index(haystack, needle, mk_int(0));
m_trail.push_back(indexof);
// immediately force internalization so that axiom setup does not fail
get_context().internalize(indexof, false);
@ -663,25 +632,23 @@ app * theory_str::mk_indexof(expr * haystack, expr * needle) {
app * theory_str::mk_strlen(expr * e) {
/*if (m_strutil.is_string(e)) {*/ if (false) {
const char * strval = 0;
m_strutil.is_string(e, &strval);
int len = strlen(strval);
zstring strval;
u.str.is_string(e, strval);
unsigned int len = strval.length();
return m_autil.mk_numeral(rational(len), true);
} else {
if (false) {
// use cache
app * lenTerm = NULL;
if (!length_ast_map.find(e, lenTerm)) {
expr * args[1] = {e};
lenTerm = get_manager().mk_app(get_id(), OP_STRLEN, 0, 0, 1, args);
lenTerm = u.str.mk_length(e);
length_ast_map.insert(e, lenTerm);
m_trail.push_back(lenTerm);
}
return lenTerm;
} else {
// always regen
expr * args[1] = {e};
return get_manager().mk_app(get_id(), OP_STRLEN, 0, 0, 1, args);
return u.str.mk_length(e);
}
}
}
@ -699,24 +666,22 @@ expr * theory_str::mk_concat_const_str(expr * n1, expr * n2) {
expr * v1 = get_eqc_value(n1, n1HasEqcValue);
expr * v2 = get_eqc_value(n2, n2HasEqcValue);
if (n1HasEqcValue && n2HasEqcValue) {
const char * n1_str_tmp;
m_strutil.is_string(v1, & n1_str_tmp);
std::string n1_str(n1_str_tmp);
const char * n2_str_tmp;
m_strutil.is_string(v2, & n2_str_tmp);
std::string n2_str(n2_str_tmp);
std::string result = n1_str + n2_str;
zstring n1_str;
u.str.is_string(v1, n1_str);
zstring n2_str;
u.str.is_string(v2, n2_str);
zstring result = n1_str + n2_str;
return mk_string(result);
} else if (n1HasEqcValue && !n2HasEqcValue) {
const char * n1_str_tmp;
m_strutil.is_string(v1, & n1_str_tmp);
if (strcmp(n1_str_tmp, "") == 0) {
zstring n1_str;
u.str.is_string(v1, n1_str);
if (n1_str.empty()) {
return n2;
}
} else if (!n1HasEqcValue && n2HasEqcValue) {
const char * n2_str_tmp;
m_strutil.is_string(v2, & n2_str_tmp);
if (strcmp(n2_str_tmp, "") == 0) {
zstring n2_str;
u.str.is_string(v2, n2_str);
if (n2_str.empty()) {
return n1;
}
}
@ -735,38 +700,42 @@ expr * theory_str::mk_concat(expr * n1, expr * n2) {
if (n1HasEqcValue && n2HasEqcValue) {
return mk_concat_const_str(n1, n2);
} else if (n1HasEqcValue && !n2HasEqcValue) {
bool n2_isConcatFunc = is_concat(to_app(n2));
if (m_strutil.get_string_constant_value(n1) == "") {
bool n2_isConcatFunc = u.str.is_concat(to_app(n2));
zstring n1_str;
u.str.is_string(n1, n1_str);
if (n1_str.empty()) {
return n2;
}
if (n2_isConcatFunc) {
expr * n2_arg0 = to_app(n2)->get_arg(0);
expr * n2_arg1 = to_app(n2)->get_arg(1);
if (m_strutil.is_string(n2_arg0)) {
if (u.str.is_string(n2_arg0)) {
n1 = mk_concat_const_str(n1, n2_arg0); // n1 will be a constant
n2 = n2_arg1;
}
}
} else if (!n1HasEqcValue && n2HasEqcValue) {
if (m_strutil.get_string_constant_value(n2) == "") {
zstring n2_str;
u.str.is_string(n2, n2_str);
if (n2_str.empty()) {
return n1;
}
if (is_concat(to_app(n1))) {
if (u.str.is_concat(to_app(n1))) {
expr * n1_arg0 = to_app(n1)->get_arg(0);
expr * n1_arg1 = to_app(n1)->get_arg(1);
if (m_strutil.is_string(n1_arg1)) {
if (u.str.is_string(n1_arg1)) {
n1 = n1_arg0;
n2 = mk_concat_const_str(n1_arg1, n2); // n2 will be a constant
}
}
} else {
if (is_concat(to_app(n1)) && is_concat(to_app(n2))) {
if (u.str.is_concat(to_app(n1)) && u.str.is_concat(to_app(n2))) {
expr * n1_arg0 = to_app(n1)->get_arg(0);
expr * n1_arg1 = to_app(n1)->get_arg(1);
expr * n2_arg0 = to_app(n2)->get_arg(0);
expr * n2_arg1 = to_app(n2)->get_arg(1);
if (m_strutil.is_string(n1_arg1) && m_strutil.is_string(n2_arg0)) {
if (u.str.is_string(n1_arg1) && u.str.is_string(n2_arg0)) {
expr * tmpN1 = n1_arg0;
expr * tmpN2 = mk_concat_const_str(n1_arg1, n2_arg0);
n1 = mk_concat(tmpN1, tmpN2);
@ -784,8 +753,7 @@ expr * theory_str::mk_concat(expr * n1, expr * n2) {
expr * concatAst = NULL;
if (!concat_astNode_map.find(n1, n2, concatAst)) {
expr * args[2] = {n1, n2};
concatAst = m.mk_app(get_id(), OP_STRCAT, 0, 0, 2, args);
concatAst = u.str.mk_concat(n1, n2);
m_trail.push_back(concatAst);
concat_astNode_map.insert(n1, n2, concatAst);
@ -841,25 +809,30 @@ void theory_str::propagate() {
for (unsigned i = 0; i < m_library_aware_axiom_todo.size(); ++i) {
enode * e = m_library_aware_axiom_todo[i];
if (is_str_to_int(e)) {
app * a = e->get_owner();
if (u.str.is_stoi(a)) {
instantiate_axiom_str_to_int(e);
} else if (is_int_to_str(e)) {
} else if (u.str.is_itos(a)) {
instantiate_axiom_int_to_str(e);
} else if (is_CharAt(e)) {
} else if (u.str.is_at(a)) {
instantiate_axiom_CharAt(e);
/* TODO NEXT: StartsWith/EndsWith -> prefixof/suffixof
} else if (is_StartsWith(e)) {
instantiate_axiom_StartsWith(e);
} else if (is_EndsWith(e)) {
instantiate_axiom_EndsWith(e);
} else if (is_Contains(e)) {
*/
} else if (u.str.is_contains(a)) {
instantiate_axiom_Contains(e);
} else if (is_Indexof(e)) {
} else if (u.str.is_index(a)) {
instantiate_axiom_Indexof(e);
/* TODO NEXT: Indexof2/Lastindexof rewrite?
} else if (is_Indexof2(e)) {
instantiate_axiom_Indexof2(e);
} else if (is_LastIndexof(e)) {
instantiate_axiom_LastIndexof(e);
} else if (is_Substr(e)) {
*/
} else if (u.str.is_substr(a)) {
instantiate_axiom_Substr(e);
} else if (is_Replace(e)) {
instantiate_axiom_Replace(e);

83
src/smt/theory_str.h
View file

@ -27,32 +27,13 @@ Revision History:
#include<set>
#include<stack>
#include<vector>
#include"str_rewriter.h"
#include<map>
#include"seq_decl_plugin.h"
#include"union_find.h"
#include"theory_seq_empty.h"
namespace smt {
class str_value_factory : public value_factory {
str_util m_util;
public:
str_value_factory(ast_manager & m, family_id fid) :
value_factory(m, fid),
m_util(m) {}
virtual ~str_value_factory() {}
virtual expr * get_some_value(sort * s) {
return m_util.mk_string("some value");
}
virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
v1 = m_util.mk_string("value 1");
v2 = m_util.mk_string("value 2");
return true;
}
virtual expr * get_fresh_value(sort * s) {
return m_util.mk_fresh_string();
}
virtual void register_value(expr * n) { /* Ignore */ }
};
// rather than modify obj_pair_map I inherit from it and add my own helper methods
class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {
public:
@ -110,12 +91,12 @@ namespace smt {
typedef union_find<theory_str> th_union_find;
typedef map<rational, expr*, obj_hash<rational>, default_eq<rational> > rational_map;
struct str_hash_proc {
unsigned operator()(std::string const & s) const {
return string_hash(s.c_str(), static_cast<unsigned>(s.length()), 17);
struct zstring_hash_proc {
unsigned operator()(zstring const & s) const {
return string_hash(s.encode().c_str(), static_cast<unsigned>(s.length()), 17);
}
};
typedef map<std::string, expr*, str_hash_proc, default_eq<std::string> > string_map;
typedef map<zstring, expr*, zstring_hash_proc, default_eq<zstring> > string_map;
protected:
theory_str_params const & m_params;
@ -188,14 +169,14 @@ namespace smt {
bool search_started;
arith_util m_autil;
str_util m_strutil;
seq_util u;
int sLevel;
bool finalCheckProgressIndicator;
expr_ref_vector m_trail; // trail for generated terms
str_value_factory * m_factory;
seq_factory * m_factory;
// terms we couldn't go through set_up_axioms() with because they weren't internalized
expr_ref_vector m_delayed_axiom_setup_terms;
@ -259,7 +240,7 @@ namespace smt {
std::map<std::pair<expr*, std::string>, expr*> regex_in_bool_map;
std::map<expr*, std::set<std::string> > regex_in_var_reg_str_map;
std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
// std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
char * char_set;
std::map<char, int> charSetLookupTable;
@ -327,7 +308,7 @@ namespace smt {
void assert_implication(expr * premise, expr * conclusion);
expr * rewrite_implication(expr * premise, expr * conclusion);
expr * mk_string(std::string str);
expr * mk_string(zstring const& str);
expr * mk_string(const char * str);
app * mk_strlen(expr * e);
@ -359,48 +340,6 @@ namespace smt {
app * mk_unroll_test_var();
void add_nonempty_constraint(expr * s);
bool is_concat(app const * a) const { return a->is_app_of(get_id(), OP_STRCAT); }
bool is_concat(enode const * n) const { return is_concat(n->get_owner()); }
bool is_string(app const * a) const { return a->is_app_of(get_id(), OP_STR); }
bool is_string(enode const * n) const { return is_string(n->get_owner()); }
bool is_strlen(app const * a) const { return a->is_app_of(get_id(), OP_STRLEN); }
bool is_strlen(enode const * n) const { return is_strlen(n->get_owner()); }
bool is_CharAt(app const * a) const { return a->is_app_of(get_id(), OP_STR_CHARAT); }
bool is_CharAt(enode const * n) const { return is_CharAt(n->get_owner()); }
bool is_StartsWith(app const * a) const { return a->is_app_of(get_id(), OP_STR_STARTSWITH); }
bool is_StartsWith(enode const * n) const { return is_StartsWith(n->get_owner()); }
bool is_EndsWith(app const * a) const { return a->is_app_of(get_id(), OP_STR_ENDSWITH); }
bool is_EndsWith(enode const * n) const { return is_EndsWith(n->get_owner()); }
bool is_Contains(app const * a) const { return a->is_app_of(get_id(), OP_STR_CONTAINS); }
bool is_Contains(enode const * n) const { return is_Contains(n->get_owner()); }
bool is_Indexof(app const * a) const { return a->is_app_of(get_id(), OP_STR_INDEXOF); }
bool is_Indexof(enode const * n) const { return is_Indexof(n->get_owner()); }
bool is_Indexof2(app const * a) const { return a->is_app_of(get_id(), OP_STR_INDEXOF2); }
bool is_Indexof2(enode const * n) const { return is_Indexof2(n->get_owner()); }
bool is_LastIndexof(app const * a) const { return a->is_app_of(get_id(), OP_STR_LASTINDEXOF); }
bool is_LastIndexof(enode const * n) const { return is_LastIndexof(n->get_owner()); }
bool is_Substr(app const * a) const { return a->is_app_of(get_id(), OP_STR_SUBSTR); }
bool is_Substr(enode const * n) const { return is_Substr(n->get_owner()); }
bool is_Replace(app const * a) const { return a->is_app_of(get_id(), OP_STR_REPLACE); }
bool is_Replace(enode const * n) const { return is_Replace(n->get_owner()); }
bool is_str_to_int(app const * a) const { return a->is_app_of(get_id(), OP_STR_STR2INT); }
bool is_str_to_int(enode const * n) const { return is_str_to_int(n->get_owner()); }
bool is_int_to_str(app const * a) const { return a->is_app_of(get_id(), OP_STR_INT2STR); }
bool is_int_to_str(enode const * n) const { return is_int_to_str(n->get_owner()); }
bool is_RegexIn(app const * a) const { return a->is_app_of(get_id(), OP_RE_REGEXIN); }
bool is_RegexIn(enode const * n) const { return is_RegexIn(n->get_owner()); }
bool is_RegexConcat(app const * a) const { return a->is_app_of(get_id(), OP_RE_REGEXCONCAT); }
bool is_RegexConcat(enode const * n) const { return is_RegexConcat(n->get_owner()); }
bool is_RegexStar(app const * a) const { return a->is_app_of(get_id(), OP_RE_REGEXSTAR); }
bool is_RegexStar(enode const * n) const { return is_RegexStar(n->get_owner()); }
bool is_RegexUnion(app const * a) const { return a->is_app_of(get_id(), OP_RE_REGEXUNION); }
bool is_RegexUnion(enode const * n) const { return is_RegexUnion(n->get_owner()); }
bool is_Str2Reg(app const * a) const { return a->is_app_of(get_id(), OP_RE_STR2REGEX); }
bool is_Str2Reg(enode const * n) const { return is_Str2Reg(n->get_owner()); }
bool is_Unroll(app const * a) const { return a->is_app_of(get_id(), OP_RE_UNROLL); }
bool is_Unroll(enode const * n) const { return is_Unroll(n->get_owner()); }
void instantiate_concat_axiom(enode * cat);
void try_eval_concat(enode * cat);
void instantiate_basic_string_axioms(enode * str);