[m-users.] delay declarations in Mercury

[Matthias Guedemann]

Dear Zoltan,

thank you for your detailed explanation.

> systems; to do the same in a statically scheduled system like Mercury,
> you need a program transformation inside the Mercury compiler.  The
> Mercury compiler does have such a transformation, but it won't handle
> every situation you may want it to.

Could you point me to where to find more information about this, please?

I am asking about the delay declarations, as I have found a paper
describing an elegant implementation of a SAT solver in Prolog[1]. In
this paper the authors implement a watched-literal optimization using
delay declarations (giving different variants: block for SICStus, when
for SWI and freeze for others).

At the core this looks like this:

,----
| :- block watch(-, ?, -, ?, ?).
| watch(Var1, Pol1, Var2, Pol2, Pairs) :-
|     nonvar(Var1) ->
|         update_watch(Var1, Pol1, Var2, Pol2, Pairs);
|         update_watch(Var2, Pol2, Var1, Pol1, Pairs).
`----

So, the watch is updated if either Var1 or Var2 becomes bound, and this
is decided using the impure nonvar/1.

My initial idea was to provide two different predicates for the update:
one with mode "in" for Var1 and one with mode "in" for Var2, in order to
eliminate nonvar/1; and to use the disjunction of these two predicates
in the predicate watch (and watch with two different modes). Would this
work?

My goal is not to have the most efficient SAT solver, but to have a
simple implementation to try out different approaches to SAT-based
model-checking on top.

Best regards,
Matthias

Footnotes:
[1]  https://www.cs.kent.ac.uk/pubs/2012/3136/content.pdf