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).