From c54485386cc89fcc233debafee4605a7b104351b Mon Sep 17 00:00:00 2001 From: tomsmeding Date: Sun, 29 Jan 2017 19:05:20 +0100 Subject: Changes --- main.cpp | 37 +++++++++++++++++++++++++++---------- 1 file changed, 27 insertions(+), 10 deletions(-) (limited to 'main.cpp') diff --git a/main.cpp b/main.cpp index 2b7e748..f4fe639 100644 --- a/main.cpp +++ b/main.cpp @@ -42,9 +42,8 @@ vector importAxioms(const vector &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 struct AscendingCompare{ @@ -99,25 +98,43 @@ vector* deduceEq(const vector &axioms,const Tree &startTree,const T } +void test_func(){ + Tree from("([2]*([2]*1))"),to("10"); + Tree subj("(([1]*1)*[1])"); + + /*unordered_set temps=to.collectTemporaries(); + for(Variable v : temps){ + cout< res=subj.replace(from,to); + for(const Tree &t : res){ + cout< 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< *res=deduceEq(axioms,t_from,t_to); + vector *res=deduceEq(axioms,t_from,t_to); if(res==nullptr){ cout<<"No deduction"<