Package org.sosy_lab.java_smt.basicimpl

Class AbstractStringFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>

java.lang.Object

org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>

All Implemented Interfaces:

StringFormulaManager

public abstract class AbstractStringFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
extends Object
implements StringFormulaManager

Field Summary

Fields

Modifier and Type	Field	Description
protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>	formulaCreator

Constructor Summary

Constructors

Modifier	Constructor	Description
protected	AbstractStringFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pCreator)

Method Summary

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.
protected abstract TFormulaInfo	allCharImpl()
protected abstract TFormulaInfo	allImpl()
StringFormula	charAt(StringFormula str, NumeralFormula.IntegerFormula index)	Get a substring of length 1 from the given String if the given index is within bounds.
protected abstract TFormulaInfo	charAt(TFormulaInfo str, TFormulaInfo index)
RegexFormula	closure(RegexFormula regex)
protected abstract TFormulaInfo	closure(TFormulaInfo pParam)
RegexFormula	complement(RegexFormula regex)
protected abstract TFormulaInfo	complement(TFormulaInfo pParam)
StringFormula	concat(List<StringFormula> parts)
protected abstract TFormulaInfo	concatImpl(List<TFormulaInfo> parts)
RegexFormula	concatRegex(List<RegexFormula> parts)
protected abstract TFormulaInfo	concatRegexImpl(List<TFormulaInfo> parts)
BooleanFormula	contains(StringFormula str, StringFormula part)
protected abstract TFormulaInfo	contains(TFormulaInfo str, TFormulaInfo part)
RegexFormula	cross(RegexFormula regex)
RegexFormula	difference(RegexFormula regex1, RegexFormula regex2)
protected TFormulaInfo	difference(TFormulaInfo pParam1, TFormulaInfo pParam2)
BooleanFormula	equal(StringFormula str1, StringFormula str2)
protected abstract TFormulaInfo	equal(TFormulaInfo pParam1, TFormulaInfo pParam2)
static String	escapeUnicodeForSmtlib(String input)	Replace Unicode letters in UTF16 representation with their escape sequences.
protected TFormulaInfo	extractInfo(Formula pBits)
StringFormula	fromCodePoint(NumeralFormula.IntegerFormula number)	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]).
protected abstract TFormulaInfo	fromCodePoint(TFormulaInfo pParam)
protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>	getFormulaCreator()
BooleanFormula	greaterOrEquals(StringFormula str1, StringFormula str2)
protected abstract TFormulaInfo	greaterOrEquals(TFormulaInfo pParam1, TFormulaInfo pParam2)
BooleanFormula	greaterThan(StringFormula str1, StringFormula str2)
protected abstract TFormulaInfo	greaterThan(TFormulaInfo pParam1, TFormulaInfo pParam2)
BooleanFormula	in(StringFormula str, RegexFormula regex)
protected abstract TFormulaInfo	in(TFormulaInfo str, TFormulaInfo 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.
protected abstract TFormulaInfo	indexOf(TFormulaInfo str, TFormulaInfo part, TFormulaInfo startIndex)
RegexFormula	intersection(RegexFormula regex1, RegexFormula regex2)
protected abstract TFormulaInfo	intersection(TFormulaInfo pParam1, TFormulaInfo pParam2)
NumeralFormula.IntegerFormula	length(StringFormula str)
protected abstract TFormulaInfo	length(TFormulaInfo pParam)
BooleanFormula	lessOrEquals(StringFormula str1, StringFormula str2)
protected abstract TFormulaInfo	lessOrEquals(TFormulaInfo pParam1, TFormulaInfo pParam2)
BooleanFormula	lessThan(StringFormula str1, StringFormula str2)
protected abstract TFormulaInfo	lessThan(TFormulaInfo pParam1, TFormulaInfo pParam2)
RegexFormula	makeRegex(String value)	Returns a RegexFormula representing the given constant.
protected abstract TFormulaInfo	makeRegexImpl(String value)
StringFormula	makeString(String value)	Creates a StringFormula representing the given constant String.
protected abstract TFormulaInfo	makeStringImpl(String value)
StringFormula	makeVariable(String pVar)	Creates a variable of type String with exactly the given name.
protected abstract TFormulaInfo	makeVariableImpl(String pVar)
RegexFormula	none()
protected abstract TFormulaInfo	noneImpl()
RegexFormula	optional(RegexFormula regex)
BooleanFormula	prefix(StringFormula prefix, StringFormula str)	Check whether the given prefix is a real prefix of str.
protected abstract TFormulaInfo	prefix(TFormulaInfo prefix, TFormulaInfo str)
RegexFormula	range(StringFormula start, StringFormula end)
protected abstract TFormulaInfo	range(TFormulaInfo start, TFormulaInfo end)
StringFormula	replace(StringFormula fullStr, StringFormula target, StringFormula replacement)	Replace the first appearances of target in fullStr with the replacement.
protected abstract TFormulaInfo	replace(TFormulaInfo fullStr, TFormulaInfo target, TFormulaInfo replacement)
StringFormula	replaceAll(StringFormula fullStr, StringFormula target, StringFormula replacement)	Replace all appearances of target in fullStr with the replacement.
protected abstract TFormulaInfo	replaceAll(TFormulaInfo fullStr, TFormulaInfo target, TFormulaInfo replacement)
StringFormula	substring(StringFormula str, NumeralFormula.IntegerFormula index, NumeralFormula.IntegerFormula length)	Get a substring from the given String.
protected abstract TFormulaInfo	substring(TFormulaInfo str, TFormulaInfo index, TFormulaInfo length)
BooleanFormula	suffix(StringFormula suffix, StringFormula str)	Check whether the given suffix is a real suffix of str.
protected abstract TFormulaInfo	suffix(TFormulaInfo suffix, TFormulaInfo str)
RegexFormula	times(RegexFormula regex, int repetitions)
NumeralFormula.IntegerFormula	toCodePoint(StringFormula number)	Returns an Integer formula representing the code point of the only character of the given String formula, if it represents a single character.
protected abstract TFormulaInfo	toCodePoint(TFormulaInfo pParam)
NumeralFormula.IntegerFormula	toIntegerFormula(StringFormula str)	Interpret a String formula as an Integer formula.
protected abstract TFormulaInfo	toIntegerFormula(TFormulaInfo pParam)
protected TType	toSolverType(FormulaType<?> formulaType)
StringFormula	toStringFormula(NumeralFormula.IntegerFormula number)	Interpret an Integer formula as a String formula.
protected abstract TFormulaInfo	toStringFormula(TFormulaInfo pParam)
static String	unescapeUnicodeForSmtlib(String input)	Replace escaped Unicode letters in SMTLIB representation with their UTF16 pendant.
RegexFormula	union(RegexFormula regex1, RegexFormula regex2)
protected abstract TFormulaInfo	union(TFormulaInfo pParam1, TFormulaInfo pParam2)
protected NumeralFormula.IntegerFormula	wrapInteger(TFormulaInfo formulaInfo)
protected RegexFormula	wrapRegex(TFormulaInfo formulaInfo)
protected StringFormula	wrapString(TFormulaInfo formulaInfo)

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

Field Detail

formulaCreator

protected final FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> formulaCreator

Constructor Detail

AbstractStringFormulaManager

protected AbstractStringFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pCreator)

