java.lang.Object
- org.sosy_lab.java_smt.delegate.debugging.DebuggingStringFormulaManager

All Implemented Interfaces:: StringFormulaManager

public class DebuggingStringFormulaManager
extends Object
implements StringFormulaManager

Method Summary

All Methods Instance Methods Concrete 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 if the given index is within bounds.
`RegexFormula`	`closure(RegexFormula regex)`
`RegexFormula`	`complement(RegexFormula regex)`
`StringFormula`	`concat(List<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)`
`StringFormula`	`fromCodePoint(NumeralFormula.IntegerFormula codepoint)`	Returns a String formula representing the single character with the given code point, if it is a valid Unicode code point within the Basic Multilingual Plane (BMP) or planes 1 and 2 (codepoints in range [0x00000, 0x2FFFF]).
`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)`	Creates a `StringFormula` representing the given constant String.
`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.
`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`	`toCodePoint(StringFormula str)`	Returns an Integer formula representing the code point of the only character of the given String formula, if it represents a single character.
`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)`

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface org.sosy_lab.java_smt.api.StringFormulaManager
concat, concat, range

- Method Detail
  - makeString
```
public StringFormula makeString(String value)
```
    Description copied from interface: StringFormulaManager
    
    Creates a StringFormula representing the given constant String.
    The String argument is expected to be a regular Java String and may contain Unicode characters from the first 3 planes (codepoints 0x00000-0x2FFFFF). Higher codepoints are not allowed due to limitations in SMTLIB. We do not support SMTLIB escape sequences in this method, and String like "\\u{abc}" are read verbatim and are not substituted with their Unicode character. If you still want to use SMTLIB Strings with this method, the function AbstractStringFormulaManager.unescapeUnicodeForSmtlib(String) can be used to handle the conversion before calling this method. Note that you may then also have to use AbstractStringFormulaManager.escapeUnicodeForSmtlib(String) to convert Strings from the model back to a format that is compatible with other SMTLIB based solvers.
    
    Specified by:
    
    makeString in interface StringFormulaManager
    
    Parameters:
    
    value - the string value the returned StringFormula should represent
    
    Returns:
    
    a StringFormula representing the given value
  - makeVariable
```
public StringFormula makeVariable(String pVar)
```
    Description copied from interface: StringFormulaManager
    
    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.
    
    Specified by:
    
    makeVariable in interface StringFormulaManager
  - equal
```
public BooleanFormula equal(StringFormula str1,
                            StringFormula str2)
```
    Specified by:
    
    equal in interface StringFormulaManager
  - greaterThan
```
public BooleanFormula greaterThan(StringFormula str1,
                                  StringFormula str2)
```
    Specified by:
    
    greaterThan in interface StringFormulaManager
  - greaterOrEquals
```
public BooleanFormula greaterOrEquals(StringFormula str1,
                                      StringFormula str2)
```
    Specified by:
    
    greaterOrEquals in interface StringFormulaManager
  - lessThan
```
public BooleanFormula lessThan(StringFormula str1,
                               StringFormula str2)
```
    Specified by:
    
    lessThan in interface StringFormulaManager
  - lessOrEquals
```
public BooleanFormula lessOrEquals(StringFormula str1,
                                   StringFormula str2)
```
    Specified by:
    
    lessOrEquals in interface StringFormulaManager
  - prefix
```
public BooleanFormula prefix(StringFormula prefix,
                             StringFormula str)
```
    Description copied from interface: StringFormulaManager
    
    Check whether the given prefix is a real prefix of str.
    
    Specified by:
    
    prefix in interface StringFormulaManager
  - suffix
```
public BooleanFormula suffix(StringFormula suffix,
                             StringFormula str)
```
    Description copied from interface: StringFormulaManager
    
    Check whether the given suffix is a real suffix of str.
    
    Specified by:
    
    suffix in interface StringFormulaManager
  - contains
```
public BooleanFormula contains(StringFormula str,
                               StringFormula part)
```
    Specified by:
    
    contains in interface StringFormulaManager
  - indexOf
```
public NumeralFormula.IntegerFormula indexOf(StringFormula str,
                                             StringFormula part,
                                             NumeralFormula.IntegerFormula startIndex)
```
    Description copied from interface: StringFormulaManager
    
    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.
    
    Specified by:
    
    indexOf in interface StringFormulaManager
  - charAt
```
public StringFormula charAt(StringFormula str,
                            NumeralFormula.IntegerFormula index)
```
    Description copied from interface: StringFormulaManager
    
    Get a substring of length 1 from the given String if the given index is within bounds. Otherwise, returns an empty string.
    
    Specified by:
    
    charAt in interface StringFormulaManager
  - substring
```
public StringFormula substring(StringFormula str,
                               NumeralFormula.IntegerFormula index,
                               NumeralFormula.IntegerFormula length)
```
    Description copied from interface: StringFormulaManager
    
    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.
    
    Specified by:
    
    substring in interface StringFormulaManager
  - replace
```
public StringFormula replace(StringFormula fullStr,
                             StringFormula target,
                             StringFormula replacement)
```
    Description copied from interface: StringFormulaManager
    
    Replace the first appearances of target in fullStr with the replacement.
    
    Specified by:
    
    replace in interface StringFormulaManager
  - replaceAll
```
public StringFormula replaceAll(StringFormula fullStr,
                                StringFormula target,
                                StringFormula replacement)
