conseqdlg.cpp

命题逻辑中的归结推理系统设计与实现,人工智能实习项目,包括实验报告

	return 0;
}

void CconseqDlg::addchar(char c)
{
	    qlink=(link*)malloc(sizeof(link));
		qlink->data=c;
		qlink->n=0;
		plink->next=qlink;
		qlink->next=NULL;
		qlink->pre=plink;
		plink=qlink;
		head->pre=qlink;
		plink->next=head;
	    
}
void CconseqDlg::addchar2(char c,int a)
{
	    qlink=(link*)malloc(sizeof(link));
		qlink->data=c;
		if( a==2 )
			qlink->n=1;
		else qlink->n=0;
		qlink->next=plink->next;
		qlink->pre=plink;
		plink->next->pre=qlink;
		plink->next=qlink;
		plink=qlink;

}
void CconseqDlg::OnBnClickedRe()
{
	// TODO: 在此添加控件通知处理程序代码

}
void CconseqDlg::init()
{
	// TODO: 在此添加控件通知处理程序代码
	num=0;
	step=1;
	memset(test,0,sizeof(test));
	memset(statu,0,sizeof(statu));

	delete []head;

	head = (link *)malloc(sizeof(link)); 
	head->next = NULL; 
	plink=head;
}
void CconseqDlg::toson()
{
    wchar_t w[200];
	GetDlgItemText(IDC_TE,w,200);
	char temp[200];
	CString c1(w); 
	int i=::WideCharToMultiByte (CP_ACP,WC_DEFAULTCHAR|WC_COMPOSITECHECK ,w,c1.GetLength (),temp,200,0,0);
	temp[i]='\0';
     CString tp=L"输入的命题为: ";
	for( int ls=0;ls<i;ls++)
	{
		if( temp[ls]=='v') 			tp+=L"∨";
		else if( temp[ls]=='>')      tp+=L"->";
		else if(temp[ls]==',')      tp+=L"∧";
		else if( temp[ls]=='(')      tp+=L"（";
		else if(temp[ls]==')')      tp+=L"）";
		else tp+=CString(temp[ls]);
	}
	CListBox* pLB = (CListBox*)GetDlgItem(IDC_OUTPUT);
			pLB->AddString(CString(tp));
	int j=0,k;
	int flag=0;
	for( j=i-1;j>=0;j--)
	{
		if(  temp[j]==')')
			flag++;
		else if( temp[j]=='(')
			flag--;
		if(!flag &&  temp[j]=='>')
			break;
	}     

	 addchar('(');
	 for( k=0;k<j;k++)                 
           addchar(temp[k] );
	 addchar(')');
	 addchar(',');

		 addchar('~');
		 addchar('(');
		 for( k=j+1;k<i;k++)
					addchar(temp[k]);       
		 addchar(')');
}
void CconseqDlg::yunhan()
{
	int flag=0;
	int again=0;
	while(1)
	{
     flag=0;
	 again=0;
	 for(plink=head->next;plink!=head;plink=plink->next)
		if( plink->data=='>')
		{
			link *cur2=(link*)malloc(sizeof(link));
			cur2=plink;
			qlink=(link*)malloc(sizeof(link));
			//qlink->data='{';
			qlink->data='(';
			qlink->next=cur2->next;
			qlink->pre=cur2;
			cur2->next->pre=qlink;
			cur2->next=qlink;
			cur2=qlink;
            flag=1;
			cur2=qlink->next;
			for(;cur2!=head;cur2=cur2->next)
			{       

				if( cur2->data=='(' || cur2->data=='{') flag++;
				if( cur2->data==')'||cur2->data=='}') flag--;
			     if( cur2->next->data==',' || cur2->next==head || cur2->next->data=='>' || !flag )
				 {
					 if( !flag )
			           cur2=cur2->pre;
					// cur2=cur2->pre;
                     qlink=(link*)malloc(sizeof(link));
				//	 qlink->data='}';
					  qlink->data=')';
			         qlink->next=cur2->next;
			         qlink->pre=cur2;
					 cur2->next->pre=qlink;
			         cur2->next=qlink;
			         cur2=qlink;
					 break;
				 }
			}
			again=1;
			plink->data='v';
			plink=plink->pre;
			//addchar2(']');
			addchar2(')',1);
			link *cur=(link*)malloc(sizeof(link));
			cur=plink->pre;
			flag=1;
			for(;cur!=head;cur=cur->pre)
			{ 
				if( cur->data==')' || cur->data==']')
					flag++;
				if( cur->data=='(' || cur->data=='[')
					flag--;
				if( cur->data==','|| cur==head || !flag )
			    {
					//cur=cur->pre;
					 qlink=(link*)malloc(sizeof(link));
		          	 qlink->data='~';
			         qlink->next=cur->next;
			         qlink->pre=cur;
					 cur->next->pre=qlink;
			         cur->next=qlink;
			         cur=qlink;
					 plink=cur;
				   // addchar2('[');
				   addchar2('(',1);
				   break;
			    }
			}
			break;
		}  
		if( again ) continue;
		else break;
	}

   delkuo();

	CString tp=L"求反消去'->': ";
	for( plink=head->next;plink!=head;plink=plink->next)
	{
		if( plink->data=='v') 			tp+=L"∨";
		else if( plink->data=='>')      tp+=L"->";
		else if( plink->data==',')      tp+=L"，";
		else if( plink->data=='(')      tp+=L"（";
		else if( plink->data==')')      tp+=L"）";
    	else if( plink->data=='&')       tp+=L"∧";
	    else tp+=CString(plink->data);

	}
	CListBox* pLB = (CListBox*)GetDlgItem(IDC_OUTPUT);
			pLB->AddString(CString(tp));

}

