[musers.] problem with unique modes
Matthias Güdemann
matthias.guedemann at googlemail.com
Sat Jul 11 00:15:39 AEST 2015
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 SATSolver 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
stepcount 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
More information about the users
mailing list