org.sat4j.minisat.constraints
Class MixedDataStructureWithBinaryAndTernary

java.lang.Object
  org.sat4j.minisat.constraints.AbstractDataStructureFactory
      org.sat4j.minisat.constraints.ClausalDataStructureWL
          org.sat4j.minisat.constraints.MixedDataStructureDaniel
              org.sat4j.minisat.constraints.MixedDataStructureWithBinaryAndTernary

All Implemented Interfaces:

java.io.Serializable, DataStructureFactory

public class MixedDataStructureWithBinaryAndTernary
extends MixedDataStructureDaniel

Author:

leberre To change the template for this generated type comment go to Window>Preferences>Java>Code Generation>Code and Comments

See Also:

Serialized Form

Constructor Summary

MixedDataStructureWithBinaryAndTernary()

Method Summary

Constr	createClause(IVecInt literals)
ILits	getVocabulary()
void	learnConstraint(Constr constr)

Methods inherited from class org.sat4j.minisat.constraints.MixedDataStructureDaniel

createCardinalityConstraint

Methods inherited from class org.sat4j.minisat.constraints.ClausalDataStructureWL

createUnregisteredClause

Methods inherited from class org.sat4j.minisat.constraints.AbstractDataStructureFactory

conflictDetectedInWatchesFor, createPseudoBooleanConstraint, createUnregisteredPseudoBooleanConstraint, getWatchesFor, reset, setLearner, setUnitPropagationListener

Methods inherited from class java.lang.Object

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

Constructor Detail

MixedDataStructureWithBinaryAndTernary

public MixedDataStructureWithBinaryAndTernary()

Method Detail

getVocabulary

public ILits getVocabulary()

Specified by:

getVocabulary in interface DataStructureFactory

Overrides:

getVocabulary in class AbstractDataStructureFactory

createClause

public Constr createClause(IVecInt literals)
                    throws ContradictionException

Specified by:

createClause in interface DataStructureFactory

Overrides:

createClause in class ClausalDataStructureWL

Parameters:

literals - a set of literals using Dimacs format (signed non null integers).

Returns:

null if the constraint is a tautology.

Throws:

ContradictionException - the constraint is trivially unsatisfiable.

learnConstraint

public void learnConstraint(Constr constr)

Specified by:

learnConstraint in interface DataStructureFactory

Overrides:

learnConstraint in class AbstractDataStructureFactory