summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.gitignore2
-rw-r--r--Makefile22
-rw-r--r--main.cpp129
-rw-r--r--tree.cpp326
-rw-r--r--tree.h94
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);