From 8a1c28bf0f37cdf35f007b932451418eaf053352 Mon Sep 17 00:00:00 2001
From: Carmine50 <carmine.rizzi@hotmail.it>
Date: Sat, 21 Dec 2024 20:15:40 +0100
Subject: [PATCH] [CEC][SimGen][LUT mapping] Adding option to consider an
 already mapped circuit before executing SimGen

---
 src/proof/cec/cecSatG2.c | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index ab7dae988..1e058c29c 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -4304,13 +4304,22 @@ Gia_Man_t * Cec_SimGenRun( Gia_Man_t * p, Cec_ParSimGen_t * pPars ){
     
     Cec4_Man_t * pManSim;  
     int i, k, iFan;
-    
+    Gia_Man_t * pMapped;
 
-    // apply technology mapping
-    If_Par_t IfPars, * pIfPars = &IfPars;
-    Gia_ManSetIfParsDefault( pIfPars );
-    pIfPars->nLutSize = 6;
-    Gia_Man_t * pMapped = Gia_ManPerformMapping( p, pIfPars );
+    if (!Gia_ManHasMapping(p)){
+      // apply technology mapping if not already done
+      If_Par_t IfPars, * pIfPars = &IfPars;
+      Gia_ManSetIfParsDefault( pIfPars );
+      pIfPars->nLutSize = 6;
+      pMapped = Gia_ManPerformMapping( p, pIfPars );
+      if(pPars->fVerbose)
+        printf("Performing LUT-mapping\n");
+    } else {
+      pMapped = Gia_ManDup( p );
+      Gia_ManDupMapping( pMapped, p );
+      if(pPars->fVerbose)
+        printf("Using already mapped network\n");
+    }
     pManSim = Cec4_ManCreate( pMapped, pPars->pCECPars );
 
     Cec_DeriveSOPs( pMapped );