/test { (input.sat) readlines } def

/testinv { (input_invalid.sat) readlines } def


/readfile { (r) file } def

/readlines { readfile { 
			dup str readline 
				{ 
					dup length 0 eq { pop } {
						iscomment { 	dup = 
								userdict (comments) get 
								exch concat (\n) concat 
								userdict exch (comments) exch put 
						} {
							parseline exch 	
						}ifelse
				} ifelse	
			}
			{ exch exit } ifelse
		} loop 
		closefile

		store % stores each line into a dictionary
		validate % validate clauses
		
	} def


/iscomment { dup 0 get 99 eq } def

/parseline {
	%data

	} def

/str { 256 string } def


%save lines in userdict
% input of form on stack = 
% 	(p cnf 5 3)
% 	(1 -5 4 0)
% claus1 -> clauseN,... clausN -> clause1, 
% result userdict is filled,
/store 	{
		% check length last element >0
		dup length 0 eq { pop } if 
		{	% count stack elements	
			count 1 sub
			% if 0 on stack, exit loop
			dup 0 eq { pop exit } if
			% remove tailing 0
			% convert and concat with (clause)
			tmpstring cvs (clause) exch concat
			% change position of last 3 items and push on userdict
			userdict 3 1 roll exch 
			removeZero put 
		} loop
		% put last line also onto the stack
		(p) exch userdict 3 1 roll put
	} def


%validate vars
% input: empty stack
% result: 
%	quit if error 
%	or 
%	continue
% 
/validate { 
	userdict (p) get % get p line from userdict
	% cvx exec % put last line on the stack
	(p cnf) anchorsearch % returns string after (p cnf)
	pop pop % remove unneded elements
	cvx exec % put elements on thack
	(count clause) userdict 3 1 roll exch put
	(count vars) userdict 3 1 roll exch put
	countclauses
	validatevars
}  def

% validates if given amount of claueses exists
% input: empty stack, userdict filled
% return: empty stack
/countclauses {
	userdict (count clause) get % retrieve clause amount from userdict
	dup 0 eq { (no clause count var was given \n exiting....) = quit } if
	userdict (vars) () put
	{
		dup 0 eq { pop (clauses are valid) = exit } if % check if number is greater than 0
		dup tmpstring cvs (clause) exch concat % to string and concat for userdict key = clauseX
		dup
		userdict exch known % check if known
		{ 
			 % store each var for varvalidation
			userdict exch get % get vars
			userdict (vars) get % get already stored vars
			concat userdict exch (vars) exch put % concat and store
			1 sub % decrease counter
		}
		{ 
			(error: invalid amount of clauses \n exiting....) = quit
		}
		ifelse
	} loop
} def


% validates for var amount
% input: empty stack, userdict filled
% return: empty stack
/validatevars {
	userdict (counts) 0 put % initial with 0
	userdict (vars) get % get max vars
	mark exch cvx exec % marker push
	{	
		dup mark eq { exit } if
		abs dup userdict exch known not % check userdict if var exist
		{ 
			userdict exch dup put % if not known push in userdict
			userdict (counts) get 1 add userdict exch (counts) exch put % increase counter
		} 
		{	
			pop % remove unneded one, cause already exists
		} ifelse
	} loop
	pop % remove stop
	userdict (counts) get
	userdict (count vars) get le  % (counts) <= (count vars)
	{ 
		(var count is valid) = 
	} 
	{ 
		(error: var count is invalid. \n exiting...) = quit 
	} ifelse
} def














%%%%%%%%%%%%%%%%%%%%%%%%%%% helpers

/concat % (string1) (string2) concatenate string3
% array1 array2 concatenate array3
{ %def
dup type 2 index type 2 copy ne { %if
pop pop
errordict begin (concatenate) typecheck end
}{ %else
/stringtype ne exch /arraytype ne and {
errordict begin (concatenate) typecheck end
} if
} ifelse
dup length 2 index length add 1 index type
/arraytype eq { array }{ string } ifelse
% stack: arg1 arg2 new
dup 0 4 index putinterval
% stack: arg1 arg2 new
dup 4 -1 roll length 4 -1 roll putinterval
% stack: new
} bind def

% helper
/tmpstring 20 string def



/rightTrim
{ dup
  length 1 sub -1 0
  { /i exch def dup i get 32 ne {exit} if
  } for
  0 i 1 add getinterval
  dup length string copy
} bind def


/removeZero
{ dup
  length 1 sub -1 0
  { /i exch def 
	dup i get 48 ne {exit} if
  } for
  0 i 1 add getinterval
  dup length string copy
} bind def