java.lang.Object
- org.sosy_lab.java_smt.basicimpl.FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>

Type Parameters:

TFormulaInfo - the solver specific type for formulas.

TType - the solver specific type for formula types.

TEnv - the solver specific type for the environment/context.
```
public abstract class FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>
extends Object
```
This is a helper class with several methods that are commonly used throughout the basicimpl package and may have solver-specific implementations. Each solver package is expected to provide an instance of this class, with the appropriate methods overwritten. Depending on the solver, some or all non-final methods in this class may need to be overwritten.

Field Summary

Fields
Modifier and Type Field Description

protected TEnv environment

Constructor Summary

Constructors
Modifier	Constructor	Description
`protected`	`FormulaCreator(TEnv env, TType boolType, @Nullable TType pIntegerType, @Nullable TType pRationalType, @Nullable TType stringType, @Nullable TType regexType)`

Method Summary

All Methods Static Methods Instance Methods Abstract Methods Concrete Methods
Modifier and Type	Method	Description
`<T extends Formula> T`	`callFunction(FunctionDeclaration<T> declaration, List<? extends Formula> args)`
`abstract TFormulaInfo`	`callFunctionImpl(TFuncDecl declaration, List<TFormulaInfo> args)`
`Object`	`convertValue(TFormulaInfo pF)`	Convert the formula into a Java object as far as possible, i.e., try to match a primitive or simple type like Boolean, BigInteger, Rational, or String.
`Object`	`convertValue(TFormulaInfo pAdditionalF, TFormulaInfo pF)`	Convert the formula into a Java object as far as possible, i.e., try to match a primitive or simple type.
`abstract TFuncDecl`	`declareUFImpl(String pName, TType pReturnType, List<TType> pArgTypes)`
`protected static String`	`dequote(String s)`	Variable names (symbols) can be wrapped with "\|".
`<T extends Formula> T`	`encapsulate(FormulaType<T> pType, TFormulaInfo pTerm)`
`protected <TI extends Formula,TE extends Formula> ArrayFormula<TI,TE>`	`encapsulateArray(TFormulaInfo pTerm, FormulaType<TI> pIndexType, FormulaType<TE> pElementType)`
`protected BitvectorFormula`	`encapsulateBitvector(TFormulaInfo pTerm)`
`BooleanFormula`	`encapsulateBoolean(TFormulaInfo pTerm)`
`protected EnumerationFormula`	`encapsulateEnumeration(TFormulaInfo pTerm)`
`protected FloatingPointFormula`	`encapsulateFloatingPoint(TFormulaInfo pTerm)`
`protected RegexFormula`	`encapsulateRegex(TFormulaInfo pTerm)`
`protected StringFormula`	`encapsulateString(TFormulaInfo pTerm)`
`Formula`	`encapsulateWithTypeOf(TFormulaInfo pTerm)`
`protected List<TFormulaInfo>`	`extractInfo(List<? extends Formula> input)`
`protected TFormulaInfo`	`extractInfo(Formula pT)`
`void`	`extractVariablesAndUFs(Formula pFormula, boolean extractUF, BiConsumer<String,Formula> pConsumer)`	Extract all free variables from the formula, optionally including UFs.
`Map<String,TFormulaInfo>`	`extractVariablesAndUFs(TFormulaInfo pFormula, boolean extractUFs)`	Wrapper for `extractVariablesAndUFs(Formula, boolean, BiConsumer)` which unwraps both input and output.
`void`	`extractVariablesAndUFs(TFormulaInfo pFormula, boolean extractUFs, BiConsumer<String,TFormulaInfo> pConsumer)`	Wrapper for `extractVariablesAndUFs(Formula, boolean, BiConsumer)` which unwraps both input and output.
`protected <TI extends Formula,TE extends Formula> FormulaType<TE>`	`getArrayFormulaElementType(ArrayFormula<TI,TE> pArray)`
`protected <TI extends Formula,TE extends Formula> FormulaType<TI>`	`getArrayFormulaIndexType(ArrayFormula<TI,TE> pArray)`
`abstract TType`	`getArrayType(TType indexType, TType elementType)`
`abstract TType`	`getBitvectorType(int bitwidth)`
`TFuncDecl`	`getBooleanVarDeclaration(BooleanFormula var)`
`protected abstract TFuncDecl`	`getBooleanVarDeclarationImpl(TFormulaInfo pTFormulaInfo)`
`TType`	`getBoolType()`
`TEnv`	`getEnv()`
`abstract TType`	`getFloatingPointType(FormulaType.FloatingPointType type)`
`protected <T extends Formula> FormulaType<T>`	`getFormulaType(T formula)`	Returns the type of the given Formula.
`abstract FormulaType<?>`	`getFormulaType(TFormulaInfo formula)`
`TType`	`getIntegerType()`
`TType`	`getRationalType()`
`TType`	`getRegexType()`
`TType`	`getStringType()`
`protected boolean`	`isCompatible(FormulaType<?> usedType, FormulaType<?> declaredType)`	This function checks whether the used type of the function argument is compatible with the declared type in the function declaration.
`abstract TFormulaInfo`	`makeVariable(TType type, String varName)`
`<T extends Formula> T`	`transformRecursively(FormulaVisitor<? extends Formula> pFormulaVisitor, T pF)`
`<T extends Formula> T`	`transformRecursively(FormulaVisitor<? extends Formula> pFormulaVisitor, T pF, Predicate<Object> shouldProcess)`
`<R> R`	`visit(Formula input, FormulaVisitor<R> visitor)`
`abstract <R> R`	`visit(FormulaVisitor<R> visitor, Formula formula, TFormulaInfo f)`
`void`	`visitRecursively(FormulaVisitor<TraversalProcess> pFormulaVisitor, Formula pF)`
`void`	`visitRecursively(FormulaVisitor<TraversalProcess> pFormulaVisitor, Formula pF, Predicate<Formula> shouldProcess)`

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

