diff options
Diffstat (limited to 'main.cpp')
| -rw-r--r-- | main.cpp | 23 |
1 files changed, 13 insertions, 10 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"); |