Skip to content

Commit d4a9b2a

Browse files
More comments on the output of last_index_of functions
1 parent 80dff96 commit d4a9b2a

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

src/solvers/refinement/string_constraint_generator_indexof.cpp

+3-2
Original file line numberDiff line numberDiff line change
@@ -201,7 +201,7 @@ Function: string_constraint_generatort::add_axioms_for_last_index_of_string
201201
from_index - an expression representing an index in strings
202202
203203
Outputs: an integer expression representing the last index of needle in
204-
haystack after from_index, or -1 if there is none
204+
haystack before or at from_index, or -1 if there is none
205205
206206
Purpose: Add axioms stating that the returned value is the index within
207207
haystack of the last occurence of needle starting the search
@@ -365,7 +365,8 @@ Function: string_constraint_generatort::add_axioms_for_last_index_of
365365
c - an expression representing a character
366366
from_index - an expression representing an index in the string
367367
368-
Outputs: a integer expression
368+
Outputs: an integer expression representing the last index of c in
369+
str before or at from_index, or -1 if there is none
369370
370371
Purpose: Add axioms stating that the returned value is the index within
371372
str of the last occurence of c starting the search backward at

0 commit comments

Comments
 (0)