%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% Simulates a Random Access Machine as defined in
%
%   John E. Savage. Models of Computation: Exploring the Power of Computing.
%   Addisson-Wesley, ISBN 0-201-89539-0, 1998.
%
%
% Usage: specify program as prog/4 constraints
%	 initialize the necessary memory cells to zero (you can use initmem/1),
%	 execution starts when the location(<firstlabel>) constraint is added.
%
% prog(label,nextlabel,instruction,operand)
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- use_module(library(chr)).

:- chr_option(inplace_updates,off).
:- chr_option(suspension_reuse,off).
%:- chr_option(reduced_garbage,off).
%:- chr_option(suspension_reuse_profiling,on).

:- chr_constraint mem(+dense_int,+int), prog(+dense_int,+int,+any,+int), prog_counter(+int).
%:- chr_constraint mem(+,+), prog(+,+,+,+), prog_counter(+).
%:- chr_constraint mem/2, prog/4, prog_counter/1.



%mem(A,_) \ mem(A,_) <=> true.

% add value of register B to register A
prog(L,L1,add(B),A), mem(B,Y) \ mem(A,X), prog_counter(L) <=> 
     Z is X+Y, mem(A,Z), prog_counter(L1).
% subtract value of register B from register A
prog(L,L1,sub(B),A), mem(B,Y) \ mem(A,X), prog_counter(L) <=> 
    Z is X-Y, mem(A,Z), prog_counter(L1).
% multiply register A with value of register B
prog(L,L1,mult(B),A), mem(B,Y) \ mem(A,X), prog_counter(L) <=> 
    Z is X*Y, mem(A,Z), prog_counter(L1).
% divide register A by value of register B
prog(L,L1,div(B),A), mem(B,Y) \ mem(A,X), prog_counter(L) <=> 
    Z is X//Y, mem(A,Z), prog_counter(L1).


% put the value in register B in register A
prog(L,L1,move(B),A), mem(B,X) \ mem(A,_), prog_counter(L) <=> 
    mem(A,X), prog_counter(L1).
% put the value in register <value in register B> in register A
prog(L,L1,i_move(B),A), mem(B,C), mem(C,X) \ mem(A,_), prog_counter(L) <=> 
    mem(A,X), prog_counter(L1).
% put the value in register B in register <value in register A>
prog(L,L1,move_i(B),A), mem(B,X), mem(A,C) \ mem(C,_), prog_counter(L) <=> 
    mem(C,X), prog_counter(L1).

%i_move_i(B), A : i_move(B), 0
%	  	  move_i(0), A

% put the value B in register A        -> redundant if consts are in init mem
prog(L,L1,const(B),A) \ mem(A,_), prog_counter(L) <=> 
    mem(A,B), prog_counter(L1).
%prog(L,L1,clr,A) \ mem(A,X), prog_counter(L) <=>   % same as const(0)
%    mem(A,0), prog_counter(L1).


% unconditional jump to label A
prog(L,L1,Instr,A) \ prog_counter(L) <=> Instr == jump |
    prog_counter(A).
% jump to label A if register R is zero, otherwise continue
prog(L,L1,cjump(R),A), mem(R,X) \ prog_counter(L) <=> X == 0 |
    prog_counter(A).
prog(L,L1,cjump(R),A), mem(R,X) \ prog_counter(L) <=> X =\= 0 |
    prog_counter(L1).

% halt
prog(L,L1,Instr,_) \ prog_counter(L) <=> Instr == halt | true.

% invalid instruction
prog_counter(L) <=> true.

%:- constraints 	initmem(+natural).
%
%initmem(N) <=> N =:= 0 | mem(0,0).
%initmem(N) <=> N>0 | mem(N,0), N1 is N-1, initmem(N1).



init(N) :- 
	mem(1,1), 
	mem(2,N), 
	mem(3,0),
	prog(1,2, add(1), 3),
	prog(2,3, sub(1), 2),
	prog(3,1, cjump(2), 4),
	prog(4,0, halt, 0).



main :-
	main(100000).

main(N):-
        init(N),
        measure(prog_counter(1), true, T1,T2,_) ->
	%chr_runtime:show_store(user),
        statistics,
	write(N: T1 - T2), write('.'),nl, fail.
%main(N) :- N1 is N*2, main(N1).
main(_).

measure(G,_,Time,GTime,swi) :-
	cputime(X),	gctime(Y),
	call(G),
	cputime(Now),	gctime(NowG),
	GTime is NowG-Y,
	Time is Now-X-GTime.
cputime(Time) :- statistics(runtime, [Time,_]).
gctime(Time) :- statistics(garbage_collection, [_,_,Time]).