diff options
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | Makefile | 22 | ||||
| -rw-r--r-- | main.cpp | 129 | ||||
| -rw-r--r-- | tree.cpp | 326 | ||||
| -rw-r--r-- | tree.h | 94 |
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=¤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; + } + } +} 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; +} @@ -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); |