summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--main.cpp23
-rw-r--r--tree.cpp8
2 files changed, 17 insertions, 14 deletions
diff --git a/main.cpp b/main.cpp
index f4fe639..781f72e 100644
--- a/main.cpp
+++ b/main.cpp
@@ -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");
diff --git a/tree.cpp b/tree.cpp
index a259e9b..c069904 100644
--- a/tree.cpp
+++ b/tree.cpp
@@ -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;