I am learning pldoc for the time in the future when I might show codes for one who asks me.
As sample, below is codes with %! comments. I am not sure for now if it fits the pldoc recommendation. The code is on gf2-solver for systems of polynomial equations over GF2. It is
an initial version, but I have no idea and plan to revise it. It seems difficult for me. I like more easier prolog programming.
gf2_system_solver
/**************************
* gf2_system_solver *
**************************/
%! gf2_solve_system(+Vs, +Eqs, -Sols, +S) is det.
% Vs : a list varialbles (indeterminates) of Eqs.
% Eqs: a list [P1, P2, ..., Pn] as a system of equations
% P1 = 0, P2 = 0, ...,, Pn = 0 of polynomials over GF2.
% Sols is unified with a zdd of a family of all subsets U of Vs
% such that U satisfies all Pi = 0.
% ?- #S, X<< (a+b), Y<< (x+y),
% gf2_solve_system([a,b,x,y], [X, Y], Z, S), psa(Z, S), card(Z, C, S).
gf2_solve_system(Ls, Eqs, Sols, S):- zdd_power(Ls, Ini, S),
gf2_solve_system(Ls, Eqs, Ini, Sols, S).
%
gf2_solve_system(_, [], Y, Y, _):-!.
gf2_solve_system(_, _, 0, 0, _):-!.
gf2_solve_system(Ls, [X|Xs], Y, Z, S):-
solve(Ls, X, Sols, S),
zdd_meet(Sols, Y, Y0, S),
gf2_solve_system(Ls, Xs, Y0, Z, S).
%! gf2_solve(+Vs, +X, -Sols, +S) is det.
% Vs: indeterminates(variables) of a polynomial over GF2.
% X : a zdd of the polynomial.
% Sols is unified with a zdd of all solutions of the polynomial.
% ?- A = [], #S, X<<pow(A), gf2_solve([], 0, Y, S), psa(Y, S).
% ?- A = [], #S, X<<pow(A), gf2_solve([], 1, Y, S), psa(Y, S).
% ?- A = [c], #S, zdd_singleton(c, C, S), gf2_solve(A, C, Y, S), psa(Y, S).
% ?- A = [a, b], #S, gf2_solve(A, 0, Y, S), psa(Y, S).
% ?- A = [], #S, X<<pow(A), gf2_solve([], X, Y, S), psa(Y, S).
% ?- A = [a], #S, X<<pow(A), gf2_solve(A, X, Y, S), psa(Y, S).
% ?- #S, X<< +[a, b], psa(X, S), gf2_solve([a,b], X, Y, S), psa(Y, S).
% ?- #S, X<< *[a, b], psa(X, S), gf2_solve([a,b], X, Y, S), psa(Y, S).
% ?- #S, X<< +[a], psa(X, S), gf2_solve([a], X, Y, S), psa(Y, S).
% ?- #S, X<< *[a,b], psa(X, S), gf2_solve([a,b], X, Y, S), psa(Y, S).
% ?- #S, X<< (*a), psa(X, S), gf2_solve([a], X, Y, S), psa(Y, S).
% ?- #S, gf2_solve([a], 0, Y, S), psa(Y, S).
% ?- #S, X<< (a*b + 1), psa(X, S), gf2_solve([a,b], X, Y, S), psa(Y, S), card(Y, C, S).
% ?- #S, X<< (a*b + x*y), psa(X, S), gf2_solve([a,b], X, Y, S), psa(Y, S), card(Y, C, S).
% ?- #S, X<< (a*b + x*y), psa(X, S), gf2_solve([a,b,x,y], X, Y, S), psa(Y, S), card(Y, C, S).
% ?- #S, X<< (a+b+x+y), psa(X, S), gf2_solve([a,b,x,y], X, Y, S), psa(Y, S), card(Y, C, S).
gf2_solve(Ls, 0, Sols, S):-!, zdd_power(Ls, Sols, S).
gf2_solve(Ls, X, Sols, S):- select_constant(X, C, X0, S),
( C = 0 -> gf2_solve_eq0(Ls, X0, Sols, S)
; gf2_solve_eq0(Ls, X0, Sols0, S),
zdd_power(Ls, All, S),
zdd_subtr(All, Sols0, Sols, S)
).
%
gf2_solve_eq0(Ls, 0, X, S):-!, zdd_power(Ls, X, S).
gf2_solve_eq0(_, 1, 0, _):-!.
gf2_solve_eq0(Ls, P, X, S):- memo(gf2_solve(P, Ls)-X, S),
( nonvar(X) -> true %, write(.) % no hits. Useless here ?
; cofact(P, t(A, L, R), S),
divide_at(A, Ls, H, T),
zdd_power(T, PowT, S),
cofact(PowAT, t(A, PowT, PowT), S),
( gf2_solve_eq0(T, R, R0, S),
cofact(AR_sols_zero, t(A, PowT, R0), S),
gf2_solve_eq0(T, L, L0, S),
cofact(L_sols_zero, t(A, L0, L0), S),
zdd_meet(AR_sols_zero, L_sols_zero, Sols_zero, S),
zdd_subtr(PowAT, AR_sols_zero, AR_sols_unit, S),
zdd_subtr(PowAT, L_sols_zero, L_sols_unit, S),
zdd_meet(AR_sols_unit, L_sols_unit, Sols_unit, S),
zdd_join(Sols_zero, Sols_unit, Sols0, S)
),
prefix_pow_rev(H, Sols0, X, S)
).
Helpers
/*****************
* Helpers *
*****************/
% ?- #S, select_constant(0, X, Y, S).
% ?- #S, select_constant(1, X, Y, S).
% ?- #S, X<< (*[a]+1), psa(X, S), select_constant(X, C, Y, S), psa(Y, S).
% ?- #S, X<< (*[a]), select_constant(X, C, Y, S), psa(Y, S).
select_constant(X, 1, Z, S):- zdd_has_1(X, S), !,
zdd_subtr(X, 1, Z, S).
select_constant(X, 0, X, _).
% ?- divide_at(a, [x,a, y], H, T).
% ?- divide_at(a, [x,y,a], H, T).
divide_at(A, L, H, T):- divide_at(A, L, [], H, T).
%
divide_at(A, [A|T], H, H, T):-!.
divide_at(A, [B|T], H, H0, T0):-
divide_at(A, T, [B|H], H0, T0).
% ?- #S, prefix_pow_rev([b, a], 1, X, S), psa(X, S).
% ?- #S, prefix_pow_rev([b], 1, X, S), prefix_pow_rev([a], X, Y, S).
prefix_pow_rev([], X, X, _).
prefix_pow_rev([A|As], X, Y, S):-
cofact(X0, t(A, X, X), S),
prefix_pow_rev(As, X0, Y, S).