kodkod.engine.fol2sat

Class Translation.Incremental

java.lang.Object

kodkod.engine.fol2sat.Translation

kodkod.engine.fol2sat.Translation.Incremental

Enclosing class:

Translation

public static final class Translation.Incremental
extends Translation

An incremental translation preserves the internal data structures used during translation. This enables the translation to be updated with CNF encodings of additional formulas and bounds using the Translator.translateIncremental(kodkod.ast.Formula, Bounds, Translation.Incremental) method.

Incremental translations are more expensive to store than whole translations, and they place some restrictions on the form of problems that are translated. In particular, logging must be disabled during translation; the translation must use an incremental SAT solver; and the addition of new clauses must not violate the invariants guaranteed by the Translation class. All three restrictions are enforced by the translateIncremental(...) methods of the Translator class.

Author:

Emina Torlak

Specfields:

symmetries: set IntSet // partition of the universe into equivalence classes induced this.originalBounds

Invariants:

this.options.logTranslation = 0 && this.options.solver.incremental()

this.symmetries = partition(this.originalBounds)

See Also:

Translator.translateIncremental(kodkod.ast.Formula, Bounds, Options), Translator.translateIncremental(kodkod.ast.Formula, Bounds, Translation.Incremental)

Nested Class Summary

Nested classes/interfaces inherited from class kodkod.engine.fol2sat.Translation

Translation.Incremental, Translation.Whole

Method Summary

Modifier and Type	Method and Description
SATSolver	cnf() Returns the SATSolver object containing the CNF encoding of this.formula.
int	numPrimaryVariables() Returns the number of primary variables allocated during translation.
IntSet	primaryVariables(Relation relation) Returns the set of primary variables that represent the tuples in the given relation.

Methods inherited from class kodkod.engine.fol2sat.Translation

bounds, interpret, options, trivial

Methods inherited from class java.lang.Object

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

Method Detail

cnf

public final SATSolver cnf()

Returns the SATSolver object containing the CNF encoding of this.formula. Satisfiability of the formula can be checked by calling SATSolver.solve(). Modification of the returned object may cause violation of Translation invariants.

Specified by:

cnf in class Translation

Returns:

{s: SATSolver | SAT(s.variables, s.clauses) iff SAT(this.formula, this.bounds, this.options) }

See Also:

Translation.cnf()

numPrimaryVariables

public int numPrimaryVariables()

Returns the number of primary variables allocated during translation. Primary variables represent the tuples of relations in this.bounds that have different lower and upper bounds (i.e. some this.bounds.upperBound[r].tuples - this.bounds.lowerBound[r].tuples).

Specified by:

numPrimaryVariables in class Translation

Returns:

#this.vars[Relation]

See Also:

Translation.numPrimaryVariables()

primaryVariables

public IntSet primaryVariables(Relation relation)

Returns the set of primary variables that represent the tuples in the given relation. If no variables were allocated to the given relation, empty set is returned. This set contains exactly this.bounds.upperBound(r).size() - this.bounds.lowerBound(r).size() variable identifiers.

Specified by:

primaryVariables in class Translation

Returns:

this.vars[relation]

See Also:

Translation.primaryVariables(kodkod.ast.Relation)