Package kodkod.engine

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

See: Description

Interface Summary

Interface	Description
KodkodSolver	A computational engine for solving relational satisfiability problems.

Class Summary

Class	Description
Evaluator	An evaluator for relational formulas and expressions with respect to a given instance and options.
IncrementalSolver	A computational engine for solving a sequence of related relational formulas and bounds (e.g., generated by a software verification or synthesis tool) with respect to a given set of configuration options.
Proof	Contains a proof of unsatisfiability of a given FOL formula.
Solution	Represents the full solution to a formula: an instance if the formula is satisfiable or a proof of unsatisfiability if not.
Solver	A computational engine for solving relational satisfiability problems.
Statistics	Stores the statistics gathered while solving a given formula.

Enum Summary

Enum	Description
Solution.Outcome	Enumerates the possible outcomes of an attempt to find a model for a FOL formula.

Exception Summary

Exception	Description
AbortedException	Indicates that a solving or evaluation task has been aborted.
CapacityExceededException	Indicates that a problem construction or translation task failed because the capacity of the index representation was exceeded.

Package kodkod.engine Description

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 Solver provides methods for finding finite models and minimal unsatisfiable cores of Kodkod formulas with respect to given Bounds and Options. An IncrementalSolver provides a way to solve a sequence of related formulas and bounds incrementally, with respect to the same Options options. An Evaluator enables the evaluation of formulas, expressions, and integer expressions with respect to a particular Instance and Options.

Related Documentation

See Also:

Bounds, Instance, Expression, IntExpression, Formula, Solver, IncrementalSolver, Evaluator