Next: Implementing solver types, Previous: Abstract solver type declarations, Up: Solver types [Contents]

A solver type definition takes the following form:

:- solver type solver_type where representation is representation_type, ground is ground_inst, any is any_inst, constraint_store is mutable_decls, equality is equality_pred, comparison is comparison_pred.

The ‘`representation`’ attribute is mandatory
‘`ground_inst`’ and ‘`any_inst`’ default to ‘`ground`’,
‘`mutable_decls`’ is either a single mutable declaration
(see Module-local mutable variables)
or a comma separated list of mutable declarations in brackets,
the equality and comparison attributes are optional (although a solver type
without equality would not be very useful), and attributes must appear in the
order shown.

The `representation_type`

is the type used to implement the
`solver_type`

. A two-tier scheme of this kind is necessary for a
number of reasons, including

- a semantic gap is necessary to accommodate the fact that non-ground
`solver_type`

values may be represented by ground`representation_type`

values (in the context of the corresponding constraint solver state); - this approach greatly simplifies the definition of equality and
comparison predicates for the
`solver_type`

.

The `ground_inst`

is the inst associated with
`representation_type`

values denoting `ground`

`solver_type`

values.

The `any_inst`

is the inst associated with
`representation_type`

values denoting `any`

`solver_type`

values.

The compiler constructs four impure functions for converting between
`solver_type`

values and `representation_type`

values
(‘`name`’ is the function symbol used to name `solver_type`

and
‘`arity`’ is the number of type parameters it takes):

:- impure func 'representation of ground name/arity'(solver_type) = representation_type. :- mode 'representation of ground name/arity'(in) = out(ground_inst) is det. :- impure func 'representation of any name/arity'(solver_type) = representation_type. :- mode 'representation of any name/arity'(in(any)) = out(any_inst) is det. :- impure func 'representation to ground name/arity'(representation_type) = solver_type. :- mode 'representation to ground name/arity'(in(ground_inst)) = out is det. :- impure func 'representation to any name/arity'(representation_type) = solver_type. :- mode 'representation to any name/arity'(in(any_inst)) = out(any) is det.

These functions are impure because of the semantic gap issue mentioned above.

These functions are constructed in-line as part of a source-to-source transformation, hence it is an error to define a solver type in the interface section of a module.

If `solver_type`

is exported then it is a requirement that
`representation_type`

, `initialisation_pred`

, and, if
specified, `equality_pred`

and `comparison_pred`

are also
exported from the same module.

If `equality_pred`

is not specified then the compiler will
generate an equality predicate that throws an exception of type
‘`exception.software_error/0`’ when called.

Likewise, if `comparison_pred`

is not specified then the compiler
will generate a comparison predicate that throws an exception of
type ‘`exception.software_error/0`’ when called.

If provided, any mutable declarations given for the `constraint_store`

attribute are equivalent to separate mutable declarations; their association
with the solver type is for the purposes of documentation. That is,

:- solver type t where ... constraint_store is [ mutable(a, int, 42, ground, []), mutable(b, string, "Hi", ground, []) ], ...

is equivalent to

:- solver type t where ... :- mutable(a, int, 42, ground, []). :- mutable(b, string, "Hi", ground, []).