# The main routine.

### args[1]:boolean,args[2]:equations, args[3]:constriants, args[4]:fvar, agrs[5]:order
### args[1] to indicate whether the constraints contains the variables donnot in fvar and order
##If ics can not work, args[6] is the triangular sets
GMain := proc()
	global _file_path;
        local cons,res;

	if nargs<6 then 
		ERROR(`Too few argument.`);
        elif nargs=6 then 
		if not type(args[1],boolean) or not type(args[2],{set,list}) or not type(args[3],{set,list}) or not type(args[4],{set,list}) or not type(args[5],{set,list}) or not type(args[6],{set,list})then 
			ERROR(`Wrong arguments.`);
                else
 			res := `cons/getResult`(args);
		fi;
       	else
		ERROR(`Too many argument`);
        fi;

	return res;
end:

###ind is boolean argument to indicate whether contains other variables in constraints, if so,
###eliminate them first, and put all the results in constraints set. eqs::equations, cons::
###constaints, fvar::free variables, ord::dependent variables with order
##If ics can not work, triangle is the triangular sets, or is []
`cons/getResult` := proc(ind::boolean,eqs,cons,fvar,ord,triangle)
	global _file_path;
	local eset,cset,Cs,T,inis,i,j,res,tran,tres,Fs1,Fs2,Fs3,Fs4,steiner,fres,Ts,tt,cc;
	
	eset := simplify(eqs); cset := simplify(cons);
	eset:={op(eset)} minus {0};

	if nops(triangle)<>0 then 
        	T:=triangle;
        else 
		#steiner can not use ics, bug
		steiner:=[2*x1-1,x2^2+x1^2-1,x4^2+x3^2-u2^2-u1^2,2*u2*x4+2*u1*x3-u2^2-u1^2,x6^2+x5^2-2*x5-u2^2-u1^2+2*u1,2*u2*x6+2*u1*x5-2*x5-u1^2-u2^2+1];
		Fs1:=[2*x1-1, 4*x2^2-3, -2*x3+u1-2*u2*x2, -2*u2*x4-2*u1*x3+u2^2+u1^2, -2*x5+u1+1-2*u2*x2, -2*u2*x6-2*u1*x5+2*x5+u1^2+u2^2-1];
		Fs2:=[2*x1-1, 4*x2^2-3, -2*x3+u1-2*u2*x2, -2*u2*x4-2*u1*x3+u2^2+u1^2, -2*x5+u1+1+2*u2*x2, -2*u2*x6-2*u1*x5+2*x5+u1^2+u2^2-1];
		Fs3:=[2*x1-1, 4*x2^2-3, -2*x3+u1+2*u2*x2, -2*u2*x4-2*u1*x3+u2^2+u1^2, -2*x5+u1+1-2*u2*x2, -2*u2*x6-2*u1*x5+2*x5+u1^2+u2^2-1];
		Fs4:=[2*x1-1, 4*x2^2-3, -2*x3+u1+2*u2*x2, -2*u2*x4-2*u1*x3+u2^2+u1^2, -2*x5+u1+1+2*u2*x2, -2*u2*x6-2*u1*x5+2*x5+u1^2+u2^2-1];

		if nops({op(steiner)} intersect {op(eset)})=6 then 
			T:=[Fs1,Fs2,Fs3,Fs4];
		else   
	   		T := [epsilon[ICS](eset,ord)];
		fi;
        fi;

	Ts:=[];
	for i from 1 to nops(T) do
		tt:=T[i];
		Ts:=[op(Ts),['primpart(tt[j],ord[j])'$'j'=1..nops(tt)]];

	od;

        # add initials <>0 of all equalities into the constraints
    	for i from 1 to nops(Ts) do 
       		inis[i] := [seq(lcoeff(Ts[i][j],ord[j]),j=1..nops(eset))];
    	od;
  
    	for i from 1 to nops(Ts) do
       		Cs[i] := cset;
      		for j from 1 to nops(eset) do
         		 Cs[i] := [op(Cs[i]), inis[i][j] <> 0];
      		 od;
    	od;
    
   	tran := [];
   	for i from 1 to nops(Ts) do
       		tran := [op(tran),[Ts[i],Cs[i]]];
    	od;

 	res := [];
        for i from 1 to nops(Ts) do
                tran[i][2] := `cons/paraRem`(ind,tran[i][2],fvar,ord);
                if op(2,op(i,tran))=false then 
			tres:=[[]];
		else
			tres := `cons/npRoot`(op(1,op(i,tran)),op(2,op(i,tran)),fvar,ord); 
		fi;
		res := [op(res),op(tres)];
        od; 

	#remove all the emptyness [] in the results and change constraints to java mode
	fres:=[];
        for i from 1 to nops(res) do 
        	if nops(res[i])<>0 then
               		fres:=[op(fres),op(i,res)];
                fi;
	od;
	
	for i from 1 to nops(fres) do 
      		if nops(fres[i])<>0 then
			cc:=[];
                        for j from 1 to nops(fres[i]) do 
				if nops(fres[i][j])<>0 then 
					cc:=[op(cc),op(j,fres[i])];
				fi;
			od;
			fres[i]:=cc;
        		fres[i][1]:=`cons/convert`(fres[i][1]);
			fres[i]:=[op(fres[i][1]),op(fres[i][2])];
                fi;
        od;

		
                
        writeto(cat(_file_path,"/results"));
    		printf(`%q`,op(fres));
        writeto(terminal); 
        
        return fres;
 end:

####description of arguments, cons::constraints set;
####fvar::free variables; ord::dependent variables; ind::indicating to remove 
####equations or not.
`cons/paraRem`:=proc(ind::boolean,cons,fvar,ord)
	local cset,i,var,evar;
	var := [op(fvar),op(ord)];

	evar := [op(indets([op(cons)]) minus {op(var)})];
	evar:=sort(evar);

	if nops(evar)=0 then 
		cset:=cons

	else
		cset:=`cons/splitEli`(ind,cons,var,evar);
	fi;

	return cset;
end:

#This routine is to compute a formula and output the results to a specified file,
#then retrieve the results and store them in a string.
`cons/fromCAD`:=proc()
	local t,line,file,memo;
	global _file_path;
	
	if nargs=1 then
		memo:=args[1]	
	else
		memo:=99999999;
	fi;


	t:=cat(`cat `,_file_path,`/.tqepcad`,`|qepcad +N`,memo, `>`,_file_path,`/.fqepcad`);
	system(t); 
	
	file:=cat(_file_path,`/.fqepcad`);
	fclose(file);
	line:=readline(file):
	while line<>"An equivalent quantifier-free formula:" do
		#if line= then 
		#	break;
		#elif line="Reason for the failure: Too few cells reclaimed." then
		#	if memo<> 99999999 then
		#		line:=`cons/fromCAD`();
		#		break;		
		#	else
		#		ERROR(`Fail:not enough memery.`);
		#	fi;
		#elif line="dfsafd" then
		#	ERROR(`Fail:not enough prime.`);
		#fi;
			
		line:=readline(file):
	od:
	line:=readline(file):
	line:=readline(file):

	#`epsilon/print`(line);
	if line=0 then
		ERROR(`FAIL:`);	
	elif line="FALSE" then
		return false
	elif line="TRUE" then
		return true
	else
		return line
	fi;
end:

#This routine is to formalize specified constraints into a form 
#that can be executed by QEPCAD. The arguments of this routine 
#should contain specified constraints, variable list and number of
#free variables
#And there may be an optimal fifth argument that holds the quantifier
#to be used in
`cons/CAD`:=proc(des,vars,fnum,cons,qua)
	local s,i,pl,var,evar,fn,res;
	global _file_path;
 	
	if nargs<4 then 
		ERROR(`too few arguments.`)
 	elif nargs=4 or nargs=5 then
		if not type(cons,{set,list}) or not type(vars,list) or
				not type(fnum,integer) then
			ERROR(`unexpected arguments.`);
		else
			pl := printlevel;
  			printlevel := 1;
 			writeto(cat(_file_path,"/.tqepcad"));

			#form description
			printf(cat(`[`,des,`]`));
                        printf(`\n`);
			#`epsilon/print`(des);
			#`epsilon/print`(`]`);

			#form variable list
			#`epsilon/print`(`(`);
			var:=[];
			#remove redundant variables
			for i in vars do
				if not member(i,var) then
					var:=[op(var),i]
				fi
			od:
			#print(op(var));
			#`epsilon/print`(`)`);
 			printf(`(%q)`,op(var));
			printf(`\n`);
			
			#form free number
			if fnum<=0 then
				fn:=0
			elif fnum>nops(var) then
				fn:=nops(var)
			else
				fn:=fnum
			fi;
			printf(`%d`,fn);
			printf(`\n`);
			
			#form prenex formula
			#an optimal agument may be added to indicate that which quantifier to be used
			#in the construction of quantifier formula
			#Here only a simple case is handled.

			evar:=[];
			for i from fnum+1 to nops(var) do
				evar:=[op(evar),op(i,vars)]
			od:
			#The fifth argument is optimal. 
			#If it exists,then it contains quantifier to be used, else default quantifier E
			#will be used.
			if nargs=5 then 
				if not type(qua,list) then
					ERROR(`quantifier list expected.`)
				else
					for i from 1 to nops(evar) do
						if i<=nops(qua) then
							if op(i,qua) in [E,A,F,G,C,xk] then
								printf(`(%a %a)`,op(i,qua),op(i,evar))
							else
								printf(`(E %a)`,op(i,evar))
							fi;
						else
							printf(`(E %a)`,op(i,evar))
						fi;
					od;
				fi;
			else
				for i from 1 to nops(evar) do
					printf(`(E %a)`,op(i,evar));
				od;
			fi;
			printf(`[`);
			for i from 1 to nops(cons) do
				if type(op(i,cons),polynom) then
					s:=StringTools[SubstituteAll](convert(op(i,cons)=0,string),"*"," ")
				elif type(op(i,cons),`<>`) then
					s:=StringTools[SubstituteAll](convert(op(i,cons),string),"*"," ");
					s:=StringTools[SubstituteAll](s,"<>","/=")
				elif type(op(i,cons),`=`) then
					s:=StringTools[SubstituteAll](convert(op(i,cons),string),"*"," ")
				elif type(op(i,cons),{`<`,`<=`}) then
					s:=StringTools[SubstituteAll](convert(op(i,cons),string),"*"," ")
				elif type(op(i,cons),string) then 
					s:=StringTools[SubstituteAll](convert(op(i,cons),string),"*"," ");
					s:=cat(`[`,s,`]`)
				fi;	
				printf(s);
				if i<>nops(cons) then
					printf(` /\\ `)
				fi;
					
			od;
			printf(`].`);
			printf(`\n`);
			
			#form to complete
			#actually, some flag can be added here to automatically interact with
			#QEPCAD
			printf("finish");
			printf(`\n`);

			writeto(terminal);
   			printlevel := pl:
			
			
		fi;
		res:= `cons/fromCAD`(88880000);
		return res;
	else
		ERROR(`too many arguments.`)		 
	fi;
	printf(`\n`);
