kodkod.engine.fol2sat
Class Translator

java.lang.Object
  kodkod.engine.fol2sat.Translator

public final class Translator
extends java.lang.Object

Translates, evaluates, and approximates nodes with respect to given bounds (or instances) and Options.

Author:

Emina Torlak

Method Summary

static kodkod.engine.bool.BooleanMatrix	approximate(kodkod.ast.Expression expression, kodkod.instance.Bounds bounds, Options options) Overapproximates the value of the given expression using the provided bounds and options.
static kodkod.engine.bool.BooleanMatrix	evaluate(kodkod.ast.Expression expression, kodkod.instance.Instance instance, Options options) Evaluates the given expression to a BooleanMatrix using the provided instance and options.
static kodkod.engine.bool.BooleanConstant	evaluate(kodkod.ast.Formula formula, kodkod.instance.Instance instance, Options options) Evaluates the given formula to a BooleanConstant using the provided instance and options.
static kodkod.engine.bool.Int	evaluate(kodkod.ast.IntExpression intExpr, kodkod.instance.Instance instance, Options options) Evalutes the given intexpression to an Int using the provided instance and options.
static kodkod.engine.fol2sat.Translation	translate(kodkod.ast.Formula formula, kodkod.instance.Bounds bounds, Options options) Translates the given formula using the specified bounds and options.

Methods inherited from class java.lang.Object

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

Method Detail

approximate

public static kodkod.engine.bool.BooleanMatrix approximate(kodkod.ast.Expression expression,
                                                           kodkod.instance.Bounds bounds,
                                                           Options options)

Overapproximates the value of the given expression using the provided bounds and options.

Returns:

a BooleanMatrix whose TRUE entries represent the tuples contained in a sound overapproximation of the expression.

Throws:

expression - = null || instance = null || options = null

kodkod.engine.fol2sat.UnboundLeafException - the expression refers to an undeclared variable or a relation not mapped by the instance

kodkod.engine.fol2sat.HigherOrderDeclException - the expression contains a higher order declaration

evaluate

public static kodkod.engine.bool.BooleanConstant evaluate(kodkod.ast.Formula formula,
                                                          kodkod.instance.Instance instance,
                                                          Options options)

Evaluates the given formula to a BooleanConstant using the provided instance and options.

Returns:

a BooleanConstant that represents the value of the formula.

Throws:

java.lang.NullPointerException - formula = null || instance = null || options = null

kodkod.engine.fol2sat.UnboundLeafException - the formula refers to an undeclared variable or a relation not mapped by the instance

kodkod.engine.fol2sat.HigherOrderDeclException - the formula contains a higher order declaration

evaluate

public static kodkod.engine.bool.BooleanMatrix evaluate(kodkod.ast.Expression expression,
                                                        kodkod.instance.Instance instance,
                                                        Options options)

Evaluates the given expression to a BooleanMatrix using the provided instance and options.

Returns:

a BooleanMatrix whose TRUE entries represent the tuples contained by the expression.

Throws:

java.lang.NullPointerException - expression = null || instance = null || options = null

kodkod.engine.fol2sat.UnboundLeafException - the expression refers to an undeclared variable or a relation not mapped by the instance

kodkod.engine.fol2sat.HigherOrderDeclException - the expression contains a higher order declaration

evaluate

public static kodkod.engine.bool.Int evaluate(kodkod.ast.IntExpression intExpr,
                                              kodkod.instance.Instance instance,
                                              Options options)

Evalutes the given intexpression to an Int using the provided instance and options.

Returns:

an Int representing the value of the intExpr with respect to the specified instance and options.

Throws:

java.lang.NullPointerException - formula = null || instance = null || options = null

kodkod.engine.fol2sat.UnboundLeafException - the expression refers to an undeclared variable or a relation not mapped by the instance

kodkod.engine.fol2sat.HigherOrderDeclException - the expression contains a higher order declaration

translate

public static kodkod.engine.fol2sat.Translation translate(kodkod.ast.Formula formula,
                                                          kodkod.instance.Bounds bounds,
                                                          Options options)
                                                   throws kodkod.engine.fol2sat.TrivialFormulaException

Translates the given formula using the specified bounds and options.

Returns:

a Translation whose solver is a SATSolver instance initialized with the CNF representation of the given formula, with respect to the given bounds. The CNF is generated in such a way that the magnitude of the literal representing the truth value of a given formula is strictly larger than the magnitudes of the literals representing the truth values of the formula's descendants.

Throws:

kodkod.engine.fol2sat.TrivialFormulaException - the given formula is reduced to a constant during translation (i.e. the formula is trivially (un)satisfiable).

java.lang.NullPointerException - any of the arguments are null

kodkod.engine.fol2sat.UnboundLeafException - the formula refers to an undeclared variable or a relation not mapped by the given bounds.

kodkod.engine.fol2sat.HigherOrderDeclException - the formula contains a higher order declaration that cannot be skolemized, or it can be skolemized but options.skolemize is false.