Method Detail

wrapString

protected StringFormula wrapString(TFormulaInfo formulaInfo)

wrapRegex

protected RegexFormula wrapRegex(TFormulaInfo formulaInfo)

wrapInteger

protected NumeralFormula.IntegerFormula wrapInteger(TFormulaInfo formulaInfo)

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 unescapeUnicodeForSmtlib(String) can be used to handle the conversion before calling this method. Note that you may then also have to use 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

escapeUnicodeForSmtlib

public static String escapeUnicodeForSmtlib(String input)

Replace Unicode letters in UTF16 representation with their escape sequences.

unescapeUnicodeForSmtlib

public static String unescapeUnicodeForSmtlib(String input)

Replace escaped Unicode letters in SMTLIB representation with their UTF16 pendant.

makeStringImpl

protected abstract TFormulaInfo makeStringImpl(String 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

makeVariableImpl

protected abstract TFormulaInfo makeVariableImpl(String pVar)

equal

public BooleanFormula equal(StringFormula str1,
                            StringFormula str2)

Specified by:

equal in interface StringFormulaManager

equal

protected abstract TFormulaInfo equal(TFormulaInfo pParam1,
                                      TFormulaInfo pParam2)

greaterThan

public BooleanFormula greaterThan(StringFormula str1,
                                  StringFormula str2)

Specified by:

greaterThan in interface StringFormulaManager

greaterThan

protected abstract TFormulaInfo greaterThan(TFormulaInfo pParam1,
                                            TFormulaInfo pParam2)

greaterOrEquals

public BooleanFormula greaterOrEquals(StringFormula str1,
                                      StringFormula str2)

Specified by:

greaterOrEquals in interface StringFormulaManager

greaterOrEquals

protected abstract TFormulaInfo greaterOrEquals(TFormulaInfo pParam1,
                                                TFormulaInfo pParam2)

lessThan

public BooleanFormula lessThan(StringFormula str1,
                               StringFormula str2)

Specified by:

lessThan in interface StringFormulaManager

lessThan

protected abstract TFormulaInfo lessThan(TFormulaInfo pParam1,
                                         TFormulaInfo pParam2)

lessOrEquals

public BooleanFormula lessOrEquals(StringFormula str1,
                                   StringFormula str2)

Specified by:

lessOrEquals in interface StringFormulaManager

lessOrEquals

protected abstract TFormulaInfo lessOrEquals(TFormulaInfo pParam1,
                                             TFormulaInfo pParam2)

length

public NumeralFormula.IntegerFormula length(StringFormula str)

Specified by:

length in interface StringFormulaManager

length

protected abstract TFormulaInfo length(TFormulaInfo pParam)

concat

public StringFormula concat(List<StringFormula> parts)

Specified by:

concat in interface StringFormulaManager

concatImpl

protected abstract TFormulaInfo concatImpl(List<TFormulaInfo> parts)

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

prefix

protected abstract TFormulaInfo prefix(TFormulaInfo prefix,
                                       TFormulaInfo str)

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

suffix

protected abstract TFormulaInfo suffix(TFormulaInfo suffix,
                                       TFormulaInfo str)

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

in

protected abstract TFormulaInfo in(TFormulaInfo str,
                                   TFormulaInfo regex)

contains

public BooleanFormula contains(StringFormula str,
                               StringFormula part)

Specified by:

contains in interface StringFormulaManager

contains

protected abstract TFormulaInfo contains(TFormulaInfo str,
                                         TFormulaInfo part)

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

indexOf

protected abstract TFormulaInfo indexOf(TFormulaInfo str,
                                        TFormulaInfo part,
                                        TFormulaInfo startIndex)

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

charAt

protected abstract TFormulaInfo charAt(TFormulaInfo str,
                                       TFormulaInfo index)

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

substring

protected abstract TFormulaInfo substring(TFormulaInfo str,
                                          TFormulaInfo index,
                                          TFormulaInfo length)

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

replace

protected abstract TFormulaInfo replace(TFormulaInfo fullStr,
                                        TFormulaInfo target,
                                        TFormulaInfo replacement)

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

replaceAll

protected abstract TFormulaInfo replaceAll(TFormulaInfo fullStr,
                                           TFormulaInfo target,
                                           TFormulaInfo replacement)

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

makeRegexImpl

protected abstract TFormulaInfo makeRegexImpl(String value)

none

public RegexFormula none()

Specified by:

none in interface StringFormulaManager

Returns:

formula denoting the empty set of strings

noneImpl

protected abstract TFormulaInfo noneImpl()

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 ".*".

allImpl

protected abstract TFormulaInfo allImpl()

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 ".".

allCharImpl

protected abstract TFormulaInfo allCharImpl()

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.

range

protected abstract TFormulaInfo range(TFormulaInfo start,
                                      TFormulaInfo end)

concatRegex

public RegexFormula concatRegex(List<RegexFormula> parts)

Specified by:

concatRegex in interface StringFormulaManager

Returns:

formula denoting the concatenation

concatRegexImpl

protected abstract TFormulaInfo concatRegexImpl(List<TFormulaInfo> parts)

union

public RegexFormula union(RegexFormula regex1,
                          RegexFormula regex2)

Specified by:

union in interface StringFormulaManager

Returns:

formula denoting the union

union

protected abstract TFormulaInfo union(TFormulaInfo pParam1,
                                      TFormulaInfo pParam2)

intersection

public RegexFormula intersection(RegexFormula regex1,
                                 RegexFormula regex2)

Specified by:

intersection in interface StringFormulaManager

Returns:

formula denoting the intersection

intersection

protected abstract TFormulaInfo intersection(TFormulaInfo pParam1,
                                             TFormulaInfo pParam2)

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.

closure

protected abstract TFormulaInfo closure(TFormulaInfo pParam)

complement

public RegexFormula complement(RegexFormula regex)

Specified by:

complement in interface StringFormulaManager

Returns:

formula denoting the Kleene closure

complement

protected abstract TFormulaInfo complement(TFormulaInfo pParam)

difference

public RegexFormula difference(RegexFormula regex1,
                               RegexFormula regex2)

Specified by:

difference in interface StringFormulaManager

Returns:

formula denoting the difference

difference

protected TFormulaInfo difference(TFormulaInfo pParam1,
                                  TFormulaInfo pParam2)

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

toIntegerFormula

protected abstract TFormulaInfo toIntegerFormula(TFormulaInfo pParam)

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

toStringFormula

protected abstract TFormulaInfo toStringFormula(TFormulaInfo pParam)

toCodePoint

public NumeralFormula.IntegerFormula toCodePoint(StringFormula number)

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

toCodePoint

protected abstract TFormulaInfo toCodePoint(TFormulaInfo pParam)

fromCodePoint

public StringFormula fromCodePoint(NumeralFormula.IntegerFormula number)

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

fromCodePoint

protected abstract TFormulaInfo fromCodePoint(TFormulaInfo pParam)

getFormulaCreator

protected final FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> getFormulaCreator()

extractInfo

protected final TFormulaInfo extractInfo(Formula pBits)

toSolverType

protected final TType toSolverType(FormulaType<?> formulaType)