Field Detail
- environment
```
protected final TEnv environment
```

Constructor Detail

FormulaCreator

protected FormulaCreator(TEnv env,
                         TType boolType,
                         @Nullable TType pIntegerType,
                         @Nullable TType pRationalType,
                         @Nullable TType stringType,
                         @Nullable TType regexType)

Method Detail

getEnv
```
public final TEnv getEnv()
```

getBoolType
```
public final TType getBoolType()
```

getIntegerType
```
public final TType getIntegerType()
```

getRationalType
```
public final TType getRationalType()
```

getBitvectorType

public abstract TType getBitvectorType(int bitwidth)

getFloatingPointType

public abstract TType getFloatingPointType(FormulaType.FloatingPointType type)

getArrayType

public abstract TType getArrayType(TType indexType,
                                   TType elementType)

getStringType
```
public final TType getStringType()
```

getRegexType
```
public final TType getRegexType()
```

makeVariable

public abstract TFormulaInfo makeVariable(TType type,
                                          String varName)

encapsulateBoolean

public BooleanFormula encapsulateBoolean(TFormulaInfo pTerm)

encapsulateBitvector

protected BitvectorFormula encapsulateBitvector(TFormulaInfo pTerm)

encapsulateFloatingPoint

protected FloatingPointFormula encapsulateFloatingPoint(TFormulaInfo pTerm)

encapsulateArray

protected <TI extends Formula,TE extends Formula> ArrayFormula<TI,TE> encapsulateArray(TFormulaInfo pTerm,
                                                                                                   FormulaType<TI> pIndexType,
                                                                                                   FormulaType<TE> pElementType)

encapsulateString

protected StringFormula encapsulateString(TFormulaInfo pTerm)

encapsulateRegex

protected RegexFormula encapsulateRegex(TFormulaInfo pTerm)

encapsulateEnumeration

protected EnumerationFormula encapsulateEnumeration(TFormulaInfo pTerm)

encapsulateWithTypeOf

public Formula encapsulateWithTypeOf(TFormulaInfo pTerm)

encapsulate

public <T extends Formula> T encapsulate(FormulaType<T> pType,
                                         TFormulaInfo pTerm)

extractInfo

protected TFormulaInfo extractInfo(Formula pT)

getArrayFormulaElementType

protected <TI extends Formula,TE extends Formula> FormulaType<TE> getArrayFormulaElementType(ArrayFormula<TI,TE> pArray)

getArrayFormulaIndexType

protected <TI extends Formula,TE extends Formula> FormulaType<TI> getArrayFormulaIndexType(ArrayFormula<TI,TE> pArray)

getFormulaType

protected <T extends Formula> FormulaType<T> getFormulaType(T formula)

Returns the type of the given Formula.

getFormulaType

public abstract FormulaType<?> getFormulaType(TFormulaInfo formula)

visit

@CanIgnoreReturnValue
public <R> R visit(Formula input,
                   FormulaVisitor<R> visitor)

See Also:: FormulaManager.visit(org.sosy_lab.java_smt.api.Formula, org.sosy_lab.java_smt.api.visitors.FormulaVisitor<R>)

visit

public abstract <R> R visit(FormulaVisitor<R> visitor,
                            Formula formula,
                            TFormulaInfo f)

See Also:: FormulaManager.visit(org.sosy_lab.java_smt.api.Formula, org.sosy_lab.java_smt.api.visitors.FormulaVisitor<R>)

extractInfo

protected List<TFormulaInfo> extractInfo(List<? extends Formula> input)

visitRecursively
```
public void visitRecursively(FormulaVisitor<TraversalProcess> pFormulaVisitor,
                             Formula pF)
```
See Also:

