diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 22156afb8..78672182a 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -240,6 +240,8 @@ public: app* mk_index(expr* a, expr* b, expr* i) { expr* es[3] = { a, b, i}; return m.mk_app(m_fid, OP_SEQ_INDEX, 3, es); } app* mk_unit(expr* u) { return m.mk_app(m_fid, OP_SEQ_UNIT, 1, &u); } app* mk_char(zstring const& s, unsigned idx); + app* mk_itos(expr* i) { return m.mk_app(m_fid, OP_STRING_ITOS, 1, &i); } + app* mk_stoi(expr* s) { return m.mk_app(m_fid, OP_STRING_STOI, 1, &s); } bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 7703f70aa..22cd6482f 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -202,6 +202,7 @@ theory_seq::theory_seq(ast_manager& m): m_exclude(m), m_axioms(m), m_axioms_head(0), + m_int_string(m), m_mg(0), m_rewrite(m), m_seq_rewrite(m), @@ -257,6 +258,11 @@ final_check_status theory_seq::final_check_eh() { TRACE("seq", tout << ">>fixed_length\n";); return FC_CONTINUE; } + if (check_int_string()) { + ++m_stats.m_int_string; + TRACE("seq", tout << ">>int_string\n";); + return FC_CONTINUE; + } if (reduce_length_eq() || branch_unit_variable() || branch_binary_variable() || branch_variable_mb() || branch_variable()) { ++m_stats.m_branch_variable; TRACE("seq", tout << ">>branch_variable\n";); @@ -2160,6 +2166,7 @@ void theory_seq::add_length(expr* e) { m_trail_stack.push(insert_obj_trail(m_length, e)); } + /* ensure that all elements in equivalence class occur under an applicatin of 'length' */ @@ -2177,6 +2184,48 @@ void theory_seq::enforce_length(enode* n) { while (n1 != n); } + +void theory_seq::add_int_string(expr* e) { + m_int_string.push_back(e); + m_trail_stack.push(push_back_vector(m_int_string)); +} + +bool theory_seq::check_int_string() { + bool change = false; + for (unsigned i = 0; i < m_int_string.size(); ++i) { + expr* e = m_int_string[i].get(), *n; + if (add_itos_axiom(e)) { + change = true; + } + else if (m_util.str.is_stoi(e, n)) { + // not (yet) handled. + // we would check that in the current proto-model + // the string at 'n', when denoting integer would map to the + // proper integer. + } + } + return change; +} + +bool theory_seq::add_itos_axiom(expr* e) { + context& ctx = get_context(); + rational val; + expr* n; + if (m_util.str.is_itos(e, n) && get_value(n, val)) { + app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m); + if (!m_itos_axioms.contains(val)) { + m_itos_axioms.insert(val); + + expr_ref n1(arith_util(m).mk_numeral(val, true), m); + add_axiom(mk_eq(m_util.str.mk_itos(n1), e1, false)); + m_trail_stack.push(insert_map(m_itos_axioms, val)); + m_trail_stack.push(push_replay(alloc(replay_axiom, m, e))); + return true; + } + } + return false; +} + void theory_seq::apply_sort_cnstr(enode* n, sort* s) { mk_var(n); } @@ -2317,6 +2366,7 @@ void theory_seq::collect_statistics(::statistics & st) const { st.update("seq add axiom", m_stats.m_add_axiom); st.update("seq extensionality", m_stats.m_extensionality); st.update("seq fixed length", m_stats.m_fixed_length); + st.update("seq int.to.str", m_stats.m_int_string); } void theory_seq::init_model(expr_ref_vector const& es) { @@ -2627,6 +2677,9 @@ void theory_seq::deque_axiom(expr* n) { else if (m_util.str.is_string(n)) { add_elim_string_axiom(n); } + else if (m_util.str.is_itos(n)) { + add_itos_axiom(n); + } } @@ -2890,6 +2943,14 @@ static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) { } } +bool theory_seq::get_value(expr* e, rational& val) const { + context& ctx = get_context(); + theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e); + expr_ref _val(m); + if (!tha || !tha->get_value(ctx.get_enode(e), _val)) return false; + return m_autil.is_numeral(_val, val) && val.is_int(); +} + bool theory_seq::lower_bound(expr* _e, rational& lo) const { context& ctx = get_context(); expr_ref e(m_util.str.mk_length(_e), m); @@ -3525,6 +3586,11 @@ void theory_seq::relevant_eh(app* n) { enque_axiom(n); } + if (m_util.str.is_itos(n) || + m_util.str.is_stoi(n)) { + add_int_string(n); + } + expr* arg; if (m_util.str.is_length(n, arg) && !has_length(arg)) { enforce_length(get_context().get_enode(arg)); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index fc37a8f06..4107f3d05 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -287,7 +287,10 @@ namespace smt { unsigned m_extensionality; unsigned m_fixed_length; unsigned m_propagate_contains; + unsigned m_int_string; }; + typedef hashtable rational_set; + ast_manager& m; dependency_manager m_dm; solution_map m_rep; // unification representative. @@ -303,6 +306,8 @@ namespace smt { obj_hashtable m_axiom_set; unsigned m_axioms_head; // index of first axiom to add. bool m_incomplete; // is the solver (clearly) incomplete for the fragment. + expr_ref_vector m_int_string; + rational_set m_itos_axioms; obj_hashtable m_length; // is length applied scoped_ptr_vector m_replay; // set of actions to replay model_generator* m_mg; @@ -481,9 +486,14 @@ namespace smt { bool enforce_length(expr_ref_vector const& es, vector& len); void enforce_length_coherence(enode* n1, enode* n2); + // model-check the functions that convert integers to strings and the other way. + void add_int_string(expr* e); + bool check_int_string(); + void add_elim_string_axiom(expr* n); void add_at_axiom(expr* n); void add_in_re_axiom(expr* n); + bool add_itos_axiom(expr* n); literal mk_literal(expr* n); literal mk_eq_empty(expr* n, bool phase = true); literal mk_seq_eq(expr* a, expr* b); @@ -496,6 +506,7 @@ namespace smt { // arithmetic integration + bool get_value(expr* s, rational& val) const; bool lower_bound(expr* s, rational& lo) const; bool upper_bound(expr* s, rational& hi) const; bool get_length(expr* s, rational& val) const;