Expression sharing on demand in LFSC (replace definitionally equivalent child argumen...

diff --git a/proofs/lfsc_checker/expr.cpp b/proofs/lfsc_checker/expr.cpp
index 5cb774fbf0fa3d01c70adc8c84ba5c6f58ac6907..784a0ad2f2a534109f4f614e23dc2af94f2391ea 100644 (file)
--- 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;