remove code that is not needed in Scryer Prolog

diff --git a/src/lib/clpb.pl b/src/lib/clpb.pl
index 213d684a246f0b391a966082857cebf58a50d7e7..4dde600bc6ec2b117a3e2849c64e8cd6dc48b6c3 100644 (file)
--- a/src/lib/clpb.pl
+++ b/src/lib/clpb.pl
@@ -1697,8 +1697,7 @@ attribute_goals(Var) -->
                 { bdd_nodes(BDD, Nodes),
                   phrase(nodes(Nodes), Ns) },
                 [clpb:'$clpb_bdd'(Ns)]
-            ;   { prepare_global_variables(BDD),
-                  phrase(sat_ands(Formula), Ands0),
+            ;   { phrase(sat_ands(Formula), Ands0),
                   ands_fusion(Ands0, Ands),
                   maplist(formula_anf, Ands, ANFs0),
                   sort(ANFs0, ANFs1),
@@ -1732,34 +1731,10 @@ del_clpb(Var) :-
         del_attr(Var, clpb_hash),
         del_attr(Var, clpb_atom).
 
-/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
-   To make residual projection work with recorded constraints, the
-   global counters must be adjusted so that new variables and nodes
-   also get new IDs. Also, clpb_next_id/2 is used to actually create
-   these counters, because creating them with b_setval/2 would make
-   them [] on backtracking, which is quite unfortunate in itself.
-- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
-
 b_setval(K, T) :- bb_b_put(K, T).
 nb_setval(K, T) :- bb_put(K, T).
 b_getval(K, T) :- bb_get(K, T).
 
-prepare_global_variables(BDD) :-
-        clpb_next_id('$clpb_next_var', V0),
-        clpb_next_id('$clpb_next_node', N0),
-        bdd_nodes(BDD, Nodes),
-        foldl(max_variable_node, Nodes, V0-N0, MaxV0-MaxN0),
-        MaxV is MaxV0 + 1,
-        MaxN is MaxN0 + 1,
-        b_setval('$clpb_next_var', MaxV),
-        b_setval('$clpb_next_node', MaxN).
-
-max_variable_node(Node, V0-N0, V-N) :-
-        node_id(Node, N1),
-        node_varindex(Node, V1),
-        N is max(N0,N1),
-        V is max(V0,V1).
-
 /* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
    Fuse formulas that share the same variables into single conjunctions.
 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */