edu.mit.csail.sdg.alloy4compiler.translator
Class A4Options

java.lang.Object
  edu.mit.csail.sdg.alloy4compiler.translator.A4Options

All Implemented Interfaces:

java.io.Serializable

public final class A4Options
extends java.lang.Object
implements java.io.Serializable

Mutable; this class encapsulates the customizable options of the Alloy-to-Kodkod translator.

See Also:

Serialized Form

Nested Class Summary

static class

A4Options.SatSolver This enum defines the set of possible SAT solvers.

Field Summary

int	coreGranularity Unsat core granularity, default is 0 (only top-level conjuncts are considered), 3 expands all quantifiers
int	coreMinimization This option specifies the unsat core minimization strategy (0=GuaranteedLocalMinimum 1=FasterButLessAccurate 2=EvenFaster...)
boolean	noOverflow This option specifies whether the solver should report only solutions that don't cause any overflows.
java.lang.String	originalFilename This option tells the compiler the "original filename" that these AST nodes came from; it is only used for generating comments and other diagnostic messages.
boolean	recordKodkod This option specifies whether the compiler should record the original Kodkod formula being generated and the resulting Kodkod instances.
int	skolemDepth This option specifies the maximum skolem-function depth.
A4Options.SatSolver	solver This option specifies the SAT solver to use (SAT4J, MiniSatJNI, MiniSatProverJNI, ZChaffJNI...)
java.lang.String	solverDirectory When this.solver is external, and the solver filename is a relative filename, then this option specifies the directory that the solver filename is relative to.
int	symmetry This option specifies the amount of symmetry breaking to do (when symmetry breaking isn't explicitly disabled).
java.lang.String	tempDirectory This specifies the directory where we may write temporary files to.
int	unrolls This option constrols how deep we unroll loops and unroll recursive predicate/function/macros (negative means it's disallowed)

Constructor Summary

A4Options()
Constructs an A4Options object with default values for everything.

Method Summary

A4Options

dup() This method makes a copy of this Options object.

Methods inherited from class java.lang.Object

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

Field Detail

symmetry

public int symmetry

This option specifies the amount of symmetry breaking to do (when symmetry breaking isn't explicitly disabled).

If a formula is unsatisfiable, then in general, the higher this value, the faster you finish the solving. But if this value is too high, it will instead slow down the solving.

If a formula is satisfiable, then in general, the lower this value, the faster you finish the solving. Setting this value to 0 usually gives the fastest solve.

Default value is 20.

skolemDepth

public int skolemDepth

This option specifies the maximum skolem-function depth.

Default value is 0, which means it will only generate skolem constants, and will not generate skolem functions.

coreMinimization

public int coreMinimization

This option specifies the unsat core minimization strategy (0=GuaranteedLocalMinimum 1=FasterButLessAccurate 2=EvenFaster...)

Default value is set to the fastest current strategy.

coreGranularity

public int coreGranularity

Unsat core granularity, default is 0 (only top-level conjuncts are considered), 3 expands all quantifiers

solver

public A4Options.SatSolver solver

This option specifies the SAT solver to use (SAT4J, MiniSatJNI, MiniSatProverJNI, ZChaffJNI...)

Default value is SAT4J.

solverDirectory

public java.lang.String solverDirectory

When this.solver is external, and the solver filename is a relative filename, then this option specifies the directory that the solver filename is relative to.

tempDirectory

public java.lang.String tempDirectory

This specifies the directory where we may write temporary files to.

originalFilename

public java.lang.String originalFilename

This option tells the compiler the "original filename" that these AST nodes came from; it is only used for generating comments and other diagnostic messages.

Default value is "".

recordKodkod

public boolean recordKodkod

This option specifies whether the compiler should record the original Kodkod formula being generated and the resulting Kodkod instances.

Default value is false.

noOverflow

public boolean noOverflow

This option specifies whether the solver should report only solutions that don't cause any overflows.

unrolls

public int unrolls

This option constrols how deep we unroll loops and unroll recursive predicate/function/macros (negative means it's disallowed)

Constructor Detail

A4Options

public A4Options()

Constructs an A4Options object with default values for everything.

Method Detail

dup

public A4Options dup()

This method makes a copy of this Options object.