// ClausesResolution.cpp : 定义控制台应用程序的入口点。
//A Implemention Of Simple Clauses Resolution
//Author: Wang Yun , ANHUI UNIVERSITY
#include "stdafx.h"
#include<iostream>
#include<cstring>
//#include<string>
#include<ctime>
using namespace std;
const short CLAUSE_LENGTH=60;
const short CLAUSES_MAX_NUM=5;
const short PARA_MAX_NUM=7;
const short PARA_LENGTH=15;
const short WORD_MAX_NUM=8; //the maximal number of words per clause
const short STACK_LENGTH=PARA_MAX_NUM*PARA_LENGTH;
static int clauses_sum=0;
const char SEPARATOR='|';
struct wordage
{
char negate;
char predicate;
short parameters_sum;
char parameters[PARA_MAX_NUM][PARA_LENGTH];
};
struct can_be_resolved
{
char pred;
int clause_index[2];
int wordage_index[2];
};
struct _sigma
{
char res_char;
char instead_char[PARA_LENGTH];
};
wordage* disassembled_clauses[CLAUSES_MAX_NUM][WORD_MAX_NUM];
char** get_clause();
short* disassemble_clause(char** clauses);
can_be_resolved* get_resolved_predicates(short* words_sum,int *resolved_wd_sum);
_sigma* get_sigma_set(can_be_resolved* reslvd_preds,int *reslvd_prds_sum,int *sigma_s);
char* get_resolution_result(_sigma* sigma,int sigma_sm,char** p_clauses,
can_be_resolved* reslvd_preds,int reslvd_prds_sum);
char** get_clause()
{
static char* p_clauses[CLAUSES_MAX_NUM];
int i;
cout<<"Enter the amount of clauses you will input:";
cin>>clauses_sum;
if(clauses_sum>CLAUSES_MAX_NUM)
cout<<"The number you entered is overflow!\n";
for (i=0;i<clauses_sum;i++)
{
cout<<"Please enter clause "<<i+1<<":\n\t";
p_clauses[i]=new char[CLAUSE_LENGTH];
cin>>p_clauses[i];
}
if(i==clauses_sum)
cout<<"Finished Entering!\n";
return p_clauses;
}
short* disassemble_clause(char** clauses)
{
int i,j,k;
int bracket_stack[STACK_LENGTH];
int stack_top=-1;
bool is_nor=false,is_predicate,is_new_word;
static short* word_sum=new short[clauses_sum];
for (i=0;i<clauses_sum;i++)
{
k=-1;
j=0;//reference to the charactor in every clause
is_new_word=true;
while (is_new_word)
{
is_new_word=false;
is_predicate=true;
++k;
word_sum[i]=k+1;//store the sum of wordages in 'i' clause
disassembled_clauses[i][k]=new wordage;
disassembled_clauses[i][k]->negate='\0';
disassembled_clauses[i][k]->parameters_sum=0;
if(clauses[i][j]=='~')
{
disassembled_clauses[i][k]->negate=clauses[i][j];
++j;
is_predicate=true;
}
if(is_predicate)
{
disassembled_clauses[i][k]->predicate=clauses[i][j];
++j;
is_predicate=false;
}
while (SEPARATOR!=clauses[i][j] && '\0'!=clauses[i][j]) //get parameters after the predicate
{
int para_i=0,para_charac_i=0;
bool is_new_para=true;
if( ('['==clauses[i][j] || '('==clauses[i][j])
&& -1==stack_top )
{
++stack_top;
bracket_stack[stack_top]=clauses[i][j];
++j;
continue;
}
while (is_new_para && -1!=stack_top)
{
if('['==clauses[i][j] || '('==clauses[i][j])
{
++stack_top;
bracket_stack[stack_top]=clauses[i][j];
}
if(']'==clauses[i][j] || ')'==clauses[i][j])
--stack_top;
if(-1==stack_top)
{ disassembled_clauses[i][k]->parameters[para_i][para_charac_i++]='\0';
disassembled_clauses[i][k]->parameters_sum++;
++j;
break;
}
disassembled_clauses[i][k]->parameters[para_i][para_charac_i++]=clauses[i][j];
++j;
if(0==stack_top && ','==clauses[i][j])
{
disassembled_clauses[i][k]->parameters[para_i][para_charac_i++]='\0';
disassembled_clauses[i][k]->parameters_sum++;
++para_i;
++j;
para_charac_i=0;
continue;
}
}//end of "while (is_new_para && -1!=stack_top)"
if(-1==stack_top) break;
}//end of "while ('|'!=clauses[i][j] && '\0'!=clauses[i][j])"
if(SEPARATOR==clauses[i][j])
{
is_new_word=true;
++j;
}
if(!clauses[i][j])
break;
}//end of "while(is_new_word)"
}//end of "for(i=0;i<clauses_sum;i++)"
return word_sum;
}//end of the function
can_be_resolved* get_resolved_predicates(short* words_sum,int *resolved_wd_sum)
{
can_be_resolved* resloved_predicates=new can_be_resolved[2*clauses_sum-2];
int i=0;
int clause_i=0,clause_j=0;
int clause_i_pred_k=0,clause_j_pred_k=0;
for (clause_i=0;clause_i<clauses_sum;clause_i++)
for (clause_i_pred_k=0;clause_i_pred_k<words_sum[clause_i];clause_i_pred_k++)
for (clause_j=clause_i+1;clause_j<clauses_sum;clause_j++)
for (clause_j_pred_k=0;clause_j_pred_k<words_sum[clause_j];clause_j_pred_k++)
{
if(disassembled_clauses[clause_j][clause_j_pred_k]->predicate==
disassembled_clauses[clause_i][clause_i_pred_k]->predicate &&
disassembled_clauses[clause_j][clause_j_pred_k]->negate!=
disassembled_clauses[clause_i][clause_i_pred_k]->negate)
{
resloved_predicates[i].pred=
disassembled_clauses[clause_j][clause_j_pred_k]->predicate;
resloved_predicates[i].clause_index[0]=clause_i;
resloved_predicates[i].clause_index[1]=clause_j;
resloved_predicates[i].wordage_index[0]=clause_i_pred_k;
resloved_predicates[i].wordage_index[1]=clause_j_pred_k;
i++;
}
}
*resolved_wd_sum=i;
return resloved_predicates;
}
_sigma* get_sigma_set(can_be_resolved* reslvd_preds,int *reslvd_prds_sum,int *sigma_s)
{
int i=0;
int j=0;
int clause_i=0,word_i=0;
int clause_j=0,word_j=0;
short para_sum=0,parameter_k=0;
short para_index=-1;
_sigma* sigma=new _sigma[*reslvd_prds_sum];
int sigma_i=0;
// for(int s=0;s<*reslvd_prds_sum;s++) //maybe deleted
// sigma[s].res_char='\0';//maybe deleted
for(i=0;i<*reslvd_prds_sum;i++)
{
clause_i=reslvd_preds[i].clause_index[0];
word_i=reslvd_preds[i].wordage_index[0];
clause_j=reslvd_preds[i].clause_index[1];
word_j=reslvd_preds[i].wordage_index[1];
para_sum=disassembled_clauses[clause_i][word_i]->parameters_sum;
for (parameter_k=0;parameter_k<para_sum;parameter_k++)
{
para_index=-1;
if(1==strlen(disassembled_clauses[clause_i][word_i]->parameters[parameter_k]))
para_index=0;//第parameter_i个参数为一个字符
if(1==strlen(disassembled_clauses[clause_j][word_j]->parameters[parameter_k]))
{
if(0==para_index)continue;
para_index=1;
}
switch(para_index)
{
case 0:
sigma[sigma_i].res_char=
disassembled_clauses[clause_i][word_i]->parameters[parameter_k][0];
strcpy(sigma[sigma_i].instead_char,
disassembled_clauses[clause_j][word_j]->parameters[parameter_k]);
sigma_i++;break;
case 1:
sigma[sigma_i].res_char=
disassembled_clauses[clause_j][word_j]->parameters[parameter_k][0];
strcpy(sigma[sigma_i].instead_char,
disassembled_clauses[clause_i][word_i]->parameters[parameter_k]);
sigma_i++;break;
default:break;
}
}
}
*sigma_s=sigma_i;
return sigma;
}
char* get_resolution_result(_sigma* sigma,int sigma_sm,char** p_clauses,
can_be_resolved* reslvd_preds,int reslvd_prds_sum)
{
char *result=new char[clauses_sum*CLAUSE_LENGTH];
int result_i=0;
for(int i=0;i<clauses_sum;i++)
{
int j=0;
while(p_clauses[i][j])
{
for(int k=0;k<reslvd_prds_sum;k++)
{
if(reslvd_preds[k].pred==p_clauses[i][j] &&
(reslvd_preds[k].clause_index[0]==i || reslvd_preds[k].clause_index[1]==i))
{
if(result_i>0 && '~'==result[result_i-1])
result_i--;
do
{
j++;
}while(SEPARATOR!=p_clauses[i][j] && '\0'!=p_clauses[i][j]);
if((/*0!=result_i && */SEPARATOR==p_clauses[i][j]) ||
('\0'==p_clauses[i][j] && i!=clauses_sum-1))
{
//if((0!=result_i && SEPARATOR==p_clauses[i][j])
if(0!=result_i && SEPARATOR!=result[result_i-1])
result[result_i++]=SEPARATOR;
if('\0'==p_clauses[i][j])
break;
else
j++;
}
}
}//end for(..k..)
if('\0'==p_clauses[i][j])//add
break;
for(int t=0;t<sigma_sm;t++)
{
int m=0;
if(p_clauses[i][j]==sigma[t].res_char)
{
while(sigma[t].instead_char[m])
{
result[result_i++]=sigma[t].instead_char[m];
m++;
}
j++;
}
}
result[result_i++]=p_clauses[i][j];
j++;
}//end while
//if(SEPARATOR!=result[result_i-1])
// result[result_i++]=SEPARATOR;
}//end for(int i=0;i<clauses_sum;i++)
if(SEPARATOR==result[result_i-1])
result[result_i-1]='\0';
else
result[result_i]='\0';
return result;
}
int _tmain(int argc, _TCHAR* argv[])
{
// clock_t start=clock();
// float use_time=0;
char** clauses;
short* words_sum_clause;//words_sum[] store the amount of words in every clause
can_be_resolved* rslvd_preds=NULL;//store the predicates can be resolved and
//record the clause index and the wordage index
int rslvd_prds_sum=0;//store the sum of predicates which can be resolved
_sigma* sigma_set=NULL;
int sigma_sum=0;
char* res_result=NULL;
clauses=get_clause();
cout<<endl;
cout<<"You Entered "<<clauses_sum<<" clauses waiting for resolving:\n";
for (int i=0;i<clauses_sum;i++)
cout<<"clause "<<i+1<<":\t"<<clauses[i]<<endl;
cout<<endl;
words_sum_clause=disassemble_clause(clauses);
rslvd_preds=get_resolved_predicates(words_sum_clause,&rslvd_prds_sum);
sigma_set=get_sigma_set(rslvd_preds,&rslvd_prds_sum,&sigma_sum);
cout<<"sigma={";//display the sigma
for(int m=0;m<sigma_sum;m++)
{
cout<<sigma_set[m].instead_char<<'/'<<sigma_set[m].res_char;
if(m==sigma_sum-1)
{
cout<<'}'<<endl;
break;
}
cout<<',';
}
res_result=get_resolution_result(sigma_set,sigma_sum,clauses,rslvd_preds,rslvd_prds_sum);
cout<<"The result of Resolution is :\t"<<res_result<<endl;
//free the memories have applied dynamically
delete []sigma_set;// to delete sigma[]
delete []rslvd_preds;
delete []words_sum_clause;
for(int i=0;i<clauses_sum;i++) //delete the memory applied for wordage type
for(short k=0;k<words_sum_clause[i];k++)
delete disassembled_clauses[i][k];
for (int i=0;i<clauses_sum;i++)
delete []clauses[i];//[]clauses[i]
//use_time=(clock()-start*1.0)/CLOCKS_PER_SEC;
// cout<<"The program costs "<<use_time<<"s.\n";
return 0;
}
