Interface FormulaVisitor<R>
-
- Type Parameters:
R
- Desired return type.
- All Known Implementing Classes:
DefaultFormulaVisitor
,ExpectedFormulaVisitor
,FormulaTransformationVisitor
public interface FormulaVisitor<R>
Visitor iterating through entire formula. UseFormulaManager.visit(org.sosy_lab.java_smt.api.Formula, org.sosy_lab.java_smt.api.visitors.FormulaVisitor<R>)
for visiting formulas.
-
-
Method Summary
All Methods Instance Methods Abstract Methods Modifier and Type Method Description R
visitBoundVariable(Formula f, int deBruijnIdx)
Visit a variable bound by a quantifier.R
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".R
visitFreeVariable(Formula f, String name)
Visit a free variable (such as "x", "y" or "z"), not bound by a quantifier.R
visitFunction(Formula f, List<Formula> args, FunctionDeclaration<?> functionDeclaration)
Visit an arbitrary, potentially uninterpreted function.R
visitQuantifier(BooleanFormula f, QuantifiedFormulaManager.Quantifier quantifier, List<Formula> boundVariables, BooleanFormula body)
Visit a quantified node.
-
-
-
Method Detail
-
visitFreeVariable
R visitFreeVariable(Formula f, String name)
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).- Parameters:
f
- Formula representing the variable.name
- Variable name.
-
visitBoundVariable
R visitBoundVariable(Formula f, int deBruijnIdx)
Visit a variable bound by a quantifier. The variable can have any sort (both boolean and non-boolean).- Parameters:
f
- Formula representing the variable.deBruijnIdx
- de-Bruijn index of the bound variable, which can be used to find the matching quantifier.
-
visitConstant
R 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".- 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
R visitFunction(Formula f, List<Formula> args, FunctionDeclaration<?> functionDeclaration)
Visit an arbitrary, potentially uninterpreted function. The function can have any sort.- Parameters:
f
- Input function.args
- List of argumentsfunctionDeclaration
- Function declaration. Can be given toFormulaManager.makeApplication(org.sosy_lab.java_smt.api.FunctionDeclaration<T>, java.util.List<? extends org.sosy_lab.java_smt.api.Formula>)
to construct a new instance of the same function with different arguments.
-
visitQuantifier
R visitQuantifier(BooleanFormula f, QuantifiedFormulaManager.Quantifier quantifier, List<Formula> boundVariables, BooleanFormula body)
Visit a quantified node.- 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.body
- Body of the quantifier.
-
-