diff options
| -rw-r--r-- | main.cpp | 23 | ||||
| -rw-r--r-- | tree.cpp | 8 |
2 files changed, 17 insertions, 14 deletions
@@ -62,12 +62,12 @@ vector<Tree>* deduceEq(const vector<Axiom> &axioms,const Tree &startTree,const T 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; - } + // cerr<<"current = "<<current; + // { + // auto it=parentMap.find(current); + // if(it!=parentMap.end())cerr<<" parent = "<<it->second<<endl; + // else cerr<<endl; + // } if(current.matches(target))break; for(const Axiom &ax : axioms){ vector<Tree> nexts=current.replace(ax.from,ax.to); @@ -114,20 +114,23 @@ void test_func(){ } int main(){ - test_func(); - return 0; + /*test_func(); + return 0;*/ const vector<Axiom> axioms=importAxioms({ // "([1]*[2])>([2]*[1])", // Commutativity // "(([1]*[2])*[3])=([1]*([2]*[3]))", // Associativity - "([1]*([1]*[2]))=[1]", // Onno's 1=2 axioms - "(([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]=([1]*([1]*([1]*[2])))", // Daan's 1=2 axioms + "(([2]*[1])*[1])=[1]", }); const Tree t_from("1"),t_to("2"); @@ -316,10 +316,10 @@ void Tree::replace(Node *subj,const Tree &pat,const Tree &repl,vector<Tree> &acc 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; - } + // 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; |