Experiments with circuit-based SAT.

1 files changed, 159 insertions, 0 deletions

diff --git a/src/aig/gia/gia.c b/src/aig/gia/gia.c
index 4fb33a9b..8f18f69c 100644
--- a/src/aig/gia/gia.c
+++ b/src/aig/gia/gia.c
@@ -26,6 +26,43 @@ ABC_NAMESPACE_IMPL_START
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
+ 
+typedef struct Slv_Man_t_ Slv_Man_t;
+struct Slv_Man_t_
+{
+    Vec_Int_t      vCis;
+    Vec_Int_t      vCos;
+    Vec_Int_t      vFanins;
+    Vec_Int_t      vFanoutN;
+    Vec_Int_t      vFanout0;
+    Vec_Str_t      vValues;
+    Vec_Int_t      vCopies;
+};
+
+static inline int  Slv_ManObjNum       ( Slv_Man_t * p )                      { return Vec_IntSize(&p->vFanins)/2;                       }
+
+static inline int  Slv_ObjFaninLit     ( Slv_Man_t * p, int iObj, int f )     { return Vec_IntEntry(&p->vFanins, Abc_Var2Lit(iObj, f));  }
+static inline int  Slv_ObjFanin        ( Slv_Man_t * p, int iObj, int f )     { return Abc_Lit2Var(Slv_ObjFaninLit(p, iObj, f));         }
+static inline int  Slv_ObjFaninC       ( Slv_Man_t * p, int iObj, int f )     { return Abc_LitIsCompl(Slv_ObjFaninLit(p, iObj, f));      }
+
+static inline int  Slv_ObjIsCi         ( Slv_Man_t * p, int iObj )            { return !Slv_ObjFaninLit(p, iObj, 0) &&  Slv_ObjFaninLit(p, iObj, 1);  }
+static inline int  Slv_ObjIsCo         ( Slv_Man_t * p, int iObj )            { return  Slv_ObjFaninLit(p, iObj, 0) && !Slv_ObjFaninLit(p, iObj, 1);  }
+static inline int  Slv_ObjIsAnd        ( Slv_Man_t * p, int iObj )            { return  Slv_ObjFaninLit(p, iObj, 0) &&  Slv_ObjFaninLit(p, iObj, 1);  }
+
+static inline int  Slv_ObjFanout0      ( Slv_Man_t * p, int iObj )            { return Vec_IntEntry(&p->vFanout0, iObj);      }
+static inline void Slv_ObjSetFanout0   ( Slv_Man_t * p, int iObj, int iLit )  { Vec_IntWriteEntry(&p->vFanout0, iObj, iLit);  }
+
+static inline int  Slv_ObjNextFanout   ( Slv_Man_t * p, int iLit )            { return Vec_IntEntry(&p->vFanoutN, iLit);      }
+static inline void Slv_ObjSetNextFanout( Slv_Man_t * p, int iLit, int iLitF ) { Vec_IntWriteEntry(&p->vFanoutN, iLit, iLitF); }
+
+static inline int  Slv_ObjCopyLit      ( Slv_Man_t * p, int iObj )            { return Vec_IntEntry(&p->vCopies, iObj);       }
+static inline void Slv_ObjSetCopyLit   ( Slv_Man_t * p, int iObj, int iLit )  { Vec_IntWriteEntry(&p->vCopies, iObj, iLit);   }
+
+#define Slv_ManForEachObj( p, iObj )                                  \
+    for ( iObj = 1; iObj < Slv_ManObjNum(p); iObj++ )
+
+#define Slv_ObjForEachFanout( p, iObj, iFanLit )                      \
+    for ( iFanLit = Slv_ObjFanout0(p, iObj); iFanLit; iFanLit = Slv_ObjNextFanout(p, iFanLit) )
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -42,6 +79,128 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+Slv_Man_t * Slv_ManAlloc( int nObjs )
+{
+    Slv_Man_t * p = ABC_CALLOC( Slv_Man_t, 1 );
+    Vec_IntGrow( &p->vCis,     100 );
+    Vec_IntGrow( &p->vCos,     100 );
+    Vec_IntGrow( &p->vFanins,  2*nObjs );
+    Vec_IntGrow( &p->vFanoutN, 2*nObjs );
+    Vec_IntGrow( &p->vFanout0, nObjs );
+    Vec_StrGrow( &p->vValues,  nObjs );
+    // constant node
+    Vec_IntFill( &p->vFanins,  2, 0 );
+    Vec_IntFill( &p->vFanoutN, 2, 0 );
+    Vec_IntFill( &p->vFanout0, 1, 0 );
+    return p;
+}
+void Slv_ManFree( Slv_Man_t * p )
+{
+    Vec_IntErase( &p->vCis     );
+    Vec_IntErase( &p->vCos     );
+    Vec_IntErase( &p->vFanins  );
+    Vec_IntErase( &p->vFanoutN );
+    Vec_IntErase( &p->vFanout0 );
+    Vec_StrErase( &p->vValues  );
+    Vec_IntErase( &p->vCopies  );
+    ABC_FREE( p );
+}
+void Slv_ManPrintFanouts( Slv_Man_t * p )
+{
+    int iObj, iFanLit;
+    Slv_ManForEachObj( p, iObj )
+    {
+        printf( "Fanouts of node %d: ", iObj );
+        Slv_ObjForEachFanout( p, iObj, iFanLit )
+            printf( "%d ", Abc_Lit2Var(iFanLit) );
+        printf( "\n" );
+    }
+}
+static inline int Slv_ManAppendObj( Slv_Man_t * p, int iLit0, int iLit1 )
+{
+    int iObj = Slv_ManObjNum(p);
+    Vec_StrPush( &p->vValues,  0 );
+    Vec_IntPush( &p->vFanout0, 0 );
+    Vec_IntPushTwo( &p->vFanoutN, 0, 0 );
+    if ( !iLit0 )  // primary input
+        assert(!iLit1), iLit1 = Vec_IntSize(&p->vCis)+1, Vec_IntPush(&p->vCis, iObj);
+    else if ( !iLit1 )  // primary output
+        assert(iLit0), Vec_IntPush(&p->vCos, iObj);
+    else
+    {
+        Slv_ObjSetNextFanout( p, Abc_Var2Lit(iObj, 0), Slv_ObjFanout0(p, Abc_Lit2Var(iLit0)) );
+        Slv_ObjSetNextFanout( p, Abc_Var2Lit(iObj, 1), Slv_ObjFanout0(p, Abc_Lit2Var(iLit1)) );
+        Slv_ObjSetFanout0( p, Abc_Lit2Var(iLit0), Abc_Var2Lit(iObj, 0) );
+        Slv_ObjSetFanout0( p, Abc_Lit2Var(iLit1), Abc_Var2Lit(iObj, 1) );
+    }
+    Vec_IntPushTwo( &p->vFanins, iLit0, iLit1 );
+    return Abc_Var2Lit( iObj, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Slv_Man_t * Slv_ManFromGia( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj; int i;
+    Slv_Man_t * pNew = Slv_ManAlloc( Gia_ManObjNum(p) );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachObj1( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Slv_ManAppendObj( pNew, Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj)), Abc_LitNotCond(Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj)) );
+        else if ( Gia_ObjIsCo(pObj) )
+            pObj->Value = Slv_ManAppendObj( pNew, Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj)), 0 );
+        else if ( Gia_ObjIsCi(pObj) )
+            pObj->Value = Slv_ManAppendObj( pNew, 0, 0 );
+        else
+            assert( 0 );
+    }
+    assert( Gia_ManObjNum(p) == Slv_ManObjNum(pNew) );
+    return pNew;
+}
+Gia_Man_t * Slv_ManToGia( Slv_Man_t * p )
+{
+    int iObj;
+    Gia_Man_t * pNew = Gia_ManStart( Slv_ManObjNum(p) ); 
+    Vec_IntFill( &p->vCopies,  Slv_ManObjNum(p), 0 );
+    Slv_ManForEachObj( p, iObj )
+        if ( Slv_ObjIsCi(p, iObj) )
+            Slv_ObjSetCopyLit( p, iObj, Gia_ManAppendCi(pNew) );
+        else if ( Slv_ObjIsCo(p, iObj) )
+        {
+            int iLit0 = Abc_LitNotCond( Slv_ObjCopyLit(p, Slv_ObjFanin(p, iObj, 0)), Slv_ObjFaninC(p, iObj, 0) );
+            Slv_ObjSetCopyLit( p, iObj, Gia_ManAppendCo(pNew, iLit0) );
+        }
+        else if ( Slv_ObjIsAnd(p, iObj) )
+        {
+            int iLit0 = Abc_LitNotCond( Slv_ObjCopyLit(p, Slv_ObjFanin(p, iObj, 0)), Slv_ObjFaninC(p, iObj, 0) );
+            int iLit1 = Abc_LitNotCond( Slv_ObjCopyLit(p, Slv_ObjFanin(p, iObj, 1)), Slv_ObjFaninC(p, iObj, 1) );
+            Slv_ObjSetCopyLit( p, iObj, Gia_ManAppendAnd(pNew, iLit0, iLit1) );
+        }
+        else assert(0);
+    assert( Gia_ManObjNum(pNew) == Slv_ManObjNum(p) );
+    return pNew;
+}
+
+Gia_Man_t * Slv_ManToAig( Gia_Man_t * pGia )
+{
+    Slv_Man_t * p = Slv_ManFromGia( pGia );
+    Gia_Man_t * pNew = Slv_ManToGia( p );
+    pNew->pName = Abc_UtilStrsav( pGia->pName );
+    pNew->pSpec = Abc_UtilStrsav( pGia->pSpec );
+    Slv_ManPrintFanouts( p );
+    Slv_ManFree( p );
+    return pNew;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///