Uses of Class
edu.mit.csail.sdg.alloy4compiler.translator.A4Solution

Packages that use A4Solution

edu.mit.csail.sdg.alloy4compiler.translator	This package contains the translator from Alloy4 to CNF (using kodkod).
edu.mit.csail.sdg.alloy4viz	This package displays Alloy4 instances.
edu.mit.csail.sdg.alloy4whole	This package contains a simple GUI client, as well as several examples on using the API.

Uses of A4Solution in edu.mit.csail.sdg.alloy4compiler.translator

Methods in edu.mit.csail.sdg.alloy4compiler.translator that return A4Solution

static A4Solution	TranslateAlloyToKodkod.execute_command(A4Reporter rep, java.lang.Iterable<Sig> sigs, Command cmd, A4Options opt) Based on the specified "options", execute one command and return the resulting A4Solution object.
static A4Solution	TranslateAlloyToKodkod.execute_commandFromBook(A4Reporter rep, java.lang.Iterable<Sig> sigs, Command cmd, A4Options opt) Based on the specified "options", execute one command and return the resulting A4Solution object.
A4Solution	A4Solution.next() If this solution is UNSAT, return itself; else return the next solution (which could be SAT or UNSAT).
static A4Solution	A4SolutionReader.read(java.lang.Iterable<Sig> sigs, XMLNode xml) Parse the XML element into an AlloyInstance.

Methods in edu.mit.csail.sdg.alloy4compiler.translator with parameters of type A4Solution

static java.lang.Object	TranslateAlloyToKodkod.alloy2kodkod(A4Solution sol, Expr expr) Translate the Alloy expression into an equivalent Kodkod Expression or IntExpression or Formula object.
boolean	Simplifier.simplify(A4Reporter rep, A4Solution sol, java.util.List<kodkod.ast.Formula> formulas) Simplify sol.bounds() based on the set of formulas, or to modify the formulas list itself.

Uses of A4Solution in edu.mit.csail.sdg.alloy4viz

Constructors in edu.mit.csail.sdg.alloy4viz with parameters of type A4Solution

AlloyInstance(A4Solution originalA4, java.lang.String filename, java.lang.String commandname, AlloyModel model, java.util.Map<AlloyAtom,java.util.Set<AlloySet>> atom2sets, java.util.Map<AlloyRelation,java.util.Set<AlloyTuple>> rel2tuples, boolean isMetamodel)
Create a new instance.

VizTree(A4Solution instance, java.lang.String title, int fontSize)
Constructs a tree to display the given instance.

Uses of A4Solution in edu.mit.csail.sdg.alloy4whole

Methods in edu.mit.csail.sdg.alloy4whole with parameters of type A4Solution

static java.util.Map<java.lang.String,Sig.PrimSig>

Helper.atom2sig(A4Solution solution) Given an A4Solution, return a map that maps every atom to its most specific signature.