Package org.sosy_lab.java_smt.api.visitors

Class DefaultFormulaVisitor<R>

java.lang.Object

org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor<R>

All Implemented Interfaces:

FormulaVisitor<R>

Direct Known Subclasses:

ExpectedFormulaVisitor

public abstract class DefaultFormulaVisitor<R>
extends Object
implements FormulaVisitor<R>

Constructor Summary

Constructors

Constructor	Description
DefaultFormulaVisitor()

Method Summary

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".
protected abstract R	visitDefault(Formula f)	Method for default case, is called by all methods from this class if they are not overridden.
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 q, List<Formula> boundVariables, BooleanFormula body)	Visit a quantified node.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

DefaultFormulaVisitor

public DefaultFormulaVisitor()

Method Detail

visitDefault

protected abstract R visitDefault(Formula f)

Method for default case, is called by all methods from this class if they are not overridden.

Parameters:

f - Formula for the currently visited node.

Returns:

An arbitrary value, will be passed through to the caller.

visitFreeVariable

public R 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 interface FormulaVisitor<R>

Parameters:

f - Formula representing the variable.

name - Variable name.

visitBoundVariable

public R 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 interface FormulaVisitor<R>

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 R 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 interface FormulaVisitor<R>

Parameters:

f - Formula representing the constant.

value - The value of the constant. It is either of type Boolean, of a subtype of Number (mostly a BigInteger, a BigDecimal, or a Rational), or String.

Returns:

An arbitrary return value that is passed to the caller.

visitFunction

public R visitFunction(Formula f,
                       List<Formula> args,
                       FunctionDeclaration<?> functionDeclaration)

Description copied from interface: FormulaVisitor

Visit an arbitrary, potentially uninterpreted function. The function can have any sort.

Specified by:

visitFunction in interface FormulaVisitor<R>

Parameters:

f - Input function.

args - List of arguments

functionDeclaration - Function declaration. Can be given to FormulaManager.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

public R visitQuantifier(BooleanFormula f,
                         QuantifiedFormulaManager.Quantifier q,
                         List<Formula> boundVariables,
                         BooleanFormula body)

Description copied from interface: FormulaVisitor

Visit a quantified node.

Specified by:

visitQuantifier in interface FormulaVisitor<R>

Parameters:

f - Quantifier formula.

q - Quantifier type: either FORALL or EXISTS.

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.