Interface BooleanFormulaVisitor<R>
-
- Type Parameters:
R
- Desired return type.
- All Known Implementing Classes:
BooleanFormulaTransformationVisitor
,DefaultBooleanFormulaVisitor
,NNFVisitor
public interface BooleanFormulaVisitor<R>
Visitor iterating through the boolean part of the formula. UseBooleanFormulaManager.visit(org.sosy_lab.java_smt.api.BooleanFormula, org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor<R>)
for visiting formulas.
-
-
Method Summary
All Methods Instance Methods Abstract Methods Modifier and Type Method Description R
visitAnd(List<BooleanFormula> operands)
Visit an AND-expression with an arbitrary number of boolean arguments.R
visitAtom(BooleanFormula atom, FunctionDeclaration<BooleanFormula> funcDecl)
Visit an SMT atom.R
visitBoundVar(BooleanFormula var, int deBruijnIdx)
Visit a boolean variable bound by a quantifier.R
visitConstant(boolean value)
Visit a constant with a given value.R
visitEquivalence(BooleanFormula operand1, BooleanFormula operand2)
Visit an equivalence between two formulas of boolean sort:operand1 = operand2
.R
visitIfThenElse(BooleanFormula condition, BooleanFormula thenFormula, BooleanFormula elseFormula)
Visit an if-then-else expression.R
visitImplication(BooleanFormula operand1, BooleanFormula operand2)
Visit an implication.R
visitNot(BooleanFormula operand)
Visit a NOT-expression.R
visitOr(List<BooleanFormula> operands)
Visit an OR-expression with an arbitrary number of boolean arguments.R
visitQuantifier(QuantifiedFormulaManager.Quantifier quantifier, BooleanFormula quantifiedAST, List<Formula> boundVars, BooleanFormula body)
Visit a quantifier: forall- or exists-.R
visitXor(BooleanFormula operand1, BooleanFormula operand2)
Visit a XOR-expression.
-
-
-
Method Detail
-
visitConstant
R visitConstant(boolean value)
Visit a constant with a given value.
-
visitBoundVar
R visitBoundVar(BooleanFormula var, int deBruijnIdx)
Visit a boolean variable bound by a quantifier.
-
visitNot
R visitNot(BooleanFormula operand)
Visit a NOT-expression.- Parameters:
operand
- Negated term.- See Also:
BooleanFormulaManager.not(org.sosy_lab.java_smt.api.BooleanFormula)
-
visitAnd
R visitAnd(List<BooleanFormula> operands)
Visit an AND-expression with an arbitrary number of boolean arguments.An AND-expression with zero arguments is equisatisfiable to 'TRUE'. An AND-expression with one argument is equal to the argument itself. In all other cases, default boolean logic applies.
-
visitOr
R visitOr(List<BooleanFormula> operands)
Visit an OR-expression with an arbitrary number of boolean arguments.An OR-expression with zero arguments is equisatisfiable to 'TRUE'. An OR-expression with one argument is equal to the argument itself. In all other cases, default boolean logic applies.
-
visitXor
R visitXor(BooleanFormula operand1, BooleanFormula operand2)
Visit a XOR-expression.
-
visitEquivalence
R visitEquivalence(BooleanFormula operand1, BooleanFormula operand2)
Visit an equivalence between two formulas of boolean sort:operand1 = operand2
.
-
visitImplication
R visitImplication(BooleanFormula operand1, BooleanFormula operand2)
Visit an implication.
-
visitIfThenElse
R visitIfThenElse(BooleanFormula condition, BooleanFormula thenFormula, BooleanFormula elseFormula)
Visit an if-then-else expression.
-
visitQuantifier
R visitQuantifier(QuantifiedFormulaManager.Quantifier quantifier, BooleanFormula quantifiedAST, List<Formula> boundVars, BooleanFormula body)
Visit a quantifier: forall- or exists-.- Parameters:
quantifier
- Quantifier type: FORALL- or EXISTS-quantifiedAST
- AST of the quantified node. Provided because it is difficult to re-create from the parameters.boundVars
- Variables bound by this quantifier.body
- Body of the quantified expression.- See Also:
QuantifiedFormulaManager.mkQuantifier(org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier, java.util.List<? extends org.sosy_lab.java_smt.api.Formula>, org.sosy_lab.java_smt.api.BooleanFormula)
,QuantifiedFormulaManager.forall(java.util.List<? extends org.sosy_lab.java_smt.api.Formula>, org.sosy_lab.java_smt.api.BooleanFormula)
,QuantifiedFormulaManager.exists(java.util.List<? extends org.sosy_lab.java_smt.api.Formula>, org.sosy_lab.java_smt.api.BooleanFormula)
-
visitAtom
R visitAtom(BooleanFormula atom, FunctionDeclaration<BooleanFormula> funcDecl)
Visit an SMT atom. An atom can be a theory expression, constant, or a variable.This is anything with a boolean sort which is not covered by the cases above.
-
-