Various changes to enable better CNF generation.

4 files changed, 66 insertions, 68 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 426660a4..8872ef83 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1175,6 +1175,9 @@ extern void                Gia_MmStepStop( Gia_MmStep_t * p, int fVerbose );
 extern char *              Gia_MmStepEntryFetch( Gia_MmStep_t * p, int nBytes );
 extern void                Gia_MmStepEntryRecycle( Gia_MmStep_t * p, char * pEntry, int nBytes );
 extern int                 Gia_MmStepReadMemUsage( Gia_MmStep_t * p );
+/*=== giaMf.c ===========================================================*/
+extern void                Mf_ManSetDefaultPars( Jf_Par_t * pPars );
+extern Gia_Man_t *         Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars );
 /*=== giaMini.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManReadMiniAig( char * pFileName );
 extern void                Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName );
diff --git a/src/aig/gia/giaIso3.c b/src/aig/gia/giaIso3.c
index 18430a6c..a88a0569 100644
--- a/src/aig/gia/giaIso3.c
+++ b/src/aig/gia/giaIso3.c
@@ -34,74 +34,6 @@ static unsigned Iso_Compl[2] = { 0x8ba63e50, 0x14d87f02 }; // non-compl, compl
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of unique entries.]
-
-  Description []
-               
-  SideEffects [] 
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline unsigned Vec_IntUniqueHashKey( unsigned char * pStr, int nChars )
-{
-    static unsigned s_BigPrimes[4] = {12582917, 25165843, 50331653, 100663319};
-    unsigned Key = 0; int c;
-    for ( c = 0; c < nChars; c++ )
-        Key += (unsigned)pStr[c] * s_BigPrimes[c & 3];
-    return Key;
-}
-static inline int * Vec_IntUniqueLookup( Vec_Int_t * vData, int i, int nIntSize, int * pNexts, int * pStart )
-{
-    int * pData = Vec_IntEntryP( vData, i*nIntSize );
-    for ( ; *pStart != -1; pStart = pNexts + *pStart )
-        if ( !memcmp( pData, Vec_IntEntryP(vData, *pStart*nIntSize), sizeof(int) * nIntSize ) )
-            return pStart;
-    return pStart;
-}
-static inline int Vec_IntUniqueCount( Vec_Int_t * vData, int nIntSize, Vec_Int_t ** pvMap )
-{
-    int nEntries  = Vec_IntSize(vData) / nIntSize;
-    int TableMask = (1 << Abc_Base2Log(nEntries)) - 1;
-    int * pTable  = ABC_FALLOC( int, TableMask+1 );
-    int * pNexts  = ABC_FALLOC( int, TableMask+1 );
-    int * pClass  = ABC_ALLOC( int, nEntries );
-    int i, Key, * pEnt, nUnique = 0;
-    assert( nEntries * nIntSize == Vec_IntSize(vData) );
-    for ( i = 0; i < nEntries; i++ )
-    {
-        pEnt = Vec_IntEntryP( vData, i*nIntSize );
-        Key  = TableMask & Vec_IntUniqueHashKey( (unsigned char *)pEnt, 4*nIntSize );
-        pEnt = Vec_IntUniqueLookup( vData, i, nIntSize, pNexts, pTable+Key );
-        if ( *pEnt == -1 )
-            *pEnt = i, nUnique++;
-        pClass[i] = *pEnt;
-    }
-    ABC_FREE( pTable );
-    ABC_FREE( pNexts );
-    if ( pvMap )
-        *pvMap = Vec_IntAllocArray( pClass, nEntries );
-    else
-        ABC_FREE( pClass );
-    return nUnique;
-}
-static inline Vec_Int_t * Vec_IntUniqifyHash( Vec_Int_t * vData, int nIntSize )
-{
-    Vec_Int_t * vMap, * vUnique;
-    int i, Ent, nUnique = Vec_IntUniqueCount( vData, nIntSize, &vMap );
-    vUnique = Vec_IntAlloc( nUnique * nIntSize );
-    Vec_IntForEachEntry( vMap, Ent, i )
-    {
-        if ( Ent < i ) continue;
-        assert( Ent == i );
-        Vec_IntPushArray( vUnique, Vec_IntEntryP(vData, i*nIntSize), nIntSize );
-    }
-    assert( Vec_IntSize(vUnique) == nUnique * nIntSize );
-    Vec_IntFree( vMap );
-    return vUnique;
-}
 
 /**Function*************************************************************
 
diff --git a/src/aig/gia/giaMf.c b/src/aig/gia/giaMf.c
new file mode 100644
index 00000000..c43b6aec
--- /dev/null
+++ b/src/aig/gia/giaMf.c
@@ -0,0 +1,62 @@
+/**CFile****************************************************************
+
+  FileName    [giaMf.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Cut computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaMf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "misc/vec/vecSet.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mf_ManSetDefaultPars( Jf_Par_t * pPars )
+{
+    Jf_ManSetDefaultPars( pPars );
+}
+Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
+{
+    return Jf_ManPerformMapping( pGia, pPars );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 2f04b372..8cd50ce8 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -34,6 +34,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaJf.c \
     src/aig/gia/giaKf.c \
     src/aig/gia/giaLf.c \
+    src/aig/gia/giaMf.c \
     src/aig/gia/giaMan.c \
     src/aig/gia/giaMem.c \
     src/aig/gia/giaMfs.c \