From b949436f4c99157397e16b23c3693fb5a99bd557 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sat, 11 Jul 2015 16:49:06 -0700
Subject: Adding new Python API 'is_func_iso'.

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

(limited to 'src/proof')

diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index 805a5d73..a0b92b52 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -197,6 +197,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_ManVerifySimple( Gia_Man_t * p );
 /*=== cecChoice.c ==========================================================*/
 extern Gia_Man_t *   Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars );
 /*=== cecCorr.c ==========================================================*/
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index 1465a721..77a6ed4a 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -413,6 +413,27 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Simple SAT run to check equivalence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManVerifySimple( Gia_Man_t * p )
+{
+    Cec_ParCec_t ParsCec, * pPars = &ParsCec;
+    Cec_ManCecSetDefaultParams( pPars );
+    pPars->fSilent = 1;
+    assert( Gia_ManCoNum(p) == 2 );
+    assert( Gia_ManRegNum(p) == 0 );
+    return Cec_ManVerify( p, pPars );
+}
+
 /**Function*************************************************************
 
   Synopsis    [New CEC engine applied to two circuits.]
-- 
cgit v1.2.3