Package org.sosy_lab.java_smt.basicimpl.tactics

Class NNFVisitor

java.lang.Object

org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor

org.sosy_lab.java_smt.basicimpl.tactics.NNFVisitor

All Implemented Interfaces:

BooleanFormulaVisitor<BooleanFormula>

public class NNFVisitor
extends BooleanFormulaTransformationVisitor

Constructor Summary

Constructors

Constructor	Description
NNFVisitor(FormulaManager pFmgr)

Method Summary

Modifier and Type	Method	Description
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	visitXor(BooleanFormula processedOperand1, BooleanFormula processedOperand2)	Visit an XOR-expression.

Methods inherited from class org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor

visitAnd, visitAtom, visitConstant, visitOr, visitQuantifier

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor

visitBoundVar

Constructor Detail

NNFVisitor

public NNFVisitor(FormulaManager pFmgr)

Method Detail

visitNot

public BooleanFormula visitNot(BooleanFormula processedOperand)

Description copied from interface: BooleanFormulaVisitor

Visit a NOT-expression.

Specified by:

visitNot in interface BooleanFormulaVisitor<BooleanFormula>

Overrides:

visitNot in class BooleanFormulaTransformationVisitor

Parameters:

processedOperand - Negated term.

See Also:

BooleanFormulaManager.not(org.sosy_lab.java_smt.api.BooleanFormula)

visitXor

public BooleanFormula visitXor(BooleanFormula processedOperand1,
                               BooleanFormula processedOperand2)

Description copied from interface: BooleanFormulaVisitor

Visit an XOR-expression.

Specified by:

visitXor in interface BooleanFormulaVisitor<BooleanFormula>

Overrides:

visitXor in class BooleanFormulaTransformationVisitor

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.

Specified by:

visitEquivalence in interface BooleanFormulaVisitor<BooleanFormula>

Overrides:

visitEquivalence in class BooleanFormulaTransformationVisitor

See Also:

BooleanFormulaManager.equivalence(org.sosy_lab.java_smt.api.BooleanFormula, org.sosy_lab.java_smt.api.BooleanFormula)

visitImplication

public BooleanFormula visitImplication(BooleanFormula processedOperand1,
                                       BooleanFormula processedOperand2)

Description copied from interface: BooleanFormulaVisitor

Visit an implication.

Specified by:

visitImplication in interface BooleanFormulaVisitor<BooleanFormula>

Overrides:

visitImplication in class BooleanFormulaTransformationVisitor

See Also:

BooleanFormulaManager.implication(org.sosy_lab.java_smt.api.BooleanFormula, org.sosy_lab.java_smt.api.BooleanFormula)

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 interface BooleanFormulaVisitor<BooleanFormula>

Overrides:

visitIfThenElse in class BooleanFormulaTransformationVisitor

See Also:

BooleanFormulaManager.ifThenElse(org.sosy_lab.java_smt.api.BooleanFormula, T, T)