Package edu.mit.csail.sdg.alloy4compiler.translator

This package contains the translator from Alloy4 to CNF (using kodkod).

See:
          Description

Class Summary
A4Options Mutable; this class encapsulates the customizable options of the Alloy-to-Kodkod translator.
A4Options.SatSolver This enum defines the set of possible SAT solvers.
A4Solution This class stores a SATISFIABLE or UNSATISFIABLE solution.
A4SolutionReader This helper class contains helper routines for reading an A4Solution object from an XML file.
A4SolutionWriter This helper class contains helper routines for writing an A4Solution object out as an XML file.
A4Tuple Immutable; represents a single Alloy tuple; comparison is by identity rather than by value.
A4TupleSet Immutable; represents a collection of Alloy tuples; comparison is by identity rather than by value.
Simplifier Immutable; this class shrinks the unknowns as much as possible in order to reduce the number of variables in final CNF.
TranslateAlloyToKodkod Translate an Alloy AST into Kodkod AST then attempt to solve it using Kodkod.
TranslateKodkodToJava Translate a Kodkod formula node to an equivalent Java program that solves the formula.
 

Package edu.mit.csail.sdg.alloy4compiler.translator Description

This package contains the translator from Alloy4 to CNF (using kodkod).