FormulaManager.visitRecursively(org.sosy_lab.java_smt.api.Formula, org.sosy_lab.java_smt.api.visitors.FormulaVisitor<org.sosy_lab.java_smt.api.visitors.TraversalProcess>)

visitRecursively

public void visitRecursively(FormulaVisitor<TraversalProcess> pFormulaVisitor,
                             Formula pF,
                             Predicate<Formula> shouldProcess)

See Also:: FormulaManager.visitRecursively(org.sosy_lab.java_smt.api.Formula, org.sosy_lab.java_smt.api.visitors.FormulaVisitor<org.sosy_lab.java_smt.api.visitors.TraversalProcess>)

transformRecursively

public <T extends Formula> T transformRecursively(FormulaVisitor<? extends Formula> pFormulaVisitor,
                                                  T pF)

transformRecursively

public <T extends Formula> T transformRecursively(FormulaVisitor<? extends Formula> pFormulaVisitor,
                                                  T pF,
                                                  Predicate<Object> shouldProcess)

extractVariablesAndUFs

public Map<String,TFormulaInfo> extractVariablesAndUFs(TFormulaInfo pFormula,
                                                             boolean extractUFs)

Wrapper for extractVariablesAndUFs(Formula, boolean, BiConsumer) which unwraps both input and output.

extractVariablesAndUFs

public void extractVariablesAndUFs(TFormulaInfo pFormula,
                                   boolean extractUFs,
                                   BiConsumer<String,TFormulaInfo> pConsumer)

Wrapper for extractVariablesAndUFs(Formula, boolean, BiConsumer) which unwraps both input and output.

extractVariablesAndUFs

public void extractVariablesAndUFs(Formula pFormula,
                                   boolean extractUF,
                                   BiConsumer<String,Formula> pConsumer)

Extract all free variables from the formula, optionally including UFs.

callFunction

public final <T extends Formula> T callFunction(FunctionDeclaration<T> declaration,
                                                List<? extends Formula> args)

isCompatible
```
protected boolean isCompatible(FormulaType<?> usedType,
                               FormulaType<?> declaredType)
```
This function checks whether the used type of the function argument is compatible with the declared type in the function declaration.
Identical types are always compatible, a subtype like INT to supertype RATIONAL is also compatible. A solver-specific wrapper can override this method if it does an explicit transformation between (some) types, e.g., from BV to BOOLEAN or from BOOLEAN to INT.

callFunctionImpl

public abstract TFormulaInfo callFunctionImpl(TFuncDecl declaration,
                                              List<TFormulaInfo> args)

declareUFImpl

public abstract TFuncDecl declareUFImpl(String pName,
                                        TType pReturnType,
                                        List<TType> pArgTypes)

getBooleanVarDeclaration

public TFuncDecl getBooleanVarDeclaration(BooleanFormula var)

getBooleanVarDeclarationImpl

protected abstract TFuncDecl getBooleanVarDeclarationImpl(TFormulaInfo pTFormulaInfo)

convertValue
```
public Object convertValue(TFormulaInfo pF)
```
Convert the formula into a Java object as far as possible, i.e., try to match a primitive or simple type like Boolean, BigInteger, Rational, or String.
If the formula is not a simple constant expression, we simply return null.

Parameters:

pF - the formula to be converted.

convertValue
```
public Object convertValue(TFormulaInfo pAdditionalF,
                           TFormulaInfo pF)
```
Convert the formula into a Java object as far as possible, i.e., try to match a primitive or simple type.

Parameters:

pAdditionalF - an additional formula where the type can be received from.

pF - the formula to be converted.

dequote
```
protected static String dequote(String s)
```
Variable names (symbols) can be wrapped with "|". This function removes those chars.

Class FormulaCreator<TFormulaInfo,​TType,​TEnv,​TFuncDecl>

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

environment

Constructor Detail

FormulaCreator

Method Detail

getEnv

getBoolType

getIntegerType

getRationalType

getBitvectorType

getFloatingPointType

getArrayType

getStringType

getRegexType

makeVariable

encapsulateBoolean

encapsulateBitvector

encapsulateFloatingPoint

encapsulateArray

encapsulateString

encapsulateRegex

encapsulateEnumeration

encapsulateWithTypeOf

encapsulate

extractInfo

getArrayFormulaElementType

getArrayFormulaIndexType

getFormulaType

getFormulaType

visit

visit

extractInfo

visitRecursively

visitRecursively

transformRecursively

transformRecursively

extractVariablesAndUFs

extractVariablesAndUFs

extractVariablesAndUFs

callFunction

isCompatible

callFunctionImpl

declareUFImpl

getBooleanVarDeclaration

getBooleanVarDeclarationImpl

convertValue

convertValue

dequote

Class FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>