mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

add handling for int.to.str

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-04-18 11:14:40 -07:00
parent 5d0db6d256
commit 4761f4f191
3 changed files with 79 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/seq_decl_plugin.h
View file

@ -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); }

66
src/smt/theory_seq.cpp
View file

@ -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<theory_seq, expr>(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<theory_seq, expr_ref_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<theory_seq, rational_set, rational>(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));

11
src/smt/theory_seq.h
View file

@ -287,7 +287,10 @@ namespace smt {
unsigned m_extensionality;
unsigned m_fixed_length;
unsigned m_propagate_contains;
unsigned m_int_string;
};
typedef hashtable<rational, rational::hash_proc, rational::eq_proc> rational_set;
ast_manager& m;
dependency_manager m_dm;
solution_map m_rep; // unification representative.
@ -303,6 +306,8 @@ namespace smt {
obj_hashtable<expr> 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<expr> m_length; // is length applied
scoped_ptr_vector<apply> 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<rational>& 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;