大连海事大学智能科学与技术专业课程设计，代码福利
写法说明
该程序可处理任意函数名，任意常量名的多语句归结。且有较优秀的效率以及十分完备的封装结构，今后的进一步维护将非常方便。
实际基本结构如下：
首先采用暴力bfs的形式扩展出每一个有可能组合形成的“horn语句”（后面称之为结点）,在bfs的过程中维护一个set用来表示已经扩展完成的结点。用当前扩展结点和set中的每一个结点都进行一次组合，这样就保证了可以生成所有结点，即一定可以找到一组归结解法。
扩展过程用了很多小技巧，比如用二重hash方法将每条语句信息进行提取，通过一颗红黑树维护好每个语句的压缩信息是否已经出现，这样就保证了每一个结点都只被扩展出一次。节约了时间。同时存储所有生成边，形成一颗树结构。
之后再通过在这棵树上，从“->”结点返向dfs搜索，输出归结结果。
附代码：
//定义数字1~100表示变量，101~200表示常量，201~300表示函数名
#include<bits/stdc++.h>
using namespace std;
typedef long long int qq;
#define maxn 10005
const qq bas1 = 721;
const qq bas2 = 737;
const qq bas3 = 1767;
const qq bas4 = 797;
const qq MOD1 = 1000000007;
const qq MOD2 = 998244353;
#define mod1(x) ((x)%MOD1)
#define mod2(x) ((x)%MOD2)
map<string,int>nameid; //将名字（函数名，变量名）映射成编号
string name[300];
int numf,numx,numc; //函数和变量的个数
struct point //原子式
{
///id(a1,a2,a3...am);
int id; //该原子式函数名的标号
vector<int>a; //该原子式内所有变量的编号
void clear(){a.clear();}
pair<qq,qq> hash()
{
pair<qq,qq>ret;
ret.first=ret.second=0;
for(int i=0;i<a.size();i++)
{
ret.first = ret.first*bas1+a[i] ;
ret.second = ret.second*bas2+a[i];
}
ret.first*=id;
ret.second*=id;
return ret;
}
void output()
{
cout<<name[id];
printf("(");
for(int i=0;i<a.size();i++)
{
if(i!=0)printf(",");
cout<<name[a[i]];
}
printf(")");
}
};
operator < (point a,point b)
{
if(a.id==b.id)
{
if(a.a.size()!=b.a.size())return a.a.size()<b.a.size();
int i=0,len=a.a.size();
while(i<len-1&&a.a[i]==b.a[i])i++;
return a.a[i]<b.a[i];
}
return a.id<b.id;
}
operator == (point a,point b)
{
if(a.id!=b.id||a.a.size()!=b.a.size())return 0;
int i=0,len=a.a.size();
while(i<len&&a.a[i]==b.a[i])i++;
if(i==len)return 1;
else return 0;
}
struct horn
{
/// s <- t
int id;//结点标号从0开始
vector<point>s;
vector<point>t;
pair<qq,qq>hast;
void clear(){s.clear();t.clear();}
pair<qq,qq> hash()
{
pair<qq,qq>ret,temp;
ret.first=ret.second=0;
for(int i=0;i<s.size();i++)
{
temp=s[i].hash();
ret.first = (ret.first+temp.first)*bas1 ;
ret.second = (ret.second+temp.second)*bas2;
}
for(int i=0;i<t.size();i++)
{
temp=t[i].hash();
ret.first = (ret.first+temp.first)*bas3;
ret.second =(ret.second+temp.second)*bas4;
}
return hast=ret;
}
void leg()//范式化
{
sort(s.begin(),s.end());
sort(t.begin(),t.end());
vector<point>ns,nt; ns.clear();nt.clear();
map<pair<qq,qq>,bool>appears; appears.clear();
map<pair<qq,qq>,bool>appeart; appeart.clear();
for(int i=0;i<s.size();i++)
if(i==0||!(s[i]==s[i-1]))
{
appears[s[i].hash()]=1;
ns.push_back(s[i]);
}
for(int i=0;i<t.size();i++)
if(i==0||!(t[i]==t[i-1]))
{
appeart[t[i].hash()]=1;
nt.push_back(t[i]);
}
s.clear(),t.clear();
for(int i=0;i<ns.size();i++)
{
if(appeart.count(ns[i].hash())==0)s.push_back(ns[i]);
}
for(int i=0;i<nt.size();i++)
{
if(appears.count(nt[i].hash())==0)t.push_back(nt[i]);
}
hast=hash();
}
horn add(int x,int k)//将变量 x 赋值成常量 k
{
horn ret;ret.clear();
for(int i=0;i<s.size();i++)
{
point temp; temp.clear();
temp.id=s[i].id;
for(int j=0;j<s[i].a.size();j++)
if(s[i].a[j]==x) temp.a.push_back(k);
else temp.a.push_back(s[i].a[j]);
ret.s.push_back(temp);
}
for(int i=0;i<t.size();i++)
{
point temp; temp.clear();
temp.id=t[i].id;
for(int j=0;j<t[i].a.size();j++)
if(t[i].a[j]==x) temp.a.push_back(k);
else temp.a.push_back(t[i].a[j]);
ret.t.push_back(temp);
}
ret.leg();
return ret;
}
void output(bool op)
{
for(int i=0;i<s.size();i++)
{
if(i!=0)printf(",");
s[i].output();
}
printf(" <- ");
for(int i=0;i<t.size();i++)
{
if(i!=0)printf(",");
t[i].output();
}
if(op)printf("\n");
}
void input()
{
char temp[500]={0},c;
int len=0;
while(scanf("%c",&c))
{
if(c=='\n')break;
temp[len++]=c;
}
//AT(dog,x1) <- AT(zhangsan,x1),AT(zhangsan,train)
int now=0;
point add;
///---------------------Get_s--------------------------------
while(now<len)
{
if(temp[now]=='<'){now+=2;break;}
if(temp[now]==' '||temp[now]=='-'){now++;continue;}
string xcx; xcx.clear();
while(now<len)
{
if(temp[now]=='('||temp[now]==')'||temp[now]==','){now++;break;}
if(temp[now]==' '){now++;continue;}
xcx+=temp[now++];
}
if(xcx.length()==0){continue;}
if(temp[now-1]!='(')//是变量或常量
{
if(nameid.count(xcx)==0)
{
if(xcx[0]=='x') nameid[xcx]=++numx;
else nameid[xcx]=(++numc+200);
name[nameid[xcx]]=xcx;
}
add.a.push_back(nameid[xcx]);
}
else//是函数名
{
if(nameid.count(xcx)==0)
{
nameid[xcx]=(++numf+100);
name[nameid[xcx]]=xcx;
}
add.id=nameid[xcx];
}
if(temp[now-1]==')'){s.push_back(add);add.clear();}
}
///---------------------Get_t--------------------------------
while(now<len)
{
if(temp[now]=='<'){now+=2;break;}
if(temp[now]==' '||temp[now]=='-'){now++;continue;}
string xcx; xcx.clear();
while(now<len)
{
if(temp[now]=='('||temp[now]==')'||temp[now]==','){now++;break;}
if(temp[now]==' '){now++;continue;}
xcx+=temp[now++];
}
if(xcx.length()==0){continue;}
if(temp[now-1]!='(')//是变量或常量
{
if(nameid.count(xcx)==0)
{
if(xcx[0]=='x') nameid[xcx]=++numx;
else nameid[xcx]=(++numc+200);
name[nameid[xcx]]=xcx;
}
add.a.push_back(nameid[xcx]);
}
else//是函数名
{
if(nameid.count(xcx)==0)
{
nameid[xcx]=(++numf+100);
name[nameid[xcx]]=xcx;
}
add.id=nameid[xcx];
}
if(temp[now-1]==')'){t.push_back(add);add.clear();}
}
leg();
}
};
struct edge
{
int op;
int op2;
int u;//下一节点的标号
///op2=-1表示该节点可由u结点与op结点结合生成
///否则表示该节点可由u结点的变量变成op2常量产生
};
vector<edge>tr[100052];
vector<horn>a;
queue<horn>q;
map<pair<qq,qq>,bool>vis;
vector<horn>rule; //事实结点（叶子节点）
int trs;///结点个数
int pos[100052];//结点id为i的结点a中为a[pos[i]]
horn oi;
int e=0,root;
bool is_aim(horn x)
{
if(x.s.size()==0)return 1;
else return 0;
}
bool is_rule(horn x)
{
if(x.t.size()==0)return 1;
else return 0;
}
horn merge(horn a,horn b)
{
horn ret; ret.clear();
bool vsa[100]={0},vta[100]={0},vsb[100]={0},vtb[100]={0};
for(int i=0;i<a.s.size();i++)
for(int j=0;j<b.t.size();j++)
if(a.s[i]==b.t[j]) vsa[i]=vtb[j]=1;
for(int i=0;i<a.t.size();i++)
for(int j=0;j<b.s.size();j++)
if(a.t[i]==b.s[j]) vta[i]=vsb[j]=1;
for(int i=0;i<a.s.size();i++)
if(vsa[i]==0)ret.s.push_back(a.s[i]);
for(int i=0;i<b.s.size();i++)
if(vsb[i]==0)ret.s.push_back(b.s[i]);
for(int i=0;i<a.t.size();i++)
if(vta[i]==0)ret.t.push_back(a.t[i]);
for(int i=0;i<b.t.size();i++)
if(vtb[i]==0)ret.t.push_back(b.t[i]);
vector<point>temp;
//temp=ret.s;ret.s=ret.t;ret.t=temp;
ret.leg();
return ret;
}
void bfs(horn aim)
{
while(!q.empty())q.pop();
a.clear();
vis.clear();
trs=0;
for(int i=0;i<rule.size();i++)
{
rule[i].id=trs++;
q.push(rule[i]);
vis[rule[i].hast]=1;
}
aim.id=trs++;
q.push(aim);vis[aim.hast]=1;
while(!q.empty())
{
horn now=q.front();
//now.output();
for(int i=0;i<a.size();i++)//当前结点now与a集合中所有组合
{
horn add=merge(a[i],now);
if(vis.count(add.hast)!=0)continue;
if(add.s.size()>max(a[i].s.size(),now.s.size())
|| add.t.size()>max(a[i].t.size(),now.t.size()))continue;
vis[add.hast]=1;
edge temp1,temp2;
temp1.op2=temp2.op2=-1;
temp1.op=a[i].id; temp1.u=now.id;
temp2.op=now.id; temp2.u=a[i].id;
tr[trs].push_back(temp1);
tr[trs].push_back(temp2);
add.id=trs++;
q.push(add);
}
bool posx[105]={0};//now中出现过的变量
for(int i=0;i<now.s.size();i++)
for(int j=0;j<now.s[i].a.size();j++)
{
if(now.s[i].a[j]>numx)continue;
posx[now.s[i].a[j]]=1;
}
for(int i=0;i<now.t.size();i++)
for(int j=0;j<now.t[i].a.size();j++)
{
if(now.t[i].a[j]>100)continue;
posx[now.t[i].a[j]]=1;
}
//if(a.size()==317){printf("--- ");now.output();}
for(int i=1;i<=numx;i++)
{
if(!posx[i])continue;
for(int j=201;j<=numc+200;j++)
{
horn add=now.add(i,j);
if(vis.count(add.hast)!=0)continue;
vis[add.hast]=1;
edge temp;
temp.op2=i;
temp.op=j;
temp.u=now.id;
tr[trs].push_back(temp);
//printf("trs2=%d ",trs);
add.id=trs++;
q.push(add);
}
}
pos[now.id]=a.size();
if(is_aim(now)&&is_rule(now))root=now.id;
if(now.hast==oi.hast)e=oi.id;
a.push_back(now);
q.pop();
}
printf("xcx\n");
/*for(int i=0;i<a.size();i++) { if(is_rule(a[i])||is_aim(a[i])) { printf("%d ",i); a[i].output(); } }*/
}
stack<edge>way;
int op_num;
void dfs(int x)
{
//printf("%d ",x);
//a[pos[x]].output();
//dfs(tr[x][0].u);
if(tr[x].size()==0)
{
printf("%d.\n",op_num++);
printf("(%d) ",a[pos[x]].id);
a[pos[x]].output(1);
return;
}
if(tr[x][0].op2==-1)///说明是合并的
{
dfs(tr[x][0].u);
dfs(tr[x][0].op);
printf("%d.\n",op_num++);
printf("(%d) ",a[pos[x]].id);
a[pos[x]].output(0);
printf("(%d)+(%d) \n",tr[x][0].u,tr[x][0].op);
}
else//是转换的
{
dfs(tr[x][0].u);
printf("%d.\n",op_num++);
printf("(%d) ",a[pos[x]].id);
a[pos[x]].output(0);
printf(" (%d): ",tr[x][0].u);
cout<<name[tr[x][0].op2]<<" --> "<<name[tr[x][0].op]<<endl;
}
}
void init()
{
numf=numx=numc=0;
rule.clear();
nameid.clear();
a.clear();
while(!q.empty())q.pop();
vis.clear();
}
int main()
{
init();
//freopen("in3.txt","r",stdin);
//freopen("out2.txt","w",stdout);
int T,cnt=1; ///cnt 为 horn 语句个数
printf("请输入事实个数:");
scanf("%d",&T);printf(" %d\n",T);getchar();
while(T--)
{
horn temp;temp.clear();
temp.input();
temp.output(1);
rule.push_back(temp);
cnt++;
}
printf("自动识别：\n变量个数：%d\n常量个数：%d\n函数个数：%d\n",numx,numc,numf);
printf("请输入目标个数:");
scanf("%d",&T);printf(" %d\n",T);getchar();
int aim_num=1;
while(T--)
{
for(int i=0;i<100052;i++)tr[i].clear();
horn temp; temp.clear();
temp.input();
oi=temp;
temp.output(1);
trs=0;
op_num=1;
bfs(temp);///广搜出图
dfs(root);///深搜出路径
//printf("归结完成\n");
while(1)getchar();
}
return 0;
}
/* 程序功能： 输入： n表示有n个规则或事实 接下来n行表示每一个规则或事实 如： AT(zhangsan,x),AT(pp,x) -> AT(dog,x) AT(zhangsan,train) <- 接下来输入m 表示有m个目标： 如： <-AT(dog,train) 输入样例： 样例一： 2 AT(dog,x1)<- AT(zhangsan,x1) AT(zhangsan,train)<- 1 <-AT(dog,train) 样例二： 3 Father(Bob,Allan)<- Brother(x2,x3)<-Father(x1,x2),Father(x1,x3) Father(Bob,Nick)<- 1 <-Brother(Allan,Nick) */
京公网安备 11010502036488号