diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 7e96f3b52..888fb8553 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1346,16 +1346,16 @@ class PythonInstallComponent(Component): Component.__init__(self, name, None, []) def main_component(self): - return is_python_install_enabled() + return False def install_deps(self, out): - if not self.main_component(): - return + if not is_python_install_enabled(): + return pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) MakeRuleCmd.make_install_directory(out, pythonPkgDirWithoutPrefix) def mk_install(self, out): - if not self.main_component(): + if not is_python_install_enabled(): return MakeRuleCmd.install_files(out, 'z3*.py', pythonPkgDirWithoutPrefix) if sys.version >= "3": @@ -1374,7 +1374,7 @@ class PythonInstallComponent(Component): out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR) def mk_uninstall(self, out): - if not self.main_component(): + if not is_python_install_enabled(): return pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) MakeRuleCmd.remove_installed_files(out, '{}*.py'.format(os.path.join(pythonPkgDirWithoutPrefix, 'z3'))) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 290f27ac5..d31d15a1b 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -441,8 +441,9 @@ extern "C" { LOG_Z3_mk_fpa_max(c, t1, t2); RESET_ERROR_CODE(); api::context * ctx = mk_c(c); - Z3_ast r = of_ast(ctx->fpautil().mk_max(to_expr(t1), to_expr(t2))); - RETURN_Z3(r); + expr * a = ctx->fpautil().mk_max(to_expr(t1), to_expr(t2)); + ctx->save_ast_trail(a); + RETURN_Z3(of_expr(a)); Z3_CATCH_RETURN(0); } diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index ca48a72bf..5f6fd8dbd 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -813,16 +813,26 @@ end = struct let s = Z3native.get_sort (context_gno ctx) no in let sk = (sort_kind_of_int (Z3native.get_sort_kind (context_gno ctx) s)) in if (Z3native.is_algebraic_number (context_gno ctx) no) then - Expr(z3_native_object_of_ast_ptr ctx no) + Expr(z3_native_object_of_ast_ptr ctx no) else - if (Z3native.is_numeral_ast (context_gno ctx) no) then - if (sk == INT_SORT || sk == REAL_SORT || sk == BV_SORT || - sk == FLOATING_POINT_SORT || sk == ROUNDING_MODE_SORT) then - Expr(z3_native_object_of_ast_ptr ctx no) - else - raise (Z3native.Exception "Unsupported numeral object") - else - Expr(z3_native_object_of_ast_ptr ctx no) + if (Z3native.is_numeral_ast (context_gno ctx) no) then + match sk with + | REAL_SORT + | BOOL_SORT + | ARRAY_SORT + | BV_SORT + | ROUNDING_MODE_SORT + | RELATION_SORT + | UNINTERPRETED_SORT + | FLOATING_POINT_SORT + | INT_SORT + | DATATYPE_SORT + | FINITE_DOMAIN_SORT -> + Expr(z3_native_object_of_ast_ptr ctx no) + | _ -> + raise (Z3native.Exception "Unsupported numeral object") + else + Expr(z3_native_object_of_ast_ptr ctx no) let expr_of_ast a = let q = (Z3enums.ast_kind_of_int (Z3native.get_ast_kind (z3obj_gnc a) (z3obj_gno a))) in diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h index c0a294c8b..c59428d9e 100644 --- a/src/api/z3_optimization.h +++ b/src/api/z3_optimization.h @@ -43,14 +43,14 @@ extern "C" { def_API('Z3_optimize_inc_ref', VOID, (_in(CONTEXT), _in(OPTIMIZE))) */ - void Z3_API Z3_optimize_inc_ref(Z3_context c,Z3_optimize d); + void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize d); /** \brief Decrement the reference counter of the given optimize context. def_API('Z3_optimize_dec_ref', VOID, (_in(CONTEXT), _in(OPTIMIZE))) */ - void Z3_API Z3_optimize_dec_ref(Z3_context c,Z3_optimize d); + void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize d); /** \brief Assert hard constraint to the optimization context. @@ -102,7 +102,7 @@ extern "C" { def_API('Z3_optimize_push', VOID, (_in(CONTEXT), _in(OPTIMIZE))) */ - void Z3_API Z3_optimize_push(Z3_context c,Z3_optimize d); + void Z3_API Z3_optimize_push(Z3_context c, Z3_optimize d); /** \brief Backtrack one level. @@ -113,7 +113,7 @@ extern "C" { def_API('Z3_optimize_pop', VOID, (_in(CONTEXT), _in(OPTIMIZE))) */ - void Z3_API Z3_optimize_pop(Z3_context c,Z3_optimize d); + void Z3_API Z3_optimize_pop(Z3_context c, Z3_optimize d); /** \brief Check consistency and produce optimal values. @@ -132,7 +132,7 @@ extern "C" { def_API('Z3_optimize_get_reason_unknown', STRING, (_in(CONTEXT), _in(OPTIMIZE) )) */ - Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c,Z3_optimize d); + Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize d); /** \brief Retrieve the model for the last #Z3_optimize_check @@ -195,9 +195,7 @@ extern "C" { def_API('Z3_optimize_to_string', STRING, (_in(CONTEXT), _in(OPTIMIZE))) */ - Z3_string Z3_API Z3_optimize_to_string( - Z3_context c, - Z3_optimize o); + Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o); /** @@ -212,7 +210,7 @@ extern "C" { def_API('Z3_optimize_get_statistics', STATS, (_in(CONTEXT), _in(OPTIMIZE))) */ - Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c,Z3_optimize d); + Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d); /*@}*/ /*@}*/ diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index f46201ec7..d0e360d21 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -20,6 +20,7 @@ Notes: #include"seq_rewriter.h" #include"arith_decl_plugin.h" #include"ast_pp.h" +#include"ast_util.h" br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { @@ -187,6 +188,21 @@ br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) { result = m().mk_bool_val(0 != strstr(d.c_str(), c.c_str())); return BR_DONE; } + // check if subsequence of a is in b. + ptr_vector as, bs; + m_util.str.get_concat(a, as); + m_util.str.get_concat(b, bs); + bool found = false; + for (unsigned i = 0; !found && i < bs.size(); ++i) { + if (as.size() > bs.size() - i) break; + unsigned j = 0; + for (; j < as.size() && as[j] == bs[i+j]; ++j) {}; + found = j == as.size(); + } + if (found) { + result = m().mk_true(); + return BR_DONE; + } return BR_FAILED; } @@ -261,6 +277,7 @@ br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& resu } br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { + TRACE("seq", tout << mk_pp(a, m()) << " " << mk_pp(b, m()) << "\n";); std::string s1, s2; bool isc1 = m_util.str.is_string(a, s1); bool isc2 = m_util.str.is_string(b, s2); @@ -276,24 +293,177 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { result = m().mk_true(); return BR_DONE; } + expr* a1 = m_util.str.get_leftmost_concat(a); + expr* b1 = m_util.str.get_leftmost_concat(b); + isc1 = m_util.str.is_string(a1, s1); + isc2 = m_util.str.is_string(b1, s2); + ptr_vector as, bs; + + if (a1 != b1 && isc1 && isc2) { + if (s1.length() <= s2.length()) { + if (strncmp(s1.c_str(), s2.c_str(), s1.length()) == 0) { + if (a == a1) { + result = m().mk_true(); + return BR_DONE; + } + 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()); + 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())); + return BR_REWRITE_FULL; + } + else { + result = m().mk_false(); + return BR_DONE; + } + } + else { + if (strncmp(s1.c_str(), s2.c_str(), s2.length()) == 0) { + if (b == b1) { + result = m().mk_false(); + return BR_DONE; + } + 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()); + 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)); + return BR_REWRITE_FULL; + } + else { + result = m().mk_false(); + return BR_DONE; + } + } + } + if (a1 != b1) { + return BR_FAILED; + } + m_util.str.get_concat(a, as); + m_util.str.get_concat(b, bs); + unsigned i = 0; + for (; i < as.size() && i < bs.size() && as[i] == bs[i]; ++i) {}; + if (i == as.size()) { + result = m().mk_true(); + return BR_DONE; + } + if (i == bs.size()) { + expr_ref_vector es(m()); + for (unsigned j = i; j < as.size(); ++j) { + es.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j])); + } + result = mk_and(es); + return BR_REWRITE3; + } + if (i > 0) { + a = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i); + b = m_util.str.mk_concat(bs.size() - i, bs.c_ptr() + i); + result = m_util.str.mk_prefix(a, b); + return BR_DONE; + } + UNREACHABLE(); return BR_FAILED; } br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) { - std::string s1, s2; - bool isc1 = m_util.str.is_string(a, s1); - if (isc1 && m_util.str.is_string(b, s2)) { - bool suffix = s1.length() <= s2.length(); - for (unsigned i = 0; i < s1.length() && suffix; ++i) { - suffix = s1[s1.length() - i - 1] == s2[s2.length() - i - 1]; - } - result = m().mk_bool_val(suffix); + if (a == b) { + result = m().mk_true(); return BR_DONE; } + std::string s1, s2; if (m_util.str.is_empty(a)) { result = m().mk_true(); return BR_DONE; } + if (m_util.str.is_empty(b)) { + result = m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), a); + return BR_REWRITE3; + } + // concatenation is left-associative, so a2, b2 are not concatenations + expr* a1, *a2, *b1, *b2; + if (m_util.str.is_concat(a, a1, a2) && + m_util.str.is_concat(b, b1, b2) && a2 == b2) { + result = m_util.str.mk_suffix(a1, b1); + return BR_REWRITE1; + } + if (m_util.str.is_concat(b, b1, b2) && b2 == a) { + result = m().mk_true(); + return BR_DONE; + } + bool isc1 = false; + bool isc2 = false; + + if (m_util.str.is_concat(a, a1, a2) && m_util.str.is_string(a2, s1)) { + isc1 = true; + } + else if (m_util.str.is_string(a, s1)) { + isc1 = true; + a2 = a; + a1 = 0; + } + + if (m_util.str.is_concat(b, b1, b2) && m_util.str.is_string(b2, s2)) { + isc2 = true; + } + else if (m_util.str.is_string(b, s2)) { + isc2 = true; + b2 = b; + b1 = 0; + } + if (isc1 && isc2) { + if (s1.length() == s2.length()) { + SASSERT(s1 != s2); + result = m().mk_false(); + return BR_DONE; + } + else if (s1.length() < s2.length()) { + bool suffix = true; + for (unsigned i = 0; i < s1.length(); ++i) { + suffix = s1[s1.length()-i-1] == s2[s2.length()-i-1]; + } + if (suffix && a1 == 0) { + result = m().mk_true(); + return BR_DONE; + } + else if (suffix) { + s2 = std::string(s2.c_str(), s2.length()-s1.length()); + b2 = m_util.str.mk_string(s2); + result = m_util.str.mk_suffix(a1, b1?m_util.str.mk_concat(b1, b2):b2); + return BR_DONE; + } + else { + result = m().mk_false(); + return BR_DONE; + } + } + else { + SASSERT(s1.length() > s2.length()); + if (b1 == 0) { + result = m().mk_false(); + return BR_DONE; + } + bool suffix = true; + for (unsigned i = 0; i < s2.length(); ++i) { + suffix = s1[s1.length()-i-1] == s2[s2.length()-i-1]; + } + if (suffix) { + s1 = std::string(s1.c_str(), s1.length()-s2.length()); + a2 = m_util.str.mk_string(s1); + result = m_util.str.mk_suffix(a1?m_util.str.mk_concat(a1, a2):a2, b1); + return BR_DONE; + } + else { + result = m().mk_false(); + return BR_DONE; + } + } + } + return BR_FAILED; } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index bdbf033d6..67812a369 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -288,9 +288,15 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, ast_manager& m = *m_manager; sort_ref rng(m); switch(k) { - case OP_SEQ_UNIT: case OP_SEQ_EMPTY: + match(*m_sigs[k], arity, domain, range, rng); + if (rng == m_string) { + parameter param(symbol("")); + return mk_func_decl(OP_STRING_CONST, 1, ¶m, 0, 0, m_string); + } + return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); + case OP_SEQ_UNIT: case OP_RE_PLUS: case OP_RE_STAR: case OP_RE_OPTION: diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index dc7c4634b..feb3a279a 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -163,13 +163,19 @@ public: 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(symbol const& 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); } + expr* mk_concat(unsigned n, expr* const* es) { if (n == 1) return es[0]; SASSERT(n > 1); return m.mk_app(m_fid, OP_SEQ_CONCAT, n, es); } app* mk_length(expr* a) { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); } app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_SEQ_EXTRACT, 3, es); } - app* mk_strctn(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); } + app* mk_contains(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); } + app* mk_prefix(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_PREFIX, 2, es); } + app* mk_suffix(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_SUFFIX, 2, es); } + bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); } @@ -180,7 +186,9 @@ public: return is_string(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true); } - 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() && strcmp(s.bare_str(),"") == 0); } + bool is_empty(expr const* n) const { symbol s; + return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0); + } bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); } bool is_length(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_LENGTH); } bool is_extract(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_EXTRACT); } @@ -209,6 +217,7 @@ public: MATCH_BINARY(is_in_re); void get_concat(expr* e, ptr_vector& es) const; + expr* get_leftmost_concat(expr* e) const { expr* e1, *e2; while (is_concat(e, e1, e2)) e = e1; return e; } }; class re { diff --git a/src/smt/arith_eq_adapter.cpp b/src/smt/arith_eq_adapter.cpp index 74e3d573a..d160d3f4e 100644 --- a/src/smt/arith_eq_adapter.cpp +++ b/src/smt/arith_eq_adapter.cpp @@ -289,9 +289,9 @@ namespace smt { void arith_eq_adapter::restart_eh() { context & ctx = get_context(); TRACE("arith_eq_adapter", tout << "restart\n";); - svector tmp(m_restart_pairs); - svector::iterator it = tmp.begin(); - svector::iterator end = tmp.end(); + enode_pair_vector tmp(m_restart_pairs); + enode_pair_vector::iterator it = tmp.begin(); + enode_pair_vector::iterator end = tmp.end(); m_restart_pairs.reset(); for (; it != end && !ctx.inconsistent(); ++it) { TRACE("arith_eq_adapter", tout << "creating arith_eq_adapter axioms at the base level #" << it->first->get_owner_id() << " #" << diff --git a/src/smt/arith_eq_adapter.h b/src/smt/arith_eq_adapter.h index ffbd15c26..01bea154f 100644 --- a/src/smt/arith_eq_adapter.h +++ b/src/smt/arith_eq_adapter.h @@ -68,7 +68,7 @@ namespace smt { arith_simplifier_plugin * m_as; already_processed m_already_processed; - svector m_restart_pairs; + enode_pair_vector m_restart_pairs; svector m_proof_hint; context & get_context() const { return m_owner.get_context(); } diff --git a/src/smt/smt_types.h b/src/smt/smt_types.h index 6c5ba6313..7f2076045 100644 --- a/src/smt/smt_types.h +++ b/src/smt/smt_types.h @@ -45,6 +45,7 @@ namespace smt { class enode; typedef ptr_vector enode_vector; typedef std::pair enode_pair; + typedef svector enode_pair_vector; class context; diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 29e4438c4..4526b283a 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -712,7 +712,7 @@ namespace smt { } } - void theory_array_base::propagate_select_to_store_parents(enode * r, enode * sel, svector & todo) { + void theory_array_base::propagate_select_to_store_parents(enode * r, enode * sel, enode_pair_vector & todo) { SASSERT(r->get_root() == r); SASSERT(is_select(sel)); if (!get_context().is_relevant(r)) { @@ -751,7 +751,7 @@ namespace smt { } } - void theory_array_base::propagate_selects_to_store_parents(enode * r, svector & todo) { + void theory_array_base::propagate_selects_to_store_parents(enode * r, enode_pair_vector & todo) { select_set * sel_set = get_select_set(r); select_set::iterator it2 = sel_set->begin(); select_set::iterator end2 = sel_set->end(); @@ -763,9 +763,9 @@ namespace smt { } void theory_array_base::propagate_selects() { - svector todo; - ptr_vector::const_iterator it = m_selects_domain.begin(); - ptr_vector::const_iterator end = m_selects_domain.end(); + enode_pair_vector todo; + enode_vector::const_iterator it = m_selects_domain.begin(); + enode_vector::const_iterator end = m_selects_domain.end(); for (; it != end; ++it) { enode * r = *it; propagate_selects_to_store_parents(r, todo); diff --git a/src/smt/theory_array_base.h b/src/smt/theory_array_base.h index 46cd60fd6..e0d16f0f2 100644 --- a/src/smt/theory_array_base.h +++ b/src/smt/theory_array_base.h @@ -58,8 +58,8 @@ namespace smt { unsigned get_dimension(sort* s) const; ptr_vector m_axiom1_todo; - svector > m_axiom2_todo; - svector > m_extensionality_todo; + enode_pair_vector m_axiom2_todo; + enode_pair_vector m_extensionality_todo; void assert_axiom(unsigned num_lits, literal * lits); void assert_axiom(literal l1, literal l2); @@ -181,8 +181,8 @@ namespace smt { bool is_unspecified_default_ok() const; void collect_defaults(); void collect_selects(); - void propagate_select_to_store_parents(enode * r, enode * sel, svector & todo); - void propagate_selects_to_store_parents(enode * r, svector & todo); + void propagate_select_to_store_parents(enode * r, enode * sel, enode_pair_vector & todo); + void propagate_selects_to_store_parents(enode * r, enode_pair_vector & todo); void propagate_selects(); select_set * get_select_set(enode * n); virtual void finalize_model(model_generator & m); diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index cf4658c7d..0c5e83928 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -438,8 +438,8 @@ namespace smt { ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), r, 0, 0, m_used_eqs.size(), m_used_eqs.c_ptr()))); TRACE("occurs_check", tout << "occurs_check: true\n"; - svector::const_iterator it = m_used_eqs.begin(); - svector::const_iterator end = m_used_eqs.end(); + enode_pair_vector::const_iterator it = m_used_eqs.begin(); + enode_pair_vector::const_iterator end = m_used_eqs.end(); for(; it != end; ++it) { enode_pair const & p = *it; tout << "eq: #" << p.first->get_owner_id() << " #" << p.second->get_owner_id() << "\n"; @@ -675,7 +675,7 @@ namespace smt { CTRACE("datatype", d->m_recognizers.empty(), ctx.display(tout);); SASSERT(!d->m_recognizers.empty()); literal_vector lits; - svector eqs; + enode_pair_vector eqs; ptr_vector::const_iterator it = d->m_recognizers.begin(); ptr_vector::const_iterator end = d->m_recognizers.end(); for (unsigned idx = 0; it != end; ++it, ++idx) { diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index 77b1ffc7c..8f47a3fc3 100644 --- a/src/smt/theory_datatype.h +++ b/src/smt/theory_datatype.h @@ -74,7 +74,7 @@ namespace smt { void sign_recognizer_conflict(enode * c, enode * r); ptr_vector m_to_unmark; - svector m_used_eqs; + enode_pair_vector m_used_eqs; enode * m_main; bool occurs_check(enode * n); bool occurs_check_core(enode * n); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp new file mode 100644 index 000000000..b3a143377 --- /dev/null +++ b/src/smt/theory_seq.cpp @@ -0,0 +1,306 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + theory_seq.h + +Abstract: + + Native theory solver for sequences. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-6-12 + +Revision History: + +--*/ + +#include "value_factory.h" +#include "smt_context.h" +#include "smt_model_generator.h" +#include "theory_seq.h" + +using namespace smt; + +theory_seq::theory_seq(ast_manager& m): + theory(m.mk_family_id("seq")), + m_axioms_head(0), + m_axioms(m), + m_ineqs(m), + m_used(false), + m_rewrite(m), + m_util(m), + m_autil(m), + m_trail_stack(*this), + m_find(*this) {} + +final_check_status theory_seq::final_check_eh() { + context & ctx = get_context(); + ast_manager& m = get_manager(); + final_check_status st = check_ineqs(); + if (st == FC_CONTINUE) { + return FC_CONTINUE; + } + return m_used?FC_GIVEUP:FC_DONE; +} + +final_check_status theory_seq::check_ineqs() { + context & ctx = get_context(); + ast_manager& m = get_manager(); + enode_pair_vector eqs; + for (unsigned i = 0; i < m_ineqs.size(); ++i) { + expr_ref a(m_ineqs[i].get(), m); + expr_ref b = canonize(a, eqs); + if (m.is_true(b)) { + ctx.internalize(a, false); + literal lit(ctx.get_literal(a)); + ctx.mark_as_relevant(lit); + ctx.assign( + lit, + ctx.mk_justification( + ext_theory_propagation_justification( + get_id(), ctx.get_region(), 0, 0, eqs.size(), eqs.c_ptr(), lit))); + return FC_CONTINUE; + } + } + return FC_DONE; +} + +final_check_status theory_seq::simplify_eqs() { + bool simplified = false; + for (unsigned i = 0; i < get_num_vars(); ++i) { + theory_var v = m_find.find(i); + if (v != i) continue; + + } + if (simplified) { + return FC_CONTINUE; + } + return FC_DONE; +} + +final_check_status theory_seq::add_axioms() { + for (unsigned i = 0; i < get_num_vars(); ++i) { + + // add axioms for len(x) when x = a ++ b + } + return FC_DONE; +} + +bool theory_seq::internalize_atom(app* a, bool) { + return internalize_term(a); +} + +bool theory_seq::internalize_term(app* term) { + m_used = true; + context & ctx = get_context(); + ast_manager& m = get_manager(); + unsigned num_args = term->get_num_args(); + for (unsigned i = 0; i < num_args; i++) { + ctx.internalize(term->get_arg(i), false); + } + if (ctx.e_internalized(term)) { + return true; + } + enode * e = ctx.mk_enode(term, false, m.is_bool(term), true); + if (m.is_bool(term)) { + bool_var bv = ctx.mk_bool_var(term); + ctx.set_var_theory(bv, get_id()); + ctx.set_enode_flag(bv, true); + } + else { + theory_var v = mk_var(e); + ctx.attach_th_var(e, this, v); + } + // assert basic axioms + if (!m_used) { m_trail_stack.push(value_trail(m_used)); m_used = true; } + return true; +} + +theory_var theory_seq::mk_var(enode* n) { + theory_var r = theory::mk_var(n); + VERIFY(r == m_find.mk_var()); + return r; +} + +bool theory_seq::can_propagate() { + return m_axioms_head < m_axioms.size(); +} + +expr_ref theory_seq::canonize(expr* e, enode_pair_vector& eqs) { + eqs.reset(); + expr_ref result = expand(e, eqs); + m_rewrite(result); + return result; +} + +expr_ref theory_seq::expand(expr* e, enode_pair_vector& eqs) { + context& ctx = get_context(); + ast_manager& m = get_manager(); + expr* e1, *e2; + SASSERT(ctx.e_internalized(e)); + enode* n = ctx.get_enode(e); + enode* start = n; + do { + e = n->get_owner(); + if (m_util.str.is_concat(e, e1, e2)) { + if (start != n) eqs.push_back(enode_pair(start, n)); + return expr_ref(m_util.str.mk_concat(expand(e1, eqs), expand(e2, eqs)), m); + } + if (m_util.str.is_empty(e) || m_util.str.is_string(e)) { + if (start != n) eqs.push_back(enode_pair(start, n)); + return expr_ref(e, m); + } + if (m.is_eq(e, e1, e2)) { + if (start != n) eqs.push_back(enode_pair(start, n)); + return expr_ref(m.mk_eq(expand(e1, eqs), expand(e2, eqs)), m); + } + if (m_util.str.is_prefix(e, e1, e2)) { + if (start != n) eqs.push_back(enode_pair(start, n)); + return expr_ref(m_util.str.mk_prefix(expand(e1, eqs), expand(e2, eqs)), m); + } + if (m_util.str.is_suffix(e, e1, e2)) { + if (start != n) eqs.push_back(enode_pair(start, n)); + return expr_ref(m_util.str.mk_suffix(expand(e1, eqs), expand(e2, eqs)), m); + } + if (m_util.str.is_contains(e, e1, e2)) { + if (start != n) eqs.push_back(enode_pair(start, n)); + return expr_ref(m_util.str.mk_contains(expand(e1, eqs), expand(e2, eqs)), m); + } +#if 0 + if (m_util.str.is_unit(e)) { + // TBD: canonize the element. + if (start != n) eqs.push_back(enode_pair(start, n)); + return expr_ref(e, m); + } +#endif + n = n->get_next(); + } + while (n != start); + return expr_ref(n->get_root()->get_owner(), m); +} + +void theory_seq::propagate() { + context & ctx = get_context(); + ast_manager& m = get_manager(); + while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) { + expr_ref e(m); + e = m_axioms[m_axioms_head].get(); + assert_axiom(e); + ++m_axioms_head; + } +} + +void theory_seq::create_axiom(expr_ref& e) { + m_trail_stack.push(push_back_vector(m_axioms)); + m_axioms.push_back(e); +} + +void theory_seq::assert_axiom(expr_ref& e) { + context & ctx = get_context(); + ast_manager& m = get_manager(); + if (m.is_true(e)) return; + TRACE("seq", tout << "asserting " << e << "\n";); + ctx.internalize(e, false); + literal lit(ctx.get_literal(e)); + ctx.mark_as_relevant(lit); + ctx.mk_th_axiom(get_id(), 1, &lit); + +} + +expr_ref theory_seq::mk_skolem(char const* name, expr* e1, expr* e2) { + ast_manager& m = get_manager(); + expr_ref result(m); + sort* s = m.get_sort(e1); + SASSERT(s == m.get_sort(e2)); + sort* ss[2] = { s, s }; + result = m.mk_app(m.mk_func_decl(symbol("#prefix_eq"), 2, ss, s), e1, e2); + return result; +} + +void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) { + context& ctx = get_context(); + ctx.internalize(e1, false); + enode* n1 = ctx.get_enode(e1); + enode* n2 = ctx.get_enode(e2); + literal lit(v); + ctx.assign_eq(n1, n2, eq_justification( + alloc(ext_theory_eq_propagation_justification, + get_id(), ctx.get_region(), 1, &lit, 0, 0, n1, n2))); +} + +void theory_seq::assign_eq(bool_var v, bool is_true) { + context & ctx = get_context(); + ast_manager& m = get_manager(); + + enode* n = ctx.bool_var2enode(v); + app* e = n->get_owner(); + if (is_true) { + expr* e1, *e2; + expr_ref f(m); + if (m_util.str.is_prefix(e, e1, e2)) { + f = mk_skolem("#prefix_eq", e1, e2); + f = m_util.str.mk_concat(e1, f); + propagate_eq(v, f, e2); + } + else if (m_util.str.is_suffix(e, e1, e2)) { + f = mk_skolem("#suffix_eq", e1, e2); + f = m_util.str.mk_concat(f, e1); + propagate_eq(v, f, e2); + } + else if (m_util.str.is_contains(e, e1, e2)) { + expr_ref f1 = mk_skolem("#contains_eq1", e1, e2); + expr_ref f2 = mk_skolem("#contains_eq2", e1, e2); + f = m_util.str.mk_concat(m_util.str.mk_concat(f1, e1), f2); + propagate_eq(v, f, e2); + } + else if (m_util.str.is_in_re(e, e1, e2)) { + NOT_IMPLEMENTED_YET(); + } + else { + UNREACHABLE(); + } + } + else { + m_trail_stack.push(push_back_vector(m_ineqs)); + m_ineqs.push_back(e); + } +} + +void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { + m_find.merge(v1, v2); +} + +void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { + ast_manager& m = get_manager(); + expr* e1 = get_enode(v1)->get_owner(); + expr* e2 = get_enode(v2)->get_owner(); + m_trail_stack.push(push_back_vector(m_ineqs)); + m_ineqs.push_back(m.mk_eq(e1, e2)); +} + +void theory_seq::push_scope_eh() { + theory::push_scope_eh(); + m_trail_stack.push_scope(); + m_trail_stack.push(value_trail(m_axioms_head)); +} + +void theory_seq::pop_scope_eh(unsigned num_scopes) { + m_trail_stack.pop_scope(num_scopes); + theory::pop_scope_eh(num_scopes); +} + +void theory_seq::restart_eh() { + +} + +void theory_seq::relevant_eh(app* n) { + ast_manager& m = get_manager(); + if (m_util.str.is_length(n)) { + expr_ref e(m); + e = m_autil.mk_le(m_autil.mk_numeral(rational(0), true), n); + create_axiom(e); + } +} diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h new file mode 100644 index 000000000..3232a8469 --- /dev/null +++ b/src/smt/theory_seq.h @@ -0,0 +1,91 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + theory_seq.h + +Abstract: + + Native theory solver for sequences. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-6-12 + +Revision History: + +--*/ +#ifndef THEORY_SEQ_H_ +#define THEORY_SEQ_H_ + +#include "smt_theory.h" +#include "seq_decl_plugin.h" +#include "theory_seq_empty.h" +#include "th_rewriter.h" +#include "union_find.h" + +namespace smt { + + class theory_seq : public theory { + typedef union_find th_union_find; + typedef trail_stack th_trail_stack; + struct stats { + stats() { reset(); } + void reset() { memset(this, 0, sizeof(stats)); } + unsigned m_num_splits; + }; + expr_ref_vector m_axioms; + expr_ref_vector m_ineqs; + unsigned m_axioms_head; + bool m_used; + th_rewriter m_rewrite; + seq_util m_util; + arith_util m_autil; + th_trail_stack m_trail_stack; + th_union_find m_find; + stats m_stats; + + virtual final_check_status final_check_eh(); + virtual bool internalize_atom(app*, bool); + virtual bool internalize_term(app*); + virtual void new_eq_eh(theory_var, theory_var); + virtual void new_diseq_eh(theory_var, theory_var); + virtual void assign_eq(bool_var v, bool is_true); + virtual bool can_propagate(); + virtual void propagate(); + virtual void push_scope_eh(); + virtual void pop_scope_eh(unsigned num_scopes); + virtual void restart_eh(); + virtual void relevant_eh(app* n); + virtual theory* mk_fresh(context* new_ctx) { return alloc(theory_seq, new_ctx->get_manager()); } + virtual char const * get_name() const { return "seq"; } + virtual theory_var mk_var(enode* n); + + final_check_status check_ineqs(); + final_check_status simplify_eqs(); + final_check_status add_axioms(); + + void assert_axiom(expr_ref& e); + void create_axiom(expr_ref& e); + expr_ref canonize(expr* e, enode_pair_vector& eqs); + expr_ref expand(expr* e, enode_pair_vector& eqs); + + void propagate_eq(bool_var v, expr* e1, expr* e2); + expr_ref mk_skolem(char const* name, expr* e1, expr* e2); + public: + theory_seq(ast_manager& m); + virtual void init_model(model_generator & mg) { + mg.register_factory(alloc(seq_factory, get_manager(), get_family_id(), mg.get_model())); + } + + th_trail_stack & get_trail_stack() { return m_trail_stack; } + virtual void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var); + static void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {} + void unmerge_eh(theory_var v1, theory_var v2); + + }; +}; + +#endif /* THEORY_SEQ_H_ */ +