All Known Implementing Classes:

AbstractStringFormulaManager, DebuggingStringFormulaManager
```
public interface StringFormulaManager
```
Manager for dealing with string formulas. Functions come from http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml.

Method Summary

All Methods Instance Methods Abstract Methods Default Methods
Modifier and Type	Method	Description
`RegexFormula`	`all()`	Note: The size of the used alphabet depends on the underlying SMT solver.
`RegexFormula`	`allChar()`	Note: The size of the used alphabet depends on the underlying SMT solver.
`StringFormula`	`charAt(StringFormula str, NumeralFormula.IntegerFormula index)`	Get a substring of length 1 from the given String.
`RegexFormula`	`closure(RegexFormula regex)`
`RegexFormula`	`complement(RegexFormula regex)`
`StringFormula`	`concat(List<StringFormula> parts)`
`default RegexFormula`	`concat(RegexFormula... parts)`
`default StringFormula`	`concat(StringFormula... parts)`
`RegexFormula`	`concatRegex(List<RegexFormula> parts)`
`BooleanFormula`	`contains(StringFormula str, StringFormula part)`
`RegexFormula`	`cross(RegexFormula regex)`
`RegexFormula`	`difference(RegexFormula regex1, RegexFormula regex2)`
`BooleanFormula`	`equal(StringFormula str1, StringFormula str2)`
`BooleanFormula`	`greaterOrEquals(StringFormula str1, StringFormula str2)`
`BooleanFormula`	`greaterThan(StringFormula str1, StringFormula str2)`
`BooleanFormula`	`in(StringFormula str, RegexFormula regex)`
`NumeralFormula.IntegerFormula`	`indexOf(StringFormula str, StringFormula part, NumeralFormula.IntegerFormula startIndex)`	Get the first index for a substring in a String, or -1 if the substring is not found.
`RegexFormula`	`intersection(RegexFormula regex1, RegexFormula regex2)`
`NumeralFormula.IntegerFormula`	`length(StringFormula str)`
`BooleanFormula`	`lessOrEquals(StringFormula str1, StringFormula str2)`
`BooleanFormula`	`lessThan(StringFormula str1, StringFormula str2)`
`RegexFormula`	`makeRegex(String value)`	Returns a `RegexFormula` representing the given constant.
`StringFormula`	`makeString(String value)`	Returns a `StringFormula` representing the given constant.
`StringFormula`	`makeVariable(String pVar)`	Creates a variable of type String with exactly the given name.
`RegexFormula`	`none()`
`RegexFormula`	`optional(RegexFormula regex)`
`BooleanFormula`	`prefix(StringFormula prefix, StringFormula str)`	Check whether the given prefix is a real prefix of str.
`default RegexFormula`	`range(char start, char end)`
`RegexFormula`	`range(StringFormula start, StringFormula end)`
`StringFormula`	`replace(StringFormula fullStr, StringFormula target, StringFormula replacement)`	Replace the first appearances of target in fullStr with the replacement.
`StringFormula`	`replaceAll(StringFormula fullStr, StringFormula target, StringFormula replacement)`	Replace all appearances of target in fullStr with the replacement.
`StringFormula`	`substring(StringFormula str, NumeralFormula.IntegerFormula index, NumeralFormula.IntegerFormula length)`	Get a substring from the given String.
`BooleanFormula`	`suffix(StringFormula suffix, StringFormula str)`	Check whether the given suffix is a real suffix of str.
`RegexFormula`	`times(RegexFormula regex, int repetitions)`
`NumeralFormula.IntegerFormula`	`toIntegerFormula(StringFormula str)`	Interpret a String formula as an Integer formula.
`StringFormula`	`toStringFormula(NumeralFormula.IntegerFormula number)`	Interpret an Integer formula as a String formula.
`RegexFormula`	`union(RegexFormula regex1, RegexFormula regex2)`

- Method Detail
  - makeString
```
StringFormula makeString(String value)
```
    Returns a StringFormula representing the given constant.
    
    Parameters:
    
    value - the string value the returned Formula should represent
    
    Returns:
    
    a Formula representing the given value
  - makeVariable
```
StringFormula makeVariable(String pVar)
```
    Creates a variable of type String with exactly the given name.
    This variable (symbol) represents a "String" for which the SMT solver needs to find a model.
    Please make sure that the given name is valid in SMT-LIB2. Take a look at FormulaManager.isValidName(java.lang.String) for further information.
    This method does not quote or unquote the given name, but uses the plain name "AS IS". Formula.toString() can return a different String than the given one.
  - equal
```
BooleanFormula equal(StringFormula str1,
                     StringFormula str2)
```
  - greaterThan
```
BooleanFormula greaterThan(StringFormula str1,
                           StringFormula str2)
```
  - greaterOrEquals
```
BooleanFormula greaterOrEquals(StringFormula str1,
                               StringFormula str2)
```
  - lessThan
```
BooleanFormula lessThan(StringFormula str1,
                        StringFormula str2)
```
  - lessOrEquals
```
BooleanFormula lessOrEquals(StringFormula str1,
                            StringFormula str2)
```
  - prefix
```
BooleanFormula prefix(StringFormula prefix,
                      StringFormula str)
```
    Check whether the given prefix is a real prefix of str.
  - suffix
```
BooleanFormula suffix(StringFormula suffix,
                      StringFormula str)
```
    Check whether the given suffix is a real suffix of str.
  - contains
```
BooleanFormula contains(StringFormula str,
                        StringFormula part)
```
  - indexOf
