Class FormulaTransformationVisitor
- java.lang.Object
-
- org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor
-
- All Implemented Interfaces:
FormulaVisitor<Formula>
public abstract class FormulaTransformationVisitor extends Object implements FormulaVisitor<Formula>
Abstract class for formula transformation.
-
-
Constructor Summary
Constructors Modifier Constructor Description protected
FormulaTransformationVisitor(FormulaManager fmgr)
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description Formula
visitBoundVariable(Formula f, int deBruijnIdx)
Visit a variable bound by a quantifier.Formula
visitConstant(Formula f, Object value)
Visit a constant, such as "true"/"false", a numeric constant like "1" or "1.0", a String constant like 2hello world" or enumeration constant like "Blue".Formula
visitFreeVariable(Formula f, String name)
Visit a free variable (such as "x", "y" or "z"), not bound by a quantifier.Formula
visitFunction(Formula f, List<Formula> newArgs, FunctionDeclaration<?> functionDeclaration)
Visit an arbitrary, potentially uninterpreted function.BooleanFormula
visitQuantifier(BooleanFormula f, QuantifiedFormulaManager.Quantifier quantifier, List<Formula> boundVariables, BooleanFormula transformedBody)
Visit a quantified node.
-
-
-
Constructor Detail
-
FormulaTransformationVisitor
protected FormulaTransformationVisitor(FormulaManager fmgr)
-
-
Method Detail
-
visitFreeVariable
public Formula visitFreeVariable(Formula f, String name)
Description copied from interface:FormulaVisitor
Visit a free variable (such as "x", "y" or "z"), not bound by a quantifier. The variable can have any sort (both boolean and non-boolean).- Specified by:
visitFreeVariable
in interfaceFormulaVisitor<Formula>
- Parameters:
f
- Formula representing the variable.name
- Variable name.
-
visitBoundVariable
public Formula visitBoundVariable(Formula f, int deBruijnIdx)
Description copied from interface:FormulaVisitor
Visit a variable bound by a quantifier. The variable can have any sort (both boolean and non-boolean).- Specified by:
visitBoundVariable
in interfaceFormulaVisitor<Formula>
- Parameters:
f
- Formula representing the variable.deBruijnIdx
- de-Bruijn index of the bound variable, which can be used to find the matching quantifier.
-
visitConstant
public Formula visitConstant(Formula f, Object value)
Description copied from interface:FormulaVisitor
Visit a constant, such as "true"/"false", a numeric constant like "1" or "1.0", a String constant like 2hello world" or enumeration constant like "Blue".- Specified by:
visitConstant
in interfaceFormulaVisitor<Formula>
- Parameters:
f
- Formula representing the constant.value
- The value of the constant. It is either of typeBoolean
, of a subtype ofNumber
(mostly aBigInteger
, aBigDecimal
, or aRational
), orString
.- Returns:
- An arbitrary return value that is passed to the caller.
-
visitFunction
public Formula visitFunction(Formula f, List<Formula> newArgs, FunctionDeclaration<?> functionDeclaration)
Description copied from interface:FormulaVisitor
Visit an arbitrary, potentially uninterpreted function. The function can have any sort.- Specified by:
visitFunction
in interfaceFormulaVisitor<Formula>
- Parameters:
f
- Input function.newArgs
- New arguments after the transformationfunctionDeclaration
- Function declaration- Returns:
- Transformed function.
-
visitQuantifier
public BooleanFormula visitQuantifier(BooleanFormula f, QuantifiedFormulaManager.Quantifier quantifier, List<Formula> boundVariables, BooleanFormula transformedBody)
Description copied from interface:FormulaVisitor
Visit a quantified node.- Specified by:
visitQuantifier
in interfaceFormulaVisitor<Formula>
- Parameters:
f
- Quantifier formula.quantifier
- Quantifier type: eitherFORALL
orEXISTS
.boundVariables
- Variables bound by the quantifier. NOTE: not all solvers hold metadata about bound variables. In case this is not available, this method will be called with an empty list, yet#mkQuantifier
will work fine with an empty list as well.transformedBody
- Quantifier body already transformed by the visitor.- Returns:
- Transformed AST
-
-