end:

#This routine is to eliminate somve variables from the formula.
#It contains 3 main arguments,that is formula(typed with set or
#list),variables(list) and variable to be eliminated(typed with
#list or an integer representing the number of eliminated variables).
#An optimal(the fourth) argument typed with list that indicates which
#quantifier will be used corresponding to an eliminated variable.
`cons/eliminate`:=proc(cons,vars,varEli,qua)
	local i,var,fvar,evar,fnum,res;
 	
	if nargs<3 then 
		ERROR(`too few arguments.`)
 	elif nargs=3 or nargs=4 then
		if not type(cons,{set,list}) or not type(vars,list) or
				not type(varEli,{list,integer}) then
			ERROR(`unexpected arguments.`);
		else
			#form variable list
			var:=[];
			#remove redundant variables
			for i in vars do
				if not member(i,var) then
					var:=[op(var),i]
				fi
			od:

			evar:=[];		
			if type(varEli,list) then
				for i in varEli do
					if not member(i,evar) then
						evar:=[op(evar),i]
					fi
				od:
				fvar:=[];
				for i in var do
					if not member(i,evar) then
						fvar:=[op(fvar),i]
					fi
				od:
				fnum:=nops(fvar);
				var:=[op(fvar),op(evar)];
			else
				fnum:=nops(var)-varEli;
				if fnum<0 then
	####				fnum:=0
				fi;		
			fi;		
		fi;
		if nargs=4 then
			res:= `cons/CAD`("",var,fnum,cons,qua)
		else
			res:= `cons/CAD`("",var,fnum,cons)
		fi;
		#return `cons/split`(res);
		return res;
	else
		ERROR(`too many arguments.`)		 
	fi;
	`epsilon/print`();	
end:


#This routine is to eliminate some variables from the specified formula.
#Since there are many cases that variables can not be eliminated simulataneous,
#to handle these cases we build such routine to eliminated ONE variable once.
#The first argument typed with boolean indicating whether to or not to remove 
#equations in the eliminated constraints set 
`cons/splitEli`:=proc(ind::boolean,cons,vars,varEli,qua)
	local i,ic,var,fvar,evar,fnum,res,cset,eset,qlis;
 	
	#var:all variables,fvar:free variables,evar:eliminated variables,fnum:number of free variables
	#res:results,eset:temp set of constraints to be computed,cset:=cons minus eset,qlis:quantifiers
	#list

	if nargs<4 then 
		ERROR(`too few arguments.`)
 	elif nargs=4 or nargs=5 then
		if not type(cons,{set,list}) or not type(vars,list) or
				not type(varEli,{list,integer}) then
			ERROR(`unexpected arguments.`);
		else
			var:=[];
			#remove redundant variables
			for i in vars do
				if not member(i,var) then
					var:=[op(var),i]
				fi
			od:
			#compute the free variable list and eliminated variable list
			fvar:=[];
			evar:=[];		
			if type(varEli,list) then
				for i in varEli do
					if not member(i,evar) then
						evar:=[op(evar),i]
					fi
				od:
				for i in var do
					if not member(i,evar) then
						fvar:=[op(fvar),i]
					fi
				od:
				fnum:=nops(fvar);			
			else
				fnum:=nops(var)-varEli;
				if fnum<0 then
					fnum:=0
				fi;	
				fvar:=['op(i,var)'$'i'=1..fnum];
			 	evar:=['op(i,var)'$'i'=fnum+1..nops(var)];
			fi;		
		fi;
		#initial some value
		var:=fvar;
		cset:={op(cons)};
		eset:={};
		qlis:=[];
		if nargs=5 and type(qua,list) then
			for i from 1 to nops(evar) do
				if i<=nops(qua) then
					if op(i,qua) in [E,A,F,G,xk,C] then
						qlis:=[op(qlis),i]
					else
						qlis:=[op(qlis),E]
					fi
				else
					qlis:=[op(qlis),E]
				fi
			od;
		else
			qlis:=['E'$'i'=1..nops(evar)]
		fi;
		print(evar);
		#construct eliminated constraints set for current variable
		for i from nops(evar) to 1 by -1 do

			#check whether a statement contains a specified eliminated variable or not.
			#if so,then add this statement into eset
			for ic in cset do
				if `cons/contain`(ic,op(i,evar)) then
					eset:={op(eset),ic}
				fi;
			od;

			if eset={} then
				break;
			else
				res:=`cons/eliminate`(eset,var,[op(i,evar)],[op(i,qlis)]);
				#verify the result is or not boolean constant false
				if type(res,boolean) then
					if not res then
						return false
					else
						cset:=cset minus eset;
					fi					
				else
					cset:=cset minus eset;
					cset:={res,op(cset)}
				fi;					
			fi;
			#update eset
			eset:={};
		od:
		#the emptyness of cset means that in each step boolean true is returned.
		if nops(cset)=0 then
			return true;
		elif nops(cset)=1 then
			return cset;
		else
			return `cons/simplify`(cset,var,ind);
		fi;
	else
		ERROR(`too many arguments.`)		 
	fi;
	`epsilon/print`();