```
NumeralFormula.IntegerFormula indexOf(StringFormula str,
                                      StringFormula part,
                                      NumeralFormula.IntegerFormula startIndex)
```
    Get the first index for a substring in a String, or -1 if the substring is not found. startIndex (inlcuded) denotes the start of the search for the index.
  - charAt
```
StringFormula charAt(StringFormula str,
                     NumeralFormula.IntegerFormula index)
```
    Get a substring of length 1 from the given String.
    The result is underspecified, if the index is out of bounds for the given String.
  - substring
```
StringFormula substring(StringFormula str,
                        NumeralFormula.IntegerFormula index,
                        NumeralFormula.IntegerFormula length)
```
    Get a substring from the given String.
    The result is underspecified, if the start index is out of bounds for the given String or if the requested length is negative. The length of the result is the minimum of the requested length and the remaining length of the given String.
  - replace
```
StringFormula replace(StringFormula fullStr,
                      StringFormula target,
                      StringFormula replacement)
```
    Replace the first appearances of target in fullStr with the replacement.
  - replaceAll
```
StringFormula replaceAll(StringFormula fullStr,
                         StringFormula target,
                         StringFormula replacement)
```
    Replace all appearances of target in fullStr with the replacement.
  - length
```
NumeralFormula.IntegerFormula length(StringFormula str)
```
  - concat
```
default StringFormula concat(StringFormula... parts)
```
  - concat
```
StringFormula concat(List<StringFormula> parts)
```
  - in
```
BooleanFormula in(StringFormula str,
                  RegexFormula regex)
```
    Parameters:
    
    str - formula representing the string to match
    
    regex - formula representing the regular expression
    
    Returns:
    
    a formula representing the acceptance of the string by the regular expression
  - makeRegex
```
RegexFormula makeRegex(String value)
```
    Returns a RegexFormula representing the given constant.
    This method does not parse an existing regex from String, but uses the String directly as a constant.
    
    Parameters:
    
    value - the regular expression the returned Formula should represent
  - none
```
RegexFormula none()
```
    Returns:
    
    formula denoting the empty set of strings
  - all
```
RegexFormula all()
```
    Note: The size of the used alphabet depends on the underlying SMT solver.
    
    Returns:
    
    formula denoting the set of all strings, also known as Regex ".*".
  - allChar
```
RegexFormula allChar()
```
    Note: The size of the used alphabet depends on the underlying SMT solver.
    
    Returns:
    
    formula denoting the set of all strings of length 1, also known as DOT operator which represents one arbitrary char, or as Regex ".".
  - range
```
RegexFormula range(StringFormula start,
                   StringFormula end)
```
    Returns:
    
    formula denoting the range regular expression over two sequences of length 1.
  - range
```
default RegexFormula range(char start,
                           char end)
```
    Returns:
    
    formula denoting the range regular expression over two chars.
    
    See Also:
    
    range(StringFormula, StringFormula)
  - concat
```
default RegexFormula concat(RegexFormula... parts)
```
    Returns:
    
    formula denoting the concatenation
  - concatRegex
```
RegexFormula concatRegex(List<RegexFormula> parts)
```
    Returns:
    
    formula denoting the concatenation
  - union
```
RegexFormula union(RegexFormula regex1,
                   RegexFormula regex2)
```
    Returns:
    
    formula denoting the union
  - intersection
```
RegexFormula intersection(RegexFormula regex1,
                          RegexFormula regex2)
```
    Returns:
    
    formula denoting the intersection
  - complement
```
RegexFormula complement(RegexFormula regex)
```
    Returns:
    
    formula denoting the Kleene closure
  - closure
```
RegexFormula closure(RegexFormula regex)
```
    Returns:
    
    formula denoting the Kleene closure (0 or more), also known as STAR operand.
  - difference
```
RegexFormula difference(RegexFormula regex1,
                        RegexFormula regex2)
```
    Returns:
    
    formula denoting the difference
  - cross
```
RegexFormula cross(RegexFormula regex)
```
    Returns:
    
    formula denoting the Kleene cross (1 or more), also known as PLUS operand.
  - optional
```
RegexFormula optional(RegexFormula regex)
```
    Returns:
    
    formula denoting the optionality, also known as QUESTIONMARK operand.
  - times
```
RegexFormula times(RegexFormula regex,
                   int repetitions)
```
    Returns:
    
    formula denoting the concatenation n times
  - toIntegerFormula
```
NumeralFormula.IntegerFormula toIntegerFormula(StringFormula str)
```
    Interpret a String formula as an Integer formula.
    The number is interpreted in base 10 and has no leading zeros. The method works as expected for positive numbers, including zero. It returns the constant value of -1 for negative numbers or invalid number representations, for example if any char is no digit.
  - toStringFormula
```
StringFormula toStringFormula(NumeralFormula.IntegerFormula number)
```
    Interpret an Integer formula as a String formula.
    The number is in base 10. The method works as expected for positive numbers, including zero. It returns the empty string "" for negative numbers.

Interface StringFormulaManager

Method Summary

Method Detail

makeString

makeVariable

equal

greaterThan

greaterOrEquals

lessThan

lessOrEquals

prefix

suffix

contains

indexOf

charAt

substring

replace

replaceAll

length

concat

concat

in

makeRegex

none

all

allChar

range

range

concat

concatRegex

union

intersection

complement

closure

difference

cross

optional

times

toIntegerFormula

toStringFormula