I would appreciate if you add to your page on an explanation of
your requirement on pre unify_hook for those who have only
basics of Boolean constraints like me. So far I must be missing
your point between pre unify_hook and such basics.
( X -> ( Y -> true ; false) ; ( Y -> true ; false ) )
?- zdd_set_vars([X,Y]),sat((X*Y) + (~X* Y)).
node(4)-(X->node(3);node(3)),node(3)-(Y->true;false),
Is ZDD a just prolog term ? if so what is the semantics of the ZDD ?
For me, result of the query depends on meanings of
these symbols; ((true -> true) or ((true->true) or false)) = true
in Boolean, isn’t it ? Surely I must be missing something.
> To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+unsubscribe@googlegroups.com.
> Visit this group at https://groups.google.com/group/swi-prolog.
> For more options, visit https://groups.google.com/d/optout.
--
You received this message because you are subscribed to the Google Groups "SWI-Prolog" group.
To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+unsubscribe@googlegroups.com.
Module:verify_attributes(-Var, +Value, -Goals)
https://sicstus.sics.se/sicstus/docs/3.7.1/html/sicstus_17.html
The SICStus documentation also says so:
"
It may succeed non-deterministically, in which
case attr_unify_hook(_) :-
...
call(Fa)
...
But Markus Trisa writes:
"The way in which this hook currently works makes the implementation of important classes of constraint solvers impossible or at least extremely impractical. For increased generality and convenience, simultaneous unifications as in[X,Y]=[0,1]
should be processed sequentially by the Prolog engine, or a more general hook should be provided in the future."
I am not sure whether SICStus Prolog solves the problem.
SICStus Prolog writes:
"This predicate is called whenever a variable Var that might have attributes in Module is about to be bound to Value (it might have none). The unification resumes after the call toverify_attributes/3
."
So although the hook is synchronous to the unification,
i.e. step by step. I am not sure what happens to the
goals. The specification only says:
"It is expected to return, in Goals, a list of goals
to be called after Var has been bound to Value.What is the meaning of after here? How much after? Are
we really save for what Markus Triska thinks a problem.
A possible workaround for Markus Triskas problem would
be to store the ZDD with different variables, and have
a map that shows which variables correspond to the
variables in the ZDD.
The in the SWI-Prolog hook, he could work step-by-step
through this map, although the map would have received
a "simultaneous" or better "multiple variable" instantiation.
Just some guesses what could be done...
> <mailto:swi-prolog+unsub...@googlegroups.com>.
> > <mailto:swi-prolog+unsub...@googlegroups.com>.
; get_attr_local(X, Fb) ->
...
meta_conj(Fb, Goal, C), put_attr_local(X, C) % rescue conjunction
...
% A (meta) conjunction of two goals meta_conj('$:'(Fa), '$:'(Fb), '$:'('basiccontrol:,'(Fa, Fb))).
Welcome to SWI-Prolog (threaded, 64 bits, version 7.5.8)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
?- freeze(X, write(foo)), freeze(X, write(bar)), get_attrs(X, A).
A = att(freeze, '$and'(user:write(foo), user:write(bar)), []),
> > > <mailto:swi-prolog+unsub...@googlegroups.com>.