mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
03d1391ded
commit
e7687132ed
|
@ -40,13 +40,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
case OP_RE_LOOP:
|
||||
case OP_RE_EMPTY_SET:
|
||||
case OP_RE_FULL_SET:
|
||||
case OP_RE_EMPTY_SEQ:
|
||||
case OP_RE_OF_PRED:
|
||||
return BR_FAILED;
|
||||
|
||||
// string specific operators.
|
||||
case OP_STRING_CONST:
|
||||
return BR_FAILED;
|
||||
|
||||
case OP_SEQ_CONCAT:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_seq_concat(args[0], args[1], result);
|
||||
|
@ -62,26 +58,31 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
|
|||
case OP_SEQ_AT:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_str_at(args[0], args[1], result);
|
||||
case OP_STRING_STRIDOF:
|
||||
SASSERT(num_args == 3);
|
||||
return mk_str_stridof(args[0], args[1], args[2], result);
|
||||
case OP_STRING_STRREPL:
|
||||
SASSERT(num_args == 3);
|
||||
return mk_str_strrepl(args[0], args[1], args[2], result);
|
||||
case OP_SEQ_PREFIX:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_seq_prefix(args[0], args[1], result);
|
||||
case OP_SEQ_SUFFIX:
|
||||
SASSERT(num_args == 2);
|
||||
return mk_seq_suffix(args[0], args[1], result);
|
||||
case OP_SEQ_TO_RE:
|
||||
return BR_FAILED;
|
||||
case OP_SEQ_IN_RE:
|
||||
return BR_FAILED;
|
||||
|
||||
case OP_STRING_CONST:
|
||||
return BR_FAILED;
|
||||
case OP_STRING_STRIDOF:
|
||||
SASSERT(num_args == 3);
|
||||
return mk_str_stridof(args[0], args[1], args[2], result);
|
||||
case OP_STRING_STRREPL:
|
||||
SASSERT(num_args == 3);
|
||||
return mk_str_strrepl(args[0], args[1], args[2], result);
|
||||
case OP_STRING_ITOS:
|
||||
SASSERT(num_args == 1);
|
||||
return mk_str_itos(args[0], result);
|
||||
case OP_STRING_STOI:
|
||||
SASSERT(num_args == 1);
|
||||
return mk_str_stoi(args[0], result);
|
||||
case OP_SEQ_TO_RE:
|
||||
case OP_SEQ_IN_RE:
|
||||
case OP_REGEXP_LOOP:
|
||||
return BR_FAILED;
|
||||
case _OP_STRING_CONCAT:
|
||||
|
@ -140,7 +141,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
|
|||
m_es.reset();
|
||||
m_util.str.get_concat(a, m_es);
|
||||
size_t len = 0;
|
||||
size_t j = 0;
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < m_es.size(); ++i) {
|
||||
if (m_util.str.is_string(m_es[i], b)) {
|
||||
len += b.length();
|
||||
|
@ -154,7 +155,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
|
|||
result = m_autil.mk_numeral(rational(len, rational::ui64()), true);
|
||||
return BR_DONE;
|
||||
}
|
||||
if (j != m_es.size()) {
|
||||
if (j != m_es.size() || j != 1) {
|
||||
expr_ref_vector es(m());
|
||||
for (unsigned i = 0; i < j; ++i) {
|
||||
es.push_back(m_util.str.mk_length(m_es[i]));
|
||||
|
|
|
@ -186,28 +186,27 @@ void seq_decl_plugin::init() {
|
|||
sort* seqAintT[2] = { seqA, 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.++", 1, 2, seqAseqA, seqA);
|
||||
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] = alloc(psig, m, "seq.prefixof", 1, 2, seqAseqA, boolT);
|
||||
m_sigs[OP_SEQ_SUFFIX] = alloc(psig, m, "seq.suffixof", 1, 2, seqAseqA, boolT);
|
||||
m_sigs[OP_SEQ_CONTAINS] = alloc(psig, m, "seq.contains", 1, 2, seqAseqA, boolT);
|
||||
m_sigs[OP_SEQ_EXTRACT] = alloc(psig, m, "seq.extract", 1, 3, seqAint2T, seqA);
|
||||
m_sigs[OP_SEQ_AT] = alloc(psig, m, "seq.at", 1, 2, seqAintT, seqA);
|
||||
m_sigs[OP_SEQ_LENGTH] = alloc(psig, m, "seq-length", 1, 1, &seqA, intT);
|
||||
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_SEQ_EXTRACT] = alloc(psig, m, "seq.extract", 1, 3, seqAint2T, seqA);
|
||||
m_sigs[OP_SEQ_AT] = alloc(psig, m, "seq.at", 1, 2, seqAintT, seqA);
|
||||
m_sigs[OP_SEQ_LENGTH] = alloc(psig, m, "seq.len", 1, 1, &seqA, intT);
|
||||
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);
|
||||
m_sigs[OP_RE_FULL_SET] = alloc(psig, m, "re-full-set", 1, 0, 0, reA);
|
||||
m_sigs[OP_SEQ_TO_RE] = alloc(psig, m, "seq.to.re", 1, 1, &seqA, reA);
|
||||
m_sigs[OP_RE_OF_PRED] = alloc(psig, m, "re-of-pred", 1, 1, &predA, reA);
|
||||
m_sigs[OP_SEQ_TO_RE] = alloc(psig, m, "seq.to.re", 1, 1, &seqA, reA);
|
||||
m_sigs[OP_SEQ_IN_RE] = alloc(psig, m, "seq.in.re", 1, 2, seqAreA, boolT);
|
||||
m_sigs[OP_STRING_CONST] = 0;
|
||||
m_sigs[OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT);
|
||||
|
|
|
@ -54,7 +54,6 @@ enum seq_op_kind {
|
|||
OP_RE_LOOP,
|
||||
OP_RE_EMPTY_SET,
|
||||
OP_RE_FULL_SET,
|
||||
OP_RE_EMPTY_SEQ,
|
||||
OP_RE_OF_PRED,
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue