org.sat4j.minisat.constraints
Class MixedDataStructureWithBinaryAndTernary

java.lang.Object
  extended by org.sat4j.minisat.constraints.AbstractDataStructureFactory<ILits23>
      extended by org.sat4j.minisat.constraints.MixedDataStructureWithBinaryAndTernary
All Implemented Interfaces:
java.io.Serializable, DataStructureFactory<ILits23>

public class MixedDataStructureWithBinaryAndTernary
extends AbstractDataStructureFactory<ILits23>

Author:
leberre
See Also:
Serialized Form

Field Summary
 
Fields inherited from class org.sat4j.minisat.constraints.AbstractDataStructureFactory
learner, lits, solver
 
Constructor Summary
MixedDataStructureWithBinaryAndTernary()
           
 
Method Summary
 Constr createClause(IVecInt literals)
           
protected  ILits23 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

MixedDataStructureWithBinaryAndTernary

public MixedDataStructureWithBinaryAndTernary()
Method Detail

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<ILits23>
Overrides:
learnConstraint in class AbstractDataStructureFactory<ILits23>

createLits

protected ILits23 createLits()
Specified by:
createLits in class AbstractDataStructureFactory<ILits23>

createUnregisteredClause

public Constr createUnregisteredClause(IVecInt literals)


Copyright © 2009 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.