mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

merging seq and string

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-12-06 22:15:56 -08:00
parent aead45a252
commit 08bfd08412
6 changed files with 93 additions and 114 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/ast_smt2_pp.cpp
View file

@ -424,6 +424,11 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
fs.push_back(mk_unsigned(m, sbits));
return mk_seq1(m, fs.begin(), fs.end(), f2f(), "_");
}
if (get_sutil().is_seq(s) && !get_sutil().is_string(s)) {
ptr_buffer<format> fs;
fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast())));
return mk_seq1(m, fs.begin(), fs.end(), f2f(), "Seq");
}
return format_ns::mk_string(get_manager(), s->get_name().str().c_str());
}

30
src/ast/rewriter/seq_rewriter.cpp
View file

@ -19,6 +19,7 @@ Notes:
#include"seq_rewriter.h"
#include"arith_decl_plugin.h"
#include"ast_pp.h"
br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
@ -28,13 +29,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_SEQ_UNIT:
case OP_SEQ_EMPTY:
case OP_SEQ_CONCAT:
case OP_SEQ_CONS:
case OP_SEQ_REV_CONS:
case OP_SEQ_HEAD:
case OP_SEQ_TAIL:
case OP_SEQ_LAST:
case OP_SEQ_FIRST:
case OP_SEQ_PREFIX_OF:
case OP_SEQ_SUFFIX_OF:
case OP_SEQ_SUBSEQ_OF:
@ -49,8 +43,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_RE_CONCAT:
case OP_RE_UNION:
case OP_RE_INTERSECT:
case OP_RE_COMPLEMENT:
case OP_RE_DIFFERENCE:
case OP_RE_LOOP:
case OP_RE_EMPTY_SET:
case OP_RE_FULL_SET:
@ -63,9 +55,10 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
// string specific operators.
case OP_STRING_CONST:
return BR_FAILED;
case OP_STRING_CONCAT:
case OP_SEQ_CONCAT:
case _OP_STRING_CONCAT:
SASSERT(num_args == 2);
return mk_str_concat(args[0], args[1], result);
return mk_seq_concat(args[0], args[1], result);
case OP_STRING_LENGTH:
SASSERT(num_args == 1);
return mk_str_length(args[0], result);
@ -96,19 +89,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_STRING_STOI:
SASSERT(num_args == 1);
return mk_str_stoi(args[0], result);
//case OP_STRING_U16TOS:
//case OP_STRING_STOU16:
//case OP_STRING_U32TOS:
//case OP_STRING_STOU32:
case OP_STRING_IN_REGEXP:
case OP_STRING_TO_REGEXP:
case OP_REGEXP_CONCAT:
case OP_REGEXP_UNION:
case OP_REGEXP_INTER:
case OP_REGEXP_STAR:
case OP_REGEXP_PLUS:
case OP_REGEXP_OPT:
case OP_REGEXP_RANGE:
case OP_REGEXP_LOOP:
return BR_FAILED;
}
@ -122,7 +104,7 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
"" + a = a
(a + string) + string = a + string
*/
br_status seq_rewriter::mk_str_concat(expr* a, expr* b, expr_ref& result) {
br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
std::string s1, s2;
expr* c, *d;
bool isc1 = m_util.str.is_const(a, s1);
@ -145,7 +127,7 @@ br_status seq_rewriter::mk_str_concat(expr* a, expr* b, expr_ref& result) {
}
if (m_util.str.is_concat(a, c, d) &&
m_util.str.is_const(d, s1) && isc2) {
result = m_util.str.mk_string(s1 + s2);
result = m_util.str.mk_concat(c, m_util.str.mk_string(s1 + s2));
return BR_DONE;
}
return BR_FAILED;

2
src/ast/rewriter/seq_rewriter.h
View file

@ -34,7 +34,7 @@ class seq_rewriter {
arith_util m_autil;
ptr_vector<expr> m_es;
br_status mk_str_concat(expr* a, expr* b, expr_ref& result);
br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
br_status mk_str_length(expr* a, expr_ref& result);
br_status mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result);
br_status mk_str_strctn(expr* a, expr* b, expr_ref& result);

119
src/ast/seq_decl_plugin.cpp
View file

@ -19,16 +19,19 @@ Revision History:
#include "seq_decl_plugin.h"
#include "arith_decl_plugin.h"
#include "array_decl_plugin.h"
#include "ast_pp.h"
#include <sstream>
seq_decl_plugin::seq_decl_plugin(): m_init(false),
m_stringc_sym("String"),
m_string(0) {}
m_string(0),
m_char(0) {}
void seq_decl_plugin::finalize() {
for (unsigned i = 0; i < m_sigs.size(); ++i)
dealloc(m_sigs[i]);
m_manager->dec_ref(m_string);
m_manager->dec_ref(m_char);
}
bool seq_decl_plugin::is_sort_param(sort* s, unsigned& idx) {
@ -38,29 +41,32 @@ bool seq_decl_plugin::is_sort_param(sort* s, unsigned& idx) {
}
bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
ast_manager& m = *m_manager;
if (s == sP) return true;
unsigned i;
if (is_sort_param(sP, i)) {
if (binding.size() <= i) binding.resize(i+1);
if (binding[i] && (binding[i] != s)) return false;
TRACE("seq", tout << "setting binding @ " << i << " to " << mk_pp(s, m) << "\n";);
binding[i] = s;
return true;
}
if (s->get_family_id() == sP->get_family_id() &&
s->get_decl_kind() == sP->get_decl_kind() &&
s->get_name() == sP->get_name()) {
SASSERT(s->get_num_parameters() == sP->get_num_parameters());
for (unsigned i = 0; i < s->get_num_parameters(); ++i) {
parameter const& p = s->get_parameter(i);
if (p.is_ast() && is_sort(p.get_ast())) {
parameter const& p2 = sP->get_parameter(i);
if (!match(binding, to_sort(p.get_ast()), to_sort(p2.get_ast()))) return false;
}
s->get_num_parameters() == sP->get_num_parameters()) {
for (unsigned i = 0; i < s->get_num_parameters(); ++i) {
parameter const& p = s->get_parameter(i);
if (p.is_ast() && is_sort(p.get_ast())) {
parameter const& p2 = sP->get_parameter(i);
if (!match(binding, to_sort(p.get_ast()), to_sort(p2.get_ast()))) return false;
}
}
return true;
}
else {
TRACE("seq", tout << "Could not match " << mk_pp(s, m) << " and " << mk_pp(sP, m) << "\n";);
return false;
}
}
@ -71,6 +77,11 @@ bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
void seq_decl_plugin::match_left_assoc(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) {
ptr_vector<sort> binding;
ast_manager& m = *m_manager;
TRACE("seq",
tout << sig.m_name << ": ";
for (unsigned i = 0; i < dsz; ++i) tout << mk_pp(dom[i], m) << " ";
if (range) tout << " range: " << mk_pp(range, m);
tout << "\n";);
if (dsz == 0) {
std::ostringstream strm;
strm << "Unexpected number of arguments to '" << sig.m_name << "' ";
@ -91,6 +102,7 @@ void seq_decl_plugin::match_left_assoc(psig& sig, unsigned dsz, sort *const* dom
m.raise_exception(strm.str().c_str());
}
range_out = apply_binding(binding, sig.m_range);
TRACE("seq", tout << mk_pp(range_out, m) << "\n";);
}
void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) {
@ -162,10 +174,8 @@ void seq_decl_plugin::init() {
sort* u16T = 0;
sort* u32T = 0;
sort* seqAseqA[2] = { seqA, seqA };
sort* seqAA[2] = { seqA, A };
sort* seqAB[2] = { seqA, B };
sort* seqAreA[2] = { seqA, reA };
sort* AseqA[2] = { A, seqA };
sort* reAreA[2] = { reA, reA };
sort* AA[2] = { A, A };
sort* seqABB[3] = { seqA, B, B };
@ -177,30 +187,22 @@ void seq_decl_plugin::init() {
sort* str2TintT[3] = { strT, strT, intT };
m_sigs.resize(LAST_SEQ_OP);
// TBD: have (par ..) construct and load parameterized signature from premable.
m_sigs[OP_SEQ_UNIT] = alloc(psig, m, "seq-unit", 1, 1, &A, seqA);
m_sigs[OP_SEQ_EMPTY] = alloc(psig, m, "seq-empty", 1, 0, 0, seqA);
m_sigs[OP_SEQ_CONCAT] = alloc(psig, m, "seq-concat", 1, 2, seqAseqA, seqA);
m_sigs[OP_SEQ_CONS] = alloc(psig, m, "seq-cons", 1, 2, AseqA, seqA);
m_sigs[OP_SEQ_REV_CONS] = alloc(psig, m, "seq-rev-cons", 1, 2, seqAA, seqA);
m_sigs[OP_SEQ_HEAD] = alloc(psig, m, "seq-head", 1, 1, &seqA, A);
m_sigs[OP_SEQ_TAIL] = alloc(psig, m, "seq-tail", 1, 1, &seqA, seqA);
m_sigs[OP_SEQ_LAST] = alloc(psig, m, "seq-last", 1, 1, &seqA, A);
m_sigs[OP_SEQ_FIRST] = alloc(psig, m, "seq-first", 1, 1, &seqA, seqA);
m_sigs[OP_SEQ_PREFIX_OF] = alloc(psig, m, "seq-prefix-of", 1, 2, seqAseqA, boolT);
m_sigs[OP_SEQ_SUFFIX_OF] = alloc(psig, m, "seq-suffix-of", 1, 2, seqAseqA, boolT);
m_sigs[OP_SEQ_UNIT] = alloc(psig, m, "seq.unit", 1, 1, &A, seqA);
m_sigs[OP_SEQ_EMPTY] = alloc(psig, m, "seq.empty", 1, 0, 0, seqA);
m_sigs[OP_SEQ_CONCAT] = alloc(psig, m, "seq.++", 1, 2, seqAseqA, seqA);
m_sigs[OP_SEQ_PREFIX_OF] = alloc(psig, m, "seq.prefixof", 1, 2, seqAseqA, boolT);
m_sigs[OP_SEQ_SUFFIX_OF] = alloc(psig, m, "seq.suffixof", 1, 2, seqAseqA, boolT);
m_sigs[OP_SEQ_SUBSEQ_OF] = alloc(psig, m, "seq-subseq-of", 1, 2, seqAseqA, boolT);
m_sigs[OP_SEQ_EXTRACT] = alloc(psig, m, "seq-extract", 2, 3, seqABB, seqA);
m_sigs[OP_SEQ_NTH] = alloc(psig, m, "seq-nth", 2, 2, seqAB, A);
m_sigs[OP_SEQ_LENGTH] = alloc(psig, m, "seq-length", 1, 1, &seqA, intT);
m_sigs[OP_RE_PLUS] = alloc(psig, m, "re-plus", 1, 1, &reA, reA);
m_sigs[OP_RE_STAR] = alloc(psig, m, "re-star", 1, 1, &reA, reA);
m_sigs[OP_RE_OPTION] = alloc(psig, m, "re-option", 1, 1, &reA, reA);
m_sigs[OP_RE_RANGE] = alloc(psig, m, "re-range", 1, 2, AA, reA);
m_sigs[OP_RE_CONCAT] = alloc(psig, m, "re-concat", 1, 2, reAreA, reA);
m_sigs[OP_RE_UNION] = alloc(psig, m, "re-union", 1, 2, reAreA, reA);
m_sigs[OP_RE_INTERSECT] = alloc(psig, m, "re-intersect", 1, 2, reAreA, reA);
m_sigs[OP_RE_DIFFERENCE] = alloc(psig, m, "re-difference", 1, 2, reAreA, reA);
m_sigs[OP_RE_COMPLEMENT] = alloc(psig, m, "re-complement", 1, 1, &reA, reA);
m_sigs[OP_RE_PLUS] = alloc(psig, m, "re.+", 1, 1, &reA, reA);
m_sigs[OP_RE_STAR] = alloc(psig, m, "re.*", 1, 1, &reA, reA);
m_sigs[OP_RE_OPTION] = alloc(psig, m, "re.opt", 1, 1, &reA, reA);
m_sigs[OP_RE_RANGE] = alloc(psig, m, "re.range", 1, 2, seqAseqA, reA);
m_sigs[OP_RE_CONCAT] = alloc(psig, m, "re.++", 1, 2, reAreA, reA);
m_sigs[OP_RE_UNION] = alloc(psig, m, "re.union", 1, 2, reAreA, reA);
m_sigs[OP_RE_INTERSECT] = alloc(psig, m, "re.inter", 1, 2, reAreA, reA);
m_sigs[OP_RE_LOOP] = alloc(psig, m, "re-loop", 1, 1, &reA, reA);
m_sigs[OP_RE_EMPTY_SEQ] = alloc(psig, m, "re-empty-seq", 1, 0, 0, reA);
m_sigs[OP_RE_EMPTY_SET] = alloc(psig, m, "re-empty-set", 1, 0, 0, reA);
@ -209,7 +211,7 @@ void seq_decl_plugin::init() {
m_sigs[OP_RE_OF_PRED] = alloc(psig, m, "re-of-pred", 1, 1, &predA, reA);
m_sigs[OP_RE_MEMBER] = alloc(psig, m, "re-member", 1, 2, seqAreA, boolT);
m_sigs[OP_STRING_CONST] = 0;
m_sigs[OP_STRING_CONCAT] = alloc(psig, m, "str.++", 0, 2, str2T, strT);
m_sigs[_OP_STRING_CONCAT] = alloc(psig, m, "str.++", 1, 2, str2T, strT);
m_sigs[OP_STRING_LENGTH] = alloc(psig, m, "str.len", 0, 1, &strT, intT);
m_sigs[OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, boolT);
m_sigs[OP_STRING_STRCTN] = alloc(psig, m, "str.contains", 0, 2, str2T, boolT);
@ -222,19 +224,15 @@ void seq_decl_plugin::init() {
m_sigs[OP_STRING_STOI] = alloc(psig, m, "str.to.int", 0, 1, &strT, intT);
m_sigs[OP_STRING_IN_REGEXP] = alloc(psig, m, "str.in.re", 0, 2, strTreT, boolT);
m_sigs[OP_STRING_TO_REGEXP] = alloc(psig, m, "str.to.re", 0, 1, &strT, reT);
m_sigs[OP_REGEXP_CONCAT] = alloc(psig, m, "re.++", 0, 2, re2T, reT);
m_sigs[OP_REGEXP_UNION] = alloc(psig, m, "re.union", 0, 2, re2T, reT);
m_sigs[OP_REGEXP_INTER] = alloc(psig, m, "re.inter", 0, 2, re2T, reT);
m_sigs[OP_REGEXP_STAR] = alloc(psig, m, "re.*", 0, 1, &reT, reT);
m_sigs[OP_REGEXP_PLUS] = alloc(psig, m, "re.+", 0, 1, &reT, reT);
m_sigs[OP_REGEXP_OPT] = alloc(psig, m, "re.opt", 0, 1, &reT, reT);
m_sigs[OP_REGEXP_RANGE] = alloc(psig, m, "re.range", 0, 2, str2T, reT);
m_sigs[OP_REGEXP_LOOP] = alloc(psig, m, "re.loop", 0, 2, strTint2T, reT); // maybe 3 arguments.
}
void seq_decl_plugin::set_manager(ast_manager* m, family_id id) {
decl_plugin::set_manager(m, id);
m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, STRING_SORT, 0, (parameter const*)0));
m_char = m->mk_sort(symbol("Char"), sort_info(m_family_id, CHAR_SORT, 0, (parameter const*)0));
m->inc_ref(m_char);
parameter param(m_char);
m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, SEQ_SORT, 1, &param));
m->inc_ref(m_string);
}
@ -249,6 +247,9 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
if (!parameters[0].is_ast() || !is_sort(parameters[0].get_ast())) {
m.raise_exception("invalid sequence sort, parameter is not a sort");
}
if (parameters[0].get_ast() == m_char) {
return m_string;
}
return m.mk_sort(symbol("Seq"), sort_info(m_family_id, SEQ_SORT, num_parameters, parameters));
case RE_SORT:
if (num_parameters != 1) {
@ -260,6 +261,8 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters));
case STRING_SORT:
return m_string;
case CHAR_SORT:
return m_char;
default:
UNREACHABLE();
return 0;
@ -274,12 +277,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
switch(k) {
case OP_SEQ_UNIT:
case OP_SEQ_EMPTY:
case OP_SEQ_CONS:
case OP_SEQ_REV_CONS:
case OP_SEQ_HEAD:
case OP_SEQ_TAIL:
case OP_SEQ_LAST:
case OP_SEQ_FIRST:
case OP_SEQ_PREFIX_OF:
case OP_SEQ_SUFFIX_OF:
case OP_SEQ_SUBSEQ_OF:
@ -289,9 +286,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
case OP_RE_OPTION:
case OP_RE_RANGE:
case OP_RE_UNION:
case OP_RE_INTERSECT:
case OP_RE_DIFFERENCE:
case OP_RE_COMPLEMENT:
case OP_RE_EMPTY_SEQ:
case OP_RE_EMPTY_SET:
case OP_RE_OF_SEQ:
@ -317,15 +311,28 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
return m.mk_const_decl(m_stringc_sym, m_string,
func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters));
case OP_SEQ_CONCAT:
case OP_RE_CONCAT:
case OP_REGEXP_CONCAT:
case OP_STRING_CONCAT: {
case OP_SEQ_CONCAT: {
match_left_assoc(*m_sigs[k], arity, domain, range, rng);
func_decl_info info(m_family_id, k);
info.set_left_associative();
if (rng == m_string) {
return m.mk_func_decl(m_sigs[_OP_STRING_CONCAT]->m_name, rng, rng, rng, info);
}
return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info);
}
case OP_RE_CONCAT: {
match_left_assoc(*m_sigs[k], arity, domain, range, rng);
func_decl_info info(m_family_id, k);
info.set_left_associative();
return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info);
}
case _OP_STRING_CONCAT: {
match_left_assoc(*m_sigs[k], arity, domain, range, rng);
func_decl_info info(m_family_id, OP_SEQ_CONCAT);
info.set_left_associative();
return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info);
}
case OP_STRING_LENGTH:
case OP_STRING_SUBSTR:
@ -339,12 +346,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
case OP_STRING_STOI:
case OP_STRING_IN_REGEXP:
case OP_STRING_TO_REGEXP:
case OP_REGEXP_UNION:
case OP_REGEXP_INTER:
case OP_REGEXP_STAR:
case OP_REGEXP_PLUS:
case OP_REGEXP_OPT:
case OP_REGEXP_RANGE:
case OP_REGEXP_LOOP:
match(*m_sigs[k], arity, domain, range, rng);
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));

