| Constructor and Description |
|---|
Var(String idvar,
Domain domain,
int lastvarnumber) |
| Modifier and Type | Method and Description |
|---|---|
Domain |
domain()
Return the domain of the evaluable.
|
int |
findValue(int[] model) |
void |
toClause(ISolver solver)
Translates a variable over a domain into a set a clauses enforcing that
exactly one value must be chosen in the domain.
|
String |
toString() |
int |
translate(int key)
Translates a value from the domain into a SAT variable in Dimacs format.
|
public Domain domain()
Evaluablepublic int translate(int key)
Evaluablepublic void toClause(ISolver solver) throws ContradictionException
EvaluabletoClause in interface Evaluablesolver - a solver to feed with the clauses.ContradictionException - if a trivial inconsistency is met.public int findValue(int[] model)
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.