org.sat4j.minisat.constraints
Class MixedDataStructureWithBinary

java.lang.Object
  org.sat4j.minisat.constraints.AbstractDataStructureFactory<ILits2>
      org.sat4j.minisat.constraints.MixedDataStructureWithBinary

All Implemented Interfaces:

java.io.Serializable, DataStructureFactory<ILits2>

public class MixedDataStructureWithBinary
extends AbstractDataStructureFactory<ILits2>

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

Field Summary

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

learner, lits, solver

Constructor Summary

MixedDataStructureWithBinary()

Method Summary

Constr	createClause(IVecInt literals)
ILits2	createLits()
Constr	createUnregisteredClause(IVecInt literals)
void	learnConstraint(Constr constr)

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

conflictDetectedInAttachesFor, createCardinalityConstraint, getAttachesFor, getVocabulary, reset, setLearner, setUnitPropagationListener

Methods inherited from class java.lang.Object

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

Constructor Detail

MixedDataStructureWithBinary

public MixedDataStructureWithBinary()

Method Detail

createLits

public ILits2 createLits()

Specified by:

createLits in class AbstractDataStructureFactory<ILits2>

createClause

public Constr createClause(IVecInt literals)
                    throws ContradictionException

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<ILits2>

Overrides:

learnConstraint in class AbstractDataStructureFactory<ILits2>

createUnregisteredClause

public Constr createUnregisteredClause(IVecInt literals)