end:

#This routine is to analyze an input argument to verify it does or not contain 
#a specified variable.
#The argument may be an algebraic expression or a string which is obtained from 
#the output of QEPCAD.So in some cases,this routine may fail.
`cons/contain`:=proc(exp,var)
	local lis,res;

	if nargs<>2 then
		ERROR(`wrong argument.`)
	else
		if type(exp,{polynom,`=`,`<>`,`<`,`<=`}) then
			lis:=indets(exp);
			if member(convert(var,symbol),lis) then
				res:=true
			else
				res:= false
			fi;
		elif type(exp,string) then
			lis:=StringTools[Words](exp);
			if member(convert(var,string),lis) then
				res:= true
			else
				res:= false
			fi;
		else
			ERROR(`wrong arguments.`)
		fi
	fi;
	return res;
end:

##This routine is to analyze an input argument to verify it does or not contain 
#even one variable in vars.
`cons/noVarContain`:=proc(exp,vars)
	local lis,res,var;

	if nargs<>2 then
		ERROR(`wrong argument.`)
	else
		res:=true;
		if type(exp,{polynom,`=`,`<>`,`<`,`<=`}) then
			lis:=indets(exp);
                        for var in vars do
                           	if member(convert(var,symbol),lis) then
					res:=false;
			                break;
			        fi;
		        od;
		elif type(exp,string) then
			lis:=StringTools[Words](exp);
                        for var in vars do
				if member(convert(var,string),lis) then
					res:= false;
					break;
				fi;
			od;
		else
			ERROR(`wrong arguments.`)
		fi;
	fi;
	return res;
end:

#This routine is to simplify a set or list of constraints with QEPCAD.
#The first and second arguments contains the constraints and involved 
#variables, the third typed with boolean indicating whether or not to
#remove redundant equations constraints.
#To be completed.
`cons/simplify`:=proc(cons,vars,ind::boolean)
	
	local cset,eset,var,i,res;
	
	cset:=cons;
	var:=vars;
	#`cons/sort`() ensures each time the two least length are computed.
	cset:=`cons/sort`(cset);
	#print(cset);
	if nops(cset)=0 then
		return true
	elif nops(cset)=1 then
		return cset
	else
	#simplify elements in cset
		
		for i from 1 to nops(cset)-1 do
			eset:=[op(1,cset),op(2,cset)];
			res:=`cons/eliminate`(eset,var,0);
			#verify the result is or not boolean constant false
			if type(res,boolean) then
				if not res then
					return false
				fi					
			else
				cset:={op(cset)} minus {op(eset)};
				cset:=`cons/sort`({op(cset),res})
			fi;
			eset:={};
		od;
		#test whether equations are removed.
		if ind then 
			cset:=`cons/removeEqs`(cset)
		fi;
		if nops(cset)=0 then
			return true
		else
			return cset
		fi;
	fi;
end:

#This routine is to sort a set or list by the length of elements
`cons/sort`:=proc(cs::{set,list})
	local i,j,lis,tem;
	lis:=[op(cs)];
	for i from 1 to nops(lis)-1 do
		for j from i+1 to nops(lis) do
			if length(op(i,lis))>length(op(j,lis)) then
				tem:=op(i,lis);
				lis[i]:=op(j,lis);
				lis[j]:=tem
			fi
		od:
	od:
	return lis;					
end:

#This routine is to remove equations from constraints list 
`cons/removeEqs`:=proc(cset::{list,set})
	local ic,cs,spl,s,t,com,i;
	cs:={};
	com:=[];
	for ic in cset do
		if type(ic,{polynom,equation})then
			#nothing to do
		elif type(ic,{`<`,`<=`,`<>`}) then
			cs:={op(cs),ic}
		elif type(ic,string) then
			spl:=`cons/split`(ic);
			for s in spl do
				if StringTools[Search]("=",s)=0 or StringTools[Search]("\\/",s)<> 0 then 
					#com:=[op(com),s]
					cs:={op(cs),s}	
				fi;	
			od;
			#combine the split string, necessary?? I think no.
			#t:="";
			#for i from 1 to nops(com) do
			#	if i<>nops(com) then
			#		t:=cat(t,op(i,com)," /\\ ")	
			#	else
			#		t:=cat(t,op(i,com))
			#	fi;
			#od:
			#com:=[];
			#cs:={op(cs),t};
		else
			ERROR(`wrong arguments.`)
		fi;
	od;
	return cs;
