summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abcProve.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci/abcProve.c')
-rw-r--r--src/base/abci/abcProve.c23
1 files changed, 23 insertions, 0 deletions
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index f3c1a825..c9e5bfd7 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -314,6 +314,29 @@ void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose
PRT( pString, clock() - clk );
}
+
+/**Function*************************************************************
+
+ Synopsis [Implements resynthesis for CEC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkMiterRwsat( Abc_Ntk_t * pNtk )
+{
+ Abc_Ntk_t * pNtkTemp;
+ Abc_NtkRewrite( pNtk, 0, 0, 0 );
+ pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp );
+ Abc_NtkRewrite( pNtk, 0, 0, 0 );
+ Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
+ return pNtk;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////