[m-users.] problem with unique modes
matthias.guedemann at googlemail.com
Sat Jul 11 00:15:39 AEST 2015
> 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
I have a type like this:
| :- type 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.
More information about the users