Interface FormulaManager
-
- All Known Implementing Classes:
AbstractFormulaManager
,DebuggingFormulaManager
public interface FormulaManager
FormulaManager class contains all operations which can be performed on formulas.
-
-
Method Summary
All Methods Instance Methods Abstract Methods Modifier and Type Method Description BooleanFormula
applyTactic(BooleanFormula input, Tactic tactic)
Apply a tactic which performs formula transformation.Appender
dumpFormula(BooleanFormula pT)
Serialize an input formula to an SMT-LIB format.String
escape(String variableName)
Get an escaped symbol/name for variables or undefined functions, if necessary.ImmutableMap<String,Formula>
extractVariables(Formula f)
Extract the names of all free variables and UFs in a formula.ImmutableMap<String,Formula>
extractVariablesAndUFs(Formula f)
Extract the names of all free variables and UFs in a formula.ArrayFormulaManager
getArrayFormulaManager()
Returns the Array-Theory.BitvectorFormulaManager
getBitvectorFormulaManager()
Returns the Bitvector-Theory.BooleanFormulaManager
getBooleanFormulaManager()
Returns the Boolean-Theory.EnumerationFormulaManager
getEnumerationFormulaManager()
Returns the Enumeration Theory, e.g., also known as 'limited domain'.FloatingPointFormulaManager
getFloatingPointFormulaManager()
Returns the Floating-Point-Theory.<T extends Formula>
FormulaType<T>getFormulaType(T formula)
Returns the type of the given Formula.IntegerFormulaManager
getIntegerFormulaManager()
Returns the Integer-Theory.QuantifiedFormulaManager
getQuantifiedFormulaManager()
Returns the interface for handling quantifiers.RationalFormulaManager
getRationalFormulaManager()
Returns the Rational-Theory.SLFormulaManager
getSLFormulaManager()
Returns the Seperation-Logic-Theory.StringFormulaManager
getStringFormulaManager()
Returns the String Theory.UFManager
getUFManager()
Returns the function for dealing with uninterpreted functions (UFs).boolean
isValidName(String variableName)
Check whether the given String can be used as symbol/name for variables or undefined functions.<T extends Formula>
TmakeApplication(FunctionDeclaration<T> declaration, List<? extends Formula> args)
Create a function application to the given list of arguments.<T extends Formula>
TmakeApplication(FunctionDeclaration<T> declaration, Formula... args)
Create a function application to the given list of arguments.<T extends Formula>
TmakeVariable(FormulaType<T> formulaType, String name)
Create variable of the type equal toformulaType
.BooleanFormula
parse(String s)
Parse a boolean formula given as a String in an SMTLIB file format.<T extends Formula>
Tsimplify(T input)
Simplify an input formula, while ensuring equivalence.<T extends Formula>
Tsubstitute(T f, Map<? extends Formula,? extends Formula> fromToMapping)
Substitute every occurrence of any item fromchangeFrom
in formulaf
to the corresponding occurrence fromchangeTo
.<T extends Formula>
TtransformRecursively(T f, FormulaTransformationVisitor pFormulaVisitor)
Visit the formula recursively with a givenFormulaVisitor
.BooleanFormula
translateFrom(BooleanFormula formula, FormulaManager otherManager)
Translates the formula from another context into the context represented bythis
.String
unescape(String variableName)
Unescape the symbol/name for variables or undefined functions, if necessary.<R> R
visit(Formula f, FormulaVisitor<R> rFormulaVisitor)
Visit the formula with a given visitor.void
visitRecursively(Formula f, FormulaVisitor<TraversalProcess> rFormulaVisitor)
Visit the formula recursively with a givenFormulaVisitor
.
-
-
-
Method Detail
-
getIntegerFormulaManager
IntegerFormulaManager getIntegerFormulaManager()
Returns the Integer-Theory. Because most SAT-solvers support automatic casting between Integer- and Rational-Theory, the Integer- and the RationalFormulaManager both return the same Formulas for numeric operations like ADD, SUBTRACT, TIMES, LESSTHAN, EQUAL and others.- Throws:
UnsupportedOperationException
- If the theory is not supported by the solver.
-
getRationalFormulaManager
RationalFormulaManager getRationalFormulaManager()
Returns the Rational-Theory. Because most SAT-solvers support automatic casting between Integer- and Rational-Theory, the Integer- and the RationalFormulaManager both return the same Formulas for numeric operations like ADD, SUBTRACT, TIMES, LESSTHAN, EQUAL, etc.- Throws:
UnsupportedOperationException
- If the theory is not supported by the solver.
-
getBooleanFormulaManager
BooleanFormulaManager getBooleanFormulaManager()
Returns the Boolean-Theory.
-
getArrayFormulaManager
ArrayFormulaManager getArrayFormulaManager()
Returns the Array-Theory.- Throws:
UnsupportedOperationException
- If the theory is not supported by the solver.
-
getBitvectorFormulaManager
BitvectorFormulaManager getBitvectorFormulaManager()
Returns the Bitvector-Theory.- Throws:
UnsupportedOperationException
- If the theory is not supported by the solver.
-
getFloatingPointFormulaManager
FloatingPointFormulaManager getFloatingPointFormulaManager()
Returns the Floating-Point-Theory.- Throws:
UnsupportedOperationException
- If the theory is not supported by the solver.
-
getUFManager
UFManager getUFManager()
Returns the function for dealing with uninterpreted functions (UFs).
-
getSLFormulaManager
SLFormulaManager getSLFormulaManager()
Returns the Seperation-Logic-Theory.- Throws:
UnsupportedOperationException
- If the theory is not supported by the solver.
-
getQuantifiedFormulaManager
QuantifiedFormulaManager getQuantifiedFormulaManager()
Returns the interface for handling quantifiers.- Throws:
UnsupportedOperationException
- If the theory is not supported by the solver.
-
getStringFormulaManager
StringFormulaManager getStringFormulaManager()
Returns the String Theory.- Throws:
UnsupportedOperationException
- If the theory is not supported by the solver.
-
getEnumerationFormulaManager
EnumerationFormulaManager getEnumerationFormulaManager()
Returns the Enumeration Theory, e.g., also known as 'limited domain'.- Throws:
UnsupportedOperationException
- If the theory is not supported by the solver.
-
makeVariable
<T extends Formula> T makeVariable(FormulaType<T> formulaType, String name)
Create variable of the type equal toformulaType
.- Parameters:
formulaType
- the type of the variable.name
- the name of the variable.- Returns:
- the created variable.
-
makeApplication
<T extends Formula> T makeApplication(FunctionDeclaration<T> declaration, List<? extends Formula> args)
Create a function application to the given list of arguments.- Parameters:
declaration
- Function declarationargs
- List of arguments- Returns:
- Constructed formula
-
makeApplication
<T extends Formula> T makeApplication(FunctionDeclaration<T> declaration, Formula... args)
Create a function application to the given list of arguments.- Parameters:
declaration
- Function declarationargs
- List of arguments- Returns:
- Constructed formula
-
getFormulaType
<T extends Formula> FormulaType<T> getFormulaType(T formula)
Returns the type of the given Formula.
-
parse
BooleanFormula parse(String s) throws IllegalArgumentException
Parse a boolean formula given as a String in an SMTLIB file format. We expect exactly one assertion to be contained in the query.Example:
(declare-fun x () Int)(assert (= 0 x))
It depends on the used SMT solver whether the given query must be self-contained and include declarations for all used symbols or not, and also whether the query is allowed to contain symbols with equal name, but different type/sort than existing symbols. The safest way is to always declare all used symbols and to avoid conflicting types for them.
The behavior of the SMT solver is undefined if commands are provided in the SMTLIB-based String that are different from declarations or an assertion, such as
push/pop
orset-info
. Most solvers just ignore those commands.Variables that are defined, but not used in the assertion, might be ignored by the SMT solver and they might not be available for later usage.
- Returns:
- A single formula from the assertion in the internal representation.
- Throws:
IllegalArgumentException
- If the string cannot be parsed.
-
dumpFormula
Appender dumpFormula(BooleanFormula pT)
Serialize an input formula to an SMT-LIB format. Very useful when passing formulas between different solvers.To get a String, simply call
Object.toString()
on the returned object. This method is lazy and does not create an output string until the returned object is actually used.- Returns:
- SMT-LIB formula serialization.
-
applyTactic
BooleanFormula applyTactic(BooleanFormula input, Tactic tactic) throws InterruptedException
Apply a tactic which performs formula transformation. The available tactics depend on the used solver.- Throws:
InterruptedException
-
simplify
<T extends Formula> T simplify(T input) throws InterruptedException
Simplify an input formula, while ensuring equivalence.For solvers that do not provide a simplification API, an original formula is returned.
- Parameters:
input
- The input formula- Returns:
- Simplified version of the formula
- Throws:
InterruptedException
-
visit
@CanIgnoreReturnValue <R> R visit(Formula f, FormulaVisitor<R> rFormulaVisitor)
Visit the formula with a given visitor.This method does not recursively visit sub-components of a formula its own, so the given
FormulaVisitor
needs to call such visitation on its own.Please be aware that calling this method might cause extensive stack usage depending on the nesting of the given formula and the given
FormulaVisitor
. Additionally, sub-formulas that are used several times in the formula might be visited several times. For an efficient formula traversing, we also providevisitRecursively(Formula, FormulaVisitor)
.- Parameters:
f
- formula to be visitedrFormulaVisitor
- an implementation that provides steps for each kind of formula.
-
visitRecursively
void visitRecursively(Formula f, FormulaVisitor<TraversalProcess> rFormulaVisitor)
Visit the formula recursively with a givenFormulaVisitor
. This method traverses sub-components of a formula automatically, depending on the return value of theTraversalProcess
in the givenFormulaVisitor
.This method guarantees that the traversal is done iteratively, without using Java recursion, and thus is not prone to StackOverflowErrors.
Furthermore, this method also guarantees that every equal part of the formula is visited only once. Thus, it can be used to traverse DAG-like formulas efficiently.
The traversal is done in PRE-ORDER manner with regard to caching identical subtrees, i.e., a parent will be visited BEFORE its children. The unmodified child-formulas are passed as argument to the parent's visitation.
-
transformRecursively
<T extends Formula> T transformRecursively(T f, FormulaTransformationVisitor pFormulaVisitor)
Visit the formula recursively with a givenFormulaVisitor
.This method guarantees that the traversal is done iteratively, without using Java recursion, and thus is not prone to StackOverflowErrors.
Furthermore, this method also guarantees that every equal part of the formula is visited only once. Thus, it can be used to traverse DAG-like formulas efficiently.
The traversal is done in POST-ORDER manner with regard to caching identical subtrees, i.e., a parent will be visited AFTER its children. The result of the child-visitation is passed as argument to the parent's visitation.
- Parameters:
pFormulaVisitor
- Transformation described by the user.
-
extractVariables
ImmutableMap<String,Formula> extractVariables(Formula f)
Extract the names of all free variables and UFs in a formula.- Parameters:
f
- The input formula- Returns:
- Map from variable names to the corresponding formulas.
-
extractVariablesAndUFs
ImmutableMap<String,Formula> extractVariablesAndUFs(Formula f)
Extract the names of all free variables and UFs in a formula.- Parameters:
f
- The input formula- Returns:
- Map from variable names to the corresponding formulas. If an UF occurs multiple times in the input formula, an arbitrary instance of an application of this UF is in the map.
-
substitute
<T extends Formula> T substitute(T f, Map<? extends Formula,? extends Formula> fromToMapping)
Substitute every occurrence of any item fromchangeFrom
in formulaf
to the corresponding occurrence fromchangeTo
.E.g. if
changeFrom
contains a variablea
andchangeTo
contains a variableb
all occurrences ofa
will be changed tob
in the returned formula.- Parameters:
f
- Formula to change.fromToMapping
- Mapping of old and new formula parts.- Returns:
- Formula with parts replaced.
-
translateFrom
BooleanFormula translateFrom(BooleanFormula formula, FormulaManager otherManager)
Translates the formula from another context into the context represented bythis
. Default implementation relies on string serialization (dumpFormula(BooleanFormula)
andparse(String)
), but each solver may implement more efficient translation between its own contexts.- Parameters:
formula
- Formula belonging tootherContext
.otherManager
- Formula manager belonging to the other context.- Returns:
- Formula belonging to
this
context.
-
isValidName
boolean isValidName(String variableName)
Check whether the given String can be used as symbol/name for variables or undefined functions.We explicitly state that with further development of SMT solvers and the SMTLib specification, the list of forbidden variable names may change in the future. Users should if possible not use logical or mathematical operators, or keywords strongly depending on SMTlib.
If a variable name is rejected, a possibility is escaping, e.g. either substituting the whole variable name or just every invalid character with an escaped form. We recommend using an escape sequence based on the token "JAVASMT", because it might be unusual enough to appear when encoding a user's problem in SMT. Please note that you might also have to handle escaping the escape sequence. Examples:
- the invalid variable name
"="
(logical operator for equality) can be replaced with a string"JAVASMT_EQUALS"
. - the invalid SMTlib-escaped variable name
"|test|"
(the solver SMTInterpol does not allow the pipe symbol"|"
in names) can be replaced with"JAVASMT_PIPEtestJAVASMT_PIPE"
.
- the invalid variable name
-
escape
String escape(String variableName)
Get an escaped symbol/name for variables or undefined functions, if necessary.See
isValidName(String)
for further details.
-
unescape
String unescape(String variableName)
Unescape the symbol/name for variables or undefined functions, if necessary.The result is undefined for Strings that are not properly escaped.
See
isValidName(String)
for further details.
-
-