kodkod.engine

Class Solver

java.lang.Object

kodkod.engine.Solver

All Implemented Interfaces:

KodkodSolver

public final class Solver
extends Object
implements KodkodSolver

A computational engine for solving relational satisfiability problems. Such a problem is described by a formula in first order relational logic; finite bounds on the value of each relation constrained by the formula; and a set of options specifying, among other global parameters, the length of bitvectors that describe the meaning of integer expressions in the given formula. The options are usually reused between invocations to the solve methods, so they are specified as a part of the solver state.

A Solver takes as input a relational problem and produces a satisfying model or an instance of it, if one exists. It can also produce a proof of unsatisfiability for problems with no models, if the options specify the use of a proof logging SAT solver.

Author:

Emina Torlak

Specfields:

options: Options

Constructor Summary

Constructors

Constructor and Description
Solver() Constructs a new Solver with the default options.
Solver(Options options) Constructs a new Solver with the given options.

Method Summary

Modifier and Type	Method and Description
void	free() Releases the resources, if any, associated with this solver.
Options	options() Returns the Options object used by this Solver to guide translation of formulas from first-order logic to cnf.
Solution	solve(Formula formula, Bounds bounds) Attempts to satisfy the given formula and bounds with respect to this.options or, optionally, prove the problem's unsatisfiability.
Iterator<Solution>	solveAll(Formula formula, Bounds bounds) Attempts to find all solutions to the given formula with respect to the specified bounds or to prove the formula's unsatisfiability.
String	toString()

Methods inherited from class java.lang.Object

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

Constructor Detail

Solver

public Solver()

Constructs a new Solver with the default options.

Ensures:

this.options' = new Options()

Solver

public Solver(Options options)

Constructs a new Solver with the given options.

Ensures:

this.options' = options

Throws:

NullPointerException - options = null

Method Detail

free

public void free()

Releases the resources, if any, associated with this solver.

Specified by:

free in interface KodkodSolver

See Also:

KodkodSolver.free()

options

public Options options()

Returns the Options object used by this Solver to guide translation of formulas from first-order logic to cnf.

Specified by:

options in interface KodkodSolver

Returns:

this.options

solve

public Solution solve(Formula formula,
                      Bounds bounds)
               throws HigherOrderDeclException,
                      UnboundLeafException,
                      AbortedException

Attempts to satisfy the given formula and bounds with respect to this.options or, optionally, prove the problem's unsatisfiability. If the method completes normally, the result is a solution containing either an instance of the given problem or, optionally, a proof of its unsatisfiability. An unsatisfiability proof will be constructed iff this.options.solver specifies a SATProver and this.options.logTranslation > 0.

Specified by:

solve in interface KodkodSolver

Returns:

some sol: Solution | some sol.instance() => sol.instance() in MODELS(formula, bounds, this.options) else UNSAT(formula, bound, this.options)

Throws:

NullPointerException - formula = null || bounds = null

UnboundLeafException - the formula contains an undeclared variable or a relation not mapped by the given bounds

HigherOrderDeclException - the formula contains a higher order declaration that cannot be skolemized, or it can be skolemized but this.options.skolemDepth is insufficiently large

AbortedException - this solving task was aborted

See Also:

Options, Solution, Instance, Proof

solveAll

public Iterator<Solution> solveAll(Formula formula,
                                   Bounds bounds)
                            throws HigherOrderDeclException,
                                   UnboundLeafException,
                                   AbortedException

Attempts to find all solutions to the given formula with respect to the specified bounds or to prove the formula's unsatisfiability. If the operation is successful, the method returns an iterator over n Solution objects. The outcome of the first n-1 solutions is SAT or trivially SAT, and the outcome of the nth solution is UNSAT or tirivally UNSAT. Note that an unsatisfiability proof will be constructed for the last solution iff this.options specifies the use of a core extracting SATSolver. Additionally, the CNF variables in the proof can be related back to the nodes in the given formula iff this.options has variable tracking enabled. Translation logging also requires that there are no subnodes in the given formula that are both syntactically shared and contain free variables.

Returns:

an iterator over all the Solutions to the formula with respect to the given bounds

Throws:

NullPointerException - formula = null || bounds = null

UnboundLeafException - the formula contains an undeclared variable or a relation not mapped by the given bounds

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

AbortedException - this solving task was interrupted with a call to Thread.interrupt on this thread

IllegalStateException - !this.options.solver().incremental()

See Also:

Solution, Options, Proof

toString

public String toString()

Overrides:

toString in class Object

See Also:

Object.toString()