From f4ec63f39c249299eaca857bf594b568268e2a9e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 6 Aug 2020 14:00:50 -0500 Subject: [PATCH] z3str3: add auxiliary str.substr axioms (#4617) --- src/smt/theory_str.cpp | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index afb997370d0..20ea3927255 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1720,6 +1720,31 @@ namespace smt { rw(case3_rw); assert_axiom(case3_rw); } + + // Auxiliary axioms + { + // base = "" --> (str.substr base pos len) = "" + { + expr_ref premise(ctx.mk_eq_atom(substrBase, mk_string("")), m); + expr_ref conclusion(ctx.mk_eq_atom(expr, mk_string("")), m); + expr_ref axiom(m.mk_implies(premise, conclusion), m); + assert_axiom_rw(axiom); + } + + // len( (str.substr base pos len) ) <= len(base) + { + expr_ref axiom(m_autil.mk_le(mk_strlen(expr), mk_strlen(substrBase)), m); + assert_axiom_rw(axiom); + } + + // len >= 0 --> len( (str.substr base pos len) ) <= len + { + expr_ref premise(m_autil.mk_ge(substrLen, mk_int(0)), m); + expr_ref conclusion(m_autil.mk_le(mk_strlen(expr), substrLen), m); + expr_ref axiom(m.mk_implies(premise, conclusion), m); + assert_axiom_rw(axiom); + } + } } // (str.replace s t t') is the string obtained by replacing the first occurrence