From fe1039d12f807c5819ec36bd1e82578c4ed3d7bd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Dec 2015 14:48:50 -0800 Subject: [PATCH 01/10] seq Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 2 +- src/smt/theory_seq.cpp | 276 +++++++++++++++++++++++++++++----------- src/smt/theory_seq.h | 54 ++++++-- 3 files changed, 248 insertions(+), 84 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 39ccbdbb2..00971f794 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -821,7 +821,7 @@ namespace smt { theory_var v2 = m_fparams.m_new_core2th_eq ? get_closest_var(n2, t2) : r2->m_th_var_list.get_th_var(); theory_var v1 = m_fparams.m_new_core2th_eq ? get_closest_var(n1, t1) : r1->m_th_var_list.get_th_var(); TRACE("merge_theory_vars", - tout << "v2: " << v2 << " #" << r1->get_owner_id() << ", v1: " << v1 << " #" << r2->get_owner_id() + tout << "v2: " << v2 << " #" << r2->get_owner_id() << ", v1: " << v1 << " #" << r1->get_owner_id() << ", t2: " << t2 << ", t1: " << t1 << "\n";); if (v2 != null_theory_var && v1 != null_theory_var) { if (t1 == t2) { diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index d9a953154..a09078ad6 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -28,18 +28,19 @@ using namespace smt; void theory_seq::solution_map::update(expr* e, expr* r, enode_pair_dependency* d) { std::pair value; if (m_map.find(e, value)) { - m_updates.push_back(DEL); - m_lhs.push_back(e); - m_rhs.push_back(value.first); - m_deps.push_back(value.second); + add_trail(DEL, e, value.first, value.second); } value.first = r; value.second = d; m_map.insert(e, value); - m_updates.push_back(INS); - m_lhs.push_back(e); - m_rhs.push_back(value.first); - m_deps.push_back(value.second); + add_trail(INS, e, r, d); +} + +void theory_seq::solution_map::add_trail(map_update op, expr* l, expr* r, enode_pair_dependency* d) { + m_updates.push_back(op); + m_lhs.push_back(l); + m_rhs.push_back(r); + m_deps.push_back(d); } expr* theory_seq::solution_map::find(expr* e, enode_pair_dependency*& d) { @@ -84,6 +85,34 @@ void theory_seq::solution_map::display(std::ostream& out) const { } } +void theory_seq::exclusion_table::update(expr* e, expr* r) { + if (e->get_id() > r->get_id()) { + std::swap(e, r); + } + if (e != r && !m_table.contains(std::make_pair(e, r))) { + m_lhs.push_back(e); + m_rhs.push_back(r); + m_table.insert(std::make_pair(e, r)); + } +} + +void theory_seq::exclusion_table::pop_scope(unsigned num_scopes) { + if (num_scopes == 0) return; + unsigned start = m_limit[m_limit.size() - num_scopes]; + for (unsigned i = start; i < m_lhs.size(); ++i) { + m_table.erase(std::make_pair(m_lhs[i].get(), m_rhs[i].get())); + } + m_lhs.resize(start); + m_rhs.resize(start); + m_limit.resize(m_limit.size() - num_scopes); +} + +void theory_seq::exclusion_table::display(std::ostream& out) const { + table_t::iterator it = m_table.begin(), end = m_table.end(); + for (; it != end; ++it) { + out << mk_pp(it->first, m) << " != " << mk_pp(it->second, m) << "\n"; + } +} theory_seq::theory_seq(ast_manager& m): theory(m.mk_family_id("seq")), @@ -91,9 +120,12 @@ theory_seq::theory_seq(ast_manager& m): m_dam(m_dep_array_value_manager, m_alloc), m_rep(m, m_dm), m_ineqs(m), + m_exclude(m), m_axioms(m), m_axioms_head(0), + m_branch_variable_head(0), m_incomplete(false), + m_model_completion(false), m_rewrite(m), m_util(m), m_autil(m), @@ -130,6 +162,15 @@ final_check_status theory_seq::final_check_eh() { if (ctx.inconsistent()) { return FC_CONTINUE; } + if (branch_variable()) { + return FC_CONTINUE; + } + if (split_variable()) { + return FC_CONTINUE; + } + if (ctx.inconsistent()) { + return FC_CONTINUE; + } if (m.size(m_lhs.back()) > 0 || m_incomplete) { return FC_GIVEUP; } @@ -152,19 +193,98 @@ bool theory_seq::check_ineqs() { return true; } +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); + 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";); + ls.reset(); rs.reset(); + m_util.str.get_concat(l, ls); + m_util.str.get_concat(r, rs); + + if (!ls.empty() && find_branch_candidate(ls[0], rs)) { + m_branch_variable_head = k; + return true; + } + if (!rs.empty() && find_branch_candidate(rs[0], ls)) { + m_branch_variable_head = k; + return true; + } + } + return false; +} + +bool theory_seq::find_branch_candidate(expr* l, ptr_vector const& rs) { + + TRACE("seq", tout << mk_pp(l, m) << " " + << (is_var(l)?"var":"not var") << "\n";); + + if (!is_var(l)) { + return false; + } + + expr_ref v0(m), v(m); + v0 = m_util.str.mk_empty(m.get_sort(l)); + if (assume_equality(l, v0)) { + return true; + } + for (unsigned j = 0; j < rs.size(); ++j) { + if (occurs(l, rs[j])) { + return false; + } + std::string 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)); + if (v0) v = m_util.str.mk_concat(v0, v); + if (assume_equality(l, v)) { + return true; + } + } + } + v0 = (j == 0)? rs[0] : m_util.str.mk_concat(v0, rs[j]); + if (assume_equality(l, v0)) { + return true; + } + } + return false; +} + +bool theory_seq::assume_equality(expr* l, expr* r) { + TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << "\n";); + context& ctx = get_context(); + if (m_exclude.contains(l, r)) { + return false; + } + else { + SASSERT(ctx.e_internalized(l)); + if (!ctx.e_internalized(r)) ctx.internalize(r, false); + enode* n1 = ctx.get_enode(l); + enode* n2 = ctx.get_enode(r); + ctx.assume_eq(n1, n2); + } + return true; +} + +bool theory_seq::split_variable() { + + return false; +} + 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 << " <- "; - for (unsigned i = 0; i < _eqs.size(); ++i) { - tout << mk_pp(_eqs[i].first->get_owner(), m) << " = " - << mk_pp(_eqs[i].second->get_owner(), m) << "\n"; - } - ); + TRACE("seq", ctx.display_detailed_literal(tout, lit); + tout << " <-\n"; display_deps(tout, dep);); justification* js = ctx.mk_justification( ext_theory_propagation_justification( @@ -177,12 +297,7 @@ void theory_seq::set_conflict(enode_pair_dependency* dep) { context& ctx = get_context(); vector _eqs; m_dm.linearize(dep, _eqs); - TRACE("seq", - for (unsigned i = 0; i < _eqs.size(); ++i) { - tout << mk_pp(_eqs[i].first->get_owner(), m) << " = " - << mk_pp(_eqs[i].second->get_owner(), m) << "\n"; - } - ); + TRACE("seq", display_deps(tout, dep);); ctx.set_conflict( ctx.mk_justification( ext_theory_conflict_justification( @@ -195,10 +310,7 @@ void theory_seq::propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2) m_dm.linearize(dep, _eqs); TRACE("seq", tout << mk_pp(n1->get_owner(), m) << " " << mk_pp(n2->get_owner(), m) << " <- "; - for (unsigned i = 0; i < _eqs.size(); ++i) { - tout << mk_pp(_eqs[i].first->get_owner(), m) << " = " - << mk_pp(_eqs[i].second->get_owner(), m) << "\n"; - } + display_deps(tout, dep); ); justification* js = ctx.mk_justification( @@ -366,13 +478,19 @@ bool theory_seq::internalize_atom(app* a, bool) { } bool theory_seq::internalize_term(app* term) { + TRACE("seq", tout << mk_pp(term, m) << "\n";); context & ctx = get_context(); unsigned num_args = term->get_num_args(); for (unsigned i = 0; i < num_args; i++) { - ctx.internalize(term->get_arg(i), false); + expr* arg = term->get_arg(i); + ctx.internalize(arg, false); + if (ctx.e_internalized(arg)) { + mk_var(ctx.get_enode(arg)); + } } + enode* e = 0; if (ctx.e_internalized(term)) { - return true; + e = ctx.get_enode(term); } if (m.is_bool(term)) { bool_var bv = ctx.mk_bool_var(term); @@ -380,9 +498,10 @@ bool theory_seq::internalize_term(app* term) { ctx.set_enode_flag(bv, true); } else { - enode * e = ctx.mk_enode(term, false, m.is_bool(term), true); - theory_var v = mk_var(e); - ctx.attach_th_var(e, this, v); + if (!e) { + e = ctx.mk_enode(term, false, m.is_bool(term), true); + } + mk_var(e); } if (!m_util.str.is_concat(term) && !m_util.str.is_string(term) && @@ -400,33 +519,43 @@ bool theory_seq::internalize_term(app* term) { } void theory_seq::apply_sort_cnstr(enode* n, sort* s) { - if (!is_attached_to_var(n)) { - mk_var(n); - } + mk_var(n); } void theory_seq::display(std::ostream & out) const { - expr_array const& lhs = m_lhs.back(); - expr_array const& rhs = m_rhs.back(); - enode_pair_dependency_array const& deps = m_deps.back(); - out << "Equations:\n"; - for (unsigned i = 0; i < m.size(lhs); ++i) { - out << mk_pp(m.get(lhs, i), m) << " = " << mk_pp(m.get(rhs, i), m) << " <-\n"; - enode_pair_dependency* dep = m_dam.get(deps, i); - if (dep) { - vector _eqs; - const_cast(m_dm).linearize(dep, _eqs); - for (unsigned i = 0; i < _eqs.size(); ++i) { - out << " " << mk_pp(_eqs[i].first->get_owner(), m) << " = " << mk_pp(_eqs[i].second->get_owner(), m) << "\n"; - } + display_equations(out); + if (!m_ineqs.empty()) { + out << "Negative constraints:\n"; + for (unsigned i = 0; i < m_ineqs.size(); ++i) { + out << mk_pp(m_ineqs[i], m) << "\n"; } } - out << "Negative constraints:\n"; - for (unsigned i = 0; i < m_ineqs.size(); ++i) { - out << mk_pp(m_ineqs[i], m) << "\n"; - } out << "Solved equations:\n"; m_rep.display(out); + m_exclude.display(out); +} + +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(); + if (m.size(lhs) == 0) { + return; + } + out << "Equations:\n"; + for (unsigned i = 0; i < m.size(lhs); ++i) { + out << mk_pp(m.get(lhs, i), m) << " = " << mk_pp(m.get(rhs, i), m) << " <-\n"; + display_deps(out, m_dam.get(deps, i)); + } +} + +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"; + } } void theory_seq::collect_statistics(::statistics & st) const { @@ -438,31 +567,13 @@ void theory_seq::init_model(model_generator & mg) { m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()); mg.register_factory(m_factory); - // TBD: this is still unsound model generation. - // disequalities are not guaranteed. we need to - // prime the factory with a prefix that cannot be - // constructed using any existing combinations of the - // strings (or units) that are used. - for (unsigned i = 0; i < get_num_vars(); ++i) { - expr* e = get_enode(i)->get_owner(); - if (m_util.is_seq(e)) { - enode_pair_dependency* deps = 0; - e = m_rep.find(e, deps); - if (is_var(e)) { - expr* val = m_factory->get_fresh_value(m.get_sort(e)); - m_rep.update(e, val, 0); - } - } - else if (m_util.is_re(e)) { - // TBD - } - } } model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { enode_pair_dependency* deps = 0; expr_ref e(n->get_owner(), m); - canonize(e, deps); + flet _model_completion(m_model_completion, true); + e = canonize(e, deps); SASSERT(is_app(e)); m_factory->add_trail(e); return alloc(expr_wrapper_proc, to_app(e)); @@ -479,7 +590,14 @@ void theory_seq::set_incomplete(app* term) { } theory_var theory_seq::mk_var(enode* n) { - return theory::mk_var(n); + if (is_attached_to_var(n)) { + return n->get_th_var(get_id()); + } + else { + theory_var v = theory::mk_var(n); + get_context().attach_th_var(n, this, v); + return v; + } } bool theory_seq::can_propagate() { @@ -515,6 +633,15 @@ expr_ref theory_seq::expand(expr* e, enode_pair_dependency*& 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); } + 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; + } + } return expr_ref(e, m); } @@ -625,11 +752,14 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { expr* e2 = get_enode(v2)->get_owner(); m_trail_stack.push(push_back_vector(m_ineqs)); m_ineqs.push_back(mk_eq_atom(e1, e2)); + m_exclude.update(e1, e2); } void theory_seq::push_scope_eh() { + TRACE("seq", tout << "push " << m_lhs.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)); @@ -644,10 +774,12 @@ void theory_seq::push_scope_eh() { } void theory_seq::pop_scope_eh(unsigned num_scopes) { + TRACE("seq", tout << "pop " << m_lhs.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()); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 3cdacaeda..06fb6fac0 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -53,10 +53,12 @@ namespace smt { ast_manager& m; enode_pair_dependency_manager& m_dm; map_t m_map; - expr_ref_vector m_lhs, m_rhs; + expr_ref_vector m_lhs, m_rhs; ptr_vector m_deps; svector m_updates; unsigned_vector m_limit; + + 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) {} void update(expr* e, expr* r, enode_pair_dependency* d); @@ -66,6 +68,24 @@ namespace smt { void display(std::ostream& out) const; }; + class exclusion_table { + typedef obj_pair_hashtable table_t; + ast_manager& m; + table_t m_table; + expr_ref_vector m_lhs, m_rhs; + unsigned_vector m_limit; + public: + exclusion_table(ast_manager& m): m(m), m_lhs(m), m_rhs(m) {} + ~exclusion_table() { } + void update(expr* e, expr* r); + bool contains(expr* e, expr* r) { + return m_table.contains(std::make_pair(e, r)); + } + void push_scope() { m_limit.push_back(m_lhs.size()); } + void pop_scope(unsigned num_scopes); + void display(std::ostream& out) const; + }; + struct stats { stats() { reset(); } void reset() { memset(this, 0, sizeof(stats)); } @@ -81,11 +101,14 @@ namespace smt { vector m_lhs, m_rhs; // persistent sets of equalities. vector m_deps; // persistent sets of dependencies. - seq_factory* m_factory; // value factory - expr_ref_vector m_ineqs; // inequalities to check - expr_ref_vector m_axioms; - unsigned m_axioms_head; - bool m_incomplete; + seq_factory* m_factory; // value factory + expr_ref_vector m_ineqs; // inequalities to check solution against + exclusion_table m_exclude; // set of asserted disequalities. + expr_ref_vector m_axioms; // list of axioms to add. + 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_model_completion; // during model construction, invent values in canonizer th_rewriter m_rewrite; seq_util m_util; arith_util m_autil; @@ -95,8 +118,8 @@ namespace smt { symbol m_suffix_sym; symbol m_contains_left_sym; symbol m_contains_right_sym; - symbol m_left_sym; - symbol m_right_sym; + symbol m_left_sym; // split variable left part + symbol m_right_sym; // split variable right part virtual final_check_status final_check_eh(); virtual bool internalize_atom(app*, bool); @@ -114,23 +137,29 @@ namespace smt { virtual char const * get_name() const { return "seq"; } virtual theory_var mk_var(enode* n); virtual void apply_sort_cnstr(enode* n, sort* s); - virtual void display(std::ostream & out) const; + virtual void display(std::ostream & out) const; virtual void collect_statistics(::statistics & st) const; virtual model_value_proc * mk_value(enode * n, model_generator & mg); virtual void init_model(model_generator & mg); - bool check_ineqs(); + bool check_ineqs(); // check if inequalities are violated. + bool simplify_and_solve_eqs(); // solve unitary equalities + bool branch_variable(); // branch on a variable + bool split_variable(); // split a variable + bool pre_process_eqs(bool simplify_or_solve); bool simplify_eqs(); bool simplify_eq(expr* l, expr* r, enode_pair_dependency* dep); bool solve_unit_eq(expr* l, expr* r, enode_pair_dependency* dep); bool solve_basic_eqs(); - bool simplify_and_solve_eqs(); void propagate_lit(enode_pair_dependency* dep, literal lit); void propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2); void propagate_eq(bool_var v, expr* e1, expr* e2); void set_conflict(enode_pair_dependency* dep); + bool find_branch_candidate(expr* l, ptr_vector const& rs); + bool assume_equality(expr* l, expr* r); + bool occurs(expr* a, expr* b); bool is_var(expr* b); void add_solution(expr* l, expr* r, enode_pair_dependency* dep); @@ -148,6 +177,9 @@ namespace smt { expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2); void set_incomplete(app* term); + + void display_equations(std::ostream& out) const; + void display_deps(std::ostream& out, enode_pair_dependency* deps) const; public: theory_seq(ast_manager& m); virtual ~theory_seq(); From c5a9d81d93b9b8e5c44ee0605a66ae77a7cfc17b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Dec 2015 20:17:00 -0800 Subject: [PATCH 02/10] seq Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.h | 3 + src/ast/rewriter/seq_rewriter.cpp | 39 ++++--- src/ast/rewriter/seq_rewriter.h | 12 +- src/ast/seq_decl_plugin.cpp | 21 +++- src/ast/seq_decl_plugin.h | 19 ++-- src/smt/theory_seq.cpp | 183 +++++++++++++++++++++++++++--- src/smt/theory_seq.h | 13 ++- 7 files changed, 239 insertions(+), 51 deletions(-) diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index e185b241b..252bd8ed6 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -328,6 +328,9 @@ public: app * mk_numeral(sexpr const * p, unsigned i) { return plugin().mk_numeral(p, i); } + app * mk_int(int i) { + return mk_numeral(rational(i), true); + } app * mk_le(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LE, arg1, arg2); } app * mk_ge(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_GE, arg1, arg2); } app * mk_lt(expr * arg1, expr * arg2) const { return m_manager.mk_app(m_afid, OP_LT, arg1, arg2); } diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index f810b48cd..96e11283e 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -55,22 +55,28 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con return mk_seq_concat(args[0], args[1], result); case OP_SEQ_LENGTH: SASSERT(num_args == 1); - return mk_str_length(args[0], result); + return mk_seq_length(args[0], result); case OP_SEQ_EXTRACT: SASSERT(num_args == 3); - return mk_str_substr(args[0], args[1], args[2], result); + return mk_seq_extract(args[0], args[1], args[2], result); case OP_SEQ_CONTAINS: SASSERT(num_args == 2); - return mk_str_strctn(args[0], args[1], result); + return mk_seq_contains(args[0], args[1], result); case OP_SEQ_AT: SASSERT(num_args == 2); - return mk_str_at(args[0], args[1], result); + return mk_seq_at(args[0], args[1], result); case OP_SEQ_PREFIX: SASSERT(num_args == 2); return mk_seq_prefix(args[0], args[1], result); case OP_SEQ_SUFFIX: SASSERT(num_args == 2); return mk_seq_suffix(args[0], args[1], result); + case OP_SEQ_INDEX: + SASSERT(num_args == 3); + return mk_seq_index(args[0], args[1], args[2], result); + case OP_SEQ_REPLACE: + SASSERT(num_args == 3); + return mk_seq_replace(args[0], args[1], args[2], result); case OP_SEQ_TO_RE: return BR_FAILED; case OP_SEQ_IN_RE: @@ -78,12 +84,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_STRING_CONST: return BR_FAILED; - case OP_STRING_STRIDOF: - SASSERT(num_args == 3); - return mk_str_stridof(args[0], args[1], args[2], result); - case OP_STRING_STRREPL: - SASSERT(num_args == 3); - return mk_str_strrepl(args[0], args[1], args[2], result); case OP_STRING_ITOS: SASSERT(num_args == 1); return mk_str_itos(args[0], result); @@ -101,7 +101,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case _OP_STRING_IN_REGEXP: case _OP_STRING_TO_REGEXP: case _OP_STRING_SUBSTR: - + case _OP_STRING_STRREPL: + case _OP_STRING_STRIDOF: UNREACHABLE(); } return BR_FAILED; @@ -143,7 +144,7 @@ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) { return BR_FAILED; } -br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) { +br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) { std::string b; m_es.reset(); m_util.str.get_concat(a, m_es); @@ -176,7 +177,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) { return BR_FAILED; } -br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result) { +br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result) { std::string s; rational pos, len; if (m_util.str.is_string(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) && @@ -188,7 +189,7 @@ br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& resul } return BR_FAILED; } -br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) { +br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) { std::string c, d; if (m_util.str.is_string(a, c) && m_util.str.is_string(b, d)) { result = m().mk_bool_val(0 != strstr(d.c_str(), c.c_str())); @@ -212,7 +213,7 @@ br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) { return BR_FAILED; } -br_status seq_rewriter::mk_str_at(expr* a, expr* b, expr_ref& result) { +br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) { std::string c; rational r; if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r) && r.is_unsigned()) { @@ -228,7 +229,7 @@ br_status seq_rewriter::mk_str_at(expr* a, expr* b, expr_ref& result) { return BR_FAILED; } -br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& result) { +br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result) { std::string s1, s2; rational r; bool isc1 = m_util.str.is_string(a, s1); @@ -257,15 +258,17 @@ br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& resu return BR_FAILED; } -br_status seq_rewriter::mk_str_strrepl(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; 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 (strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) { + 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]; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index d4652f614..ec1747a4b 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -35,12 +35,12 @@ class seq_rewriter { 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); - br_status mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result); - br_status mk_str_strctn(expr* a, expr* b, expr_ref& result); - br_status mk_str_at(expr* a, expr* b, expr_ref& result); - br_status mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& result); - br_status mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result); + br_status mk_seq_length(expr* a, expr_ref& result); + br_status mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result); + br_status mk_seq_contains(expr* a, expr* b, expr_ref& result); + br_status mk_seq_at(expr* a, expr* b, expr_ref& result); + br_status mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result); + br_status mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& result); br_status mk_seq_prefix(expr* a, expr* b, expr_ref& result); br_status mk_seq_suffix(expr* a, expr* b, expr_ref& result); br_status mk_str_itos(expr* a, expr_ref& result); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 2946bb1bc..5639356cc 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -177,6 +177,7 @@ void seq_decl_plugin::init() { sort* reAreA[2] = { reA, reA }; sort* AA[2] = { A, A }; sort* seqAint2T[3] = { seqA, intT, intT }; + sort* seq2AintT[3] = { seqA, seqA, intT }; sort* str2T[2] = { strT, strT }; sort* str3T[3] = { strT, strT, strT }; sort* strTint2T[3] = { strT, intT, intT }; @@ -184,6 +185,7 @@ void seq_decl_plugin::init() { sort* strTreT[2] = { strT, reT }; sort* str2TintT[3] = { strT, strT, intT }; sort* seqAintT[2] = { seqA, intT }; + sort* seq3A[3] = { seqA, seqA, seqA }; m_sigs.resize(LAST_SEQ_OP); // TBD: have (par ..) construct and load parameterized signature from premable. m_sigs[OP_SEQ_UNIT] = alloc(psig, m, "seq.unit", 1, 1, &A, seqA); @@ -193,6 +195,8 @@ void seq_decl_plugin::init() { m_sigs[OP_SEQ_SUFFIX] = alloc(psig, m, "seq.suffixof", 1, 2, seqAseqA, boolT); m_sigs[OP_SEQ_CONTAINS] = alloc(psig, m, "seq.contains", 1, 2, seqAseqA, boolT); m_sigs[OP_SEQ_EXTRACT] = alloc(psig, m, "seq.extract", 1, 3, seqAint2T, seqA); + m_sigs[OP_SEQ_REPLACE] = alloc(psig, m, "seq.replace", 1, 3, seq3A, strT); + m_sigs[OP_SEQ_INDEX] = alloc(psig, m, "seq.indexof", 1, 3, seq2AintT, intT); m_sigs[OP_SEQ_AT] = alloc(psig, m, "seq.at", 1, 2, seqAintT, seqA); m_sigs[OP_SEQ_LENGTH] = alloc(psig, m, "seq.len", 1, 1, &seqA, intT); m_sigs[OP_RE_PLUS] = alloc(psig, m, "re.+", 1, 1, &reA, reA); @@ -209,8 +213,8 @@ void seq_decl_plugin::init() { m_sigs[OP_SEQ_TO_RE] = alloc(psig, m, "seq.to.re", 1, 1, &seqA, reA); m_sigs[OP_SEQ_IN_RE] = alloc(psig, m, "seq.in.re", 1, 2, seqAreA, boolT); m_sigs[OP_STRING_CONST] = 0; - m_sigs[OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT); - m_sigs[OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT); + m_sigs[_OP_STRING_STRIDOF] = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT); + m_sigs[_OP_STRING_STRREPL] = alloc(psig, m, "str.replace", 0, 3, str3T, strT); m_sigs[OP_STRING_ITOS] = alloc(psig, m, "int.to.str", 0, 1, &intT, strT); m_sigs[OP_STRING_STOI] = alloc(psig, m, "str.to.int", 0, 1, &strT, intT); m_sigs[OP_REGEXP_LOOP] = alloc(psig, m, "re.loop", 0, 2, strTint2T, reT); // maybe 3 arguments. @@ -347,6 +351,17 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, info.set_left_associative(); return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info); } + + case OP_SEQ_REPLACE: + return mk_seq_fun(k, arity, domain, range, _OP_STRING_STRREPL); + case _OP_STRING_STRREPL: + return mk_str_fun(k, arity, domain, range, OP_SEQ_REPLACE); + + case OP_SEQ_INDEX: + return mk_seq_fun(k, arity, domain, range, _OP_STRING_STRIDOF); + case _OP_STRING_STRIDOF: + return mk_str_fun(k, arity, domain, range, OP_SEQ_INDEX); + case OP_SEQ_PREFIX: return mk_seq_fun(k, arity, domain, range, _OP_STRING_PREFIX); case _OP_STRING_PREFIX: @@ -387,8 +402,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case _OP_STRING_SUBSTR: return mk_str_fun(k, arity, domain, range, OP_SEQ_EXTRACT); - case OP_STRING_STRIDOF: - case OP_STRING_STRREPL: case OP_STRING_ITOS: case OP_STRING_STOI: case OP_REGEXP_LOOP: diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 0ab889c38..33091ebd2 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -39,8 +39,10 @@ enum seq_op_kind { OP_SEQ_SUFFIX, OP_SEQ_CONTAINS, OP_SEQ_EXTRACT, + OP_SEQ_REPLACE, OP_SEQ_AT, - OP_SEQ_LENGTH, + OP_SEQ_LENGTH, + OP_SEQ_INDEX, OP_SEQ_TO_RE, OP_SEQ_IN_RE, @@ -59,12 +61,11 @@ enum seq_op_kind { // string specific operators. OP_STRING_CONST, - OP_STRING_STRIDOF, // TBD generalize - OP_STRING_STRREPL, // TBD generalize OP_STRING_ITOS, OP_STRING_STOI, OP_REGEXP_LOOP, // TBD re-loop: integers as parameters or arguments? // internal only operators. Converted to SEQ variants. + _OP_STRING_STRREPL, _OP_STRING_CONCAT, _OP_STRING_LENGTH, _OP_STRING_STRCTN, @@ -74,6 +75,7 @@ enum seq_op_kind { _OP_STRING_TO_REGEXP, _OP_STRING_CHARAT, _OP_STRING_SUBSTR, + _OP_STRING_STRIDOF, _OP_SEQ_SKOLEM, LAST_SEQ_OP }; @@ -175,6 +177,9 @@ public: 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); + } 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); } @@ -200,8 +205,8 @@ public: 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_index(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_INDEX); } + bool is_replace(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_REPLACE); } 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); } @@ -215,8 +220,8 @@ public: MATCH_TERNARY(is_extract); MATCH_BINARY(is_contains); MATCH_BINARY(is_at); - MATCH_BINARY(is_stridof); - MATCH_BINARY(is_repl); + MATCH_BINARY(is_index); + MATCH_TERNARY(is_replace); MATCH_BINARY(is_prefix); MATCH_BINARY(is_suffix); MATCH_UNARY(is_itos); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index a09078ad6..e0ab35fea 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -465,13 +465,6 @@ bool theory_seq::simplify_and_solve_eqs() { } -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); @@ -513,8 +506,6 @@ bool theory_seq::internalize_term(app* term) { !m_util.is_skolem(term)) { set_incomplete(term); } - - // assert basic axioms return true; } @@ -667,6 +658,170 @@ void theory_seq::create_axiom(expr_ref& e) { m_axioms.push_back(e); } +/* + encode that s is not a proper prefix of xs +*/ +expr_ref theory_seq::tightest_prefix(expr* s, expr* x) { + expr_ref s1 = mk_skolem(symbol("first"), s); + expr_ref c = mk_skolem(symbol("last"), s); + expr_ref fml(m); + + fml = m.mk_and(m.mk_eq(s, m_util.str.mk_concat(s1, c)), + m.mk_eq(m_util.str.mk_length(c), m_autil.mk_int(1)), + m.mk_not(m_util.str.mk_contains(s, m_util.str.mk_concat(x, s1)))); + + return fml; +} + + +void theory_seq::new_eq_len_concat(enode* n1, enode* n2) { + context& ctx = get_context(); + // TBD: walk use list of n1 for concat, walk use-list of n2 for length. + // instantiate length distributes over concatenation axiom. + SASSERT(n1->get_root() != n2->get_root()); + if (!m_util.is_seq(n1->get_owner())) { + return; + } + func_decl* f_len = 0; + + // TBD: extract length function for sort if it is used. + // TBD: add filter for already processed length equivalence classes + if (!f_len) { + return; + } + enode_vector::const_iterator it = ctx.begin_enodes_of(f_len); + enode_vector::const_iterator end = ctx.end_enodes_of(f_len); + bool has_concat = true; + for (; has_concat && it != end; ++it) { + if ((*it)->get_root() == n1->get_root()) { + enode* start2 = n2; + do { + if (m_util.str.is_concat(n2->get_owner())) { + has_concat = true; + add_len_concat_axiom(n2->get_owner()); + } + n2 = n2->get_next(); + } + while (n2 != start2); + } + } +} + +void theory_seq::add_len_concat_axiom(expr* c) { + // or just internalize lc and have relevancy propagation create axiom? + expr *a, *b; + expr_ref la(m), lb(m), lc(m), fml(m); + VERIFY(m_util.str.is_concat(c, a, b)); + la = m_util.str.mk_length(a); + lb = m_util.str.mk_length(b); + lc = m_util.str.mk_length(c); + fml = m.mk_eq(m_autil.mk_add(la, lb), lc); + create_axiom(fml); +} + +/* + let i = Index(s, t) + + (!contains(s, t) -> i = -1) + (contains(s, t) & s = empty -> i = 0) + (contains(s, t) & s != empty -> t = xsy & tightest_prefix(s, x)) + + optional lemmas: + (len(s) > len(t) -> i = -1) + (len(s) <= len(t) -> i <= len(t)-len(s)) +*/ +void theory_seq::add_indexof_axiom(expr* i) { + expr* s, *t; + VERIFY(m_util.str.is_index(i, s, t)); + expr_ref cnt(m), fml(m), eq_empty(m); + expr_ref x = mk_skolem(m_contains_left_sym, s, t); + expr_ref y = mk_skolem(m_contains_right_sym, s, t); + eq_empty = m.mk_eq(s, m_util.str.mk_empty(m.get_sort(s))); + cnt = m_util.str.mk_contains(s, t); + fml = m.mk_or(cnt, m.mk_eq(i, m_autil.mk_int(-1))); + create_axiom(fml); + fml = m.mk_or(m.mk_not(cnt), m.mk_not(eq_empty), m.mk_eq(i, m_autil.mk_int(0))); + create_axiom(fml); + fml = m.mk_or(m.mk_not(cnt), eq_empty, m.mk_eq(t, m_util.str.mk_concat(x,s,y))); + create_axiom(fml); + fml = m.mk_or(m.mk_not(cnt), eq_empty, tightest_prefix(s, x)); + create_axiom(fml); +} + +/* + let r = replace(a, s, t) + + (contains(s, a) -> r = xty & a = xsy & tightest_prefix(s,xs)) & + (!contains(s, a) -> r = a) + +*/ +void theory_seq::add_replace_axiom(expr* r) { + expr* a, *s, *t; + VERIFY(m_util.str.is_replace(r, a, s, t)); + expr_ref cnt(m), fml(m); + cnt = m_util.str.mk_contains(s, a); + expr_ref x = mk_skolem(m_contains_left_sym, s, a); + expr_ref y = mk_skolem(m_contains_right_sym, s, a); + fml = m.mk_or(m.mk_not(cnt), m.mk_eq(a, m_util.str.mk_concat(x, s, y))); + create_axiom(fml); + fml = m.mk_or(m.mk_not(cnt), m.mk_eq(r, m_util.str.mk_concat(x, t, y))); + create_axiom(fml); + fml = m.mk_or(m.mk_not(cnt), tightest_prefix(s, x)); + create_axiom(fml); + fml = m.mk_or(cnt, m.mk_eq(r, a)); + create_axiom(fml); +} + +/* + let n = len(x) + + len(x) >= 0 + len(x) = 0 => x = "" + x = "" => len(x) = 0 + len(x) = rewrite(len(x)) + */ +void theory_seq::add_len_axiom(expr* n) { + expr* x; + VERIFY(m_util.str.is_length(n, x)); + expr_ref fml(m), eq1(m), eq2(m), nr(m); + eq1 = m.mk_eq(m_autil.mk_int(0), n); + eq2 = m.mk_eq(x, m_util.str.mk_empty(m.get_sort(x))); + fml = m_autil.mk_le(m_autil.mk_int(0), n); + create_axiom(fml); + fml = m.mk_or(m.mk_not(eq1), eq2); + create_axiom(fml); + fml = m.mk_or(m.mk_not(eq2), eq1); + create_axiom(fml); + nr = n; + m_rewrite(nr); + if (nr != n) { + fml = m.mk_eq(n, nr); + create_axiom(fml); + } +} + +/* + check semantics of extract. + + let e = extract(s, i, l) + + 0 <= i < len(s) -> prefix(xe,s) & len(x) = i + 0 <= i < len(s) & l >= len(s) - i -> len(e) = len(s) - i + 0 <= i < len(s) & 0 <= l < len(s) - i -> len(e) = l + 0 <= i < len(s) & l < 0 -> len(e) = 0 + i < 0 -> e = s + i >= len(s) -> e = empty +*/ + +void theory_seq::add_extract_axiom(expr* e) { + expr* s, *i, *j; + VERIFY(m_util.str.is_extract(e, s, i, j)); + expr_ref i_ge_0(m), i_le_j(m), j_lt_s(m); + + NOT_IMPLEMENTED_YET(); + +} + void theory_seq::assert_axiom(expr_ref& e) { context & ctx = get_context(); if (m.is_true(e)) return; @@ -679,7 +834,7 @@ void theory_seq::assert_axiom(expr_ref& e) { 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, 2, es, m.get_sort(e1)), m); + return expr_ref(m_util.mk_skolem(name, e2?2:1, es, m.get_sort(e1)), m); } void theory_seq::propagate_eq(bool_var v, expr* e1, expr* e2) { @@ -744,6 +899,9 @@ void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { m.push_back(m_lhs.back(), n1->get_owner()); m.push_back(m_rhs.back(), n2->get_owner()); m_dam.push_back(m_deps.back(), m_dm.mk_leaf(enode_pair(n1, n2))); + + new_eq_len_concat(n1, n2); + new_eq_len_concat(n2, n1); } } @@ -807,8 +965,7 @@ void theory_seq::restart_eh() { void theory_seq::relevant_eh(app* n) { 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); + add_len_axiom(n); } } + diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 06fb6fac0..87a6a2dc6 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -166,15 +166,22 @@ namespace smt { bool is_left_select(expr* a, expr*& b); bool is_right_select(expr* a, expr*& b); - final_check_status add_axioms(); - void assert_axiom(expr_ref& e); void create_axiom(expr_ref& e); + void add_indexof_axiom(expr* e); + void add_replace_axiom(expr* e); + void add_extract_axiom(expr* e); + void add_len_concat_axiom(expr* c); + void add_len_axiom(expr* n); + + void new_eq_len_concat(enode* n1, enode* n2); + + expr_ref tightest_prefix(expr* s, expr* x); expr_ref canonize(expr* e, enode_pair_dependency*& eqs); expr_ref expand(expr* e, enode_pair_dependency*& eqs); void add_dependency(enode_pair_dependency*& dep, enode* a, enode* b); - expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2); + expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0); void set_incomplete(app* term); From d58c219b540590fe40c98071b72d489edc01d455 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Dec 2015 22:18:02 -0800 Subject: [PATCH 03/10] seq Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 267 ++++++++++++++++++++++++++--------------- src/smt/theory_seq.h | 8 +- 2 files changed, 177 insertions(+), 98 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index e0ab35fea..a9d6925fd 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -22,6 +22,7 @@ Revision History: #include "smt_model_generator.h" #include "theory_seq.h" #include "seq_rewriter.h" +#include "ast_trail.h" using namespace smt; @@ -118,7 +119,9 @@ 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_rep(m, m_dm), + m_sort2len_fn(m), + m_factory(0), m_ineqs(m), m_exclude(m), m_axioms(m), @@ -129,7 +132,7 @@ theory_seq::theory_seq(ast_manager& m): m_rewrite(m), m_util(m), m_autil(m), - m_trail_stack(*this) { + m_trail_stack(*this) { m_lhs.push_back(expr_array()); m_rhs.push_back(expr_array()); m_deps.push_back(enode_pair_dependency_array()); @@ -506,6 +509,11 @@ 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; } @@ -555,8 +563,7 @@ void theory_seq::collect_statistics(::statistics & st) const { } void theory_seq::init_model(model_generator & mg) { - m_factory = alloc(seq_factory, get_manager(), - get_family_id(), mg.get_model()); + m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()); mg.register_factory(m_factory); } @@ -575,7 +582,7 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { void theory_seq::set_incomplete(app* term) { TRACE("seq", tout << "No support for: " << mk_pp(term, m) << "\n";); if (!m_incomplete) { - m_trail_stack.push(value_trail(m_incomplete)); + m_trail_stack.push(value_trail(m_incomplete)); m_incomplete = true; } } @@ -659,72 +666,73 @@ void theory_seq::create_axiom(expr_ref& e) { } /* - encode that s is not a proper prefix of xs -*/ -expr_ref theory_seq::tightest_prefix(expr* s, expr* x) { - expr_ref s1 = mk_skolem(symbol("first"), s); - expr_ref c = mk_skolem(symbol("last"), s); - expr_ref fml(m); - - fml = m.mk_and(m.mk_eq(s, m_util.str.mk_concat(s1, c)), - m.mk_eq(m_util.str.mk_length(c), m_autil.mk_int(1)), - m.mk_not(m_util.str.mk_contains(s, m_util.str.mk_concat(x, s1)))); - - return fml; -} - - + \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(); - // TBD: walk use list of n1 for concat, walk use-list of n2 for length. - // instantiate length distributes over concatenation axiom. SASSERT(n1->get_root() != n2->get_root()); if (!m_util.is_seq(n1->get_owner())) { return; } func_decl* f_len = 0; - - // TBD: extract length function for sort if it is used. - // TBD: add filter for already processed length equivalence classes - if (!f_len) { + if (!m_sort2len_fn.find(m.get_sort(n1->get_owner()), f_len)) { return; } - enode_vector::const_iterator it = ctx.begin_enodes_of(f_len); + + 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_concat = true; - for (; has_concat && it != end; ++it) { - if ((*it)->get_root() == n1->get_root()) { - enode* start2 = n2; - do { - if (m_util.str.is_concat(n2->get_owner())) { - has_concat = true; - add_len_concat_axiom(n2->get_owner()); - } - n2 = n2->get_next(); - } - while (n2 != start2); - } + bool has_len = false; + for (; !has_len && it != end; ++it) { + has_len = ((*it)->get_root() == r1); } + if (!has_len) { + return; + } + enode* start2 = n2; + do { + if (m_util.str.is_concat(n2->get_owner())) { + expr_ref ln(m); + ln = m_util.str.mk_length(n2->get_owner()); + add_len_axiom(ln); + } + n2 = n2->get_next(); + } + while (n2 != start2); } -void theory_seq::add_len_concat_axiom(expr* c) { - // or just internalize lc and have relevancy propagation create axiom? - expr *a, *b; - expr_ref la(m), lb(m), lc(m), fml(m); - VERIFY(m_util.str.is_concat(c, a, b)); - la = m_util.str.mk_length(a); - lb = m_util.str.mk_length(b); - lc = m_util.str.mk_length(c); - fml = m.mk_eq(m_autil.mk_add(la, lb), lc); - create_axiom(fml); + +/* + encode that s is not a proper prefix of xs1 + where s1 is all of s, except the last element. + + lit or s = "" or s = s1*c + 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) { + expr_ref s1 = mk_skolem(symbol("first"), s); + expr_ref c = mk_skolem(symbol("last"), s); + expr_ref s1c(m_util.str.mk_concat(s1, c), m); + expr_ref lc(m_util.str.mk_length(c), m); + 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)))); } /* let i = Index(s, t) (!contains(s, t) -> i = -1) - (contains(s, t) & s = empty -> i = 0) - (contains(s, t) & s != empty -> t = xsy & tightest_prefix(s, x)) + (s = empty -> i = 0) + (contains(s, t) & s != empty -> t = xsy) + (contains(s, t) -> tightest_prefix(s, x)) optional lemmas: (len(s) > len(t) -> i = -1) @@ -733,43 +741,41 @@ void theory_seq::add_len_concat_axiom(expr* c) { void theory_seq::add_indexof_axiom(expr* i) { expr* s, *t; VERIFY(m_util.str.is_index(i, s, t)); - expr_ref cnt(m), fml(m), eq_empty(m); + expr_ref fml(m), emp(m), minus_one(m), zero(m), xsy(m); expr_ref x = mk_skolem(m_contains_left_sym, s, t); expr_ref y = mk_skolem(m_contains_right_sym, s, t); - eq_empty = m.mk_eq(s, m_util.str.mk_empty(m.get_sort(s))); - cnt = m_util.str.mk_contains(s, t); - fml = m.mk_or(cnt, m.mk_eq(i, m_autil.mk_int(-1))); - create_axiom(fml); - fml = m.mk_or(m.mk_not(cnt), m.mk_not(eq_empty), m.mk_eq(i, m_autil.mk_int(0))); - create_axiom(fml); - fml = m.mk_or(m.mk_not(cnt), eq_empty, m.mk_eq(t, m_util.str.mk_concat(x,s,y))); - create_axiom(fml); - fml = m.mk_or(m.mk_not(cnt), eq_empty, tightest_prefix(s, x)); - create_axiom(fml); + minus_one = m_autil.mk_int(-1); + zero = m_autil.mk_int(0); + emp = m_util.str.mk_empty(m.get_sort(s)); + xsy = m_util.str.mk_concat(x,s,y); + literal cnt = mk_literal(m_util.str.mk_contains(s, t)); + 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); } /* let r = replace(a, s, t) - (contains(s, a) -> r = xty & a = xsy & tightest_prefix(s,xs)) & + (contains(s, a) -> tightest_prefix(s,xs)) + (contains(s, a) -> r = xty & a = xsy) & (!contains(s, a) -> r = a) */ void theory_seq::add_replace_axiom(expr* r) { expr* a, *s, *t; VERIFY(m_util.str.is_replace(r, a, s, t)); - expr_ref cnt(m), fml(m); - cnt = m_util.str.mk_contains(s, a); expr_ref x = mk_skolem(m_contains_left_sym, s, a); expr_ref y = mk_skolem(m_contains_right_sym, s, a); - fml = m.mk_or(m.mk_not(cnt), m.mk_eq(a, m_util.str.mk_concat(x, s, y))); - create_axiom(fml); - fml = m.mk_or(m.mk_not(cnt), m.mk_eq(r, m_util.str.mk_concat(x, t, y))); - create_axiom(fml); - fml = m.mk_or(m.mk_not(cnt), tightest_prefix(s, x)); - create_axiom(fml); - fml = m.mk_or(cnt, m.mk_eq(r, a)); - create_axiom(fml); + expr_ref xsy(m_util.str.mk_concat(x, t, y), m); + expr_ref xty(m_util.str.mk_concat(x, s, y), m); + literal cnt = mk_literal(m_util.str.mk_contains(s, a)); + add_axiom(cnt, mk_eq(r, a, false)); + add_axiom(~cnt, mk_eq(a, xsy, false)); + add_axiom(~cnt, mk_eq(r, xty, false)); + tightest_prefix(s, x, ~cnt); } /* @@ -781,27 +787,26 @@ void theory_seq::add_replace_axiom(expr* r) { len(x) = rewrite(len(x)) */ void theory_seq::add_len_axiom(expr* n) { - expr* x; + expr* x, *a, *b; VERIFY(m_util.str.is_length(n, x)); - expr_ref fml(m), eq1(m), eq2(m), nr(m); - eq1 = m.mk_eq(m_autil.mk_int(0), n); - eq2 = m.mk_eq(x, m_util.str.mk_empty(m.get_sort(x))); - fml = m_autil.mk_le(m_autil.mk_int(0), n); - create_axiom(fml); - fml = m.mk_or(m.mk_not(eq1), eq2); - create_axiom(fml); - fml = m.mk_or(m.mk_not(eq2), eq1); - create_axiom(fml); - nr = n; - m_rewrite(nr); - if (nr != n) { - fml = m.mk_eq(n, nr); - create_axiom(fml); + expr_ref zero(m), emp(m); + zero = m_autil.mk_int(0); + emp = m_util.str.mk_empty(m.get_sort(x)); + literal eq1(mk_eq(zero, n, false)); + literal eq2(mk_eq(x, emp, false)); + add_axiom(mk_literal(m_autil.mk_le(zero, n))); + add_axiom(~eq1, eq2); + add_axiom(~eq2, eq1); + 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)); } } /* - check semantics of extract. + TBD: check semantics of extract. let e = extract(s, i, l) @@ -809,17 +814,73 @@ void theory_seq::add_len_axiom(expr* n) { 0 <= i < len(s) & l >= len(s) - i -> len(e) = len(s) - i 0 <= i < len(s) & 0 <= l < len(s) - i -> len(e) = l 0 <= i < len(s) & l < 0 -> len(e) = 0 - i < 0 -> e = s - i >= len(s) -> e = empty + * i < 0 -> e = s + * i >= len(s) -> e = empty */ void theory_seq::add_extract_axiom(expr* e) { - expr* s, *i, *j; - VERIFY(m_util.str.is_extract(e, s, i, j)); - expr_ref i_ge_0(m), i_le_j(m), j_lt_s(m); - - NOT_IMPLEMENTED_YET(); + expr* s, *i, *l; + VERIFY(m_util.str.is_extract(e, s, i, l)); + expr_ref x(mk_skolem(symbol("extract_prefix"), s, e), m); + expr_ref ls(m_util.str.mk_length(s), m); + expr_ref lx(m_util.str.mk_length(x), m); + expr_ref le(m_util.str.mk_length(e), m); + expr_ref ls_minus_i(m_autil.mk_sub(ls, i), m); + expr_ref xe(m_util.str.mk_concat(x, e), m); + expr_ref zero(m_autil.mk_int(0), m); + literal i_ge_0 = mk_literal(m_autil.mk_ge(i, m_autil.mk_int(0))); + literal i_le_l = mk_literal(m_autil.mk_le(i, l)); + literal i_ge_ls = mk_literal(m_autil.mk_ge(i, ls)); + literal l_ge_ls = mk_literal(m_autil.mk_ge(l, ls)); + literal l_ge_zero = mk_literal(m_autil.mk_ge(l, zero)); + + add_axiom(~i_ge_0, i_ge_ls, mk_literal(m_util.str.mk_prefix(xe, s))); + add_axiom(~i_ge_0, i_ge_ls, mk_eq(lx, i, false)); + add_axiom(~i_ge_0, i_ge_ls, ~l_ge_ls, mk_eq(le, ls_minus_i, false)); + add_axiom(~i_ge_0, i_ge_ls, l_ge_zero, mk_eq(le, zero, false)); +} + +/* + let e = at(s, i) + + 0 <= i < len(s) -> s = xey & len(x) = i & len(e) = 1 + +*/ +void theory_seq::add_at_axiom(expr* e) { + expr* s, *i; + VERIFY(m_util.str.is_at(e, s, i)); + expr_ref x(m), y(m), lx(m), le(m), xey(m), one(m), len_e(m), len_x(m); + x = mk_skolem(symbol("at_left"), s); + y = mk_skolem(symbol("at_right"), s); + xey = m_util.str.mk_concat(x, e, y); + one = m_autil.mk_int(1); + len_e = m_util.str.mk_length(e); + len_x = m_util.str.mk_length(x); + + literal i_ge_0 = mk_literal(m_autil.mk_ge(i, m_autil.mk_int(0))); + literal i_ge_len_s = mk_literal(m_autil.mk_ge(i, m_util.str.mk_length(s))); + + add_axiom(~i_ge_0, i_ge_len_s, mk_eq(s, xey, false)); + add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e, false)); + add_axiom(~i_ge_0, i_ge_len_s, mk_eq(i, len_x, false)); +} + + +literal theory_seq::mk_literal(expr* _e) { + expr_ref e(_e, m); + context& ctx = get_context(); + ctx.internalize(e, false); + return ctx.get_literal(e); +} + +void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) { + literal_vector lits; + if (l1 != null_literal) lits.push_back(l1); + if (l2 != null_literal) lits.push_back(l2); + if (l3 != null_literal) lits.push_back(l3); + if (l4 != null_literal) lits.push_back(l4); + get_context().mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); } void theory_seq::assert_axiom(expr_ref& e) { @@ -967,5 +1028,17 @@ void theory_seq::relevant_eh(app* n) { if (m_util.str.is_length(n)) { add_len_axiom(n); } + else if (m_util.str.is_index(n)) { + add_indexof_axiom(n); + } + else if (m_util.str.is_replace(n)) { + add_replace_axiom(n); + } + else if (m_util.str.is_extract(n)) { + add_extract_axiom(n); + } + else if (m_util.str.is_at(n)) { + add_at_axiom(n); + } } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 87a6a2dc6..fe58cfeb4 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -24,6 +24,7 @@ Revision History: #include "theory_seq_empty.h" #include "th_rewriter.h" #include "union_find.h" +#include "ast_trail.h" namespace smt { @@ -101,6 +102,7 @@ namespace smt { vector m_lhs, m_rhs; // persistent sets of equalities. vector m_deps; // persistent sets of dependencies. + 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. @@ -168,15 +170,19 @@ namespace smt { void assert_axiom(expr_ref& e); void create_axiom(expr_ref& e); + void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal); + void add_indexof_axiom(expr* e); void add_replace_axiom(expr* e); void add_extract_axiom(expr* e); void add_len_concat_axiom(expr* c); void add_len_axiom(expr* n); + void add_at_axiom(expr* n); + literal mk_literal(expr* n); + void tightest_prefix(expr* s, expr* x, literal lit); void new_eq_len_concat(enode* n1, enode* n2); - expr_ref tightest_prefix(expr* s, expr* x); expr_ref canonize(expr* e, enode_pair_dependency*& eqs); expr_ref expand(expr* e, enode_pair_dependency*& eqs); void add_dependency(enode_pair_dependency*& dep, enode* a, enode* b); From f9ca66d90b519346b7a17c83863984737773c670 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Dec 2015 23:19:16 -0800 Subject: [PATCH 04/10] seq Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 6 ++ src/smt/theory_seq.cpp | 97 ++++++++++++++++++------------- src/smt/theory_seq.h | 7 +-- 3 files changed, 66 insertions(+), 44 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 96e11283e..564074ea8 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -154,6 +154,12 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) { if (m_util.str.is_string(m_es[i], b)) { len += b.length(); } + else if (m_util.str.is_unit(m_es[i])) { + len += 1; + } + else if (m_util.str.is_empty(m_es[i])) { + // skip + } else { m_es[j] = m_es[i]; ++j; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index a9d6925fd..2ed9ea1c7 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -655,16 +655,34 @@ void theory_seq::propagate() { while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) { expr_ref e(m); e = m_axioms[m_axioms_head].get(); - assert_axiom(e); + deque_axiom(e); ++m_axioms_head; } } -void theory_seq::create_axiom(expr_ref& e) { +void theory_seq::enque_axiom(expr* e) { m_trail_stack.push(push_back_vector(m_axioms)); m_axioms.push_back(e); } +void theory_seq::deque_axiom(expr* n) { + if (m_util.str.is_length(n)) { + add_length_axiom(n); + } + else if (m_util.str.is_index(n)) { + add_indexof_axiom(n); + } + else if (m_util.str.is_replace(n)) { + add_replace_axiom(n); + } + else if (m_util.str.is_extract(n)) { + add_extract_axiom(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, @@ -694,10 +712,13 @@ void theory_seq::new_eq_len_concat(enode* n1, enode* n2) { } enode* start2 = n2; do { - if (m_util.str.is_concat(n2->get_owner())) { - expr_ref ln(m); - ln = m_util.str.mk_length(n2->get_owner()); - add_len_axiom(ln); + expr* o = n2->get_owner(); + if (m_util.str.is_concat(o) || + m_util.str.is_unit(o) || + m_util.str.is_string(o) || + m_util.str.is_empty(o)) { + expr_ref ln(m_util.str.mk_length(o), m); + enque_axiom(ln); } n2 = n2->get_next(); } @@ -786,23 +807,37 @@ void theory_seq::add_replace_axiom(expr* r) { x = "" => len(x) = 0 len(x) = rewrite(len(x)) */ -void theory_seq::add_len_axiom(expr* n) { +void theory_seq::add_length_axiom(expr* n) { expr* x, *a, *b; VERIFY(m_util.str.is_length(n, x)); - expr_ref zero(m), emp(m); + expr_ref zero(m), one(m), emp(m); zero = m_autil.mk_int(0); - emp = m_util.str.mk_empty(m.get_sort(x)); - literal eq1(mk_eq(zero, n, false)); - literal eq2(mk_eq(x, emp, false)); - add_axiom(mk_literal(m_autil.mk_le(zero, n))); - add_axiom(~eq1, eq2); - add_axiom(~eq2, eq1); - if (m_util.str.is_concat(n, a, b)) { + 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)); + literal eq1(mk_eq(zero, n, false)); + literal eq2(mk_eq(x, emp, false)); + add_axiom(mk_literal(m_autil.mk_ge(n, zero))); + add_axiom(~eq1, eq2); + add_axiom(~eq2, eq1); + } } /* @@ -883,15 +918,6 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) { get_context().mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); } -void theory_seq::assert_axiom(expr_ref& e) { - context & ctx = get_context(); - 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(symbol const& name, expr* e1, expr* e2) { expr* es[2] = { e1, e2 }; @@ -1024,21 +1050,12 @@ void theory_seq::restart_eh() { #endif } -void theory_seq::relevant_eh(app* n) { - if (m_util.str.is_length(n)) { - add_len_axiom(n); - } - else if (m_util.str.is_index(n)) { - add_indexof_axiom(n); - } - else if (m_util.str.is_replace(n)) { - add_replace_axiom(n); - } - else if (m_util.str.is_extract(n)) { - add_extract_axiom(n); - } - else if (m_util.str.is_at(n)) { - add_at_axiom(n); +void theory_seq::relevant_eh(app* n) { + if (m_util.str.is_length(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)) { + enque_axiom(n); } } - diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index fe58cfeb4..b5f8ac476 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -168,15 +168,14 @@ namespace smt { bool is_left_select(expr* a, expr*& b); bool is_right_select(expr* a, expr*& b); - void assert_axiom(expr_ref& e); - void create_axiom(expr_ref& e); + void enque_axiom(expr* e); + void deque_axiom(expr* e); void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal); void add_indexof_axiom(expr* e); void add_replace_axiom(expr* e); void add_extract_axiom(expr* e); - void add_len_concat_axiom(expr* c); - void add_len_axiom(expr* n); + void add_length_axiom(expr* n); void add_at_axiom(expr* n); literal mk_literal(expr* n); void tightest_prefix(expr* s, expr* x, literal lit); From d81186eacae24b522851d1a59b65a04b39728447 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Dec 2015 01:36:17 -0800 Subject: [PATCH 05/10] seq Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 10 ++++-- src/smt/theory_seq.cpp | 68 ++++++++++++++++++++----------------- src/smt/theory_seq.h | 19 +++++++---- 3 files changed, 56 insertions(+), 41 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 5639356cc..7ddd6ecac 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -90,6 +90,7 @@ void seq_decl_plugin::match_left_assoc(psig& sig, unsigned dsz, sort *const* dom } bool is_match = true; for (unsigned i = 0; is_match && i < dsz; ++i) { + SASSERT(dom[i]); is_match = match(binding, dom[i], sig.m_dom[0].get()); } if (range && is_match) { @@ -102,6 +103,7 @@ void seq_decl_plugin::match_left_assoc(psig& sig, unsigned dsz, sort *const* dom m.raise_exception(strm.str().c_str()); } range_out = apply_binding(binding, sig.m_range); + SASSERT(range_out); TRACE("seq_verbose", tout << mk_pp(range_out, m) << "\n";); } @@ -134,6 +136,7 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran m.raise_exception(strm.str().c_str()); } range_out = apply_binding(binding, sig.m_range); + SASSERT(range_out); } sort* seq_decl_plugin::apply_binding(ptr_vector const& binding, sort* s) { @@ -195,7 +198,7 @@ void seq_decl_plugin::init() { m_sigs[OP_SEQ_SUFFIX] = alloc(psig, m, "seq.suffixof", 1, 2, seqAseqA, boolT); m_sigs[OP_SEQ_CONTAINS] = alloc(psig, m, "seq.contains", 1, 2, seqAseqA, boolT); m_sigs[OP_SEQ_EXTRACT] = alloc(psig, m, "seq.extract", 1, 3, seqAint2T, seqA); - m_sigs[OP_SEQ_REPLACE] = alloc(psig, m, "seq.replace", 1, 3, seq3A, strT); + m_sigs[OP_SEQ_REPLACE] = alloc(psig, m, "seq.replace", 1, 3, seq3A, seqA); m_sigs[OP_SEQ_INDEX] = alloc(psig, m, "seq.indexof", 1, 3, seq2AintT, intT); m_sigs[OP_SEQ_AT] = alloc(psig, m, "seq.at", 1, 2, seqAintT, seqA); m_sigs[OP_SEQ_LENGTH] = alloc(psig, m, "seq.len", 1, 1, &seqA, intT); @@ -226,7 +229,7 @@ void seq_decl_plugin::init() { m_sigs[_OP_STRING_SUFFIX] = alloc(psig, m, "str.suffixof", 0, 2, str2T, boolT); m_sigs[_OP_STRING_IN_REGEXP] = alloc(psig, m, "str.in.re", 0, 2, strTreT, boolT); m_sigs[_OP_STRING_TO_REGEXP] = alloc(psig, m, "str.to.re", 0, 1, &strT, reT); - m_sigs[_OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, boolT); + m_sigs[_OP_STRING_SUBSTR] = alloc(psig, m, "str.substr", 0, 3, strTint2T, strT); } void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { @@ -409,7 +412,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); case _OP_SEQ_SKOLEM: - return m.mk_func_decl(symbol("seq.skolem"), arity, domain, rng, func_decl_info(m_family_id, k)); + return m.mk_func_decl(symbol("seq.skolem"), arity, domain, range, func_decl_info(m_family_id, k)); default: UNREACHABLE(); return 0; @@ -444,6 +447,7 @@ bool seq_decl_plugin::is_value(app* e) const { } app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) { + SASSERT(range); parameter param(name); func_decl* f = m.mk_func_decl(get_family_id(), _OP_SEQ_SKOLEM, 1, ¶m, n, args, range); return m.mk_app(f, n, args); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 2ed9ea1c7..fe6a0b12b 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -269,9 +269,7 @@ bool theory_seq::assume_equality(expr* l, expr* r) { else { SASSERT(ctx.e_internalized(l)); if (!ctx.e_internalized(r)) ctx.internalize(r, false); - enode* n1 = ctx.get_enode(l); - enode* n2 = ctx.get_enode(r); - ctx.assume_eq(n1, n2); + ctx.assume_eq(ctx.get_enode(l), ctx.get_enode(r)); } return true; } @@ -398,7 +396,12 @@ bool theory_seq::occurs(expr* a, expr* b) { } bool theory_seq::is_var(expr* a) { - return is_uninterp(a) || m_util.is_skolem(a); + return + m_util.is_seq(a) && + !m_util.str.is_concat(a) && + !m_util.str.is_empty(a) && + !m_util.str.is_string(a) && + !m_util.str.is_unit(a); } bool theory_seq::is_left_select(expr* a, expr*& b) { @@ -411,15 +414,12 @@ bool theory_seq::is_right_select(expr* a, expr*& b) { to_app(a)->get_decl()->get_parameter(0).get_symbol() == m_right_sym && (b = to_app(a)->get_arg(0), true); } - void theory_seq::add_solution(expr* l, expr* r, enode_pair_dependency* deps) { context& ctx = get_context(); m_rep.update(l, r, deps); // TBD: skip new equalities for non-internalized terms. if (ctx.e_internalized(l) && ctx.e_internalized(r)) { - enode* n1 = ctx.get_enode(l); - enode* n2 = ctx.get_enode(r); - propagate_eq(deps, n1, n2); + propagate_eq(deps, ctx.get_enode(l), ctx.get_enode(r)); } } @@ -467,8 +467,6 @@ bool theory_seq::simplify_and_solve_eqs() { return change; } - - bool theory_seq::internalize_atom(app* a, bool) { return internalize_term(a); } @@ -484,17 +482,16 @@ bool theory_seq::internalize_term(app* term) { mk_var(ctx.get_enode(arg)); } } - enode* e = 0; - if (ctx.e_internalized(term)) { - e = ctx.get_enode(term); - } 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 { - if (!e) { + enode* e = 0; + if (ctx.e_internalized(term)) { + e = ctx.get_enode(term); + } + else { e = ctx.mk_enode(term, false, m.is_bool(term), true); } mk_var(e); @@ -580,8 +577,8 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { void theory_seq::set_incomplete(app* term) { - TRACE("seq", tout << "No support for: " << mk_pp(term, m) << "\n";); if (!m_incomplete) { + TRACE("seq", tout << "Incomplete operator: " << mk_pp(term, m) << "\n";); m_trail_stack.push(value_trail(m_incomplete)); m_incomplete = true; } @@ -691,6 +688,9 @@ void theory_seq::deque_axiom(expr* n) { */ void theory_seq::new_eq_len_concat(enode* n1, enode* n2) { context& ctx = get_context(); + if (n1->get_root() == n2->get_root()) { + return; + } SASSERT(n1->get_root() != n2->get_root()); if (!m_util.is_seq(n1->get_owner())) { return; @@ -713,10 +713,7 @@ void theory_seq::new_eq_len_concat(enode* n1, enode* n2) { enode* start2 = n2; do { expr* o = n2->get_owner(); - if (m_util.str.is_concat(o) || - m_util.str.is_unit(o) || - m_util.str.is_string(o) || - m_util.str.is_empty(o)) { + if (!is_var(o)) { expr_ref ln(m_util.str.mk_length(o), m); enque_axiom(ln); } @@ -790,8 +787,8 @@ void theory_seq::add_replace_axiom(expr* r) { VERIFY(m_util.str.is_replace(r, a, s, t)); expr_ref x = mk_skolem(m_contains_left_sym, s, a); expr_ref y = mk_skolem(m_contains_right_sym, s, a); - expr_ref xsy(m_util.str.mk_concat(x, t, y), m); - expr_ref xty(m_util.str.mk_concat(x, s, y), m); + expr_ref xty(m_util.str.mk_concat(x, t, y), m); + expr_ref xsy(m_util.str.mk_concat(x, s, y), m); literal cnt = mk_literal(m_util.str.mk_contains(s, a)); add_axiom(cnt, mk_eq(r, a, false)); add_axiom(~cnt, mk_eq(a, xsy, false)); @@ -840,6 +837,10 @@ void theory_seq::add_length_axiom(expr* n) { } } +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)); +} + /* TBD: check semantics of extract. @@ -860,14 +861,14 @@ void theory_seq::add_extract_axiom(expr* e) { expr_ref ls(m_util.str.mk_length(s), m); expr_ref lx(m_util.str.mk_length(x), m); expr_ref le(m_util.str.mk_length(e), m); - expr_ref ls_minus_i(m_autil.mk_sub(ls, i), m); + expr_ref ls_minus_i(mk_sub(ls, i), m); expr_ref xe(m_util.str.mk_concat(x, e), m); expr_ref zero(m_autil.mk_int(0), m); - literal i_ge_0 = mk_literal(m_autil.mk_ge(i, m_autil.mk_int(0))); - literal i_le_l = mk_literal(m_autil.mk_le(i, l)); - literal i_ge_ls = mk_literal(m_autil.mk_ge(i, ls)); - literal l_ge_ls = mk_literal(m_autil.mk_ge(l, ls)); + literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero)); + literal i_le_l = mk_literal(m_autil.mk_le(mk_sub(i, l), zero)); + literal i_ge_ls = mk_literal(m_autil.mk_ge(mk_sub(i, ls), zero)); + literal l_ge_ls = mk_literal(m_autil.mk_ge(mk_sub(l, ls), zero)); literal l_ge_zero = mk_literal(m_autil.mk_ge(l, zero)); add_axiom(~i_ge_0, i_ge_ls, mk_literal(m_util.str.mk_prefix(xe, s))); @@ -885,16 +886,17 @@ void theory_seq::add_extract_axiom(expr* e) { void theory_seq::add_at_axiom(expr* e) { expr* s, *i; VERIFY(m_util.str.is_at(e, s, i)); - expr_ref x(m), y(m), lx(m), le(m), xey(m), one(m), len_e(m), len_x(m); + expr_ref x(m), y(m), lx(m), le(m), xey(m), zero(m), one(m), len_e(m), len_x(m); x = mk_skolem(symbol("at_left"), s); y = mk_skolem(symbol("at_right"), s); xey = m_util.str.mk_concat(x, e, y); + zero = m_autil.mk_int(0); one = m_autil.mk_int(1); len_e = m_util.str.mk_length(e); len_x = m_util.str.mk_length(x); - literal i_ge_0 = mk_literal(m_autil.mk_ge(i, m_autil.mk_int(0))); - literal i_ge_len_s = mk_literal(m_autil.mk_ge(i, m_util.str.mk_length(s))); + literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero)); + literal i_ge_len_s = mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero)); add_axiom(~i_ge_0, i_ge_len_s, mk_eq(s, xey, false)); add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e, false)); @@ -910,12 +912,14 @@ literal theory_seq::mk_literal(expr* _e) { } void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) { + context& ctx = get_context(); literal_vector lits; if (l1 != null_literal) lits.push_back(l1); if (l2 != null_literal) lits.push_back(l2); if (l3 != null_literal) lits.push_back(l3); if (l4 != null_literal) lits.push_back(l4); - get_context().mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); + ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index b5f8ac476..49a906e62 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -143,7 +143,8 @@ namespace smt { virtual void collect_statistics(::statistics & st) const; virtual model_value_proc * mk_value(enode * n, model_generator & mg); virtual void init_model(model_generator & mg); - + + // final check bool check_ineqs(); // check if inequalities are violated. bool simplify_and_solve_eqs(); // solve unitary equalities bool branch_variable(); // branch on a variable @@ -154,6 +155,8 @@ namespace smt { bool simplify_eq(expr* l, expr* r, enode_pair_dependency* dep); bool solve_unit_eq(expr* l, expr* r, enode_pair_dependency* dep); bool solve_basic_eqs(); + + // asserting consequences void propagate_lit(enode_pair_dependency* dep, literal lit); void propagate_eq(enode_pair_dependency* dep, enode* n1, enode* n2); void propagate_eq(bool_var v, expr* e1, expr* e2); @@ -162,16 +165,21 @@ namespace smt { bool find_branch_candidate(expr* l, ptr_vector const& rs); bool assume_equality(expr* l, expr* r); + // variable solving utilities bool occurs(expr* a, expr* b); bool is_var(expr* b); void add_solution(expr* l, expr* r, enode_pair_dependency* dep); bool is_left_select(expr* a, expr*& b); bool is_right_select(expr* a, expr*& b); + expr_ref canonize(expr* e, enode_pair_dependency*& eqs); + expr_ref expand(expr* e, enode_pair_dependency*& eqs); + void add_dependency(enode_pair_dependency*& dep, enode* a, enode* b); + + // terms whose meaning are encoded using axioms. void enque_axiom(expr* e); void deque_axiom(expr* e); - void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal); - + void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal); void add_indexof_axiom(expr* e); void add_replace_axiom(expr* e); void add_extract_axiom(expr* e); @@ -179,17 +187,16 @@ namespace smt { void add_at_axiom(expr* n); literal mk_literal(expr* n); void tightest_prefix(expr* s, expr* x, literal lit); + expr* mk_sub(expr* a, expr* b); void new_eq_len_concat(enode* n1, enode* n2); - expr_ref canonize(expr* e, enode_pair_dependency*& eqs); - expr_ref expand(expr* e, enode_pair_dependency*& eqs); - void add_dependency(enode_pair_dependency*& dep, enode* a, enode* b); expr_ref mk_skolem(symbol const& s, expr* e1, expr* e2 = 0); void set_incomplete(app* term); + // diagnostics void display_equations(std::ostream& out) const; void display_deps(std::ostream& out, enode_pair_dependency* deps) const; public: From 30580a012af8ab26ed2e09786d6646a104311a61 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Dec 2015 02:38:56 -0800 Subject: [PATCH 06/10] seq Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 4 +++ src/ast/seq_decl_plugin.h | 2 +- src/smt/theory_seq.cpp | 48 ++++++++++++++++++++----------- 3 files changed, 36 insertions(+), 18 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 564074ea8..a0e1bb955 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -72,6 +72,10 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 2); return mk_seq_suffix(args[0], args[1], result); case OP_SEQ_INDEX: + if (num_args == 2) { + expr_ref arg3(m_autil.mk_int(0), m()); + return mk_seq_index(args[0], args[1], arg3, result); + } SASSERT(num_args == 3); return mk_seq_index(args[0], args[1], args[2], result); case OP_SEQ_REPLACE: diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 33091ebd2..208a29c78 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -220,7 +220,7 @@ public: MATCH_TERNARY(is_extract); MATCH_BINARY(is_contains); MATCH_BINARY(is_at); - MATCH_BINARY(is_index); + MATCH_TERNARY(is_index); MATCH_TERNARY(is_replace); MATCH_BINARY(is_prefix); MATCH_BINARY(is_suffix); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index fe6a0b12b..555cefff7 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -745,33 +745,47 @@ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit) { } /* - let i = Index(s, t) + let i = Index(s, t, offset) - (!contains(s, t) -> i = -1) - (s = empty -> i = 0) - (contains(s, t) & s != empty -> t = xsy) - (contains(s, t) -> tightest_prefix(s, x)) + if offset = 0: + (!contains(s, t) -> i = -1) + (s = empty -> i = 0) + (contains(s, t) & s != empty -> t = xsy) + (contains(s, t) -> 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: + ? optional lemmas: (len(s) > len(t) -> i = -1) (len(s) <= len(t) -> i <= len(t)-len(s)) */ void theory_seq::add_indexof_axiom(expr* i) { - expr* s, *t; - VERIFY(m_util.str.is_index(i, s, t)); - expr_ref fml(m), emp(m), minus_one(m), zero(m), xsy(m); - expr_ref x = mk_skolem(m_contains_left_sym, s, t); - expr_ref y = mk_skolem(m_contains_right_sym, s, t); + expr* s, *t, *offset; + rational r; + VERIFY(m_util.str.is_index(i, s, t, offset)); + expr_ref emp(m), minus_one(m), zero(m), xsy(m); minus_one = m_autil.mk_int(-1); zero = m_autil.mk_int(0); emp = m_util.str.mk_empty(m.get_sort(s)); - xsy = m_util.str.mk_concat(x,s,y); - literal cnt = mk_literal(m_util.str.mk_contains(s, t)); - 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); + if (m_autil.is_numeral(offset, r) && r.is_zero()) { + expr_ref x = mk_skolem(m_contains_left_sym, s, t); + expr_ref y = mk_skolem(m_contains_right_sym, s, t); + xsy = m_util.str.mk_concat(x,s,y); + literal cnt = mk_literal(m_util.str.mk_contains(s, t)); + 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); + } + else { + // TBD + } } /* From 5eb23e1e7a1b0ad2883635ef572c688667cfdd50 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Dec 2015 19:20:16 -0800 Subject: [PATCH 07/10] seq Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 157 ++++++++++++++++++++++-------- src/ast/rewriter/seq_rewriter.h | 7 +- src/ast/seq_decl_plugin.cpp | 84 +++++++++------- src/ast/seq_decl_plugin.h | 13 +++ src/cmd_context/basic_cmds.cpp | 6 +- src/cmd_context/check_logic.cpp | 5 + src/cmd_context/cmd_context.cpp | 10 +- src/smt/smt_theory.h | 2 +- src/smt/theory_arith_pp.h | 1 + src/smt/theory_array.cpp | 3 +- src/smt/theory_bv.cpp | 3 +- src/smt/theory_datatype.cpp | 3 +- src/smt/theory_dl.cpp | 3 + src/smt/theory_fpa.cpp | 12 ++- src/smt/theory_seq.cpp | 112 ++++++++++++--------- src/smt/theory_seq.h | 2 + src/smt/theory_seq_empty.h | 5 + 17 files changed, 287 insertions(+), 141 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index a0e1bb955..c94608457 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -74,7 +74,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_SEQ_INDEX: if (num_args == 2) { expr_ref arg3(m_autil.mk_int(0), m()); - return mk_seq_index(args[0], args[1], arg3, result); + result = m_util.str.mk_index(args[0], args[1], arg3); + return BR_REWRITE1; } SASSERT(num_args == 3); return mk_seq_index(args[0], args[1], args[2], result); @@ -202,19 +203,19 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) { std::string c, d; if (m_util.str.is_string(a, c) && m_util.str.is_string(b, d)) { - result = m().mk_bool_val(0 != strstr(d.c_str(), c.c_str())); + result = m().mk_bool_val(0 != strstr(c.c_str(), d.c_str())); return BR_DONE; } - // check if subsequence of a is in b. + // check if subsequence of b is in a. 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; + for (unsigned i = 0; !found && i < as.size(); ++i) { + if (bs.size() > as.size() - i) break; unsigned j = 0; - for (; j < as.size() && as[j] == bs[i+j]; ++j) {}; - found = j == as.size(); + for (; j < bs.size() && as[j] == bs[i+j]; ++j) {}; + found = j == bs.size(); } if (found) { result = m().mk_true(); @@ -260,7 +261,7 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result return BR_DONE; } - if (m_util.str.is_empty(b)) { + if (m_util.str.is_empty(b) && m_autil.is_numeral(c, r) && r.is_zero()) { result = c; return BR_DONE; } @@ -380,6 +381,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) { return BR_REWRITE3; } if (i > 0) { + SASSERT(i < as.size() && i < bs.size()); 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); @@ -657,54 +659,127 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve } bool is_sat; - if (!change) { - if (is_subsequence(m_lhs.size(), m_lhs.c_ptr(), m_rhs.size(), m_rhs.c_ptr(), lhs, rhs, is_sat)) { - return is_sat; - } + unsigned szl = m_lhs.size() - head1, szr = m_rhs.size() - head2; + expr* const* ls = m_lhs.c_ptr() + head1, * const*rs = m_rhs.c_ptr() + head2; + if (length_constrained(szl, ls, szr, rs, lhs, rhs, is_sat)) { + return is_sat; + } + if (is_subsequence(szl, ls, szr, rs, lhs, rhs, is_sat)) { + return is_sat; + } + + if (szl == 0 && szr == 0) { + return true; + } + else 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 { // could solve if either side is fixed size. - SASSERT(head1 < m_lhs.size() && head2 < m_rhs.size()); - if (is_subsequence(m_lhs.size() - head1, m_lhs.c_ptr() + head1, - m_rhs.size() - head2, m_rhs.c_ptr() + head2, lhs, rhs, is_sat)) { - return is_sat; - } + else { + // could solve if either side is fixed size. + SASSERT(szl > 0 && szr > 0); - 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)); + lhs.push_back(m_util.str.mk_concat(szl, ls)); + rhs.push_back(m_util.str.mk_concat(szr, rs)); } return true; } -bool seq_rewriter::set_empty(unsigned sz, expr* const* es, expr_ref_vector& lhs, expr_ref_vector& rhs) { +expr* seq_rewriter::concat_non_empty(unsigned n, expr* const* as) { + SASSERT(n > 0); + ptr_vector bs; + for (unsigned i = 0; i < n; ++i) { + if (m_util.str.is_unit(as[i]) || + m_util.str.is_string(as[i])) { + bs.push_back(as[i]); + } + } + if (bs.empty()) { + return m_util.str.mk_empty(m().get_sort(as[0])); + } + else { + return m_util.str.mk_concat(bs.size(), bs.c_ptr()); + } +} + +bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, 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 (all) return false; } - if (m_util.str.is_empty(es[i])) { + else if (m_util.str.is_empty(es[i])) { continue; } - if (m_util.str.is_string(es[i], s)) { - SASSERT(s.length() > 0); - return false; + else if (m_util.str.is_string(es[i], s)) { + if (all) { + SASSERT(s.length() > 0); + return false; + } + } + else { + lhs.push_back(m_util.str.mk_empty(m().get_sort(es[i]))); + rhs.push_back(es[i]); } - lhs.push_back(m_util.str.mk_empty(m().get_sort(es[i]))); - rhs.push_back(es[i]); } return true; } +bool seq_rewriter::min_length(unsigned n, expr* const* es, size_t& len) { + std::string s; + bool bounded = true; + len = 0; + for (unsigned i = 0; i < n; ++i) { + if (m_util.str.is_unit(es[i])) { + ++len; + } + else if (m_util.str.is_empty(es[i])) { + continue; + } + else if (m_util.str.is_string(es[i], s)) { + len += s.length(); + } + else { + bounded = false; + } + } + return bounded; +} + +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; + bool bounded1 = min_length(szl, l, len1); + bool bounded2 = min_length(szr, r, len2); + if (bounded1 && len1 < len2) { + is_sat = false; + return true; + } + if (bounded2 && len2 < len1) { + is_sat = false; + return true; + } + if (bounded1 && len1 == len2 && len1 > 0) { + is_sat = set_empty(szr, r, false, lhs, rhs); + if (is_sat) { + lhs.push_back(concat_non_empty(szl, l)); + rhs.push_back(concat_non_empty(szr, r)); + } + return true; + } + if (bounded2 && len1 == len2 && len1 > 0) { + is_sat = set_empty(szl, l, false, lhs, rhs); + if (is_sat) { + lhs.push_back(concat_non_empty(szl, l)); + rhs.push_back(concat_non_empty(szr, r)); + } + return true; + } + + return false; +} + bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, expr* const* r, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat) { is_sat = true; @@ -733,13 +808,15 @@ bool seq_rewriter::is_subsequence(unsigned szl, expr* const* l, unsigned szr, ex if (rpos.contains(j)) { rs.push_back(r[j]); } - else if (!set_empty(1, r + j, lhs, rhs)) { + else if (!set_empty(1, r + j, true, lhs, rhs)) { is_sat = false; return true; } } SASSERT(szl == rs.size()); - lhs.push_back(m_util.str.mk_concat(szl, l)); - rhs.push_back(m_util.str.mk_concat(szl, rs.c_ptr())); + if (szl > 0) { + lhs.push_back(m_util.str.mk_concat(szl, l)); + rhs.push_back(m_util.str.mk_concat(szl, rs.c_ptr())); + } return true; } diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index ec1747a4b..998b37d1a 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -53,9 +53,14 @@ 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); + bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs); bool is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& is_sat); + 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); + expr* concat_non_empty(unsigned n, expr* const* es); + public: seq_rewriter(ast_manager & m, params_ref const & p = params_ref()): m_util(m), m_autil(m) { diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 7ddd6ecac..49b1873d9 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -289,6 +289,18 @@ func_decl* seq_decl_plugin::mk_str_fun(decl_kind k, unsigned arity, sort* const* return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k_seq)); } +func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq, decl_kind k_string) { + ast_manager& m = *m_manager; + sort_ref rng(m); + if (arity == 0) { + m.raise_exception("Invalid function application. At least one argument expected"); + } + match_left_assoc(*m_sigs[k], arity, domain, range, rng); + func_decl_info info(m_family_id, k_seq); + info.set_left_associative(); + return m.mk_func_decl(m_sigs[(rng == m_string)?k_string:k_seq]->m_name, rng, rng, rng, info); +} + func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { init(); @@ -308,18 +320,21 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_RE_STAR: case OP_RE_OPTION: case OP_RE_RANGE: - case OP_RE_UNION: case OP_RE_EMPTY_SET: - case OP_RE_OF_PRED: + case OP_STRING_ITOS: + case OP_STRING_STOI: + case OP_REGEXP_LOOP: match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); + case OP_RE_LOOP: match(*m_sigs[k], arity, domain, range, rng); if (num_parameters != 2 || !parameters[0].is_int() || !parameters[1].is_int()) { m.raise_exception("Expecting two numeral parameters to function re-loop"); } return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters)); + case OP_STRING_CONST: if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) { m.raise_exception("invalid string declaration"); @@ -327,33 +342,17 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return m.mk_const_decl(m_stringc_sym, m_string, func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters)); - case OP_SEQ_CONCAT: { - if (arity == 0) { - m.raise_exception("invalid concatenation. At least one argument expected"); - } - match_left_assoc(*m_sigs[k], arity, domain, range, rng); - func_decl_info info(m_family_id, k); - info.set_left_associative(); - return m.mk_func_decl(m_sigs[(rng == m_string)?_OP_STRING_CONCAT:k]->m_name, rng, rng, rng, info); - } - case OP_RE_CONCAT: { - if (arity == 0) { - m.raise_exception("invalid concatenation. At least one argument expected"); - } - match_left_assoc(*m_sigs[k], arity, domain, range, rng); - func_decl_info info(m_family_id, k); - info.set_left_associative(); - return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info); - } - case _OP_STRING_CONCAT: { - if (arity == 0) { - m.raise_exception("invalid concatenation. At least one argument expected"); - } - match_left_assoc(*m_sigs[k], arity, domain, range, rng); - func_decl_info info(m_family_id, OP_SEQ_CONCAT); - info.set_left_associative(); - return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info); - } + case OP_RE_UNION: + return mk_assoc_fun(k, arity, domain, range, k, k); + + case OP_RE_CONCAT: + return mk_assoc_fun(k, arity, domain, range, k, k); + + case OP_SEQ_CONCAT: + return mk_assoc_fun(k, arity, domain, range, k, _OP_STRING_CONCAT); + + case _OP_STRING_CONCAT: + return mk_assoc_fun(k, arity, domain, range, OP_SEQ_CONCAT, k); case OP_SEQ_REPLACE: return mk_seq_fun(k, arity, domain, range, _OP_STRING_STRREPL); @@ -361,8 +360,20 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return mk_str_fun(k, arity, domain, range, OP_SEQ_REPLACE); case OP_SEQ_INDEX: + if (arity == 2) { + sort* dom[3] = { domain[0], domain[1], arith_util(m).mk_int() }; + sort_ref rng(m); + match(*m_sigs[k], 3, dom, range, rng); + return m.mk_func_decl(m_sigs[(dom[0] == m_string)?_OP_STRING_STRIDOF:k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); + } return mk_seq_fun(k, arity, domain, range, _OP_STRING_STRIDOF); case _OP_STRING_STRIDOF: + if (arity == 2) { + sort* dom[3] = { domain[0], domain[1], arith_util(m).mk_int() }; + sort_ref rng(m); + match(*m_sigs[k], 3, dom, range, rng); + return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, OP_SEQ_INDEX)); + } return mk_str_fun(k, arity, domain, range, OP_SEQ_INDEX); case OP_SEQ_PREFIX: @@ -405,14 +416,13 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case _OP_STRING_SUBSTR: return mk_str_fun(k, arity, domain, range, OP_SEQ_EXTRACT); - case OP_STRING_ITOS: - case OP_STRING_STOI: - case OP_REGEXP_LOOP: - match(*m_sigs[k], arity, domain, range, rng); - return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); - - case _OP_SEQ_SKOLEM: - return m.mk_func_decl(symbol("seq.skolem"), arity, domain, range, func_decl_info(m_family_id, k)); + case _OP_SEQ_SKOLEM: { + if (num_parameters != 1 || !parameters[0].is_symbol()) { + m.raise_exception("one symbol parameter expected to skolem symbol"); + } + symbol s = parameters[0].get_symbol(); + return m.mk_func_decl(s, arity, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters)); + } default: UNREACHABLE(); return 0; diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 208a29c78..7026a73cb 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -116,6 +116,7 @@ class seq_decl_plugin : public decl_plugin { func_decl* mk_seq_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string); func_decl* mk_str_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq); + func_decl* mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq); void init(); @@ -158,8 +159,10 @@ public: bool is_string(sort* s) const { return is_seq(s) && seq.is_char(s->get_parameter(0).get_ast()); } bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); } bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); } + bool is_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_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); } app* mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range); bool is_skolem(expr const* e) const { return is_app_of(e, m_fid, _OP_SEQ_SKOLEM); } @@ -186,6 +189,7 @@ public: 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); } + 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); } bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); } @@ -239,6 +243,15 @@ public: public: re(seq_util& u): m(u.m), m_fid(u.m_fid) {} + app* mk_to_re(expr* s) { return m.mk_app(m_fid, OP_SEQ_TO_RE, 1, &s); } + app* mk_in_re(expr* s, expr* r) { return m.mk_app(m_fid, OP_SEQ_IN_RE, s, r); } + app* mk_concat(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_CONCAT, r1, r2); } + app* mk_union(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_UNION, r1, r2); } + app* mk_inter(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_INTERSECT, r1, r2); } + app* mk_star(expr* r) { return m.mk_app(m_fid, OP_RE_STAR, r); } + app* mk_plus(expr* r) { return m.mk_app(m_fid, OP_RE_PLUS, r); } + app* mk_opt(expr* r) { return m.mk_app(m_fid, OP_RE_OPTION, r); } + bool is_to_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); } bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_RE_CONCAT); } bool is_union(expr const* n) const { return is_app_of(n, m_fid, OP_RE_UNION); } diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index a12e38f80..957cbef4e 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -222,8 +222,10 @@ ATOMIC_CMD(reset_assertions_cmd, "reset-assertions", "reset all asserted formula UNARY_CMD(set_logic_cmd, "set-logic", "", "set the background logic.", CPK_SYMBOL, symbol const &, if (ctx.set_logic(arg)) ctx.print_success(); - else - ctx.print_unsupported(symbol::null, m_line, m_pos); + else { + std::string msg = "ignoring unsupported logic " + arg.str(); + ctx.print_unsupported(symbol(msg.c_str()), m_line, m_pos); + } ); UNARY_CMD(pp_cmd, "display", "", "display the given term.", CPK_EXPR, expr *, { diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp index 99b0f2521..191a3ccc1 100644 --- a/src/cmd_context/check_logic.cpp +++ b/src/cmd_context/check_logic.cpp @@ -168,6 +168,11 @@ struct check_logic::imp { m_bvs = true; m_quantifiers = true; } + else if (logic == "UF_S") { + m_uf = true; + m_bvs = true; + m_quantifiers = false; + } else { m_unknown_logic = true; } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 1b5d9d470..0dbba83d6 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -576,7 +576,7 @@ bool cmd_context::logic_has_bv() const { } bool cmd_context::logic_has_seq_core(symbol const& s) const { - return s == "QF_BVRE"; + return s == "QF_BVRE" || s == "QF_S"; } bool cmd_context::logic_has_seq() const { @@ -712,13 +712,7 @@ bool cmd_context::set_logic(symbol const & s) { if (has_manager() && m_main_ctx) throw cmd_exception("logic must be set before initialization"); if (!supported_logic(s)) { - if (m_params.m_smtlib2_compliant) { - return false; - } - else { - warning_msg("unknown logic, ignoring set-logic command"); - return true; - } + return false; } m_logic = s; if (is_logic("QF_RDL") || diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index c5fb80a1e..f48d75b2e 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -315,7 +315,7 @@ namespace smt { } virtual void display(std::ostream & out) const { - out << "Theory " << static_cast(get_id()) << " does not have a display method\n"; + out << "Theory " << static_cast(get_id()) << typeid(*this).name() << " does not have a display method\n"; display_var2enode(out); } diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h index ea4581925..ec14d8374 100644 --- a/src/smt/theory_arith_pp.h +++ b/src/smt/theory_arith_pp.h @@ -48,6 +48,7 @@ namespace smt { template void theory_arith::display(std::ostream & out) const { + if (get_num_vars() == 0) return; out << "Theory arithmetic:\n"; display_vars(out); display_nl_monomials(out); diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index 2e42a7abf..7ba94d9cb 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -431,8 +431,9 @@ namespace smt { } void theory_array::display(std::ostream & out) const { - out << "Theory array:\n"; unsigned num_vars = get_num_vars(); + if (num_vars == 0) return; + out << "Theory array:\n"; for (unsigned v = 0; v < num_vars; v++) { display_var(out, v); } diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index e381e81c1..51b2c1b59 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1586,8 +1586,9 @@ namespace smt { } void theory_bv::display(std::ostream & out) const { - out << "Theory bv:\n"; unsigned num_vars = get_num_vars(); + if (num_vars == 0) return; + out << "Theory bv:\n"; for (unsigned v = 0; v < num_vars; v++) { display_var(out, v); } diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 0c5e83928..89a19da65 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -522,8 +522,9 @@ namespace smt { } void theory_datatype::display(std::ostream & out) const { - out << "Theory datatype:\n"; unsigned num_vars = get_num_vars(); + if (num_vars == 0) return; + out << "Theory datatype:\n"; for (unsigned v = 0; v < num_vars; v++) display_var(out, v); } diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index ac64db74c..588b134b7 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -194,6 +194,9 @@ namespace smt { } } + virtual void display(std::ostream & out) const { + } + private: diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 0cd803cc0..3e43cc4ce 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -921,14 +921,20 @@ namespace smt { ast_manager & m = get_manager(); context & ctx = get_context(); - out << "fpa theory variables:" << std::endl; + bool first = true; ptr_vector::const_iterator it = ctx.begin_enodes(); ptr_vector::const_iterator end = ctx.end_enodes(); for (; it != end; it++) { theory_var v = (*it)->get_th_var(get_family_id()); - if (v != -1) out << v << " -> " << - mk_ismt2_pp((*it)->get_owner(), m) << std::endl; + if (v != -1) { + if (first) out << "fpa theory variables:" << std::endl; + out << v << " -> " << + mk_ismt2_pp((*it)->get_owner(), m) << std::endl; + first = false; + } } + // if there are no fpa theory variables, was fp ever used? + if (first) return; out << "bv theory variables:" << std::endl; it = ctx.begin_enodes(); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 555cefff7..18b223eee 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -136,12 +136,12 @@ theory_seq::theory_seq(ast_manager& m): m_lhs.push_back(expr_array()); m_rhs.push_back(expr_array()); m_deps.push_back(enode_pair_dependency_array()); - m_prefix_sym = "prefix"; - m_suffix_sym = "suffix"; - m_left_sym = "left"; - m_right_sym = "right"; - m_contains_left_sym = "contains_left"; - m_contains_right_sym = "contains_right"; + m_prefix_sym = "seq.prefix.suffix"; + m_suffix_sym = "seq.suffix.prefix"; + m_left_sym = "seq.left"; + m_right_sym = "seq.right"; + m_contains_left_sym = "seq.contains.left"; + m_contains_right_sym = "seq.contains.right"; } theory_seq::~theory_seq() { @@ -261,17 +261,19 @@ bool theory_seq::find_branch_candidate(expr* l, ptr_vector const& rs) { } bool theory_seq::assume_equality(expr* l, expr* r) { - TRACE("seq", tout << mk_pp(l, m) << " = " << mk_pp(r, m) << "\n";); context& ctx = get_context(); if (m_exclude.contains(l, r)) { return false; } else { - SASSERT(ctx.e_internalized(l)); + 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.assume_eq(ctx.get_enode(l), ctx.get_enode(r)); + 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)); + return true; } - return true; } bool theory_seq::split_variable() { @@ -519,26 +521,37 @@ void theory_seq::apply_sort_cnstr(enode* n, sort* s) { } void theory_seq::display(std::ostream & out) const { - display_equations(out); + if (m.size(m_lhs.back()) == 0 && + m_ineqs.empty() && + m_rep.empty() && + m_exclude.empty()) { + return; + } + out << "Theory seq\n"; + if (m.size(m_lhs.back()) > 0) { + out << "Equations:\n"; + display_equations(out); + } if (!m_ineqs.empty()) { out << "Negative constraints:\n"; for (unsigned i = 0; i < m_ineqs.size(); ++i) { out << mk_pp(m_ineqs[i], m) << "\n"; } } - out << "Solved equations:\n"; - m_rep.display(out); - m_exclude.display(out); + if (!m_rep.empty()) { + out << "Solved equations:\n"; + m_rep.display(out); + } + if (!m_exclude.empty()) { + out << "Exclusions:\n"; + m_exclude.display(out); + } } 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(); - if (m.size(lhs) == 0) { - return; - } - out << "Equations:\n"; for (unsigned i = 0; i < m.size(lhs); ++i) { out << mk_pp(m.get(lhs, i), m) << " = " << mk_pp(m.get(rhs, i), m) << " <-\n"; display_deps(out, m_dam.get(deps, i)); @@ -585,6 +598,10 @@ void theory_seq::set_incomplete(app* term) { } theory_var theory_seq::mk_var(enode* n) { + if (!m_util.is_seq(n->get_owner()) || + !m_util.is_re(n->get_owner())) { + return null_theory_var; + } if (is_attached_to_var(n)) { return n->get_th_var(get_id()); } @@ -658,6 +675,7 @@ void theory_seq::propagate() { } void theory_seq::enque_axiom(expr* e) { + TRACE("seq", tout << "add axioms for: " << mk_pp(e, m) << "\n";); m_trail_stack.push(push_back_vector(m_axioms)); m_axioms.push_back(e); } @@ -732,8 +750,8 @@ void theory_seq::new_eq_len_concat(enode* n1, enode* n2) { lit or s = "" or !prefix(s, x*s1) */ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit) { - expr_ref s1 = mk_skolem(symbol("first"), s); - expr_ref c = mk_skolem(symbol("last"), s); + 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); expr_ref lc(m_util.str.mk_length(c), m); expr_ref one(m_autil.mk_int(1), m); @@ -745,13 +763,13 @@ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit) { } /* - let i = Index(s, t, offset) + let i = Index(t, s, offset) if offset = 0: - (!contains(s, t) -> i = -1) + (!contains(t, s) -> i = -1) (s = empty -> i = 0) - (contains(s, t) & s != empty -> t = xsy) - (contains(s, t) -> tightest_prefix(s, x)) + (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' @@ -767,16 +785,16 @@ void theory_seq::tightest_prefix(expr* s, expr* x, literal lit) { void theory_seq::add_indexof_axiom(expr* i) { expr* s, *t, *offset; rational r; - VERIFY(m_util.str.is_index(i, s, t, offset)); + VERIFY(m_util.str.is_index(i, t, s, offset)); expr_ref emp(m), minus_one(m), zero(m), xsy(m); 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()) { - expr_ref x = mk_skolem(m_contains_left_sym, s, t); - expr_ref y = mk_skolem(m_contains_right_sym, s, t); + 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(s, t)); + 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)); @@ -791,19 +809,19 @@ void theory_seq::add_indexof_axiom(expr* i) { /* let r = replace(a, s, t) - (contains(s, a) -> tightest_prefix(s,xs)) - (contains(s, a) -> r = xty & a = xsy) & - (!contains(s, a) -> r = a) + (contains(a, s) -> tightest_prefix(s,xs)) + (contains(a, s) -> r = xty & a = xsy) & + (!contains(a, s) -> r = a) */ void theory_seq::add_replace_axiom(expr* r) { expr* a, *s, *t; VERIFY(m_util.str.is_replace(r, a, s, t)); - expr_ref x = mk_skolem(m_contains_left_sym, s, a); - expr_ref y = mk_skolem(m_contains_right_sym, s, a); + expr_ref x = mk_skolem(m_contains_left_sym, a, s); + expr_ref y = mk_skolem(m_contains_right_sym, a, s); expr_ref xty(m_util.str.mk_concat(x, t, y), m); expr_ref xsy(m_util.str.mk_concat(x, s, y), m); - literal cnt = mk_literal(m_util.str.mk_contains(s, a)); + literal cnt = mk_literal(m_util.str.mk_contains(a ,s)); add_axiom(cnt, mk_eq(r, a, false)); add_axiom(~cnt, mk_eq(a, xsy, false)); add_axiom(~cnt, mk_eq(r, xty, false)); @@ -871,7 +889,7 @@ expr* theory_seq::mk_sub(expr* a, expr* b) { void theory_seq::add_extract_axiom(expr* e) { expr* s, *i, *l; VERIFY(m_util.str.is_extract(e, s, i, l)); - expr_ref x(mk_skolem(symbol("extract_prefix"), s, e), m); + expr_ref x(mk_skolem(symbol("seq.extract.prefix"), s, e), m); expr_ref ls(m_util.str.mk_length(s), m); expr_ref lx(m_util.str.mk_length(x), m); expr_ref le(m_util.str.mk_length(e), m); @@ -901,8 +919,8 @@ void theory_seq::add_at_axiom(expr* e) { expr* s, *i; VERIFY(m_util.str.is_at(e, s, i)); expr_ref x(m), y(m), lx(m), le(m), xey(m), zero(m), one(m), len_e(m), len_x(m); - x = mk_skolem(symbol("at_left"), s); - y = mk_skolem(symbol("at_right"), s); + x = mk_skolem(symbol("seq.at.left"), s); + y = mk_skolem(symbol("seq.at.right"), s); xey = m_util.str.mk_concat(x, e, y); zero = m_autil.mk_int(0); one = m_autil.mk_int(1); @@ -928,10 +946,10 @@ literal theory_seq::mk_literal(expr* _e) { void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4) { context& ctx = get_context(); literal_vector lits; - if (l1 != null_literal) lits.push_back(l1); - if (l2 != null_literal) lits.push_back(l2); - if (l3 != null_literal) lits.push_back(l3); - if (l4 != null_literal) lits.push_back(l4); + if (l1 != null_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); } + if (l2 != null_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); } + if (l3 != null_literal) { ctx.mark_as_relevant(l3); lits.push_back(l3); } + if (l4 != null_literal) { ctx.mark_as_relevant(l4); lits.push_back(l4); } TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); } @@ -981,11 +999,11 @@ void theory_seq::assign_eq(bool_var v, bool is_true) { else if (m_util.str.is_contains(e, e1, e2)) { expr_ref f1 = mk_skolem(m_contains_left_sym, e1, e2); expr_ref f2 = mk_skolem(m_contains_right_sym, e1, e2); - f = m_util.str.mk_concat(m_util.str.mk_concat(f1, e1), f2); - propagate_eq(v, f, e2); + f = m_util.str.mk_concat(m_util.str.mk_concat(f1, e2), f2); + propagate_eq(v, f, e1); } else if (m_util.str.is_in_re(e, e1, e2)) { - NOT_IMPLEMENTED_YET(); + // TBD } else { UNREACHABLE(); @@ -1001,8 +1019,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) { - m.push_back(m_lhs.back(), n1->get_owner()); - m.push_back(m_rhs.back(), n2->get_owner()); + 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))); new_eq_len_concat(n1, n2); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index 49a906e62..f1010f73c 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -62,6 +62,7 @@ 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) {} + bool empty() const { return m_map.empty(); } void update(expr* e, expr* r, enode_pair_dependency* d); expr* find(expr* e, enode_pair_dependency*& d); void push_scope() { m_limit.push_back(m_updates.size()); } @@ -78,6 +79,7 @@ namespace smt { public: exclusion_table(ast_manager& m): m(m), m_lhs(m), m_rhs(m) {} ~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)); diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index b1bab6c05..f391dab40 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -89,6 +89,11 @@ namespace smt { return u.str.mk_string(sym); } } + sort* seq = 0; + if (u.is_re(s, seq)) { + expr* v0 = get_fresh_value(seq); + return u.re.mk_to_re(v0); + } NOT_IMPLEMENTED_YET(); return 0; } From 58411f64e8fe27f43febd8971c94d4b3a3c05491 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Dec 2015 20:25:12 -0800 Subject: [PATCH 08/10] seq Signed-off-by: Nikolaj Bjorner --- src/cmd_context/check_logic.cpp | 12 ++++++++++-- src/cmd_context/cmd_context.cpp | 1 + src/smt/smt_context.cpp | 6 +++++- src/smt/theory_seq.cpp | 10 +++++++++- src/smt/theory_seq.h | 1 + 5 files changed, 26 insertions(+), 4 deletions(-) diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp index 191a3ccc1..733689ac9 100644 --- a/src/cmd_context/check_logic.cpp +++ b/src/cmd_context/check_logic.cpp @@ -20,6 +20,7 @@ Revision History: #include"arith_decl_plugin.h" #include"array_decl_plugin.h" #include"bv_decl_plugin.h" +#include"seq_decl_plugin.h" #include"ast_pp.h" #include"for_each_expr.h" @@ -29,6 +30,7 @@ struct check_logic::imp { arith_util m_a_util; bv_util m_bv_util; array_util m_ar_util; + seq_util m_seq_util; bool m_uf; // true if the logic supports uninterpreted functions bool m_arrays; // true if the logic supports arbitrary arrays bool m_bv_arrays; // true if the logic supports only bv arrays @@ -40,7 +42,7 @@ struct check_logic::imp { bool m_quantifiers; // true if the logic supports quantifiers bool m_unknown_logic; - imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m) { + imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m), m_seq_util(m) { reset(); } @@ -168,9 +170,12 @@ struct check_logic::imp { m_bvs = true; m_quantifiers = true; } - else if (logic == "UF_S") { + else if (logic == "QF_S") { m_uf = true; m_bvs = true; + m_ints = true; + m_arrays = true; + m_reals = true; m_quantifiers = false; } else { @@ -424,6 +429,9 @@ struct check_logic::imp { else if (m.is_builtin_family_id(fid)) { // nothing to check } + else if (fid == m_seq_util.get_family_id()) { + // nothing to check + } else { fail("logic does not support theory"); } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 0dbba83d6..3e76481d6 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -544,6 +544,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const { s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || + s == "QF_S" || s == "HORN"; } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 00971f794..0be27bc08 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -312,6 +312,8 @@ namespace smt { d.m_phase_available = true; d.m_phase = !l.sign(); TRACE("phase_selection", tout << "saving phase, is_pos: " << d.m_phase << " l: " << l << "\n";); + TRACE("relevancy", + tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(bool_var2expr(l.var())) << "\n";); if (d.is_atom() && (m_fparams.m_relevancy_lvl == 0 || (m_fparams.m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(bool_var2expr(l.var())))) m_atom_propagation_queue.push_back(l); @@ -805,8 +807,10 @@ namespace smt { void context::merge_theory_vars(enode * n2, enode * n1, eq_justification js) { enode * r2 = n2->get_root(); enode * r1 = n1->get_root(); - if (!r1->has_th_vars() && !r2->has_th_vars()) + if (!r1->has_th_vars() && !r2->has_th_vars()) { + TRACE("merge_theory_vars", tout << "Neither have theory vars #" << n1->get_owner()->get_id() << " #" << n2->get_owner()->get_id() << "\n";); return; + } theory_id from_th = null_theory_id; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 18b223eee..a402437d3 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -469,6 +469,9 @@ bool theory_seq::simplify_and_solve_eqs() { return change; } +void theory_seq::internalize_eq_eh(app * atom, bool_var v) { +} + bool theory_seq::internalize_atom(app* a, bool) { return internalize_term(a); } @@ -598,7 +601,7 @@ void theory_seq::set_incomplete(app* term) { } theory_var theory_seq::mk_var(enode* n) { - if (!m_util.is_seq(n->get_owner()) || + if (!m_util.is_seq(n->get_owner()) && !m_util.is_re(n->get_owner())) { return null_theory_var; } @@ -608,6 +611,7 @@ theory_var theory_seq::mk_var(enode* n) { else { theory_var v = theory::mk_var(n); get_context().attach_th_var(n, this, v); + get_context().mark_as_relevant(n); return v; } } @@ -1005,6 +1009,10 @@ 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 f1010f73c..28a35c564 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -128,6 +128,7 @@ namespace smt { virtual final_check_status final_check_eh(); virtual bool internalize_atom(app*, bool); virtual bool internalize_term(app*); + virtual void internalize_eq_eh(app * atom, bool_var v); 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); From 85b9bb3cc69c3d09e5444340800bb6e97c690eca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 11 Dec 2015 08:37:47 -0800 Subject: [PATCH 09/10] seq Signed-off-by: Nikolaj Bjorner --- src/ast/normal_forms/nnf.cpp | 1 + src/smt/proto_model/proto_model.cpp | 3 +++ src/smt/smt_setup.cpp | 2 +- 3 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index c3ea69e77..45f85e154 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -708,6 +708,7 @@ struct nnf::imp { } bool process_app(app * t, frame & fr) { + TRACE("nnf", tout << mk_ismt2_pp(t, m()) << "\n";); SASSERT(m().is_bool(t)); if (t->get_family_id() == m().get_basic_family_id()) { switch (static_cast(t->get_decl_kind())) { diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index 26b35f0ed..26ff0136c 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -196,6 +196,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { ptr_buffer args; expr * null = static_cast(0); todo.push_back(std::make_pair(e, null)); + expr * a; expr * expanded_a; @@ -254,6 +255,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { if (new_t.get() == 0) { // t is interpreted or model completion is disabled. m_simplifier.mk_app(f, num_args, args.c_ptr(), new_t); + TRACE("model_eval", tout << mk_pp(t, m_manager) << " -> " << new_t << "\n";); trail.push_back(new_t); if (!is_app(new_t) || to_app(new_t)->get_decl() != f) { // if the result is not of the form (f ...), then assume we must simplify it. @@ -302,6 +304,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { else { SASSERT(r1); trail.push_back(r1); + TRACE("model_eval", tout << mk_pp(a, m_manager) << "\nevaluates to: " << r1 << "\n";); expr * r2 = 0; if (!eval_cache.find(r1.get(), r2)) { todo.back().second = r1; 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() { From ee4ed1749af2f6a746dd6395b4fbedbcff405af4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 11 Dec 2015 09:09:25 -0800 Subject: [PATCH 10/10] add cancel checks in model finder, patch by Sarah Winkler Signed-off-by: Nikolaj Bjorner --- src/smt/smt_model_finder.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index e4a34d3db..08cf34e72 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -1744,7 +1744,7 @@ namespace smt { // when the quantifier is satisfied by a macro/hint, it may not be processed by the AUF solver. // in this case, the quantifier_info stores the instantiation sets. ptr_vector * m_uvar_inst_sets; - bool m_cancel; + volatile bool m_cancel; friend class quantifier_analyzer; @@ -1893,8 +1893,10 @@ namespace smt { (*it)->populate_inst_sets(m_flat_q, s, ctx); // second pass it = m_qinfo_vect.begin(); - for (; it != end; ++it) + for (; it != end; ++it) { + checkpoint(); (*it)->populate_inst_sets2(m_flat_q, s, ctx); + } } func_decl_set const & get_ng_decls() const { @@ -3593,6 +3595,10 @@ namespace smt { void model_finder::set_cancel(bool f) { m_cancel = f; m_analyzer->set_cancel(f); + obj_map::iterator it = m_q2info.begin(); + obj_map::iterator end = m_q2info.end(); + for (; it != end; ++it) + (*it).m_value->set_cancel(f); } };