[m-users.] problem with unique modes

[Matthias Güdemann]

Hi Zoltan,

> The constraint based mode analysis described in that paper is in the
> Mercury compiler, but it is experimental only, and not ready for real
> use. First, it covers only a subset of Mercury, and second, its
> performance is not good enough.  The usual mode analysis algorithm is
> completely separate from this experiment.

ok, thanks for the clarification. I had read about the performance in
the paper and David's thesis. There he stated that most time is consumed
in construction and computation on ROBDDs. Therefore I had thought about
looking at a possibility to give this problem to a SAT-Solver instead (I
also saw that this has been stated on the mailing list a few years ago).

> If you could tell us more about the problem, maybe we could propose a
> workaround.

I have a type like this:

,----
| :- type proof_state --->
|     proof_state(
|                 state :: property_result,
|                 po_type :: property_type,
|                 k ::int,
|                 po :: int,
|                 prover :: prover_state,
|                 unproven_model :: model_state
|               ).
`----

A proof_state encapsulates a single proof goal and there can be multiple
proof_states, each with its own proof goal; prover_state and model_state
refer to external C/C++ stateful objects.

For each existing proof_state, I execute one step in the proof. This
potentially modifies the state (from unproven to proven/falsified) the
step-count k and the prover_state and model_state.

I advance sequentially each proof_state one step and continue to do so,
until no state is unproven.

I have a predicate advance_proof_states that loops over a list of
proof_state values, and a predicate advance_proof_state with

,----
| :- pred advance_proof_state(proof_state::di, proof_state::uo) is det.
`----

advance_proof_states is as follows:

,----
| :- pred advance_proof_states(list(proof_state)::in, list(proof_state)::in, list(proof_state)::out) is det.
| 
| advance_proof_states(PSList, ResList, OutPSList) :-
|     (
|       PSList = [],
|       OutPSList = reverse(ResList)
|     ;
|       PSList = [PS | PSRest],
|       unsafe_promise_unique(PS, PS0),
|       advance_proof_state(PS0, NewPS),
|       advance_proof_states(PSRest, [NewPS | ResList], OutPSList)
|     ).
`----

This works and seems to do exactly what it should do. If you have a
suggestion of how to improve it or if you see any problems with this
approach, please tell me.

Best regards,
Matthias