ENHANCED: library(sandbox): Allow b_setval/2 and b_getval/2 when the first argument is instantiated.
Merge branch 'master' into clpb2.0

Conflicts:
	library/clp/clpb.pl
work in progress on correctly registering new nodes
enable BDD validation
experimental version that allows sharing nodes between BDDs.

The node table is now kept *per variable*, which allows fast node
lookup even when the nodes come from different BDDs. This allows some
shortcuts in apply//4. However, it requires rebuilding the tables
occasionally so that nodes that are no longer reachable are removed.

Some (fixable) issues remain. Mainly: Unnecessary variables may appear
in residual goals, if they are still reachable via a local node table.
Second, this requires much more testing before it can be merged into
master. For example, suppose I erroneously add rebuild_hashes(BDD) as
the final goal in sat_bdd/2. bool_queens runs into this problem and
throws an exception. But we need many more systematic test cases that
find this problem too.

Performance on N-queens (2.33 GHz iMac):

   |queens(0)| = 1           after 0.00s
   |queens(1)| = 1           after 0.00s
   |queens(4)| = 2           after 0.08s
   |queens(5)| = 10          after 0.50s
   |queens(6)| = 4           after 2.55s
   |queens(7)| = 40          after 13.34s
   |queens(8)| = 92          after 69.97s
   |queens(9)| = 352         after 407.85s

Previously:

   |queens(0)| = 1           after 0.00s
   |queens(1)| = 1           after 0.00s
   |queens(4)| = 2           after 0.16s
   |queens(5)| = 10          after 1.11s
   |queens(6)| = 4           after 5.74s
   |queens(7)| = 40          after 32.29s
   |queens(8)| = 92          after 172.25s
   |queens(9)| = 352         after 962.64s
   |queens(10)| = 724        after 5538.98s
   |queens(11)| = 2680       after 40545.80s
reset all attributes in taut/2 so that eliminated nodes do not appear in residual goals

Example:

   %?- taut(card([0,1,2,3], [A,B,C]), T).
   %@ T = 1,
   %@ sat(A=:=A),
   %@ sat(B=:=B),
   %@ sat(C=:=C).

I also found a test case for erroneous rebuild_hashes/1 in sat_bdd/2:

   :- use_module(clpb).

   sat(_)  --> [].
   sat(X*Y) --> [_], sat(X), sat(Y).
   sat(X+Y) --> [_], sat(X), sat(Y).
   sat(X#Y) --> [_], sat(X), sat(Y).

   eqs([], _).
   eqs(_, []).
   eqs([V|Vs], [A|As]) :- ( true ; sat(V =:= A) ), eqs(Vs, As).

   run(N) :-
           length(Ls, N),
           portray_clause(N),
           phrase(sat(Sat1), Ls),
           sat(Sat1),
           phrase(sat(Sat2), Ls),
           sat(Sat2),
           term_variables(Sat1, Vs1),
           term_variables(Sat2, Vs2),
           eqs(Vs1, Vs2),
           sat(Sat1 + Sat2),
           false.

   run :- run(_).

Example:

   %?- run.
   %@ 0.
   %@ 1.
   %@ 2.
   %@ ERROR: Domain error: `reduced_ites' expected, found `[_G6392-ite(_G6400,_G6687,_G6645),_G6645-ite(_G6543,_G6613,0),_G6613-ite(_G6585,_G6442,0),_G6442-ite(_G6426,_G6470,_G6460),_G6460-ite(_G6468,_G6470,0),_G6470-ite(_G6500,1,0),_G6687-ite(_G6585,_G6442,0)],[ite(_G6400,_G6687,_G6645),ite(_G6543,_G6613,0),ite(_G6585,_G6442,0),ite(_G6426,_G6470,_G6460),ite(_G6468,_G6470,0),ite(_G6500,1,0),ite(_G6585,_G6442,0)],[ite(_G6400,_G6687,_G6645),ite(_G6543,_G6613,0),ite(_G6585,_G6442,0),ite(_G6500,1,0),ite(_G6426,_G6470,_G6460),ite(_G6468,_G6470,0)]'
fewer nodes due to sharing
remove intermediate variables at the place of their origin

This is the right place to do it. Otherwise, they may show up in residual
goals. This also lets us shorten unsatisfiable_conjunction/2.
add BDD validation
this can now be made unconditional.

The reason this needed to be conditional was that existential counter
variables (introduced by card()) were able to refer to the (already
processed) root although they were no longer part of the BDD at all,
and they could appear in residuals because their nodes were still
reachable by the local association list of some variable. We now
remove the attributes of all existential counter variables at the
place of their origin, so they can no longer appear in residuals.
reorder a few predicates and comments for better readability
synch with master
reorder predicates for better readability
reset attributes after taut/2 to reclaim nodes from local hash tables
shorten cases in bdd_restriction_//4
comment on declarations for library(sandbox) and future perspectives
introduce bdd_nodes/2 and make it the building block for other relations

bdd_ites/2 uses too much memory to be useful in larger tasks, since it
essentially duplicates the entire BDD even though only a small subset
of its elements are often needed.
save some space in all tables by not wrapping node IDs in node(...)

Note that 0 and 1 get dedicated IDs (false and true) and therefore
still do not interfere with other IDs, which are always integers.
synch with master
correct comment