declare

% Lazy problem solving (Solve)

% This is the Solve operation, which returns a lazy list of solutions
% to a relational program.  The list is ordered according to a
% depth-first traversal.  Solve is written using the computation space
% operations of the Space module.


%% 9/28/06 JTH added a counter for non-succeeded nodes of the search tree
local Counter={NewCell 0} in
   fun {Solve Script}
      Counter := 0
    {SolStep {Space.new Script} nil}
   end

   fun {SolStep S Rest}
      case {Space.ask S}
      of failed then Counter := @Counter+1 Rest
      [] succeeded then {Space.merge S}|Rest
      [] alternatives(N) then {SolLoop S 1 N Rest}
      end
   end

   fun lazy {SolLoop S I N Rest}
      Counter := @Counter+1 
      if I>N then Rest
      elseif I==N then   %% last alternative
	 %% thus, we don't need to clone S, we already cloned enough for I through N-1
	 
	 %% so commit to this one with I==N and see what happens
	 {Space.commit S I}   %% resume execution inside S, keeps running (?)
	 %% until achieves alternatives(N), failed, merged or succeeded

	 {SolStep S Rest}     %% meanwhile we continue on
	 
      else Right C in
	 Right={SolLoop S I+1 N Rest}     %% by laziness this doesn't really execute

	 C={Space.clone S} %% we do need to clone this so as not to ruin S for the others

	 {Space.commit C I}           
	 {SolStep C Right}
      end
   end

   fun {SolveOne F}
      L={Solve F}
   in
      if L==nil then nil else [L.1] end
   end
   
   fun {SolveAll F}
      L={Solve F}
      proc {TouchAll L}
	 if L==nil then skip else {TouchAll L.2} end
      end
   in
      {TouchAll L}
      L
   end

   fun {ShowCounter}
      @Counter
   end
end