```
    Description copied from interface: StringFormulaManager
    
    Replace all appearances of target in fullStr with the replacement.
    
    Specified by:
    
    replaceAll in interface StringFormulaManager
  - length
```
public NumeralFormula.IntegerFormula length(StringFormula str)
```
    Specified by:
    
    length in interface StringFormulaManager
  - concat
```
public StringFormula concat(List<StringFormula> parts)
```
    Specified by:
    
    concat in interface StringFormulaManager
  - in
```
public BooleanFormula in(StringFormula str,
                         RegexFormula regex)
```
    Specified by:
    
    in in interface StringFormulaManager
    
    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
```
public RegexFormula makeRegex(String value)
```
    Description copied from interface: StringFormulaManager
    
    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.
    
    Specified by:
    
    makeRegex in interface StringFormulaManager
    
    Parameters:
    
    value - the regular expression the returned Formula should represent
  - none
```
public RegexFormula none()
```
    Specified by:
    
    none in interface StringFormulaManager
    
    Returns:
    
    formula denoting the empty set of strings
  - all
```
public RegexFormula all()
```
    Description copied from interface: StringFormulaManager
    
    Note: The size of the used alphabet depends on the underlying SMT solver.
    
    Specified by:
    
    all in interface StringFormulaManager
    
    Returns:
    
    formula denoting the set of all strings, also known as Regex ".*".
  - allChar
```
public RegexFormula allChar()
```
    Description copied from interface: StringFormulaManager
    
    Note: The size of the used alphabet depends on the underlying SMT solver.
    
    Specified by:
    
    allChar in interface StringFormulaManager
    
    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
```
public RegexFormula range(StringFormula start,
                          StringFormula end)
```
    Specified by:
    
    range in interface StringFormulaManager
    
    Returns:
    
    formula denoting the range regular expression over two sequences of length 1.
  - concatRegex
```
public RegexFormula concatRegex(List<RegexFormula> parts)
```
    Specified by:
    
    concatRegex in interface StringFormulaManager
    
    Returns:
    
    formula denoting the concatenation
  - union
```
public RegexFormula union(RegexFormula regex1,
                          RegexFormula regex2)
```
    Specified by:
    
    union in interface StringFormulaManager
    
    Returns:
    
    formula denoting the union
  - intersection
```
public RegexFormula intersection(RegexFormula regex1,
                                 RegexFormula regex2)
```
    Specified by:
    
    intersection in interface StringFormulaManager
    
    Returns:
    
    formula denoting the intersection
  - complement
```
public RegexFormula complement(RegexFormula regex)
```
    Specified by:
    
    complement in interface StringFormulaManager
    
    Returns:
    
    formula denoting the Kleene closure
  - closure
```
public RegexFormula closure(RegexFormula regex)
```
    Specified by:
    
    closure in interface StringFormulaManager
    
    Returns:
    
    formula denoting the Kleene closure (0 or more), also known as STAR operand.
  - difference
```
public RegexFormula difference(RegexFormula regex1,
                               RegexFormula regex2)
```
    Specified by:
    
    difference in interface StringFormulaManager
    
    Returns:
    
    formula denoting the difference
  - cross
```
public RegexFormula cross(RegexFormula regex)
```
    Specified by:
    
    cross in interface StringFormulaManager
    
    Returns:
    
    formula denoting the Kleene cross (1 or more), also known as PLUS operand.
  - optional
```
public RegexFormula optional(RegexFormula regex)
```
    Specified by:
    
    optional in interface StringFormulaManager
    
    Returns:
    
    formula denoting the optionality, also known as QUESTIONMARK operand.
  - times
```
public RegexFormula times(RegexFormula regex,
                          int repetitions)
```
    Specified by:
    
    times in interface StringFormulaManager
    
    Returns:
    
    formula denoting the concatenation n times
  - toIntegerFormula
```
public NumeralFormula.IntegerFormula toIntegerFormula(StringFormula str)
```
    Description copied from interface: StringFormulaManager
    
    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.
    
    Specified by:
    
    toIntegerFormula in interface StringFormulaManager
  - toStringFormula
```
public StringFormula toStringFormula(NumeralFormula.IntegerFormula number)
```
    Description copied from interface: StringFormulaManager
    
    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.
    
    Specified by:
    
    toStringFormula in interface StringFormulaManager
  - toCodePoint
```
public NumeralFormula.IntegerFormula toCodePoint(StringFormula str)
```
    Description copied from interface: StringFormulaManager
    
    Returns an Integer formula representing the code point of the only character of the given String formula, if it represents a single character. Otherwise, returns -1.
    
    Specified by:
    
    toCodePoint in interface StringFormulaManager
  - fromCodePoint
```
public StringFormula fromCodePoint(NumeralFormula.IntegerFormula codepoint)
```
    Description copied from interface: StringFormulaManager
    
    Returns a String formula representing the single character with the given code point, if it is a valid Unicode code point within the Basic Multilingual Plane (BMP) or planes 1 and 2 (codepoints in range [0x00000, 0x2FFFF]). Otherwise, returns the empty string.
    
    Specified by:
    
    fromCodePoint in interface StringFormulaManager

Class DebuggingStringFormulaManager

Method Summary

Methods inherited from class java.lang.Object

Methods inherited from interface org.sosy_lab.java_smt.api.StringFormulaManager

Method Detail

makeString

makeVariable

equal

greaterThan

greaterOrEquals

lessThan

lessOrEquals

prefix

suffix

contains

indexOf

charAt

substring

replace

replaceAll

length

concat

in

makeRegex

none

all

allChar

range

concatRegex

union

intersection

complement

closure

difference

cross

optional

times

toIntegerFormula

toStringFormula

toCodePoint

fromCodePoint