17.3 Solver type definitions

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. The ground_inst and any_inst attributes are optional and default to ground. The constraint_store attribute is mandatory: mutable_decls must be 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. The attributes that are not omitted must appear in the order shown above.

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.

Solver types may be exported from their defining module, but only in an abstract form. This requires the full definition to appear in the implementation section of the module, and an abstract declaration like the following in its interface:

:- solver type solver_type.

If a solver type is exported, then its representation type, and, if specified, its equality and/or comparison predicates must also exported from the same module.

If a solver type has no equality predicate specified, then the compiler will generate an equality predicate that throws an exception of type ‘exception.software_error/0’ when called.

Likewise, if a solver type has no equality comparison 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, []).