remove code that is not needed in Scryer Prolog
This commit is contained in:
@@ -1697,8 +1697,7 @@ attribute_goals(Var) -->
|
|||||||
{ bdd_nodes(BDD, Nodes),
|
{ bdd_nodes(BDD, Nodes),
|
||||||
phrase(nodes(Nodes), Ns) },
|
phrase(nodes(Nodes), Ns) },
|
||||||
[clpb:'$clpb_bdd'(Ns)]
|
[clpb:'$clpb_bdd'(Ns)]
|
||||||
; { prepare_global_variables(BDD),
|
; { phrase(sat_ands(Formula), Ands0),
|
||||||
phrase(sat_ands(Formula), Ands0),
|
|
||||||
ands_fusion(Ands0, Ands),
|
ands_fusion(Ands0, Ands),
|
||||||
maplist(formula_anf, Ands, ANFs0),
|
maplist(formula_anf, Ands, ANFs0),
|
||||||
sort(ANFs0, ANFs1),
|
sort(ANFs0, ANFs1),
|
||||||
@@ -1732,34 +1731,10 @@ del_clpb(Var) :-
|
|||||||
del_attr(Var, clpb_hash),
|
del_attr(Var, clpb_hash),
|
||||||
del_attr(Var, clpb_atom).
|
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).
|
b_setval(K, T) :- bb_b_put(K, T).
|
||||||
nb_setval(K, T) :- bb_put(K, T).
|
nb_setval(K, T) :- bb_put(K, T).
|
||||||
b_getval(K, T) :- bb_get(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.
|
Fuse formulas that share the same variables into single conjunctions.
|
||||||
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
|
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
|
||||||
|
|||||||
Reference in New Issue
Block a user