From e7687132ed476db655a63cff1145eccb69302dea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Dec 2015 03:34:58 -0800 Subject: [PATCH 1/9] seq Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 31 ++++++++++++++++--------------- src/ast/seq_decl_plugin.cpp | 29 ++++++++++++++--------------- src/ast/seq_decl_plugin.h | 1 - 3 files changed, 30 insertions(+), 31 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 96590a40a..f46201ec7 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -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])); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index b47c4209d..bdbf033d6 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -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); diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index c61e3cc43..dc7c4634b 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -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, From 5aabc643129c3de76d4ad07b4313614c83289ba4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Dec 2015 08:11:00 -0800 Subject: [PATCH 2/9] seq Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 1 - src/smt/theory_seq.cpp | 62 ++++++++++++++++++++++++++++++------- src/smt/theory_seq.h | 12 ++++--- 3 files changed, 58 insertions(+), 17 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 67812a369..77e57b07c 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -302,7 +302,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_EMPTY_SEQ: case OP_RE_EMPTY_SET: case OP_RE_OF_PRED: diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index b3a143377..fa3ddfb23 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -26,15 +26,20 @@ using namespace smt; theory_seq::theory_seq(ast_manager& m): theory(m.mk_family_id("seq")), - m_axioms_head(0), - m_axioms(m), + m_rep(m), + m_eqs_head(0), m_ineqs(m), + m_axioms(m), + m_axioms_head(0), m_used(false), m_rewrite(m), m_util(m), m_autil(m), m_trail_stack(*this), - m_find(*this) {} + m_find(*this) { + m_lhs.push_back(expr_array()); + m_rhs.push_back(expr_array()); +} final_check_status theory_seq::final_check_eh() { context & ctx = get_context(); @@ -68,17 +73,27 @@ final_check_status theory_seq::check_ineqs() { return FC_DONE; } -final_check_status theory_seq::simplify_eqs() { +bool theory_seq::simplify_eqs() { + context & ctx = get_context(); + ast_manager& m = get_manager(); bool simplified = false; - for (unsigned i = 0; i < get_num_vars(); ++i) { - theory_var v = m_find.find(i); - if (v != i) continue; - + expr_array& lhs = m_lhs.back(); + expr_array& rhs = m_rhs.back(); + for (unsigned i = m_eqs_head; i < m.size(lhs); ++i) { + expr* l = m.get(lhs, i); + expr* r = m.get(rhs, i); +#if 0 + if (reduce(l, r)) { + ++m_eq_head; + } + else { + // equality is not simplified + // move forward pointer + } +#endif + } - if (simplified) { - return FC_CONTINUE; - } - return FC_DONE; + return simplified; } final_check_status theory_seq::add_axioms() { @@ -122,6 +137,7 @@ bool theory_seq::internalize_term(app* term) { theory_var theory_seq::mk_var(enode* n) { theory_var r = theory::mk_var(n); VERIFY(r == m_find.mk_var()); + m_rep.push_back(n->get_owner()); return r; } @@ -270,7 +286,13 @@ void theory_seq::assign_eq(bool_var v, bool is_true) { } void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { + ast_manager& m = get_manager(); m_find.merge(v1, v2); + expr_ref e1(m), e2(m); + e1 = get_enode(v1)->get_owner(); + e2 = get_enode(v2)->get_owner(); + m.push_back(m_lhs.back(), get_enode(v1)->get_owner()); + m.push_back(m_rhs.back(), get_enode(v2)->get_owner()); } void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { @@ -282,14 +304,30 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { } void theory_seq::push_scope_eh() { + ast_manager& m = get_manager(); theory::push_scope_eh(); m_trail_stack.push_scope(); m_trail_stack.push(value_trail(m_axioms_head)); + m_trail_stack.push(value_trail(m_eqs_head)); + expr_array lhs, rhs; + m.copy(m_lhs.back(), lhs); + m.copy(m_rhs.back(), rhs); + m_lhs.push_back(lhs); + m_rhs.push_back(rhs); } void theory_seq::pop_scope_eh(unsigned num_scopes) { + ast_manager& m = get_manager(); m_trail_stack.pop_scope(num_scopes); theory::pop_scope_eh(num_scopes); + m_rep.resize(get_num_vars()); + while (num_scopes > 0) { + --num_scopes; + m.del(m_lhs.back()); + m.del(m_rhs.back()); + m_lhs.pop_back(); + m_rhs.pop_back(); + } } void theory_seq::restart_eh() { diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 3232a8469..9b6258a2c 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -35,10 +35,14 @@ namespace smt { void reset() { memset(this, 0, sizeof(stats)); } unsigned m_num_splits; }; - expr_ref_vector m_axioms; - expr_ref_vector m_ineqs; + expr_ref_vector m_rep; // unification representative. + vector m_lhs, m_rhs; // persistent sets of equalities. + unsigned m_eqs_head; // index of unprocessed equation. + + expr_ref_vector m_ineqs; // inequalities to check + expr_ref_vector m_axioms; unsigned m_axioms_head; - bool m_used; + bool m_used; // deprecate th_rewriter m_rewrite; seq_util m_util; arith_util m_autil; @@ -63,7 +67,7 @@ namespace smt { virtual theory_var mk_var(enode* n); final_check_status check_ineqs(); - final_check_status simplify_eqs(); + bool simplify_eqs(); final_check_status add_axioms(); void assert_axiom(expr_ref& e); From 895d03299692c28b3e344e2a30c75f62c04f5989 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Dec 2015 10:33:09 -0800 Subject: [PATCH 3/9] seq Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 8 ++ src/ast/rewriter/seq_rewriter.cpp | 164 ++++++++++++++++++++++++++++++ src/ast/rewriter/seq_rewriter.h | 6 +- src/ast/rewriter/th_rewriter.cpp | 2 + src/ast/seq_decl_plugin.h | 24 +++-- src/smt/theory_seq.cpp | 72 ++++++++----- src/smt/theory_seq.h | 4 + 7 files changed, 242 insertions(+), 38 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 8db78f827..7cc6d12cc 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -65,6 +65,7 @@ IS_WINDOWS=False IS_LINUX=False IS_OSX=False IS_FREEBSD=False +IS_OPENBSD=False VERBOSE=True DEBUG_MODE=False SHOW_CPPS = True @@ -126,6 +127,9 @@ def is_linux(): def is_freebsd(): return IS_FREEBSD +def is_openbsd(): + return IS_OPENBSD + def is_osx(): return IS_OSX @@ -582,6 +586,8 @@ elif os.name == 'posix': IS_LINUX=True elif os.uname()[0] == 'FreeBSD': IS_FREEBSD=True + elif os.uname()[0] == 'OpenBSD': + IS_OPENBSD=True def display_help(exit_code): print("mk_make.py: Z3 Makefile generator\n") @@ -1596,6 +1602,8 @@ class JavaDLLComponent(Component): t = t.replace('PLATFORM', 'linux') elif IS_FREEBSD: t = t.replace('PLATFORM', 'freebsd') + elif IS_OPENBSD: + t = t.replace('PLATFORM', 'openbsd') else: t = t.replace('PLATFORM', 'win32') out.write(t) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index d0e360d21..ef73bd2f2 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -510,3 +510,167 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) { br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) { return BR_FAILED; } + +br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) { + expr_ref_vector lhs(m()), rhs(m()), res(m()); + if (!reduce_eq(l, r, lhs, rhs)) { + result = m().mk_false(); + return BR_DONE; + } + if (lhs.size() == 1 && lhs[0].get() == l && rhs[0].get() == r) { + return BR_FAILED; + } + for (unsigned i = 0; i < lhs.size(); ++i) { + res.push_back(m().mk_eq(lhs[i].get(), rhs[i].get())); + } + result = mk_and(res); + return BR_REWRITE3; +} + +bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs) { + expr* a, *b; + bool change = false; + expr_ref_vector trail(m()); + m_lhs.reset(); + m_rhs.reset(); + m_util.str.get_concat(l, m_lhs); + m_util.str.get_concat(r, m_rhs); + + // solve from back + while (!m_lhs.empty() && !m_rhs.empty()) { + if (m_lhs.back() == m_rhs.back()) { + m_lhs.pop_back(); + m_rhs.pop_back(); + } + else if(m_util.str.is_unit(m_lhs.back(), a) && + m_util.str.is_unit(m_rhs.back(), b)) { + lhs.push_back(a); + rhs.push_back(b); + m_lhs.pop_back(); + m_rhs.pop_back(); + } + else if (!m_rhs.empty() && m_util.str.is_empty(m_rhs.back())) { + m_rhs.pop_back(); + } + else if (!m_lhs.empty() && m_util.str.is_empty(m_lhs.back())) { + m_lhs.pop_back(); + } + else { + break; + } + change = true; + } + + // solve from front + unsigned head1 = 0, head2 = 0; + while (head1 < m_lhs.size() && head2 < m_rhs.size()) { + if (m_lhs[head1] == m_rhs[head2]) { + ++head1; + ++head2; + } + else if(m_util.str.is_unit(m_lhs[head1], a) && + m_util.str.is_unit(m_rhs[head2], b)) { + lhs.push_back(a); + rhs.push_back(b); + ++head1; + ++head2; + } + else if (head1 < m_lhs.size() && m_util.str.is_empty(m_lhs[head1])) { + ++head1; + } + else if (head2 < m_rhs.size() && m_util.str.is_empty(m_rhs[head2])) { + ++head2; + } + else { + break; + } + change = true; + } + // reduce strings + std::string s1, s2; + if (head1 < m_lhs.size() && + head2 < m_rhs.size() && + m_util.str.is_string(m_lhs[head1], s1) && + m_util.str.is_string(m_rhs[head2], s2)) { + size_t l = std::min(s1.length(), s2.length()); + for (size_t i = 0; i < l; ++i) { + if (s1[i] != s2[i]) { + return false; + } + } + if (l == s1.length()) { + ++head1; + } + else { + m_lhs[head1] = m_util.str.mk_string(std::string(s1.c_str()+l,s1.length()-l)); + trail.push_back(m_lhs[head1]); + } + if (l == s2.length()) { + ++head2; + } + else { + m_rhs[head2] = m_util.str.mk_string(std::string(s2.c_str()+l,s2.length()-l)); + trail.push_back(m_rhs[head2]); + } + change = true; + } + if (head1 < m_lhs.size() && + head2 < m_rhs.size() && + m_util.str.is_string(m_lhs.back(), s1) && + m_util.str.is_string(m_rhs.back(), s2)) { + size_t l = std::min(s1.length(), s2.length()); + for (size_t i = 0; i < l; ++i) { + if (s1[s1.length()-i-1] != s2[s2.length()-i-1]) { + return false; + } + } + m_lhs.pop_back(); + m_rhs.pop_back(); + if (l < s1.length()) { + m_lhs.push_back(m_util.str.mk_string(std::string(s1.c_str(),s1.length()-l))); + trail.push_back(m_lhs.back()); + } + if (l < s2.length()) { + m_rhs.push_back(m_util.str.mk_string(std::string(s2.c_str(),s2.length()-l))); + trail.push_back(m_rhs.back()); + } + change = true; + } + 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 { // head1 < m_lhs.size() && head2 < m_rhs.size() // could solve if either side is fixed size. + 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)); + } + return true; +} + +bool seq_rewriter::set_empty(unsigned sz, expr* const* es, 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 (m_util.str.is_empty(es[i])) { + continue; + } + if (m_util.str.is_string(es[i], s)) { + SASSERT(s.length() > 0); + return false; + } + lhs.push_back(m_util.str.mk_empty(m().get_sort(es[i]))); + rhs.push_back(es[i]); + } + return true; +} diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 4674a7535..57926efdf 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -32,7 +32,7 @@ Notes: class seq_rewriter { seq_util m_util; arith_util m_autil; - ptr_vector m_es; + ptr_vector 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); @@ -53,6 +53,7 @@ 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); public: seq_rewriter(ast_manager & m, params_ref const & p = params_ref()): m_util(m), m_autil(m) { @@ -64,6 +65,9 @@ public: static void get_param_descrs(param_descrs & r) {} br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); + br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); + + bool reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs); }; diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index a8aea47b6..aa1b35b89 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -177,6 +177,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg { st = m_f_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_ar_rw.get_fid()) st = m_ar_rw.mk_eq_core(args[0], args[1], result); + else if (s_fid == m_seq_rw.get_fid()) + st = m_seq_rw.mk_eq_core(args[0], args[1], result); if (st != BR_FAILED) return st; diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index feb3a279a..c317f8236 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -189,18 +189,19 @@ public: bool is_empty(expr const* n) const { symbol s; return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0); } - 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_SEQ_LENGTH); } + 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_SEQ_LENGTH); } 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_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); } - bool is_stoi(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STOI); } - bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); } + 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_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); } + bool is_stoi(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STOI); } + bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); } + bool is_unit(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_UNIT); } MATCH_BINARY(is_concat); @@ -215,6 +216,7 @@ public: MATCH_UNARY(is_itos); MATCH_UNARY(is_stoi); MATCH_BINARY(is_in_re); + MATCH_UNARY(is_unit); void get_concat(expr* e, ptr_vector& es) const; expr* get_leftmost_concat(expr* e) const { expr* e1, *e2; while (is_concat(e, e1, e2)) e = e1; return e; } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index fa3ddfb23..fd79aa46e 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -21,11 +21,13 @@ Revision History: #include "smt_context.h" #include "smt_model_generator.h" #include "theory_seq.h" +#include "seq_rewriter.h" using namespace smt; theory_seq::theory_seq(ast_manager& m): theory(m.mk_family_id("seq")), + m(m), m_rep(m), m_eqs_head(0), m_ineqs(m), @@ -43,7 +45,6 @@ theory_seq::theory_seq(ast_manager& m): final_check_status theory_seq::final_check_eh() { context & ctx = get_context(); - ast_manager& m = get_manager(); final_check_status st = check_ineqs(); if (st == FC_CONTINUE) { return FC_CONTINUE; @@ -53,7 +54,6 @@ final_check_status theory_seq::final_check_eh() { final_check_status theory_seq::check_ineqs() { context & ctx = get_context(); - ast_manager& m = get_manager(); enode_pair_vector eqs; for (unsigned i = 0; i < m_ineqs.size(); ++i) { expr_ref a(m_ineqs[i].get(), m); @@ -75,27 +75,58 @@ final_check_status theory_seq::check_ineqs() { bool theory_seq::simplify_eqs() { context & ctx = get_context(); - ast_manager& m = get_manager(); bool simplified = false; expr_array& lhs = m_lhs.back(); expr_array& rhs = m_rhs.back(); - for (unsigned i = m_eqs_head; i < m.size(lhs); ++i) { - expr* l = m.get(lhs, i); - expr* r = m.get(rhs, i); -#if 0 - if (reduce(l, r)) { - ++m_eq_head; + for (unsigned i = 0; !ctx.inconsistent() && i < m.size(lhs); ++i) { + if (simplify_eq(m.get(lhs, i), m.get(rhs, i), m_deps)) { + if (i + 1 != m.size(lhs)) { + m.set(lhs, i, m.get(lhs, m.size(lhs)-1)); + m.set(rhs, i, m.get(rhs, m.size(rhs)-1)); + --i; + simplified = true; + } + m.pop_back(lhs); + m.pop_back(rhs); } - else { - // equality is not simplified - // move forward pointer - } -#endif - } return simplified; } +bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_vector& deps) { + context& ctx = get_context(); + seq_rewriter rw(m); + expr_ref_vector lhs(m), rhs(m); + SASSERT(ctx.e_internalized(l)); + SASSERT(ctx.e_internalized(r)); + expr_ref lh = canonize(l, deps); + expr_ref rh = canonize(r, deps); + if (!rw.reduce_eq(l, r, lhs, rhs)) { + // equality is inconsistent. + // create conflict assignment. + expr_ref a(m); + a = m.mk_eq(l, r); + literal lit(ctx.get_literal(a)); + ctx.assign( + ~lit, + ctx.mk_justification( + ext_theory_propagation_justification( + get_id(), ctx.get_region(), 0, 0, deps.size(), deps.c_ptr(), ~lit))); + return true; + } + if (lhs.size() == 1 && l == lhs[0].get() && + rhs.size() == 1 && r == rhs[0].get()) { + return false; + } + SASSERT(lhs.size() == rhs.size()); + for (unsigned i = 0; i < lhs.size(); ++i) { + m.push_back(m_lhs.back(), lhs[i].get()); + m.push_back(m_rhs.back(), rhs[i].get()); + // TBD m_deps.push_back(deps); + } + return true; +} + final_check_status theory_seq::add_axioms() { for (unsigned i = 0; i < get_num_vars(); ++i) { @@ -111,7 +142,6 @@ bool theory_seq::internalize_atom(app* a, bool) { bool theory_seq::internalize_term(app* term) { m_used = true; context & ctx = get_context(); - ast_manager& m = get_manager(); unsigned num_args = term->get_num_args(); for (unsigned i = 0; i < num_args; i++) { ctx.internalize(term->get_arg(i), false); @@ -154,7 +184,6 @@ expr_ref theory_seq::canonize(expr* e, enode_pair_vector& eqs) { expr_ref theory_seq::expand(expr* e, enode_pair_vector& eqs) { context& ctx = get_context(); - ast_manager& m = get_manager(); expr* e1, *e2; SASSERT(ctx.e_internalized(e)); enode* n = ctx.get_enode(e); @@ -200,7 +229,6 @@ expr_ref theory_seq::expand(expr* e, enode_pair_vector& eqs) { void theory_seq::propagate() { context & ctx = get_context(); - ast_manager& m = get_manager(); while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) { expr_ref e(m); e = m_axioms[m_axioms_head].get(); @@ -216,7 +244,6 @@ void theory_seq::create_axiom(expr_ref& e) { void theory_seq::assert_axiom(expr_ref& e) { context & ctx = get_context(); - ast_manager& m = get_manager(); if (m.is_true(e)) return; TRACE("seq", tout << "asserting " << e << "\n";); ctx.internalize(e, false); @@ -227,7 +254,6 @@ void theory_seq::assert_axiom(expr_ref& e) { } expr_ref theory_seq::mk_skolem(char const* name, expr* e1, expr* e2) { - ast_manager& m = get_manager(); expr_ref result(m); sort* s = m.get_sort(e1); SASSERT(s == m.get_sort(e2)); @@ -249,7 +275,6 @@ void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) { void theory_seq::assign_eq(bool_var v, bool is_true) { context & ctx = get_context(); - ast_manager& m = get_manager(); enode* n = ctx.bool_var2enode(v); app* e = n->get_owner(); @@ -286,7 +311,6 @@ void theory_seq::assign_eq(bool_var v, bool is_true) { } void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { - ast_manager& m = get_manager(); m_find.merge(v1, v2); expr_ref e1(m), e2(m); e1 = get_enode(v1)->get_owner(); @@ -296,7 +320,6 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { } void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { - ast_manager& m = get_manager(); expr* e1 = get_enode(v1)->get_owner(); expr* e2 = get_enode(v2)->get_owner(); m_trail_stack.push(push_back_vector(m_ineqs)); @@ -304,7 +327,6 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { } void theory_seq::push_scope_eh() { - ast_manager& m = get_manager(); theory::push_scope_eh(); m_trail_stack.push_scope(); m_trail_stack.push(value_trail(m_axioms_head)); @@ -317,7 +339,6 @@ void theory_seq::push_scope_eh() { } void theory_seq::pop_scope_eh(unsigned num_scopes) { - ast_manager& m = get_manager(); m_trail_stack.pop_scope(num_scopes); theory::pop_scope_eh(num_scopes); m_rep.resize(get_num_vars()); @@ -335,7 +356,6 @@ void theory_seq::restart_eh() { } void theory_seq::relevant_eh(app* n) { - ast_manager& m = get_manager(); if (m_util.str.is_length(n)) { expr_ref e(m); e = m_autil.mk_le(m_autil.mk_numeral(rational(0), true), n); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 9b6258a2c..3a7b978e9 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -35,9 +35,12 @@ namespace smt { void reset() { memset(this, 0, sizeof(stats)); } unsigned m_num_splits; }; + ast_manager& m; expr_ref_vector m_rep; // unification representative. vector m_lhs, m_rhs; // persistent sets of equalities. unsigned m_eqs_head; // index of unprocessed equation. + enode_pair_vector m_deps; // TBD - convert to dependency structure. + expr_ref_vector m_ineqs; // inequalities to check expr_ref_vector m_axioms; @@ -68,6 +71,7 @@ namespace smt { final_check_status check_ineqs(); bool simplify_eqs(); + bool simplify_eq(expr* l, expr* r, enode_pair_vector& deps); final_check_status add_axioms(); void assert_axiom(expr_ref& e); From 932a3a83876ec68d8a0a0688b72ef3462415331d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Dec 2015 13:27:17 -0800 Subject: [PATCH 4/9] seq Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 197 ++++++++++++++++++++++++++++++++--------- src/smt/theory_seq.h | 55 +++++++++--- 2 files changed, 199 insertions(+), 53 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index fd79aa46e..1494b3afd 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -28,12 +28,13 @@ using namespace smt; 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_eqs_head(0), m_ineqs(m), m_axioms(m), m_axioms_head(0), - m_used(false), + m_incomplete(false), m_rewrite(m), m_util(m), m_autil(m), @@ -41,59 +42,48 @@ theory_seq::theory_seq(ast_manager& m): m_find(*this) { m_lhs.push_back(expr_array()); m_rhs.push_back(expr_array()); + m_deps.push_back(enode_pair_dependency_array()); } final_check_status theory_seq::final_check_eh() { context & ctx = get_context(); - final_check_status st = check_ineqs(); - if (st == FC_CONTINUE) { + if (!check_ineqs()) { return FC_CONTINUE; } - return m_used?FC_GIVEUP:FC_DONE; + if (simplify_and_solve_eqs()) { + return FC_CONTINUE; + } + if (m.size(m_lhs.back()) > 0) { + return FC_GIVEUP; + } + return m_incomplete?FC_GIVEUP:FC_DONE; } -final_check_status theory_seq::check_ineqs() { +bool theory_seq::check_ineqs() { context & ctx = get_context(); - enode_pair_vector eqs; for (unsigned i = 0; i < m_ineqs.size(); ++i) { expr_ref a(m_ineqs[i].get(), m); + enode_pair_dependency* eqs = 0; expr_ref b = canonize(a, eqs); if (m.is_true(b)) { ctx.internalize(a, false); literal lit(ctx.get_literal(a)); ctx.mark_as_relevant(lit); + vector _eqs; + m_dm.linearize(eqs, _eqs); ctx.assign( lit, ctx.mk_justification( ext_theory_propagation_justification( - get_id(), ctx.get_region(), 0, 0, eqs.size(), eqs.c_ptr(), lit))); - return FC_CONTINUE; + get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), lit))); + return false; } } - return FC_DONE; + return true; } -bool theory_seq::simplify_eqs() { - context & ctx = get_context(); - bool simplified = false; - expr_array& lhs = m_lhs.back(); - expr_array& rhs = m_rhs.back(); - for (unsigned i = 0; !ctx.inconsistent() && i < m.size(lhs); ++i) { - if (simplify_eq(m.get(lhs, i), m.get(rhs, i), m_deps)) { - if (i + 1 != m.size(lhs)) { - m.set(lhs, i, m.get(lhs, m.size(lhs)-1)); - m.set(rhs, i, m.get(rhs, m.size(rhs)-1)); - --i; - simplified = true; - } - m.pop_back(lhs); - m.pop_back(rhs); - } - } - return simplified; -} -bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_vector& deps) { +bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_dependency* deps) { context& ctx = get_context(); seq_rewriter rw(m); expr_ref_vector lhs(m), rhs(m); @@ -107,11 +97,13 @@ bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_vector& deps) { expr_ref a(m); a = m.mk_eq(l, r); literal lit(ctx.get_literal(a)); + vector _eqs; + m_dm.linearize(deps, _eqs); ctx.assign( ~lit, ctx.mk_justification( ext_theory_propagation_justification( - get_id(), ctx.get_region(), 0, 0, deps.size(), deps.c_ptr(), ~lit))); + get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), ~lit))); return true; } if (lhs.size() == 1 && l == lhs[0].get() && @@ -122,11 +114,96 @@ bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_vector& deps) { for (unsigned i = 0; i < lhs.size(); ++i) { m.push_back(m_lhs.back(), lhs[i].get()); m.push_back(m_rhs.back(), rhs[i].get()); - // TBD m_deps.push_back(deps); + m_dam.push_back(m_deps.back(), deps); } return true; } +bool theory_seq::solve_unit_eq(expr* l, expr* r, enode_pair_dependency* deps) { + expr_ref lh = canonize(l, deps); + expr_ref rh = canonize(r, deps); + if (is_var(lh) && !occurs(lh, rh)) { + add_solution(lh, rh, deps); + return true; + } + if (is_var(rh) && !occurs(rh, lh)) { + add_solution(rh, lh, deps); + return true; + } + // Use instead reference counts for dependencies to GC? + + return false; +} + +bool theory_seq::occurs(expr* a, expr* b) { + // TBD + return true; +} + +bool theory_seq::is_var(expr* a) { + // TBD + return false; +} + +void theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) { + context& ctx = get_context(); + // TBD: internalize lh, rh; + // + enode* n1 = ctx.get_enode(l); + enode* n2 = ctx.get_enode(r); + // TBD: add substitution l -> r + vector _eqs; + m_dm.linearize(deps, _eqs); + // alloc? + ctx.assign_eq(n1, n2, eq_justification( + alloc(ext_theory_eq_propagation_justification, + get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), n1, n2))); +} + +bool theory_seq::simplify_eqs() { + return pre_process_eqs(true); +} + +bool theory_seq::solve_basic_eqs() { + return pre_process_eqs(false); +} + +bool theory_seq::pre_process_eqs(bool simplify_or_solve) { + context& ctx = get_context(); + bool change = false; + expr_array& lhs = m_lhs.back(); + expr_array& rhs = m_rhs.back(); + enode_pair_dependency_array& deps = m_deps.back(); + for (unsigned i = 0; !ctx.inconsistent() && i < m.size(lhs); ++i) { + if (simplify_or_solve? + simplify_eq(m.get(lhs, i), m.get(rhs, i), m_dam.get(deps, i)): + solve_unit_eq(m.get(lhs, i), m.get(rhs, i), m_dam.get(deps, i))) { + if (i + 1 != m.size(lhs)) { + m.set(lhs, i, m.get(lhs, m.size(lhs)-1)); + m.set(rhs, i, m.get(rhs, m.size(rhs)-1)); + m_dam.set(deps, i, m_dam.get(deps, m_dam.size(deps)-1)); + --i; + change = true; + } + m.pop_back(lhs); + m.pop_back(rhs); + m_dam.pop_back(deps); + } + } + return change; +} + +bool theory_seq::simplify_and_solve_eqs() { + context & ctx = get_context(); + bool change = simplify_eqs(); + while (!ctx.inconsistent() && solve_basic_eqs()) { + simplify_eqs(); + change = true; + } + return change; +} + + final_check_status theory_seq::add_axioms() { for (unsigned i = 0; i < get_num_vars(); ++i) { @@ -140,7 +217,6 @@ bool theory_seq::internalize_atom(app* a, bool) { } bool theory_seq::internalize_term(app* term) { - m_used = true; context & ctx = get_context(); unsigned num_args = term->get_num_args(); for (unsigned i = 0; i < num_args; i++) { @@ -159,11 +235,26 @@ bool theory_seq::internalize_term(app* term) { theory_var v = mk_var(e); ctx.attach_th_var(e, this, v); } + if (!m_util.str.is_concat(term) && + !m_util.str.is_string(term) && + !m_util.str.is_suffix(term) && + !m_util.str.is_prefix(term) && + !m_util.str.is_contains(term)) { + set_incomplete(term); + } + // assert basic axioms - if (!m_used) { m_trail_stack.push(value_trail(m_used)); m_used = true; } return true; } +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(m_incomplete)); + m_incomplete = true; + } +} + theory_var theory_seq::mk_var(enode* n) { theory_var r = theory::mk_var(n); VERIFY(r == m_find.mk_var()); @@ -175,14 +266,13 @@ bool theory_seq::can_propagate() { return m_axioms_head < m_axioms.size(); } -expr_ref theory_seq::canonize(expr* e, enode_pair_vector& eqs) { - eqs.reset(); +expr_ref theory_seq::canonize(expr* e, enode_pair_dependency*& eqs) { expr_ref result = expand(e, eqs); m_rewrite(result); return result; } -expr_ref theory_seq::expand(expr* e, enode_pair_vector& eqs) { +expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) { context& ctx = get_context(); expr* e1, *e2; SASSERT(ctx.e_internalized(e)); @@ -191,27 +281,27 @@ expr_ref theory_seq::expand(expr* e, enode_pair_vector& eqs) { do { e = n->get_owner(); if (m_util.str.is_concat(e, e1, e2)) { - if (start != n) eqs.push_back(enode_pair(start, n)); + add_dependency(eqs, start, n); return expr_ref(m_util.str.mk_concat(expand(e1, eqs), expand(e2, eqs)), m); } if (m_util.str.is_empty(e) || m_util.str.is_string(e)) { - if (start != n) eqs.push_back(enode_pair(start, n)); + add_dependency(eqs, start, n); return expr_ref(e, m); } if (m.is_eq(e, e1, e2)) { - if (start != n) eqs.push_back(enode_pair(start, n)); + add_dependency(eqs, start, n); return expr_ref(m.mk_eq(expand(e1, eqs), expand(e2, eqs)), m); } if (m_util.str.is_prefix(e, e1, e2)) { - if (start != n) eqs.push_back(enode_pair(start, n)); + add_dependency(eqs, start, n); return expr_ref(m_util.str.mk_prefix(expand(e1, eqs), expand(e2, eqs)), m); } if (m_util.str.is_suffix(e, e1, e2)) { - if (start != n) eqs.push_back(enode_pair(start, n)); + add_dependency(eqs, start, n); return expr_ref(m_util.str.mk_suffix(expand(e1, eqs), expand(e2, eqs)), m); } if (m_util.str.is_contains(e, e1, e2)) { - if (start != n) eqs.push_back(enode_pair(start, n)); + add_dependency(eqs, start, n); return expr_ref(m_util.str.mk_contains(expand(e1, eqs), expand(e2, eqs)), m); } #if 0 @@ -227,6 +317,20 @@ expr_ref theory_seq::expand(expr* e, enode_pair_vector& eqs) { return expr_ref(n->get_root()->get_owner(), m); } +void theory_seq::add_dependency(enode_pair_dependency*& dep, enode* a, enode* b) { + dep = join(dep, leaf(a, b)); +} + +theory_seq::enode_pair_dependency* theory_seq::join(enode_pair_dependency* a, enode_pair_dependency* b) { + if (!a) return b; + if (!b) return a; + return m_dm.mk_join(a, b); +} + +theory_seq::enode_pair_dependency* theory_seq::leaf(enode* a, enode* b) { + return (a == b)?0:m_dm.mk_leaf(std::make_pair(a, b)); +} + void theory_seq::propagate() { context & ctx = get_context(); while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) { @@ -328,26 +432,33 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { void theory_seq::push_scope_eh() { theory::push_scope_eh(); + m_dm.push_scope(); m_trail_stack.push_scope(); m_trail_stack.push(value_trail(m_axioms_head)); m_trail_stack.push(value_trail(m_eqs_head)); expr_array lhs, rhs; + enode_pair_dependency_array deps; m.copy(m_lhs.back(), lhs); m.copy(m_rhs.back(), rhs); + m_dam.copy(m_deps.back(), deps); m_lhs.push_back(lhs); m_rhs.push_back(rhs); + m_deps.push_back(deps); } void theory_seq::pop_scope_eh(unsigned num_scopes) { m_trail_stack.pop_scope(num_scopes); - theory::pop_scope_eh(num_scopes); + theory::pop_scope_eh(num_scopes); + m_dm.pop_scope(num_scopes); m_rep.resize(get_num_vars()); while (num_scopes > 0) { --num_scopes; m.del(m_lhs.back()); m.del(m_rhs.back()); + m_dam.del(m_deps.back()); m_lhs.pop_back(); m_rhs.pop_back(); + m_deps.pop_back(); } } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 3a7b978e9..236a34a04 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -28,6 +28,22 @@ Revision History: namespace smt { class theory_seq : public theory { + struct config { + static const bool preserve_roots = true; + static const unsigned max_trail_sz = 16; + static const unsigned factor = 2; + typedef small_object_allocator allocator; + }; + typedef scoped_dependency_manager enode_pair_dependency_manager; + typedef enode_pair_dependency_manager::dependency enode_pair_dependency; + struct enode_pair_dependency_array_config : public config { + typedef enode_pair_dependency* value; + typedef dummy_value_manager value_manager; + static const bool ref_count = false; + }; + typedef parray_manager enode_pair_dependency_array_manager; + typedef enode_pair_dependency_array_manager::ref enode_pair_dependency_array; + typedef union_find th_union_find; typedef trail_stack th_trail_stack; struct stats { @@ -35,17 +51,23 @@ namespace smt { void reset() { memset(this, 0, sizeof(stats)); } unsigned m_num_splits; }; - ast_manager& m; - expr_ref_vector m_rep; // unification representative. - vector m_lhs, m_rhs; // persistent sets of equalities. - unsigned m_eqs_head; // index of unprocessed equation. - enode_pair_vector m_deps; // TBD - convert to dependency structure. + ast_manager& m; + small_object_allocator m_alloc; + enode_pair_dependency_array_config::value_manager m_dep_array_value_manager; + enode_pair_dependency_manager m_dm; + enode_pair_dependency_array_manager m_dam; + expr_ref_vector m_rep; // unification representative. + vector m_lhs, m_rhs; // persistent sets of equalities. + vector m_deps; + + unsigned m_eqs_head; // index of unprocessed equation. deprecate + expr_ref_vector m_ineqs; // inequalities to check expr_ref_vector m_axioms; unsigned m_axioms_head; - bool m_used; // deprecate + bool m_incomplete; th_rewriter m_rewrite; seq_util m_util; arith_util m_autil; @@ -69,18 +91,31 @@ namespace smt { virtual char const * get_name() const { return "seq"; } virtual theory_var mk_var(enode* n); - final_check_status check_ineqs(); + bool check_ineqs(); + bool pre_process_eqs(bool simplify_or_solve); bool simplify_eqs(); - bool simplify_eq(expr* l, expr* r, enode_pair_vector& deps); + bool simplify_eq(expr* l, expr* r, enode_pair_dependency* deps); + bool solve_unit_eq(expr* l, expr* r, enode_pair_dependency* deps); + bool solve_basic_eqs(); + bool simplify_and_solve_eqs(); + bool occurs(expr* a, expr* b); + bool is_var(expr* b); + void add_solution(expr* l, expr* r, enode_pair_dependency* dep); + final_check_status add_axioms(); void assert_axiom(expr_ref& e); void create_axiom(expr_ref& e); - expr_ref canonize(expr* e, enode_pair_vector& eqs); - expr_ref expand(expr* e, enode_pair_vector& eqs); + 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); + enode_pair_dependency* leaf(enode* a, enode* b); + enode_pair_dependency* join(enode_pair_dependency* a, enode_pair_dependency* b); void propagate_eq(bool_var v, expr* e1, expr* e2); expr_ref mk_skolem(char const* name, expr* e1, expr* e2); + + void set_incomplete(app* term); public: theory_seq(ast_manager& m); virtual void init_model(model_generator & mg) { From 6c2e7e767521f81112b9801835a2f12a57cb477b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Dec 2015 16:03:24 -0800 Subject: [PATCH 5/9] seq Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 209 +++++++++++++++++++++++++++-------------- src/smt/theory_seq.h | 31 ++++-- 2 files changed, 164 insertions(+), 76 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 1494b3afd..48b034965 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -25,12 +25,59 @@ Revision History: using namespace smt; +void theory_seq::solution_map::update(expr* e, expr* r, enode_pair_dependency* d) { + std::pair 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); + } + 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); +} + +expr* theory_seq::solution_map::find(expr* e, enode_pair_dependency*& d) { + std::pair value; + if (m_map.find(e, value)) { + d = value.second; + return value.first; + } + else { + d = 0; + return e; + } +} + +void theory_seq::solution_map::pop_scope(unsigned num_scopes) { + if (num_scopes == 0) return; + unsigned start = m_limit[m_limit.size() - num_scopes]; + for (unsigned i = m_updates.size(); i > start; ) { + --i; + if (m_updates[i] == INS) { + m_map.remove(m_lhs[i].get()); + } + else { + m_map.insert(m_lhs[i].get(), std::make_pair(m_rhs[i].get(), m_deps[i])); + } + } + m_updates.resize(start); + m_lhs.resize(start); + m_rhs.resize(start); + m_deps.resize(start); + m_limit.resize(m_limit.size() - num_scopes); +} + 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_eqs_head(0), m_ineqs(m), m_axioms(m), m_axioms_head(0), @@ -38,8 +85,7 @@ theory_seq::theory_seq(ast_manager& m): m_rewrite(m), m_util(m), m_autil(m), - m_trail_stack(*this), - m_find(*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()); @@ -122,6 +168,9 @@ bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_dependency* deps) { bool theory_seq::solve_unit_eq(expr* l, expr* r, enode_pair_dependency* deps) { expr_ref lh = canonize(l, deps); expr_ref rh = canonize(r, deps); + if (lh == rh) { + return true; + } if (is_var(lh) && !occurs(lh, rh)) { add_solution(lh, rh, deps); return true; @@ -132,32 +181,55 @@ bool theory_seq::solve_unit_eq(expr* l, expr* r, enode_pair_dependency* deps) { } // Use instead reference counts for dependencies to GC? + // TBD: Solutions to units are not necessarily variables, but + // they may induce new equations. + return false; } bool theory_seq::occurs(expr* a, expr* b) { - // TBD - return true; -} - -bool theory_seq::is_var(expr* a) { - // TBD + SASSERT(is_var(a)); + // true if a occurs under an interpreted function or under left/right selector. + if (a == b) { + return true; + } + expr* e1, *e2; + if (m_util.str.is_concat(b, e1, e2)) { + return occurs(a, e1) || occurs(a, e2); + } + if (is_left_select(b, e1) || is_right_select(b, e1)) { + return occurs(a, e1); + } return false; } +bool theory_seq::is_var(expr* a) { + return is_uninterp(a); +} + +bool theory_seq::is_left_select(expr* a, expr*& b) { + return false; +} + +bool theory_seq::is_right_select(expr* a, expr*& b) { + return false; +} + + void theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) { context& ctx = get_context(); - // TBD: internalize lh, rh; - // - enode* n1 = ctx.get_enode(l); - enode* n2 = ctx.get_enode(r); - // TBD: add substitution l -> r - vector _eqs; - m_dm.linearize(deps, _eqs); - // alloc? - ctx.assign_eq(n1, n2, eq_justification( - alloc(ext_theory_eq_propagation_justification, - get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), n1, n2))); + 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); + vector _eqs; + m_dm.linearize(deps, _eqs); + // alloc? + ctx.assign_eq(n1, n2, eq_justification( + alloc(ext_theory_eq_propagation_justification, + get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), n1, n2))); + } } bool theory_seq::simplify_eqs() { @@ -237,6 +309,8 @@ bool theory_seq::internalize_term(app* term) { } if (!m_util.str.is_concat(term) && !m_util.str.is_string(term) && + !m_util.str.is_empty(term) && + !m_util.str.is_unit(term) && !m_util.str.is_suffix(term) && !m_util.str.is_prefix(term) && !m_util.str.is_contains(term)) { @@ -247,6 +321,13 @@ bool theory_seq::internalize_term(app* term) { return true; } +void theory_seq::apply_sort_cnstr(enode* n, sort* s) { + if (!is_attached_to_var(n)) { + mk_var(n); + } +} + + void theory_seq::set_incomplete(app* term) { TRACE("seq", tout << "No support for: " << mk_pp(term, m) << "\n";); if (!m_incomplete) { @@ -257,8 +338,6 @@ void theory_seq::set_incomplete(app* term) { theory_var theory_seq::mk_var(enode* n) { theory_var r = theory::mk_var(n); - VERIFY(r == m_find.mk_var()); - m_rep.push_back(n->get_owner()); return r; } @@ -273,48 +352,29 @@ expr_ref theory_seq::canonize(expr* e, enode_pair_dependency*& eqs) { } expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) { - context& ctx = get_context(); + enode_pair_dependency* deps = 0; + e = m_rep.find(e, deps); expr* e1, *e2; - SASSERT(ctx.e_internalized(e)); - enode* n = ctx.get_enode(e); - enode* start = n; - do { - e = n->get_owner(); - if (m_util.str.is_concat(e, e1, e2)) { - add_dependency(eqs, start, n); - return expr_ref(m_util.str.mk_concat(expand(e1, eqs), expand(e2, eqs)), m); - } - if (m_util.str.is_empty(e) || m_util.str.is_string(e)) { - add_dependency(eqs, start, n); - return expr_ref(e, m); - } - if (m.is_eq(e, e1, e2)) { - add_dependency(eqs, start, n); - return expr_ref(m.mk_eq(expand(e1, eqs), expand(e2, eqs)), m); - } - if (m_util.str.is_prefix(e, e1, e2)) { - add_dependency(eqs, start, n); - return expr_ref(m_util.str.mk_prefix(expand(e1, eqs), expand(e2, eqs)), m); - } - if (m_util.str.is_suffix(e, e1, e2)) { - add_dependency(eqs, start, n); - return expr_ref(m_util.str.mk_suffix(expand(e1, eqs), expand(e2, eqs)), m); - } - if (m_util.str.is_contains(e, e1, e2)) { - add_dependency(eqs, start, n); - return expr_ref(m_util.str.mk_contains(expand(e1, eqs), expand(e2, eqs)), m); - } -#if 0 - if (m_util.str.is_unit(e)) { - // TBD: canonize the element. - if (start != n) eqs.push_back(enode_pair(start, n)); - return expr_ref(e, m); - } -#endif - n = n->get_next(); + eqs = join(eqs, deps); + if (m_util.str.is_concat(e, e1, e2)) { + return expr_ref(m_util.str.mk_concat(expand(e1, eqs), expand(e2, eqs)), m); + } + if (m_util.str.is_empty(e) || m_util.str.is_string(e)) { + return expr_ref(e, m); } - while (n != start); - return expr_ref(n->get_root()->get_owner(), m); + if (m.is_eq(e, e1, e2)) { + return expr_ref(m.mk_eq(expand(e1, eqs), expand(e2, eqs)), m); + } + if (m_util.str.is_prefix(e, e1, e2)) { + return expr_ref(m_util.str.mk_prefix(expand(e1, eqs), expand(e2, eqs)), m); + } + if (m_util.str.is_suffix(e, e1, e2)) { + return expr_ref(m_util.str.mk_suffix(expand(e1, eqs), expand(e2, eqs)), m); + } + if (m_util.str.is_contains(e, e1, e2)) { + return expr_ref(m_util.str.mk_contains(expand(e1, eqs), expand(e2, eqs)), m); + } + return expr_ref(e, m); } void theory_seq::add_dependency(enode_pair_dependency*& dep, enode* a, enode* b) { @@ -415,12 +475,11 @@ void theory_seq::assign_eq(bool_var v, bool is_true) { } void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { - m_find.merge(v1, v2); - expr_ref e1(m), e2(m); - e1 = get_enode(v1)->get_owner(); - e2 = get_enode(v2)->get_owner(); - m.push_back(m_lhs.back(), get_enode(v1)->get_owner()); - m.push_back(m_rhs.back(), get_enode(v2)->get_owner()); + enode* n1 = get_enode(v1); + enode* n2 = get_enode(v2); + m.push_back(m_lhs.back(), n1->get_owner()); + m.push_back(m_rhs.back(), n2->get_owner()); + m_dam.push_back(m_deps.back(), leaf(n1, n2)); } void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { @@ -432,10 +491,10 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { void theory_seq::push_scope_eh() { theory::push_scope_eh(); + m_rep.push_scope(); m_dm.push_scope(); m_trail_stack.push_scope(); m_trail_stack.push(value_trail(m_axioms_head)); - m_trail_stack.push(value_trail(m_eqs_head)); expr_array lhs, rhs; enode_pair_dependency_array deps; m.copy(m_lhs.back(), lhs); @@ -450,7 +509,7 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) { m_trail_stack.pop_scope(num_scopes); theory::pop_scope_eh(num_scopes); m_dm.pop_scope(num_scopes); - m_rep.resize(get_num_vars()); + m_rep.pop_scope(num_scopes); while (num_scopes > 0) { --num_scopes; m.del(m_lhs.back()); @@ -463,6 +522,16 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) { } void theory_seq::restart_eh() { + SASSERT(m_lhs.size() == 1); + m.del(m_lhs.back()); + m.del(m_rhs.back()); + m_dam.del(m_deps.back()); + m_lhs.reset(); + m_rhs.reset(); + m_deps.reset(); + m_lhs.push_back(expr_array()); + m_rhs.push_back(expr_array()); + m_deps.push_back(enode_pair_dependency_array()); } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 236a34a04..505b3aa5e 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -46,6 +46,23 @@ namespace smt { typedef union_find th_union_find; typedef trail_stack th_trail_stack; + + class solution_map { + enum map_update { INS, DEL }; + ast_manager& m; + obj_map > m_map; + expr_ref_vector m_lhs, m_rhs; + ptr_vector m_deps; + svector m_updates; + unsigned_vector m_limit; + public: + solution_map(ast_manager& m): m(m), m_lhs(m), m_rhs(m) {} + 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()); } + void pop_scope(unsigned num_scopes); + }; + struct stats { stats() { reset(); } void reset() { memset(this, 0, sizeof(stats)); } @@ -56,12 +73,9 @@ namespace smt { enode_pair_dependency_array_config::value_manager m_dep_array_value_manager; enode_pair_dependency_manager m_dm; enode_pair_dependency_array_manager m_dam; - expr_ref_vector m_rep; // unification representative. + solution_map m_rep; // unification representative. vector m_lhs, m_rhs; // persistent sets of equalities. - vector m_deps; - - unsigned m_eqs_head; // index of unprocessed equation. deprecate - + vector m_deps; // persistent sets of dependencies. expr_ref_vector m_ineqs; // inequalities to check @@ -72,7 +86,6 @@ namespace smt { seq_util m_util; arith_util m_autil; th_trail_stack m_trail_stack; - th_union_find m_find; stats m_stats; virtual final_check_status final_check_eh(); @@ -90,6 +103,7 @@ namespace smt { virtual theory* mk_fresh(context* new_ctx) { return alloc(theory_seq, new_ctx->get_manager()); } virtual char const * get_name() const { return "seq"; } virtual theory_var mk_var(enode* n); + virtual void apply_sort_cnstr(enode* n, sort* s); bool check_ineqs(); bool pre_process_eqs(bool simplify_or_solve); @@ -101,6 +115,9 @@ namespace smt { 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(); @@ -122,10 +139,12 @@ namespace smt { mg.register_factory(alloc(seq_factory, get_manager(), get_family_id(), mg.get_model())); } +#if 0 th_trail_stack & get_trail_stack() { return m_trail_stack; } virtual void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var); static void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {} void unmerge_eh(theory_var v1, theory_var v2); +#endif }; }; From 24de0a9b908321fed4ee76a09b346737939dc447 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Dec 2015 16:37:08 -0800 Subject: [PATCH 6/9] seq Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 15 +++++++-------- src/smt/theory_seq.h | 5 +++-- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 48b034965..213e671db 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -44,14 +44,13 @@ void theory_seq::solution_map::update(expr* e, expr* r, enode_pair_dependency* d expr* theory_seq::solution_map::find(expr* e, enode_pair_dependency*& d) { std::pair value; - if (m_map.find(e, value)) { - d = value.second; - return value.first; - } - else { - d = 0; - return e; + d = 0; + // TBD add path compression? + while (m_map.find(e, value)) { + d = d ? m_dm.mk_join(d, value.second) : value.second;; + e = value.first; } + return e; } void theory_seq::solution_map::pop_scope(unsigned num_scopes) { @@ -77,7 +76,7 @@ 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_rep(m, m_dm), m_ineqs(m), m_axioms(m), m_axioms_head(0), diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 505b3aa5e..4aee7e61c 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -46,17 +46,18 @@ namespace smt { typedef union_find th_union_find; typedef trail_stack th_trail_stack; - + class solution_map { enum map_update { INS, DEL }; ast_manager& m; + enode_pair_dependency_manager& m_dm; obj_map > m_map; expr_ref_vector m_lhs, m_rhs; ptr_vector m_deps; svector m_updates; unsigned_vector m_limit; public: - solution_map(ast_manager& m): m(m), m_lhs(m), m_rhs(m) {} + solution_map(ast_manager& m, enode_pair_dependency_manager& dm): m(m), m_dm(dm), m_lhs(m), m_rhs(m) {} 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()); } From 94bd2fdbe41b65fecb0ea6153e8e373936932c04 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Dec 2015 21:03:28 -0800 Subject: [PATCH 7/9] seq Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 49 ++++++- src/ast/rewriter/seq_rewriter.h | 2 + src/ast/seq_decl_plugin.cpp | 24 +++- src/ast/seq_decl_plugin.h | 6 + src/smt/theory_seq.cpp | 207 +++++++++++++++++++++++------- src/smt/theory_seq.h | 49 +++---- src/smt/theory_seq_empty.h | 26 +++- 7 files changed, 285 insertions(+), 78 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index ef73bd2f2..072471898 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -636,7 +636,12 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve } change = true; } + + 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; + } lhs.push_back(l); rhs.push_back(r); } @@ -649,7 +654,13 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve else if (head2 == m_rhs.size()) { return set_empty(m_lhs.size() - head1, m_lhs.c_ptr() + head1, lhs, rhs); } - else { // head1 < m_lhs.size() && head2 < m_rhs.size() // could solve if either side is fixed size. + 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; + } + 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)); } @@ -674,3 +685,39 @@ bool seq_rewriter::set_empty(unsigned sz, expr* const* es, expr_ref_vector& lhs, } return true; } + +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; + if (szl == szr) return false; + if (szr < szl) { + std::swap(szl, szr); + std::swap(l, r); + } + + for (unsigned i = 1; i + szl <= szr; ++i) { + bool eq = true; + for (unsigned j = 0; eq && j < szl; ++j) { + eq = l[j] == r[i+j]; + } + if (eq) { + SASSERT(szr >= i + szl); + is_sat = set_empty(i, r, lhs, rhs); + is_sat &= set_empty(szr - (i + szl), r + i + szl, lhs, rhs); + + TRACE("seq", + for (unsigned k = 0; k < szl; ++k) { + tout << mk_pp(l[k], m()) << " "; + } + tout << "\n"; + for (unsigned k = 0; k < szr; ++k) { + tout << mk_pp(r[k], m()) << " "; + } + tout << "\n"; + tout << lhs << "; " << rhs << "\n";); + + return true; + } + } + return false; +} diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 57926efdf..d4652f614 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -54,6 +54,8 @@ class seq_rewriter { 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 is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r, + expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat); public: seq_rewriter(ast_manager & m, params_ref const & p = params_ref()): m_util(m), m_autil(m) { diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 77e57b07c..7973d0b6e 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -47,7 +47,7 @@ bool seq_decl_plugin::match(ptr_vector& binding, sort* s, sort* sP) { 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";); + TRACE("seq_verbose", tout << "setting binding @ " << i << " to " << mk_pp(s, m) << "\n";); binding[i] = s; return true; } @@ -77,7 +77,7 @@ bool seq_decl_plugin::match(ptr_vector& 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 binding; ast_manager& m = *m_manager; - TRACE("seq", + TRACE("seq_verbose", 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); @@ -102,7 +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";); + TRACE("seq_verbose", 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) { @@ -321,18 +321,27 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters)); case OP_SEQ_CONCAT: { + if (arity < 2) { + m.raise_exception("invalid concatenation. At least two arguments expected"); + } 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 < 2) { + m.raise_exception("invalid concatenation. At least two arguments expected"); + } 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 < 2) { + m.raise_exception("invalid string concatenation. At least two arguments 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(); @@ -386,6 +395,8 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, 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)); default: UNREACHABLE(); return 0; @@ -419,6 +430,13 @@ bool seq_decl_plugin::is_value(app* e) const { return is_app_of(e, m_family_id, OP_STRING_CONST); } +app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) { + parameter param(name); + func_decl* f = m.mk_func_decl(get_family_id(), _OP_SEQ_SKOLEM, 1, ¶m, n, args, range); + return m.mk_app(f, n, args); +} + + app* seq_util::str::mk_string(symbol const& s) { return u.seq.mk_string(s); } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index c317f8236..c11f830b4 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -74,6 +74,7 @@ enum seq_op_kind { _OP_STRING_TO_REGEXP, _OP_STRING_CHARAT, _OP_STRING_SUBSTR, + _OP_SEQ_SKOLEM, LAST_SEQ_OP }; @@ -155,6 +156,11 @@ 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_seq(expr* e) const { return is_seq(m.get_sort(e)); } + bool is_re(expr* e) const { return is_re(m.get_sort(e)); } + + 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); } class str { seq_util& u; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 213e671db..befe7b419 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -72,6 +72,14 @@ void theory_seq::solution_map::pop_scope(unsigned num_scopes) { m_limit.resize(m_limit.size() - num_scopes); } +void theory_seq::solution_map::display(std::ostream& out) const { + map_t::iterator it = m_map.begin(), end = m_map.end(); + for (; it != end; ++it) { + out << mk_pp(it->m_key, m) << " |-> " << mk_pp(it->m_value.first, m) << "\n"; + } +} + + theory_seq::theory_seq(ast_manager& m): theory(m.mk_family_id("seq")), m(m), @@ -88,10 +96,17 @@ theory_seq::theory_seq(ast_manager& m): 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"; } final_check_status theory_seq::final_check_eh() { context & ctx = get_context(); + TRACE("seq", display(tout);); if (!check_ineqs()) { return FC_CONTINUE; } @@ -111,44 +126,50 @@ bool theory_seq::check_ineqs() { enode_pair_dependency* eqs = 0; expr_ref b = canonize(a, eqs); if (m.is_true(b)) { + TRACE("seq", tout << "Evaluates to false: " << a << "\n";); ctx.internalize(a, false); literal lit(ctx.get_literal(a)); - ctx.mark_as_relevant(lit); - vector _eqs; - m_dm.linearize(eqs, _eqs); - ctx.assign( - lit, - ctx.mk_justification( - ext_theory_propagation_justification( - get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), lit))); + propagate(lit, eqs); return false; } } return true; } +void theory_seq::propagate(literal lit, enode_pair_dependency* dep) { + context& ctx = get_context(); + ctx.mark_as_relevant(lit); + vector _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"; + } + ); + + ctx.assign( + lit, + ctx.mk_justification( + ext_theory_propagation_justification( + get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), lit))); +} + + bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_dependency* deps) { context& ctx = get_context(); seq_rewriter rw(m); expr_ref_vector lhs(m), rhs(m); - SASSERT(ctx.e_internalized(l)); - SASSERT(ctx.e_internalized(r)); expr_ref lh = canonize(l, deps); expr_ref rh = canonize(r, deps); if (!rw.reduce_eq(l, r, lhs, rhs)) { // equality is inconsistent. // create conflict assignment. - expr_ref a(m); - a = m.mk_eq(l, r); - literal lit(ctx.get_literal(a)); - vector _eqs; - m_dm.linearize(deps, _eqs); - ctx.assign( - ~lit, - ctx.mk_justification( - ext_theory_propagation_justification( - get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), ~lit))); + literal lit(mk_eq(l, r, false)); + propagate(~lit, deps); return true; } if (lhs.size() == 1 && l == lhs[0].get() && @@ -161,6 +182,13 @@ bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_dependency* deps) { m.push_back(m_rhs.back(), rhs[i].get()); m_dam.push_back(m_deps.back(), deps); } + TRACE("seq", + tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " => "; + for (unsigned i = 0; i < lhs.size(); ++i) { + tout << mk_pp(lhs[i].get(), m) << " = " << mk_pp(rhs[i].get(), m) << "; "; + } + tout << "\n"; + ); return true; } @@ -187,31 +215,36 @@ bool theory_seq::solve_unit_eq(expr* l, expr* r, enode_pair_dependency* deps) { } bool theory_seq::occurs(expr* a, expr* b) { + // true if a occurs under an interpreted function or under left/right selector. SASSERT(is_var(a)); - // true if a occurs under an interpreted function or under left/right selector. - if (a == b) { - return true; - } expr* e1, *e2; + while (is_left_select(a, e1) || is_right_select(a, e1)) { + a = e1; + } if (m_util.str.is_concat(b, e1, e2)) { return occurs(a, e1) || occurs(a, e2); } - if (is_left_select(b, e1) || is_right_select(b, e1)) { - return occurs(a, e1); - } + while (is_left_select(b, e1) || is_right_select(b, e1)) { + b = e1; + } + if (a == b) { + return true; + } return false; } bool theory_seq::is_var(expr* a) { - return is_uninterp(a); + return is_uninterp(a) || m_util.is_skolem(a); } bool theory_seq::is_left_select(expr* a, expr*& b) { - return false; + return m_util.is_skolem(a) && + to_app(a)->get_decl()->get_parameter(0).get_symbol() == m_left_sym && (b = to_app(a)->get_arg(0), true); } bool theory_seq::is_right_select(expr* a, expr*& b) { - return false; + return m_util.is_skolem(a) && + to_app(a)->get_decl()->get_parameter(0).get_symbol() == m_right_sym && (b = to_app(a)->get_arg(0), true); } @@ -224,10 +257,18 @@ void theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) { enode* n2 = ctx.get_enode(r); vector _eqs; m_dm.linearize(deps, _eqs); - // alloc? - ctx.assign_eq(n1, n2, eq_justification( - alloc(ext_theory_eq_propagation_justification, - get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), n1, n2))); + 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"; + } + ); + + justification* js = ctx.mk_justification( + ext_theory_eq_propagation_justification( + get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), n1, n2)); + ctx.assign_eq(n1, n2, eq_justification(js)); } } @@ -254,6 +295,7 @@ bool theory_seq::pre_process_eqs(bool simplify_or_solve) { m.set(rhs, i, m.get(rhs, m.size(rhs)-1)); m_dam.set(deps, i, m_dam.get(deps, m_dam.size(deps)-1)); --i; + ++m_stats.m_num_reductions; change = true; } m.pop_back(lhs); @@ -312,7 +354,8 @@ bool theory_seq::internalize_term(app* term) { !m_util.str.is_unit(term) && !m_util.str.is_suffix(term) && !m_util.str.is_prefix(term) && - !m_util.str.is_contains(term)) { + !m_util.str.is_contains(term) && + !m_util.is_skolem(term)) { set_incomplete(term); } @@ -326,6 +369,70 @@ void theory_seq::apply_sort_cnstr(enode* n, sort* s) { } } +void theory_seq::display(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 _eqs; + const_cast(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 { + st.update("seq num splits", m_stats.m_num_splits); + st.update("seq num reductions", m_stats.m_num_reductions); +} + +void theory_seq::init_model(model_generator & mg) { + 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(m); + canonize(e, deps); + SASSERT(is_app(e)); + m_factory->add_trail(e); + return alloc(expr_wrapper_proc, to_app(e)); +} + + void theory_seq::set_incomplete(app* term) { TRACE("seq", tout << "No support for: " << mk_pp(term, m) << "\n";); @@ -413,27 +520,29 @@ void theory_seq::assert_axiom(expr_ref& e) { literal lit(ctx.get_literal(e)); ctx.mark_as_relevant(lit); ctx.mk_th_axiom(get_id(), 1, &lit); - } -expr_ref theory_seq::mk_skolem(char const* name, expr* e1, expr* e2) { +expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2) { expr_ref result(m); - sort* s = m.get_sort(e1); - SASSERT(s == m.get_sort(e2)); - sort* ss[2] = { s, s }; - result = m.mk_app(m.mk_func_decl(symbol("#prefix_eq"), 2, ss, s), e1, e2); + expr* es[2] = { e1, e2 }; + result = m_util.mk_skolem(name, 2, es, m.get_sort(e1)); return result; } void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) { context& ctx = get_context(); + TRACE("seq", + tout << mk_pp(ctx.bool_var2enode(v)->get_owner(), m) << " => " + << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";); + ctx.internalize(e1, false); enode* n1 = ctx.get_enode(e1); enode* n2 = ctx.get_enode(e2); literal lit(v); - ctx.assign_eq(n1, n2, eq_justification( - alloc(ext_theory_eq_propagation_justification, - get_id(), ctx.get_region(), 1, &lit, 0, 0, n1, n2))); + justification* js = ctx.mk_justification(ext_theory_eq_propagation_justification( + get_id(), ctx.get_region(), 1, &lit, 0, 0, n1, n2)); + + ctx.assign_eq(n1, n2, eq_justification(js)); } void theory_seq::assign_eq(bool_var v, bool is_true) { @@ -445,18 +554,18 @@ void theory_seq::assign_eq(bool_var v, bool is_true) { expr* e1, *e2; expr_ref f(m); if (m_util.str.is_prefix(e, e1, e2)) { - f = mk_skolem("#prefix_eq", e1, e2); + f = mk_skolem(m_prefix_sym, e1, e2); f = m_util.str.mk_concat(e1, f); propagate_eq(v, f, e2); } else if (m_util.str.is_suffix(e, e1, e2)) { - f = mk_skolem("#suffix_eq", e1, e2); + f = mk_skolem(m_suffix_sym, e1, e2); f = m_util.str.mk_concat(f, e1); propagate_eq(v, f, e2); } else if (m_util.str.is_contains(e, e1, e2)) { - expr_ref f1 = mk_skolem("#contains_eq1", e1, e2); - expr_ref f2 = mk_skolem("#contains_eq2", 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); } @@ -485,7 +594,7 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { expr* e1 = get_enode(v1)->get_owner(); expr* e2 = get_enode(v2)->get_owner(); m_trail_stack.push(push_back_vector(m_ineqs)); - m_ineqs.push_back(m.mk_eq(e1, e2)); + m_ineqs.push_back(mk_eq_atom(e1, e2)); } void theory_seq::push_scope_eh() { diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 4aee7e61c..63dd2bdc6 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -49,25 +49,28 @@ namespace smt { class solution_map { enum map_update { INS, DEL }; - ast_manager& m; - enode_pair_dependency_manager& m_dm; - obj_map > m_map; - expr_ref_vector m_lhs, m_rhs; + typedef obj_map > map_t; + ast_manager& m; + enode_pair_dependency_manager& m_dm; + map_t m_map; + expr_ref_vector m_lhs, m_rhs; ptr_vector m_deps; - svector m_updates; - unsigned_vector m_limit; + svector m_updates; + unsigned_vector m_limit; public: solution_map(ast_manager& m, enode_pair_dependency_manager& dm): m(m), m_dm(dm), m_lhs(m), m_rhs(m) {} 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()); } void pop_scope(unsigned num_scopes); + void display(std::ostream& out) const; }; struct stats { stats() { reset(); } void reset() { memset(this, 0, sizeof(stats)); } unsigned m_num_splits; + unsigned m_num_reductions; }; ast_manager& m; small_object_allocator m_alloc; @@ -78,7 +81,7 @@ namespace smt { vector m_lhs, m_rhs; // persistent sets of equalities. vector 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; @@ -88,13 +91,19 @@ namespace smt { arith_util m_autil; th_trail_stack m_trail_stack; stats m_stats; + symbol m_prefix_sym; + symbol m_suffix_sym; + symbol m_contains_left_sym; + symbol m_contains_right_sym; + symbol m_left_sym; + symbol m_right_sym; virtual final_check_status final_check_eh(); virtual bool internalize_atom(app*, bool); virtual bool internalize_term(app*); 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); + virtual void assign_eq(bool_var v, bool is_true); virtual bool can_propagate(); virtual void propagate(); virtual void push_scope_eh(); @@ -105,21 +114,25 @@ 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 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(); bool pre_process_eqs(bool simplify_or_solve); bool simplify_eqs(); - bool simplify_eq(expr* l, expr* r, enode_pair_dependency* deps); - bool solve_unit_eq(expr* l, expr* r, enode_pair_dependency* deps); + 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(); + void propagate(literal lit, enode_pair_dependency* dep); 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); @@ -131,21 +144,11 @@ namespace smt { enode_pair_dependency* join(enode_pair_dependency* a, enode_pair_dependency* b); void propagate_eq(bool_var v, expr* e1, expr* e2); - expr_ref mk_skolem(char const* name, expr* e1, expr* e2); + expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2); void set_incomplete(app* term); public: theory_seq(ast_manager& m); - virtual void init_model(model_generator & mg) { - mg.register_factory(alloc(seq_factory, get_manager(), get_family_id(), mg.get_model())); - } - -#if 0 - th_trail_stack & get_trail_stack() { return m_trail_stack; } - virtual void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var); - static void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {} - void unmerge_eh(theory_var v1, theory_var v2); -#endif }; }; diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index e8e619bf8..b1bab6c05 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -25,22 +25,44 @@ Revision History: namespace smt { class seq_factory : public value_factory { typedef hashtable symbol_set; + ast_manager& m; proto_model& m_model; seq_util u; symbol_set m_strings; unsigned m_next; + std::string m_unique_prefix; + obj_map m_unique_sequences; + expr_ref_vector m_trail; public: + seq_factory(ast_manager & m, family_id fid, proto_model & md): value_factory(m, fid), + m(m), m_model(md), u(m), - m_next(0) + m_next(0), + m_unique_prefix("#B"), + m_trail(m) { m_strings.insert(symbol("")); m_strings.insert(symbol("a")); m_strings.insert(symbol("b")); } + void add_trail(expr* e) { + m_trail.push_back(e); + } + + void set_prefix(char const* p) { + m_unique_prefix = p; + } + + // generic method for setting unique sequences + void set_prefix(expr* uniq) { + m_trail.push_back(uniq); + m_unique_sequences.insert(m.get_sort(uniq), uniq); + } + virtual expr* get_some_value(sort* s) { if (u.is_string(s)) return u.str.mk_string(symbol("")); @@ -60,7 +82,7 @@ namespace smt { if (u.is_string(s)) { while (true) { std::ostringstream strm; - strm << "S" << m_next++; + strm << m_unique_prefix << m_next++; symbol sym(strm.str().c_str()); if (m_strings.contains(sym)) continue; m_strings.insert(sym); From b9302e6cafcbd915032b4a1fb0df2e42ce297873 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Dec 2015 00:38:03 -0800 Subject: [PATCH 8/9] seq Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 67 ++++++++------ src/ast/seq_decl_plugin.cpp | 12 +-- src/smt/smt_setup.cpp | 5 +- src/smt/theory_seq.cpp | 148 ++++++++++++++++++------------ src/smt/theory_seq.h | 10 +- 5 files changed, 142 insertions(+), 100 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 072471898..f810b48cd 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -21,6 +21,7 @@ Notes: #include"arith_decl_plugin.h" #include"ast_pp.h" #include"ast_util.h" +#include"uint_set.h" br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { @@ -42,9 +43,14 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_RE_EMPTY_SET: case OP_RE_FULL_SET: case OP_RE_OF_PRED: + case _OP_SEQ_SKOLEM: return BR_FAILED; case OP_SEQ_CONCAT: + if (num_args == 1) { + result = args[0]; + return BR_DONE; + } SASSERT(num_args == 2); return mk_seq_concat(args[0], args[1], result); case OP_SEQ_LENGTH: @@ -588,10 +594,10 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve } // reduce strings std::string s1, s2; - if (head1 < m_lhs.size() && - head2 < m_rhs.size() && - m_util.str.is_string(m_lhs[head1], s1) && - m_util.str.is_string(m_rhs[head2], s2)) { + while (head1 < m_lhs.size() && + head2 < m_rhs.size() && + m_util.str.is_string(m_lhs[head1], s1) && + m_util.str.is_string(m_rhs[head2], s2)) { size_t l = std::min(s1.length(), s2.length()); for (size_t i = 0; i < l; ++i) { if (s1[i] != s2[i]) { @@ -614,10 +620,10 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve } change = true; } - if (head1 < m_lhs.size() && - head2 < m_rhs.size() && - m_util.str.is_string(m_lhs.back(), s1) && - m_util.str.is_string(m_rhs.back(), s2)) { + while (head1 < m_lhs.size() && + head2 < m_rhs.size() && + m_util.str.is_string(m_lhs.back(), s1) && + m_util.str.is_string(m_rhs.back(), s2)) { size_t l = std::min(s1.length(), s2.length()); for (size_t i = 0; i < l; ++i) { if (s1[s1.length()-i-1] != s2[s2.length()-i-1]) { @@ -695,29 +701,32 @@ bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, ex std::swap(l, r); } - for (unsigned i = 1; i + szl <= szr; ++i) { - bool eq = true; - for (unsigned j = 0; eq && j < szl; ++j) { - eq = l[j] == r[i+j]; + uint_set rpos; + for (unsigned i = 0; i < szl; ++i) { + bool found = false; + unsigned j = 0; + for (; !found && j < szr; ++j) { + found = !rpos.contains(j) && l[i] == r[j]; } - if (eq) { - SASSERT(szr >= i + szl); - is_sat = set_empty(i, r, lhs, rhs); - is_sat &= set_empty(szr - (i + szl), r + i + szl, lhs, rhs); - - TRACE("seq", - for (unsigned k = 0; k < szl; ++k) { - tout << mk_pp(l[k], m()) << " "; - } - tout << "\n"; - for (unsigned k = 0; k < szr; ++k) { - tout << mk_pp(r[k], m()) << " "; - } - tout << "\n"; - tout << lhs << "; " << rhs << "\n";); - + if (!found) { + return false; + } + SASSERT(0 < j && j <= szr); + rpos.insert(j-1); + } + // if we reach here, then every element of l is contained in r in some position. + ptr_vector rs; + for (unsigned j = 0; j < szr; ++j) { + if (rpos.contains(j)) { + rs.push_back(r[j]); + } + else if (!set_empty(1, r + j, lhs, rhs)) { + is_sat = false; return true; } } - return false; + 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())); + return true; } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 7973d0b6e..4022b1402 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -321,8 +321,8 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters)); case OP_SEQ_CONCAT: { - if (arity < 2) { - m.raise_exception("invalid concatenation. At least two arguments expected"); + 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, k); @@ -330,8 +330,8 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, 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 < 2) { - m.raise_exception("invalid concatenation. At least two arguments expected"); + 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, k); @@ -339,8 +339,8 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info); } case _OP_STRING_CONCAT: { - if (arity < 2) { - m.raise_exception("invalid string concatenation. At least two arguments expected"); + 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); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index edb4f1e55..8a40f9d7a 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -30,6 +30,7 @@ Revision History: #include"theory_dummy.h" #include"theory_dl.h" #include"theory_seq_empty.h" +#include"theory_seq.h" #include"theory_pb.h" #include"theory_fpa.h" @@ -200,7 +201,7 @@ namespace smt { void setup::setup_QF_BVRE() { setup_QF_BV(); setup_QF_LIA(); - m_context.register_plugin(alloc(smt::theory_seq_empty, m_manager)); + setup_seq(); } void setup::setup_QF_UF(static_features const & st) { @@ -814,7 +815,7 @@ namespace smt { } void setup::setup_seq() { - m_context.register_plugin(alloc(theory_seq_empty, m_manager)); + m_context.register_plugin(alloc(theory_seq, m_manager)); } void setup::setup_card() { diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index befe7b419..d8bc522f8 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -45,12 +45,17 @@ void theory_seq::solution_map::update(expr* e, expr* r, enode_pair_dependency* d expr* theory_seq::solution_map::find(expr* e, enode_pair_dependency*& d) { std::pair value; d = 0; - // TBD add path compression? - while (m_map.find(e, value)) { - d = d ? m_dm.mk_join(d, value.second) : value.second;; - e = value.first; + unsigned num_finds = 0; + expr* result = e; + while (m_map.find(result, value)) { + d = m_dm.mk_join(d, value.second); + result = value.first; + ++num_finds; } - return e; + if (num_finds > 1) { // path compression for original key only. + update(e, result, d); + } + return result; } void theory_seq::solution_map::pop_scope(unsigned num_scopes) { @@ -104,6 +109,15 @@ theory_seq::theory_seq(ast_manager& m): m_contains_right_sym = "contains_right"; } +theory_seq::~theory_seq() { + unsigned num_scopes = m_lhs.size()-1; + if (num_scopes > 0) pop_scope_eh(num_scopes); + m.del(m_lhs.back()); + m.del(m_rhs.back()); + m_dam.del(m_deps.back()); +} + + final_check_status theory_seq::final_check_eh() { context & ctx = get_context(); TRACE("seq", display(tout);); @@ -113,30 +127,32 @@ final_check_status theory_seq::final_check_eh() { if (simplify_and_solve_eqs()) { return FC_CONTINUE; } - if (m.size(m_lhs.back()) > 0) { + if (ctx.inconsistent()) { + return FC_CONTINUE; + } + if (m.size(m_lhs.back()) > 0 || m_incomplete) { return FC_GIVEUP; } - return m_incomplete?FC_GIVEUP:FC_DONE; + return FC_DONE; } bool theory_seq::check_ineqs() { context & ctx = get_context(); for (unsigned i = 0; i < m_ineqs.size(); ++i) { - expr_ref a(m_ineqs[i].get(), m); + expr* a = m_ineqs[i].get(); enode_pair_dependency* eqs = 0; expr_ref b = canonize(a, eqs); if (m.is_true(b)) { - TRACE("seq", tout << "Evaluates to false: " << a << "\n";); + TRACE("seq", tout << "Evaluates to false: " << mk_pp(a,m) << "\n";); ctx.internalize(a, false); - literal lit(ctx.get_literal(a)); - propagate(lit, eqs); + propagate_lit(eqs, ctx.get_literal(a)); return false; } } return true; } -void theory_seq::propagate(literal lit, enode_pair_dependency* dep) { +void theory_seq::propagate_lit(enode_pair_dependency* dep, literal lit) { context& ctx = get_context(); ctx.mark_as_relevant(lit); vector _eqs; @@ -149,12 +165,46 @@ void theory_seq::propagate(literal lit, enode_pair_dependency* dep) { << mk_pp(_eqs[i].second->get_owner(), m) << "\n"; } ); - - ctx.assign( - lit, + justification* js = ctx.mk_justification( ext_theory_propagation_justification( - get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), lit))); + get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), lit)); + + ctx.assign(lit, js); +} + +void theory_seq::set_conflict(enode_pair_dependency* dep) { + context& ctx = get_context(); + vector _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"; + } + ); + ctx.set_conflict( + ctx.mk_justification( + ext_theory_conflict_justification( + get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), 0, 0))); +} + +void theory_seq::propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2) { + context& ctx = get_context(); + vector _eqs; + 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"; + } + ); + + justification* js = ctx.mk_justification( + ext_theory_eq_propagation_justification( + get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), n1, n2)); + ctx.assign_eq(n1, n2, eq_justification(js)); } @@ -165,11 +215,10 @@ bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_dependency* deps) { expr_ref_vector lhs(m), rhs(m); expr_ref lh = canonize(l, deps); expr_ref rh = canonize(r, deps); - if (!rw.reduce_eq(l, r, lhs, rhs)) { + if (!rw.reduce_eq(lh, rh, lhs, rhs)) { // equality is inconsistent. - // create conflict assignment. - literal lit(mk_eq(l, r, false)); - propagate(~lit, deps); + TRACE("seq", tout << lh << " != " << rh << "\n";); + set_conflict(deps); return true; } if (lhs.size() == 1 && l == lhs[0].get() && @@ -255,20 +304,7 @@ void theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) { if (ctx.e_internalized(l) && ctx.e_internalized(r)) { enode* n1 = ctx.get_enode(l); enode* n2 = ctx.get_enode(r); - vector _eqs; - m_dm.linearize(deps, _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"; - } - ); - - justification* js = ctx.mk_justification( - ext_theory_eq_propagation_justification( - get_id(), ctx.get_region(), 0, 0, _eqs.size(), _eqs.c_ptr(), n1, n2)); - ctx.assign_eq(n1, n2, eq_justification(js)); + propagate_eq(deps, n1, n2); } } @@ -296,11 +332,11 @@ bool theory_seq::pre_process_eqs(bool simplify_or_solve) { m_dam.set(deps, i, m_dam.get(deps, m_dam.size(deps)-1)); --i; ++m_stats.m_num_reductions; - change = true; } m.pop_back(lhs); m.pop_back(rhs); m_dam.pop_back(deps); + change = true; } } return change; @@ -338,13 +374,13 @@ bool theory_seq::internalize_term(app* term) { if (ctx.e_internalized(term)) { return true; } - enode * e = ctx.mk_enode(term, false, m.is_bool(term), true); 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); } @@ -425,7 +461,7 @@ void theory_seq::init_model(model_generator & mg) { model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { enode_pair_dependency* deps = 0; - expr_ref e(m); + expr_ref e(n->get_owner(), m); canonize(e, deps); SASSERT(is_app(e)); m_factory->add_trail(e); @@ -443,8 +479,7 @@ void theory_seq::set_incomplete(app* term) { } theory_var theory_seq::mk_var(enode* n) { - theory_var r = theory::mk_var(n); - return r; + return theory::mk_var(n); } bool theory_seq::can_propagate() { @@ -461,7 +496,7 @@ expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) { enode_pair_dependency* deps = 0; e = m_rep.find(e, deps); expr* e1, *e2; - eqs = join(eqs, deps); + eqs = m_dm.mk_join(eqs, deps); if (m_util.str.is_concat(e, e1, e2)) { return expr_ref(m_util.str.mk_concat(expand(e1, eqs), expand(e2, eqs)), m); } @@ -484,18 +519,11 @@ expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) { } void theory_seq::add_dependency(enode_pair_dependency*& dep, enode* a, enode* b) { - dep = join(dep, leaf(a, b)); + if (a != b) { + dep = m_dm.mk_join(dep, m_dm.mk_leaf(std::make_pair(a, b))); + } } -theory_seq::enode_pair_dependency* theory_seq::join(enode_pair_dependency* a, enode_pair_dependency* b) { - if (!a) return b; - if (!b) return a; - return m_dm.mk_join(a, b); -} - -theory_seq::enode_pair_dependency* theory_seq::leaf(enode* a, enode* b) { - return (a == b)?0:m_dm.mk_leaf(std::make_pair(a, b)); -} void theory_seq::propagate() { context & ctx = get_context(); @@ -523,10 +551,8 @@ void theory_seq::assert_axiom(expr_ref& e) { } expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2) { - expr_ref result(m); expr* es[2] = { e1, e2 }; - result = m_util.mk_skolem(name, 2, es, m.get_sort(e1)); - return result; + return expr_ref(m_util.mk_skolem(name, 2, es, m.get_sort(e1)), m); } void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) { @@ -536,18 +562,20 @@ void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) { << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";); ctx.internalize(e1, false); + SASSERT(ctx.e_internalized(e2)); enode* n1 = ctx.get_enode(e1); enode* n2 = ctx.get_enode(e2); literal lit(v); - justification* js = ctx.mk_justification(ext_theory_eq_propagation_justification( - get_id(), ctx.get_region(), 1, &lit, 0, 0, n1, n2)); + justification* js = + ctx.mk_justification( + ext_theory_eq_propagation_justification( + get_id(), ctx.get_region(), 1, &lit, 0, 0, n1, n2)); ctx.assign_eq(n1, n2, eq_justification(js)); } void theory_seq::assign_eq(bool_var v, bool is_true) { context & ctx = get_context(); - enode* n = ctx.bool_var2enode(v); app* e = n->get_owner(); if (is_true) { @@ -585,9 +613,11 @@ void theory_seq::assign_eq(bool_var v, bool is_true) { void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { enode* n1 = get_enode(v1); enode* n2 = get_enode(v2); - m.push_back(m_lhs.back(), n1->get_owner()); - m.push_back(m_rhs.back(), n2->get_owner()); - m_dam.push_back(m_deps.back(), leaf(n1, n2)); + if (n1 != n2) { + m.push_back(m_lhs.back(), n1->get_owner()); + m.push_back(m_rhs.back(), n2->get_owner()); + m_dam.push_back(m_deps.back(), m_dm.mk_leaf(enode_pair(n1, n2))); + } } void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 63dd2bdc6..3cdacaeda 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -126,7 +126,11 @@ namespace smt { bool solve_unit_eq(expr* l, expr* r, enode_pair_dependency* dep); bool solve_basic_eqs(); bool simplify_and_solve_eqs(); - void propagate(literal lit, enode_pair_dependency* dep); + 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 occurs(expr* a, expr* b); bool is_var(expr* b); void add_solution(expr* l, expr* r, enode_pair_dependency* dep); @@ -140,15 +144,13 @@ namespace smt { 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); - enode_pair_dependency* leaf(enode* a, enode* b); - enode_pair_dependency* join(enode_pair_dependency* a, enode_pair_dependency* b); - void propagate_eq(bool_var v, expr* e1, expr* e2); expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2); void set_incomplete(app* term); public: theory_seq(ast_manager& m); + virtual ~theory_seq(); }; }; From b1a1aa5007a736bec7334a9c71a373aaabb4443e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Dec 2015 07:09:23 -0800 Subject: [PATCH 9/9] remove unused field Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 4 ---- src/ast/seq_decl_plugin.h | 7 +++---- 2 files changed, 3 insertions(+), 8 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 4022b1402..2946bb1bc 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -437,10 +437,6 @@ app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort } -app* seq_util::str::mk_string(symbol const& s) { - return u.seq.mk_string(s); -} - void seq_util::str::get_concat(expr* e, ptr_vector& es) const { expr* e1, *e2; while (is_concat(e, e1, e2)) { diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index c11f830b4..0ab889c38 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -167,11 +167,11 @@ public: ast_manager& m; family_id m_fid; public: - str(seq_util& u):u(u), m(u.m), m_fid(u.m_fid) {} + str(seq_util& u): u(u), m(u.m), m_fid(u.m_fid) {} sort* mk_seq(sort* s) { parameter param(s); return m.mk_sort(m_fid, SEQ_SORT, 1, ¶m); } app* mk_empty(sort* s) { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, 0, 0, (expr*const*)0, s)); } - app* mk_string(symbol const& s); + app* mk_string(symbol const& s) { return u.seq.mk_string(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_SEQ_CONCAT, 2, es); } @@ -229,11 +229,10 @@ public: }; class re { - seq_util& u; ast_manager& m; family_id m_fid; public: - re(seq_util& u):u(u), m(u.m), m_fid(u.m_fid) {} + re(seq_util& u): m(u.m), m_fid(u.m_fid) {} 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); }