16.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 ‘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, []).