diff options
Diffstat (limited to 'proofs/lfsc_checker/expr.cpp')
-rw-r--r-- | proofs/lfsc_checker/expr.cpp | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp index 5cb774fbf..784a0ad2f 100644 --- a/proofs/lfsc_checker/expr.cpp +++ b/proofs/lfsc_checker/expr.cpp @@ -577,8 +577,21 @@ bool Expr::defeq(Expr *e) { { int counter = 0; while( e1->kids[counter] ){ - if( !e2->kids[counter] || !e1->kids[counter]->defeq( e2->kids[counter] ) ) - return false; + if( e1->kids[counter]!=e2->kids[counter] ){ + if( !e2->kids[counter] || !e1->kids[counter]->defeq( e2->kids[counter] ) ) + return false; + //--- optimization : replace child with equivalent pointer if was defeq + if( e1->kids[counter]<e2->kids[counter] ){ + e1->kids[counter]->dec(); + e2->kids[counter]->inc(); + e1->kids[counter] = e2->kids[counter]; + }else{ + e2->kids[counter]->dec(); + e1->kids[counter]->inc(); + e2->kids[counter] = e1->kids[counter]; + } + } + //--- counter++; } return e2->kids[counter]==NULL; |