/*Complied with g++.
*this program is primarily used for testing individual DNF with more than
6 variables to see if there is any counterexample to the
conjecture described in the thesis  
*
*/
# include <stdio.h>
# include <math.h>
# include <stdlib.h>
# include <fstream.h>
# include <iostream.h>

#define Nvar 6 //the number of variables in a DNF
#define Nterm 64 //the max number of terms in a 6 vars DNF

void nrerror(char error_text[])
	/*Numerical Recipes standard error handler*/
{
	int i;
	printf("\n\n");
	fprintf(stderr,"Numerical Recipes run-time error...\n");
	fprintf(stderr,"%s\n",error_text);
	fprintf(stderr,"...now exiting to system...\n");
	exit(1);
}

int **imatrix(int nrl,int nrh,int ncl,int nch)
	/*Allocates a float matrix with range [nrl..nrh][ncl..nch]*/
{
	int i;
	int **m;

	m = new(int *[nrh-nrl+1]);
	if(!m)nrerror("Allocation failure 1 in matrix()");
	m-=nrl;

	for(i=nrl;i<=nrh;i++){
		m[i] = new(int [nch-ncl+1]);
		if(!m[i]) nrerror("Allocation failure 2 in matrix");
		m[i] -= ncl;
	}

	return(m);
}
void free_imatrix(int **m,int nrl,int nrh,int ncl,int nch)
	/*Frees a matrix allocated by matrix()*/
{   
	int i;
	for(i=nrh;i>=nrl;i--) delete [] (m[i]+ncl);
	delete [] (m+nrl);
}

int influence_cal(int **m,int tm,int n)
	/* the array vlist stores the list of variables as well as its inf,
	 * sorted from the max inf to min inf 
	 */
{
	//to calculate the inf using the naive method, which defines the inf as a ratio of the numb of changed f(v)|v:0->1, 	
	//with the total 2^n numbers. And here the inf is defined without normalized by 2^n since one only cares the relative inf
	int dnf[Nterm],v[n];
	int i,j,k,l;
	int fv,tv; //either 0 or 1
	int tmp, indxf;
	int max=0, mindex;
	int vinf[n];
	

	for(i=0;i<Nterm;i++) //calculate the DNF[i] for i= 0 to 2^n
	{
		//initialize the varibles
		for(j=0;j<n;j++)
			v[j]=((i>>j)&1)? 1:0 ;

		//calculate the DNF function value for each i
		fv=0;
		for(k=1;k<=tm;k++)
		{
			tv=1; //initialize the term value
			for(l=1;l<=n;l++)
			{
				if(m[k][l]&1) //variable exsits
					tv&=v[l-1];
			}
			fv|=tv;
			if(fv&1)  break; //if DNF is already 1, calculation is done
		}
		dnf[i]=fv;
	}

	//cal the inf for each varible
	for(j=0;j<n;j++)//for each var
	{
		vinf[j]=0; //initialize 
		for(i=0;i<Nterm;i++)//go through the whole list
		{
		  if(!((i>>j)&1))//if the var_j is 0 
		  {
			  tmp=dnf[i];  
			  indxf=(i|(1<<j)); //flip the var_j from 0 to 1
			  if(tmp!=dnf[indxf])//if the DNF changes
			  vinf[j]++; 
		  }
		}//end of the list
	} //end of the inf cal

	for(j=0;j<n;j++) //for each var
	{
		if(max<vinf[j])
		{
			mindex=j;
			max=vinf[j];
		}
	}

	//now return the index of the max influce var 
	return mindex+1;
}

