%filename import - use to add source code
/import {
	(r) file cvx exec
} def

%IMPORTS:
(psss_generator) import
(psss_input_reader) import
(psss_output_writer) import

%CONFIG:
userdict (print valid assignments) true put
userdict (make output file) true put
userdict (exit after found) false put
userdict (output file) (output.sat) put
userdict (satisfiable) false put
userdict (multiple output to file) false put
userdict (automatic cleanup) false put
userdict (comments) () put

%START:
(Enter (FILENAME) and call "doit":) =

%MAIN METHOD:
/doit {
	readlines
	makeEvalMethod
	solve
	output_writer_finishfile
	
	userdict (satisfiable) get true eq 
	{(SAT instance is satisfiable!)=}
	{(SAT instance is NOT satisfiable!)=} ifelse

	userdict (automatic cleanup) get true eq
	{ (Performing cleanup...) = cleanup } if	

	(DONE) =
} def


/cleanup{
	clear
	userdict (eval method) undef
	userdict (count vars) undef
	userdict (count clause) undef
	userdict (counts) undef
	userdict (comments) () put
	0 1 10 
	{ 
		dup userdict exch undef 
		userdict exch (clause) exch 2 string cvs concat undef
	} for
	generator_reset
	output_writer_cleanup
} def


/solve {	
	0	%counter
	{
		() = %empty line
		%print current program step
		dup 1 add (Doing iteration: ) exch 10 string cvs concat =

		%change variable assignment		
		generator_assignvars

		%evaluate
		userdict (eval method) get cvx exec

		%if satisfiable
		dup true eq {
			(Found a valid assignment!) =
			userdict (print valid assignments) get true eq { printAssignment } if
			userdict (make output file) get true eq { output_writer_writetofile } if
			userdict (exit after found) get true eq { exch pop exit } if
			userdict (satisfiable) true put
		} if	
	
		%increment counter
		exch 1 add	

		%exit if done all assignments
		dup 2 generator_getvarcount exp eq { pop exit } if
	} loop
} def


%in userdict:
%count clause: 3
%clause1: (1 2 -3 4)
%clause2: (2 3 -5)
%clause3: (1 2 3)
%1: true
%2: true
%.....
%method should be afterwards: 
%{ userdict 1 get userdict 2 get userdict 3 get neg userdict 4 get or or or 
%userdict 2 get userdict 3 get userdict 5 get or or
%userdict 1 get userdict 2 get userdict 3 get or or
%and and }
/makeEvalMethod{
	1 {	%STACK 1
		%push stop indicator
		dup mark exch	%STACK 1 (stop) 1
		%create key
		(clause) exch 10 string cvs concat	%STACK 1 (stop) (clause1)
		%get clause		
		userdict exch get %STACK 1 (stop) (1 2 -3 4)
		cvx exec	%STACK 1 (stop) 1 2 -3 4
		1 {		%STACK 1 (stop) 1 2 -3 4 1
			exch	%STACK 1 (stop) 1 2 -3 1 4
			( userdict ) appendStringToMethod	%STACK 1 (stop) 1 2 -3 1 4
			dup abs appendIntToMethod	%STACK 1 (stop) 1 2 -3 1
			( get ) appendStringToMethod	%STACK 1 (stop) 1 2 -3 1
			0 lt { ( not ) appendStringToMethod } if	%STACK 1 (stop) 1 2 -3 1
			exch dup mark eq { pop exit } if	
			exch 1 add 
		}loop 
		
		dup 1 eq {
			%only one variable
			pop
		} {
			1 sub {	%add or's
				( or ) appendStringToMethod
				1 sub
				dup 0 eq { pop exit } if			
			} loop
		} ifelse	

		
		
		dup userdict (count clause) get eq { exit } if
		1 add	
	}loop

	1 sub {	%append and's
		( and ) appendStringToMethod
		1 sub
		dup 0 eq { pop exit } if	
	} loop
} def



/appendIntToMethod{
	10 string cvs %convert to string
	appendStringToMethod
} def

/appendStringToMethod{
	userdict (eval method) known false eq { userdict (eval method) () put } if
	userdict (eval method) get exch concat
	userdict exch (eval method) exch put
} def 



/printAssignment {	
	1 {		
		dup dup userdict exch get 10 string cvs			% 1 1 (false)
		(=) exch concat						% 1 1 (=false)
		exch 10 string cvs					% 1 (=false) (1)
		exch							% 1 (1) (=false)
		concat							% 1 (1=false)
		=							% 1 

		%exit if done all assignments
		dup generator_getvarcount eq { pop exit } if	

		%increment counter
		1 add							% 2  
	} loop
} def