mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-12-11 17:48:50 +00:00
commit ea353d77e9
23 changed files with 936 additions and 272 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/arith_decl_plugin.h
View file

@ -328,6 +328,9 @@ public:
app * mk_numeral(sexpr const * p, unsigned i) {
return plugin().mk_numeral(p, i);
}
app * mk_int(int i) {
return mk_numeral(rational(i), true);
}
app * mk_le(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LE, arg1, arg2); }
app * mk_ge(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GE, arg1, arg2); }
app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LT, arg1, arg2); }

1
src/ast/normal_forms/nnf.cpp
View file

@ -708,6 +708,7 @@ struct nnf::imp {
}
bool process_app(app * t, frame & fr) {
TRACE("nnf", tout << mk_ismt2_pp(t, m()) << "\n";);
SASSERT(m().is_bool(t));
if (t->get_family_id() == m().get_basic_family_id()) {
switch (static_cast<basic_op_kind>(t->get_decl_kind())) {

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

@ -55,22 +55,33 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
return mk_seq_concat(args[0], args[1], result);
case OP_SEQ_LENGTH:
SASSERT(num_args == 1);
return mk_str_length(args[0], result);
return mk_seq_length(args[0], result);
case OP_SEQ_EXTRACT:
SASSERT(num_args == 3);
return mk_str_substr(args[0], args[1], args[2], result);
return mk_seq_extract(args[0], args[1], args[2], result);
case OP_SEQ_CONTAINS:
SASSERT(num_args == 2);
return mk_str_strctn(args[0], args[1], result);
return mk_seq_contains(args[0], args[1], result);
case OP_SEQ_AT:
SASSERT(num_args == 2);
return mk_str_at(args[0], args[1], result);
return mk_seq_at(args[0], args[1], 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_INDEX:
if (num_args == 2) {
expr_ref arg3(m_autil.mk_int(0), m());
result = m_util.str.mk_index(args[0], args[1], arg3);
return BR_REWRITE1;
}
SASSERT(num_args == 3);
return mk_seq_index(args[0], args[1], args[2], result);
case OP_SEQ_REPLACE:
SASSERT(num_args == 3);
return mk_seq_replace(args[0], args[1], args[2], result);
case OP_SEQ_TO_RE:
return BR_FAILED;
case OP_SEQ_IN_RE:
@ -78,12 +89,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
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);
@ -101,7 +106,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case _OP_STRING_IN_REGEXP:
case _OP_STRING_TO_REGEXP:
case _OP_STRING_SUBSTR:
case _OP_STRING_STRREPL:
case _OP_STRING_STRIDOF:
UNREACHABLE();
}
return BR_FAILED;
@ -143,7 +149,7 @@ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
return BR_FAILED;
}
br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) {
std::string b;
m_es.reset();
m_util.str.get_concat(a, m_es);
@ -153,6 +159,12 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
if (m_util.str.is_string(m_es[i], b)) {
len += b.length();
}
else if (m_util.str.is_unit(m_es[i])) {
len += 1;
}
else if (m_util.str.is_empty(m_es[i])) {
// skip
}
else {
m_es[j] = m_es[i];
++j;
@ -176,7 +188,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
return BR_FAILED;
}
br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result) {
br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result) {
std::string s;
rational pos, len;
if (m_util.str.is_string(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) &&
@ -188,22 +200,22 @@ br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& resul
}
return BR_FAILED;
}
br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) {
br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
std::string c, d;
if (m_util.str.is_string(a, c) && m_util.str.is_string(b, d)) {
result = m().mk_bool_val(0 != strstr(d.c_str(), c.c_str()));
result = m().mk_bool_val(0 != strstr(c.c_str(), d.c_str()));
return BR_DONE;
}
// check if subsequence of a is in b.
// check if subsequence of b is in a.
ptr_vector<expr> as, bs;
m_util.str.get_concat(a, as);
m_util.str.get_concat(b, bs);
bool found = false;
for (unsigned i = 0; !found && i < bs.size(); ++i) {
if (as.size() > bs.size() - i) break;
for (unsigned i = 0; !found && i < as.size(); ++i) {
if (bs.size() > as.size() - i) break;
unsigned j = 0;
for (; j < as.size() && as[j] == bs[i+j]; ++j) {};
found = j == as.size();
for (; j < bs.size() && as[j] == bs[i+j]; ++j) {};
found = j == bs.size();
}
if (found) {
result = m().mk_true();
@ -212,7 +224,7 @@ br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) {
return BR_FAILED;
}
br_status seq_rewriter::mk_str_at(expr* a, expr* b, expr_ref& result) {
br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
std::string c;
rational r;
if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r) && r.is_unsigned()) {
@ -228,7 +240,7 @@ br_status seq_rewriter::mk_str_at(expr* a, expr* b, expr_ref& result) {
return BR_FAILED;
}
br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& result) {
br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result) {
std::string s1, s2;
rational r;
bool isc1 = m_util.str.is_string(a, s1);
@ -249,7 +261,7 @@ br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& resu
return BR_DONE;
}
if (m_util.str.is_empty(b)) {
if (m_util.str.is_empty(b) && m_autil.is_numeral(c, r) && r.is_zero()) {
result = c;
return BR_DONE;
}
@ -257,15 +269,17 @@ br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& resu
return BR_FAILED;
}
br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result) {
br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result) {
std::string s1, s2, s3;
if (m_util.str.is_string(a, s1) && m_util.str.is_string(b, s2) &&
m_util.str.is_string(c, s3)) {
std::ostringstream buffer;
bool can_replace = true;
for (size_t i = 0; i < s1.length(); ) {
if (strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) {
if (can_replace && strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) {
buffer << s3;
i += s2.length();
can_replace = false;
}
else {
buffer << s1[i];
@ -367,6 +381,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
return BR_REWRITE3;
}
if (i > 0) {
SASSERT(i < as.size() && i < bs.size());
a = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i);
b = m_util.str.mk_concat(bs.size() - i, bs.c_ptr() + i);
result = m_util.str.mk_prefix(a, b);
@ -644,54 +659,127 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve
}
bool is_sat;
if (!change) {
if (is_subsequence(m_lhs.size(), m_lhs.c_ptr(), m_rhs.size(), m_rhs.c_ptr(), lhs, rhs, is_sat)) {
return is_sat;
}
unsigned szl = m_lhs.size() - head1, szr = m_rhs.size() - head2;
expr* const* ls = m_lhs.c_ptr() + head1, * const*rs = m_rhs.c_ptr() + head2;
if (length_constrained(szl, ls, szr, rs, lhs, rhs, is_sat)) {
return is_sat;
}
if (is_subsequence(szl, ls, szr, rs, lhs, rhs, is_sat)) {
return is_sat;
}
if (szl == 0 && szr == 0) {
return true;
}
else if (!change) {
lhs.push_back(l);
rhs.push_back(r);
}
else if (head1 == m_lhs.size() && head2 == m_rhs.size()) {
// skip
}
else if (head1 == m_lhs.size()) {
return set_empty(m_rhs.size() - head2, m_rhs.c_ptr() + head2, lhs, rhs);
}
else if (head2 == m_rhs.size()) {
return set_empty(m_lhs.size() - head1, m_lhs.c_ptr() + head1, lhs, rhs);
}
else { // could solve if either side is fixed size.
SASSERT(head1 < m_lhs.size() && head2 < m_rhs.size());
if (is_subsequence(m_lhs.size() - head1, m_lhs.c_ptr() + head1,
m_rhs.size() - head2, m_rhs.c_ptr() + head2, lhs, rhs, is_sat)) {
return is_sat;
}
else {
// could solve if either side is fixed size.
SASSERT(szl > 0 && szr > 0);
lhs.push_back(m_util.str.mk_concat(m_lhs.size() - head1, m_lhs.c_ptr() + head1));
rhs.push_back(m_util.str.mk_concat(m_rhs.size() - head2, m_rhs.c_ptr() + head2));
lhs.push_back(m_util.str.mk_concat(szl, ls));
rhs.push_back(m_util.str.mk_concat(szr, rs));
}
return true;
}
bool seq_rewriter::set_empty(unsigned sz, expr* const* es, expr_ref_vector& lhs, expr_ref_vector& rhs) {
expr* seq_rewriter::concat_non_empty(unsigned n, expr* const* as) {
SASSERT(n > 0);
ptr_vector<expr> bs;
for (unsigned i = 0; i < n; ++i) {
if (m_util.str.is_unit(as[i]) ||
m_util.str.is_string(as[i])) {
bs.push_back(as[i]);
}
}
if (bs.empty()) {
return m_util.str.mk_empty(m().get_sort(as[0]));
}
else {
return m_util.str.mk_concat(bs.size(), bs.c_ptr());
}
}
bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs) {
std::string s;
for (unsigned i = 0; i < sz; ++i) {
if (m_util.str.is_unit(es[i])) {
return false;
if (all) return false;
}
if (m_util.str.is_empty(es[i])) {
else if (m_util.str.is_empty(es[i])) {
continue;
}
if (m_util.str.is_string(es[i], s)) {
SASSERT(s.length() > 0);
return false;
else if (m_util.str.is_string(es[i], s)) {
if (all) {
SASSERT(s.length() > 0);
return false;
}
}
else {
lhs.push_back(m_util.str.mk_empty(m().get_sort(es[i])));
rhs.push_back(es[i]);
}
lhs.push_back(m_util.str.mk_empty(m().get_sort(es[i])));
rhs.push_back(es[i]);
}
return true;
}
bool seq_rewriter::min_length(unsigned n, expr* const* es, size_t& len) {
std::string s;
bool bounded = true;
len = 0;
for (unsigned i = 0; i < n; ++i) {
if (m_util.str.is_unit(es[i])) {
++len;
}
else if (m_util.str.is_empty(es[i])) {
continue;
}
else if (m_util.str.is_string(es[i], s)) {
len += s.length();
}
else {
bounded = false;
}
}
return bounded;
}
bool seq_rewriter::length_constrained(unsigned szl, expr* const* l, unsigned szr, expr* const* r,
expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) {
is_sat = true;
size_t len1 = 0, len2 = 0;
bool bounded1 = min_length(szl, l, len1);
bool bounded2 = min_length(szr, r, len2);
if (bounded1 && len1 < len2) {
is_sat = false;
return true;
}
if (bounded2 && len2 < len1) {
is_sat = false;
return true;
}
if (bounded1 && len1 == len2 && len1 > 0) {
is_sat = set_empty(szr, r, false, lhs, rhs);
if (is_sat) {
lhs.push_back(concat_non_empty(szl, l));
rhs.push_back(concat_non_empty(szr, r));
}
return true;
}
if (bounded2 && len1 == len2 && len1 > 0) {
is_sat = set_empty(szl, l, false, lhs, rhs);
if (is_sat) {
lhs.push_back(concat_non_empty(szl, l));
rhs.push_back(concat_non_empty(szr, r));
}
return true;
}
return false;
}
bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, expr* const* r,
expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) {
is_sat = true;
@ -720,13 +808,15 @@ bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, ex
if (rpos.contains(j)) {
rs.push_back(r[j]);
}
else if (!set_empty(1, r + j, lhs, rhs)) {
else if (!set_empty(1, r + j, true, lhs, rhs)) {
is_sat = false;
return true;
}
}
SASSERT(szl == rs.size());
lhs.push_back(m_util.str.mk_concat(szl, l));
rhs.push_back(m_util.str.mk_concat(szl, rs.c_ptr()));
if (szl > 0) {
lhs.push_back(m_util.str.mk_concat(szl, l));
rhs.push_back(m_util.str.mk_concat(szl, rs.c_ptr()));
}
return true;
}

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

@ -35,12 +35,12 @@ class seq_rewriter {
ptr_vector<expr> m_es, m_lhs, m_rhs;
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);
br_status mk_str_at(expr* a, expr* b, expr_ref& result);
br_status mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& result);
br_status mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result);
br_status mk_seq_length(expr* a, expr_ref& result);
br_status mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result);
br_status mk_seq_contains(expr* a, expr* b, expr_ref& result);
br_status mk_seq_at(expr* a, expr* b, expr_ref& result);
br_status mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result);
br_status mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result);
br_status mk_seq_prefix(expr* a, expr* b, expr_ref& result);
br_status mk_seq_suffix(expr* a, expr* b, expr_ref& result);
br_status mk_str_itos(expr* a, expr_ref& result);
@ -53,9 +53,14 @@ class seq_rewriter {
br_status mk_re_plus(expr* a, expr_ref& result);
br_status mk_re_opt(expr* a, expr_ref& result);
bool set_empty(unsigned sz, expr* const* es, expr_ref_vector& lhs, expr_ref_vector& rhs);
bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs);
bool is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r,
expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat);
bool length_constrained(unsigned n, expr* const* l, unsigned m, expr* const* r,
expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat);
bool min_length(unsigned n, expr* const* es, size_t& len);
expr* concat_non_empty(unsigned n, expr* const* es);
public:
seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m), m_autil(m) {

107
src/ast/seq_decl_plugin.cpp
View file

@ -90,6 +90,7 @@ void seq_decl_plugin::match_left_assoc(psig& sig, unsigned dsz, sort *const* dom
}
bool is_match = true;
for (unsigned i = 0; is_match && i < dsz; ++i) {
SASSERT(dom[i]);
is_match = match(binding, dom[i], sig.m_dom[0].get());
}
if (range && is_match) {
@ -102,6 +103,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);
SASSERT(range_out);
TRACE("seq_verbose", tout << mk_pp(range_out, m) << "\n";);
}
@ -134,6 +136,7 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran
m.raise_exception(strm.str().c_str());
}
range_out = apply_binding(binding, sig.m_range);
SASSERT(range_out);
}
sort* seq_decl_plugin::apply_binding(ptr_vector<sort> const& binding, sort* s) {
@ -177,6 +180,7 @@ void seq_decl_plugin::init() {
sort* reAreA[2] = { reA, reA };
sort* AA[2] = { A, A };
sort* seqAint2T[3] = { seqA, intT, intT };
sort* seq2AintT[3] = { seqA, seqA, intT };
sort* str2T[2] = { strT, strT };
sort* str3T[3] = { strT, strT, strT };
sort* strTint2T[3] = { strT, intT, intT };
@ -184,6 +188,7 @@ void seq_decl_plugin::init() {
sort* strTreT[2] = { strT, reT };
sort* str2TintT[3] = { strT, strT, intT };
sort* seqAintT[2] = { seqA, intT };
sort* seq3A[3] = { seqA, seqA, seqA };
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);
@ -193,6 +198,8 @@ void seq_decl_plugin::init() {
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_REPLACE] = alloc(psig, m, "seq.replace", 1, 3, seq3A, seqA);
m_sigs[OP_SEQ_INDEX] = alloc(psig, m, "seq.indexof", 1, 3, seq2AintT, intT);
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);
@ -209,8 +216,8 @@ void seq_decl_plugin::init() {
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);
m_sigs[OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT);
m_sigs[_OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT);
m_sigs[_OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT);
m_sigs[OP_STRING_ITOS] = alloc(psig, m, "int.to.str", 0, 1, &intT, strT);
m_sigs[OP_STRING_STOI] = alloc(psig, m, "str.to.int", 0, 1, &strT, intT);
m_sigs[OP_REGEXP_LOOP] = alloc(psig, m, "re.loop", 0, 2, strTint2T, reT); // maybe 3 arguments.
@ -222,7 +229,7 @@ void seq_decl_plugin::init() {
m_sigs[_OP_STRING_SUFFIX] = alloc(psig, m, "str.suffixof", 0, 2, str2T, boolT);
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_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, boolT);
m_sigs[_OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, strT);
}
void seq_decl_plugin::set_manager(ast_manager* m, family_id id) {
@ -282,6 +289,18 @@ func_decl* seq_decl_plugin::mk_str_fun(decl_kind k, unsigned arity, sort* const*
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k_seq));
}
func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq, decl_kind k_string) {
ast_manager& m = *m_manager;
sort_ref rng(m);
if (arity == 0) {
m.raise_exception("Invalid function application. At least one argument expected");
}
match_left_assoc(*m_sigs[k], arity, domain, range, rng);
func_decl_info info(m_family_id, k_seq);
info.set_left_associative();
return m.mk_func_decl(m_sigs[(rng == m_string)?k_string:k_seq]->m_name, rng, rng, rng, info);
}
func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
init();
@ -301,18 +320,21 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
case OP_RE_STAR:
case OP_RE_OPTION:
case OP_RE_RANGE:
case OP_RE_UNION:
case OP_RE_EMPTY_SET:
case OP_RE_OF_PRED:
case OP_STRING_ITOS:
case OP_STRING_STOI:
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));
case OP_RE_LOOP:
match(*m_sigs[k], arity, domain, range, rng);
if (num_parameters != 2 || !parameters[0].is_int() || !parameters[1].is_int()) {
m.raise_exception("Expecting two numeral parameters to function re-loop");
}
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters));
case OP_STRING_CONST:
if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) {
m.raise_exception("invalid string declaration");
@ -320,33 +342,40 @@ 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: {
if (arity == 0) {
m.raise_exception("invalid concatenation. At least one argument expected");
case OP_RE_UNION:
return mk_assoc_fun(k, arity, domain, range, k, k);
case OP_RE_CONCAT:
return mk_assoc_fun(k, arity, domain, range, k, k);
case OP_SEQ_CONCAT:
return mk_assoc_fun(k, arity, domain, range, k, _OP_STRING_CONCAT);
case _OP_STRING_CONCAT:
return mk_assoc_fun(k, arity, domain, range, OP_SEQ_CONCAT, k);
case OP_SEQ_REPLACE:
return mk_seq_fun(k, arity, domain, range, _OP_STRING_STRREPL);
case _OP_STRING_STRREPL:
return mk_str_fun(k, arity, domain, range, OP_SEQ_REPLACE);
case OP_SEQ_INDEX:
if (arity == 2) {
sort* dom[3] = { domain[0], domain[1], arith_util(m).mk_int() };
sort_ref rng(m);
match(*m_sigs[k], 3, dom, range, rng);
return m.mk_func_decl(m_sigs[(dom[0] == m_string)?_OP_STRING_STRIDOF:k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
}
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[(rng == m_string)?_OP_STRING_CONCAT:k]->m_name, rng, rng, rng, info);
}
case OP_RE_CONCAT: {
if (arity == 0) {
m.raise_exception("invalid concatenation. At least one argument expected");
return mk_seq_fun(k, arity, domain, range, _OP_STRING_STRIDOF);
case _OP_STRING_STRIDOF:
if (arity == 2) {
sort* dom[3] = { domain[0], domain[1], arith_util(m).mk_int() };
sort_ref rng(m);
match(*m_sigs[k], 3, dom, range, rng);
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, OP_SEQ_INDEX));
}
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: {
if (arity == 0) {
m.raise_exception("invalid concatenation. At least one argument expected");
}
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);
}
return mk_str_fun(k, arity, domain, range, OP_SEQ_INDEX);
case OP_SEQ_PREFIX:
return mk_seq_fun(k, arity, domain, range, _OP_STRING_PREFIX);
case _OP_STRING_PREFIX:
@ -387,16 +416,13 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
case _OP_STRING_SUBSTR:
return mk_str_fun(k, arity, domain, range, OP_SEQ_EXTRACT);
case OP_STRING_STRIDOF:
case OP_STRING_STRREPL:
case OP_STRING_ITOS:
case OP_STRING_STOI:
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));
case _OP_SEQ_SKOLEM:
return m.mk_func_decl(symbol("seq.skolem"), arity, domain, rng, func_decl_info(m_family_id, k));
case _OP_SEQ_SKOLEM: {
if (num_parameters != 1 || !parameters[0].is_symbol()) {
m.raise_exception("one symbol parameter expected to skolem symbol");
}
symbol s = parameters[0].get_symbol();
return m.mk_func_decl(s, arity, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters));
}
default:
UNREACHABLE();
return 0;
@ -431,6 +457,7 @@ bool seq_decl_plugin::is_value(app* e) const {
}
app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) {
SASSERT(range);
parameter param(name);
func_decl* f = m.mk_func_decl(get_family_id(), _OP_SEQ_SKOLEM, 1, &param, n, args, range);
return m.mk_app(f, n, args);

32
src/ast/seq_decl_plugin.h
View file

@ -39,8 +39,10 @@ enum seq_op_kind {
OP_SEQ_SUFFIX,
OP_SEQ_CONTAINS,
OP_SEQ_EXTRACT,
OP_SEQ_REPLACE,
OP_SEQ_AT,
OP_SEQ_LENGTH,
OP_SEQ_LENGTH,
OP_SEQ_INDEX,
OP_SEQ_TO_RE,
OP_SEQ_IN_RE,
@ -59,12 +61,11 @@ enum seq_op_kind {
// string specific operators.
OP_STRING_CONST,
OP_STRING_STRIDOF, // TBD generalize
OP_STRING_STRREPL, // TBD generalize
OP_STRING_ITOS,
OP_STRING_STOI,
OP_REGEXP_LOOP, // TBD re-loop: integers as parameters or arguments?
// internal only operators. Converted to SEQ variants.
_OP_STRING_STRREPL,
_OP_STRING_CONCAT,
_OP_STRING_LENGTH,
_OP_STRING_STRCTN,
@ -74,6 +75,7 @@ enum seq_op_kind {
_OP_STRING_TO_REGEXP,
_OP_STRING_CHARAT,
_OP_STRING_SUBSTR,
_OP_STRING_STRIDOF,
_OP_SEQ_SKOLEM,
LAST_SEQ_OP
};
@ -114,6 +116,7 @@ class seq_decl_plugin : public decl_plugin {
func_decl* mk_seq_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string);
func_decl* mk_str_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq);
func_decl* mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq);
void init();
@ -156,8 +159,10 @@ public:
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); }
bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); }
bool is_re(sort* s, sort*& seq) const { return is_sort_of(s, m_fid, RE_SORT) && (seq = to_sort(s->get_parameter(0).get_ast()), true); }
bool is_seq(expr* e) const { return is_seq(m.get_sort(e)); }
bool is_re(expr* e) const { return is_re(m.get_sort(e)); }
bool is_re(expr* e, sort*& seq) const { return is_re(m.get_sort(e), seq); }
app* mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range);
bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); }
@ -175,12 +180,16 @@ public:
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_SEQ_CONCAT, 2, es); }
app* mk_concat(expr* a, expr* b, expr* c) {
return mk_concat(mk_concat(a, b), c);
}
expr* mk_concat(unsigned n, expr* const* es) { if (n == 1) return es[0]; SASSERT(n > 1); return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); }
app* mk_length(expr* a) { return m.mk_app(m_fid, OP_SEQ_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_SEQ_EXTRACT, 3, es); }
app* mk_contains(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); }
app* mk_prefix(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_PREFIX, 2, es); }
app* mk_suffix(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_SUFFIX, 2, es); }
app* mk_index(expr* a, expr* b, expr* i) { expr* es[3] = { a, b, i}; return m.mk_app(m_fid, OP_SEQ_INDEX, 3, es); }
bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
@ -200,8 +209,8 @@ public:
bool is_extract(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_EXTRACT); }
bool is_contains(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONTAINS); }
bool is_at(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_AT); }
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_index(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_INDEX); }
bool is_replace(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_REPLACE); }
bool is_prefix(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_PREFIX); }
bool is_suffix(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_SUFFIX); }
bool is_itos(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_ITOS); }
@ -215,8 +224,8 @@ public:
MATCH_TERNARY(is_extract);
MATCH_BINARY(is_contains);
MATCH_BINARY(is_at);
MATCH_BINARY(is_stridof);
MATCH_BINARY(is_repl);
MATCH_TERNARY(is_index);
MATCH_TERNARY(is_replace);
MATCH_BINARY(is_prefix);
MATCH_BINARY(is_suffix);
MATCH_UNARY(is_itos);
@ -234,6 +243,15 @@ public:
public:
re(seq_util& u): m(u.m), m_fid(u.m_fid) {}
app* mk_to_re(expr* s) { return m.mk_app(m_fid, OP_SEQ_TO_RE, 1, &s); }
app* mk_in_re(expr* s, expr* r) { return m.mk_app(m_fid, OP_SEQ_IN_RE, s, r); }
app* mk_concat(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_CONCAT, r1, r2); }
app* mk_union(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_UNION, r1, r2); }
app* mk_inter(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_INTERSECT, r1, r2); }
app* mk_star(expr* r) { return m.mk_app(m_fid, OP_RE_STAR, r); }
app* mk_plus(expr* r) { return m.mk_app(m_fid, OP_RE_PLUS, r); }
app* mk_opt(expr* r) { return m.mk_app(m_fid, OP_RE_OPTION, r); }
bool is_to_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); }
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); }