void CconseqDlg::delkuo()
{
	 int flag=0;
	 while(1)
	 {
       flag=0;
	   delnot();
	  for( plink=head->next;plink!=head;plink=plink->next)
	   {
	     
	      if( plink->data=='~' && plink->next->data=='~' )
			  {				
                     plink->data='!';
					 plink->next->data='!';
					 flag=1;break;
		      }
		  if( plink->data=='(' && plink->next->next->data==')' )
		  {         plink->data='!' ;
		            plink->next->next->data='!';
					 flag=1;
					 break;
		  }
		  if(  plink->data=='(' && plink->next->next->next->data==')'&& plink->pre->data=='~' && plink->next->data=='~' )
		  {
                   plink->data='!' ;
                   plink->next->next->next->data='!';
                   plink->pre->data='!';
				   plink->next->data='!';
				   flag=1;
				   break;
		  }
		  if( plink->data=='(' && plink->next->next->next->data==')'&& plink->pre->data!='~' && plink->next->data=='~')
		  {          
                    plink->data='!' ;
					plink->next->next->next->data='!';
					 flag=1;break;
		  }
	  }
	  if( flag ) continue;
	  else break;
	 }
	 while(1)
	 {
     	  flag=0;
		  delnot();
		  for( plink=head->next;plink!=head;plink=plink->next)
		   {
			  if( plink->data=='(' && plink->next->data=='(' )
			  {	
				  int nms=1;
				  link *cur=(link*)malloc(sizeof(link));
				  for( cur=plink->next->next;cur!=head;cur=cur->next)
				  {
					  if( cur->data=='(' )  nms++;
					  else if( cur->data==')') nms--;
					  if( !nms )
					  {
						 if(cur->next->data==')')
						 {
						  plink->data='!';
						  cur->data='!';
						  flag=1;
						  break;
						 }
						 break;
					  }
				  }
			  }
			  if( flag ) break;
		   }
		  if( flag ) continue;
		  else break;
	 }
	 while(1)
	 {
			  flag=0;
			  delnot();
			  qlink=head->next;
			  if( qlink->data=='(')
			  {
				  int nums=1;
				  for( plink=qlink->next; ;plink=plink->next)
				  {
					  if( plink->data=='(')				  nums++;
					  else if( plink->data==')')          nums--;
					  if( !nums )
					  {
						  if( plink->next->data==',')   
						    {
							  qlink->data='!';
							  plink->data='!';
							  flag=1;
							  break;
						      }
						  break;
						}
				  }
			  }
			 if( flag ) continue;
			 else break;
	 }


	 while(1)
	 {
	   flag=0;
	  for( qlink=qlink->next; qlink->data!=',';qlink=qlink->next);

	  for( plink=qlink->pre;plink!=head;plink=plink->next)
		  {
			  if( plink->data==',' && plink->next->data=='(' ) 
			  {	
				  link *cur=(link*)malloc(sizeof(link));
				  for( cur=plink->next->next;cur!=head;cur=cur->next)
				  {
					  if( (cur->data==')' && cur->next->data==',')|| ( cur->data==')' && cur->next==head) )
					  {
						  plink->next->data='!';
						  cur->data='!';
						  flag=1;
                          break;
					  }
					  else if( cur->data!=')' && cur->next->data==',')
						  break;
				  }
			  }
			  if( flag ) break;
		   }
	      if( flag )
		  {
			  delnot();
			  continue;
		  }
		  else break;
	 }

	 

     delnot();
}
void CconseqDlg::delnot()
{
	 int flag=0;

	while(1)
	 {
       flag=0;
	  for( plink=head->next;plink!=head;)
	   {
		   if( plink->data=='!')
		   {
			   plink->next->pre=plink->pre;
			   plink->pre->next=plink->next;
			   qlink=plink->next;
			   plink->next=NULL;
			   plink->pre=NULL;
			   plink=qlink;
			   flag=1;
			   break;
		   }
		   else plink=plink->next;
	   }
	  if( flag ) 
	  {	continue;
	  }
	  else break;
	 }
}
void CconseqDlg::fei()
{
    int flag=0;
	 while(1)
	 {
      flag=0;
	  delkuo();
	 // addkuo();
	  for( plink=head->next;plink!=head;plink=plink->next)
	   {
		   if( plink->data=='~'&& plink->next->data=='(')
		   {
			   link *curtmp=(link*)malloc(sizeof(link));
               curtmp=plink->pre;
	           qlink=(link*)malloc(sizeof(link));
		       qlink->data='(';
			   qlink->next=curtmp->next;
			   qlink->pre=curtmp;
			   curtmp->next->pre=qlink;
			   curtmp->next=qlink;

			   plink->data='!';
			   int nums=1;
			   link *cur=(link*)malloc(sizeof(link));
			   for( cur=plink->next->next;cur!=head;cur=cur->next)
			       {
					   if( cur->data=='~' ) continue;
					   else if( cur->data=='v' && nums==1 )
						   cur->data='&';
					   else  if( cur->data=='(') 
					   {
                         link *curtmp=(link*)malloc(sizeof(link));
					     curtmp=cur->pre;
					     qlink=(link*)malloc(sizeof(link));
		            	 qlink->data='~';
						 qlink->next=curtmp->next;
						 qlink->pre=curtmp;
						 curtmp->next->pre=qlink;
						 curtmp->next=qlink;
						   nums++;
					   }
					   else if( cur->data==')')
					   {
						   nums--;
					   }
					   else if( cur->data>='a' && cur->data<='z'&& nums==1 )
					   {
					    link *curtmp=(link*)malloc(sizeof(link));
					    curtmp=cur->pre;
					    qlink=(link*)malloc(sizeof(link));
		            	qlink->data='~';
			            qlink->next=curtmp->next;
			            qlink->pre=curtmp;
					    curtmp->next->pre=qlink;
			            curtmp->next=qlink;
					   }
					   if( !nums )
					   {
						plink=cur;
						addchar2(')',1);
			           flag=1;
			           break;
					   }
			       }
			   if( flag ) break;
		   }
	   }
	  if( flag ) 
	  {			continue;
	  }
	  else break;
	 }
    CString tp=L"化简'非'得:   ";
	for( plink=head->next;plink!=head;plink=plink->next)
	{
		if( plink->data=='v') 			tp+=L"∨";
		else if( plink->data=='>')      tp+=L"->";
		else if( plink->data==',')      tp+=L"，";
		else if( plink->data=='(')      tp+=L"（";
		else if( plink->data==')')      tp+=L"）";
	    else if( plink->data=='&')       tp+=L"∧";
	    else tp+=CString(plink->data);

	}
	CListBox* pLB = (CListBox*)GetDlgItem(IDC_OUTPUT);
			pLB->AddString(CString(tp));

}
void CconseqDlg::hequ()
{
   
	plink=head;
	addchar2('(',1);
	link* scur=(link*)malloc(sizeof(link));
	for( scur=head->next;scur->data!=',';scur=scur->next)
	{
		scur->n=0;
	}
	plink=scur->pre;
	addchar2(')',1);