1 files changed, 129 insertions, 0 deletions
diff --git a/main.cpp b/main.cpp
new file mode 100644
index 0000000..2b7e748
--- /dev/null
+++ b/main.cpp
@@ -0,0 +1,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=&current;
+	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;
+		}
+	}
+}