end:

#This routine is to split a string which contain formulae into 
#a list of smaller formulae, the union of the list is equavalent 
#to the original string.
`cons/split`:=proc(str::string)
	local sub,res,s,lis,i,ic;
	s:="";
	res:=[];
	sub:=StringTools[SubstituteAll](str,"/\\","&");
	lis:=StringTools[Split](sub,"&");
	if nops(lis)=1 then
		return lis
	else
		for i from 1 to nops(lis) do
			s:=cat(s,op(i,lis));
			if `cons/match`(s) then 
				res:=[op(res),s];
				s:=""
			else
				s:=cat(s,"/\\")	
			fi;	
		od:
	fi;
	return res;
end:

#This routine is to test bracket matching(square brackets only)
`cons/match`:=proc(str::string)
	local lis,i,s;
	lis:=[];
	for i from 1 to length(str) do
		s:=substring(str,i..i);
	if s="[" then
		lis:=[op(lis),s]
	elif s="]" then
		if op(nops(lis),lis)="[" then
			lis:=['op(j,lis)'$'j'=1..nops(lis)-1]
		else
			return false;
		fi;
	fi;
	od:
	if nops(lis)=0 then
		return true;
	else
		return false;
	fi;
end:

`cons/polyCheck`:=proc(p)
	local tn;
	if type(p,`+`) then
		tn:=nops(p);
	else
		tn:=1;
	fi;
	if degree(p,indets(p))<=20 and tn<50 then
		return true;
	else
		return false;
	fi;
end:

