Provides classes for analyzing and evaluating Kodkod ASTs with respect to finite bounds or instances.

Package Specification

Contains classes for analyzing and evaluating Kodkod ASTs with respect to finite bounds or instances. A {@linkplain kodkod.engine.Solver Solver} provides methods for finding finite models and minimal unsatisfiable cores of Kodkod formulas with respect to given {@linkplain kodkod.instance.Bounds Bounds} and {@linkplain kodkod.engine.config.Options Options}. An {@linkplain kodkod.engine.IncrementalSolver IncrementalSolver} provides a way to solve a sequence of related formulas and bounds incrementally, with respect to the same {@linkplain kodkod.engine.config.Options Options options}. An {@linkplain kodkod.engine.Evaluator Evaluator} enables the evaluation of formulas, expressions, and integer expressions with respect to a particular {@linkplain kodkod.instance.Instance Instance} and {@linkplain kodkod.engine.config.Options Options}.

Related Documentation

@see kodkod.instance.Bounds @see kodkod.instance.Instance @see kodkod.ast.Expression @see kodkod.ast.IntExpression @see kodkod.ast.Formula @see kodkod.engine.Solver @see kodkod.engine.IncrementalSolver @see kodkod.engine.Evaluator