mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

add support for default semantics for stoi (non-integer strings map to -1). Issue #670

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-07-08 10:45:19 -07:00
parent 0d0d504d62
commit bdbf1c9bf4
2 changed files with 28 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
src/smt/theory_seq.cpp
View file

@ -2197,16 +2197,37 @@ bool theory_seq::check_int_string() {
if (m_util.str.is_itos(e) && add_itos_axiom(e)) { if (m_util.str.is_itos(e) && add_itos_axiom(e)) {
change = true; change = true;
} }
else if (m_util.str.is_stoi(e, n)) { else if (m_util.str.is_stoi(e, n) && add_stoi_axiom(e)) {
// not (yet) handled. change = true;
// we would check that in the current proto-model
// the string at 'n', when denoting integer would map to the
// proper integer.
} }
} }
return change; return change;
} }
bool theory_seq::add_stoi_axiom(expr* e) {
context& ctx = get_context();
expr* n;
rational val;
VERIFY(m_util.str.is_stoi(e, n));
if (get_value(e, val) && !m_stoi_axioms.contains(val)) {
m_stoi_axioms.insert(val);
if (!val.is_minus_one()) {
app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m);
expr_ref n1(arith_util(m).mk_numeral(val, true), m);
literal eq1 = mk_eq(e, n1, false);
literal eq2 = mk_eq(n, e1, false);
add_axiom(~eq1, eq2);
add_axiom(~eq2, eq1);
ctx.force_phase(eq1);
ctx.force_phase(eq2);
m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_stoi_axioms, val));
m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
return true;
}
}
return false;
}
bool theory_seq::add_itos_axiom(expr* e) { bool theory_seq::add_itos_axiom(expr* e) {
context& ctx = get_context(); context& ctx = get_context();
rational val; rational val;

2
src/smt/theory_seq.h
View file

@ -308,6 +308,7 @@ namespace smt {
bool m_incomplete; // is the solver (clearly) incomplete for the fragment. bool m_incomplete; // is the solver (clearly) incomplete for the fragment.
expr_ref_vector m_int_string; expr_ref_vector m_int_string;
rational_set m_itos_axioms; rational_set m_itos_axioms;
rational_set m_stoi_axioms;
obj_hashtable<expr> m_length; // is length applied obj_hashtable<expr> m_length; // is length applied
scoped_ptr_vector<apply> m_replay; // set of actions to replay scoped_ptr_vector<apply> m_replay; // set of actions to replay
model_generator* m_mg; model_generator* m_mg;
@ -493,6 +494,7 @@ namespace smt {
void add_elim_string_axiom(expr* n); void add_elim_string_axiom(expr* n);
void add_at_axiom(expr* n); void add_at_axiom(expr* n);
void add_in_re_axiom(expr* n); void add_in_re_axiom(expr* n);
bool add_stoi_axiom(expr* n);
bool add_itos_axiom(expr* n); bool add_itos_axiom(expr* n);
void add_itos_length_axiom(expr* n); void add_itos_length_axiom(expr* n);
literal mk_literal(expr* n); literal mk_literal(expr* n);