/* 

  Reversible version of factorial in Picat.

  This program shows how to do a reversible version of factorial(N,F)
  i.e. where both N and F can be given as variables.

  It also shows a reversible CP version.

  Note that factorial1/2 (but not factorial/2 since it use once/1 for convenience) 
  is also generating the solutions:
  Picat> factorial1(N,F)
  N = 0
  F = 1 ?;
  N = 1
  F = 1 ?;
  N = 2
  F = 2 ?;
  N = 3
  F = 6 ?;
  N = 4
  F = 24 ?;
  N = 5
  F = 120 ?;
  N = 6
  F = 720 ?;
  N = 7
  F = 5040 ?


  This Picat model was created by Hakan Kjellerstrand, hakank@gmail.com
  See also my Picat page: http://www.hakank.org/picat/

*/

import cp.

main => go.

%
% Plain Picat
%
go => 
   factorial(7,F7),
   println(f7=F7),
   factorial(N5040,5040),
   println(n5040=N5040),

   factorial(17,F17),
   println(f17=F17),
   factorial(N17,F17),
   println(n17=N17),

   factorial(18,F18),
   factorial(N18,F18),
   println([f18=F18,n18=N18]),

   factorial(19,F19),
   factorial(N19,F19),
   println([f19=F19,n19=N19]),

   nl.

% some harder cases
go2 =>
   foreach(I in 1..11)
     println(i=I),
     N = 2**I,
     println(n=N),
     time(factorial(N,F1)),
     println(f1=F1),
     println(len=F1.to_string.len), % number of digits
     
     % and back
     time(factorial(N2,F1)),
     println(n2=N2),
     nl
   end,
   nl.


%
% CP version
% Note: For N > 18, factorial(N) is larger than domain of CP variables - 2**56 - (and will fail).
%
go3 =>
   foreach(I in 0..19) 
     time2(println(check_cp(I)))
   end,
   nl.


%
% This version of factorial/2 is reversible
% once/1 added so we don't get into infinite loop
% if/when backtracking.
%
% It don't need to be tabled.
% table
factorial(N,F) =>
  once(factorial1(N,F)).

% note: if stated as fact(0,F) it don't work.
% This should _not_ be tabled.
factorial1(N,F) :-
  N = 0,
  F = 1.
factorial1(N,F) :-
  factorial1(N1,F1),
  N = N1 + 1,
  F = N * F1.


% CP version
factorial_cp(N,F) ?=> 
  N #= 0,
  F #= 1.
factorial_cp(N,F) => 
  N #> 0, N #<= F,
  N1 #= N-1,
  factorial_cp(N1,F1),
  F #= N*F1.

check_cp(N) = [n=N,f=F,n2=N2] =>
  factorial_cp(N,F),  % forward
  factorial_cp(N2,F). % and back