6
src/cmd_context/basic_cmds.cpp
View file

@ -222,8 +222,10 @@ ATOMIC_CMD(reset_assertions_cmd, "reset-assertions", "reset all asserted formula
UNARY_CMD(set_logic_cmd, "set-logic", "<symbol>", "set the background logic.", CPK_SYMBOL, symbol const &,
if (ctx.set_logic(arg))
ctx.print_success();
else
ctx.print_unsupported(symbol::null, m_line, m_pos);
else {
std::string msg = "ignoring unsupported logic " + arg.str();
ctx.print_unsupported(symbol(msg.c_str()), m_line, m_pos);
}
);
UNARY_CMD(pp_cmd, "display", "<term>", "display the given term.", CPK_EXPR, expr *, {

15
src/cmd_context/check_logic.cpp
View file

@ -20,6 +20,7 @@ Revision History:
#include"arith_decl_plugin.h"
#include"array_decl_plugin.h"
#include"bv_decl_plugin.h"
#include"seq_decl_plugin.h"
#include"ast_pp.h"
#include"for_each_expr.h"
@ -29,6 +30,7 @@ struct check_logic::imp {
arith_util m_a_util;
bv_util m_bv_util;
array_util m_ar_util;
seq_util m_seq_util;
bool m_uf; // true if the logic supports uninterpreted functions
bool m_arrays; // true if the logic supports arbitrary arrays
bool m_bv_arrays; // true if the logic supports only bv arrays
@ -40,7 +42,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) {
imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m), m_seq_util(m) {
reset();
}
@ -168,6 +170,14 @@ struct check_logic::imp {
m_bvs = true;
m_quantifiers = true;
}
else if (logic == "QF_S") {
m_uf = true;
m_bvs = true;
m_ints = true;
m_arrays = true;
m_reals = true;
m_quantifiers = false;
}
else {
m_unknown_logic = true;
}
@ -419,6 +429,9 @@ struct check_logic::imp {
else if (m.is_builtin_family_id(fid)) {
// nothing to check
}
else if (fid == m_seq_util.get_family_id()) {
// nothing to check
}
else {
fail("logic does not support theory");
}

11
src/cmd_context/cmd_context.cpp
View file

@ -544,6 +544,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
s == "QF_FP" ||
s == "QF_FPBV" ||
s == "QF_BVFP" ||
s == "QF_S" ||
s == "HORN";
}
@ -576,7 +577,7 @@ bool cmd_context::logic_has_bv() const {
}
bool cmd_context::logic_has_seq_core(symbol const& s) const {
return s == "QF_BVRE";
return s == "QF_BVRE" || s == "QF_S";
}
bool cmd_context::logic_has_seq() const {
@ -712,13 +713,7 @@ bool cmd_context::set_logic(symbol const & s) {
if (has_manager() && m_main_ctx)
throw cmd_exception("logic must be set before initialization");
if (!supported_logic(s)) {
if (m_params.m_smtlib2_compliant) {
return false;
}
else {
warning_msg("unknown logic, ignoring set-logic command");
return true;
}
return false;
}
m_logic = s;
if (is_logic("QF_RDL") ||

3
src/smt/proto_model/proto_model.cpp
View file

@ -196,6 +196,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
ptr_buffer<expr> args;
expr * null = static_cast<expr*>(0);
todo.push_back(std::make_pair(e, null));
expr * a;
expr * expanded_a;
@ -254,6 +255,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
if (new_t.get() == 0) {
// t is interpreted or model completion is disabled.
m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t);
TRACE("model_eval", tout << mk_pp(t, m_manager) << " -> " << new_t << "\n";);
trail.push_back(new_t);
if (!is_app(new_t) || to_app(new_t)->get_decl() != f) {
// if the result is not of the form (f ...), then assume we must simplify it.
@ -302,6 +304,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
else {
SASSERT(r1);
trail.push_back(r1);
TRACE("model_eval", tout << mk_pp(a, m_manager) << "\nevaluates to: " << r1 << "\n";);
expr * r2 = 0;
if (!eval_cache.find(r1.get(), r2)) {
todo.back().second = r1;

8
src/smt/smt_context.cpp
View file

@ -312,6 +312,8 @@ namespace smt {
d.m_phase_available = true;
d.m_phase = !l.sign();
TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";);
TRACE("relevancy",
tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(bool_var2expr(l.var())) << "\n";);
if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(bool_var2expr(l.var()))))
m_atom_propagation_queue.push_back(l);
@ -805,8 +807,10 @@ namespace smt {
void context::merge_theory_vars(enode * n2, enode * n1, eq_justification js) {
enode * r2 = n2->get_root();
enode * r1 = n1->get_root();
if (!r1->has_th_vars() && !r2->has_th_vars())
if (!r1->has_th_vars() && !r2->has_th_vars()) {
TRACE("merge_theory_vars", tout << "Neither have theory vars #" << n1->get_owner()->get_id() << " #" << n2->get_owner()->get_id() << "\n";);
return;
}
theory_id from_th = null_theory_id;
@ -821,7 +825,7 @@ namespace smt {
theory_var v2 = m_fparams.m_new_core2th_eq ? get_closest_var(n2, t2) : r2->m_th_var_list.get_th_var();
theory_var v1 = m_fparams.m_new_core2th_eq ? get_closest_var(n1, t1) : r1->m_th_var_list.get_th_var();
TRACE("merge_theory_vars",
tout << "v2: " << v2 << " #" << r1->get_owner_id() << ", v1: " << v1 << " #" << r2->get_owner_id()
tout << "v2: " << v2 << " #" << r2->get_owner_id() << ", v1: " << v1 << " #" << r1->get_owner_id()
<< ", t2: " << t2 << ", t1: " << t1 << "\n";);
if (v2 != null_theory_var && v1 != null_theory_var) {
if (t1 == t2) {

10
src/smt/smt_model_finder.cpp
View file

@ -1744,7 +1744,7 @@ namespace smt {
// when the quantifier is satisfied by a macro/hint, it may not be processed by the AUF solver.
// in this case, the quantifier_info stores the instantiation sets.
ptr_vector<instantiation_set> * m_uvar_inst_sets;
bool m_cancel;
volatile bool m_cancel;
friend class quantifier_analyzer;
@ -1893,8 +1893,10 @@ namespace smt {
(*it)->populate_inst_sets(m_flat_q, s, ctx);
// second pass
it = m_qinfo_vect.begin();
for (; it != end; ++it)
for (; it != end; ++it) {
checkpoint();
(*it)->populate_inst_sets2(m_flat_q, s, ctx);
}
}
func_decl_set const & get_ng_decls() const {
@ -3593,6 +3595,10 @@ namespace smt {
void model_finder::set_cancel(bool f) {
m_cancel = f;
m_analyzer->set_cancel(f);
obj_map<quantifier, quantifier_info *>::iterator it = m_q2info.begin();
obj_map<quantifier, quantifier_info *>::iterator end = m_q2info.end();
for (; it != end; ++it)
(*it).m_value->set_cancel(f);
}
};

2
src/smt/smt_setup.cpp
View file

@ -815,7 +815,7 @@ namespace smt {
}
void setup::setup_seq() {
m_context.register_plugin(alloc(theory_seq, m_manager));
m_context.register_plugin(alloc(theory_seq_empty, m_manager));
}
void setup::setup_card() {

2
src/smt/smt_theory.h
View file

@ -315,7 +315,7 @@ namespace smt {
}
virtual void display(std::ostream & out) const {
out << "Theory " << static_cast<int>(get_id()) << " does not have a display method\n";
out << "Theory " << static_cast<int>(get_id()) << typeid(*this).name() << " does not have a display method\n";
display_var2enode(out);
}

1
src/smt/theory_arith_pp.h
View file

@ -48,6 +48,7 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::display(std::ostream & out) const {
if (get_num_vars() == 0) return;
out << "Theory arithmetic:\n";
display_vars(out);
display_nl_monomials(out);

3
src/smt/theory_array.cpp
View file

@ -431,8 +431,9 @@ namespace smt {
}
void theory_array::display(std::ostream & out) const {
out << "Theory array:\n";
unsigned num_vars = get_num_vars();
if (num_vars == 0) return;
out << "Theory array:\n";
for (unsigned v = 0; v < num_vars; v++) {
display_var(out, v);
}

3
src/smt/theory_bv.cpp
View file

@ -1586,8 +1586,9 @@ namespace smt {
}
void theory_bv::display(std::ostream & out) const {
out << "Theory bv:\n";
unsigned num_vars = get_num_vars();
if (num_vars == 0) return;
out << "Theory bv:\n";
for (unsigned v = 0; v < num_vars; v++) {
display_var(out, v);
}

3
src/smt/theory_datatype.cpp
View file

@ -522,8 +522,9 @@ namespace smt {
}
void theory_datatype::display(std::ostream & out) const {
out << "Theory datatype:\n";
unsigned num_vars = get_num_vars();
if (num_vars == 0) return;
out << "Theory datatype:\n";
for (unsigned v = 0; v < num_vars; v++)
display_var(out, v);
}

3
src/smt/theory_dl.cpp
View file

@ -194,6 +194,9 @@ namespace smt {
}
}
virtual void display(std::ostream & out) const {
}
private:

12
src/smt/theory_fpa.cpp
View file

@ -921,14 +921,20 @@ namespace smt {
ast_manager & m = get_manager();
context & ctx = get_context();
out << "fpa theory variables:" << std::endl;
bool first = true;
ptr_vector<enode>::const_iterator it = ctx.begin_enodes();
ptr_vector<enode>::const_iterator end = ctx.end_enodes();
for (; it != end; it++) {
theory_var v = (*it)->get_th_var(get_family_id());
if (v != -1) out << v << " -> " <<
mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
if (v != -1) {
if (first) out << "fpa theory variables:" << std::endl;
out << v << " -> " <<
mk_ismt2_pp((*it)->get_owner(), m) << std::endl;
first = false;
}
}
// if there are no fpa theory variables, was fp ever used?
if (first) return;
out << "bv theory variables:" << std::endl;
it = ctx.begin_enodes();

665
src/smt/theory_seq.cpp
View file

@ -22,24 +22,26 @@ Revision History:
#include "smt_model_generator.h"
#include "theory_seq.h"
#include "seq_rewriter.h"
#include "ast_trail.h"
using namespace smt;
void theory_seq::solution_map::update(expr* e, expr* r, enode_pair_dependency* d) {
std::pair<expr*, enode_pair_dependency*> value;
if (m_map.find(e, value)) {
m_updates.push_back(DEL);
m_lhs.push_back(e);
m_rhs.push_back(value.first);
m_deps.push_back(value.second);
add_trail(DEL, e, value.first, value.second);
}
value.first = r;
value.second = d;
m_map.insert(e, value);
m_updates.push_back(INS);
m_lhs.push_back(e);
m_rhs.push_back(value.first);
m_deps.push_back(value.second);
add_trail(INS, e, r, d);
}
void theory_seq::solution_map::add_trail(map_update op, expr* l, expr* r, enode_pair_dependency* d) {
m_updates.push_back(op);
m_lhs.push_back(l);
m_rhs.push_back(r);
m_deps.push_back(d);
}
expr* theory_seq::solution_map::find(expr* e, enode_pair_dependency*& d) {
@ -84,29 +86,62 @@ void theory_seq::solution_map::display(std::ostream& out) const {
}
}
void theory_seq::exclusion_table::update(expr* e, expr* r) {
if (e->get_id() > r->get_id()) {
std::swap(e, r);
}
if (e != r && !m_table.contains(std::make_pair(e, r))) {
m_lhs.push_back(e);
m_rhs.push_back(r);
m_table.insert(std::make_pair(e, r));
}
}
void theory_seq::exclusion_table::pop_scope(unsigned num_scopes) {
if (num_scopes == 0) return;
unsigned start = m_limit[m_limit.size() - num_scopes];
for (unsigned i = start; i < m_lhs.size(); ++i) {
m_table.erase(std::make_pair(m_lhs[i].get(), m_rhs[i].get()));
}
m_lhs.resize(start);
m_rhs.resize(start);
m_limit.resize(m_limit.size() - num_scopes);
}
void theory_seq::exclusion_table::display(std::ostream& out) const {
table_t::iterator it = m_table.begin(), end = m_table.end();
for (; it != end; ++it) {
out << mk_pp(it->first, m) << " != " << mk_pp(it->second, m) << "\n";
}
}
theory_seq::theory_seq(ast_manager& m):
theory(m.mk_family_id("seq")),
m(m),
m_dam(m_dep_array_value_manager, m_alloc),
m_rep(m, m_dm),
m_rep(m, m_dm),
m_sort2len_fn(m),
m_factory(0),
m_ineqs(m),
m_exclude(m),
m_axioms(m),
m_axioms_head(0),
m_branch_variable_head(0),
m_incomplete(false),
m_model_completion(false),
m_rewrite(m),
m_util(m),
m_autil(m),
m_trail_stack(*this) {
m_trail_stack(*this) {
m_lhs.push_back(expr_array());
m_rhs.push_back(expr_array());
m_deps.push_back(enode_pair_dependency_array());
m_prefix_sym = "prefix";
m_suffix_sym = "suffix";
m_left_sym = "left";
m_right_sym = "right";
m_contains_left_sym = "contains_left";
m_contains_right_sym = "contains_right";
m_prefix_sym = "seq.prefix.suffix";
m_suffix_sym = "seq.suffix.prefix";
m_left_sym = "seq.left";
m_right_sym = "seq.right";
m_contains_left_sym = "seq.contains.left";
m_contains_right_sym = "seq.contains.right";
}
theory_seq::~theory_seq() {
@ -130,6 +165,15 @@ final_check_status theory_seq::final_check_eh() {
if (ctx.inconsistent()) {
return FC_CONTINUE;
}
if (branch_variable()) {
return FC_CONTINUE;
}
if (split_variable()) {
return FC_CONTINUE;
}
if (ctx.inconsistent()) {
return FC_CONTINUE;
}
if (m.size(m_lhs.back()) > 0 || m_incomplete) {
return FC_GIVEUP;
}
@ -152,19 +196,98 @@ bool theory_seq::check_ineqs() {
return true;
}
bool theory_seq::branch_variable() {
context& ctx = get_context();
TRACE("seq", ctx.display(tout););
expr_array& lhs = m_lhs.back();
expr_array& rhs = m_rhs.back();
unsigned sz = m.size(lhs);
ptr_vector<expr> ls, rs;
for (unsigned i = 0; i < sz; ++i) {
unsigned k = (i + m_branch_variable_head) % sz;
expr* l = m.get(lhs, k);
expr* r = m.get(rhs, k);
TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << "\n";);
ls.reset(); rs.reset();
m_util.str.get_concat(l, ls);
m_util.str.get_concat(r, rs);
if (!ls.empty() && find_branch_candidate(ls[0], rs)) {
m_branch_variable_head = k;
return true;
}
if (!rs.empty() && find_branch_candidate(rs[0], ls)) {
m_branch_variable_head = k;
return true;
}
}
return false;
}
bool theory_seq::find_branch_candidate(expr* l, ptr_vector<expr> const& rs) {
TRACE("seq", tout << mk_pp(l, m) << " "
<< (is_var(l)?"var":"not var") << "\n";);
if (!is_var(l)) {
return false;
}
expr_ref v0(m), v(m);
v0 = m_util.str.mk_empty(m.get_sort(l));
if (assume_equality(l, v0)) {
return true;
}
for (unsigned j = 0; j < rs.size(); ++j) {
if (occurs(l, rs[j])) {
return false;
}
std::string s;
if (m_util.str.is_string(rs[j], s)) {
for (size_t k = 1; k < s.length(); ++k) {
v = m_util.str.mk_string(std::string(s.c_str(), k));
if (v0) v = m_util.str.mk_concat(v0, v);
if (assume_equality(l, v)) {
return true;
}
}
}
v0 = (j == 0)? rs[0] : m_util.str.mk_concat(v0, rs[j]);
if (assume_equality(l, v0)) {
return true;
}
}
return false;
}
bool theory_seq::assume_equality(expr* l, expr* r) {
context& ctx = get_context();
if (m_exclude.contains(l, r)) {
return false;
}
else {
TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << "\n";);
if (!ctx.e_internalized(l)) ctx.internalize(l, false);
if (!ctx.e_internalized(r)) ctx.internalize(r, false);
ctx.mark_as_relevant(ctx.get_enode(l));
ctx.mark_as_relevant(ctx.get_enode(r));
ctx.assume_eq(ctx.get_enode(l), ctx.get_enode(r));
return true;
}
}
bool theory_seq::split_variable() {
return false;
}
void theory_seq::propagate_lit(enode_pair_dependency* dep, literal lit) {
context& ctx = get_context();
ctx.mark_as_relevant(lit);
vector<enode_pair, false> _eqs;
m_dm.linearize(dep, _eqs);
TRACE("seq",
ctx.display_detailed_literal(tout, lit);
tout << " <- ";
for (unsigned i = 0; i < _eqs.size(); ++i) {
tout << mk_pp(_eqs[i].first->get_owner(), m) << " = "
<< mk_pp(_eqs[i].second->get_owner(), m) << "\n";
}
);
TRACE("seq", ctx.display_detailed_literal(tout, lit);
tout << " <-\n"; display_deps(tout, dep););
justification* js =
ctx.mk_justification(
ext_theory_propagation_justification(
@ -177,12 +300,7 @@ void theory_seq::set_conflict(enode_pair_dependency* dep) {
context& ctx = get_context();
vector<enode_pair, false> _eqs;
m_dm.linearize(dep, _eqs);
TRACE("seq",
for (unsigned i = 0; i < _eqs.size(); ++i) {
tout << mk_pp(_eqs[i].first->get_owner(), m) << " = "
<< mk_pp(_eqs[i].second->get_owner(), m) << "\n";
}
);
TRACE("seq", display_deps(tout, dep););
ctx.set_conflict(
ctx.mk_justification(
ext_theory_conflict_justification(
@ -195,10 +313,7 @@ void theory_seq::propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2)
m_dm.linearize(dep, _eqs);
TRACE("seq",
tout << mk_pp(n1->get_owner(), m) << " " << mk_pp(n2->get_owner(), m) << " <- ";
for (unsigned i = 0; i < _eqs.size(); ++i) {
tout << mk_pp(_eqs[i].first->get_owner(), m) << " = "
<< mk_pp(_eqs[i].second->get_owner(), m) << "\n";
}
display_deps(tout, dep);
);
justification* js = ctx.mk_justification(
@ -283,7 +398,12 @@ bool theory_seq::occurs(expr* a, expr* b) {
}
bool theory_seq::is_var(expr* a) {
return is_uninterp(a) || m_util.is_skolem(a);
return
m_util.is_seq(a) &&
!m_util.str.is_concat(a) &&
!m_util.str.is_empty(a) &&
!m_util.str.is_string(a) &&
!m_util.str.is_unit(a);
}
bool theory_seq::is_left_select(expr* a, expr*& b) {
@ -296,15 +416,12 @@ bool theory_seq::is_right_select(expr* a, expr*& b) {
to_app(a)->get_decl()->get_parameter(0).get_symbol() == m_right_sym && (b = to_app(a)->get_arg(0), true);
}
void theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) {
context& ctx = get_context();
m_rep.update(l, r, deps);
// TBD: skip new equalities for non-internalized terms.
if (ctx.e_internalized(l) && ctx.e_internalized(r)) {
enode* n1 = ctx.get_enode(l);
enode* n2 = ctx.get_enode(r);
propagate_eq(deps, n1, n2);
propagate_eq(deps, ctx.get_enode(l), ctx.get_enode(r));
}
}
@ -352,13 +469,7 @@ bool theory_seq::simplify_and_solve_eqs() {
return change;
}
final_check_status theory_seq::add_axioms() {
for (unsigned i = 0; i < get_num_vars(); ++i) {
// add axioms for len(x) when x = a ++ b
}
return FC_DONE;
void theory_seq::internalize_eq_eh(app * atom, bool_var v) {
}
bool theory_seq::internalize_atom(app* a, bool) {
@ -366,23 +477,29 @@ bool theory_seq::internalize_atom(app* a, bool) {
}
bool theory_seq::internalize_term(app* term) {
TRACE("seq", tout << mk_pp(term, m) << "\n";);
context & ctx = get_context();
unsigned num_args = term->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
ctx.internalize(term->get_arg(i), false);
}
if (ctx.e_internalized(term)) {
return true;
expr* arg = term->get_arg(i);
ctx.internalize(arg, false);
if (ctx.e_internalized(arg)) {
mk_var(ctx.get_enode(arg));
}
}
if (m.is_bool(term)) {
bool_var bv = ctx.mk_bool_var(term);
ctx.set_var_theory(bv, get_id());
ctx.set_enode_flag(bv, true);
}
else {
enode * e = ctx.mk_enode(term, false, m.is_bool(term), true);
theory_var v = mk_var(e);
ctx.attach_th_var(e, this, v);
enode* e = 0;
if (ctx.e_internalized(term)) {
e = ctx.get_enode(term);
}
else {
e = ctx.mk_enode(term, false, m.is_bool(term), true);
}
mk_var(e);
}
if (!m_util.str.is_concat(term) &&
!m_util.str.is_string(term) &&
@ -394,39 +511,63 @@ bool theory_seq::internalize_term(app* term) {
!m_util.is_skolem(term)) {
set_incomplete(term);
}
// assert basic axioms
expr* arg;
func_decl* fn;
if (m_util.str.is_length(term, arg) && !m_sort2len_fn.find(m.get_sort(arg), fn)) {
m_trail_stack.push(ast2ast_trail<theory_seq, sort, func_decl>(m_sort2len_fn, m.get_sort(arg), term->get_decl()));
}
return true;
}
void theory_seq::apply_sort_cnstr(enode* n, sort* s) {
if (!is_attached_to_var(n)) {
mk_var(n);
}
mk_var(n);
}
void theory_seq::display(std::ostream & out) const {
if (m.size(m_lhs.back()) == 0 &&
m_ineqs.empty() &&
m_rep.empty() &&
m_exclude.empty()) {
return;
}
out << "Theory seq\n";
if (m.size(m_lhs.back()) > 0) {
out << "Equations:\n";
display_equations(out);
}
if (!m_ineqs.empty()) {
out << "Negative constraints:\n";
for (unsigned i = 0; i < m_ineqs.size(); ++i) {
out << mk_pp(m_ineqs[i], m) << "\n";
}
}
if (!m_rep.empty()) {
out << "Solved equations:\n";
m_rep.display(out);
}
if (!m_exclude.empty()) {
out << "Exclusions:\n";
m_exclude.display(out);
}
}
void theory_seq::display_equations(std::ostream& out) const {
expr_array const& lhs = m_lhs.back();
expr_array const& rhs = m_rhs.back();
enode_pair_dependency_array const& deps = m_deps.back();
out << "Equations:\n";
for (unsigned i = 0; i < m.size(lhs); ++i) {
out << mk_pp(m.get(lhs, i), m) << " = " << mk_pp(m.get(rhs, i), m) << " <-\n";
enode_pair_dependency* dep = m_dam.get(deps, i);
if (dep) {
vector<enode_pair, false> _eqs;
const_cast<enode_pair_dependency_manager&>(m_dm).linearize(dep, _eqs);
for (unsigned i = 0; i < _eqs.size(); ++i) {
out << " " << mk_pp(_eqs[i].first->get_owner(), m) << " = " << mk_pp(_eqs[i].second->get_owner(), m) << "\n";
}
}
display_deps(out, m_dam.get(deps, i));
}
}
void theory_seq::display_deps(std::ostream& out, enode_pair_dependency* dep) const {
if (!dep) return;
vector<enode_pair, false> _eqs;
const_cast<enode_pair_dependency_manager&>(m_dm).linearize(dep, _eqs);
for (unsigned i = 0; i < _eqs.size(); ++i) {
out << " " << mk_pp(_eqs[i].first->get_owner(), m) << " = " << mk_pp(_eqs[i].second->get_owner(), m) << "\n";
}
out << "Negative constraints:\n";
for (unsigned i = 0; i < m_ineqs.size(); ++i) {
out << mk_pp(m_ineqs[i], m) << "\n";
}
out << "Solved equations:\n";
m_rep.display(out);
}
void theory_seq::collect_statistics(::statistics & st) const {
@ -435,34 +576,15 @@ void theory_seq::collect_statistics(::statistics & st) const {
}
void theory_seq::init_model(model_generator & mg) {
m_factory = alloc(seq_factory, get_manager(),
get_family_id(), mg.get_model());
m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model());
mg.register_factory(m_factory);
// TBD: this is still unsound model generation.
// disequalities are not guaranteed. we need to
// prime the factory with a prefix that cannot be
// constructed using any existing combinations of the
// strings (or units) that are used.
for (unsigned i = 0; i < get_num_vars(); ++i) {
expr* e = get_enode(i)->get_owner();
if (m_util.is_seq(e)) {
enode_pair_dependency* deps = 0;
e = m_rep.find(e, deps);
if (is_var(e)) {
expr* val = m_factory->get_fresh_value(m.get_sort(e));
m_rep.update(e, val, 0);
}
}
else if (m_util.is_re(e)) {
// TBD
}
}
}
model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
enode_pair_dependency* deps = 0;
expr_ref e(n->get_owner(), m);
canonize(e, deps);
flet<bool> _model_completion(m_model_completion, true);
e = canonize(e, deps);
SASSERT(is_app(e));
m_factory->add_trail(e);
return alloc(expr_wrapper_proc, to_app(e));
@ -471,15 +593,27 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
void theory_seq::set_incomplete(app* term) {
TRACE("seq", tout << "No support for: " << mk_pp(term, m) << "\n";);
if (!m_incomplete) {
m_trail_stack.push(value_trail<theory_seq,bool>(m_incomplete));
TRACE("seq", tout << "Incomplete operator: " << mk_pp(term, m) << "\n";);
m_trail_stack.push(value_trail<theory_seq, bool>(m_incomplete));
m_incomplete = true;
}
}
theory_var theory_seq::mk_var(enode* n) {
return theory::mk_var(n);
if (!m_util.is_seq(n->get_owner()) &&
!m_util.is_re(n->get_owner())) {
return null_theory_var;
}
if (is_attached_to_var(n)) {
return n->get_th_var(get_id());
}
else {
theory_var v = theory::mk_var(n);
get_context().attach_th_var(n, this, v);
get_context().mark_as_relevant(n);
return v;
}
}
bool theory_seq::can_propagate() {
@ -515,6 +649,15 @@ expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) {
if (m_util.str.is_contains(e, e1, e2)) {
return expr_ref(m_util.str.mk_contains(expand(e1, eqs), expand(e2, eqs)), m);
}
if (m_model_completion && is_var(e)) {
SASSERT(m_factory);
expr_ref val(m);
val = m_factory->get_fresh_value(m.get_sort(e));
if (val) {
m_rep.update(e, val, 0);
return val;
}
}
return expr_ref(e, m);
}
@ -530,29 +673,295 @@ void theory_seq::propagate() {
while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) {
expr_ref e(m);
e = m_axioms[m_axioms_head].get();
assert_axiom(e);
deque_axiom(e);
++m_axioms_head;
}
}
void theory_seq::create_axiom(expr_ref& e) {
void theory_seq::enque_axiom(expr* e) {
TRACE("seq", tout << "add axioms for: " << mk_pp(e, m) << "\n";);
m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_axioms));
m_axioms.push_back(e);
}
void theory_seq::assert_axiom(expr_ref& e) {
context & ctx = get_context();
if (m.is_true(e)) return;
TRACE("seq", tout << "asserting " << e << "\n";);
ctx.internalize(e, false);
literal lit(ctx.get_literal(e));
ctx.mark_as_relevant(lit);
ctx.mk_th_axiom(get_id(), 1, &lit);
void theory_seq::deque_axiom(expr* n) {
if (m_util.str.is_length(n)) {
add_length_axiom(n);
}
else if (m_util.str.is_index(n)) {
add_indexof_axiom(n);
}
else if (m_util.str.is_replace(n)) {
add_replace_axiom(n);
}
else if (m_util.str.is_extract(n)) {
add_extract_axiom(n);
}
else if (m_util.str.is_at(n)) {
add_at_axiom(n);
}
}
/*
\brief nodes n1 and n2 are about to get merged.
if n1 occurs in the context of a length application,
then instantiate length axioms for each concatenation in the class of n2.
In this way we ensure that length respects concatenation.
*/
void theory_seq::new_eq_len_concat(enode* n1, enode* n2) {
context& ctx = get_context();
if (n1->get_root() == n2->get_root()) {
return;
}
SASSERT(n1->get_root() != n2->get_root());
if (!m_util.is_seq(n1->get_owner())) {
return;
}
func_decl* f_len = 0;
if (!m_sort2len_fn.find(m.get_sort(n1->get_owner()), f_len)) {
return;
}
enode* r1 = n1->get_root();
enode_vector::const_iterator it = ctx.begin_enodes_of(f_len);
enode_vector::const_iterator end = ctx.end_enodes_of(f_len);
bool has_len = false;
for (; !has_len && it != end; ++it) {
has_len = ((*it)->get_root() == r1);
}
if (!has_len) {
return;
}
enode* start2 = n2;
do {
expr* o = n2->get_owner();
if (!is_var(o)) {
expr_ref ln(m_util.str.mk_length(o), m);
enque_axiom(ln);
}
n2 = n2->get_next();
}
while (n2 != start2);
}
/*
encode that s is not a proper prefix of xs1
where s1 is all of s, except the last element.
lit or s = "" or s = s1*c
lit or s = "" or len(c) = 1
lit or s = "" or !prefix(s, x*s1)
*/
void theory_seq::tightest_prefix(expr* s, expr* x, literal lit) {
expr_ref s1 = mk_skolem(symbol("seq.first"), s);
expr_ref c = mk_skolem(symbol("seq.last"), s);
expr_ref s1c(m_util.str.mk_concat(s1, c), m);
expr_ref lc(m_util.str.mk_length(c), m);
expr_ref one(m_autil.mk_int(1), m);
expr_ref emp(m_util.str.mk_empty(m.get_sort(s)), m);
literal s_eq_emp = mk_eq(s, emp, false);
add_axiom(lit, s_eq_emp, mk_eq(s, s1c, false));
add_axiom(lit, s_eq_emp, mk_eq(lc, one, false));
add_axiom(lit, s_eq_emp, ~mk_literal(m_util.str.mk_contains(s, m_util.str.mk_concat(x, s1))));
}
/*
let i = Index(t, s, offset)
if offset = 0:
(!contains(t, s) -> i = -1)
(s = empty -> i = 0)
(contains(t, s) & s != empty -> t = xsy)
(contains(t, s) -> tightest_prefix(s, x))
if 0 <= offset < len(t):
t = zt' & len(z) == offset
add above constraints with t'
if offset >= len(t):
i = -1
if offset < 0:
?
optional lemmas:
(len(s) > len(t) -> i = -1)
(len(s) <= len(t) -> i <= len(t)-len(s))
*/
void theory_seq::add_indexof_axiom(expr* i) {
expr* s, *t, *offset;
rational r;
VERIFY(m_util.str.is_index(i, t, s, offset));
expr_ref emp(m), minus_one(m), zero(m), xsy(m);
minus_one = m_autil.mk_int(-1);
zero = m_autil.mk_int(0);
emp = m_util.str.mk_empty(m.get_sort(s));
if (m_autil.is_numeral(offset, r) && r.is_zero()) {
expr_ref x = mk_skolem(m_contains_left_sym, t, s);
expr_ref y = mk_skolem(m_contains_right_sym, t, s);
xsy = m_util.str.mk_concat(x,s,y);
literal cnt = mk_literal(m_util.str.mk_contains(t, s));
literal eq_empty = mk_eq(s, emp, false);
add_axiom(cnt, mk_eq(i, minus_one, false));
add_axiom(~eq_empty, mk_eq(i, zero, false));
add_axiom(~cnt, eq_empty, mk_eq(t, xsy, false));
tightest_prefix(s, x, ~cnt);
}
else {
// TBD
}
}
/*
let r = replace(a, s, t)
(contains(a, s) -> tightest_prefix(s,xs))
(contains(a, s) -> r = xty & a = xsy) &
(!contains(a, s) -> r = a)
*/
void theory_seq::add_replace_axiom(expr* r) {
expr* a, *s, *t;
VERIFY(m_util.str.is_replace(r, a, s, t));
expr_ref x = mk_skolem(m_contains_left_sym, a, s);
expr_ref y = mk_skolem(m_contains_right_sym, a, s);
expr_ref xty(m_util.str.mk_concat(x, t, y), m);
expr_ref xsy(m_util.str.mk_concat(x, s, y), m);
literal cnt = mk_literal(m_util.str.mk_contains(a ,s));
add_axiom(cnt, mk_eq(r, a, false));
add_axiom(~cnt, mk_eq(a, xsy, false));
add_axiom(~cnt, mk_eq(r, xty, false));
tightest_prefix(s, x, ~cnt);
}
/*
let n = len(x)
len(x) >= 0
len(x) = 0 => x = ""
x = "" => len(x) = 0
len(x) = rewrite(len(x))
*/
void theory_seq::add_length_axiom(expr* n) {
expr* x, *a, *b;
VERIFY(m_util.str.is_length(n, x));
expr_ref zero(m), one(m), emp(m);
zero = m_autil.mk_int(0);
std::string s;
if (m_util.str.is_unit(n)) {
one = m_autil.mk_int(1);
add_axiom(mk_eq(n, one, false));
}
else if (m_util.str.is_empty(n)) {
add_axiom(mk_eq(n, zero, false));
}
else if (m_util.str.is_string(n, s)) {
expr_ref ls(m_autil.mk_numeral(rational(s.length(), rational::ui64()), true), m);
add_axiom(mk_eq(n, ls, false));
}
else if (m_util.str.is_concat(n, a, b)) {
expr_ref _a(m_util.str.mk_length(a), m);
expr_ref _b(m_util.str.mk_length(b), m);
expr_ref a_p_b(m_autil.mk_add(_a, _b), m);
add_axiom(mk_eq(n, a_p_b, false));
}
else {
emp = m_util.str.mk_empty(m.get_sort(x));
literal eq1(mk_eq(zero, n, false));
literal eq2(mk_eq(x, emp, false));
add_axiom(mk_literal(m_autil.mk_ge(n, zero)));
add_axiom(~eq1, eq2);
add_axiom(~eq2, eq1);
}
}
expr* theory_seq::mk_sub(expr* a, expr* b) {
return m_autil.mk_add(a, m_autil.mk_mul(m_autil.mk_int(-1), b));
}
/*
TBD: check semantics of extract.
let e = extract(s, i, l)
0 <= i < len(s) -> prefix(xe,s) & len(x) = i
0 <= i < len(s) & l >= len(s) - i -> len(e) = len(s) - i
0 <= i < len(s) & 0 <= l < len(s) - i -> len(e) = l
0 <= i < len(s) & l < 0 -> len(e) = 0
* i < 0 -> e = s
* i >= len(s) -> e = empty
*/
void theory_seq::add_extract_axiom(expr* e) {
expr* s, *i, *l;
VERIFY(m_util.str.is_extract(e, s, i, l));
expr_ref x(mk_skolem(symbol("seq.extract.prefix"), s, e), m);
expr_ref ls(m_util.str.mk_length(s), m);
expr_ref lx(m_util.str.mk_length(x), m);
expr_ref le(m_util.str.mk_length(e), m);
expr_ref ls_minus_i(mk_sub(ls, i), m);
expr_ref xe(m_util.str.mk_concat(x, e), m);
expr_ref zero(m_autil.mk_int(0), m);
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
literal i_le_l = mk_literal(m_autil.mk_le(mk_sub(i, l), zero));
literal i_ge_ls = mk_literal(m_autil.mk_ge(mk_sub(i, ls), zero));
literal l_ge_ls = mk_literal(m_autil.mk_ge(mk_sub(l, ls), zero));
literal l_ge_zero = mk_literal(m_autil.mk_ge(l, zero));
add_axiom(~i_ge_0, i_ge_ls, mk_literal(m_util.str.mk_prefix(xe, s)));
add_axiom(~i_ge_0, i_ge_ls, mk_eq(lx, i, false));
add_axiom(~i_ge_0, i_ge_ls, ~l_ge_ls, mk_eq(le, ls_minus_i, false));
add_axiom(~i_ge_0, i_ge_ls, l_ge_zero, mk_eq(le, zero, false));
}
/*
let e = at(s, i)
0 <= i < len(s) -> s = xey & len(x) = i & len(e) = 1
*/
void theory_seq::add_at_axiom(expr* e) {
expr* s, *i;
VERIFY(m_util.str.is_at(e, s, i));
expr_ref x(m), y(m), lx(m), le(m), xey(m), zero(m), one(m), len_e(m), len_x(m);
x = mk_skolem(symbol("seq.at.left"), s);
y = mk_skolem(symbol("seq.at.right"), s);
xey = m_util.str.mk_concat(x, e, y);
zero = m_autil.mk_int(0);
one = m_autil.mk_int(1);
len_e = m_util.str.mk_length(e);
len_x = m_util.str.mk_length(x);
literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero));
literal i_ge_len_s = mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero));
add_axiom(~i_ge_0, i_ge_len_s, mk_eq(s, xey, false));
add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e, false));
add_axiom(~i_ge_0, i_ge_len_s, mk_eq(i, len_x, false));
}
literal theory_seq::mk_literal(expr* _e) {
expr_ref e(_e, m);
context& ctx = get_context();
ctx.internalize(e, false);
return ctx.get_literal(e);
}
void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) {
context& ctx = get_context();
literal_vector lits;
if (l1 != null_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); }
if (l2 != null_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); }
if (l3 != null_literal) { ctx.mark_as_relevant(l3); lits.push_back(l3); }
if (l4 != null_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); }
TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";);
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
}
expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2) {
expr* es[2] = { e1, e2 };
return expr_ref(m_util.mk_skolem(name, 2, es, m.get_sort(e1)), m);
return expr_ref(m_util.mk_skolem(name, e2?2:1, es, m.get_sort(e1)), m);
}
void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) {
@ -594,11 +1003,15 @@ void theory_seq::assign_eq(bool_var v, bool is_true) {
else if (m_util.str.is_contains(e, e1, e2)) {
expr_ref f1 = mk_skolem(m_contains_left_sym, e1, e2);
expr_ref f2 = mk_skolem(m_contains_right_sym, e1, e2);
f = m_util.str.mk_concat(m_util.str.mk_concat(f1, e1), f2);
propagate_eq(v, f, e2);
f = m_util.str.mk_concat(m_util.str.mk_concat(f1, e2), f2);
propagate_eq(v, f, e1);
}
else if (m_util.str.is_in_re(e, e1, e2)) {
NOT_IMPLEMENTED_YET();
// TBD
}
else if (m.is_eq(e, e1, e2)) {
new_eq_eh(ctx.get_enode(e1)->get_th_var(get_id()),
ctx.get_enode(e1)->get_th_var(get_id()));
}
else {
UNREACHABLE();
@ -614,9 +1027,14 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
enode* n1 = get_enode(v1);
enode* n2 = get_enode(v2);
if (n1 != n2) {
m.push_back(m_lhs.back(), n1->get_owner());
m.push_back(m_rhs.back(), n2->get_owner());
expr* o1 = n1->get_owner(), *o2 = n2->get_owner();
TRACE("seq", tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";);
m.push_back(m_lhs.back(), o1);
m.push_back(m_rhs.back(), o2);
m_dam.push_back(m_deps.back(), m_dm.mk_leaf(enode_pair(n1, n2)));
new_eq_len_concat(n1, n2);
new_eq_len_concat(n2, n1);
}
}
@ -625,11 +1043,14 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
expr* e2 = get_enode(v2)->get_owner();
m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_ineqs));
m_ineqs.push_back(mk_eq_atom(e1, e2));
m_exclude.update(e1, e2);
}
void theory_seq::push_scope_eh() {
TRACE("seq", tout << "push " << m_lhs.size() << "\n";);
theory::push_scope_eh();
m_rep.push_scope();
m_exclude.push_scope();
m_dm.push_scope();
m_trail_stack.push_scope();
m_trail_stack.push(value_trail<theory_seq, unsigned>(m_axioms_head));
@ -644,10 +1065,12 @@ void theory_seq::push_scope_eh() {
}
void theory_seq::pop_scope_eh(unsigned num_scopes) {
TRACE("seq", tout << "pop " << m_lhs.size() << "\n";);
m_trail_stack.pop_scope(num_scopes);
theory::pop_scope_eh(num_scopes);
m_dm.pop_scope(num_scopes);
m_rep.pop_scope(num_scopes);
m_exclude.pop_scope(num_scopes);
while (num_scopes > 0) {
--num_scopes;
m.del(m_lhs.back());
@ -673,10 +1096,12 @@ void theory_seq::restart_eh() {
#endif
}
void theory_seq::relevant_eh(app* n) {
if (m_util.str.is_length(n)) {
expr_ref e(m);
e = m_autil.mk_le(m_autil.mk_numeral(rational(0), true), n);
create_axiom(e);
void theory_seq::relevant_eh(app* n) {
if (m_util.str.is_length(n) ||
m_util.str.is_index(n) ||
m_util.str.is_replace(n) ||
m_util.str.is_extract(n) ||
m_util.str.is_at(n)) {
enque_axiom(n);
}
}

90
src/smt/theory_seq.h
View file

@ -24,6 +24,7 @@ Revision History:
#include "theory_seq_empty.h"
#include "th_rewriter.h"
#include "union_find.h"
#include "ast_trail.h"
namespace smt {
@ -53,12 +54,15 @@ namespace smt {
ast_manager& m;
enode_pair_dependency_manager& m_dm;
map_t m_map;
expr_ref_vector m_lhs, m_rhs;
expr_ref_vector m_lhs, m_rhs;
ptr_vector<enode_pair_dependency> m_deps;
svector<map_update> m_updates;
unsigned_vector m_limit;
void add_trail(map_update op, expr* l, expr* r, enode_pair_dependency* d);
public:
solution_map(ast_manager& m, enode_pair_dependency_manager& dm): m(m), m_dm(dm), m_lhs(m), m_rhs(m) {}
bool empty() const { return m_map.empty(); }
void update(expr* e, expr* r, enode_pair_dependency* d);
expr* find(expr* e, enode_pair_dependency*& d);
void push_scope() { m_limit.push_back(m_updates.size()); }
@ -66,6 +70,25 @@ namespace smt {
void display(std::ostream& out) const;
};
class exclusion_table {
typedef obj_pair_hashtable<expr, expr> table_t;
ast_manager& m;
table_t m_table;
expr_ref_vector m_lhs, m_rhs;
unsigned_vector m_limit;
public:
exclusion_table(ast_manager& m): m(m), m_lhs(m), m_rhs(m) {}
~exclusion_table() { }
bool empty() const { return m_table.empty(); }
void update(expr* e, expr* r);
bool contains(expr* e, expr* r) {
return m_table.contains(std::make_pair(e, r));
}
void push_scope() { m_limit.push_back(m_lhs.size()); }
void pop_scope(unsigned num_scopes);
void display(std::ostream& out) const;
};
struct stats {
stats() { reset(); }
void reset() { memset(this, 0, sizeof(stats)); }
@ -81,11 +104,15 @@ namespace smt {
vector<expr_array> m_lhs, m_rhs; // persistent sets of equalities.
vector<enode_pair_dependency_array> m_deps; // persistent sets of dependencies.
seq_factory* m_factory; // value factory
expr_ref_vector m_ineqs; // inequalities to check
expr_ref_vector m_axioms;
unsigned m_axioms_head;
bool m_incomplete;
ast2ast_trailmap<sort, func_decl> m_sort2len_fn; // length functions per sort.
seq_factory* m_factory; // value factory
expr_ref_vector m_ineqs; // inequalities to check solution against
exclusion_table m_exclude; // set of asserted disequalities.
expr_ref_vector m_axioms; // list of axioms to add.
unsigned m_axioms_head; // index of first axiom to add.
unsigned m_branch_variable_head; // index of first equation to examine.
bool m_incomplete; // is the solver (clearly) incomplete for the fragment.
bool m_model_completion; // during model construction, invent values in canonizer
th_rewriter m_rewrite;
seq_util m_util;
arith_util m_autil;
@ -95,12 +122,13 @@ namespace smt {
symbol m_suffix_sym;
symbol m_contains_left_sym;
symbol m_contains_right_sym;
symbol m_left_sym;
symbol m_right_sym;
symbol m_left_sym; // split variable left part
symbol m_right_sym; // split variable right part
virtual final_check_status final_check_eh();
virtual bool internalize_atom(app*, bool);
virtual bool internalize_term(app*);
virtual void internalize_eq_eh(app * atom, bool_var v);
virtual void new_eq_eh(theory_var, theory_var);
virtual void new_diseq_eh(theory_var, theory_var);
virtual void assign_eq(bool_var v, bool is_true);
@ -114,40 +142,66 @@ namespace smt {
virtual char const * get_name() const { return "seq"; }
virtual theory_var mk_var(enode* n);
virtual void apply_sort_cnstr(enode* n, sort* s);
virtual void display(std::ostream & out) const;
virtual void display(std::ostream & out) const;
virtual void collect_statistics(::statistics & st) const;
virtual model_value_proc * mk_value(enode * n, model_generator & mg);
virtual void init_model(model_generator & mg);
bool check_ineqs();
// final check
bool check_ineqs(); // check if inequalities are violated.
bool simplify_and_solve_eqs(); // solve unitary equalities
bool branch_variable(); // branch on a variable
bool split_variable(); // split a variable
bool pre_process_eqs(bool simplify_or_solve);
bool simplify_eqs();
bool simplify_eq(expr* l, expr* r, enode_pair_dependency* dep);
bool solve_unit_eq(expr* l, expr* r, enode_pair_dependency* dep);
bool solve_basic_eqs();
bool simplify_and_solve_eqs();
// asserting consequences
void propagate_lit(enode_pair_dependency* dep, literal lit);
void propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2);
void propagate_eq(bool_var v, expr* e1, expr* e2);
void set_conflict(enode_pair_dependency* dep);
bool find_branch_candidate(expr* l, ptr_vector<expr> const& rs);
bool assume_equality(expr* l, expr* r);
// variable solving utilities
bool occurs(expr* a, expr* b);
bool is_var(expr* b);
void add_solution(expr* l, expr* r, enode_pair_dependency* dep);
bool is_left_select(expr* a, expr*& b);
bool is_right_select(expr* a, expr*& b);
final_check_status add_axioms();
void assert_axiom(expr_ref& e);
void create_axiom(expr_ref& e);
expr_ref canonize(expr* e, enode_pair_dependency*& eqs);
expr_ref expand(expr* e, enode_pair_dependency*& eqs);
void add_dependency(enode_pair_dependency*& dep, enode* a, enode* b);
expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2);
// terms whose meaning are encoded using axioms.
void enque_axiom(expr* e);
void deque_axiom(expr* e);
void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal);
void add_indexof_axiom(expr* e);
void add_replace_axiom(expr* e);
void add_extract_axiom(expr* e);
void add_length_axiom(expr* n);
void add_at_axiom(expr* n);
literal mk_literal(expr* n);
void tightest_prefix(expr* s, expr* x, literal lit);
expr* mk_sub(expr* a, expr* b);
void new_eq_len_concat(enode* n1, enode* n2);
expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0);
void set_incomplete(app* term);
// diagnostics
void display_equations(std::ostream& out) const;
void display_deps(std::ostream& out, enode_pair_dependency* deps) const;
public:
theory_seq(ast_manager& m);
virtual ~theory_seq();

5
src/smt/theory_seq_empty.h
View file

@ -89,6 +89,11 @@ namespace smt {
return u.str.mk_string(sym);
}
}
sort* seq = 0;
if (u.is_re(s, seq)) {
expr* v0 = get_fresh_value(seq);
return u.re.mk_to_re(v0);
}
NOT_IMPLEMENTED_YET();
return 0;
}