| 
||||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | |||||||||
java.lang.Objectorg.sat4j.minisat.constraints.AbstractDataStructureFactory<ILits23>
org.sat4j.minisat.constraints.MixedDataStructureWithBinaryAndTernary
public class MixedDataStructureWithBinaryAndTernary
| 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 | 
|---|
public MixedDataStructureWithBinaryAndTernary()
| Method Detail | 
|---|
public Constr createClause(IVecInt literals)
                    throws ContradictionException
literals - a set of literals using Dimacs format (signed non null
            integers).
ContradictionException - the constraint is trivially unsatisfiable.public void learnConstraint(Constr constr)
learnConstraint in interface DataStructureFactory<ILits23>learnConstraint in class AbstractDataStructureFactory<ILits23>protected ILits23 createLits()
createLits in class AbstractDataStructureFactory<ILits23>public Constr createUnregisteredClause(IVecInt literals)
  | 
||||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | |||||||||