1:- module(zdd_misc, [subst_atomic/3]). 2:- use_module(zdd('zdd-array')). 3 4% :- use_module(pac(basic)). 5% From util(math). 6% ?- bdd_bench:subst_atomic([1-true, 0-false], f(1,0,1), R). 7%@ R = f(true, false, true). 8% ?- bdd_bench:subst_atomic([1-true, 0-false], g([1,0,1], f(0)), R). 9 10% ?- rel_to_fun([1-2,1-3,2-3],R). 11%% rel_to_fun(+R, -F) is det. 12% Unify F with a function from dom(R) to 13% the pow(ran(R)) which assigns to each A in dom(R) 14% the set of B in ran(R) such that A and B stands in the realtion R. 15 16rel_to_fun(X, Y):- rel_to_fun(X, Y, []). 17 18rel_to_fun([], Y, Y). 19rel_to_fun([A-B|R], [A-[B|P]|Y], Z):- 20 rel_to_fun(R, A, R0, P, []), 21 rel_to_fun(R0, Y, Z). 22% 23rel_to_fun([], _, [], P, P). 24rel_to_fun([A-B|R], A, U, [B|P], Q):-!, 25 rel_to_fun(R, A, U, P, Q). 26rel_to_fun(R, _, R, P, P). 27 28% ?- zdd_misc:key_val_check([a-b], a, X). 29% ?- zdd_misc:key_val_check([a-b], c, X). 30 31key_val_check([X-Y|_], X, Y) :-!. 32key_val_check([P|_], X, Y) :- arg(1, P, X), !, arg(2, P, Y). 33key_val_check([_|A], X, Y) :- key_val_check(A, X, Y).
?- zdd_misc:subst_atomic([a-b, b-a], f(a, b), F).
?- zdd_misc:subst_atomic([a-b, b-a], f(c, d), F).
44subst_atomic(M, X, Y) :- 45 ( atomic(X), ( key_val_check(M, X, Y); Y = X ), ! 46 ; functor(X, F, N), 47 functor(Y, F, N), 48 subst_atomic_args(N, M, X, Y) 49 ). 50 51% 52subst_atomic_args(0, _, _, _) :- !. 53subst_atomic_args(J, M, X, Y) :- 54 arg(J, X, A), 55 arg(J, Y, B), 56 subst_atomic(M, A, B), 57 K is J-1, 58 subst_atomic_args(K, M, X, Y).
dom(M) | P(A) is true}.
That is, the substitution M' on the terms is defined as follows:
dom(M), then M'(X) = M(X).f(X1,...,Xn), M'(X) = f(M'(X1), ..., M'(Xn)).
?- zdd_misc:pred_subst(atomic, [a-b, b-a], f(a, b), F).
?- zdd_misc:pred_subst(integer, [a-b, b-a], f(a, b), F).
?- zdd_misc:pred_subst(atom, [a-b, b-a, 1-c], [a, 1,[a,b], f(a,b), b,c], F).
@ F = [b, 1, [b, a], f(b, a), a, c].
?- zdd_misc:pred_subst(atomic, [a-b, b-a, 1-c], [a, 1,[a,b], f(a,b), b,c], F).
@ F = [b, c, [b, a], f(b, a), a, c].
?- zdd_misc:pred_subst(atomic, [a-b, b-a, a(b)-c], a(b), F).
@ F = a(a).
78:- meta_predicate pred_subst(, , , ). 79pred_subst(Pred, M, X, Y) :- 80 ( call(Pred, X), key_val_check(M, X, Y) -> true 81 ; atomic(X) -> Y = X 82 ; functor(X, F, N), 83 functor(Y, F, N), 84 pred_subst_args(N, Pred, M, X, Y) 85 ). 86 87% 88pred_subst_args(0, _, _, _, _) :- !. 89pred_subst_args(J, Pred, M, X, Y) :- 90 arg(J, X, A), 91 arg(J, Y, B), 92 pred_subst(Pred, M, A, B), 93 K is J-1, 94 pred_subst_args(K, Pred, M, X, Y). 95 96 97% ?- module(zdd_misc). 98% ?- empty_assoc(E). 99% ?- empty_assoc(E), assoc(E, a, b, R), assoc(R, a, A, R0), 100% assoc(R0, b, c, R1), assoc(R1, a, A0, R2), 101% assoc(R2, b, B, R3). 102%@ E = (-), 103%@ R = R0, R0 = t(a, b, -, -), 104%@ A = A0, A0 = b, 105%@ R1 = R2, R2 = R3, R3 = t(a, b, -, t(b, c, -, -)), 106%@ B = c. 107 108empty_assoc(_). 109 110% no update version. 111%% assoc(+T, +X, -Y) 112% Unify Y with X such that Y is associated with X 113% in T. 114 115assoc(T, X, Y):- var(T), !, T = t(X, Y, _, _). 116assoc(t(X, Y, _, _), X, Y):- !. 117assoc(t(U, _, L, R), X, Y):- 118 ( X @< U 119 -> assoc(L, X, Y) 120 ; assoc(R, X, Y) 121 ). 122 123% normal (update) version. 124%% assoc(+T, +X, -Y, -U) is det. 125% An assoc list U is unified with a minimum extension of an assoc list T, 126% and Y with a term such that Y is associated with X in U. 127 128assoc(-, X, Y, t(X, Y, -, -)):-!. 129assoc(t(X, Y, L, R), X, Y, t(X, Y, L, R)):- !. 130assoc(t(U, V, L, R), X, Y, t(U, V, L0, R0)):- 131 ( X @< U 132 -> R0 = R, 133 assoc(L, X, Y, L0) 134 ; L0 = L, 135 assoc(R, X, Y, R0) 136).
144zip([], [], []). 145zip([X|Xs], [Y|Ys], [Z|Zs]) :- 146 ( Z = X-Y 147 ; Z = (X:Y) 148 ; functor(Z, X, 1), 149 arg(1, Z, Y) 150 ), !, 151 zip(Xs, Ys, Zs). 152 153% % Complementary conjunction 154% slim_rule(A, true):- literal_in(+, A, not(X)), 155% literal_in(+, A, X). 156% % 157% literal_in(+, X+_, Y):- literal_in(+, X, Y). 158% literal_in(+, _+X, Y):- literal_in(+, X, Y). 159% literal_in(_, X, X):- (atomic(X); X = not(_)). 160 161 /************** 162 * math * 163 **************/ 164% ?- Z is gcd(10, 11). 165% ?- A is gcd(0, 3). 166% ?- gcd([12, 6, 4], Z). 167% ?- lcm([1,2,3,4,5,6,7,8], Z). 168% ?- mul_list([1,2,3,4,5,6,7,8,9,10], Z). 169% ?- factorial(10, F), numlist(1, 10, L), mul_list(L, F). 170 171mul_list([], 1). 172mul_list([A|As], M):- mul_list(As, M0), M is A * M0. 173 174% ?- nCr(4,2,Z), factorial(4, R), factorial(2, S), factorial(2, T), Z is div(R, S*T). 175nCr_list(M, R):- sum_list(M, S), factorial(S, FS), 176 mul_fact_list(M, 1, PF), 177 R is div(FS, PF). 178% 179mul_fact_list([], X, X). 180mul_fact_list([A|As], X, Y):- factorial(A, FA), X0 is X*FA, 181 mul_fact_list(As, X0, Y). 182 183lcm(X, Y, L):- L is div(X*Y, gcd(X, Y)). 184 185lcm([],1). 186lcm([A|As], L):- lcm(As, L0), lcm(A, L0, L). 187 188gcd([], 0):-!. 189gcd([A|As], G):- gcd(As, G0), G is gcd(A, G0). 190 191% 192sum_prod([], _, N, N). 193sum_prod([P|Ps], Ws, U, V):- 194 prod(P, Ws, 1, Q), 195 multi_combi(P, MC), 196 U0 is Q*MC + U, 197 sum_prod(Ps, Ws, U0, V). 198 199prod([], _, V, V). 200prod([A|As], [W|Ws], U, V):- 201 U0 is (W**A)*U, 202 prod(As, Ws, U0, V). 203 204 205% ?- module(zdd_misc). 206% ?- N=2, setof(P->Q, move(N, P->Q), Moves), zdd:univ_to_binary(->(Moves), Log). 207 208move(N, p(I, J)->p(K, L)):- 209 between(0, N, I), 210 between(0, N, J), 211 between(0, N, K), 212 between(0, N, L), 213 one_step(p(I,J), p(K,L)). 214% 215one_step(p(I,J),p(I0, J)):- succ(I, I0). 216one_step(p(I,J),p(I, J0)):- succ(J, J0). 217 218 219% ?- reverse_dag(3,f(a-[2,1,3], a-[1], a-[1,2]), R). 220%@ R = f([1, 2, 3], [1, 3], [1]) . 221 222reverse_dag(N, D, R):- functor(D, F, K), 223 functor(R, F, K), 224 initial_args(R, []), 225 reverse_dag_step(N, D, R). 226% 227reverse_dag_step(0, _, _):-!. 228reverse_dag_step(I, A, B):-arg(I, A, E), 229 E = _- S, 230 reverse_direction(S, I, B), 231 succ(J, I), 232 reverse_dag_step(J, A, B). 233% 234reverse_direction([], _, _). 235reverse_direction([J|Js], I, A):- arg(J, A, S), 236 setarg(J, A, [I|S]), 237 reverse_direction(Js, I, A). 238 239 240% 241product_with_atom(_, true, true):- !. 242product_with_atom(_, false, false):-!. 243product_with_atom(A, X, Y):- cofact(X, if(I, L, R)), 244 product_with_atom(A, L, L0), 245 product_with_atom(A, R, R0), 246 make_pair(A, I, Pair), 247 cofact(Y, if(Pair, L0, R0)). 248 249% 250succ_list_to_zdd(Initial, Dag, Initial0, Index):- 251 internalize(Initial-Dag, U), 252 U = Initial0-Dag0, 253 succ_list_to_zdd(Dag0, Index). 254% 255succ_list_to_zdd([], _). 256succ_list_to_zdd([X-As|G], IDX):- 257 succ_list_to_zdd(G, IDX), 258 elem(X, IDX, V), 259 succ_list_to_zdd_with_index(As, X, V0, IDX), 260 V = V0. 261% 262succ_list_to_zdd_with_index(false, _, false, _):-!. 263succ_list_to_zdd_with_index(true, X, U, IDX):-!, 264 succ_list_to_zdd_with_index([], X, U, IDX). 265succ_list_to_zdd_with_index([], X, U, _):-!, 266 cofact(U, if(X, true, false)). 267succ_list_to_zdd_with_index([A], X, U, IDX):-!, 268 elem(A, IDX, R), 269 cofact(U, if(X, R, false)). 270succ_list_to_zdd_with_index([A|As], X, U, IDX):- 271 succ_list_to_zdd_with_index(As, X, V, IDX), 272 elem(A, IDX, R), 273 ( nonvar(R) 274 -> cofact(W,if(X, R, false)), 275 zdd([join(W, V, U)]) 276 ; R = false 277% ; throw(forward_reference_bug(A)) 278 ). 279% ?- module(zdd_misc). 280% ?- time(zdd_misc:usual_n_queens(8, C)). 281 282%@ % 68,761 inferences, 0.008 CPU in 0.008 seconds (98% CPU, 8581181 Lips) 283%@ C = 92 . 284% ?- time(zdd_misc:usual_n_queens(9, C)). 285%@ % 304,612 inferences, 0.032 CPU in 0.033 seconds (99% CPU, 9450315 Lips) 286%@ C = 352 . 287 288%@ % 304,481 inferences, 0.033 CPU in 0.033 seconds (99% CPU, 9203827 Lips) 289%@ C = 352 . 290%@ % 304,612 inferences, 0.034 CPU in 0.034 seconds (99% CPU, 9056130 Lips) 291% ?- time(zdd_misc:usual_n_queens(10, C)). 292%@ % 1,394,360 inferences, 0.155 CPU in 0.156 seconds (100% CPU, 9002318 Lips) 293%@ C = 724 . 294 295% ?- time(zdd_misc:usual_n_queens(13, C)). 296% ?- time(zdd_misc:usual_n_queens(14, C)). 297%@ % 1,360,772,993 inferences, 175.021 CPU in 175.629 seconds (100% CPU, 7774894 Lips) 298%@ C = 365596 . 299%@ C = 365596. 300% ?- time(zdd_misc:usual_n_queens(15, C)). 301 302% 303usual_n_queens(N, Count):- zdd:n_queen_matrix(N, M), 304 usual_n_queens(M, [], [], [], S), 305 length(S, Count). 306% 307usual_n_queens([], _, _, _, [[]]). 308usual_n_queens([C|R], Po, Ne, Ho, U):- 309 usual_n_queens(C, R, Po, Ne, Ho, U). 310% 311usual_n_queens([], _, _, _, _, []). 312usual_n_queens([_I-J|D], R, Po, Ne, Ho, U):- memberchk(J, Ho), !, 313 usual_n_queens(D, R, Po, Ne, Ho, U). 314usual_n_queens([I-J|D], R, Po, Ne, Ho, U):- K is I+J, L is I-J, 315 ( zdd:check_safe(K, L, Po, Ne) 316 -> usual_n_queens(R, [K|Po], [L|Ne], [J|Ho], V), 317 maplist(zdd:cons(K-L), V, V0), 318 usual_n_queens(D, R, Po, Ne, Ho, U0), 319 append(V0, U0, U) 320 ; usual_n_queens(D, R, Po, Ne, Ho, U) 321 )