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:17:33 -07:00
parent 4761f4f191
commit 81232808ba
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/smt/theory_seq.cpp
View file

@ -2194,7 +2194,7 @@ 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)) {
if (m_util.str.is_itos(e) && add_itos_axiom(e)) {
change = true;
}
else if (m_util.str.is_stoi(e, n)) {
@ -2211,11 +2211,12 @@ 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);
VERIFY(m_util.str.is_itos(e, n));
if (get_value(n, val)) {
if (!m_itos_axioms.contains(val)) {
m_itos_axioms.insert(val);
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);
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));