kodkod.engine.config
Class Options

java.lang.Object
  kodkod.engine.config.Options

public final class Options
extends java.lang.Object

Stores information about various user-level translation and analysis options. It can be used to choose the SAT solver, control symmetry breaking, etc.

Author:

Emina Torlak

Nested Class Summary

static class

Options.IntEncoding Integer encoding options for the translation of int expressions.

Constructor Summary

Options()
Constructs an Options object initalized with default values.

Method Summary

int	bitwidth() Returns the size of the integer representation.
int	coreGranularity() Returns the core granularity level.
boolean	flatten() Returns the value of the flattening flag, which specifies whether to eliminate extraneous intermediate variables.
OrderingMethod	getOrderingMethod() Returns the present method to tamper with SAT solver's variable ordering.
kodkod.util.ints.IntRange	integers() Returns the range of integers that can be encoded using this.intEncoding and this.bitwidth.
Options.IntEncoding	intEncoding() Returns the integer encoding that will be used for translating int nodes.
int	logTranslation() Returns the translation logging level (0, 1, or 2), where 0 means logging is not performed, 1 means only the translations of top level formulas are logged, and 2 means all formula translations are logged.
kodkod.engine.config.Reporter	reporter() Returns this.reporter.
void	setBitwidth(int bitwidth) Sets this.bitwidth to the given value.
void	setCoreGranularity(int coreGranularity) Sets the core granularity level.
void	setFlatten(boolean flatten) Sets the flattening option to the given value.
void	setIntEncoding(Options.IntEncoding encoding) Sets the intEncoding option to the given value.
void	setLogTranslation(int logTranslation) Sets the translation logging level.
void	setOrderingMethod(OrderingMethod ordering) Specify a method to tamper with SAT solver's variable ordering.
void	setReporter(kodkod.engine.config.Reporter reporter) Sets this.reporter to the given reporter.
void	setSharing(int sharing) Sets the sharing option to the given value.
void	setSkolemDepth(int skolemDepth) Sets the skolemDepth to the given value.
void	setSolver(kodkod.engine.satlab.SATFactory solver) Sets the solver option to the given value.
void	setSymmetryBreaking(int symmetryBreaking) Sets the symmetryBreaking option to the given value.
int	sharing() Returns the depth to which circuits are checked for equivalence during translation.
int	skolemDepth() Returns the depth to which existential quantifiers are skolemized.
kodkod.engine.satlab.SATFactory	solver() Returns the value of the solver options.
int	symmetryBreaking() Returns the 'amount' of symmetry breaking to perform.
java.lang.String	toString() Returns a string representation of this Options object.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

Options

public Options()

Constructs an Options object initalized with default values.

Method Detail

solver

public kodkod.engine.satlab.SATFactory solver()

Returns the value of the solver options. The default is SATSolver.DefaultSAT4J.

Returns:

this.solver

setOrderingMethod

public void setOrderingMethod(OrderingMethod ordering)

Specify a method to tamper with SAT solver's variable ordering. This is only applied if the chosen SAT solver implements the interface OrderableSolver. DefaultOrdering is used if this option is untouched.

Parameters:

ordering - is an instance of the provided ordering methods

getOrderingMethod

public OrderingMethod getOrderingMethod()

Returns the present method to tamper with SAT solver's variable ordering. If this option was untouched it an instance of DefaultOrdering is returned.

setSolver

public void setSolver(kodkod.engine.satlab.SATFactory solver)

Sets the solver option to the given value.

Throws:

java.lang.NullPointerException - solver = null

reporter

public kodkod.engine.config.Reporter reporter()

Returns this.reporter.

Returns:

this.reporter

setReporter

public void setReporter(kodkod.engine.config.Reporter reporter)

Sets this.reporter to the given reporter.

Throws:

java.lang.NullPointerException - reporter = null

intEncoding

public Options.IntEncoding intEncoding()

Returns the integer encoding that will be used for translating int nodes. The default is BINARY representation, which allows negative numbers. UNARY representation is best suited to problems with small scopes, in which cardinalities are only compared (and possibly added to each other or non-negative numbers).

Returns:

this.intEncoding

setIntEncoding

public void setIntEncoding(Options.IntEncoding encoding)

Sets the intEncoding option to the given value.

Throws:

java.lang.NullPointerException - encoding = null

java.lang.IllegalArgumentException - this.bitwidth is not a valid bitwidth for the specified encoding

bitwidth

public int bitwidth()

