From 5c04b9eee2875d91955bd2578611a7a7f27699f0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 9 Feb 2021 16:38:03 -0800 Subject: [PATCH] fix #5012 teething stage for from/to code axiomatization --- src/smt/seq_axioms.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/smt/seq_axioms.cpp b/src/smt/seq_axioms.cpp index 077b342f6..42010ef5f 100644 --- a/src/smt/seq_axioms.cpp +++ b/src/smt/seq_axioms.cpp @@ -804,6 +804,7 @@ void seq_axioms::add_is_digit_axiom(expr* n) { /** len(e) = 1 => 0 <= to_code(e) <= max_code + len(e) = 1 => from_code(to_code(e)) = e len(e) != 1 => to_code(e) = -1 */ void seq_axioms::add_str_to_code_axiom(expr* n) { @@ -812,6 +813,8 @@ void seq_axioms::add_str_to_code_axiom(expr* n) { literal len_is1 = mk_eq(mk_len(e), a.mk_int(1)); add_axiom(~len_is1, mk_ge(n, 0)); add_axiom(~len_is1, mk_le(n, seq.max_char())); + if (!seq.str.is_from_code(e)) + add_axiom(~len_is1, mk_eq(e, seq.str.mk_from_code(n))); add_axiom(len_is1, mk_eq(n, a.mk_int(-1))); } @@ -827,7 +830,8 @@ void seq_axioms::add_str_from_code_axiom(expr* n) { literal le = mk_le(e, seq.max_char()); literal emp = mk_literal(seq.str.mk_is_empty(n)); add_axiom(~ge, ~le, mk_eq(mk_len(n), a.mk_int(1))); - add_axiom(~ge, ~le, mk_eq(seq.str.mk_to_code(n), e)); + if (!seq.str.is_to_code(e)) + add_axiom(~ge, ~le, mk_eq(seq.str.mk_to_code(n), e)); add_axiom(ge, emp); add_axiom(le, emp); }