From 895d03299692c28b3e344e2a30c75f62c04f5989 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 8 Dec 2015 10:33:09 -0800 Subject: [PATCH] seq Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 8 ++ src/ast/rewriter/seq_rewriter.cpp | 164 ++++++++++++++++++++++++++++++ src/ast/rewriter/seq_rewriter.h | 6 +- src/ast/rewriter/th_rewriter.cpp | 2 + src/ast/seq_decl_plugin.h | 24 +++-- src/smt/theory_seq.cpp | 72 ++++++++----- src/smt/theory_seq.h | 4 + 7 files changed, 242 insertions(+), 38 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 8db78f827..7cc6d12cc 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -65,6 +65,7 @@ IS_WINDOWS=False IS_LINUX=False IS_OSX=False IS_FREEBSD=False +IS_OPENBSD=False VERBOSE=True DEBUG_MODE=False SHOW_CPPS = True @@ -126,6 +127,9 @@ def is_linux(): def is_freebsd(): return IS_FREEBSD +def is_openbsd(): + return IS_OPENBSD + def is_osx(): return IS_OSX @@ -582,6 +586,8 @@ elif os.name == 'posix': IS_LINUX=True elif os.uname()[0] == 'FreeBSD': IS_FREEBSD=True + elif os.uname()[0] == 'OpenBSD': + IS_OPENBSD=True def display_help(exit_code): print("mk_make.py: Z3 Makefile generator\n") @@ -1596,6 +1602,8 @@ class JavaDLLComponent(Component): t = t.replace('PLATFORM', 'linux') elif IS_FREEBSD: t = t.replace('PLATFORM', 'freebsd') + elif IS_OPENBSD: + t = t.replace('PLATFORM', 'openbsd') else: t = t.replace('PLATFORM', 'win32') out.write(t) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index d0e360d21..ef73bd2f2 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -510,3 +510,167 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) { br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) { return BR_FAILED; } + +br_status seq_rewriter::mk_eq_core(expr * l, expr * r, expr_ref & result) { + expr_ref_vector lhs(m()), rhs(m()), res(m()); + if (!reduce_eq(l, r, lhs, rhs)) { + result = m().mk_false(); + return BR_DONE; + } + if (lhs.size() == 1 && lhs[0].get() == l && rhs[0].get() == r) { + return BR_FAILED; + } + for (unsigned i = 0; i < lhs.size(); ++i) { + res.push_back(m().mk_eq(lhs[i].get(), rhs[i].get())); + } + result = mk_and(res); + return BR_REWRITE3; +} + +bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs) { + expr* a, *b; + bool change = false; + expr_ref_vector trail(m()); + m_lhs.reset(); + m_rhs.reset(); + m_util.str.get_concat(l, m_lhs); + m_util.str.get_concat(r, m_rhs); + + // solve from back + while (!m_lhs.empty() && !m_rhs.empty()) { + if (m_lhs.back() == m_rhs.back()) { + m_lhs.pop_back(); + m_rhs.pop_back(); + } + else if(m_util.str.is_unit(m_lhs.back(), a) && + m_util.str.is_unit(m_rhs.back(), b)) { + lhs.push_back(a); + rhs.push_back(b); + m_lhs.pop_back(); + m_rhs.pop_back(); + } + else if (!m_rhs.empty() && m_util.str.is_empty(m_rhs.back())) { + m_rhs.pop_back(); + } + else if (!m_lhs.empty() && m_util.str.is_empty(m_lhs.back())) { + m_lhs.pop_back(); + } + else { + break; + } + change = true; + } + + // solve from front + unsigned head1 = 0, head2 = 0; + while (head1 < m_lhs.size() && head2 < m_rhs.size()) { + if (m_lhs[head1] == m_rhs[head2]) { + ++head1; + ++head2; + } + else if(m_util.str.is_unit(m_lhs[head1], a) && + m_util.str.is_unit(m_rhs[head2], b)) { + lhs.push_back(a); + rhs.push_back(b); + ++head1; + ++head2; + } + else if (head1 < m_lhs.size() && m_util.str.is_empty(m_lhs[head1])) { + ++head1; + } + else if (head2 < m_rhs.size() && m_util.str.is_empty(m_rhs[head2])) { + ++head2; + } + else { + break; + } + change = true; + } + // reduce strings + std::string s1, s2; + if (head1 < m_lhs.size() && + head2 < m_rhs.size() && + m_util.str.is_string(m_lhs[head1], s1) && + m_util.str.is_string(m_rhs[head2], s2)) { + size_t l = std::min(s1.length(), s2.length()); + for (size_t i = 0; i < l; ++i) { + if (s1[i] != s2[i]) { + return false; + } + } + if (l == s1.length()) { + ++head1; + } + else { + m_lhs[head1] = m_util.str.mk_string(std::string(s1.c_str()+l,s1.length()-l)); + trail.push_back(m_lhs[head1]); + } + if (l == s2.length()) { + ++head2; + } + else { + m_rhs[head2] = m_util.str.mk_string(std::string(s2.c_str()+l,s2.length()-l)); + trail.push_back(m_rhs[head2]); + } + change = true; + } + if (head1 < m_lhs.size() && + head2 < m_rhs.size() && + m_util.str.is_string(m_lhs.back(), s1) && + m_util.str.is_string(m_rhs.back(), s2)) { + size_t l = std::min(s1.length(), s2.length()); + for (size_t i = 0; i < l; ++i) { + if (s1[s1.length()-i-1] != s2[s2.length()-i-1]) { + return false; + } + } + m_lhs.pop_back(); + m_rhs.pop_back(); + if (l < s1.length()) { + m_lhs.push_back(m_util.str.mk_string(std::string(s1.c_str(),s1.length()-l))); + trail.push_back(m_lhs.back()); + } + if (l < s2.length()) { + m_rhs.push_back(m_util.str.mk_string(std::string(s2.c_str(),s2.length()-l))); + trail.push_back(m_rhs.back()); + } + change = true; + } + if (!change) { + lhs.push_back(l); + rhs.push_back(r); + } + else if (head1 == m_lhs.size() && head2 == m_rhs.size()) { + // skip + } + else if (head1 == m_lhs.size()) { + return set_empty(m_rhs.size() - head2, m_rhs.c_ptr() + head2, lhs, rhs); + } + else if (head2 == m_rhs.size()) { + return set_empty(m_lhs.size() - head1, m_lhs.c_ptr() + head1, lhs, rhs); + } + else { // head1 < m_lhs.size() && head2 < m_rhs.size() // could solve if either side is fixed size. + lhs.push_back(m_util.str.mk_concat(m_lhs.size() - head1, m_lhs.c_ptr() + head1)); + rhs.push_back(m_util.str.mk_concat(m_rhs.size() - head2, m_rhs.c_ptr() + head2)); + } + return true; +} + +bool seq_rewriter::set_empty(unsigned sz, expr* const* es, expr_ref_vector& lhs, expr_ref_vector& rhs) { + std::string s; + for (unsigned i = 0; i < sz; ++i) { + if (m_util.str.is_unit(es[i])) { + return false; + } + if (m_util.str.is_empty(es[i])) { + continue; + } + if (m_util.str.is_string(es[i], s)) { + SASSERT(s.length() > 0); + return false; + } + lhs.push_back(m_util.str.mk_empty(m().get_sort(es[i]))); + rhs.push_back(es[i]); + } + return true; +} diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 4674a7535..57926efdf 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -32,7 +32,7 @@ Notes: class seq_rewriter { seq_util m_util; arith_util m_autil; - ptr_vector m_es; + ptr_vector m_es, m_lhs, m_rhs; br_status mk_seq_concat(expr* a, expr* b, expr_ref& result); br_status mk_str_length(expr* a, expr_ref& result); @@ -53,6 +53,7 @@ class seq_rewriter { br_status mk_re_plus(expr* a, expr_ref& result); br_status mk_re_opt(expr* a, expr_ref& result); + bool set_empty(unsigned sz, expr* const* es, expr_ref_vector& lhs, expr_ref_vector& rhs); public: seq_rewriter(ast_manager & m, params_ref const & p = params_ref()): m_util(m), m_autil(m) { @@ -64,6 +65,9 @@ public: static void get_param_descrs(param_descrs & r) {} br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); + br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); + + bool reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_vector& rhs); }; diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index a8aea47b6..aa1b35b89 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -177,6 +177,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg { st = m_f_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_ar_rw.get_fid()) st = m_ar_rw.mk_eq_core(args[0], args[1], result); + else if (s_fid == m_seq_rw.get_fid()) + st = m_seq_rw.mk_eq_core(args[0], args[1], result); if (st != BR_FAILED) return st; diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index feb3a279a..c317f8236 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -189,18 +189,19 @@ public: bool is_empty(expr const* n) const { symbol s; return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0); } - bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); } - bool is_length(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_LENGTH); } + bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); } + bool is_length(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_LENGTH); } bool is_extract(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_EXTRACT); } - bool is_contains(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONTAINS); } - bool is_at(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_AT); } - bool is_stridof(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STRIDOF); } - bool is_repl(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STRREPL); } - bool is_prefix(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_PREFIX); } - bool is_suffix(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_SUFFIX); } - bool is_itos(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_ITOS); } - bool is_stoi(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STOI); } - bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); } + bool is_contains(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONTAINS); } + bool is_at(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_AT); } + bool is_stridof(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STRIDOF); } + bool is_repl(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STRREPL); } + bool is_prefix(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_PREFIX); } + bool is_suffix(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_SUFFIX); } + bool is_itos(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_ITOS); } + bool is_stoi(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STOI); } + bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); } + bool is_unit(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_UNIT); } MATCH_BINARY(is_concat); @@ -215,6 +216,7 @@ public: MATCH_UNARY(is_itos); MATCH_UNARY(is_stoi); MATCH_BINARY(is_in_re); + MATCH_UNARY(is_unit); void get_concat(expr* e, ptr_vector& es) const; expr* get_leftmost_concat(expr* e) const { expr* e1, *e2; while (is_concat(e, e1, e2)) e = e1; return e; } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index fa3ddfb23..fd79aa46e 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -21,11 +21,13 @@ Revision History: #include "smt_context.h" #include "smt_model_generator.h" #include "theory_seq.h" +#include "seq_rewriter.h" using namespace smt; theory_seq::theory_seq(ast_manager& m): theory(m.mk_family_id("seq")), + m(m), m_rep(m), m_eqs_head(0), m_ineqs(m), @@ -43,7 +45,6 @@ theory_seq::theory_seq(ast_manager& m): final_check_status theory_seq::final_check_eh() { context & ctx = get_context(); - ast_manager& m = get_manager(); final_check_status st = check_ineqs(); if (st == FC_CONTINUE) { return FC_CONTINUE; @@ -53,7 +54,6 @@ final_check_status theory_seq::final_check_eh() { final_check_status theory_seq::check_ineqs() { context & ctx = get_context(); - ast_manager& m = get_manager(); enode_pair_vector eqs; for (unsigned i = 0; i < m_ineqs.size(); ++i) { expr_ref a(m_ineqs[i].get(), m); @@ -75,27 +75,58 @@ final_check_status theory_seq::check_ineqs() { bool theory_seq::simplify_eqs() { context & ctx = get_context(); - ast_manager& m = get_manager(); bool simplified = false; expr_array& lhs = m_lhs.back(); expr_array& rhs = m_rhs.back(); - for (unsigned i = m_eqs_head; i < m.size(lhs); ++i) { - expr* l = m.get(lhs, i); - expr* r = m.get(rhs, i); -#if 0 - if (reduce(l, r)) { - ++m_eq_head; + for (unsigned i = 0; !ctx.inconsistent() && i < m.size(lhs); ++i) { + if (simplify_eq(m.get(lhs, i), m.get(rhs, i), m_deps)) { + if (i + 1 != m.size(lhs)) { + m.set(lhs, i, m.get(lhs, m.size(lhs)-1)); + m.set(rhs, i, m.get(rhs, m.size(rhs)-1)); + --i; + simplified = true; + } + m.pop_back(lhs); + m.pop_back(rhs); } - else { - // equality is not simplified - // move forward pointer - } -#endif - } return simplified; } +bool theory_seq::simplify_eq(expr* l, expr* r, enode_pair_vector& deps) { + context& ctx = get_context(); + seq_rewriter rw(m); + expr_ref_vector lhs(m), rhs(m); + SASSERT(ctx.e_internalized(l)); + SASSERT(ctx.e_internalized(r)); + expr_ref lh = canonize(l, deps); + expr_ref rh = canonize(r, deps); + if (!rw.reduce_eq(l, r, lhs, rhs)) { + // equality is inconsistent. + // create conflict assignment. + expr_ref a(m); + a = m.mk_eq(l, r); + literal lit(ctx.get_literal(a)); + ctx.assign( + ~lit, + ctx.mk_justification( + ext_theory_propagation_justification( + get_id(), ctx.get_region(), 0, 0, deps.size(), deps.c_ptr(), ~lit))); + return true; + } + if (lhs.size() == 1 && l == lhs[0].get() && + rhs.size() == 1 && r == rhs[0].get()) { + return false; + } + SASSERT(lhs.size() == rhs.size()); + for (unsigned i = 0; i < lhs.size(); ++i) { + m.push_back(m_lhs.back(), lhs[i].get()); + m.push_back(m_rhs.back(), rhs[i].get()); + // TBD m_deps.push_back(deps); + } + return true; +} + final_check_status theory_seq::add_axioms() { for (unsigned i = 0; i < get_num_vars(); ++i) { @@ -111,7 +142,6 @@ bool theory_seq::internalize_atom(app* a, bool) { bool theory_seq::internalize_term(app* term) { m_used = true; context & ctx = get_context(); - ast_manager& m = get_manager(); unsigned num_args = term->get_num_args(); for (unsigned i = 0; i < num_args; i++) { ctx.internalize(term->get_arg(i), false); @@ -154,7 +184,6 @@ expr_ref theory_seq::canonize(expr* e, enode_pair_vector& eqs) { expr_ref theory_seq::expand(expr* e, enode_pair_vector& eqs) { context& ctx = get_context(); - ast_manager& m = get_manager(); expr* e1, *e2; SASSERT(ctx.e_internalized(e)); enode* n = ctx.get_enode(e); @@ -200,7 +229,6 @@ expr_ref theory_seq::expand(expr* e, enode_pair_vector& eqs) { void theory_seq::propagate() { context & ctx = get_context(); - ast_manager& m = get_manager(); while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) { expr_ref e(m); e = m_axioms[m_axioms_head].get(); @@ -216,7 +244,6 @@ void theory_seq::create_axiom(expr_ref& e) { void theory_seq::assert_axiom(expr_ref& e) { context & ctx = get_context(); - ast_manager& m = get_manager(); if (m.is_true(e)) return; TRACE("seq", tout << "asserting " << e << "\n";); ctx.internalize(e, false); @@ -227,7 +254,6 @@ void theory_seq::assert_axiom(expr_ref& e) { } expr_ref theory_seq::mk_skolem(char const* name, expr* e1, expr* e2) { - ast_manager& m = get_manager(); expr_ref result(m); sort* s = m.get_sort(e1); SASSERT(s == m.get_sort(e2)); @@ -249,7 +275,6 @@ void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) { void theory_seq::assign_eq(bool_var v, bool is_true) { context & ctx = get_context(); - ast_manager& m = get_manager(); enode* n = ctx.bool_var2enode(v); app* e = n->get_owner(); @@ -286,7 +311,6 @@ void theory_seq::assign_eq(bool_var v, bool is_true) { } void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { - ast_manager& m = get_manager(); m_find.merge(v1, v2); expr_ref e1(m), e2(m); e1 = get_enode(v1)->get_owner(); @@ -296,7 +320,6 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { } void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { - ast_manager& m = get_manager(); expr* e1 = get_enode(v1)->get_owner(); expr* e2 = get_enode(v2)->get_owner(); m_trail_stack.push(push_back_vector(m_ineqs)); @@ -304,7 +327,6 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { } void theory_seq::push_scope_eh() { - ast_manager& m = get_manager(); theory::push_scope_eh(); m_trail_stack.push_scope(); m_trail_stack.push(value_trail(m_axioms_head)); @@ -317,7 +339,6 @@ void theory_seq::push_scope_eh() { } void theory_seq::pop_scope_eh(unsigned num_scopes) { - ast_manager& m = get_manager(); m_trail_stack.pop_scope(num_scopes); theory::pop_scope_eh(num_scopes); m_rep.resize(get_num_vars()); @@ -335,7 +356,6 @@ void theory_seq::restart_eh() { } void theory_seq::relevant_eh(app* n) { - ast_manager& m = get_manager(); if (m_util.str.is_length(n)) { expr_ref e(m); e = m_autil.mk_le(m_autil.mk_numeral(rational(0), true), n); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 9b6258a2c..3a7b978e9 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -35,9 +35,12 @@ namespace smt { void reset() { memset(this, 0, sizeof(stats)); } unsigned m_num_splits; }; + ast_manager& m; expr_ref_vector m_rep; // unification representative. vector m_lhs, m_rhs; // persistent sets of equalities. unsigned m_eqs_head; // index of unprocessed equation. + enode_pair_vector m_deps; // TBD - convert to dependency structure. + expr_ref_vector m_ineqs; // inequalities to check expr_ref_vector m_axioms; @@ -68,6 +71,7 @@ namespace smt { final_check_status check_ineqs(); bool simplify_eqs(); + bool simplify_eq(expr* l, expr* r, enode_pair_vector& deps); final_check_status add_axioms(); void assert_axiom(expr_ref& e);