procedure execlb (R1 : Int ; var R : Int) ;  begin     R := R1 ;     with R.lo do        if (cardinality = infinite) then           R.hi := MinusFiniteS         else           R.hi := R.lo ;     R.hi.edge := hin ;     R.lo := MinusInfS ;  end ;procedure execub (var X , Xd : Int) ;var     Dum : Int ;       begin     Xd := X ;     execadd (Xd, Dum, Zero, Dum, Xd, Dum) ;     execlb (Xd,Xd) ;     execadd (Xd, Dum, Zero, Dum, Xd, Dum) ;  end ;procedure execcopy (R0 :Int; var R1:Int);begin  R1:=R0;end;procedure execless(var Sr:State; var R0,R1:Int);{R0 < R1}begin   if Point(R0) or Point(R1) then Sr:=-1;   if gtS(R1.lo,R0.hi) then Sr:= -1 else   begin      R0.hi:=R1.hi;      R0.hi.edge:=hout;      R1.lo:=R0.lo;      R1.lo.edge:=lout;   end;end;{execless}procedure execleq(var Sr:State; var R0,R1:Int);{R0 =< R1}begin   if Point(R0) or Point(R1) then Sr:=-1;   if geS(R1.lo,R0.hi) then Sr:= -1 else   begin      R0.hi:=R1.hi;      R1.lo:=R0.lo;   end;end;{execleq}procedure execnoteq(var Sr:State; var R0,R1:Int);{R0 <> R1}begin   case Sr of   0:{nothing done yet}     begin     if gtS(R0.lo,R1.hi) or gtS(R1.lo,R0.hi)      then Sr:=-1 {no need to check in future}     else      begin        if Point(R0) then 	begin	   OuterExec(PC,DCurr,true,1,Counter,Level+1);	   Sr:=2;	   execless(Sr,R1,R0);	end else	if Point(R1) then	begin	   OuterExec(PC,DCurr,true,2,Counter,Level+1);	   Sr:=1;	   execless(Sr,R0,R1);	end;     end;     end;   1:execless(Sr,R0,R1);   2:execless(Sr,R1,R0);   end;end;{execnoteq}procedure execsqrr(var R0,R1:Int);begin{execsqrr}end;{execsqrr}procedure execminr(var R0,R1,R2:Int);begin{execminr}end;{execminr}procedure execmaxr(var R0,R1,R2:Int);  procedure chmaxhi(S0,S1:Sreal; var S2:Sreal);  var Closed:boolean;  Exp,M0,M1:integer;  begin{chmaxhi}  with S2 do  begin     if (S0.cardinality=infinite)or(S1.cardinality=infinite) then     begin          S2:=PlusInfS;        Closed:=((S0.cardinality=infinite)and(S0.edge=hin))or	        ((S1.cardinality=infinite)and(S1.edge=hin));     end else     begin        Closed:=(S0.edge=hin)and(S1.edge=hin);        AlignUp(S0.exp,S0.mantissa,S1.exp,S1.mantissa,Exp,M0,M1,Closed);        if M1 > M0 then           M0 := M1 ;	NormalizeUp(Exp,M0,S2,Closed)     end;     if Closed then S2.edge:=hin else S2.edge:=hout;  end;  end;{chmaxhi}    procedure chmaxlo(S0,S1:Sreal; var S2:Sreal);  var Closed:boolean;  Exp,M0,M1:integer;  begin{chmaxlo}  with S2 do  begin     if (S0.cardinality=infinite)or(S1.cardinality=infinite) then     begin          S2:=MinusInfS;        Closed:=((S0.cardinality=infinite)and(S0.edge=lin))or	        ((S1.cardinality=infinite)and(S1.edge=lin));     end else     begin        Closed:=(S0.edge=lin)and(S1.edge=lin);        AlignUp(S0.exp,-S0.mantissa,S1.exp,-S1.mantissa,Exp,M0,M1,Closed);	NormalizeUp(Exp,M0+M1,S2,Closed); mantissa:=-mantissa;     end;     if Closed then S2.edge:=lin else S2.edge:=lout;  end;  end;{addlo}begin{execmaxr}end;{execmaxr}procedure execmodu(var R0,R1,R2:Int);begin{execmodu}end;{execmodu}procedure execabsr(var R0,R1:Int);begin{execabsr}end;{execabsr}procedure exectrig(var R0,R1,R2:Int);begin{exectrig}end;{exectrig}procedure execexpr(var R0,R1:Int);begin{execexpr}end;{execexpr}function Exec(I:Instr;var PC:Loc0;var Change:boolean):boolean;var	R:array[0..Par] of Int;  {working registers}	Sr:State;  {State register}	P:0..Par;	E:boolean;	NewPC:Loc0;	TraceChange:boolean;   procedure WritePars; {write out list of parameter registers for curr ins}   begin   with I do   begin      write(PC:2,Code:5,Sr:3);      for P := 0 to Par do         if Pars[P] <> 0 then 	 begin	    write(Pars[P]:3);	    WriteInt(R[P]);	 end;      writeln;   end;   end;{WritePars}begin{Exec}with I,DCurr dobegin   Counter:=Counter+1;   {get parameters}   for P := 0 to ParN[Code] do    begin R[P]:=D[Pars[P]]; assert(CheckInt(R[P]));   end;      Sr:=S[PC];   if Debug >= trace then  begin write(' '); WritePars; end;   E:=true;   Change:=false;   NewPC:=PC;{!!}case Code of    print: execprint(PC,Pars[0],R[0]);   pr   : execpr(Sr,Pars[0]);   tr   : exectr(Sr,Pars[0]);   soln : execsoln(Sr,Pars[0]);   readr: execreadr(Sr,R[0]);   halve: exechalve(NewPC,Sr,R[0],E,Change);   halves:exechalves(NewPC,Sr,R[0],E,Change);   linh : execlinh(NewPC,Sr,R[0],E,Change);   mult : execmult (Sr,R[0],R[1],R[2],R[0],R[1],R[2],E);   add  : execadd  (R[0],R[1],R[2],R[0],R[1],R[2]);   intgr: execintgr(Sr,R[0]);   less : execless (Sr,R[0],R[1]);   leq  : execleq  (Sr,R[0],R[1]);   noteq: execnoteq(Sr,R[0],R[1]);   sqrr : execsqrr(R[0],R[1]);   minr : execminr(R[0],R[1],R[2]);   maxr : execmaxr(R[0],R[1],R[2]);   modu : execmodu(R[0],R[1],R[2]);   absr : execabsr(R[0],R[1]);   trig : exectrig(R[0],R[1],R[2]);   expr : execexpr(R[0],R[1]);   lb   : execlb (R[0],R[1]);   ub   : execub (R[0],R[1]);   copy : execcopy(R[0],R[1]);   end;   TraceChange:=false;   AllPoints:=true;   for P := 0 to ParN[Code] do   with D[Pars[P]] do   begin      if DF.PF[Pars[P]]=PPrint then TraceChange:=true;      assert(CheckLo(R[P].lo));assert(CheckHi(R[P].hi));      if ParIntersect [Code] then         begin            maxS(R[P].lo,lo,R[P].lo);            minS(R[P].hi,hi,R[P].hi);         end ;      if gtS(R[P].lo,R[P].hi) then       begin E:=false; assert(CheckLo(R[P].lo));assert(CheckHi(R[P].hi));      end      else begin         if D[Pars[P]] <> R[P] then          begin 	    D[Pars[P]] := R[P]; 	    Change:=true;	    if DF.PF[Pars[P]] = PTrace then TraceChange:=true;         end;         AllPoints:=AllPoints and Point(R[P]);         assert(CheckInt(R[P])); assert(CheckInt(D[Pars[P]]));      end;   end;   if (Debug=activity) and TraceChange then writeln;   if (Debug >=activity) then    begin if Change then write('*') else write ('.');   end;   Exec:=E;   if E then   begin      if AllPoints then Sr:=-1;       if (Sr <> S[PC]) then begin S[PC]:=Sr; Change:=true; end;      if (Debug=activity) and TraceChange then WritePars;      if Debug >= post then  WritePars;      if Debug = dump then DumpMem(DCurr);   end else    if Debug >= activity then    begin writeln('FAILED'); write(' '); WritePars;    end;   PC:=NewPC;end;end;{Exec}begin{OuterExec}   writeln;   writeln(Level:2,'Entering  Count:',OldCounter:0); OldCounter:=0;   Counter:=0;   Fail:=false;   if First <> 0 then DCurr.S[PC]:=First;   {Run simulation until failure or nothing further to be done}   repeat        if (PC = End) then    	begin PC:=1; Change:=false; DCurr.LastHalve:=1; end;   	while (PC < End) and not Fail and not GlobalEnd do   	with I[PC] do   	begin   	   if DCurr.S[PC] > -1 then	   begin Fail:=not Exec(I[PC],PC,LocalChange); 	      Change:=Change or LocalChange;	   end;   	   PC:=PC+1;   	end;   until Fail or (not Change) or GlobalEnd;   writeln;   write(Level:2,'Exiting  Count:',Counter:0);   if not (Fail or GlobalEnd) then   begin       if (Cut=once) then GlobalEnd:=true;      writeln('SOLUTION');      WriteMem(DCurr);   end    else writeln;end;{OuterExec}procedure Clear;var tL:Loc;     tD,tDF:Ptr;     tPar:1..Par;     DI:1..Digits;    J:1..Maxexp;    MaxDiff:real;begin   Shift[0]:=1;   for DI:= 1 to Digits do Shift[DI]:=Shift[DI-1]*10;   with PlusInfS do   begin      edge:=hin;cardinality:=infinite;mantissa:=Maxinf;      exp:=Maxexp;   end;   with MinusInfS do   begin      edge:=lin;cardinality:=infinite;mantissa:=Mininf;      exp:=Maxexp;   end;   with PlusFiniteS do   begin      edge:=hin;cardinality:=finite;mantissa:=Maxman;      exp:=Maxexp;   end;   with MinusFiniteS do   begin      edge:=lin;cardinality:=finite;mantissa:=Minman;      exp:=Maxexp;   end;   with ZeroS do   begin exp:=0;mantissa:=0;edge:=hin;cardinality:=finite;   end;   with PlusSmallS do   begin exp:=Minexp;mantissa:=Maxinf div 10; cardinality:=finite;   end;   with MinusSmallS do   begin exp:=Minexp;mantissa:=Mininf div 10; cardinality:=finite;   end;      with Zero do   begin lo:=ZeroS;lo.edge:=lin; hi:=ZeroS;hi.edge:=hin;   end;   with All do   begin hi:=PlusInfS; lo:=MinusInfS;   end;   with AllFinite do   begin lo:=MinusFiniteS; hi:=PlusFiniteS;   end;   with DF do   begin        for tDF:= 1 to DMem do PF[tDF]:=PNull;   end;     with DInit do   begin	for tD:= 1 to DMem do	   if Verifiable then D[tD]:=AllFinite	   		 else D[tD]:=All;	LastHalve:=1;	MaxDiff:=2;	for J:=1 to Maxexp do MaxDiff:=MaxDiff*10;		for tL := 1 to IMem do	begin	   RHalve[tL]:=MaxDiff;	   S[tL]:=0;	   with I[tL] do	   for tPar := 1 to Par do		Pars[tPar]:=0;	end;{!!}	ParN[print]:=0;        ParN[pr]:=0;        ParN[tr]:=0;        ParN[soln]:=0;	ParN[halve]:=0;	ParN[halves]:=0;	ParN[readr]:=0;	ParN[linh]:=0;	ParN[mult]:=2;	ParN[add]:=2;	ParN[intgr]:= 0;	ParN[less]:= 1;	ParN[leq]:= 1;	ParN[noteq]:= 1;	ParN[sqrr]:= 1;	ParN[minr]:=2;	ParN[maxr]:=2;	ParN[modu]:= 1;	ParN[absr]:= 1;	ParN[trig]:=2;	ParN[expr]:= 1;        ParN[lb]:= 1;        ParN[ub]:= 1;         ParN[copy]:= 1; 	ParN[stop]:=-1;{!!}	ParIntersect[print]:= true;        ParIntersect[pr]:= true;        ParIntersect[tr]:= true;        ParIntersect[soln]:= true;	ParIntersect[halve]:=true;	ParIntersect[halves]:=true;	ParIntersect[readr]:=true;	ParIntersect[linh]:=true;	ParIntersect[mult]:=true;	ParIntersect[add]:=true;	ParIntersect[intgr]:= true;	ParIntersect[less]:= true;	ParIntersect[leq]:= true;	ParIntersect[noteq]:= true;	ParIntersect[sqrr]:= true;	ParIntersect[minr]:= true;	ParIntersect[maxr]:= true;	ParIntersect[modu]:= true;	ParIntersect[absr]:= true;	ParIntersect[trig]:= true;	ParIntersect[expr]:= true;        ParIntersect[lb]:= false;        ParIntersect[ub]:= false;	ParIntersect[stop]:= true;	ParIntersect[copy]:= true;   end;end;{Clear}	procedure ReadInstr;var	tP:0..Par;	Op:OpType;	tDat:Ptr;begin   with DInit do   begin	End:=1;	MaxDMem:=0;	repeat	   with I[End] do	   begin	      read(Op);	      Code:=Op;	      for tP := 0 to ParN[Op] do with I[End] do 	      begin	         read(tDat); Pars[tP]:=tDat;		 if tDat>MaxDMem then MaxDMem:=tDat;		 if MaxDMem > DMem then 		 begin writeln('Too many variables');halt;		 end;	      end;	      readln;	   end;	   End:=End+1; 	   if End >= IMem then begin writeln('Too many instructions');halt;end;	until Op = stop;	End:=End-1;	while not eof do {read constant values for memory locations}	begin   	   read(tDat);	   if tDat > DMem then writeln('Variable out of range',tDat,DMem);	   ReadInt(D[tDat]);	   readln;	end;   end;end;{ReadInstr}begin	GlobalEnd:=false;	InitialOptions;	readln(Cut);	writeln(Cut);	Clear;	{ set to initial values, read instructions}	ReadInstr;	if Debug = dump then begin DumpTables; DumpMem(DInit); end;	if Debug >= activity then WriteMem(DInit);	Dummy:=0;	OuterExec(1,DInit,false,0,Dummy,0);	if Debug = dump then DumpMem(DInit);end.