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
DOC: CLP(B): Add example for sat_count/2.
synch with master
reorder predicates for better readability
use library functions that have become available
Updated pengines
improve first sentences, used as the predicate summary in search results
Updated http
elements must be integers
Updated pengines