Returns the size of the integer representation. For example, if this.intEncoding is BINARY and this.bitwidth = 5 (the default), then all operations will yield one of the five-bit numbers in the range [-16..15]. If this.intEncoding is UNARY and this.bitwidth = 5, then all operations will yield one of the numbers in the range [0..5].

Returns:

this.bitwidth

setBitwidth

public void setBitwidth(int bitwidth)

Sets this.bitwidth to the given value.

Throws:

java.lang.IllegalArgumentException - bitwidth < 1

java.lang.IllegalArgumentException - this.intEncoding==BINARY && bitwidth > 32

integers

public kodkod.util.ints.IntRange integers()

Returns the range of integers that can be encoded using this.intEncoding and this.bitwidth.

Returns:

range of integers that can be encoded using this.intEncoding and this.bitwidth.

flatten

public boolean flatten()

Returns the value of the flattening flag, which specifies whether to eliminate extraneous intermediate variables. The flag is false by default. Flattening must be off if translation logging is enabled.

Returns:

this.flatten

setFlatten

public void setFlatten(boolean flatten)

Sets the flattening option to the given value.

Throws:

java.lang.IllegalArgumentException - this.logTranslation>0 && flatten

symmetryBreaking

public int symmetryBreaking()

Returns the 'amount' of symmetry breaking to perform. If a non-symmetric solver is chosen for this.solver, this value controls the maximum length of the generated lex-leader symmetry breaking predicate. If a symmetric solver is chosen, this value controls the amount of symmetry information to pass to the solver. (For example, if a formula has 10 relations on which symmetry can be broken, and the symmetryBreaking option is set to 5, then symmetry information will be computed for only 5 of the 10 relations.) In general, the higher this value, the more symmetries will be broken, and the faster the formula will be solved. But, setting the value too high may have the opposite effect and slow down the solving. The default value for this property is 20.

Returns:

this.symmetryBreaking

setSymmetryBreaking

public void setSymmetryBreaking(int symmetryBreaking)

Sets the symmetryBreaking option to the given value.

Throws:

java.lang.IllegalArgumentException - symmetryBreaking !in [0..Integer.MAX_VALUE]

sharing

public int sharing()

Returns the depth to which circuits are checked for equivalence during translation. The default depth is 3, and the minimum allowed depth is 1. Increasing the sharing may result in a smaller CNF, but at the cost of slower translation times.

Returns:

this.sharing

setSharing

public void setSharing(int sharing)

Sets the sharing option to the given value.

Throws:

java.lang.IllegalArgumentException - sharing !in [1..Integer.MAX_VALUE]

skolemDepth

public int skolemDepth()

Returns the depth to which existential quantifiers are skolemized. A negative depth means that no skolemization is performed. The default depth of 0 means that only existentials that are not nested within a universal quantifiers are skolemized. A depth of 1 means that existentials nested within a single universal are also skolemized, etc.

Returns:

this.skolemDepth

setSkolemDepth

public void setSkolemDepth(int skolemDepth)

Sets the skolemDepth to the given value.

logTranslation

public int logTranslation()

Returns the translation logging level (0, 1, or 2), where 0 means logging is not performed, 1 means only the translations of top level formulas are logged, and 2 means all formula translations are logged. This is necessary for determining which formulas occur in the unsat core of an unsatisfiable formula. Flattening must be off whenever logging is enabled. Logging is off by default, since it incurs a non-trivial time overhead.

Returns:

this.logTranslation

setLogTranslation

public void setLogTranslation(int logTranslation)

Sets the translation logging level. If the level is above 0, flattening is automatically disabled.

Throws:

java.lang.IllegalArgumentException - logTranslation !in [0..2]

coreGranularity

public int coreGranularity()

Returns the core granularity level. The default is 0, which means that top-level conjuncts of the input formula are used as "roots" for the purposes of core minimization and extraction. Granularity of 1 means that the top-level conjuncts of the input formula's negation normal form (NNF) are used as roots; granularity of 2 means that the top-level conjuncts of the formula's skolemized NNF (SNNF) are used as roots; and, finally, a granularity of 3 means that the universal quantifiers of the formula's SNNF are broken up and that the resulting top-level conjuncts are then used as roots for core minimization and extraction.

Note that the finer granularity (that is, a larger value of this.coreGranularity) will provide better information at the cost of slower core extraction and, in particular, minimization.

Returns:

this.coreGranularity

setCoreGranularity

public void setCoreGranularity(int coreGranularity)

Sets the core granularity level.

Throws:

java.lang.IllegalArgumentException - coreGranularity !in [0..3]

toString

public java.lang.String toString()

Returns a string representation of this Options object.

Overrides:

toString in class java.lang.Object

Returns:

a string representation of this Options object.