Initial

5 files changed, 573 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..df0f618
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+*.o
+boog
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..e6d626b
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,22 @@
+CXX = g++
+CXXFLAGS = -Wall -Wextra -std=c++11 -g -fwrapv
+LDFLAGS =
+TARGET = boog
+
+.PHONY: all clean remake
+
+all: $(TARGET)
+
+clean:
+	rm -f *.o $(TARGET)
+	rm -rf *.dSYM
+
+remake: clean
+	make all
+
+
+$(TARGET): $(patsubst %.cpp,%.o,$(wildcard *.cpp))
+	$(CXX) $^ -o $@ $(LDFLAGS)
+
+%.o: %.cpp $(wildcard *.h)
+	$(CXX) $(CXXFLAGS) -c -o $@ $<
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;
+		}
+	}
+}
diff --git a/tree.cpp b/tree.cpp
new file mode 100644
index 0000000..8d677db
--- /dev/null
+++ b/tree.cpp
@@ -0,0 +1,326 @@
+#include <cctype>
+#include <cassert>
+#include "tree.h"
+
+using namespace std;
+
+
+int uniqid(){
+	static int id=10;
+	return id++;
+}
+
+
+bool Variable::isOperator() const {
+	return id==0;
+}
+
+bool Variable::isFixed() const {
+	return id<0;
+}
+
+bool Variable::isTemp() const {
+	return id>0;
+}
+
+bool Variable::operator==(Variable v) const {
+	return id==v.id;
+}
+
+bool Variable::operator!=(Variable v) const {
+	return id!=v.id;
+}
+
+Variable::operator int() const {
+	return id;
+}
+
+namespace std {
+	size_t hash<Variable>::operator()(Variable v) const {
+		return inthasher(v.id);
+	}
+}
+
+ostream& operator<<(ostream &os,const Variable &v){
+	assert(!v.isOperator());
+	if(v.isFixed())return os<<-v.id;
+	else return os<<'['<<v.id<<']';
+}
+
+
+Tree::Node::Node(Variable v):v(v),left(nullptr),right(nullptr){}
+
+Tree::Node::Node(Node *left,Node *right):v(0),left(left),right(right){
+	assert(left&&right);
+}
+
+Tree::Node::Node(const Node &other):v(other.v){
+	if(v.isOperator()){
+		assert(other.left&&other.right);
+		left=new Node(*other.left);
+		right=new Node(*other.right);
+	} else {
+		assert(!other.left&&!other.right);
+		left=right=nullptr;
+	}
+}
+
+Tree::Node::~Node(){
+	if(left){
+		assert(right);
+		delete left;
+		delete right;
+	} else {
+		assert(!right);
+	}
+}
+
+Tree::Node& Tree::Node::operator=(const Node &other){
+	v=other.v;
+	if(left){
+		assert(right);
+		delete left;
+		delete right;
+	} else {
+		assert(!right);
+	}
+	if(other.left){
+		assert(other.right);
+		left=new Node(*other.left);
+		right=new Node(*other.right);
+	} else {
+		assert(!other.right);
+		left=right=nullptr;
+	}
+	return *this;
+}
+
+Tree::Assign* Tree::Node::match(const Node &pat,Assign *accum) const {
+	//cerr<<"Matching "<<*this<<" and "<<pat<<endl;
+	if(pat.v.isOperator()&&!v.isOperator()){
+		if(v.isTemp()){
+			//cerr<<"  -> ok, L="<<__LINE__<<endl;
+			return accum;
+		}
+		//cerr<<"  -> null, L="<<__LINE__<<endl;
+		if(accum)delete accum;
+		return nullptr;
+	}
+	if(pat.v.isOperator()){
+		assert(v.isOperator());
+		assert(left&&right&&pat.left&&pat.right);
+		Assign *as=left->match(*pat.left,accum);
+		if(!as){
+			//cerr<<"  -> null, L="<<__LINE__<<endl;
+			return nullptr;
+		}
+		Assign *right_res=right->match(*pat.right,as);
+		if(!right_res){
+			//cerr<<"  -> null, L="<<__LINE__<<endl;
+			return nullptr;
+		}
+		return as;
+	}
+	assert(!pat.left&&!pat.right);
+	if(pat.v.isFixed()){
+		if(v.isOperator()||(v.isFixed()&&pat.v!=v)){
+			//cerr<<"  -> null, L="<<__LINE__<<endl;
+			if(accum)delete accum;
+			return nullptr;
+		}
+		//cerr<<"  -> ok, L="<<__LINE__<<endl;
+		if(accum)return accum;
+		else return new Assign();
+	}
+	if(!accum){
+		accum=new Assign();
+		accum->emplace(pat.v,*this);
+		//cerr<<"  -> ok, L="<<__LINE__<<endl;
+		return accum;
+	}
+	auto it=accum->find(pat.v);
+	if(it==accum->end()){
+		accum->emplace(pat.v,*this);
+		//cerr<<"  -> ok, L="<<__LINE__<<endl;
+		return accum;
+	}
+	if(it->second==*this){
+		//cerr<<"  -> ok, L="<<__LINE__<<endl;
+		return accum;
+	} else {
+		//cerr<<"  -> null, L="<<__LINE__<<endl;
+		delete accum;
+		return nullptr;
+	}
+}
+
+Tree::Node* Tree::Node::apply(const Assign &as) const {
+	Node *n=new Node(v);
+	if(v.isOperator()){
+		n->left=left->apply(as);
+		n->right=right->apply(as);
+	} else {
+		auto it=as.find(v);
+		if(it==as.end())n->v=v;
+		else *n=it->second;
+	}
+	return n;
+}
+
+int Tree::Node::nleaves() const {
+	if(v.isOperator()){
+		return left->nleaves()+right->nleaves();
+	} else {
+		return 1;
+	}
+}
+
+int Tree::Node::compare(const Node &other) const {
+	if(v.isTemp()&&other.v.isTemp())return 0;
+	if(v<other.v)return -1;
+	if(v>other.v)return 1;
+	if(!v.isOperator())return 0;
+	int c=left->compare(*other.left);
+	if(c!=0)return c;
+	return right->compare(*other.right);
+}
+
+bool operator==(const Tree::Node &a,const Tree::Node &b){
+	if(a.v.isTemp()&&b.v.isTemp())return true;
+	if(a.v!=b.v)return false;
+	if(!a.v.isOperator())return true;
+	return *a.left==*b.left&&*a.right==*b.right;
+}
+
+bool operator!=(const Tree::Node &a,const Tree::Node &b){
+	return !(a==b);
+}
+
+ostream& operator<<(ostream &os,const Tree::Node &node){
+	if(node.v.isOperator()){
+		return os<<'('<<*node.left<<'*'<<*node.right<<')';
+	} else {
+		return os<<node.v;
+	}
+}
+
+Tree::Node* Tree::parseTerm(const string &expr,size_t &idx){
+	if(expr[idx]=='('){
+		idx++;
+		Node *node=parseNode(expr,idx);
+		assert(expr[idx]==')');
+		idx++;
+		return node;
+	} else if(expr[idx]=='['){
+		idx++;
+		char *endp;
+		const char *data=expr.data();
+		assert(isdigit(data[idx]));
+		Variable v=strtol(data+idx,&endp,10);
+		assert(endp-(data+idx)>0);
+		idx=endp-data;
+		assert(data[idx]==']');
+		idx++;
+		assert(!v.isOperator());
+		return new Node(v);
+	} else {
+		char *endp;
+		const char *data=expr.data();
+		assert(isdigit(data[idx]));
+		Variable v=-strtol(data+idx,&endp,10);
+		assert(endp-(data+idx)>0);
+		idx=endp-data;
+		assert(!v.isOperator());
+		return new Node(v);
+	}
+}
+
+Tree::Node* Tree::parseNode(const string &expr,size_t &idx){
+	Node *l=parseTerm(expr,idx);
+	if(idx==expr.size())return l;
+	assert(expr[idx]=='*');
+	idx++;
+	Node *r=parseTerm(expr,idx);
+	assert(idx==expr.size()||expr[idx]==')');
+	return new Node(l,r);
+}
+
+Tree::Tree():root(nullptr){}
+
+Tree::Tree(const string &expr){
+	size_t idx=0;
+	root=parseNode(expr,idx);
+}
+
+Tree::Tree(const Tree &other){
+	if(root)delete root;
+	if(other.root){
+		root=new Node(*other.root);
+	} else {
+		root=nullptr;
+	}
+}
+
+Tree::~Tree(){
+	if(root)delete root;
+}
+
+Tree& Tree::operator=(const Tree &other){
+	assert(other.root);
+	if(root)delete root;
+	root=new Node(*other.root);
+	return *this;
+}
+
+bool Tree::matches(const Tree &pat) const {
+	assert(root&&pat.root);
+	Assign *as=root->match(*pat.root);
+	if(as){
+		delete as;
+		return true;
+	} else {
+		return false;
+	}
+}
+
+void Tree::replace(Node *subj,const Tree &pat,const Tree &repl,vector<Tree> &accum){
+	Assign *as=subj->match(*pat.root);
+	if(as){
+		Node *res=repl.root->apply(*as);
+		Node backup=*subj;
+		*subj=*res;
+		accum.push_back(*this);
+		*subj=backup;
+		delete res;
+		delete as;
+	}
+	if(subj->left){
+		replace(subj->left,pat,repl,accum);
+		replace(subj->right,pat,repl,accum);
+	}
+}
+
+vector<Tree> Tree::replace(const Tree &pat,const Tree &repl){
+	assert(root&&pat.root);
+	vector<Tree> res;
+	replace(root,pat,repl,res);
+	return res;
+}
+
+int Tree::nleaves() const {
+	assert(root);
+	return root->nleaves();
+}
+
+int Tree::compare(const Tree &other) const {
+	assert(root&&other.root);
+	return root->compare(*other.root);
+}
+
+bool TreeCompare::operator()(const Tree &a,const Tree &b) const {
+	return a.compare(b)<0;
+}
+
+ostream& operator<<(ostream &os,const Tree &tree){
+	return os<<*tree.root;
+}
diff --git a/tree.h b/tree.h
new file mode 100644
index 0000000..7d8cf15
--- /dev/null
+++ b/tree.h
@@ -0,0 +1,94 @@
+#pragma once
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <unordered_map>
+
+using namespace std;
+
+
+int uniqid();
+
+struct Variable{
+	int id;
+
+	Variable(int id):id(id){}
+
+	bool isOperator() const;
+	bool isFixed() const;
+	bool isTemp() const;
+
+	bool operator==(Variable v) const;
+	bool operator!=(Variable v) const;
+
+	operator int() const;
+};
+
+namespace std {
+	template <>
+	struct hash<Variable>{
+		hash<int> inthasher;
+		size_t operator()(Variable v) const;
+	};
+}
+
+class Tree{
+	struct Node;
+
+	using Assign = unordered_map<Variable,Node>;
+
+	struct Node{
+		Variable v;
+		Node *left,*right;
+
+		explicit Node(Variable v);
+		Node(Node *left,Node *right);
+		Node(const Node &other);
+		~Node();
+
+		Node& operator=(const Node &other);
+
+		Assign* match(const Node &pat,Assign *accum=nullptr) const;
+
+		Node* apply(const Assign &as) const;
+
+		int nleaves() const;
+
+		int compare(const Node &other) const;
+	};
+
+	Node *root=nullptr;
+
+	static Node* parseTerm(const string &expr,size_t &idx);
+	static Node* parseNode(const string &expr,size_t &idx);
+
+	void replace(Node *subj,const Tree &pat,const Tree &repl,vector<Tree> &accum);
+
+public:
+	Tree(); // Creates invalid tree
+	Tree(const string &expr);
+	Tree(const Tree &other);
+	~Tree();
+
+	Tree& operator=(const Tree &other);
+
+	bool matches(const Tree &pat) const;
+	vector<Tree> replace(const Tree &pat,const Tree &repl);
+
+	int nleaves() const;
+
+	int compare(const Tree &other) const;
+
+	friend ostream& operator<<(ostream &os,const Variable &v);
+	friend ostream& operator<<(ostream &os,const Node &node);
+	friend ostream& operator<<(ostream &os,const Tree &tree);
+	friend bool operator==(const Node &a,const Node &b);
+	friend bool operator!=(const Node &a,const Node &b);
+};
+
+struct TreeCompare{
+	bool operator()(const Tree &a,const Tree &b) const;
+};
+
+ostream& operator<<(ostream &os,const Tree &tree);