//this method is used to cal the number of leaves in a OPT tree
//using a standard recursive tree algo
int opt_cal(int ** mdnf,int nt, int nv, int flag)
	/* The mdnf mtree is the matrix representation of the DNF
	 * and this matrix by default has the number of col from 1 to N.
	 * But this number changes once we exclude one var as a root and set root 
	 * to 0 or 1.
	 * The number of rows is the nrow which is total number of terms
	 * in a DNF expression.
	 * It seems like that this ALGo has O(2^N) complexity.
	 */
{
	int i,j,k,l,h;
	int min=200;//Nterm; //the total number of leaves for each var as a root
	int leaf[nv+1];
	int v0f[nt+1]; //a set of flag bits once set v<-0
	int cn0; //the counts for the non-zero terms in the remaining dnf once set v<-0
	int ** lsub=NULL, ** rsub=NULL; //left and right subtree
	int var_sum;

	for(i=1;i<=nv;i++)
		leaf[i]=0;

	if(flag==1)//if DNF is already a constant
	{
		return 1;
	}
	else //if not
	{
		for(i=1;i<=nv;i++)
		{
			//v<-0, the left subtree
			for(j=1;j<=nt;j++)
				v0f[j]=-1;

			cn0=nt;
			for(j=1;j<=nt;j++)
			{
				if(mdnf[j][i]==1)//if var_i exists
				{
					cn0--;
					v0f[j]=0;
				}
				else
				{
					v0f[j]=1;
				}
			}

			if(cn0==0)//the dnf is 0
			{
				leaf[i]++;// opt_cal(NULL,0,0,1);
			}
			else
			{
				//since the left subtree is not a const
				//then we has to recursively call the opt method
				lsub=imatrix(1,cn0,1,nv-1);//allocate a dnf of left subtree

				//the following code copy the orignal dnf to the new left subtree dnf
				//when v<-0 to the root
				k=1;
				for(h=1;h<=nt;h++)
				{
					if(v0f[h]==1)//the term exists
					{
						for(l=1;l<=i-1;l++)
							lsub[k][l]=mdnf[h][l]; //copy original dnf
						for(l=i+1;l<=nv;l++)
							lsub[k][l-1]=mdnf[h][l]; //copy original dnf
						k++;
					}
				}
					

				//now call recursivly
			       // cout<<"cn0 is "<<cn0<<"\n";
			       // cout<<"nv is "<<nv<<"\n";
				//for(h=1;h<=cn0;h++)
				//	for(l=1;l<=(nv-1);l++)
				//		cout <<" lsub["<<h<<"]["<<l<<"] is"<<lsub[h][l]<<"\n";

				leaf[i]+=opt_cal(lsub,cn0,nv-1,0);
				free_imatrix(lsub,1,cn0,1,nv-1);
			} //done of the v<-0 case 

			//cout<<"cn0 is "<<cn0<<"\n";
			//cout<<"nv is "<<nv<<"\n";
			
			//v<-1 , the right subtree
			for(j=1;j<=nt;j++)
			{
				var_sum=0; //initializeing for every row
				if(mdnf[j][i]==1)//if var_i exists
					for(k=1;k<=nv;k++)
						var_sum+=mdnf[j][k];

				if(var_sum==1) break;

			}
			if(var_sum==1)//the dnf is 1
			{
			       	leaf[i]++; //opt_cal(NULL,0,0,1);
			}
			else //a big else part
			{
				//since the right subtree is not a const
				//then we has to recursively call the opt method
				rsub=imatrix(1,nt,1,nv-1);//allocate a dnf of right subtree

				//the following code copy the orignal dnf to the new right subtree dnf
				//when v<-1 to the root
				for(k=1;k<=nt;k++)
				{
					for(l=1;l<=i-1;l++)
						rsub[k][l]=mdnf[k][l]; //copy original dnf
					for(l=i+1;l<=nv;l++)
						rsub[k][l-1]=mdnf[k][l]; //copy original dnf
				}

				//now call recursivly
				leaf[i]+=opt_cal(rsub,nt,nv-1,0);
				free_imatrix(rsub,1,nt,1,nv-1);
			} //done for the right subtree

			if(min>leaf[i])
			{
				min=leaf[i];  //get the min leaves
			//cout << "i is "<<i<<"  leaf[i] is " <<leaf[i]<<"\n";
			}
		}
		
		//after all the vars get tried and the min leaves number were tried
		return min;
	} //end of else flag
}

