ENHANCED: CLP(B): Various changes that improve space and time efficiency:
                  Nodes can now be shared between BDDs and are represented
                  more efficiently. This allows some shortcuts when fusing
                  BDDs. Intermediate results are also stored more compactly.
                  Tables are now stored *per variable* for faster access.

Squashed commit of the following:

commit d3e5a1ca6ead624c68e5985049c11ccd84d431c2
Merge: db98ada 85770fe
Author: Markus Triska <markus.triska@gmx.at>
Date:   Sun Aug 24 21:52:08 2014 +0200

    synch with master

commit db98adac2331351a59aef55c7c87bf1f09f3c03d
Author: Markus Triska <markus.triska@gmx.at>
Date:   Sun Aug 24 21:09:56 2014 +0200

    shorter key for result cache, saving some space

commit 0d5450d40913f9e1a8e8b1a459074807b273b374
Author: Markus Triska <markus.triska@gmx.at>
Date:   Sun Aug 24 21:00:07 2014 +0200

    use a single attribute per node, saving some space and simplifying sandboxing

commit 2c61714110ca1a20fb92daf49a6eaa9d7ee6704b
Author: Markus Triska <markus.triska@gmx.at>
Date:   Sun Aug 24 20:51:06 2014 +0200

    correct comment

commit 2a5c6191e9592a58f1c02152b7490ac2717ff9a3
Merge: 33f7409 e67373b
Author: Markus Triska <markus.triska@gmx.at>
Date:   Sun Aug 24 20:45:09 2014 +0200

    synch with master

commit 33f7409f9166b86727e08ef9ac85c1a11da78307
Author: Markus Triska <markus.triska@gmx.at>
Date:   Sat Aug 23 18:15:37 2014 +0200

    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.

commit e316bf682b966979a243ad9fef5cb33c29a84c2c
Author: Markus Triska <markus.triska@gmx.at>
Date:   Sat Aug 23 18:10:03 2014 +0200

    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.

commit aab999e62408e5b69ae0d80cc7b6fcf9dc9d7c46
Author: Markus Triska <markus.triska@gmx.at>
Date:   Sat Aug 23 17:54:04 2014 +0200

    comment on declarations for library(sandbox) and future perspectives

commit b7be4ce02e846664aba72cc05d792db859107ad5
Author: Markus Triska <markus.triska@gmx.at>
Date:   Sat Aug 23 17:50:12 2014 +0200

    shorten cases in bdd_restriction_//4

commit ecfeea8ab56e36b48fc2e5b7f6432f0c2abfb052
Author: Markus Triska <markus.triska@gmx.at>
Date:   Sat Aug 23 17:48:18 2014 +0200

    reset attributes after taut/2 to reclaim nodes from local hash tables

commit 892437772110a8143389dc5d513c047a7bc723aa
Author: Markus Triska <markus.triska@gmx.at>
Date:   Wed Aug 20 21:20:08 2014 +0200

    reorder predicates for better readability

commit ed71204fb3cebfd32d02d96656a3526f5491ea88
Merge: 638e14d e7709a4
Author: Markus Triska <markus.triska@gmx.at>
Date:   Wed Aug 20 20:42:08 2014 +0200

    synch with master

commit 638e14dad329c4a687a5e1e90eb9e15679d5404b
Author: Markus Triska <markus.triska@gmx.at>
Date:   Wed Aug 20 20:25:05 2014 +0200

    reorder a few predicates and comments for better readability

commit 163f39bb88754fea3448416a1eeadc0291d1bb60
Author: Markus Triska <markus.triska@gmx.at>
Date:   Wed Aug 20 20:24:10 2014 +0200

    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.

commit 16bb9963ac1a246cdfedef1b7fc120fd8ce9bdfb
Author: Markus Triska <markus.triska@gmx.at>
Date:   Wed Aug 20 20:18:15 2014 +0200

    add BDD validation

commit 52cc128af3bfbdf462a4d25111dbdba31c1809b5
Author: Markus Triska <markus.triska@gmx.at>
Date:   Wed Aug 20 20:17:45 2014 +0200

    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.

commit 83afddbd20ee4f2487eadc87dfd0a7ed9e42eaca
Author: Markus Triska <markus.triska@gmx.at>
Date:   Wed Aug 20 02:14:38 2014 +0200

    fewer nodes due to sharing

commit dd4f34951e1fb929f1aed62b8bc497415bc94c0f
Author: Markus Triska <markus.triska@gmx.at>
Date:   Wed Aug 20 02:08:04 2014 +0200

    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)]'

commit 4195f7995f1b8a4b896266364dbac6d2229f381e
Author: Markus Triska <markus.triska@gmx.at>
Date:   Wed Aug 20 01:09:52 2014 +0200

    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

commit 9ee4c8bfa6d345f298d1c6f43b76400d06a2a3be
Author: Markus Triska <markus.triska@gmx.at>
Date:   Mon Aug 18 22:43:35 2014 +0200

    enable BDD validation

commit c29a0bc023f0a9e81e943bb1c64f77a3467d7927
Author: Markus Triska <markus.triska@gmx.at>
Date:   Mon Aug 18 22:41:19 2014 +0200

    work in progress on correctly registering new nodes

commit 7e6af5258ba33cfafe0dd314162a51b88ad5e654
Merge: 6daa449 bdf7455
Author: Markus Triska <markus.triska@gmx.at>
Date:   Mon Aug 18 22:39:22 2014 +0200

    Merge branch 'master' into clpb2.0

    Conflicts:
    	library/clp/clpb.pl

commit 6daa4494556bc2149ac22b50b764fa89e455fc41
Author: Markus Triska <markus.triska@gmx.at>
Date:   Thu Aug 14 19:06:27 2014 +0200

    ENHANCED: library(sandbox): Allow b_setval/2 and b_getval/2 when the first argument is instantiated.
disable BDD validation when optimisation is enabled

BDD validation consumes a lot of memory, so disabling it can help when
solving larger problems. Eventually, this test will be disabled
altogether by default, after sufficient testing of this library.
prevent bad line break on www.swi-prolog.org/pldoc/man?section=clpb
sync with master