New SAT-based optimization package.

1 files changed, 147 insertions, 0 deletions

diff --git a/src/opt/sbd/sbdCnf.c b/src/opt/sbd/sbdCnf.c
new file mode 100644
index 00000000..6291baed
--- /dev/null
+++ b/src/opt/sbd/sbdCnf.c
@@ -0,0 +1,147 @@
+/**CFile****************************************************************
+
+  FileName    [sbdCnf.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    [CNF computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sbdCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sbd_PrintCnf( Vec_Str_t * vCnf )
+{
+    char Entry;
+    int i, Lit;
+    Vec_StrForEachEntry( vCnf, Entry, i )
+    {
+        Lit = (int)Entry;
+        if ( Lit == -1 )
+            printf( "\n" );
+        else
+            printf( "%s%d ", Abc_LitIsCompl(Lit) ? "-":"", Abc_Lit2Var(Lit) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sbd_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
+{
+    Vec_StrClear( vCnf );
+    if ( Truth == 0 || ~Truth == 0 )
+    {
+//        assert( nVars == 0 );
+        Vec_StrPush( vCnf, (char)(Truth == 0) );
+        Vec_StrPush( vCnf, (char)-1 );
+        return 1;
+    }
+    else 
+    {
+        int i, k, c, RetValue, Literal, Cube, nCubes = 0;
+        assert( nVars > 0 );
+        for ( c = 0; c < 2; c ++ )
+        {
+            Truth = c ? ~Truth : Truth;
+            RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
+            assert( RetValue == 0 );
+            nCubes += Vec_IntSize( vCover );
+            Vec_IntForEachEntry( vCover, Cube, i )
+            {
+                for ( k = 0; k < nVars; k++ )
+                {
+                    Literal = 3 & (Cube >> (k << 1));
+                    if ( Literal == 1 )      // '0'  -> pos lit
+                        Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) );
+                    else if ( Literal == 2 ) // '1'  -> neg lit
+                        Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) );
+                    else if ( Literal != 0 )
+                        assert( 0 );
+                }
+                Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
+                Vec_StrPush( vCnf, (char)-1 );
+            }
+        }
+        return nCubes;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sbd_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar )
+{
+    Vec_Int_t * vClause;
+    char Entry;
+    int i, Lit;
+    Vec_WecClear( vRes );
+    vClause = Vec_WecPushLevel( vRes );
+    Vec_StrForEachEntry( vCnf, Entry, i )
+    {
+        if ( (int)Entry == -1 )
+        {
+            vClause = Vec_WecPushLevel( vRes );
+            continue;
+        }
+        Lit = Abc_Lit2LitV( Vec_IntArray(vFaninMap), (int)Entry );
+        Lit = Abc_LitNotCond( Lit, Abc_Lit2Var(Lit) == iPivotVar );
+        Vec_IntPush( vClause, Lit );
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+