45
src/ast/seq_decl_plugin.h
View file

@ -25,19 +25,14 @@ Revision History:
enum seq_sort_kind {
SEQ_SORT,
RE_SORT,
STRING_SORT
STRING_SORT,
CHAR_SORT
};
enum seq_op_kind {
OP_SEQ_UNIT,
OP_SEQ_EMPTY,
OP_SEQ_CONCAT,
OP_SEQ_CONS,
OP_SEQ_REV_CONS,
OP_SEQ_HEAD,
OP_SEQ_TAIL,
OP_SEQ_LAST,
OP_SEQ_FIRST,
OP_SEQ_PREFIX_OF,
OP_SEQ_SUFFIX_OF,
OP_SEQ_SUBSEQ_OF,
@ -52,8 +47,6 @@ enum seq_op_kind {
OP_RE_CONCAT,
OP_RE_UNION,
OP_RE_INTERSECT,
OP_RE_COMPLEMENT,
OP_RE_DIFFERENCE,
OP_RE_LOOP,
OP_RE_EMPTY_SET,
OP_RE_FULL_SET,
@ -65,7 +58,7 @@ enum seq_op_kind {
// string specific operators.
OP_STRING_CONST,
OP_STRING_CONCAT,
_OP_STRING_CONCAT,
OP_STRING_LENGTH,
OP_STRING_SUBSTR,
OP_STRING_STRCTN,
@ -78,13 +71,6 @@ enum seq_op_kind {
OP_STRING_STOI,
OP_STRING_IN_REGEXP,
OP_STRING_TO_REGEXP,
OP_REGEXP_CONCAT,
OP_REGEXP_UNION,
OP_REGEXP_INTER,
OP_REGEXP_STAR,
OP_REGEXP_PLUS,
OP_REGEXP_OPT,
OP_REGEXP_RANGE,
OP_REGEXP_LOOP,
LAST_SEQ_OP
@ -112,6 +98,7 @@ class seq_decl_plugin : public decl_plugin {
bool m_init;
symbol m_stringc_sym;
sort* m_string;
sort* m_char;
void match(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng);
@ -148,6 +135,8 @@ public:
virtual bool is_unique_value(app * e) const { return is_value(e); }
bool is_char(ast* a) const { return a == m_char; }
app* mk_string(symbol const& s);
};
@ -159,6 +148,9 @@ public:
ast_manager& get_manager() const { return m; }
bool is_string(sort* s) const { return is_seq(s) && seq.is_char(s->get_parameter(0).get_ast()); }
bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); }
class str {
seq_util& u;
ast_manager& m;
@ -169,7 +161,7 @@ public:
app* mk_string(symbol const& 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_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_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); }
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); }
@ -183,8 +175,7 @@ public:
return is_const(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), 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_concat(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_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); }
@ -222,13 +213,13 @@ 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_concat(expr const* n) const { return is_app_of(n, m_fid, OP_RE_CONCAT); }
bool is_union(expr const* n) const { return is_app_of(n, m_fid, OP_RE_UNION); }
bool is_inter(expr const* n) const { return is_app_of(n, m_fid, OP_RE_INTERSECT); }
bool is_star(expr const* n) const { return is_app_of(n, m_fid, OP_RE_STAR); }
bool is_plus(expr const* n) const { return is_app_of(n, m_fid, OP_RE_PLUS); }
bool is_opt(expr const* n) const { return is_app_of(n, m_fid, OP_RE_OPTION); }
bool is_range(expr const* n) const { return is_app_of(n, m_fid, OP_RE_RANGE); }
bool is_loop(expr const* n) const { return is_app_of(n, m_fid, OP_REGEXP_LOOP); }
MATCH_UNARY(is_to_regexp);

6
src/smt/theory_seq_empty.h
View file

@ -42,13 +42,13 @@ namespace smt {
}
virtual expr* get_some_value(sort* s) {
if (u.str.is_string(s))
if (u.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)) {
if (u.is_string(s)) {
v1 = u.str.mk_string("a");
v2 = u.str.mk_string("b");
return true;
@ -57,7 +57,7 @@ namespace smt {
return false;
}
virtual expr* get_fresh_value(sort* s) {
if (u.str.is_string(s)) {
if (u.is_string(s)) {
while (true) {
std::ostringstream strm;
strm << "S" << m_next++;