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()
Evaluable
public int translate(int key)
Evaluable
public void toClause(ISolver solver) throws ContradictionException
Evaluable
toClause
in interface Evaluable
solver
- 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.