##the main function to eliminate all the variables from the constraints
##the arguments are equations, constraints, free varialbes and dependent variables with order
`cons/npRoot`:=proc(cs,cons,fvar,ord)
	local res,var,i,j,k,d,ic,cset,eset,val,res1,res2,tres,eqs,flag,tflag,qa,qb,qc,qd,qe,
		CS,pp1,pp2,pp3,pp4,ss,cc1,cc2,tt,DD1,DD2,DD3;
	res:=[[{op(cons)},cs,[]]];
	eset:={};
	var:=[op(fvar),op(ord)];
	val:=[];
	eqs:=[op(cs)];

	
	if nargs<4 then
		ERROR(`too few arguments.`)
	elif not type(cs,list) then 
		ERROR(cat(`wrong arguments:`,`cs `,`should be a list.`))
	elif not type(cons,{set,list}) then
		ERROR(cat(`wrong arguments:`,`cons `,`should be set or list.`))
	elif not type(fvar,list) then
		ERROR(cat(`wrong arguments:`,`fvar `,`should be a list.`))
	elif not type(ord,list) then 
		ERROR(cat(`wrong arguments:`,`ord `,`should be a list.`))
	else
		for i from nops(eqs) to 1 by -1 do
			flag:=0;
			tres:=[];
			eset:={op(i,eqs)};
			var:=['op(k,var)'$'k'=1..nops(var)-1];
			d:= degree(op(i,eqs),op(i,ord));

			if `cons/polyCheck`(cs[i]) then 
				CS:=['op(k,eqs)'$'k'=1..i-1];

				if d=1 then		
					val:=simplify(-coeff(eqs[i],ord[i],0)/coeff(eqs[i],ord[i],1));

					for j from 1 to nops(res) do
						cset:=op(1,op(j,res));
						eset:={op(i,eqs)};
			
						for ic in cset do
							if `cons/contain`(ic,op(i,ord)) then
								eset:={op(eset),ic};
							fi;
							if `cons/noVarContain`(ic,ord) then
								eset:={op(eset),ic};
							fi;
						od;
							
						res1:=`cons/eliminate`(eset,var,[op(i,ord)]);
						#contradiction occured:go to contradication handler
						if res1=false then
						#current conditions are always satisfied
						elif res1=true then
							cset:={op(cset minus eset)};
							tres:=[op(tres),[cset,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						else	
							res2:={op(cset minus eset),res1};
							tres:=[op(tres),[res2,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						fi;
						print(res1);
					od;

				elif d=2 then
					qa := coeff(cs[i],ord[i],2);
                			qb := coeff(cs[i],ord[i],1);
                			qc := coeff(cs[i],ord[i],0);
                
					for j from 1 to nops(res) do
						
						cset:=op(1,op(j,res));
						eset:={op(i,eqs)};
						for ic in cset do
							if `cons/contain`(ic,op(i,ord)) then
								eset:={op(eset),ic}
							fi;
							if `cons/noVarContain`(ic,ord) then
								eset:={op(eset),ic};
							fi;
						od;	
						
						#^2Case 1
						res1:=`cons/eliminate`({op(eset),2*qa*op(i,ord)+qb>=0},var,[op(i,ord)]);
						#contradiction occured:go to contradication handler
						if res1=false then
						#current conditions are always satisfied
						elif res1=true then
							val=-qb/2/qa+sqrt(qb^2-4*qa*qc)/2/qa;
							cset:={op(cset minus eset)};
							tres:=[op(tres),[cset,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						else
							val:=-qb/2/qa+sqrt(qb^2-4*qa*qc)/2/qa;	
							res2:={op(cset minus eset),res1};
							tres:=[op(tres),[res2,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						fi;						
						print(res1);
						#^2Case 2
						res1:=`cons/eliminate`({op(eset),2*qa*op(i,ord)+qb<=0},var,[op(i,ord)]);
						#contradiction occured:go to contradication handler
						if res1=false then
						#current conditions are always satisfied
						elif res1=true then
							val:=-qb/2/qa-sqrt(qb^2-4*qa*qc)/2/qa;
							cset:={op(cset minus eset)};
							tres:=[op(tres),[cset,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						else	
							val:=-qb/2/qa-sqrt(qb^2-4*qa*qc)/2/qa;
							res2:={op(cset minus eset),res1};
							tres:=[op(tres),[res2,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						fi;
                                                print(res1);
					od;
				elif d=3 then
					qa := coeff(cs[i],ord[i],3);
                			qb := coeff(cs[i],ord[i],2);
                			qc := coeff(cs[i],ord[i],1);
					qd := coeff(cs[i],ord[i],0);
			
					pp1:=simplify(-4*qc^3*qa+qc^2*qb^2+18*qc*qb*qa*qd-27*qd^2*qa^2-4*qd*qb^3);
					pp2:=simplify(9*qa*qb*qc-27*qa^2*qd-2*qb^3);
					#cSquare:complex square, cRMulti:real number multiply complex number
                                        #cAdd,cMulti,cRDivi,cCubic,ww=-1/2+squre(3)i/2,tt=msign(pp2)
					#w(i)=w^i
					# p1=pp1,p2=pp2,s=ss,c1=cc1,c2=cc2,t=tt
					#ss:=cSquare(cRMulti(-3,p1));
					#cc1:=cCubic(cRDivi(cAdd(p2,cRMulti(3,s)),2));
					#cc2:=cCubic(cRDivi(cAdd(p2,cRMulti(-3,s)),2));
					#tt:=mSign(p2);

					DD1:=diff(cs[i],ord[i]$1);
					DD2:=diff(cs[i],ord[i]$2);
				
					for j from 1 to nops(res) do
						cset:=op(1,op(j,res));
						eset:={op(i,eqs)};
						for ic in cset do
							if `cons/contain`(ic,op(i,ord)) then
								eset:={op(eset),ic}
							fi;
							if `cons/noVarContain`(ic,ord) then
								eset:={op(eset),ic};
							fi;
						od;
	        				
						#^3Case 1
						res1:=`cons/eliminate`({op(eset),cat("[[",convert(DD1,string),">0 /\\ ",convert(DD2,string),">0] \\/ [",convert(DD1,string),"=0 /\\ ",convert(DD2,string),">=0]]")},var,[op(i,ord)]);
						#contradiction occured:go to contradication handler
						if res1=false then
							#
						#current conditions are always satisfied
						elif res1=true then
							val:=cat("cubic_1(",convert(qb,string),":",convert(qa,string),":",convert(pp1,string),":",convert(pp2,string),")");
							cset:={op(cset minus eset)};
							tres:=[op(tres),[cset,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						else
						        val:=cat("cubic_1(",convert(qb,string),":",convert(qa,string),":",convert(pp1,string),":",convert(pp2,string),")");	
							res2:={op(cset minus eset),res1};
							tres:=[op(tres),[res2,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						fi;
                                                print("case 31");print(res1);
						
						#^3Case 2
						res1:=`cons/eliminate`({op(eset),cat("[[",convert(DD1,string),"<=0 ] \\/ [",convert(DD2,string),"=0]]")},var,[op(i,ord)]);
						#contradiction occured:go to contradication handler
						if res1=false then
							#
						#current conditions are always satisfied
						elif res1=true then
							val:=cat("cubic_2(",convert(qb,string),":",convert(qa,string),":",convert(pp1,string),":",convert(pp2,string),")");
							cset:={op(cset minus eset)};
							tres:=[op(tres),[cset,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						else
							val:=cat("cubic_2(",convert(qb,string),":",convert(qa,string),":",convert(pp1,string),":",convert(pp2,string),")");
							res2:={op(cset minus eset),res1};
							tres:=[op(tres),[res2,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						fi;
                                                print("case 32");print(res1);

						##^3Case 3
						res1:=`cons/eliminate`({op(eset),cat("[[",convert(DD1,string),">0 /\\ ",convert(DD2,string),"<0] \\/ [",convert(DD1,string),"=0 /\\ ",convert(DD2,string),"<=0]]")},var,[op(i,ord)]);
						#contradiction occured:go to contradication handler
						if res1=false then
							#
						#current conditions are always satisfied
						elif res1=true then
							val:=cat("cubic_3(",convert(qb,string),":",convert(qa,string),":",convert(pp1,string),":",convert(pp2,string),")");
							cset:={op(cset minus eset)};	
							tres:=[op(tres),[cset,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						else
						        val:=cat("cubic_3(",convert(qb,string),":",convert(qa,string),":",convert(pp1,string),":",convert(pp2,string),")");		
							res2:={op(cset minus eset),res1};
							tres:=[op(tres),[res2,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						fi;
                                                print("case 33");print(res1);
					od;

				elif d=4 then 
					qa := coeff(cs[i],ord[i],4);
                			qb := coeff(cs[i],ord[i],3);
                			qc := coeff(cs[i],ord[i],2);
					qd := coeff(cs[i],ord[i],1);
					qe := coeff(cs[i],ord[i],0);
					print(qa);

					pp1:=simplify(-6*qa*qe*qb^2*qd^2+144*qa*qe^2*qc*qb^2+144*qa^2*qe*qc*qd^2+18*qa*qb*qd^3*qc+qc^2*qb^2*qd^2-4*qc^3*qb^2*qe-80*qa*qb*qd*qc^2*qe+18*qb^3*qd*qc*qe-128*qa^2*qe^2*qc^2-4*qb^3*qd^3+16*qc^4*qa*qe-4*qc^3*qa*qd^2-27*qb^4*qe^2+256*qa^3*qe^3-192*qa^2*qe^2*qb*qd-27*qa^2*qd^4);
					pp2:=simplify(-27*qb^2*qe+9*qb*qc*qd-2*qc^3+72*qc*qe*qa-27*qd^2*qa);
					pp3:=simplify(-8*qc*qa+3*qb^2);
					pp4:=simplify(4*qa^2*qb*qc-8*qa^3*qd-qb^3*qa);
					pp5:=simplify(16*qc*qe*qa^2-18*qd^2*qa^2-4*qc^3*qa+14*qc*qa*qd*qb-6*qb^2*qe*qa+qb^2*qc^2-3*qb^3*qd);

					DD1:=diff(cs[i],ord[i]$1);
					DD2:=diff(cs[i],ord[i]$2);
					DD3:=diff(cs[i],ord[i]$3);

					for j from 1 to nops(res) do
						cset:=op(1,op(j,res));
						eset:={op(i,eqs)};
						for ic in cset do
							if `cons/contain`(ic,op(i,ord)) then
								eset:={op(eset),ic}
							fi;
							if `cons/noVarContain`(ic,ord) then
								eset:={op(eset),ic};
							fi;
						od;

						#^4Case 1
						res1:=`cons/eliminate`({op(eset),cat("[[",convert(pp1,string),">=0 /\\ ",convert(DD1,string),">=0 /\\ ",convert(DD2,string),">=0 /\\ ",convert(DD3,string),">=0] \\/ [",convert(pp1,string),"<0 /\\ ",convert(pp4,string),">0 /\\ ",convert(DD1,string),">0]]")},var,[op(i,ord)]);
						#contradiction occured:go to contradication handler
						if res1=false then
								#
						#current conditions are always satisfied
						elif res1=true then
							val:=cat("quartic_1(",convert(qb,string),":",convert(qa,string),":",convert(pp1,string),":",convert(pp2,string),":",convert(pp3,string),":",convert(pp4,string),":",convert(pp5,string),")");
							cset:={op(cset minus eset)};
							tres:=[op(tres),[cset,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						else
							val:=cat("quartic_1(",convert(qb,string),":",convert(qa,string),":",convert(pp1,string),":",convert(pp2,string),":",convert(pp3,string),":",convert(pp4,string),":",convert(pp5,string),")");
							res2:={op(cset minus eset),res1};
							tres:=[op(tres),[res2,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						fi;

						#^4Case 2
						res1:=`cons/eliminate`({op(eset),cat("[[",convert(pp1,string),">=0 /\\ ",convert(DD1,string),"<=0 /\\ [",convert(DD2,string),"<=0 \\/ ",convert(DD3,string),">=0]] \\/ [",convert(pp1,string),"<0 /\\ ",convert(pp4,string),"<=0 /\\ ",convert(DD1,string),">0]]")},var,[op(i,ord)]);
						#contradiction occured:go to contradication handler
						if res1=false then
								#
						#current conditions are always satisfied
						elif res1=true then
							val:=cat("quartic_2(",convert(qb,string),":",convert(qa,string),":",convert(pp1,string),":",convert(pp2,string),":",convert(pp3,string),":",convert(pp4,string),":",convert(pp5,string),")");
							cset:={op(cset minus eset)};
							tres:=[op(tres),[cset,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						else
							val:=cat("quartic_2(",convert(qb,string),":",convert(qa,string),":",convert(pp1,string),":",convert(pp2,string),":",convert(pp3,string),":",convert(pp4,string),":",convert(pp5,string),")");
							res2:={op(cset minus eset),res1};
							tres:=[op(tres),[res2,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						fi;

						#^4Case 3
						res1:=`cons/eliminate`({op(eset),cat("[[",convert(pp1,string),">=0 /\\ ",convert(DD1,string),">=0 /\\ [",convert(DD2,string),"<=0 \\/ ",convert(DD3,string),"<=0]] \\/ [",convert(pp1,string),"<0 /\\ ",convert(pp4,string),">0 /\\ ",convert(DD1,string),"<0]]")},var,[op(i,ord)]);
						#contradiction occured:go to contradication handler
						if res1=false then
								#
						#current conditions are always satisfied
						elif res1=true then
							val:=cat("quartic_3(",convert(qb,string),":",convert(qa,string),":",convert(pp1,string),":",convert(pp2,string),":",convert(pp3,string),":",convert(pp4,string),":",convert(pp5,string),")");
							cset:={op(cset minus eset)};
							tres:=[op(tres),[cset,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						else
							val:=cat("quartic_3(",convert(qb,string),":",convert(qa,string),":",convert(pp1,string),":",convert(pp2,string),":",convert(pp3,string),":",convert(pp4,string),":",convert(pp5,string),")");
							res2:={op(cset minus eset),res1};
							tres:=[op(tres),[res2,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						fi;

						#^4Case 4
						res1:=`cons/eliminate`({op(eset),cat("[[",convert(pp1,string),">=0 /\\ ",convert(DD1,string),"<=0 /\\ ",convert(DD2,string),">=0 /\\ ",convert(DD3,string),"<=0] \\/ [",convert(pp1,string),"<0 /\\ ",convert(pp4,string),"<=0 /\\ ",convert(DD1,string),"<0]]")},var,[op(i,ord)]);
						#contradiction occured:go to contradication handler
						if res1=false then
								#
						#current conditions are always satisfied
						elif res1=true then
							val:=cat("quartic_4(",convert(qb,string),":",convert(qa,string),":",convert(pp1,string),":",convert(pp2,string),":",convert(pp3,string),":",convert(pp4,string),":",convert(pp5,string),")");
							cset:={op(cset minus eset)};
							tres:=[op(tres),[cset,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						else
							val:=cat("quartic_4(",convert(qb,string),":",convert(qa,string),":",convert(pp1,string),":",convert(pp2,string),":",convert(pp3,string),":",convert(pp4,string),":",convert(pp5,string),")");
							res2:={op(cset minus eset),res1};
							tres:=[op(tres),[res2,CS,[ord[i]=val,op(op(3,op(j,res)))]]];
							flag:=flag+1;
						fi;
					od;
				#          degree=4 here.
				else 
					flag:=1;
					tres:=res;
				fi;
				#contradiction occured
				if flag=0 then 
					return []
				else
					flag:=0;
					res:=tres;
				fi;
                                print(res);
			else
				break;
			fi;
			
		od;        		
		return res;
	fi
end proc:

## change the QEPCAD mode to java mode
`cons/convert`:=proc(cons)
	local i,str;

	str:="";
	if type(cons,string) then
		str:=cat(`(`,`cons/convertSub`(cons),`)`)
	elif type(cons,polynom) then
		str:=cat(`(`,convert(cons,string),`=0)`);
	elif type(cons,{`=`,`<`,`<=`,`<>`}) then
		str:=cat(`(`,`cons/convertSub`(convert(cons,string)),`)`);
	elif type(cons,{set,list}) then
		for i from 1 to nops(cons) do
			if type(op(i,cons),string) then
				str:=cat(str,`(`,`cons/convertSub`(op(i,cons)),`)`)
			elif type(op(i,cons),polynom) then
				str:=cat(str,`(`,convert(op(i,cons),string),`=0)`);
			elif type(op(i,cons),{`=`,`<`,`<=`,`<>`}) then
				str:=cat(str,`(`,`cons/convertSub`(convert(op(i,cons),string)),`)`);
			else
				ERROR(`Wrong arguments.`);
				return "";
			fi;
			if i<>nops(cons) then
				str:=cat(str," && ");
			fi
		od:
	else
 		ERROR(`Wrong arguments.`);
 		return "";
 	fi;
	return str;	
end:

`cons/convertSub`:=proc(str::string)
	local i,s,cur,nex,res;
	s:=StringTools[Remove](rcurry( member, { "\t", "\n", "\t", "\v", "\f" } ),str);
	s:=StringTools[Squeeze](s);
	s:=StringTools[SubstituteAll](s,"\\/","||");
	s:=StringTools[SubstituteAll](s,"/\\","&&");
	s:=StringTools[SubstituteAll](s,"/=","!=");
	s:=StringTools[SubstituteAll](s,"[","(");
	s:=StringTools[SubstituteAll](s,"]",")");
	s:=StringTools[SubstituteAll](s,"<>","!=");

	cur:=`cons/nextWord`(s,1);
	res:=cur;
	for i from 1+length(cur) to length(s) do
		nex:=`cons/nextWord`(s,i);
		if not `cons/isOp`(cur) then 
			if not `cons/isOp`(nex) then
				res:=cat(res,`*`);
			elif nex="(" then 
				res:=cat(res,`*`);
			fi;
		fi;
		cur:=nex;
		res:=cat(res,cur);
		i:=i+length(cur);						
	od:
	return res;
end:
`cons/nextWord`:=proc(str::string,i)
	local s,ind;
	s:="";
	ind:=i;
	while StringTools[IsSpace](substring(str,ind..ind)) do
		ind:=ind+1;
		s:=cat(s,` `);
	od;
	while not StringTools[IsSpace](substring(str,ind..ind)) do 
		s:=cat(s,substring(str,ind..ind));
		ind:=ind+1;
	od;			
	s;
end:


`cons/isOp`:=proc(str::string)
	if member(StringTools[Trim](str),
					{"=",">=",">","<","<=","!=","||","&&","+","-","/","(",")"}) then
		return true
	else
		return false
	fi
end:
