Class BooleanFormulaTransformationVisitor
- java.lang.Object
-
- org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor
-
- All Implemented Interfaces:
BooleanFormulaVisitor<BooleanFormula>
- Direct Known Subclasses:
NNFVisitor
public abstract class BooleanFormulaTransformationVisitor extends Object implements BooleanFormulaVisitor<BooleanFormula>
Base class for visitors for boolean formulas that recursively transform boolean formulas.
-
-
Constructor Summary
Constructors Modifier Constructor Description protected
BooleanFormulaTransformationVisitor(FormulaManager pMgr)
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description BooleanFormula
visitAnd(List<BooleanFormula> processedOperands)
Visit an AND-expression with an arbitrary number of boolean arguments.BooleanFormula
visitAtom(BooleanFormula pAtom, FunctionDeclaration<BooleanFormula> decl)
Visit an SMT atom.BooleanFormula
visitBoundVar(BooleanFormula var, int deBruijnIdx)
Visit a boolean variable bound by a quantifier.BooleanFormula
visitConstant(boolean value)
Visit a constant with a given value.BooleanFormula
visitEquivalence(BooleanFormula processedOperand1, BooleanFormula processedOperand2)
Visit an equivalence between two formulas of boolean sort:operand1 = operand2
.BooleanFormula
visitIfThenElse(BooleanFormula processedCondition, BooleanFormula processedThenFormula, BooleanFormula processedElseFormula)
Visit an if-then-else expression.BooleanFormula
visitImplication(BooleanFormula processedOperand1, BooleanFormula processedOperand2)
Visit an implication.BooleanFormula
visitNot(BooleanFormula processedOperand)
Visit a NOT-expression.BooleanFormula
visitOr(List<BooleanFormula> processedOperands)
Visit an OR-expression with an arbitrary number of boolean arguments.BooleanFormula
visitQuantifier(QuantifiedFormulaManager.Quantifier quantifier, BooleanFormula quantifiedAST, List<Formula> boundVars, BooleanFormula processedBody)
Visit a quantifier: forall- or exists-.BooleanFormula
visitXor(BooleanFormula processedOperand1, BooleanFormula processedOperand2)
Visit a XOR-expression.
-
-
-
Constructor Detail
-
BooleanFormulaTransformationVisitor
protected BooleanFormulaTransformationVisitor(FormulaManager pMgr)
-
-
Method Detail
-
visitConstant
public BooleanFormula visitConstant(boolean value)
Description copied from interface:BooleanFormulaVisitor
Visit a constant with a given value.- Specified by:
visitConstant
in interfaceBooleanFormulaVisitor<BooleanFormula>
- See Also:
BooleanFormulaManager.makeBoolean(boolean)
-
visitBoundVar
public BooleanFormula visitBoundVar(BooleanFormula var, int deBruijnIdx)
Description copied from interface:BooleanFormulaVisitor
Visit a boolean variable bound by a quantifier.- Specified by:
visitBoundVar
in interfaceBooleanFormulaVisitor<BooleanFormula>
-
visitAtom
public BooleanFormula visitAtom(BooleanFormula pAtom, FunctionDeclaration<BooleanFormula> decl)
Description copied from interface:BooleanFormulaVisitor
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.
- Specified by:
visitAtom
in interfaceBooleanFormulaVisitor<BooleanFormula>
-
visitNot
public BooleanFormula visitNot(BooleanFormula processedOperand)
Description copied from interface:BooleanFormulaVisitor
Visit a NOT-expression.- Specified by:
visitNot
in interfaceBooleanFormulaVisitor<BooleanFormula>
- Parameters:
processedOperand
- Negated term.- See Also:
BooleanFormulaManager.not(org.sosy_lab.java_smt.api.BooleanFormula)
-
visitAnd
public BooleanFormula visitAnd(List<BooleanFormula> processedOperands)
Description copied from interface:BooleanFormulaVisitor
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.
- Specified by:
visitAnd
in interfaceBooleanFormulaVisitor<BooleanFormula>
- See Also:
BooleanFormulaManager.and(org.sosy_lab.java_smt.api.BooleanFormula, org.sosy_lab.java_smt.api.BooleanFormula)
-
visitOr
public BooleanFormula visitOr(List<BooleanFormula> processedOperands)
Description copied from interface:BooleanFormulaVisitor
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.
- Specified by:
visitOr
in interfaceBooleanFormulaVisitor<BooleanFormula>
- See Also:
BooleanFormulaManager.or(org.sosy_lab.java_smt.api.BooleanFormula, org.sosy_lab.java_smt.api.BooleanFormula)
-
visitXor
public BooleanFormula visitXor(BooleanFormula processedOperand1, BooleanFormula processedOperand2)
Description copied from interface:BooleanFormulaVisitor
Visit a XOR-expression.- Specified by:
visitXor
in interfaceBooleanFormulaVisitor<BooleanFormula>
- See Also:
BooleanFormulaManager.xor(org.sosy_lab.java_smt.api.BooleanFormula, org.sosy_lab.java_smt.api.BooleanFormula)
-
visitEquivalence
public BooleanFormula visitEquivalence(BooleanFormula processedOperand1, BooleanFormula processedOperand2)
Description copied from interface:BooleanFormulaVisitor
Visit an equivalence between two formulas of boolean sort:operand1 = operand2
.
-
visitImplication
public BooleanFormula visitImplication(BooleanFormula processedOperand1, BooleanFormula processedOperand2)
Description copied from interface:BooleanFormulaVisitor
Visit an implication.
-
visitIfThenElse
public BooleanFormula visitIfThenElse(BooleanFormula processedCondition, BooleanFormula processedThenFormula, BooleanFormula processedElseFormula)
Description copied from interface:BooleanFormulaVisitor
Visit an if-then-else expression.- Specified by:
visitIfThenElse
in interfaceBooleanFormulaVisitor<BooleanFormula>
- See Also:
BooleanFormulaManager.ifThenElse(org.sosy_lab.java_smt.api.BooleanFormula, T, T)
-
visitQuantifier
public BooleanFormula visitQuantifier(QuantifiedFormulaManager.Quantifier quantifier, BooleanFormula quantifiedAST, List<Formula> boundVars, BooleanFormula processedBody)
Description copied from interface:BooleanFormulaVisitor
Visit a quantifier: forall- or exists-.- Specified by:
visitQuantifier
in interfaceBooleanFormulaVisitor<BooleanFormula>
- 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.processedBody
- 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)
-
-