From a7e2fb31e3e7a19aa79ed482633d75252c2df946 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 12 Dec 2015 11:36:49 -0800 Subject: [PATCH 1/4] updates to resource exceptions, update master possibly handle pull request issue Signed-off-by: Nikolaj Bjorner --- src/ast/normal_forms/nnf.cpp | 2 +- src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 2 +- src/qe/qe.cpp | 2 +- src/qe/qe_lite.cpp | 10 +++++----- src/qe/qe_sat_tactic.cpp | 2 +- src/qe/qe_tactic.cpp | 2 +- src/sat/tactic/goal2sat.cpp | 4 ++-- src/smt/smt_model_finder.cpp | 2 +- src/smt/tactic/unit_subsumption_tactic.cpp | 2 +- src/smt/theory_seq.cpp | 7 +++++++ src/smt/theory_seq.h | 4 +--- src/tactic/aig/aig.cpp | 2 +- src/tactic/arith/arith_bounds_tactic.cpp | 2 +- src/tactic/arith/degree_shift_tactic.cpp | 2 +- src/tactic/arith/diff_neq_tactic.cpp | 2 +- src/tactic/arith/fm_tactic.cpp | 4 ++-- src/tactic/bv/bv_size_reduction_tactic.cpp | 2 +- src/tactic/bv/bvarray2uf_tactic.cpp | 2 +- src/tactic/core/cofactor_elim_term_ite.cpp | 2 +- src/tactic/core/ctx_simplify_tactic.cpp | 2 +- src/tactic/core/reduce_args_tactic.cpp | 2 +- src/tactic/core/solve_eqs_tactic.cpp | 4 ++-- src/tactic/sls/sls_engine.cpp | 2 +- src/tactic/ufbv/quasi_macros_tactic.cpp | 4 ++-- 24 files changed, 38 insertions(+), 33 deletions(-) diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 0d8aa90e3..6b10e8c10 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -373,7 +373,7 @@ struct nnf::imp { if (memory::get_allocation_size() > m_max_memory) throw nnf_exception(Z3_MAX_MEMORY_MSG); if (m().canceled()) - throw nnf_exception(Z3_CANCELED_MSG); + throw nnf_exception(m().limit().get_cancel_msg()); } void set_new_child_flag() { diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 74721d981..38a608f5f 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -28,7 +28,7 @@ void bit_blaster_tpl::checkpoint() { if (memory::get_allocation_size() > m_max_memory) throw rewriter_exception(Z3_MAX_MEMORY_MSG); if (m().canceled()) - throw rewriter_exception(Z3_CANCELED_MSG); + throw rewriter_exception(m().limit().get_cancel_msg()); cooperate("bit-blaster"); } diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 846cb6c68..150198bab 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -2051,7 +2051,7 @@ namespace qe { void checkpoint() { if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); cooperate("qe"); } diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 4364d4a21..9a981cc9b 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -738,7 +738,7 @@ namespace eq { void checkpoint() { cooperate("der"); if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); } public: @@ -917,8 +917,8 @@ namespace ar { void checkpoint() { cooperate("der"); if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); - } + throw tactic_exception(m.limit().get_cancel_msg()); + } public: @@ -2207,7 +2207,7 @@ namespace fm { void checkpoint() { cooperate("fm"); if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); } public: @@ -2477,7 +2477,7 @@ class qe_lite_tactic : public tactic { void checkpoint() { if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); cooperate("qe-lite"); } diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp index d3e145e1b..455c1d08e 100644 --- a/src/qe/qe_sat_tactic.cpp +++ b/src/qe/qe_sat_tactic.cpp @@ -662,7 +662,7 @@ namespace qe { void checkpoint() { if (m.canceled()) { - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); } cooperate("qe-sat"); } diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp index d72727250..c8660b916 100644 --- a/src/qe/qe_tactic.cpp +++ b/src/qe/qe_tactic.cpp @@ -45,7 +45,7 @@ class qe_tactic : public tactic { void checkpoint() { if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); cooperate("qe"); } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index fbf34e741..b82f00a92 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -333,7 +333,7 @@ struct goal2sat::imp { loop: cooperate("goal2sat"); if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); frame & fr = m_frame_stack.back(); @@ -626,7 +626,7 @@ struct sat2goal::imp { void checkpoint() { if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); } diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 1f51e8bf2..2e260cbca 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -3318,7 +3318,7 @@ namespace smt { void model_finder::checkpoint(char const* msg) { cooperate(msg); if (m_context && m_context->get_cancel_flag()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m_context->get_manager().limit().get_cancel_msg()); } mf::quantifier_info * model_finder::get_quantifier_info(quantifier * q) const { diff --git a/src/smt/tactic/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp index ab7b40a26..745bfa2de 100644 --- a/src/smt/tactic/unit_subsumption_tactic.cpp +++ b/src/smt/tactic/unit_subsumption_tactic.cpp @@ -58,7 +58,7 @@ struct unit_subsumption_tactic : public tactic { void checkpoint() { if (m.canceled()) { - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); } } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index a402437d3..f0b82adbb 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -86,6 +86,13 @@ void theory_seq::solution_map::display(std::ostream& out) const { } } +bool theory_seq::exclusion_table::contains(expr* e, expr* r) const { + if (e->get_id() > r->get_id()) { + std::swap(e, r); + } + return m_table.contains(std::make_pair(e, r)); +} + void theory_seq::exclusion_table::update(expr* e, expr* r) { if (e->get_id() > r->get_id()) { std::swap(e, r); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 28a35c564..72363772b 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -81,9 +81,7 @@ namespace smt { ~exclusion_table() { } bool empty() const { return m_table.empty(); } void update(expr* e, expr* r); - bool contains(expr* e, expr* r) { - return m_table.contains(std::make_pair(e, r)); - } + bool contains(expr* e, expr* r) const; void push_scope() { m_limit.push_back(m_lhs.size()); } void pop_scope(unsigned num_scopes); void display(std::ostream& out) const; diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index 3f5e7bdfe..b84ae68f0 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -131,7 +131,7 @@ struct aig_manager::imp { if (memory::get_allocation_size() > m_max_memory) throw aig_exception(TACTIC_MAX_MEMORY_MSG); if (m().canceled()) - throw aig_exception(TACTIC_CANCELED_MSG); + throw aig_exception(m().limit().get_cancel_msg()); cooperate("aig"); } diff --git a/src/tactic/arith/arith_bounds_tactic.cpp b/src/tactic/arith/arith_bounds_tactic.cpp index 1111d7f1f..fe054aaea 100644 --- a/src/tactic/arith/arith_bounds_tactic.cpp +++ b/src/tactic/arith/arith_bounds_tactic.cpp @@ -37,7 +37,7 @@ struct arith_bounds_tactic : public tactic { void checkpoint() { if (m.canceled()) { - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); } } diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index f4455e672..6c5527d12 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -100,7 +100,7 @@ class degree_shift_tactic : public tactic { void checkpoint() { if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); cooperate("degree_shift"); } diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index 5cc021f6f..410185cf8 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/src/tactic/arith/diff_neq_tactic.cpp @@ -289,7 +289,7 @@ class diff_neq_tactic : public tactic { unsigned nvars = num_vars(); while (m_stack.size() < nvars) { if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); TRACE("diff_neq_tactic", display_model(tout);); var x = m_stack.size(); if (extend_model(x)) diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index 4674459dd..698128e26 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -197,7 +197,7 @@ class fm_tactic : public tactic { clauses::iterator it = m_clauses[i].begin(); clauses::iterator end = m_clauses[i].end(); for (; it != end; ++it) { - if (m.canceled()) throw tactic_exception(TACTIC_CANCELED_MSG); + if (m.canceled()) throw tactic_exception(m.limit().get_cancel_msg()); switch (process(x, *it, u, ev, val)) { case NONE: TRACE("fm_mc", tout << "no bound for:\n" << mk_ismt2_pp(*it, m) << "\n";); @@ -1543,7 +1543,7 @@ class fm_tactic : public tactic { void checkpoint() { cooperate("fm"); if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); } diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 8c93aeb90..25127cb90 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -176,7 +176,7 @@ struct bv_size_reduction_tactic::imp { void checkpoint() { if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); } void operator()(goal & g, model_converter_ref & mc) { diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp index 50063b8a5..42ceaf78c 100644 --- a/src/tactic/bv/bvarray2uf_tactic.cpp +++ b/src/tactic/bv/bvarray2uf_tactic.cpp @@ -50,7 +50,7 @@ class bvarray2uf_tactic : public tactic { void checkpoint() { if (m_manager.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m_manager.limit().get_cancel_msg()); } void operator()(goal_ref const & g, diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp index 43e3559ba..15f0e06ea 100644 --- a/src/tactic/core/cofactor_elim_term_ite.cpp +++ b/src/tactic/core/cofactor_elim_term_ite.cpp @@ -36,7 +36,7 @@ struct cofactor_elim_term_ite::imp { if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); } // Collect atoms that contain term if-then-else diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 987d5a48d..1cfaa78cf 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -96,7 +96,7 @@ struct ctx_simplify_tactic::imp { if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); if (m.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m.limit().get_cancel_msg()); } bool shared(expr * t) const { diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index 121dbeef3..cf83a5a10 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -94,7 +94,7 @@ struct reduce_args_tactic::imp { void checkpoint() { if (m_manager.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m_manager.limit().get_cancel_msg()); cooperate("reduce-args"); } diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index 01c4bc10b..f1ffe4b53 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -77,8 +77,8 @@ class solve_eqs_tactic : public tactic { void checkpoint() { if (m().canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); - cooperate("solve-eqs"); + throw tactic_exception(m().limit().get_cancel_msg()); + cooperate("solve-eqs"); } // Check if the number of occurrences of t is below the specified threshold :solve-eqs-max-occs diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index d0798e375..4418808dd 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -95,7 +95,7 @@ void sls_engine::collect_statistics(statistics& st) const { void sls_engine::checkpoint() { if (m_manager.canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); + throw tactic_exception(m_manager.limit().get_cancel_msg()); cooperate("sls"); } diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index 5a5cba1f0..d1320bc0d 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -77,8 +77,8 @@ class quasi_macros_tactic : public tactic { while (more) { // CMW: use repeat(...) ? if (m().canceled()) - throw tactic_exception(TACTIC_CANCELED_MSG); - + throw tactic_exception(m().limit().get_cancel_msg()); + new_forms.reset(); new_proofs.reset(); more = qm(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs); From 3c50508762bc1b4ee88aff20741be6a6ad2f9945 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 12 Dec 2015 20:46:28 -0800 Subject: [PATCH 2/4] use ADT for strings Signed-off-by: Nikolaj Bjorner --- src/ast/ast_smt2_pp.cpp | 10 +- src/ast/rewriter/seq_rewriter.cpp | 118 +++++--------- src/ast/rewriter/seq_rewriter.h | 2 +- src/ast/seq_decl_plugin.cpp | 159 +++++++++++++++++++ src/ast/seq_decl_plugin.h | 46 +++++- src/parsers/smt2/smt2parser.cpp | 2 +- src/smt/smt_setup.cpp | 2 +- src/smt/theory_seq.cpp | 256 +++++++++++++++++------------- src/smt/theory_seq.h | 23 ++- src/smt/theory_seq_empty.h | 4 +- 10 files changed, 421 insertions(+), 201 deletions(-) diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 523d98a93..333c9c229 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -364,16 +364,18 @@ format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned d } format * smt2_pp_environment::pp_string_literal(app * t) { - std::string s; + zstring s; + std::string encs; VERIFY (get_sutil().str.is_string(t, s)); + encs = s.encode(); std::ostringstream buffer; buffer << "\""; - for (unsigned i = 0; i < s.length(); ++i) { - if (s[i] == '\"') { + for (unsigned i = 0; i < encs.length(); ++i) { + if (encs[i] == '\"') { buffer << "\"\""; } else { - buffer << s[i]; + buffer << encs[i]; } } buffer << "\""; diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index e64dacdf1..1eaf6b42b 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -121,7 +121,7 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con (a + string) + string = a + string */ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) { - std::string s1, s2; + zstring s1, s2; expr* c, *d; bool isc1 = m_util.str.is_string(a, s1); bool isc2 = m_util.str.is_string(b, s2); @@ -150,10 +150,10 @@ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) { } br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) { - std::string b; + zstring b; m_es.reset(); m_util.str.get_concat(a, m_es); - size_t len = 0; + unsigned len = 0; unsigned j = 0; for (unsigned i = 0; i < m_es.size(); ++i) { if (m_util.str.is_string(m_es[i], b)) { @@ -189,21 +189,21 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) { } br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result) { - std::string s; + zstring s; rational pos, len; if (m_util.str.is_string(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) && pos.is_unsigned() && len.is_unsigned() && pos.get_unsigned() <= s.length()) { unsigned _pos = pos.get_unsigned(); unsigned _len = len.get_unsigned(); - result = m_util.str.mk_string(s.substr(_pos, _len)); + result = m_util.str.mk_string(s.extract(_pos, _len)); return BR_DONE; } return BR_FAILED; } br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) { - std::string c, d; + zstring c, d; if (m_util.str.is_string(a, c) && m_util.str.is_string(b, d)) { - result = m().mk_bool_val(0 != strstr(c.c_str(), d.c_str())); + result = m().mk_bool_val(c.contains(d)); return BR_DONE; } // check if subsequence of b is in a. @@ -225,15 +225,12 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) { } br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) { - std::string c; + zstring c; rational r; if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r) && r.is_unsigned()) { unsigned j = r.get_unsigned(); if (j < c.length()) { - char ch = c[j]; - c[0] = ch; - c[1] = 0; - result = m_util.str.mk_string(c); + result = m_util.str.mk_string(c.extract(j, 1)); return BR_DONE; } } @@ -241,19 +238,14 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) { } br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result) { - std::string s1, s2; + zstring s1, s2; rational r; bool isc1 = m_util.str.is_string(a, s1); bool isc2 = m_util.str.is_string(b, s2); if (isc1 && isc2 && m_autil.is_numeral(c, r) && r.is_unsigned()) { - for (unsigned i = r.get_unsigned(); i < s1.length(); ++i) { - if (strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) { - result = m_autil.mk_numeral(rational(i) - r, true); - return BR_DONE; - } - } - result = m_autil.mk_numeral(rational(-1), true); + int idx = s1.indexof(s2, r.get_unsigned()); + result = m_autil.mk_numeral(rational(idx), true); return BR_DONE; } if (m_autil.is_numeral(c, r) && r.is_neg()) { @@ -270,23 +262,10 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result } br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result) { - std::string s1, s2, s3; + zstring s1, s2, s3; if (m_util.str.is_string(a, s1) && m_util.str.is_string(b, s2) && m_util.str.is_string(c, s3)) { - std::ostringstream buffer; - bool can_replace = true; - for (size_t i = 0; i < s1.length(); ) { - if (can_replace && strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) { - buffer << s3; - i += s2.length(); - can_replace = false; - } - else { - buffer << s1[i]; - ++i; - } - } - result = m_util.str.mk_string(buffer.str()); + result = m_util.str.mk_string(s1.replace(s2, s3)); return BR_DONE; } if (b == c) { @@ -298,15 +277,11 @@ br_status seq_rewriter::mk_seq_replace(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; + zstring s1, s2; bool isc1 = m_util.str.is_string(a, s1); bool isc2 = m_util.str.is_string(b, s2); if (isc1 && isc2) { - bool prefix = s1.length() <= s2.length(); - for (unsigned i = 0; i < s1.length() && prefix; ++i) { - prefix = s1[i] == s2[i]; - } - result = m().mk_bool_val(prefix); + result = m().mk_bool_val(s1.prefixof(s2)); return BR_DONE; } if (m_util.str.is_empty(a)) { @@ -321,7 +296,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { if (a1 != b1 && isc1 && isc2) { if (s1.length() <= s2.length()) { - if (strncmp(s1.c_str(), s2.c_str(), s1.length()) == 0) { + if (s1.prefixof(s2)) { if (a == a1) { result = m().mk_true(); return BR_DONE; @@ -329,10 +304,10 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { m_util.str.get_concat(a, as); m_util.str.get_concat(b, bs); SASSERT(as.size() > 1); - s2 = std::string(s2.c_str() + s1.length(), s2.length() - s1.length()); + s2 = s2.extract(s1.length(), s2.length()-s1.length()); bs[0] = m_util.str.mk_string(s2); 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())); + m_util.str.mk_concat(bs.size(), bs.c_ptr())); return BR_REWRITE_FULL; } else { @@ -341,7 +316,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { } } else { - if (strncmp(s1.c_str(), s2.c_str(), s2.length()) == 0) { + if (s2.prefixof(s1)) { if (b == b1) { result = m().mk_false(); return BR_DONE; @@ -349,7 +324,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { m_util.str.get_concat(a, as); m_util.str.get_concat(b, bs); SASSERT(bs.size() > 1); - s1 = std::string(s1.c_str() + s2.length(), s1.length() - s2.length()); + s1 = s1.extract(s2.length(), s1.length() - s2.length()); as[0] = m_util.str.mk_string(s1); 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)); @@ -396,7 +371,7 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) { result = m().mk_true(); return BR_DONE; } - std::string s1, s2; + zstring s1, s2; if (m_util.str.is_empty(a)) { result = m().mk_true(); return BR_DONE; @@ -438,21 +413,18 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) { } if (isc1 && isc2) { if (s1.length() == s2.length()) { - SASSERT(s1 != s2); + //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]; - } + bool suffix = s1.suffixof(s2); if (suffix && a1 == 0) { result = m().mk_true(); return BR_DONE; } else if (suffix) { - s2 = std::string(s2.c_str(), s2.length()-s1.length()); + s2 = s2.extract(0, 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; @@ -468,12 +440,9 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) { 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]; - } + bool suffix = s2.suffixof(s1); if (suffix) { - s1 = std::string(s1.c_str(), s1.length()-s2.length()); + s1 = s1.extract(0, 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; @@ -491,14 +460,15 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) { br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) { rational r; if (m_autil.is_numeral(a, r)) { - result = m_util.str.mk_string(r.to_string()); + result = m_util.str.mk_string(symbol(r.to_string().c_str())); return BR_DONE; } return BR_FAILED; } br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) { - std::string s; - if (m_util.str.is_string(a, s)) { + zstring str; + if (m_util.str.is_string(a, str)) { + std::string s = str.encode(); for (unsigned i = 0; i < s.length(); ++i) { if (s[i] == '-') { if (i != 0) return BR_FAILED; } else if ('0' <= s[i] && s[i] <= '9') continue; @@ -608,13 +578,13 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve change = true; } // reduce strings - std::string s1, s2; + zstring s1, 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) { + unsigned l = std::min(s1.length(), s2.length()); + for (unsigned i = 0; i < l; ++i) { if (s1[i] != s2[i]) { return false; } @@ -623,14 +593,14 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve ++head1; } else { - m_lhs[head1] = m_util.str.mk_string(std::string(s1.c_str()+l,s1.length()-l)); + m_lhs[head1] = m_util.str.mk_string(s1.extract(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)); + m_rhs[head2] = m_util.str.mk_string(s2.extract(l, s2.length()-l)); trail.push_back(m_rhs[head2]); } change = true; @@ -639,8 +609,8 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve 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) { + unsigned l = std::min(s1.length(), s2.length()); + for (unsigned i = 0; i < l; ++i) { if (s1[s1.length()-i-1] != s2[s2.length()-i-1]) { return false; } @@ -648,11 +618,11 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve 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))); + m_lhs.push_back(m_util.str.mk_string(s1.extract(0, 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))); + m_rhs.push_back(m_util.str.mk_string(s2.extract(0, s2.length()-l))); trail.push_back(m_rhs.back()); } change = true; @@ -703,7 +673,7 @@ expr* seq_rewriter::concat_non_empty(unsigned n, expr* const* as) { } bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs) { - std::string s; + zstring s; for (unsigned i = 0; i < sz; ++i) { if (m_util.str.is_unit(es[i])) { if (all) return false; @@ -725,8 +695,8 @@ bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_ve return true; } -bool seq_rewriter::min_length(unsigned n, expr* const* es, size_t& len) { - std::string s; +bool seq_rewriter::min_length(unsigned n, expr* const* es, unsigned& len) { + zstring s; bool bounded = true; len = 0; for (unsigned i = 0; i < n; ++i) { @@ -749,7 +719,7 @@ bool seq_rewriter::min_length(unsigned n, expr* const* es, size_t& len) { bool seq_rewriter::length_constrained(unsigned szl, expr* const* l, unsigned szr, expr* const* r, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) { is_sat = true; - size_t len1 = 0, len2 = 0; + unsigned len1 = 0, len2 = 0; bool bounded1 = min_length(szl, l, len1); bool bounded2 = min_length(szr, r, len2); if (bounded1 && len1 < len2) { diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 998b37d1a..de3634a51 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -58,7 +58,7 @@ class seq_rewriter { expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat); bool length_constrained(unsigned n, expr* const* l, unsigned m, expr* const* r, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat); - bool min_length(unsigned n, expr* const* es, size_t& len); + bool min_length(unsigned n, expr* const* es, unsigned& len); expr* concat_non_empty(unsigned n, expr* const* es); public: diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 49b1873d9..e33da18f2 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -22,6 +22,145 @@ Revision History: #include "ast_pp.h" #include +zstring::zstring(encoding enc): m_encoding(enc) {} + +zstring::zstring(char const* s, encoding enc): m_encoding(enc) { + // TBD: epply decoding + while (*s) { + m_buffer.push_back(*s); + ++s; + } +} + +zstring::zstring(zstring const& other) { + m_buffer = other.m_buffer; + m_encoding = other.m_encoding; +} + +zstring::zstring(unsigned num_bits, bool const* ch) { + SASSERT(num_bits == 8 || num_bits == 16); + m_encoding = (num_bits == 8)?ascii:unicode; + unsigned n = 0; + for (unsigned i = 0; i < num_bits; ++i) { + n |= (((unsigned)ch[i]) << num_bits); + } + m_buffer.push_back(n); +} + +zstring::zstring(unsigned ch, encoding enc) { + m_encoding = enc; + m_buffer.push_back(ch & ((enc == ascii)?0x000000FF:0x0000FFFF)); +} + +zstring& zstring::operator=(zstring const& other) { + m_encoding = other.m_encoding; + m_buffer.reset(); + m_buffer.append(other.m_buffer); + return *this; +} + +zstring zstring::replace(zstring const& src, zstring const& dst) const { + zstring result(m_encoding); + if (length() < src.length()) { + return zstring(*this); + } + bool found = false; + for (unsigned i = 0; i <= length() - src.length(); ++i) { + bool eq = !found; + for (unsigned j = 0; eq && j < src.length(); ++j) { + eq = m_buffer[i+j] == src[j]; + } + if (eq) { + result.m_buffer.append(dst.m_buffer); + found = true; + } + else { + result.m_buffer.push_back(m_buffer[i]); + } + } + return result; +} + +std::string zstring::encode() const { + // TBD apply encodings. + SASSERT(m_encoding == ascii); + std::ostringstream strm; + for (unsigned i = 0; i < m_buffer.size(); ++i) { + strm << (char)(m_buffer[i]); + } + return strm.str(); +} + +bool zstring::suffixof(zstring const& other) const { + if (length() > other.length()) return false; + bool suffix = true; + for (unsigned i = 0; suffix && i < length(); ++i) { + suffix = m_buffer[length()-i-1] == other[other.length()-i-1]; + } + return suffix; +} + +bool zstring::prefixof(zstring const& other) const { + if (length() > other.length()) return false; + bool prefix = true; + for (unsigned i = 0; prefix && i < length(); ++i) { + prefix = m_buffer[i] == other[i]; + } + return prefix; +} + +bool zstring::contains(zstring const& other) const { + if (other.length() > length()) return false; + unsigned last = length() - other.length(); + bool cont = false; + for (unsigned i = 0; !cont && i <= last; ++i) { + cont = true; + for (unsigned j = 0; cont && j < other.length(); ++j) { + cont = other[j] == m_buffer[j+i]; + } + } + return cont; +} + +int zstring::indexof(zstring const& other, int offset) const { + SASSERT(offset >= 0); + if (offset == length()) return -1; + if (other.length() + offset > length()) return -1; + unsigned last = length() - other.length(); + for (unsigned i = static_cast(offset); i <= last; ++i) { + bool prefix = true; + for (unsigned j = 0; prefix && j < other.length(); ++j) { + prefix = m_buffer[i + j] == other[j]; + } + if (prefix) { + return static_cast(i); + } + } + return -1; +} + +zstring zstring::extract(int offset, int len) const { + zstring result(m_encoding); + SASSERT(0 <= offset && 0 <= len); + int last = std::min(offset+len, static_cast(length())); + for (int i = offset; i < last; ++i) { + result.m_buffer.push_back(m_buffer[i]); + } + return result; +} + +zstring zstring::operator+(zstring const& other) const { + SASSERT(m_encoding == other.m_encoding); + zstring result(*this); + result.m_buffer.append(other.m_buffer); + return result; +} + +std::ostream& zstring::operator<<(std::ostream& out) const { + return out << encode(); +} + + seq_decl_plugin::seq_decl_plugin(): m_init(false), m_stringc_sym("String"), m_string(0), @@ -452,6 +591,14 @@ app* seq_decl_plugin::mk_string(symbol const& s) { return m_manager->mk_const(f); } +app* seq_decl_plugin::mk_string(zstring const& s) { + symbol sym(s.encode().c_str()); + parameter param(sym); + func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string, + func_decl_info(m_family_id, OP_STRING_CONST, 1, ¶m)); + return m_manager->mk_const(f); +} + bool seq_decl_plugin::is_value(app* e) const { return is_app_of(e, m_family_id, OP_STRING_CONST); } @@ -463,6 +610,18 @@ app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort return m.mk_app(f, n, args); } +app* seq_util::str::mk_string(zstring const& s) { return u.seq.mk_string(s); } + +bool seq_util::str::is_string(expr const* n, zstring& s) const { + if (is_string(n)) { + s = zstring(to_app(n)->get_decl()->get_parameter(0).get_symbol().bare_str()); + return true; + } + else { + return false; + } +} + void seq_util::str::get_concat(expr* e, ptr_vector& es) const { expr* e1, *e2; diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 7026a73cb..156bf4735 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -81,6 +81,36 @@ enum seq_op_kind { }; +class zstring { +public: + enum encoding { + ascii, + unicode + }; +private: + buffer m_buffer; + encoding m_encoding; +public: + zstring(encoding enc = ascii); + zstring(char const* s, encoding enc = ascii); + zstring(zstring const& other); + zstring(unsigned num_bits, bool const* ch); + zstring(unsigned ch, encoding enc = ascii); + zstring& operator=(zstring const& other); + zstring replace(zstring const& src, zstring const& dst) const; + unsigned num_bits() const { return (m_encoding==ascii)?8:16; } + std::string encode() const; + unsigned length() const { return m_buffer.size(); } + unsigned operator[](unsigned i) const { return m_buffer[i]; } + bool empty() const { return m_buffer.empty(); } + bool suffixof(zstring const& other) const; + bool prefixof(zstring const& other) const; + bool contains(zstring const& other) const; + int indexof(zstring const& other, int offset) const; + zstring extract(int lo, int hi) const; + zstring operator+(zstring const& other) const; + std::ostream& operator<<(std::ostream& out) const; +}; class seq_decl_plugin : public decl_plugin { struct psig { @@ -146,6 +176,7 @@ public: bool is_char(ast* a) const { return a == m_char; } app* mk_string(symbol const& s); + app* mk_string(zstring const& s); }; class seq_util { @@ -171,14 +202,18 @@ public: seq_util& u; ast_manager& m; family_id m_fid; + + 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())); } + + public: 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(zstring 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); } app* mk_concat(expr* a, expr* b, expr* c) { return mk_concat(mk_concat(a, b), c); @@ -193,14 +228,13 @@ public: bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); } - - bool is_string(expr const* n, std::string& s) const { - return is_string(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol().str(), true); - } + bool is_string(expr const* n, symbol& s) const { return is_string(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true); } + bool is_string(expr const* n, zstring& s) const; + 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); } diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 404c04d3a..c6736c1e0 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -1069,7 +1069,7 @@ namespace smt2 { void parse_string_const() { SASSERT(curr() == scanner::STRING_TOKEN); - expr_stack().push_back(sutil().str.mk_string(m_scanner.get_string())); + expr_stack().push_back(sutil().str.mk_string(symbol(m_scanner.get_string()))); TRACE("smt2parser", tout << "new string: " << mk_pp(expr_stack().back(), m()) << "\n";); next(); } diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 8ebfa2d71..8a40f9d7a 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -815,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 f0b82adbb..67ab2cfe3 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -127,6 +127,7 @@ theory_seq::theory_seq(ast_manager& m): m(m), m_dam(m_dep_array_value_manager, m_alloc), m_rep(m, m_dm), + m_cache(m), m_sort2len_fn(m), m_factory(0), m_ineqs(m), @@ -135,6 +136,7 @@ theory_seq::theory_seq(ast_manager& m): m_axioms_head(0), m_branch_variable_head(0), m_incomplete(false), + m_has_length(false), m_model_completion(false), m_rewrite(m), m_util(m), @@ -249,10 +251,10 @@ bool theory_seq::find_branch_candidate(expr* l, ptr_vector const& rs) { if (occurs(l, rs[j])) { return false; } - std::string s; + zstring s; if (m_util.str.is_string(rs[j], s)) { for (size_t k = 1; k < s.length(); ++k) { - v = m_util.str.mk_string(std::string(s.c_str(), k)); + v = m_util.str.mk_string(s.extract(0, k)); if (v0) v = m_util.str.mk_concat(v0, v); if (assume_equality(l, v)) { return true; @@ -426,6 +428,7 @@ bool theory_seq::is_right_select(expr* a, expr*& b) { void theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) { context& ctx = get_context(); m_rep.update(l, r, deps); + m_cache.reset(); // TBD: skip new equalities for non-internalized terms. if (ctx.e_internalized(l) && ctx.e_internalized(r)) { propagate_eq(deps, ctx.get_enode(l), ctx.get_enode(r)); @@ -508,6 +511,10 @@ bool theory_seq::internalize_term(app* term) { } mk_var(e); } + if (m_util.str.is_length(term) && !m_has_length) { + m_trail_stack.push(value_trail(m_has_length)); + m_has_length = true; + } if (!m_util.str.is_concat(term) && !m_util.str.is_string(term) && !m_util.str.is_empty(term) && @@ -635,37 +642,49 @@ expr_ref theory_seq::canonize(expr* e, enode_pair_dependency*& eqs) { expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) { enode_pair_dependency* deps = 0; + expr* r = 0; + if (m_cache.find(e, r)) { + return expr_ref(r, m); + } e = m_rep.find(e, deps); + expr_ref result(m); expr* e1, *e2; 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); + result = m_util.str.mk_concat(expand(e1, eqs), expand(e2, eqs)); } - if (m_util.str.is_empty(e) || m_util.str.is_string(e)) { - return expr_ref(e, m); + else if (m_util.str.is_empty(e) || m_util.str.is_string(e)) { + result = e; } - if (m.is_eq(e, e1, e2)) { - return expr_ref(m.mk_eq(expand(e1, eqs), expand(e2, eqs)), m); + else if (m.is_eq(e, e1, e2)) { + result = m.mk_eq(expand(e1, eqs), expand(e2, eqs)); } - if (m_util.str.is_prefix(e, e1, e2)) { - return expr_ref(m_util.str.mk_prefix(expand(e1, eqs), expand(e2, eqs)), m); + else if (m_util.str.is_prefix(e, e1, e2)) { + result = m_util.str.mk_prefix(expand(e1, eqs), expand(e2, eqs)); } - if (m_util.str.is_suffix(e, e1, e2)) { - return expr_ref(m_util.str.mk_suffix(expand(e1, eqs), expand(e2, eqs)), m); + else if (m_util.str.is_suffix(e, e1, e2)) { + result = m_util.str.mk_suffix(expand(e1, eqs), expand(e2, eqs)); } - if (m_util.str.is_contains(e, e1, e2)) { - return expr_ref(m_util.str.mk_contains(expand(e1, eqs), expand(e2, eqs)), m); + else if (m_util.str.is_contains(e, e1, e2)) { + result = m_util.str.mk_contains(expand(e1, eqs), expand(e2, eqs)); } - if (m_model_completion && is_var(e)) { + else if (m_model_completion && is_var(e)) { SASSERT(m_factory); expr_ref val(m); val = m_factory->get_fresh_value(m.get_sort(e)); if (val) { m_rep.update(e, val, 0); - return val; + result = val; + } + else { + result = e; } } - return expr_ref(e, m); + else { + result = e; + } + m_cache.insert(e, result); + return result; } void theory_seq::add_dependency(enode_pair_dependency*& dep, enode* a, enode* b) { @@ -707,48 +726,18 @@ void theory_seq::deque_axiom(expr* n) { else if (m_util.str.is_at(n)) { add_at_axiom(n); } -} - -/* - \brief nodes n1 and n2 are about to get merged. - if n1 occurs in the context of a length application, - then instantiate length axioms for each concatenation in the class of n2. - In this way we ensure that length respects concatenation. - */ -void theory_seq::new_eq_len_concat(enode* n1, enode* n2) { - context& ctx = get_context(); - if (n1->get_root() == n2->get_root()) { - return; + else if (m_util.str.is_unit(n)) { + add_length_unit_axiom(n); } - SASSERT(n1->get_root() != n2->get_root()); - if (!m_util.is_seq(n1->get_owner())) { - return; + else if (m_util.str.is_empty(n)) { + add_length_empty_axiom(n); } - func_decl* f_len = 0; - if (!m_sort2len_fn.find(m.get_sort(n1->get_owner()), f_len)) { - return; + else if (m_util.str.is_concat(n)) { + add_length_concat_axiom(n); } - - enode* r1 = n1->get_root(); - enode_vector::const_iterator it = ctx.begin_enodes_of(f_len); - enode_vector::const_iterator end = ctx.end_enodes_of(f_len); - bool has_len = false; - for (; !has_len && it != end; ++it) { - has_len = ((*it)->get_root() == r1); + else if (m_util.str.is_string(n)) { + add_length_string_axiom(n); } - if (!has_len) { - return; - } - enode* start2 = n2; - do { - expr* o = n2->get_owner(); - if (!is_var(o)) { - expr_ref ln(m_util.str.mk_length(o), m); - enque_axiom(ln); - } - n2 = n2->get_next(); - } - while (n2 != start2); } @@ -760,7 +749,7 @@ void theory_seq::new_eq_len_concat(enode* n1, enode* n2) { lit or s = "" or len(c) = 1 lit or s = "" or !prefix(s, x*s1) */ -void theory_seq::tightest_prefix(expr* s, expr* x, literal lit) { +void theory_seq::tightest_prefix(expr* s, expr* x, literal lit1, literal lit2) { expr_ref s1 = mk_skolem(symbol("seq.first"), s); expr_ref c = mk_skolem(symbol("seq.last"), s); expr_ref s1c(m_util.str.mk_concat(s1, c), m); @@ -768,26 +757,32 @@ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit) { expr_ref one(m_autil.mk_int(1), m); expr_ref emp(m_util.str.mk_empty(m.get_sort(s)), m); literal s_eq_emp = mk_eq(s, emp, false); - add_axiom(lit, s_eq_emp, mk_eq(s, s1c, false)); - add_axiom(lit, s_eq_emp, mk_eq(lc, one, false)); - add_axiom(lit, s_eq_emp, ~mk_literal(m_util.str.mk_contains(s, m_util.str.mk_concat(x, s1)))); + add_axiom(lit1, lit2, s_eq_emp, mk_eq(s, s1c, false)); + add_axiom(lit1, lit2, s_eq_emp, mk_eq(lc, one, false)); + add_axiom(lit1, lit2, s_eq_emp, ~mk_literal(m_util.str.mk_contains(s, m_util.str.mk_concat(x, s1)))); } /* + // index of s in t starting at offset. + + let i = Index(t, s, 0): + + len(t) = 0 => i = -1 + len(t) != 0 & !contains(t, s) => i = -1 + len(t) != 0 & contains(t, s) => t = xsy & i = len(x) + len(t) != 0 & contains(t, s) & s != emp => tightest_prefix(x, s) + let i = Index(t, s, offset) - if offset = 0: - (!contains(t, s) -> i = -1) - (s = empty -> i = 0) - (contains(t, s) & s != empty -> t = xsy) - (contains(t, s) -> tightest_prefix(s, x)) - if 0 <= offset < len(t): - t = zt' & len(z) == offset - add above constraints with t' - if offset >= len(t): - i = -1 - if offset < 0: - ? + + 0 <= offset < len(t) => xy = t & len(x) = offset & (-1 = indexof(t, s, 0) => -1 = i) + & (indexof(t, s, 0) >= 0 => indexof(t, s, 0) + offset = i) + + + offset = len(t) => i = -1 + + if offset < 0 or offset >= len(t) + under specified optional lemmas: (len(s) > len(t) -> i = -1) @@ -801,20 +796,45 @@ void theory_seq::add_indexof_axiom(expr* i) { minus_one = m_autil.mk_int(-1); zero = m_autil.mk_int(0); emp = m_util.str.mk_empty(m.get_sort(s)); - if (m_autil.is_numeral(offset, r) && r.is_zero()) { + literal offset_ne_zero = null_literal; + bool is_num = m_autil.is_numeral(offset, r); + if (is_num && r.is_zero()) { + offset_ne_zero = null_literal; + } + else { + offset_ne_zero = ~mk_eq(offset, zero, false); + } + if (!is_num || r.is_zero()) { expr_ref x = mk_skolem(m_contains_left_sym, t, s); expr_ref y = mk_skolem(m_contains_right_sym, t, s); xsy = m_util.str.mk_concat(x,s,y); literal cnt = mk_literal(m_util.str.mk_contains(t, s)); literal eq_empty = mk_eq(s, emp, false); - add_axiom(cnt, mk_eq(i, minus_one, false)); - add_axiom(~eq_empty, mk_eq(i, zero, false)); - add_axiom(~cnt, eq_empty, mk_eq(t, xsy, false)); - tightest_prefix(s, x, ~cnt); + add_axiom(offset_ne_zero, cnt, mk_eq(i, minus_one, false)); + add_axiom(offset_ne_zero, ~eq_empty, mk_eq(i, zero, false)); + add_axiom(offset_ne_zero, ~cnt, eq_empty, mk_eq(t, xsy, false)); + tightest_prefix(s, x, ~cnt, offset_ne_zero); } - else { - // TBD + if (is_num && r.is_zero()) { + return; } + // offset >= len(t) => indexof(s, t, offset) = -1 + expr_ref len_t(m_util.str.mk_length(t), m); + literal offset_ge_len = mk_literal(m_autil.mk_ge(mk_sub(offset, len_t), zero)); + add_axiom(offset_ge_len, mk_eq(i, minus_one, false)); + + // 0 <= offset & offset < len(t) => t = xy + // 0 <= offset & offset < len(t) => len(x) = offset + // 0 <= offset & offset < len(t) & ~contains(s, y) => indexof(t, s, offset) = -1 + // 0 <= offset & offset < len(t) & contains(s, y) => index(t, s, offset) = indexof(y, s, 0) + len(t) + expr_ref x = mk_skolem(symbol("seq.indexof.left"), t, s, offset); + expr_ref y = mk_skolem(symbol("seq.indexof.right"), t, s, offset); + expr_ref indexof(m_util.str.mk_index(y, s, zero), m); + // TBD: + //literal offset_ge_0 = mk_literal(m_autil.mk_ge(offset, zero)); + //add_axiom(~offset_ge_0, offset_ge_len, mk_eq(indexof, i, false)); + //add_axiom(~offset_ge_0, offset_ge_len, mk_eq(m_util.str.mk_length(x), offset, false)); + //add_axiom(~offset_ge_0, offset_ge_len, mk_eq(t, m_util.str.mk_concat(x, y), false)); } /* @@ -839,39 +859,56 @@ void theory_seq::add_replace_axiom(expr* r) { tightest_prefix(s, x, ~cnt); } +void theory_seq::add_length_unit_axiom(expr* n) { + if (!m_has_length) return; + SASSERT(m_util.str.is_unit(n)); + expr_ref one(m_autil.mk_int(1), m), len(m_util.str.mk_length(n), m); + add_axiom(mk_eq(len, one, false)); +} + +void theory_seq::add_length_empty_axiom(expr* n) { + if (!m_has_length) return; + SASSERT(m_util.str.is_empty(n)); + expr_ref zero(m_autil.mk_int(0), m), len(m_util.str.mk_length(n), m); + add_axiom(mk_eq(len, zero, false)); +} + +void theory_seq::add_length_string_axiom(expr* n) { + if (!m_has_length) return; + zstring s; + VERIFY(m_util.str.is_string(n, s)); + expr_ref len(m_util.str.mk_length(n), m); + expr_ref ls(m_autil.mk_numeral(rational(s.length(), rational::ui64()), true), m); + add_axiom(mk_eq(len, ls, false)); +} + +void theory_seq::add_length_concat_axiom(expr* n) { + if (!m_has_length) return; + expr* a, *b; + VERIFY(m_util.str.is_concat(n, a, b)); + expr_ref len(m_util.str.mk_length(n), m); + expr_ref _a(m_util.str.mk_length(a), m); + expr_ref _b(m_util.str.mk_length(b), m); + expr_ref a_p_b(m_autil.mk_add(_a, _b), m); + add_axiom(mk_eq(len, a_p_b, false)); +} + /* let n = len(x) len(x) >= 0 len(x) = 0 => x = "" x = "" => len(x) = 0 - len(x) = rewrite(len(x)) */ void theory_seq::add_length_axiom(expr* n) { - expr* x, *a, *b; + expr* x; VERIFY(m_util.str.is_length(n, x)); - expr_ref zero(m), one(m), emp(m); - zero = m_autil.mk_int(0); - std::string s; - if (m_util.str.is_unit(n)) { - one = m_autil.mk_int(1); - add_axiom(mk_eq(n, one, false)); - } - else if (m_util.str.is_empty(n)) { - add_axiom(mk_eq(n, zero, false)); - } - else if (m_util.str.is_string(n, s)) { - expr_ref ls(m_autil.mk_numeral(rational(s.length(), rational::ui64()), true), m); - add_axiom(mk_eq(n, ls, false)); - } - else if (m_util.str.is_concat(n, a, b)) { - expr_ref _a(m_util.str.mk_length(a), m); - expr_ref _b(m_util.str.mk_length(b), m); - expr_ref a_p_b(m_autil.mk_add(_a, _b), m); - add_axiom(mk_eq(n, a_p_b, false)); - } - else { - emp = m_util.str.mk_empty(m.get_sort(x)); + if (!m_util.str.is_unit(x) && + !m_util.str.is_empty(x) && + !m_util.str.is_string(x) && + !m_util.str.is_concat(x)) { + expr_ref zero(m_autil.mk_int(0), m); + expr_ref emp(m_util.str.mk_empty(m.get_sort(x)), m); literal eq1(mk_eq(zero, n, false)); literal eq2(mk_eq(x, emp, false)); add_axiom(mk_literal(m_autil.mk_ge(n, zero))); @@ -966,9 +1003,10 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) { } -expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2) { - expr* es[2] = { e1, e2 }; - return expr_ref(m_util.mk_skolem(name, e2?2:1, es, m.get_sort(e1)), m); +expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2, expr* e3) { + expr* es[3] = { e1, e2, e3 }; + unsigned len = e3?3:(e2?2:1); + return expr_ref(m_util.mk_skolem(name, len, es, m.get_sort(e1)), m); } void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) { @@ -1040,8 +1078,7 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { m.push_back(m_rhs.back(), o2); m_dam.push_back(m_deps.back(), m_dm.mk_leaf(enode_pair(n1, n2))); - new_eq_len_concat(n1, n2); - new_eq_len_concat(n2, n1); + // add length-equal axiom? } } @@ -1087,6 +1124,7 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) { m_rhs.pop_back(); m_deps.pop_back(); } + m_cache.reset(); } void theory_seq::restart_eh() { @@ -1108,7 +1146,11 @@ void theory_seq::relevant_eh(app* n) { m_util.str.is_index(n) || m_util.str.is_replace(n) || m_util.str.is_extract(n) || - m_util.str.is_at(n)) { + m_util.str.is_at(n) || + m_util.str.is_concat(n) || + m_util.str.is_empty(n) || + m_util.str.is_unit(n) || + m_util.str.is_string(n)) { enque_axiom(n); } } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 72363772b..1bf0454a8 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -87,6 +87,16 @@ namespace smt { void display(std::ostream& out) const; }; + class eval_cache { + obj_map m_map; + expr_ref_vector m_trail; + public: + eval_cache(ast_manager& m): m_trail(m) {} + bool find(expr* v, expr*& r) const { return m_map.find(v, r); } + void insert(expr* v, expr* r) { m_trail.push_back(v); m_trail.push_back(r); m_map.insert(v, r); } + void reset() { m_map.reset(); m_trail.reset(); } + }; + struct stats { stats() { reset(); } void reset() { memset(this, 0, sizeof(stats)); } @@ -101,6 +111,7 @@ namespace smt { solution_map m_rep; // unification representative. vector m_lhs, m_rhs; // persistent sets of equalities. vector m_deps; // persistent sets of dependencies. + eval_cache m_cache; ast2ast_trailmap m_sort2len_fn; // length functions per sort. seq_factory* m_factory; // value factory @@ -110,6 +121,7 @@ namespace smt { unsigned m_axioms_head; // index of first axiom to add. unsigned m_branch_variable_head; // index of first equation to examine. bool m_incomplete; // is the solver (clearly) incomplete for the fragment. + bool m_has_length; // is length applied bool m_model_completion; // during model construction, invent values in canonizer th_rewriter m_rewrite; seq_util m_util; @@ -185,15 +197,16 @@ namespace smt { void add_replace_axiom(expr* e); void add_extract_axiom(expr* e); void add_length_axiom(expr* n); + void add_length_unit_axiom(expr* n); + void add_length_empty_axiom(expr* n); + void add_length_concat_axiom(expr* n); + void add_length_string_axiom(expr* n); void add_at_axiom(expr* n); literal mk_literal(expr* n); - void tightest_prefix(expr* s, expr* x, literal lit); + void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal); expr* mk_sub(expr* a, expr* b); - void new_eq_len_concat(enode* n1, enode* n2); - - - expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0); + expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0, expr* e3 = 0); void set_incomplete(app* term); diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index f391dab40..58a0fa85f 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -71,8 +71,8 @@ namespace smt { } virtual bool get_some_values(sort* s, expr_ref& v1, expr_ref& v2) { if (u.is_string(s)) { - v1 = u.str.mk_string("a"); - v2 = u.str.mk_string("b"); + v1 = u.str.mk_string(symbol("a")); + v2 = u.str.mk_string(symbol("b")); return true; } NOT_IMPLEMENTED_YET(); From 72883df1344ace471c98e9cb0fe8bca7a6179f67 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 13 Dec 2015 16:02:17 -0800 Subject: [PATCH 3/4] fix build, add seq features Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 4 - src/ast/rewriter/seq_rewriter.cpp | 99 ++++++++++-- src/ast/rewriter/seq_rewriter.h | 4 +- src/muz/base/dl_context.h | 4 +- src/muz/rel/rel_context.cpp | 6 + src/smt/smt_setup.cpp | 2 +- src/smt/theory_seq.cpp | 250 +++++++++++++++++------------- src/smt/theory_seq.h | 70 +++++---- src/smt/theory_seq_empty.h | 11 +- src/util/scoped_vector.h | 128 +++++++++++++++ 10 files changed, 404 insertions(+), 174 deletions(-) create mode 100644 src/util/scoped_vector.h diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 27bfa6590..f5b2a1e6e 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -5693,8 +5693,6 @@ class Statistics: >>> s.check() sat >>> st = s.statistics() - >>> st.keys() - ['nlsat propagations', 'nlsat stages', 'rlimit count', 'max memory', 'memory', 'num allocs'] """ return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))] @@ -5730,8 +5728,6 @@ class Statistics: >>> s.check() sat >>> st = s.statistics() - >>> st.keys() - ['nlsat propagations', 'nlsat stages', 'rlimit count', 'max memory', 'memory', 'num allocs'] >>> st.nlsat_propagations 2 >>> st.nlsat_stages diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 1eaf6b42b..d61ccc4a5 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -520,6 +520,7 @@ br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) { bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs) { expr* a, *b; + zstring s; bool change = false; expr_ref_vector trail(m()); m_lhs.reset(); @@ -528,23 +529,55 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve 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()) { + while (true) { + while (!m_rhs.empty() && m_util.str.is_empty(m_rhs.back())) { + m_rhs.pop_back(); + change = true; + } + while (!m_lhs.empty() && m_util.str.is_empty(m_lhs.back())) { + m_lhs.pop_back(); + change = true; + } + if (m_lhs.empty() || m_rhs.empty()) { + break; + } + expr* l = m_lhs.back(); + expr* r = m_rhs.back(); + if (m_util.str.is_unit(r) && m_util.str.is_string(l)) { + std::swap(l, r); + std::swap(m_lhs, m_rhs); + } + if (l == r) { 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)) { + else if(m_util.str.is_unit(l, a) && + m_util.str.is_unit(r, 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())) { + else if (m_util.str.is_unit(l, a) && m_util.str.is_string(r, s)) { + SASSERT(s.length() > 0); + + unsigned ch = s[s.length()-1]; + SASSERT(s.num_bits() == m_butil.get_bv_size(a)); + expr_ref bv(m()); + + bv = m_butil.mk_numeral(ch, s.num_bits()); + SASSERT(m_butil.is_bv(a)); + lhs.push_back(bv); + rhs.push_back(a); m_lhs.pop_back(); + if (s.length() == 1) { + m_rhs.pop_back(); + } + else { + expr_ref s2(m_util.str.mk_string(s.extract(0, s.length()-2)), m()); + m_rhs[m_rhs.size()-1] = s2; + trail.push_back(s2); + } } else { break; @@ -554,23 +587,55 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve // solve from front unsigned head1 = 0, head2 = 0; - while (head1 < m_lhs.size() && head2 < m_rhs.size()) { - if (m_lhs[head1] == m_rhs[head2]) { + while (true) { + while (head1 < m_lhs.size() && m_util.str.is_empty(m_lhs[head1])) { + ++head1; + } + while (head2 < m_rhs.size() && m_util.str.is_empty(m_rhs[head2])) { + ++head2; + } + if (head1 == m_lhs.size() || head2 == m_rhs.size()) { + break; + } + SASSERT(head1 < m_lhs.size() && head2 == m_rhs.size()); + + expr* l = m_lhs[head1]; + expr* r = m_rhs[head2]; + if (m_util.str.is_unit(r) && m_util.str.is_string(l)) { + std::swap(l, r); + std::swap(m_lhs, m_rhs); + } + if (l == r) { ++head1; ++head2; } - else if(m_util.str.is_unit(m_lhs[head1], a) && - m_util.str.is_unit(m_rhs[head2], b)) { + else if(m_util.str.is_unit(l, a) && + m_util.str.is_unit(r, 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 if (m_util.str.is_unit(l, a) && m_util.str.is_string(r, s)) { + SASSERT(s.length() > 0); + + unsigned ch = s[0]; + SASSERT(s.num_bits() == m_butil.get_bv_size(a)); + expr_ref bv(m()); + + bv = m_butil.mk_numeral(ch, s.num_bits()); + SASSERT(m_butil.is_bv(a)); + lhs.push_back(bv); + rhs.push_back(a); + m_lhs.pop_back(); + if (s.length() == 1) { + m_rhs.pop_back(); + } + else { + expr_ref s2(m_util.str.mk_string(s.extract(1, s.length()-1)), m()); + m_rhs[m_rhs.size()-1] = s2; + trail.push_back(s2); + } } else { break; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index de3634a51..ffc8addd3 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -21,6 +21,7 @@ Notes: #include"seq_decl_plugin.h" #include"arith_decl_plugin.h" +#include"bv_decl_plugin.h" #include"rewriter_types.h" #include"params.h" #include"lbool.h" @@ -32,6 +33,7 @@ Notes: class seq_rewriter { seq_util m_util; arith_util m_autil; + bv_util m_butil; ptr_vector m_es, m_lhs, m_rhs; br_status mk_seq_concat(expr* a, expr* b, expr_ref& result); @@ -63,7 +65,7 @@ class seq_rewriter { public: seq_rewriter(ast_manager & m, params_ref const & p = params_ref()): - m_util(m), m_autil(m) { + m_util(m), m_autil(m), m_butil(m) { } ast_manager & m() const { return m_util.get_manager(); } family_id get_fid() const { return m_util.get_family_id(); } diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index e5639959b..f37169cac 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -487,9 +487,7 @@ namespace datalog { // ----------------------------------- bool canceled() { - if (m.limit().inc()) return true; - m_last_status = CANCELED; - return false; + return m.canceled() && (m_last_status = CANCELED, true); } void cleanup(); diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index 25af7d798..68bc25c27 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -151,6 +151,7 @@ namespace datalog { m_context.ensure_closed(); transform_rules(); if (m_context.canceled()) { + TRACE("dl", tout << "canceled\n";); result = l_undef; break; } @@ -191,6 +192,7 @@ namespace datalog { IF_VERBOSE(10, m_ectx.report_big_relations(1000, verbose_stream());); if (m_context.canceled()) { + TRACE("dl", tout << "canceled\n";); result = l_undef; break; } @@ -206,6 +208,7 @@ namespace datalog { } if (timeout_after_this_round) { m_context.set_status(TIMEOUT); + TRACE("dl", tout << "timeout\n";); result = l_undef; break; } @@ -272,6 +275,7 @@ namespace datalog { if (some_non_empty) { m_answer = mk_and(m, ans.size(), ans.c_ptr()); if (is_approx) { + TRACE("dl", tout << "approx\n";); res = l_undef; m_context.set_status(APPROX); } @@ -286,6 +290,7 @@ namespace datalog { m_answer = m.mk_false(); break; case l_undef: + TRACE("dl", tout << "saturation in undef\n";); break; } return res; @@ -367,6 +372,7 @@ namespace datalog { m_last_result_relation->to_formula(m_answer); if (!m_last_result_relation->is_precise()) { m_context.set_status(APPROX); + TRACE("dl", tout << "approx\n";); res = l_undef; } } diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 8a40f9d7a..8ebfa2d71 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -815,7 +815,7 @@ namespace smt { } void setup::setup_seq() { - m_context.register_plugin(alloc(theory_seq, m_manager)); + m_context.register_plugin(alloc(theory_seq_empty, m_manager)); } void setup::setup_card() { diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 67ab2cfe3..718e3fd70 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -27,6 +27,7 @@ Revision History: using namespace smt; void theory_seq::solution_map::update(expr* e, expr* r, enode_pair_dependency* d) { + m_cache.reset(); std::pair value; if (m_map.find(e, value)) { add_trail(DEL, e, value.first, value.second); @@ -47,21 +48,17 @@ void theory_seq::solution_map::add_trail(map_update op, expr* l, expr* r, enode_ expr* theory_seq::solution_map::find(expr* e, enode_pair_dependency*& d) { std::pair value; d = 0; - 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; - } - 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) { if (num_scopes == 0) return; + m_cache.reset(); unsigned start = m_limit[m_limit.size() - num_scopes]; for (unsigned i = m_updates.size(); i > start; ) { --i; @@ -80,7 +77,7 @@ void theory_seq::solution_map::pop_scope(unsigned num_scopes) { } void theory_seq::solution_map::display(std::ostream& out) const { - map_t::iterator it = m_map.begin(), end = m_map.end(); + eqdep_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"; } @@ -125,10 +122,7 @@ void theory_seq::exclusion_table::display(std::ostream& out) const { theory_seq::theory_seq(ast_manager& m): theory(m.mk_family_id("seq")), m(m), - m_dam(m_dep_array_value_manager, m_alloc), m_rep(m, m_dm), - m_cache(m), - m_sort2len_fn(m), m_factory(0), m_ineqs(m), m_exclude(m), @@ -142,9 +136,6 @@ theory_seq::theory_seq(ast_manager& m): m_util(m), m_autil(m), m_trail_stack(*this) { - m_lhs.push_back(expr_array()); - m_rhs.push_back(expr_array()); - m_deps.push_back(enode_pair_dependency_array()); m_prefix_sym = "seq.prefix.suffix"; m_suffix_sym = "seq.suffix.prefix"; m_left_sym = "seq.left"; @@ -154,11 +145,6 @@ theory_seq::theory_seq(ast_manager& m): } 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()); } @@ -183,10 +169,14 @@ final_check_status theory_seq::final_check_eh() { if (ctx.inconsistent()) { return FC_CONTINUE; } - if (m.size(m_lhs.back()) > 0 || m_incomplete) { - return FC_GIVEUP; + if (!check_length_coherence()) { + return FC_CONTINUE; } - return FC_DONE; + if (is_solved()) { + return FC_DONE; + } + + return FC_GIVEUP; } bool theory_seq::check_ineqs() { @@ -201,6 +191,9 @@ bool theory_seq::check_ineqs() { propagate_lit(eqs, ctx.get_literal(a)); return false; } + else if (!m.is_false(b)) { + TRACE("seq", tout << "equality is undetermined: " << mk_pp(a, m) << " " << b << "\n";); + } } return true; } @@ -208,18 +201,15 @@ bool theory_seq::check_ineqs() { bool theory_seq::branch_variable() { context& ctx = get_context(); TRACE("seq", ctx.display(tout);); - expr_array& lhs = m_lhs.back(); - expr_array& rhs = m_rhs.back(); - unsigned sz = m.size(lhs); + unsigned sz = m_eqs.size(); ptr_vector ls, rs; for (unsigned i = 0; i < sz; ++i) { unsigned k = (i + m_branch_variable_head) % sz; - expr* l = m.get(lhs, k); - expr* r = m.get(rhs, k); - TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << "\n";); + eq e = m_eqs[k]; + TRACE("seq", tout << e.m_lhs << " = " << e.m_rhs << "\n";); ls.reset(); rs.reset(); - m_util.str.get_concat(l, ls); - m_util.str.get_concat(r, rs); + m_util.str.get_concat(e.m_lhs, ls); + m_util.str.get_concat(e.m_rhs, rs); if (!ls.empty() && find_branch_candidate(ls[0], rs)) { m_branch_variable_head = k; @@ -290,13 +280,90 @@ bool theory_seq::split_variable() { return false; } +bool theory_seq::check_length_coherence() { + if (!m_has_length) return true; + return false; + context& ctx = get_context(); + bool coherent = true; + for (unsigned i = 0; i < m_eqs.size(); ++i) { + m_eqs[i].m_dep; + expr_ref v1(m), v2(m), l(m_eqs[i].m_lhs), r(m_eqs[i].m_rhs); + expr_ref len1(m_util.str.mk_length(l), m); + expr_ref len2(m_util.str.mk_length(r), m); + if (!ctx.e_internalized(len1)) ctx.internalize(len1, false); + if (!ctx.e_internalized(len2)) ctx.internalize(len2, false); + enode* n1 = get_enode(len1); + enode* n2 = get_enode(len2); + if (n1->get_root() != n2->get_root()) { + propagate_eq(m_eqs[i].m_dep, n1, n2); + coherent = false; + } + } + // each variable that canonizes to itself can have length 0. + unsigned sz = get_num_vars(); + for (unsigned i = 0; i < sz; ++i) { + enode* n = get_enode(i); + expr* e = n->get_owner(); + if (!m_util.is_seq(e)) { + continue; + } + // extend length of variables. + enode_pair_dependency* dep = 0; + if (is_var(m_rep.find(e, dep))) { + expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m); + if (!assume_equality(e, emp)) { + // e = emp \/ e = head*tail & head = unit(v) + // add_axiom(mk_eq(e, emp, false), mk_eq(e, m_util.mk_concat(x, y), e)); + // add_axiom(mk_eq(e, emp, false), mk_eq(x, unit_x)); + } + coherent = false; + } + } + + return coherent; +} + +bool theory_seq::check_ineq_coherence() { + bool all_false = true; + for (unsigned i = 0; all_false && i < m_ineqs.size(); ++i) { + expr* a = m_ineqs[i].get(); + enode_pair_dependency* eqs = 0; + expr_ref b = canonize(a, eqs); + all_false = m.is_false(b); + if (all_false) { + TRACE("seq", tout << "equality is undetermined: " << mk_pp(a, m) << " " << b << "\n";); + } + } + return all_false; +} + +/* + - Eqs = 0 + - Diseqs evaluate to false + - lengths are coherent. +*/ + +bool theory_seq::is_solved() { + if (!m_eqs.empty()) { + return false; + } + if (!check_ineq_coherence()) { + return false; + } + + SASSERT(check_length_coherence()); + + return true; + +} + void theory_seq::propagate_lit(enode_pair_dependency* dep, literal lit) { 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 << " <-\n"; display_deps(tout, dep);); + tout << " <- "; display_deps(tout, dep);); justification* js = ctx.mk_justification( ext_theory_propagation_justification( @@ -321,7 +388,7 @@ void theory_seq::propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2) vector _eqs; m_dm.linearize(dep, _eqs); TRACE("seq", - tout << mk_pp(n1->get_owner(), m) << " " << mk_pp(n2->get_owner(), m) << " <- "; + tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << " <- "; display_deps(tout, dep); ); @@ -351,14 +418,12 @@ bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_dependency* deps) { } 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()); - m_dam.push_back(m_deps.back(), deps); + m_eqs.push_back(eq(expr_ref(lhs[i].get(), m), expr_ref(rhs[i].get(), m), 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) << "; "; + for (unsigned i = 0; i < m_eqs.size(); ++i) { + tout << m_eqs[i].m_lhs << " = " << m_eqs[i].m_rhs << "; "; } tout << "\n"; ); @@ -428,7 +493,6 @@ bool theory_seq::is_right_select(expr* a, expr*& b) { void theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) { context& ctx = get_context(); m_rep.update(l, r, deps); - m_cache.reset(); // TBD: skip new equalities for non-internalized terms. if (ctx.e_internalized(l) && ctx.e_internalized(r)) { propagate_eq(deps, ctx.get_enode(l), ctx.get_enode(r)); @@ -446,23 +510,19 @@ bool theory_seq::solve_basic_eqs() { 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) { + for (unsigned i = 0; !ctx.inconsistent() && i < m_eqs.size(); ++i) { + eq e = m_eqs[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)); + simplify_eq(e.m_lhs, e.m_rhs, e.m_dep): + solve_unit_eq(e.m_lhs, e.m_rhs, e.m_dep)) { + if (i + 1 != m_eqs.size()) { + eq e1 = m_eqs[m_eqs.size()-1]; + m_eqs.set(i, e1); --i; ++m_stats.m_num_reductions; } - m.pop_back(lhs); - m.pop_back(rhs); - m_dam.pop_back(deps); + m_eqs.pop_back(); change = true; } } @@ -525,11 +585,6 @@ bool theory_seq::internalize_term(app* term) { !m_util.is_skolem(term)) { set_incomplete(term); } - expr* arg; - func_decl* fn; - if (m_util.str.is_length(term, arg) && !m_sort2len_fn.find(m.get_sort(arg), fn)) { - m_trail_stack.push(ast2ast_trail(m_sort2len_fn, m.get_sort(arg), term->get_decl())); - } return true; } @@ -538,14 +593,14 @@ void theory_seq::apply_sort_cnstr(enode* n, sort* s) { } void theory_seq::display(std::ostream & out) const { - if (m.size(m_lhs.back()) == 0 && + if (m_eqs.size() == 0 && m_ineqs.empty() && m_rep.empty() && m_exclude.empty()) { return; } out << "Theory seq\n"; - if (m.size(m_lhs.back()) > 0) { + if (m_eqs.size() > 0) { out << "Equations:\n"; display_equations(out); } @@ -566,22 +621,20 @@ void theory_seq::display(std::ostream & out) const { } void theory_seq::display_equations(std::ostream& out) const { - expr_array const& lhs = m_lhs.back(); - expr_array const& rhs = m_rhs.back(); - enode_pair_dependency_array const& deps = m_deps.back(); - 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"; - display_deps(out, m_dam.get(deps, i)); + for (unsigned i = 0; i < m_eqs.size(); ++i) { + eq const& e = m_eqs[i]; + out << e.m_lhs << " = " << e.m_rhs << " <- "; + display_deps(out, e.m_dep); } } void theory_seq::display_deps(std::ostream& out, enode_pair_dependency* dep) const { - if (!dep) return; 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 << " " << mk_pp(_eqs[i].first->get_owner(), m) << " = " << mk_pp(_eqs[i].second->get_owner(), m); } + out << "\n"; } void theory_seq::collect_statistics(::statistics & st) const { @@ -642,36 +695,38 @@ expr_ref theory_seq::canonize(expr* e, enode_pair_dependency*& eqs) { expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) { enode_pair_dependency* deps = 0; + expr_dep ed; expr* r = 0; - if (m_cache.find(e, r)) { - return expr_ref(r, m); + + if (m_rep.find_cache(e, ed)) { + eqs = m_dm.mk_join(eqs, ed.second); + return expr_ref(ed.first, m); } e = m_rep.find(e, deps); expr_ref result(m); expr* e1, *e2; - eqs = m_dm.mk_join(eqs, deps); if (m_util.str.is_concat(e, e1, e2)) { - result = m_util.str.mk_concat(expand(e1, eqs), expand(e2, eqs)); + result = m_util.str.mk_concat(expand(e1, deps), expand(e2, deps)); } else if (m_util.str.is_empty(e) || m_util.str.is_string(e)) { result = e; } else if (m.is_eq(e, e1, e2)) { - result = m.mk_eq(expand(e1, eqs), expand(e2, eqs)); + result = m.mk_eq(expand(e1, deps), expand(e2, deps)); } else if (m_util.str.is_prefix(e, e1, e2)) { - result = m_util.str.mk_prefix(expand(e1, eqs), expand(e2, eqs)); + result = m_util.str.mk_prefix(expand(e1, deps), expand(e2, deps)); } else if (m_util.str.is_suffix(e, e1, e2)) { - result = m_util.str.mk_suffix(expand(e1, eqs), expand(e2, eqs)); + result = m_util.str.mk_suffix(expand(e1, deps), expand(e2, deps)); } else if (m_util.str.is_contains(e, e1, e2)) { - result = m_util.str.mk_contains(expand(e1, eqs), expand(e2, eqs)); + result = m_util.str.mk_contains(expand(e1, deps), expand(e2, deps)); } else if (m_model_completion && is_var(e)) { SASSERT(m_factory); expr_ref val(m); - val = m_factory->get_fresh_value(m.get_sort(e)); + val = m_factory->get_some_value(m.get_sort(e)); if (val) { m_rep.update(e, val, 0); result = val; @@ -683,7 +738,8 @@ expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) { else { result = e; } - m_cache.insert(e, result); + m_rep.add_cache(e, expr_dep(result, deps)); + eqs = m_dm.mk_join(eqs, deps); return result; } @@ -1072,13 +1128,10 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { enode* n1 = get_enode(v1); enode* n2 = get_enode(v2); if (n1 != n2) { - expr* o1 = n1->get_owner(), *o2 = n2->get_owner(); - TRACE("seq", tout << mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";); - m.push_back(m_lhs.back(), o1); - m.push_back(m_rhs.back(), o2); - m_dam.push_back(m_deps.back(), m_dm.mk_leaf(enode_pair(n1, n2))); - - // add length-equal axiom? + expr_ref o1(n1->get_owner(), m); + expr_ref o2(n2->get_owner(), m); + TRACE("seq", tout << o1 << " = " << o2 << "\n";); + m_eqs.push_back(eq(o1, o2, m_dm.mk_leaf(enode_pair(n1, n2)))); } } @@ -1091,54 +1144,27 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { } void theory_seq::push_scope_eh() { - TRACE("seq", tout << "push " << m_lhs.size() << "\n";); + TRACE("seq", tout << "push " << m_eqs.size() << "\n";); theory::push_scope_eh(); m_rep.push_scope(); m_exclude.push_scope(); m_dm.push_scope(); m_trail_stack.push_scope(); m_trail_stack.push(value_trail(m_axioms_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); + m_eqs.push_scope(); } void theory_seq::pop_scope_eh(unsigned num_scopes) { - TRACE("seq", tout << "pop " << m_lhs.size() << "\n";); + TRACE("seq", tout << "pop " << m_eqs.size() << "\n";); m_trail_stack.pop_scope(num_scopes); theory::pop_scope_eh(num_scopes); m_dm.pop_scope(num_scopes); m_rep.pop_scope(num_scopes); m_exclude.pop_scope(num_scopes); - while (num_scopes > 0) { - --num_scopes; - m.del(m_lhs.back()); - m.del(m_rhs.back()); - m_dam.del(m_deps.back()); - m_lhs.pop_back(); - m_rhs.pop_back(); - m_deps.pop_back(); - } - m_cache.reset(); + m_eqs.pop_scopes(num_scopes); } void theory_seq::restart_eh() { -#if 0 - 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()); -#endif } void theory_seq::relevant_eh(app* n) { diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 1bf0454a8..ad500aac6 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -23,37 +23,38 @@ Revision History: #include "seq_decl_plugin.h" #include "theory_seq_empty.h" #include "th_rewriter.h" -#include "union_find.h" #include "ast_trail.h" +#include "scoped_vector.h" 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; + typedef std::pair expr_dep; + typedef obj_map eqdep_map_t; + + // cache to track evaluations under equalities + class eval_cache { + eqdep_map_t m_map; + expr_ref_vector m_trail; + public: + eval_cache(ast_manager& m): m_trail(m) {} + bool find(expr* v, expr_dep& r) const { return m_map.find(v, r); } + void insert(expr* v, expr_dep& r) { m_trail.push_back(v); m_trail.push_back(r.first); m_map.insert(v, r); } + void reset() { m_map.reset(); m_trail.reset(); } + }; + // map from variables to representatives + // + a cache for normalization. class solution_map { enum map_update { INS, DEL }; - typedef obj_map > map_t; ast_manager& m; enode_pair_dependency_manager& m_dm; - map_t m_map; + eqdep_map_t m_map; + eval_cache m_cache; expr_ref_vector m_lhs, m_rhs; ptr_vector m_deps; svector m_updates; @@ -61,15 +62,20 @@ namespace smt { void add_trail(map_update op, expr* l, expr* r, enode_pair_dependency* d); public: - solution_map(ast_manager& m, enode_pair_dependency_manager& dm): m(m), m_dm(dm), m_lhs(m), m_rhs(m) {} + solution_map(ast_manager& m, enode_pair_dependency_manager& dm): + m(m), m_cache(m), m_dm(dm), m_lhs(m), m_rhs(m) {} bool empty() const { return m_map.empty(); } void update(expr* e, expr* r, enode_pair_dependency* d); + void add_cache(expr* v, expr_dep& r) { m_cache.insert(v, r); } + bool find_cache(expr* v, expr_dep& r) { return m_cache.find(v, r); } expr* find(expr* e, enode_pair_dependency*& d); + void cache(expr* e, expr* r, 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; }; + // Table of current disequalities class exclusion_table { typedef obj_pair_hashtable table_t; ast_manager& m; @@ -87,14 +93,15 @@ namespace smt { void display(std::ostream& out) const; }; - class eval_cache { - obj_map m_map; - expr_ref_vector m_trail; - public: - eval_cache(ast_manager& m): m_trail(m) {} - bool find(expr* v, expr*& r) const { return m_map.find(v, r); } - void insert(expr* v, expr* r) { m_trail.push_back(v); m_trail.push_back(r); m_map.insert(v, r); } - void reset() { m_map.reset(); m_trail.reset(); } + // Asserted or derived equality with dependencies + struct eq { + expr_ref m_lhs; + expr_ref m_rhs; + enode_pair_dependency* m_dep; + eq(expr_ref& l, expr_ref& r, enode_pair_dependency* d): + m_lhs(l), m_rhs(r), m_dep(d) {} + eq(eq const& other): m_lhs(other.m_lhs), m_rhs(other.m_rhs), m_dep(other.m_dep) {} + eq& operator=(eq const& other) { m_lhs = other.m_lhs; m_rhs = other.m_rhs; m_dep = other.m_dep; return *this; } }; struct stats { @@ -104,16 +111,10 @@ namespace smt { unsigned m_num_reductions; }; 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; solution_map m_rep; // unification representative. - vector m_lhs, m_rhs; // persistent sets of equalities. - vector m_deps; // persistent sets of dependencies. - eval_cache m_cache; + scoped_vector m_eqs; // set of current equations. - ast2ast_trailmap m_sort2len_fn; // length functions per sort. seq_factory* m_factory; // value factory expr_ref_vector m_ineqs; // inequalities to check solution against exclusion_table m_exclude; // set of asserted disequalities. @@ -162,6 +163,9 @@ namespace smt { bool simplify_and_solve_eqs(); // solve unitary equalities bool branch_variable(); // branch on a variable bool split_variable(); // split a variable + bool is_solved(); + bool check_length_coherence(); + bool check_ineq_coherence(); bool pre_process_eqs(bool simplify_or_solve); bool simplify_eqs(); diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index 58a0fa85f..04f38020c 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -64,9 +64,14 @@ namespace smt { } virtual expr* get_some_value(sort* s) { - if (u.is_string(s)) - return u.str.mk_string(symbol("")); - NOT_IMPLEMENTED_YET(); + if (u.is_seq(s)) { + return u.str.mk_empty(s); + } + sort* seq = 0; + if (u.is_re(s, seq)) { + return u.re.mk_to_re(u.str.mk_empty(seq)); + } + UNREACHABLE(); return 0; } virtual bool get_some_values(sort* s, expr_ref& v1, expr_ref& v2) { diff --git a/src/util/scoped_vector.h b/src/util/scoped_vector.h new file mode 100644 index 000000000..ed75fd561 --- /dev/null +++ b/src/util/scoped_vector.h @@ -0,0 +1,128 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + scoped_vector.h + +Abstract: + + Vector that restores during backtracking. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-12-13 + +Revision History: + +--*/ +#ifndef SCOPED_VECTOR_H_ +#define SCOPED_VECTOR_H_ + +#include"vector.h" + +template +class scoped_vector { + unsigned m_size; + unsigned m_elems_start; + unsigned_vector m_sizes; + vector m_elems; + unsigned_vector m_elems_lim; + unsigned_vector m_index; + unsigned_vector m_src, m_dst; + unsigned_vector m_src_lim; +public: + scoped_vector(): m_size(0), m_elems_start(0) {} + + // m_index : External-Index -> Internal-Index + // m_index.size() = max(m_sizes) + // m_src[i] -> m_dst[i] // trail into m_index updates + // m_src_lim last index to be updated. + + void push_scope() { + m_elems_start = m_elems.size(); + m_sizes.push_back(m_size); + m_src_lim.push_back(m_src.size()); + m_elems_lim.push_back(m_elems_start); + } + + void pop_scopes(unsigned num_scopes) { + if (num_scopes == 0) return; + unsigned new_size = m_sizes.size() - num_scopes; + unsigned src_lim = m_src_lim[new_size]; + + for (unsigned i = m_src.size(); i > src_lim; ) { + --i; + m_index[m_src[i]] = m_dst[i]; + } + m_src.shrink(src_lim); + m_dst.shrink(src_lim); + m_src_lim.shrink(new_size); + + m_elems.shrink(m_elems_lim[new_size]); + m_elems_lim.resize(new_size); + m_elems_start = m_elems.size(); + + m_size = m_sizes[new_size]; + m_sizes.shrink(new_size); + } + + T const& operator[](unsigned idx) const { + SASSERT(idx < m_size); + return m_elems[m_index[idx]]; + } + + void set(unsigned idx, T const& t) { + SASSERT(idx < m_size); + unsigned n = m_index[idx]; + if (n >= m_elems_start) { + m_elems[n] = t; + } + else { + set_index(idx, m_elems.size()); + m_elems.push_back(t); + } + SASSERT(invariant()); + } + + void push_back(T const& t) { + set_index(m_size, m_elems.size()); + m_elems.push_back(t); + ++m_size; + SASSERT(invariant()); + } + + void pop_back() { + SASSERT(m_size > 0); + if (m_size == m_elems.size() && m_size > m_elems_start) { + m_elems.pop_back(); + } + --m_size; + SASSERT(invariant()); + } + + unsigned size() const { return m_size; } + + bool empty() const { return m_size == 0; } + +private: + void set_index(unsigned src, unsigned dst) { + while (src >= m_index.size()) { + m_index.push_back(0); + } + SASSERT(src < m_index.size()); + if (src < m_elems_start) { + m_src.push_back(src); + m_dst.push_back(m_index[src]); + } + m_index[src] = dst; + } + + bool invariant() const { + return + m_size <= m_elems.size() && + m_elems_start <= m_elems.size(); + } +}; + +#endif From f3d94db88946ae7870f51e676c26ace5de042bc5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 13 Dec 2015 23:47:45 -0800 Subject: [PATCH 4/4] bild on gcc #376 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 2 +- src/ast/seq_decl_plugin.h | 2 + src/smt/theory_seq.cpp | 103 ++++++++++++++++++++---------- src/smt/theory_seq.h | 4 +- src/util/scoped_vector.h | 3 +- 5 files changed, 77 insertions(+), 37 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index d61ccc4a5..d8afe0b49 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -597,7 +597,7 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve if (head1 == m_lhs.size() || head2 == m_rhs.size()) { break; } - SASSERT(head1 < m_lhs.size() && head2 == m_rhs.size()); + SASSERT(head1 < m_lhs.size() && head2 < m_rhs.size()); expr* l = m_lhs[head1]; expr* r = m_rhs[head2]; diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 156bf4735..ce63f8dc8 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -192,6 +192,7 @@ public: bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); } bool is_re(sort* s, sort*& seq) const { return is_sort_of(s, m_fid, RE_SORT) && (seq = to_sort(s->get_parameter(0).get_ast()), true); } bool is_seq(expr* e) const { return is_seq(m.get_sort(e)); } + bool is_seq(sort* s, sort*& seq) { return is_seq(s) && (seq = to_sort(s->get_parameter(0).get_ast()), true); } bool is_re(expr* e) const { return is_re(m.get_sort(e)); } bool is_re(expr* e, sort*& seq) const { return is_re(m.get_sort(e), seq); } @@ -225,6 +226,7 @@ public: app* mk_prefix(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_PREFIX, 2, es); } app* mk_suffix(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_SUFFIX, 2, es); } app* mk_index(expr* a, expr* b, expr* i) { expr* es[3] = { a, b, i}; return m.mk_app(m_fid, OP_SEQ_INDEX, 3, es); } + app* mk_unit(expr* u) { return m.mk_app(m_fid, OP_SEQ_UNIT, 1, &u); } bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 718e3fd70..f27043e8d 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -161,18 +161,26 @@ final_check_status theory_seq::final_check_eh() { return FC_CONTINUE; } if (branch_variable()) { + TRACE("seq", tout << "branch\n";); return FC_CONTINUE; } if (split_variable()) { + TRACE("seq", tout << "split_variable\n";); return FC_CONTINUE; } if (ctx.inconsistent()) { return FC_CONTINUE; } if (!check_length_coherence()) { + TRACE("seq", tout << "check_length_coherence\n";); return FC_CONTINUE; } + if (!check_length_coherence_tbd()) { + TRACE("seq", tout << "check_length_coherence\n";); + return FC_GIVEUP; + } if (is_solved()) { + TRACE("seq", tout << "is_solved\n";); return FC_DONE; } @@ -192,7 +200,7 @@ bool theory_seq::check_ineqs() { return false; } else if (!m.is_false(b)) { - TRACE("seq", tout << "equality is undetermined: " << mk_pp(a, m) << " " << b << "\n";); + TRACE("seq", tout << "Disequality is undetermined: " << mk_pp(a, m) << " " << b << "\n";); } } return true; @@ -200,7 +208,6 @@ bool theory_seq::check_ineqs() { bool theory_seq::branch_variable() { context& ctx = get_context(); - TRACE("seq", ctx.display(tout);); unsigned sz = m_eqs.size(); ptr_vector ls, rs; for (unsigned i = 0; i < sz; ++i) { @@ -266,11 +273,11 @@ bool theory_seq::assume_equality(expr* l, expr* r) { } else { TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << "\n";); - if (!ctx.e_internalized(l)) ctx.internalize(l, false); - if (!ctx.e_internalized(r)) ctx.internalize(r, false); - ctx.mark_as_relevant(ctx.get_enode(l)); - ctx.mark_as_relevant(ctx.get_enode(r)); - ctx.assume_eq(ctx.get_enode(l), ctx.get_enode(r)); + enode* n1 = ensure_enode(l); + enode* n2 = ensure_enode(r); + ctx.mark_as_relevant(n1); + ctx.mark_as_relevant(n2); + ctx.assume_eq(n1, n2); return true; } } @@ -282,7 +289,6 @@ bool theory_seq::split_variable() { bool theory_seq::check_length_coherence() { if (!m_has_length) return true; - return false; context& ctx = get_context(); bool coherent = true; for (unsigned i = 0; i < m_eqs.size(); ++i) { @@ -290,38 +296,54 @@ bool theory_seq::check_length_coherence() { expr_ref v1(m), v2(m), l(m_eqs[i].m_lhs), r(m_eqs[i].m_rhs); expr_ref len1(m_util.str.mk_length(l), m); expr_ref len2(m_util.str.mk_length(r), m); - if (!ctx.e_internalized(len1)) ctx.internalize(len1, false); - if (!ctx.e_internalized(len2)) ctx.internalize(len2, false); - enode* n1 = get_enode(len1); - enode* n2 = get_enode(len2); + enode* n1 = ensure_enode(len1); + enode* n2 = ensure_enode(len2); if (n1->get_root() != n2->get_root()) { + TRACE("seq", tout << len1 << " = " << len2 << "\n";); propagate_eq(m_eqs[i].m_dep, n1, n2); coherent = false; } } + return coherent; +} + +bool theory_seq::check_length_coherence_tbd() { + if (!m_has_length) return true; + context& ctx = get_context(); + bool coherent = true; // each variable that canonizes to itself can have length 0. unsigned sz = get_num_vars(); for (unsigned i = 0; i < sz; ++i) { enode* n = get_enode(i); expr* e = n->get_owner(); - if (!m_util.is_seq(e)) { + if (m_util.is_re(e)) { continue; } + SASSERT(m_util.is_seq(e)); // extend length of variables. enode_pair_dependency* dep = 0; - if (is_var(m_rep.find(e, dep))) { + expr* f = m_rep.find(e, dep); + if (is_var(f) && f == e) { expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m); + TRACE("seq", tout << "Unsolved " << mk_pp(e, m) << "\n";); +#if 0 if (!assume_equality(e, emp)) { // e = emp \/ e = head*tail & head = unit(v) - // add_axiom(mk_eq(e, emp, false), mk_eq(e, m_util.mk_concat(x, y), e)); - // add_axiom(mk_eq(e, emp, false), mk_eq(x, unit_x)); + sort* char_sort = 0; + VERIFY(m_util.is_seq(m.get_sort(e), char_sort)); + expr_ref tail(mk_skolem(symbol("seq.tail"), e), m); + expr_ref v(mk_skolem(symbol("seq.head.elem"), e, 0, 0, char_sort), m); + expr_ref head(m_util.str.mk_unit(v), m); + expr_ref conc(m_util.str.mk_concat(head, tail), m); + literal e_eq_emp(mk_eq(e, emp, false)); + add_axiom(e_eq_emp, mk_eq(e, conc, false)); } +#endif coherent = false; } } - return coherent; -} +} bool theory_seq::check_ineq_coherence() { bool all_false = true; @@ -418,7 +440,14 @@ bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_dependency* deps) { } SASSERT(lhs.size() == rhs.size()); for (unsigned i = 0; i < lhs.size(); ++i) { - m_eqs.push_back(eq(expr_ref(lhs[i].get(), m), expr_ref(rhs[i].get(), m), deps)); + expr_ref l(lhs[i].get(), m); + expr_ref r(rhs[i].get(), m); + if (m_util.is_seq(l) || m_util.is_re(l)) { + m_eqs.push_back(eq(l, r, deps)); + } + else { + propagate_eq(deps, ensure_enode(l), ensure_enode(r)); + } } TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << " => "; @@ -552,10 +581,7 @@ bool theory_seq::internalize_term(app* term) { unsigned num_args = term->get_num_args(); for (unsigned i = 0; i < num_args; i++) { expr* arg = term->get_arg(i); - ctx.internalize(arg, false); - if (ctx.e_internalized(arg)) { - mk_var(ctx.get_enode(arg)); - } + mk_var(ensure_enode(arg)); } if (m.is_bool(term)) { bool_var bv = ctx.mk_bool_var(term); @@ -738,7 +764,8 @@ expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& eqs) { else { result = e; } - m_rep.add_cache(e, expr_dep(result, deps)); + expr_dep edr(result, deps); + m_rep.add_cache(e, edr); eqs = m_dm.mk_join(eqs, deps); return result; } @@ -977,6 +1004,15 @@ expr* theory_seq::mk_sub(expr* a, expr* b) { return m_autil.mk_add(a, m_autil.mk_mul(m_autil.mk_int(-1), b)); } +enode* theory_seq::ensure_enode(expr* e) { + context& ctx = get_context(); + if (!ctx.e_internalized(e)) { + ctx.internalize(e, false); + ctx.mark_as_relevant(ctx.get_enode(e)); + } + return ctx.get_enode(e); +} + /* TBD: check semantics of extract. @@ -1043,7 +1079,7 @@ void theory_seq::add_at_axiom(expr* e) { literal theory_seq::mk_literal(expr* _e) { expr_ref e(_e, m); context& ctx = get_context(); - ctx.internalize(e, false); + ensure_enode(e); return ctx.get_literal(e); } @@ -1059,10 +1095,14 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) { } -expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2, expr* e3) { +expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, + expr* e2, expr* e3, sort* range) { expr* es[3] = { e1, e2, e3 }; unsigned len = e3?3:(e2?2:1); - return expr_ref(m_util.mk_skolem(name, len, es, m.get_sort(e1)), m); + if (!range) { + range = m.get_sort(e1); + } + return expr_ref(m_util.mk_skolem(name, len, es, range), m); } void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) { @@ -1071,10 +1111,9 @@ void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) { tout << mk_pp(ctx.bool_var2enode(v)->get_owner(), m) << " => " << 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); + enode* n1 = ensure_enode(e1); + enode* n2 = ensure_enode(e2); literal lit(v); justification* js = ctx.mk_justification( @@ -1110,10 +1149,6 @@ void theory_seq::assign_eq(bool_var v, bool is_true) { else if (m_util.str.is_in_re(e, e1, e2)) { // TBD } - else if (m.is_eq(e, e1, e2)) { - new_eq_eh(ctx.get_enode(e1)->get_th_var(get_id()), - ctx.get_enode(e1)->get_th_var(get_id())); - } else { UNREACHABLE(); } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index ad500aac6..c25d2d7ff 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -165,6 +165,7 @@ namespace smt { bool split_variable(); // split a variable bool is_solved(); bool check_length_coherence(); + bool check_length_coherence_tbd(); bool check_ineq_coherence(); bool pre_process_eqs(bool simplify_or_solve); @@ -209,8 +210,9 @@ namespace smt { literal mk_literal(expr* n); void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal); expr* mk_sub(expr* a, expr* b); + enode* ensure_enode(expr* a); - expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0, expr* e3 = 0); + expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0, expr* e3 = 0, sort* range = 0); void set_incomplete(app* term); diff --git a/src/util/scoped_vector.h b/src/util/scoped_vector.h index ed75fd561..917ecf2ab 100644 --- a/src/util/scoped_vector.h +++ b/src/util/scoped_vector.h @@ -94,7 +94,8 @@ public: void pop_back() { SASSERT(m_size > 0); - if (m_size == m_elems.size() && m_size > m_elems_start) { + if (m_index[m_size-1] == m_elems.size()-1 && + m_elems.size() > m_elems_start) { m_elems.pop_back(); } --m_size;