From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 15 Aug 2016 21:30:07 +0000 (-0500)
Subject: Expression sharing on demand in LFSC (replace definitionally equivalent child argumen... 
X-Git-Tag: cvc5-1.0.0~6040^2~3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=20fc32c0c4a2518673e1cbaa0afb3c4fb284ffe6;p=cvc5.git

Expression sharing on demand in LFSC (replace definitionally equivalent child arguments after successful comparison).
---

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;