API tools faq
paste
Advertisement
logicmoo

sICSTUS hYBRID

logicmoo
Apr 1st, 2019
674
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Prolog 13.56 KB | None | 0 0
raw download clone embed print report
  1. root@gitlab:/mnt/sdf1/usr/local/sicstus4.3.5/lib/sicstus-4.3.5/library/clpfd# grep -i bdd ../ -R
  2. Binary file ../x86_64-linux-glibc2.17/clpfd.s.o matches
  3. Binary file ../x86_64-linux-glibc2.17/clpfd/lcc_d.o matches
  4. Binary file ../x86_64-linux-glibc2.17/clpfd/lin_d.o matches
  5. Binary file ../x86_64-linux-glibc2.17/clpfd/sorting_d.o matches
  6. Binary file ../x86_64-linux-glibc2.17/clpfd/fdsets_s.o matches
  7. Binary file ../x86_64-linux-glibc2.17/clpfd/arith_s.o matches
  8. Binary file ../x86_64-linux-glibc2.17/clpfd/discrete_d.o matches
  9. Binary file ../x86_64-linux-glibc2.17/clpfd/alldifferent_d.o matches
  10. Binary file ../x86_64-linux-glibc2.17/clpfd/arith_d.o matches
  11. Binary file ../x86_64-linux-glibc2.17/clpfd/multi_cumulative_s.o matches
  12. Binary file ../x86_64-linux-glibc2.17/clpfd/fdsets_d.o matches
  13. Binary file ../x86_64-linux-glibc2.17/clpfd/setsingleton_d.o matches
  14. Binary file ../x86_64-linux-glibc2.17/clpfd/symmcum_d.o matches
  15. Binary file ../x86_64-linux-glibc2.17/clpfd/multi_cumulative_d.o matches
  16. Binary file ../x86_64-linux-glibc2.17/clpfd/setsingleton_s.o matches
  17. Binary file ../x86_64-linux-glibc2.17/clpfd/disjoint2_s.o matches
  18. Binary file ../x86_64-linux-glibc2.17/clpfd/indexical_d.o matches
  19. Binary file ../x86_64-linux-glibc2.17/clpfd/dvars_s.o matches
  20. Binary file ../x86_64-linux-glibc2.17/clpfd/relation_d.o matches
  21. Binary file ../x86_64-linux-glibc2.17/clpfd/lh_s.o matches
  22. Binary file ../x86_64-linux-glibc2.17/clpfd/alldistinct_s.o matches
  23. Binary file ../x86_64-linux-glibc2.17/clpfd/discrete_s.o matches
  24. Binary file ../x86_64-linux-glibc2.17/clpfd/disjoint2_d.o matches
  25. Binary file ../x86_64-linux-glibc2.17/clpfd/relation_s.o matches
  26. Binary file ../x86_64-linux-glibc2.17/clpfd/ac3intervals_d.o matches
  27. Binary file ../x86_64-linux-glibc2.17/clpfd.so matches
  28. ../clpb.pl:     bdd_to_formula(G, F, M),
  29. ../clpb.pl:     formula_to_bdd(Var, X, 1, [], _, Dic),
  30. ../clpb.pl:     ;   prolog:'$bdd_negate'(X, Y), bool1(Dic, [Y])
  31. ../clpb.pl:     prolog:'$bdd_build'(I, 1, 0, Node),
  32. ../clpb.pl:         prolog:'$bdd_negate'(PNode, NNode),
  33. ../clpb.pl:         bdd_to_bdd(G, M, Node, Free0, Free1, Dic0, Dic1),
  34. ../clpb.pl:         bdd_univ(Node, NNode, PNode, Eq),
  35. ../clpb.pl:% Translating from BDD to internal polynomial format.
  36. ../clpb.pl:bdd_to_formula(0, [], _) :- !.
  37. ../clpb.pl:bdd_to_formula(1, [[]], _) :- !.
  38. ../clpb.pl:bdd_to_formula(Graph, F, Dic) :-
  39. ../clpb.pl:     bdd_parts(Graph, V, Q, R, Dic),
  40. ../clpb.pl:     prolog:'$bdd_type'(Q, R, Type),
  41. ../clpb.pl:     bdd_to_formula(Type, V, Q, R, Dic, F).
  42. ../clpb.pl:bdd_to_formula(0, V, _, _, _,   [[V]]).
  43. ../clpb.pl:bdd_to_formula(1, V, _, _, _,   [[],[V]]).
  44. ../clpb.pl:bdd_to_formula(2, V, _, R, Dic, Formula) :-
  45. ../clpb.pl:     bdd_to_formula(R, R1, Dic),
  46. ../clpb.pl:bdd_to_formula(3, V, _, R, Dic, Formula) :-
  47. ../clpb.pl:     bdd_to_formula(R, R1, Dic),
  48. ../clpb.pl:bdd_to_formula(4, V, Q, _, Dic, Formula) :-
  49. ../clpb.pl:     bdd_to_formula(Q, Q1, Dic),
  50. ../clpb.pl:bdd_to_formula(5, V, Q, _, Dic, Formula) :-
  51. ../clpb.pl:     bdd_to_formula(Q, Q1, Dic),
  52. ../clpb.pl:bdd_to_formula(6, V, _, R, Dic, Formula) :-
  53. ../clpb.pl:     bdd_to_formula(R, R1, Dic),
  54. ../clpb.pl:bdd_to_formula(7, V, Q, R, Dic, Formula) :-
  55. ../clpb.pl:     bdd_to_formula(Q, Q1, Dic),
  56. ../clpb.pl:     bdd_to_formula(R, R1, Dic),
  57. ../clpb.pl:     bdd_subst_set(Unifier0, Sub0, Sub),
  58. ../clpb.pl:     (   prolog:'$bdd_parts'(Sub, V, 1, 0) -> Unifier1=Unifier0
  59. ../clpb.pl:     bdd_subst_set(Unifier, G, G1),
  60. ../clpb.pl:     (   prolog:'$bdd_parts'(G, I, 1, 0)
  61. ../clpb.pl:     formulas_to_bdds(Parts, Graphs, 1, [], _, _),
  62. ../clpb.pl:     formulas_to_bdds(Parts, Graphs, 1, [], _, Dic),
  63. ../clpb.pl:     prolog:'$bdd_subst_reset',
  64. ../clpb.pl:formulas_to_bdds([], [], F, Dic, F, Dic).
  65. ../clpb.pl:formulas_to_bdds([E|Es], [G|Gs], F0, Dic0, F, Dic) :-
  66. ../clpb.pl:     formula_to_bdd(E, G, F0, Dic0, F1, Dic1),
  67. ../clpb.pl:     formulas_to_bdds(Es, Gs, F1, Dic1, F, Dic).
  68. ../clpb.pl:bdd_to_bdd(Graph0, Map, Graph, Free0, Free, Dic0, Dic) :-
  69. ../clpb.pl:     bdd_map_to_unifier(Map, Unifier, Free0, Free, Dic0, Dic),
  70. ../clpb.pl:     prolog:'$bdd_subst_reset',
  71. ../clpb.pl:     bdd_subst_set(Unifier, Graph0, Graph).
  72. ../clpb.pl:bdd_map_to_unifier([], [], Free, Free, Dic, Dic).
  73. ../clpb.pl:bdd_map_to_unifier([V-Formula|Map], Unifier0, Free0, Free, Dic0, Dic) :-
  74. ../clpb.pl:     formula_to_bdd(Formula1, Graph, Free0, Dic0, Free1, Dic1),
  75. ../clpb.pl:     (   prolog:'$bdd_parts'(Graph, V, 1, 0) -> Unifier0=Unifier
  76. ../clpb.pl:     bdd_map_to_unifier(Map, Unifier, Free1, Free, Dic1, Dic).
  77. ../clpb.pl:formula_to_bdd(F, Graph, Free0, Dic0, Free, Dic) :-
  78. ../clpb.pl:         bdd_to_bdd(G1, M1, Graph, Free0, Free, Dic0, Dic1),
  79. ../clpb.pl:         prolog:'$bdd_build'(Free0, 1, 0, Graph)
  80. ../clpb.pl:formula_to_bdd(F, Graph, Free0, Dic0, Free, Dic) :-
  81. ../clpb.pl:     prolog:'$bdd_build'(F, 1, 0, Graph).
  82. ../clpb.pl:formula_to_bdd(0, 0, Free, Dic, Free, Dic).
  83. ../clpb.pl:formula_to_bdd(1, 1, Free, Dic, Free, Dic).
  84. ../clpb.pl:formula_to_bdd(F1*F2, P, Free0, Dic0, Free, Dic) :-
  85. ../clpb.pl:     formula_to_bdd(F1, P1, Free0, Dic0, Free1, Dic1),
  86. ../clpb.pl:     formula_to_bdd(F2, P2, Free1, Dic1, Free, Dic),
  87. ../clpb.pl:     bdd_univ(P1, P2, 0, P).
  88. ../clpb.pl:formula_to_bdd(F1+F2, P, Free0, Dic0, Free, Dic) :-
  89. ../clpb.pl:     formula_to_bdd(F1, P1, Free0, Dic0, Free1, Dic1),
  90. ../clpb.pl:     formula_to_bdd(F2, P2, Free1, Dic1, Free, Dic),
  91. ../clpb.pl:     bdd_univ(P1, 1, P2, P).
  92. ../clpb.pl:formula_to_bdd(F1#F2, P, Free0, Dic0, Free, Dic) :- F2==1, !,
  93. ../clpb.pl:     formula_to_bdd(F1, P1, Free0, Dic0, Free, Dic),
  94. ../clpb.pl:     prolog:'$bdd_negate'(P1, P).
  95. ../clpb.pl:formula_to_bdd(F1#F2, P, Free0, Dic0, Free, Dic) :-
  96. ../clpb.pl:     formula_to_bdd(F1, P1, Free0, Dic0, Free1, Dic1),
  97. ../clpb.pl:     formula_to_bdd(F2, P2, Free1, Dic1, Free, Dic),
  98. ../clpb.pl:     prolog:'$bdd_negate'(P2, N2),
  99. ../clpb.pl:     bdd_univ(P1, N2, P2, P).
  100. ../clpb.pl:formula_to_bdd(Var^F2, P, Free0, Dic0, Free, Dic) :-
  101. ../clpb.pl:     formula_to_bdd(F2, P1, Free0, Dic0, Free, Dic),
  102. ../clpb.pl:         prolog:'$bdd_parts'(Graph, V, 1, 0)
  103. ../clpb.pl:         prolog:'$bdd_build'(-0x2000000, 1, 0, Node),
  104. ../clpb.pl:         prolog:'$bdd_subst_reset',
  105. ../clpb.pl:         bdd_subst_set([V-Node], P1, P2),
  106. ../clpb.pl:         prolog:'$bdd_parts'(P2, -0x2000000, Q, R) ->
  107. ../clpb.pl:         bdd_univ(Q, 1, R, P)
  108. ../clpb.pl:formula_to_bdd(card(Cset,List), P, Free0, Dic0, Free, Dic) :-
  109. ../clpb.pl:     card_to_bdd(Cset2, N, List3, P).
  110. ../clpb.pl:     {formula_to_bdd(X, Y, Free0, Dic0, Free1, Dic1)},
  111. ../clpb.pl:card_to_bdd(0, _, _, 0) :- !.
  112. ../clpb.pl:card_to_bdd(Cset, N, _, 1) :- Cset is (2<<N)-1, !.
  113. ../clpb.pl:card_to_bdd(1, _, List, P) :- !,
  114. ../clpb.pl:     prolog:'$bdd_negate'(P1, P).
  115. ../clpb.pl:card_to_bdd(Cset, N, List, P) :- Cset is (2<<N)-2, !,
  116. ../clpb.pl:card_to_bdd(Cset, N, List, P) :- Cset is 1<<N, !,
  117. ../clpb.pl:card_to_bdd(Cset, N, List, P) :- Cset is (1<<N)-1, !,
  118. ../clpb.pl:     prolog:'$bdd_negate'(P1, P).
  119. ../clpb.pl:card_to_bdd(Cset, N, List, P) :-
  120. ../clpb.pl:     card_to_bdd(List, L, P).
  121. ../clpb.pl:card_disj([_-X|Xs], P0, P) :- bdd_univ(X, 1, P0, P1), card_disj(Xs, P1, P).
  122. ../clpb.pl:card_conj([_-X|Xs], P0, P) :- bdd_univ(X, P0, 0, P1), card_conj(Xs, P1, P).
  123. ../clpb.pl:card_to_bdd([], [P], P).
  124. ../clpb.pl:card_to_bdd([_-X|Xs], [N|Ns], P) :-
  125. ../clpb.pl:     card_to_bdd(Xs, Ms, P).
  126. ../clpb.pl:     bdd_univ(X, N1, N0, M),
  127. ../clpb.pl:     prolog:'$bdd_parts'(Eq, V, Q, R),
  128. ../clpb.pl:     prolog:'$bdd_type'(Q, R, Type),
  129. ../clpb.pl:     prolog:'$bdd_build'(V, 1, R, Sub).
  130. ../clpb.pl:     prolog:'$bdd_negate'(Q, IQ),
  131. ../clpb.pl:     prolog:'$bdd_build'(V, IQ, 0, Sub).
  132. ../clpb.pl:     prolog:'$bdd_negate'(Q, IQ),
  133. ../clpb.pl:     prolog:'$bdd_build'(V, IQ, R, Sub),
  134. ../clpb.pl:     bdd_univ(Q, R, 0, Residue).
  135. ../clpb.pl:     prolog:'$bdd_parts'(Graph0, Var0, Q0, R0),
  136. ../clpb.pl:     prolog:'$bdd_parts'(Graph1, Var0, Q1, R1),
  137. ../clpb.pl:     bdd_univ(Q0, 1, Q1, Q),
  138. ../clpb.pl:     bdd_univ(R0, 1, R1, R),
  139. ../clpb.pl:     prolog:'$bdd_build'(Var0, Q, R, Graph),
  140. ../clpb.pl:bdd_parts(Graph, V1, Q, R, Dic) :-
  141. ../clpb.pl:     prolog:'$bdd_parts'(Graph, V, Q, R),
  142. ../clpb.pl:bdd_univ(F, G, H, Val) :-
  143. ../clpb.pl:     prolog:'$bdd_univ_case'(F, G, H, C, X, Y, Z),
  144. ../clpb.pl:     bdd_univ(C, X, Y, Z, Val).
  145. ../clpb.pl:bdd_univ(1, F, _, _, F).                     % F
  146. ../clpb.pl:bdd_univ(11, F, G, H, Val) :-                        % F*G + ~F*H, F on top
  147. ../clpb.pl:     prolog:'$bdd_parts'(F, V, FQ, FR),
  148. ../clpb.pl:     bdd_univ(FQ, FR, G, G, H, H, V, Val),
  149. ../clpb.pl:     prolog:'$bdd_store'(F, G, H, Val).
  150. ../clpb.pl:bdd_univ(12, F, G, H, Val) :-                        % F*G + ~F*H, G on top
  151. ../clpb.pl:     prolog:'$bdd_parts'(G, V, GQ, GR),
  152. ../clpb.pl:     bdd_univ(F, F, GQ, GR, H, H, V, Val),
  153. ../clpb.pl:     prolog:'$bdd_store'(F, G, H, Val).
  154. ../clpb.pl:bdd_univ(13, F, G, H, Val) :-                        % F*G + ~F*H, H on top
  155. ../clpb.pl:     prolog:'$bdd_parts'(H, V, HQ, HR),
  156. ../clpb.pl:     bdd_univ(F, F, G, G, HQ, HR, V, Val),
  157. ../clpb.pl:     prolog:'$bdd_store'(F, G, H, Val).
  158. ../clpb.pl:bdd_univ(14, F, G, H, Val) :-                        % F*G + ~F*H, FG on top
  159. ../clpb.pl:     prolog:'$bdd_parts'(F, V, FQ, FR),
  160. ../clpb.pl:     prolog:'$bdd_parts'(G, V, GQ, GR),
  161. ../clpb.pl:     bdd_univ(FQ, FR, GQ, GR, H, H, V, Val),
  162. ../clpb.pl:     prolog:'$bdd_store'(F, G, H, Val).
  163. ../clpb.pl:bdd_univ(15, F, G, H, Val) :-                        % F*G + ~F*H, FH on top
  164. ../clpb.pl:     prolog:'$bdd_parts'(F, V, FQ, FR),
  165. ../clpb.pl:     prolog:'$bdd_parts'(H, V, HQ, HR),
  166. ../clpb.pl:     bdd_univ(FQ, FR, G, G, HQ, HR, V, Val),
  167. ../clpb.pl:     prolog:'$bdd_store'(F, G, H, Val).
  168. ../clpb.pl:bdd_univ(16, F, G, H, Val) :-                        % F*G + ~F*H, GH on top
  169. ../clpb.pl:     prolog:'$bdd_parts'(G, V, GQ, GR),
  170. ../clpb.pl:     prolog:'$bdd_parts'(H, V, HQ, HR),
  171. ../clpb.pl:     bdd_univ(F, F, GQ, GR, HQ, HR, V, Val),
  172. ../clpb.pl:     prolog:'$bdd_store'(F, G, H, Val).
  173. ../clpb.pl:bdd_univ(17, F, G, H, Val) :-                        % F*G + ~F*H, FGH on top
  174. ../clpb.pl:     prolog:'$bdd_parts'(F, V, FQ, FR),
  175. ../clpb.pl:     prolog:'$bdd_parts'(G, V, GQ, GR),
  176. ../clpb.pl:     prolog:'$bdd_parts'(H, V, HQ, HR),
  177. ../clpb.pl:     bdd_univ(FQ, FR, GQ, GR, HQ, HR, V, Val),
  178. ../clpb.pl:     prolog:'$bdd_store'(F, G, H, Val).
  179. ../clpb.pl:bdd_univ(FQ, FR, GQ, GR, HQ, HR, V, Val) :-
  180. ../clpb.pl:     bdd_univ(FQ, GQ, HQ, Q),
  181. ../clpb.pl:     bdd_univ(FR, GR, HR, R),
  182. ../clpb.pl:     prolog:'$bdd_build'(V, Q, R, Val).
  183. ../clpb.pl:% bdd_subst_set(VarsGs, F, Result) :- Result is F with Vars replaced by Gs
  184. ../clpb.pl:bdd_subst_set(Unifier, In, Out) :-
  185. ../clpb.pl:     prolog:'$bdd_subst_case'(Unifier, In, C, Unifier1, AbsIn, T, Q, R),
  186. ../clpb.pl:     bdd_subst_case(C, Unifier1, AbsIn, T, Q, R, Out).
  187. ../clpb.pl:bdd_subst_case(0, _, Out, _, _, _, Out).
  188. ../clpb.pl:bdd_subst_case(1, _, Out1, _, _, _, Out) :-
  189. ../clpb.pl:     prolog:'$bdd_negate'(Out1, Out).
  190. ../clpb.pl:bdd_subst_case(10, Unifier, In, T, Q, R, Out) :- % normal recursion
  191. ../clpb.pl:     bdd_subst_set(Unifier, Q, Q1),
  192. ../clpb.pl:     bdd_subst_set(Unifier, R, R1),
  193. ../clpb.pl:     bdd_univ(T, Q1, R1, Out),
  194. ../clpb.pl:     prolog:'$bdd_subst_store'(In, Out).
  195. ../clpb.pl:bdd_subst_case(11, Unifier, In, T, Q, R, Out) :- % recurse and negate
  196. ../clpb.pl:     bdd_subst_set(Unifier, Q, Q1),
  197. ../clpb.pl:     bdd_subst_set(Unifier, R, R1),
  198. ../clpb.pl:     bdd_univ(T, Q1, R1, Out1),
  199. ../clpb.pl:     prolog:'$bdd_subst_store'(In, Out1),
  200. ../clpb.pl:     prolog:'$bdd_negate'(Out1, Out).
  201. ../clpb.pl:bdd_subst_case(20, Unifier, In, T, Q, _, Out) :- % Q=\=R, recurse
  202. ../clpb.pl:     bdd_subst_set(Unifier, Q, Q1),
  203. ../clpb.pl:     prolog:'$bdd_negate'(Q1, R1),
  204. ../clpb.pl:     bdd_univ(T, Q1, R1, Out),
  205. ../clpb.pl:     prolog:'$bdd_subst_store'(In, Out).
  206. ../clpb.pl:bdd_subst_case(21, Unifier, In, T, Q, _, Out) :- % Q=\=R, recurse and negate
  207. ../clpb.pl:     bdd_subst_set(Unifier, Q, Q1),
  208. ../clpb.pl:     prolog:'$bdd_negate'(Q1, R1),
  209. ../clpb.pl:     bdd_univ(T, Q1, R1, Out1),
  210. ../clpb.pl:     prolog:'$bdd_subst_store'(In, Out1),
  211. ../clpb.pl:     prolog:'$bdd_negate'(Out1, Out).
  212. ../zinc/tests/fcts/builtins/bool/bool_le.fzn:% RUNS ON fzn_bdd_canon
  213. ../zinc/tests/fcts/builtins/bool/bool_or.fzn:% RUNS ON fzn_bdd_canon
  214. ../zinc/tests/fcts/builtins/bool/bool_not.fzn:% RUNS ON fzn_bdd_canon
  215. ../zinc/tests/fcts/builtins/bool/bool_xor.fzn:% RUNS ON fzn_bdd_canon
  216. ../zinc/tests/fcts/builtins/bool/bool_le_reif.fzn:% RUNS ON fzn_bdd_canon
  217. ../zinc/tests/fcts/builtins/bool/bool_lt_reif.fzn:% RUNS ON fzn_bdd_canon
  218. ../zinc/tests/fcts/builtins/bool/bool_eq_reif.fzn:% RUNS ON fzn_bdd_canon
  219. ../zinc/tests/fcts/builtins/bool/bool_eq.fzn:% RUNS ON fzn_bdd_canon
  220. ../zinc/tests/fcts/builtins/bool/bool_lt.fzn:% RUNS ON fzn_bdd_canon
  221. ../zinc/tests/fcts/builtins/bool/bool_and.fzn:% RUNS ON fzn_bdd_canon
  222. root@gitlab:/mnt/sdf1/usr/local/sicstus4.3.5/lib/sicstus-4.3.5/library/clpfd#  wc -l ../clpb.pl  *.c *.h
  223.     760 ../clpb.pl
  224.     800 ac3intervals.c
  225.     490 alldifferent.c
  226.    2856 alldistinct.c
  227.     942 arith.c
  228.    1471 bc_alldiff.c
  229.     421 bool.c
  230.    7422 discrete.c
  231.    5269 disjoint2.c
  232.    1500 dvars.c
  233.    1988 fdsets.c
  234.    2001 gcc.c
  235.   11060 geost.c
  236.    3619 indexical.c
  237.     892 keysorting.c
  238.     639 lcc.c
  239.    1335 lex.c
  240.    1337 lh.c
  241.    1183 lin.c
  242.    1051 linfast.c
  243.     540 linpbool.c
  244.     308 linubool.c
  245.     262 main.c
  246.    1662 mddi.c
  247.    2086 multi_cumulative.c
  248.    1242 nvalue.c
  249.     409 profile.c
  250.     592 reified.c
  251.    1229 relation.c
  252.     490 setsingleton.c
  253.     871 sorting.c
  254.      63 statistics.c
  255.    1647 support.c
  256.    2563 symmcum.c
  257.     463 dvars.h
  258.     975 fd.h
  259.     268 fd_insn.h
  260.   62706 total
  261. root@gitlab:/mnt/sdf1/usr/local/sicstus4.3.5/lib/sicstus-4.3.5/library/clpfd#
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!