org.kahina.logic.sat.io.free

Class TseitinTransformationVisitor

java.lang.Object

org.kahina.logic.sat.io.free.TseitinTransformationVisitor

All Implemented Interfaces:

BooleanFormulaVisitor<java.lang.Integer>

public class TseitinTransformationVisitor
extends java.lang.Object
implements BooleanFormulaVisitor<java.lang.Integer>

Constructor Summary

Constructors

Constructor and Description
TseitinTransformationVisitor()

Method Summary

Methods

Modifier and Type	Method and Description
CnfSatInstance	getCNF(int topVar)
java.lang.Integer	visitConjunction(Conjunction fm)
java.lang.Integer	visitConstant(BooleanConstant fm)
java.lang.Integer	visitDisjunction(Disjunction fm)
java.lang.Integer	visitNegation(Negation fm)
java.lang.Integer	visitVariable(BooleanVariable fm)

Methods inherited from class java.lang.Object

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

Constructor Detail

TseitinTransformationVisitor

public TseitinTransformationVisitor()

Method Detail

visitVariable

public java.lang.Integer visitVariable(BooleanVariable fm)

Specified by:

visitVariable in interface BooleanFormulaVisitor<java.lang.Integer>

visitNegation

public java.lang.Integer visitNegation(Negation fm)

Specified by:

visitNegation in interface BooleanFormulaVisitor<java.lang.Integer>

visitDisjunction

public java.lang.Integer visitDisjunction(Disjunction fm)

Specified by:

visitDisjunction in interface BooleanFormulaVisitor<java.lang.Integer>

visitConjunction

public java.lang.Integer visitConjunction(Conjunction fm)

Specified by:

visitConjunction in interface BooleanFormulaVisitor<java.lang.Integer>

visitConstant

public java.lang.Integer visitConstant(BooleanConstant fm)

Specified by:

visitConstant in interface BooleanFormulaVisitor<java.lang.Integer>

getCNF

public CnfSatInstance getCNF(int topVar)