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

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

All Implemented Interfaces:

kodkod.ast.visitor.VoidVisitor

public final class TranslateKodkodToJava
extends java.lang.Object
implements kodkod.ast.visitor.VoidVisitor

Translate a Kodkod formula node to an equivalent Java program that solves the formula.

Requirements: atoms must be String objects (since we cannot possibly output a Java source code that can re-generate arbitrary Java objects).

Method Summary

static java.lang.String	convert(kodkod.ast.Formula formula, int bitwidth, java.lang.Iterable<java.lang.String> atoms, kodkod.instance.Bounds bounds, java.util.Map<java.lang.Object,java.lang.String> atomMap) Given a Kodkod formula node, return a Java program that (when compiled and executed) would solve that formula.
static int	countHeight(kodkod.ast.Node node) Count the height of the given Kodkod AST tree.
void	visit(kodkod.ast.BinaryExpression x)
void	visit(kodkod.ast.BinaryFormula x)
void	visit(kodkod.ast.BinaryIntExpression x)
void	visit(kodkod.ast.ComparisonFormula x)
void	visit(kodkod.ast.Comprehension x)
void	visit(kodkod.ast.ConstantExpression x)
void	visit(kodkod.ast.ConstantFormula x)
void	visit(kodkod.ast.Decl x)
void	visit(kodkod.ast.Decls x)
void	visit(kodkod.ast.ExprToIntCast x)
void	visit(kodkod.ast.IfExpression x)
void	visit(kodkod.ast.IfIntExpression x)
void	visit(kodkod.ast.IntComparisonFormula x)
void	visit(kodkod.ast.IntConstant x)
void	visit(kodkod.ast.IntToExprCast x)
void	visit(kodkod.ast.MultiplicityFormula x)
void	visit(kodkod.ast.NaryExpression x)
void	visit(kodkod.ast.NaryFormula x)
void	visit(kodkod.ast.NaryIntExpression x)
void	visit(kodkod.ast.NotFormula x)
void	visit(kodkod.ast.ProjectExpression x)
void	visit(kodkod.ast.QuantifiedFormula x)
void	visit(kodkod.ast.Relation x)
void	visit(kodkod.ast.RelationPredicate x)
void	visit(kodkod.ast.SumExpression x)
void	visit(kodkod.ast.UnaryExpression x)
void	visit(kodkod.ast.UnaryIntExpression x)
void	visit(kodkod.ast.Variable x)

Methods inherited from class java.lang.Object

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

Method Detail

countHeight

public static int countHeight(kodkod.ast.Node node)

Count the height of the given Kodkod AST tree.

convert

public static java.lang.String convert(kodkod.ast.Formula formula,
                                       int bitwidth,
                                       java.lang.Iterable<java.lang.String> atoms,
                                       kodkod.instance.Bounds bounds,
                                       java.util.Map<java.lang.Object,java.lang.String> atomMap)

Given a Kodkod formula node, return a Java program that (when compiled and executed) would solve that formula.

Requirement: atoms must be String objects (since we cannot possibly output a Java source code that can re-generate arbitrary Java objects).

Parameters:

formula - - the formula to convert

bitwidth - - the integer bitwidth

atoms - - an iterator over the set of all atoms

bounds - - the Kodkod bounds object to use

atomMap - - if nonnull, it is used to map the atom name before printing

visit

public void visit(kodkod.ast.Relation x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.BinaryExpression x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.ComparisonFormula x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.ProjectExpression x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.IntComparisonFormula x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.BinaryFormula x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.BinaryIntExpression x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.UnaryIntExpression x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.UnaryExpression x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.IfExpression x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.IfIntExpression x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.NotFormula x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.IntToExprCast x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.ExprToIntCast x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.IntConstant x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.ConstantFormula x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.ConstantExpression x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.Variable x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.Comprehension x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.QuantifiedFormula x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.SumExpression x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.MultiplicityFormula x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.Decl x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.Decls x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.RelationPredicate x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.NaryExpression x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.NaryIntExpression x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor

visit

public void visit(kodkod.ast.NaryFormula x)

Specified by:

visit in interface kodkod.ast.visitor.VoidVisitor