//this method is used to cal the number of leaves in a OPT tree
//using a standard recursive tree algo
//except everytime choosing the max influnce var as the root
int inf_opt_cal(int ** mdnf,int nt, int nv, int flag)
	/* The mdnf mtree is the matrix representation of the DNF
	 * and this matrix by default has the number of col from 1 to N.
	 * But this number changes once we exclude one var as a root and set root 
	 * to 0 or 1.
	 * The number of rows is the nrow which is total number of terms
	 * in a DNF expression.
	 * It seems like that this ALGo has O(2^N) complexity.
	 */
{
	int i,j,k,l,h;
	int min=Nterm; //the total number of leaves for each var as a root
	int leafn=0;
	int v0f[nt+1]; //a set of flag bits once set v<-0
	int cn0; //the counts for the non-zero terms in the remaining dnf once set v<-0
	int ** lsub, ** rsub; //left and right subtree
	int var_sum;

	if(flag==1)//if DNF is already a constant
	{
		return 1;
	}
	else //if not
	{
		i=influence_cal(mdnf,nt,nv);  //get the max inf index
		cout<<"max inf index is "<<i<<"\n";

			//v<-0, the left subtree
			cn0=nt;
			for(j=1;j<=nt;j++)
			{
				if(mdnf[j][i]==1)//if var_i exists
				{
					cn0--;
					v0f[j]=0;
				}
				else
				{
					v0f[j]=1;
				}
			}

			if(cn0==0)//the dnf is 0
			{
				leafn++; //inf_opt_cal(NULL,0,0,1);
			}
			else
			{
				//since the left subtree is not a const
				//then we has to recursively call the opt method
				lsub=imatrix(1,cn0,1,nv-1);//allocate a dnf of left subtree
				//initializing the new dnf matrix
				
				for(k=1;k<=cn0;k++)//terms
					for(l=1;l<=nv-1;l++)//vars
						lsub[k][l]=0;

				//the following code copy the orignal dnf to the new left subtree dnf
				//when v<-0 to the root
				k=1;
				for(h=1;h<=nt;h++)
				{
					if(v0f[h]==1)//the term exists
					{
						for(l=1;l<=i-1;l++)
							lsub[k][l]=mdnf[h][l]; //copy original dnf
						for(l=i+1;l<=nv;l++)
							lsub[k][l-1]=mdnf[h][l]; //copy original dnf
						k++;
					}
				}
					

				//now call recursivly
				leafn+=inf_opt_cal(lsub,cn0,nv-1,0);
				free_imatrix(lsub,1,cn0,1,nv-1);
			} //done of the v<-0 case 
			
			//v<-1 , the right subtree
			for(j=1;j<=nt;j++)
			{
				var_sum=0; //initializeing for every row
				if(mdnf[j][i]==1)//if var_i exists
					for(k=1;k<=nv;k++)
						var_sum+=mdnf[j][k];

				if(var_sum==1) break;

			}
			if(var_sum==1)//the dnf is 1
			{
				leafn++; //=inf_opt_cal(NULL,0,0,1);
			}
			else //a big else part
			{
				//since the right subtree is not a const
				//then we has to recursively call the opt method
				rsub=imatrix(1,nt,1,nv-1);//allocate a dnf of right subtree
				//initializing the new dnf matrix
				
				for(k=1;k<=nt;k++)//terms
					for(l=1;l<=nv-1;l++)//vars
						rsub[k][l]=0;

				//the following code copy the orignal dnf to the new right subtree dnf
				//when v<-1 to the root
				for(k=1;k<=nt;k++)
				{
					for(l=1;l<=i-1;l++)
						rsub[k][l]=mdnf[k][l]; //copy original dnf
					for(l=i+1;l<=nv;l++)
						rsub[k][l-1]=mdnf[k][l]; //copy original dnf
				}

				//now call recursivly
				leafn+=inf_opt_cal(rsub,nt,nv-1,0);
				free_imatrix(rsub,1,nt,1,nv-1);
			} //done for the right subtree

		//after all the vars get tried and the min leaves number were tried
		//return the result
		return leafn;
	} //end of else flag
}


int main(int argv, char *argc[])
{
        char c; 
	int i,j;
        int ** DNF; //the dynamincal matrix used to represent a DNF function
	int leaf_opt;
	int leaf_opt_inf;

	if(argv<2)
	{
	  printf("syntax: <inf_cal.out> <txt file> \n");
	  exit(0);
	}


	//allocating and initializing a DNF matrix
	DNF=imatrix(1,Nterm,1,Nvar);
        for(i=1;i<=Nterm;i++)
	{
		for(j=1;j<=Nvar;j++)
		{
			DNF[i][j]=0;
		}
	}

	int tn=1; //to keep track of the actual terms in a DNF

	//the following reads a DNF function from a file and stores in a matrix
        ifstream fin;
	fin.open(argc[1],ifstream::in);
        int vn;
        fin.get(c);
	while(c!='\n')
	{
		fin>>vn;
		DNF[tn][vn]=1;
		fin.get(c);
		if(c=='+')
		{
			tn++;
			fin.get(c);
		}
	}

	fin.close(); //finishing reading the  file
/*
 * debug the output
 * of the input reading
 */
	cout<<" the input file has "<<tn<<"terms\n";
	cout<<"the dnf matrix is:\n";
	/*
        for(i=1;i<=tn;i++)
	{
		for(j=1;j<=Nvar;j++)
		{
			cout<<DNF[i][j];
		}
		cout<<"\n";
	}
	*/

       //calculate the OPT tree's number of leaves
       leaf_opt=opt_cal(DNF,tn,Nvar,0);
       leaf_opt_inf=inf_opt_cal(DNF,tn,Nvar,0);

       if(leaf_opt!=leaf_opt_inf)
       {
	       cout << " counter example is found\n";
	       cout <<"the leaf_opt is "<<leaf_opt<<"\n";
	       cout <<"the leaf_opt_inf is "<<leaf_opt_inf<<"\n";
       }
       else
       {
	       cout <<"No counter example is found\n";
	       cout <<"the leaf_opt is "<<leaf_opt<<"\n";
	       cout <<"the leaf_opt_inf is "<<leaf_opt_inf<<"\n";
       }

	return 0;
}