From 07bc19b489c61ac2e416ea8d0bd9d0575383500a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Aug 2017 07:19:04 -0700 Subject: [PATCH] add documentation to string rewriting Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index fc38f0ae4..36a99c592 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1083,6 +1083,16 @@ br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) { return BR_FAILED; } +/** + \brief rewrite str.to.int according to the rules: + - if the expression is a string which is a non-empty + sequence of digits 0-9 extract the corresponding numeral. + - if the expression is a string that contains any other character + or is empty, produce -1 + - if the expression is int.to.str(x) produce + ite(x >= 0, x, -1) + +*/ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) { zstring str; if (m_util.str.is_string(a, str)) {