From 2da2646dd65e0458311a2dccfb04850c0b7d9e3c Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 10 Jun 2020 12:50:52 -0700 Subject: Add support for str.replace_re/str.replace_re_all (#4594) This commit adds support for the last remaining string operators from the new SMT-LIB standard for the theory of strings. The commit adds the kinds, type checking, reductions, and evaluation rewrites for `str.replace_re` and `str.replace_re_all`. --- src/theory/strings/term_registry.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'src/theory/strings/term_registry.cpp') diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 6330d7c10..395604f76 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -76,9 +76,10 @@ void TermRegistry::preRegisterTerm(TNode n) if (!options::stringExp()) { if (k == STRING_STRIDOF || k == STRING_ITOS || k == STRING_STOI - || k == STRING_STRREPL || k == STRING_STRREPLALL || k == STRING_STRCTN - || k == STRING_LEQ || k == STRING_TOLOWER || k == STRING_TOUPPER - || k == STRING_REV) + || k == STRING_STRREPL || k == STRING_STRREPLALL + || k == STRING_REPLACE_RE || k == STRING_REPLACE_RE_ALL + || k == STRING_STRCTN || k == STRING_LEQ || k == STRING_TOLOWER + || k == STRING_TOUPPER || k == STRING_REV) { std::stringstream ss; ss << "Term of kind " << k -- cgit v1.2.3