diff options
| -rw-r--r-- | main.cpp | 37 | ||||
| -rw-r--r-- | tree.cpp | 46 | ||||
| -rw-r--r-- | tree.h | 12 |
3 files changed, 83 insertions, 12 deletions
@@ -42,9 +42,8 @@ vector<Axiom> importAxioms(const vector<string> &list){ using Heuristic = int (*)(const Tree&); -int heuristic(const Tree &tree){ - return tree.nleaves(); -} +int heuristic_nleaves(const Tree &tree){return tree.nleaves();} +int heuristic_height(const Tree &tree){return tree.height();} template <Heuristic F> struct AscendingCompare{ @@ -99,25 +98,43 @@ vector<Tree>* deduceEq(const vector<Axiom> &axioms,const Tree &startTree,const T } +void test_func(){ + Tree from("([2]*([2]*1))"),to("10"); + Tree subj("(([1]*1)*[1])"); + + /*unordered_set<Variable> temps=to.collectTemporaries(); + for(Variable v : temps){ + cout<<v<<endl; + }*/ + + vector<Tree> res=subj.replace(from,to); + for(const Tree &t : res){ + cout<<t<<endl; + } +} + int main(){ + test_func(); + return 0; + const vector<Axiom> axioms=importAxioms({ - // "([1]*[2])>([2]*[1])", - // "(([1]*[2])*[3])=([1]*([2]*[3]))", + // "([1]*[2])>([2]*[1])", // Commutativity + // "(([1]*[2])*[3])=([1]*([2]*[3]))", // Associativity - // "([1]*([1]*[2]))=[1]", - // "(([2]*[1])*[1])=[1]", + "([1]*([1]*[2]))=[1]", // Onno's 1=2 axioms + "(([2]*[1])*[1])=[1]", // "[1]=([1]*[1])", // "(([1]*[2])*[3])=(([2]*[3])*[1])", - "[1]=[2]", + // "[1]=[2]", }); - const Tree t_from("(1*2)"),t_to("(2*1)"); + const Tree t_from("1"),t_to("2"); for(const Axiom &ax : axioms)cout<<ax<<endl; cout<<endl; - vector<Tree> *res=deduceEq<heuristic>(axioms,t_from,t_to); + vector<Tree> *res=deduceEq<heuristic_nleaves>(axioms,t_from,t_to); if(res==nullptr){ cout<<"No deduction"<<endl; } else { @@ -11,6 +11,8 @@ int uniqid(){ } +Variable::Variable(int id):id(id){} + bool Variable::isOperator() const { return id==0; } @@ -167,6 +169,15 @@ Tree::Node* Tree::Node::apply(const Assign &as) const { return n; } +void Tree::Node::collectTemporaries(unordered_set<Variable> &accum) const { + if(v.isOperator()){ + left->collectTemporaries(accum); + right->collectTemporaries(accum); + } else { + accum.insert(v); + } +} + int Tree::Node::nleaves() const { if(v.isOperator()){ return left->nleaves()+right->nleaves(); @@ -175,6 +186,11 @@ int Tree::Node::nleaves() const { } } +int Tree::Node::height() const { + if(v.isOperator())return max(left->height(),right->height()); + 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; @@ -283,9 +299,27 @@ bool Tree::matches(const Tree &pat) const { } } +void Tree::refreshUnassigned(const Tree &repl,Assign &as) const { + unordered_set<Variable> temps=repl.collectTemporaries(); + // cerr<<"rU:"<<endl; + for(Variable v : temps){ + // cerr<<" v = "<<v<<endl; + if(v.isTemp()&&as.find(v)==as.end()){ + int id=uniqid(); + as.emplace(v,Node(id)); + // cerr<<" emplace("<<v<<","<<Node(id)<<")"<<endl; + } + } +} + void Tree::replace(Node *subj,const Tree &pat,const Tree &repl,vector<Tree> &accum){ Assign *as=subj->match(*pat.root); if(as){ + refreshUnassigned(repl,*as); + cerr<<"replace("<<*subj<<","<<pat<<","<<repl<<"); as:"<<endl; + for(const pair<Variable,Node> &p : *as){ + cerr<<" "<<p.first<<" -> "<<p.second<<endl; + } Node *res=repl.root->apply(*as); Node backup=*subj; *subj=*res; @@ -307,11 +341,23 @@ vector<Tree> Tree::replace(const Tree &pat,const Tree &repl){ return res; } +unordered_set<Variable> Tree::collectTemporaries() const { + assert(root); + unordered_set<Variable> temps; + root->collectTemporaries(temps); + return temps; +} + int Tree::nleaves() const { assert(root); return root->nleaves(); } +int Tree::height() const { + assert(root); + return root->height(); +} + int Tree::compare(const Tree &other) const { assert(root&&other.root); return root->compare(*other.root); @@ -4,6 +4,7 @@ #include <string> #include <vector> #include <unordered_map> +#include <unordered_set> using namespace std; @@ -13,7 +14,7 @@ int uniqid(); struct Variable{ int id; - Variable(int id):id(id){} + Variable(int id); bool isOperator() const; bool isFixed() const; @@ -25,6 +26,8 @@ struct Variable{ operator int() const; }; +ostream& operator<<(ostream &os,const Variable &v); + namespace std { template <> struct hash<Variable>{ @@ -50,10 +53,11 @@ class Tree{ Node& operator=(const Node &other); Assign* match(const Node &pat,Assign *accum=nullptr) const; - Node* apply(const Assign &as) const; + void collectTemporaries(unordered_set<Variable> &accum) const; int nleaves() const; + int height() const; int compare(const Node &other) const; }; @@ -65,6 +69,8 @@ class Tree{ void replace(Node *subj,const Tree &pat,const Tree &repl,vector<Tree> &accum); + void refreshUnassigned(const Tree &repl,Assign &as) const; + public: Tree(); // Creates invalid tree Tree(const string &expr); @@ -75,8 +81,10 @@ public: bool matches(const Tree &pat) const; vector<Tree> replace(const Tree &pat,const Tree &repl); + unordered_set<Variable> collectTemporaries() const; int nleaves() const; + int height() const; int compare(const Tree &other) const; |