From d86e8d9ed858d2ab081fe1ca5bfacdfb7aa28018 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 6 Mar 2022 00:09:35 -0800
Subject: Experiments with word-level data structures.

---
 src/proof/cec/cec.h    |  1 +
 src/proof/cec/cecCec.c | 15 +++++++++++++++
 2 files changed, 16 insertions(+)

(limited to 'src/proof')

diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index 7c101570..40aa9799 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -206,6 +206,7 @@ struct Cec_ParSeq_t_
 /*=== cecCec.c ==========================================================*/
 extern int           Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars );
 extern int           Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose );
+extern int           Cec_ManVerifyTwoInv( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose );
 extern int           Cec_ManVerifySimple( Gia_Man_t * p );
 /*=== cecChoice.c ==========================================================*/
 extern Gia_Man_t *   Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars );
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index cfa07ff8..f6a1ab52 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -465,6 +465,21 @@ int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose )
     Gia_ManStop( pMiter );
     return RetValue;
 }
+int Cec_ManVerifyTwoInv( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose )
+{
+    Cec_ParCec_t ParsCec, * pPars = &ParsCec;
+    Gia_Man_t * pMiter;
+    int RetValue;
+    Cec_ManCecSetDefaultParams( pPars );
+    pPars->fVerbose = fVerbose;
+    pMiter = Gia_ManMiterInverse( p0, p1, 1, pPars->fVerbose );
+    if ( pMiter == NULL )
+        return -1;
+    RetValue = Cec_ManVerify( pMiter, pPars );
+    p0->pCexComb = pMiter->pCexComb; pMiter->pCexComb = NULL;
+    Gia_ManStop( pMiter );
+    return RetValue;
+}
 
 /**Function*************************************************************
 
-- 
cgit v1.2.3