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

java.lang.Object
  extended by 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.