diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index a46d4207b..f50d3334c 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -276,6 +276,7 @@ br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& resu } br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { + TRACE("seq", tout << mk_pp(a, m()) << " " << mk_pp(b, m()) << "\n";); std::string s1, s2; bool isc1 = m_util.str.is_string(a, s1); bool isc2 = m_util.str.is_string(b, s2); @@ -309,7 +310,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { SASSERT(as.size() > 1); s2 = std::string(s2.c_str() + s1.length(), s2.length() - s1.length()); bs[0] = m_util.str.mk_string(s2); - m_util.str.mk_prefix(m_util.str.mk_concat(as.size()-1, as.c_ptr()+1), + result = m_util.str.mk_prefix(m_util.str.mk_concat(as.size()-1, as.c_ptr()+1), m_util.str.mk_concat(bs.size(), bs.c_ptr())); return BR_REWRITE_FULL; } @@ -329,7 +330,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { SASSERT(bs.size() > 1); s1 = std::string(s1.c_str() + s2.length(), s1.length() - s2.length()); as[0] = m_util.str.mk_string(s1); - m_util.str.mk_prefix(m_util.str.mk_concat(as.size(), as.c_ptr()), + result = m_util.str.mk_prefix(m_util.str.mk_concat(as.size(), as.c_ptr()), m_util.str.mk_concat(bs.size()-1, bs.c_ptr()+1)); return BR_REWRITE_FULL; } @@ -352,7 +353,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { } if (i == bs.size()) { expr_ref_vector es(m()); - for (unsigned j = i; j < as.size(); ++i) { + for (unsigned j = i; j < as.size(); ++j) { es.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j])); } result = mk_and(es); @@ -369,16 +370,11 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { } br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) { - std::string s1, s2; - bool isc1 = m_util.str.is_string(a, s1); - if (isc1 && m_util.str.is_string(b, s2)) { - bool suffix = s1.length() <= s2.length(); - for (unsigned i = 0; i < s1.length() && suffix; ++i) { - suffix = s1[s1.length() - i - 1] == s2[s2.length() - i - 1]; - } - result = m().mk_bool_val(suffix); + if (a == b) { + result = m().mk_true(); return BR_DONE; } + std::string s1, s2; if (m_util.str.is_empty(a)) { result = m().mk_true(); return BR_DONE; @@ -394,6 +390,79 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) { result = m_util.str.mk_suffix(a1, b1); return BR_REWRITE1; } + if (m_util.str.is_concat(b, b1, b2) && b2 == a) { + result = m().mk_true(); + return BR_DONE; + } + bool isc1 = false; + bool isc2 = false; + + if (m_util.str.is_concat(a, a1, a2) && m_util.str.is_string(a2, s1)) { + isc1 = true; + } + else if (m_util.str.is_string(a, s1)) { + isc1 = true; + a2 = a; + a1 = 0; + } + + if (m_util.str.is_concat(b, b1, b2) && m_util.str.is_string(b2, s2)) { + isc2 = true; + } + else if (m_util.str.is_string(b, s2)) { + isc2 = true; + b2 = b; + b1 = 0; + } + if (isc1 && isc2) { + if (s1.length() == s2.length()) { + SASSERT(s1 != s2); + result = m().mk_false(); + return BR_DONE; + } + else if (s1.length() < s2.length()) { + bool suffix = true; + for (unsigned i = 0; i < s1.length(); ++i) { + suffix = s1[s1.length()-i-1] == s2[s2.length()-i-1]; + } + if (suffix && a1 == 0) { + result = m().mk_true(); + return BR_DONE; + } + else if (suffix) { + s2 = std::string(s2.c_str(), s2.length()-s1.length()); + b2 = m_util.str.mk_string(s2); + result = m_util.str.mk_suffix(a1, b1?m_util.str.mk_concat(b1, b2):b2); + return BR_DONE; + } + else { + result = m().mk_false(); + return BR_DONE; + } + } + else { + SASSERT(s1.length() > s2.length()); + if (b1 == 0) { + result = m().mk_false(); + return BR_DONE; + } + bool suffix = true; + for (unsigned i = 0; i < s2.length(); ++i) { + suffix = s1[s1.length()-i-1] == s2[s2.length()-i-1]; + } + if (suffix) { + s1 = std::string(s1.c_str(), s1.length()-s2.length()); + a2 = m_util.str.mk_string(s1); + result = m_util.str.mk_suffix(a1?m_util.str.mk_concat(a1, a2):a2, b1); + return BR_DONE; + } + else { + result = m().mk_false(); + return BR_DONE; + } + } + } + return BR_FAILED; } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index b47c4209d..e22979163 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -289,9 +289,15 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, ast_manager& m = *m_manager; sort_ref rng(m); switch(k) { - case OP_SEQ_UNIT: case OP_SEQ_EMPTY: + match(*m_sigs[k], arity, domain, range, rng); + if (rng == m_string) { + parameter param(symbol("")); + return mk_func_decl(OP_STRING_CONST, 1, ¶m, 0, 0, m_string); + } + return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); + case OP_SEQ_UNIT: case OP_RE_PLUS: case OP_RE_STAR: case OP_RE_OPTION: diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp new file mode 100644 index 000000000..b3a143377 --- /dev/null +++ b/src/smt/theory_seq.cpp @@ -0,0 +1,306 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + theory_seq.h + +Abstract: + + Native theory solver for sequences. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-6-12 + +Revision History: + +--*/ + +#include "value_factory.h" +#include "smt_context.h" +#include "smt_model_generator.h" +#include "theory_seq.h" + +using namespace smt; + +theory_seq::theory_seq(ast_manager& m): + theory(m.mk_family_id("seq")), + m_axioms_head(0), + m_axioms(m), + m_ineqs(m), + m_used(false), + m_rewrite(m), + m_util(m), + m_autil(m), + m_trail_stack(*this), + m_find(*this) {} + +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; + } + return m_used?FC_GIVEUP:FC_DONE; +} + +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); + 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); + 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; + } + } + return FC_DONE; +} + +final_check_status theory_seq::simplify_eqs() { + bool simplified = false; + for (unsigned i = 0; i < get_num_vars(); ++i) { + theory_var v = m_find.find(i); + if (v != i) continue; + + } + if (simplified) { + return FC_CONTINUE; + } + return FC_DONE; +} + +final_check_status theory_seq::add_axioms() { + for (unsigned i = 0; i < get_num_vars(); ++i) { + + // add axioms for len(x) when x = a ++ b + } + return FC_DONE; +} + +bool theory_seq::internalize_atom(app* a, bool) { + return internalize_term(a); +} + +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); + } + 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 { + theory_var v = mk_var(e); + ctx.attach_th_var(e, this, v); + } + // assert basic axioms + if (!m_used) { m_trail_stack.push(value_trail(m_used)); m_used = true; } + return true; +} + +theory_var theory_seq::mk_var(enode* n) { + theory_var r = theory::mk_var(n); + VERIFY(r == m_find.mk_var()); + return r; +} + +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 result = expand(e, eqs); + m_rewrite(result); + return result; +} + +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); + enode* start = n; + do { + e = n->get_owner(); + if (m_util.str.is_concat(e, e1, e2)) { + if (start != n) eqs.push_back(enode_pair(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)); + return expr_ref(e, m); + } + if (m.is_eq(e, e1, e2)) { + if (start != n) eqs.push_back(enode_pair(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)); + 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)); + 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)); + 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(); + } + while (n != start); + return expr_ref(n->get_root()->get_owner(), m); +} + +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(); + assert_axiom(e); + ++m_axioms_head; + } +} + +void theory_seq::create_axiom(expr_ref& e) { + m_trail_stack.push(push_back_vector(m_axioms)); + m_axioms.push_back(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); + 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) { + ast_manager& m = get_manager(); + 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); + return result; +} + +void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) { + context& ctx = get_context(); + 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))); +} + +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(); + if (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 = 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 = 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); + f = m_util.str.mk_concat(m_util.str.mk_concat(f1, e1), f2); + propagate_eq(v, f, e2); + } + else if (m_util.str.is_in_re(e, e1, e2)) { + NOT_IMPLEMENTED_YET(); + } + else { + UNREACHABLE(); + } + } + else { + m_trail_stack.push(push_back_vector(m_ineqs)); + m_ineqs.push_back(e); + } +} + +void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { + m_find.merge(v1, 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)); + m_ineqs.push_back(m.mk_eq(e1, e2)); +} + +void theory_seq::push_scope_eh() { + theory::push_scope_eh(); + m_trail_stack.push_scope(); + m_trail_stack.push(value_trail(m_axioms_head)); +} + +void theory_seq::pop_scope_eh(unsigned num_scopes) { + m_trail_stack.pop_scope(num_scopes); + theory::pop_scope_eh(num_scopes); +} + +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); + create_axiom(e); + } +} diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h new file mode 100644 index 000000000..3232a8469 --- /dev/null +++ b/src/smt/theory_seq.h @@ -0,0 +1,91 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + theory_seq.h + +Abstract: + + Native theory solver for sequences. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-6-12 + +Revision History: + +--*/ +#ifndef THEORY_SEQ_H_ +#define THEORY_SEQ_H_ + +#include "smt_theory.h" +#include "seq_decl_plugin.h" +#include "theory_seq_empty.h" +#include "th_rewriter.h" +#include "union_find.h" + +namespace smt { + + class theory_seq : public theory { + typedef union_find th_union_find; + typedef trail_stack th_trail_stack; + struct stats { + stats() { reset(); } + void reset() { memset(this, 0, sizeof(stats)); } + unsigned m_num_splits; + }; + expr_ref_vector m_axioms; + expr_ref_vector m_ineqs; + unsigned m_axioms_head; + bool m_used; + th_rewriter m_rewrite; + 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(); + 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 bool can_propagate(); + virtual void propagate(); + virtual void push_scope_eh(); + virtual void pop_scope_eh(unsigned num_scopes); + virtual void restart_eh(); + virtual void relevant_eh(app* n); + 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); + + final_check_status check_ineqs(); + final_check_status simplify_eqs(); + 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); + + void propagate_eq(bool_var v, expr* e1, expr* e2); + expr_ref mk_skolem(char const* name, expr* e1, expr* e2); + 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())); + } + + 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 /* THEORY_SEQ_H_ */ +