%main method of this module
%uses generate and writes the variable assignment into the userdict with keys="0","1","2",...
/generator_assignvars {
	generator_generate
	0 {
		%duplicate counter
		dup 1 add
		%write to userdict
	  	userdict
		exch
		3 index
		0 eq { false } { true } ifelse	
		put
		%increment counter
		1 add
		%delete processed element
		exch pop
		%exit if enough
		dup generator_getvarcount eq { pop exit } if
	} loop
} def


/generator_reset {
	userdict (step) 0 put
} def


%creates a new variable assignment needs a value in userdict (count vars)
/generator_generate {
	userdict (step) known true ne { userdict (step) 0 put } if
	%get current step
	userdict (step) get	
	%get binary on stack	
	dup 0 ne { generator_tobin } if
	%compute count of zeros
	generator_getvarcount exch sub
	%add zeros	
	generator_zeros
	%increase step by one
	generator_increasestep
} def


%sets the count of variables used
/generator_setvarcount {
	userdict exch (count vars) exch put
} def

%returns the count of variables used by the SAT instance
/generator_getvarcount {
 	userdict (count vars) get
} def

%used by the generator to remember its current state
/generator_increasestep {
	userdict (step) get 1 add userdict exch (step) exch put
} def


%input step , output binary on stack and count of elements pushed to the stack
/generator_tobin {		 
 	dup
	2 mod
	exch
	2 idiv
	dup 0 ne { generator_tobin 1 add } { pop 1 } ifelse 
} def


%in: count zeros, out: count x 0 on stack
/generator_zeros {
	dup 0 eq { pop } { 0 exch 1 sub generator_zeros } ifelse 
} def