public interface DataStructureFactory
Modifier and Type | Method and Description |
---|---|
void |
conflictDetectedInWatchesFor(int p,
int i) |
Constr |
createCardinalityConstraint(IVecInt literals,
int degree)
Create a cardinality constraint of the form sum li >= degree.
|
Constr |
createClause(IVecInt literals) |
Constr |
createUnregisteredCardinalityConstraint(IVecInt literals,
int degree) |
Constr |
createUnregisteredClause(IVecInt literals) |
ILits |
getVocabulary() |
IVec<Propagatable> |
getWatchesFor(int p) |
void |
learnConstraint(Constr constr) |
void |
reset() |
void |
setLearner(Learner l) |
void |
setUnitPropagationListener(UnitPropagationListener s) |
Constr createClause(IVecInt literals) throws ContradictionException
literals
- a set of literals using Dimacs format (signed non null
integers).ContradictionException
- the constraint is trivially unsatisfiable.UnsupportedOperationException
- there is no concrete implementation for that constraint.void learnConstraint(Constr constr)
Constr createCardinalityConstraint(IVecInt literals, int degree) throws ContradictionException
literals
- a set of literals.degree
- the degree of the cardinality constraint.ContradictionException
Constr createUnregisteredCardinalityConstraint(IVecInt literals, int degree)
void setUnitPropagationListener(UnitPropagationListener s)
void setLearner(Learner l)
void reset()
ILits getVocabulary()
IVec<Propagatable> getWatchesFor(int p)
p
- void conflictDetectedInWatchesFor(int p, int i)
p
- i
- the index of the conflicting constraintCopyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.