1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
#include <iostream>
#include <string>
#include <vector>
#include <map>
#include <queue>
#include <cassert>
#include "tree.h"
using namespace std;
struct Axiom{
Tree from,to;
};
ostream& operator<<(ostream &os,const Axiom &ax){
return os<<ax.from<<" -> "<<ax.to;
}
void parseAxiom(vector<Axiom> &dst,const string &expr){
size_t idx=expr.find('=');
bool twoway=true;
if(idx==string::npos){
idx=expr.find('>');
assert(idx!=string::npos);
twoway=false;
}
assert(expr.find('=',idx+1)==string::npos);
assert(expr.find('>',idx+1)==string::npos);
string from=expr.substr(0,idx),to=expr.substr(idx+1);
dst.push_back({Tree(from),Tree(to)});
if(twoway)dst.push_back({Tree(to),Tree(from)});
}
vector<Axiom> importAxioms(const vector<string> &list){
vector<Axiom> axioms;
for(const string &str : list){
parseAxiom(axioms,str);
}
return axioms;
}
using Heuristic = int (*)(const Tree&);
int heuristic(const Tree &tree){
return tree.nleaves();
}
template <Heuristic F>
struct AscendingCompare{
bool operator()(const Tree &a,const Tree &b) const {
return F(a)>F(b);
}
};
template <Heuristic F>
vector<Tree>* deduceEq(const vector<Axiom> &axioms,const Tree &startTree,const Tree &target){
priority_queue<Tree,vector<Tree>,AscendingCompare<F>> pqu;
map<Tree,Tree,TreeCompare> parentMap;
pqu.push(startTree);
Tree current;
while(true){
if(pqu.size()==0)return nullptr;
current=pqu.top();
pqu.pop();
cerr<<"current = "<<current;
{
auto it=parentMap.find(current);
if(it!=parentMap.end())cout<<" parent = "<<it->second<<endl;
else cout<<endl;
}
if(current.matches(target))break;
for(const Axiom &ax : axioms){
vector<Tree> nexts=current.replace(ax.from,ax.to);
// cerr<<" ax = "<<ax<<endl;
// cerr<<" nexts.size() = "<<nexts.size()<<endl;
for(const Tree &t : nexts){
auto it=parentMap.find(t);
if(it==parentMap.end()&&t.compare(startTree)!=0){
parentMap.emplace(t,current);
pqu.push(t);
// cerr<<" Pushing "<<t<<endl;
} else {
// cerr<<" Skipping "<<t<<" because already seen"<<endl;
}
}
}
}
vector<Tree> *v=new vector<Tree>();
Tree *t=¤t;
while(true){
// cerr<<"*t = "<<*t<<endl;
v->push_back(*t);
auto it=parentMap.find(*t);
if(it==parentMap.end())break;
t=&it->second;
}
return v;
}
int main(){
const vector<Axiom> axioms=importAxioms({
// "([1]*[2])>([2]*[1])",
// "(([1]*[2])*[3])=([1]*([2]*[3]))",
// "([1]*([1]*[2]))=[1]",
// "(([2]*[1])*[1])=[1]",
// "[1]=([1]*[1])",
// "(([1]*[2])*[3])=(([2]*[3])*[1])",
"[1]=[2]",
});
const Tree t_from("(1*2)"),t_to("(2*1)");
for(const Axiom &ax : axioms)cout<<ax<<endl;
cout<<endl;
vector<Tree> *res=deduceEq<heuristic>(axioms,t_from,t_to);
if(res==nullptr){
cout<<"No deduction"<<endl;
} else {
cout<<"Deduction:"<<endl;
for(int i=res->size()-1;i>=0;i--){
cout<<res->at(i)<<endl;
}
}
}
|
