From 6ffb475007875a861f81769b8f969dbfd63a437d Mon Sep 17 00:00:00 2001 From: Federico Mora Date: Tue, 26 Nov 2019 20:20:10 -0800 Subject: [PATCH] Add comments and make implication into xor. Logically equivalent. --- src/smt/theory_str.cpp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 5142942ff..7b89bc9a4 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1879,11 +1879,13 @@ namespace smt { expr_ref axiom1(ctx.mk_eq_atom(axiom1_lhs, axiom1_rhs), m); SASSERT(axiom1); assert_axiom(axiom1); - - expr_ref zero(mk_string("0"), m); - expr_ref pref(u.str.mk_prefix(zero, ex), m); - assert_implication(pref, ctx.mk_eq_atom(ex, zero)); } + + // axiom 2: (str.from-int N) should not result in a string with leading zeros. + expr_ref zero(mk_string("0"), m); + expr_ref pref(u.str.mk_prefix(zero, ex), m); + // The result does not start with a "0" xor the result is "0" + assert_axiom(m.mk_or(m.mk_and(mk_not(m, pref), ctx.mk_eq_atom(ex, zero)), m.mk_and(pref, mk_not(m, ctx.mk_eq_atom(ex, zero))))); } expr * theory_str::mk_RegexIn(expr * str, expr * regexp) {