Version abc90220

1 files changed, 602 insertions, 0 deletions

diff --git a/src/aig/gia/giaCSat1.c b/src/aig/gia/giaCSat1.c
new file mode 100644
index 00000000..12b7071f
--- /dev/null
+++ b/src/aig/gia/giaCSat1.c
@@ -0,0 +1,602 @@
+/**CFile****************************************************************
+
+  FileName    [giaCsat1.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Circuit-based SAT solver.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaCsat1.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+typedef struct Css_Fan_t_ Css_Fan_t;
+struct Css_Fan_t_
+{
+    unsigned       iFan     : 31;    // ID of the fanin/fanout
+    unsigned       fCompl   :  1;    // complemented attribute
+};
+
+typedef struct Css_Obj_t_ Css_Obj_t;
+struct Css_Obj_t_
+{
+    unsigned       fCi      :  1;    // terminal node CI
+    unsigned       fCo      :  1;    // terminal node CO
+    unsigned       fAssign  :  1;    // assigned variable
+    unsigned       fValue   :  1;    // variable value
+    unsigned       fPhase   :  1;    // value under 000 pattern
+    unsigned       nFanins  :  5;    // the number of fanins
+    unsigned       nFanouts : 22;    // total number of fanouts
+    unsigned       hHandle;          // application specific data
+    union {
+    unsigned       iFanouts;         // application specific data
+    int            TravId;           // ID of the node
+    };
+    Css_Fan_t      Fanios[0];        // the array of fanins/fanouts
+};
+
+typedef struct Css_Man_t_ Css_Man_t;
+struct Css_Man_t_
+{
+    Gia_Man_t *    pGia;             // the original AIG manager
+    Vec_Int_t *    vCis;             // the vector of CIs (PIs + LOs)
+    Vec_Int_t *    vCos;             // the vector of COs (POs + LIs)
+    int            nObjs;            // the number of objects
+    int            nNodes;           // the number of nodes
+    int *          pObjData;         // the logic network defined for the AIG
+    int            nObjData;         // the size of array to store the logic network
+    int *          pLevels;          // the linked lists of levels
+    int            nLevels;          // the max number of logic levels
+    int            nTravIds;         // traversal ID to mark the cones
+    Vec_Int_t *    vTrail;           // sequence of assignments
+    int            nConfsMax;         // max number of conflicts
+};
+
+static inline unsigned    Gia_ObjHandle( Gia_Obj_t * pObj )                           { return pObj->Value;                                 } 
+
+static inline int         Css_ObjIsCi( Css_Obj_t * pObj )                             { return pObj->fCi;                                   } 
+static inline int         Css_ObjIsCo( Css_Obj_t * pObj )                             { return pObj->fCo;                                   } 
+static inline int         Css_ObjIsNode( Css_Obj_t * pObj )                           { return!pObj->fCi &&!pObj->fCo && pObj->nFanins > 0; } 
+static inline int         Css_ObjIsConst0( Css_Obj_t * pObj )                         { return!pObj->fCi &&!pObj->fCo && pObj->nFanins == 0;} 
+
+static inline int         Css_ObjFaninNum( Css_Obj_t * pObj )                         { return pObj->nFanins;                               } 
+static inline int         Css_ObjFanoutNum( Css_Obj_t * pObj )                        { return pObj->nFanouts;                              } 
+static inline int         Css_ObjSize( Css_Obj_t * pObj )                             { return sizeof(Css_Obj_t) / 4 + pObj->nFanins + pObj->nFanouts;  } 
+static inline int         Css_ObjId( Css_Obj_t * pObj )                               { assert( 0 ); return -1;                             } 
+
+static inline Css_Obj_t * Css_ManObj( Css_Man_t * p, unsigned iHandle )               { return (Css_Obj_t *)(p->pObjData + iHandle);        } 
+static inline Css_Obj_t * Css_ObjFanin( Css_Obj_t * pObj, int i )                     { return (Css_Obj_t *)(((int *)pObj) - pObj->Fanios[i].iFan);               } 
+static inline Css_Obj_t * Css_ObjFanout( Css_Obj_t * pObj, int i )                    { return (Css_Obj_t *)(((int *)pObj) + pObj->Fanios[pObj->nFanins+i].iFan); } 
+static inline int         Css_ObjFaninC( Css_Obj_t * pObj, int i )                    { return pObj->Fanios[i].fCompl;                      } 
+static inline int         Css_ObjFanoutC( Css_Obj_t * pObj, int i )                   { return pObj->Fanios[pObj->nFanins+i].fCompl;        } 
+
+static inline int         Css_ManObjNum( Css_Man_t * p )                              { return p->nObjs;                                    } 
+static inline int         Css_ManNodeNum( Css_Man_t * p )                             { return p->nNodes;                                   } 
+ 
+static inline void        Css_ManIncrementTravId( Css_Man_t * p )                     { p->nTravIds++;                                      }
+static inline void        Css_ObjSetTravId( Css_Obj_t * pObj, int TravId )            { pObj->TravId = TravId;                              }
+static inline void        Css_ObjSetTravIdCurrent( Css_Man_t * p, Css_Obj_t * pObj )  { pObj->TravId = p->nTravIds;                         }
+static inline void        Css_ObjSetTravIdPrevious( Css_Man_t * p, Css_Obj_t * pObj ) { pObj->TravId = p->nTravIds - 1;                     }
+static inline int         Css_ObjIsTravIdCurrent( Css_Man_t * p, Css_Obj_t * pObj )   { return ((int)pObj->TravId == p->nTravIds);          }
+static inline int         Css_ObjIsTravIdPrevious( Css_Man_t * p, Css_Obj_t * pObj )  { return ((int)pObj->TravId == p->nTravIds - 1);      }
+
+static inline int   Css_VarIsAssigned( Css_Obj_t * pVar )      { return pVar->fAssign;                        }
+static inline void  Css_VarAssign( Css_Obj_t * pVar )          { assert(!pVar->fAssign); pVar->fAssign = 1;   }
+static inline void  Css_VarUnassign( Css_Obj_t * pVar )        { assert(pVar->fAssign);  pVar->fAssign = 0;   }
+static inline int   Css_VarValue( Css_Obj_t * pVar )           { assert(pVar->fAssign);  return pVar->fValue; }
+static inline void  Css_VarSetValue( Css_Obj_t * pVar, int v ) { assert(pVar->fAssign);  pVar->fValue = v;    }
+
+#define Css_ManForEachObj( p, pObj, i )               \
+    for ( i = 0; (i < p->nObjData) && (pObj = Css_ManObj(p,i)); i += Css_ObjSize(pObj) )
+#define Css_ManForEachObjVecStart( vVec, p, pObj, i, iStart )            \
+    for ( i = iStart; (i < Vec_IntSize(vVec)) && (pObj = Css_ManObj(p,Vec_IntEntry(vVec,i))); i++ )
+#define Css_ManForEachNode( p, pObj, i )              \
+    for ( i = 0; (i < p->nObjData) && (pObj = Css_ManObj(p,i)); i += Css_ObjSize(pObj) ) if ( Css_ObjIsTerm(pObj) ) {} else
+#define Css_ObjForEachFanin( pObj, pNext, i )         \
+    for ( i = 0; (i < (int)pObj->nFanins) && (pNext = Css_ObjFanin(pObj,i)); i++ )
+#define Css_ObjForEachFanout( pObj, pNext, i )        \
+    for ( i = 0; (i < (int)pObj->nFanouts) && (pNext = Css_ObjFanout(pObj,i)); i++ )
+#define Css_ObjForEachFaninLit( pObj, pNext, fCompl, i )         \
+    for ( i = 0; (i < (int)pObj->nFanins) && (pNext = Css_ObjFanin(pObj,i)) && ((fCompl = Css_ObjFaninC(pObj,i)),1); i++ )
+#define Css_ObjForEachFanoutLit( pObj, pNext, fCompl, i )        \
+    for ( i = 0; (i < (int)pObj->nFanouts) && (pNext = Css_ObjFanout(pObj,i)) && ((fCompl = Css_ObjFanoutC(pObj,i)),1); i++ )
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates logic network isomorphic to the given AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Css_Man_t * Css_ManCreateLogicSimple( Gia_Man_t * pGia )
+{
+    Css_Man_t * p;
+    Css_Obj_t * pObjLog, * pFanLog;
+    Gia_Obj_t * pObj;
+    int i, iHandle = 0;
+    p = ABC_CALLOC( Css_Man_t, 1 );
+    p->pGia = pGia;
+    p->vCis = Vec_IntAlloc( Gia_ManCiNum(pGia) );
+    p->vCos = Vec_IntAlloc( Gia_ManCoNum(pGia) );
+    p->nObjData = (sizeof(Css_Obj_t) / 4) * Gia_ManObjNum(pGia) + 4 * Gia_ManAndNum(pGia) + 2 * Gia_ManCoNum(pGia);
+    p->pObjData = ABC_CALLOC( int, p->nObjData );
+    ABC_FREE( pGia->pRefs );
+    Gia_ManCreateRefs( pGia );
+    Gia_ManForEachObj( pGia, pObj, i )
+    {
+        pObj->Value = iHandle;
+        pObjLog = Css_ManObj( p, iHandle );
+        pObjLog->nFanins  = 0;
+        pObjLog->nFanouts = Gia_ObjRefs( pGia, pObj );
+        pObjLog->hHandle  = iHandle;
+        pObjLog->iFanouts = 0;
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            pFanLog = Css_ManObj( p, Gia_ObjHandle(Gia_ObjFanin0(pObj)) ); 
+            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts].iFan = 
+                pObjLog->Fanios[pObjLog->nFanins].iFan = pObjLog->hHandle - pFanLog->hHandle;
+            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts++].fCompl =
+                pObjLog->Fanios[pObjLog->nFanins++].fCompl = Gia_ObjFaninC0(pObj);
+
+            pFanLog = Css_ManObj( p, Gia_ObjHandle(Gia_ObjFanin1(pObj)) ); 
+            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts].iFan = 
+                pObjLog->Fanios[pObjLog->nFanins].iFan = pObjLog->hHandle - pFanLog->hHandle;
+            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts++].fCompl =
+                pObjLog->Fanios[pObjLog->nFanins++].fCompl = Gia_ObjFaninC1(pObj);
+
+            p->nNodes++;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+        {
+            pFanLog = Css_ManObj( p, Gia_ObjHandle(Gia_ObjFanin0(pObj)) ); 
+            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts].iFan = 
+                pObjLog->Fanios[pObjLog->nFanins].iFan = pObjLog->hHandle - pFanLog->hHandle;
+            pFanLog->Fanios[pFanLog->nFanins + pFanLog->iFanouts++].fCompl =
+                pObjLog->Fanios[pObjLog->nFanins++].fCompl = Gia_ObjFaninC0(pObj);
+
+            pObjLog->fCo = 1;
+            Vec_IntPush( p->vCos, iHandle );
+        }
+        else if ( Gia_ObjIsCi(pObj) )
+        {
+            pObjLog->fCi = 1;
+            Vec_IntPush( p->vCis, iHandle );
+        }
+        iHandle += Css_ObjSize( pObjLog );
+        p->nObjs++;
+    }
+    assert( iHandle == p->nObjData );
+    Gia_ManForEachObj( pGia, pObj, i )
+    {
+        pObjLog = Css_ManObj( p, Gia_ObjHandle(pObj) );
+        assert( pObjLog->nFanouts == pObjLog->iFanouts );
+        pObjLog->TravId = 0;
+    }
+    p->nTravIds = 1;
+    p->vTrail = Vec_IntAlloc( 100 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates logic network isomorphic to the given AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Css_ManStop( Css_Man_t * p )
+{
+    Vec_IntFree( p->vTrail );
+    Vec_IntFree( p->vCis );
+    Vec_IntFree( p->vCos );
+    ABC_FREE( p->pObjData );
+    ABC_FREE( p->pLevels );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Propagates implications for the net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Css_ManImplyNet_rec( Css_Man_t * p, Css_Obj_t * pVar, unsigned Value )
+{
+    static inline Css_ManImplyNode_rec( Css_Man_t * p, Css_Obj_t * pVar );
+    Css_Obj_t * pNext;
+    int i;
+    if ( !Css_ObjIsTravIdCurrent(p, pVar) )
+        return 0;
+    // assign the variable
+    assert( !Css_VarIsAssigned(pVar) );
+    Css_VarAssign( pVar );
+    Css_VarSetValue( pVar, Value );
+    Vec_IntPush( p->vTrail, pVar->hHandle );
+    // propagate fanouts, then fanins
+    Css_ObjForEachFanout( pVar, pNext, i )
+        if ( Css_ManImplyNode_rec( p, pNext ) )
+            return 1;
+    Css_ObjForEachFanin( pVar, pNext, i )
+        if ( Css_ManImplyNode_rec( p, pNext ) )
+            return 1;
+    return 0;
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Propagates implications for the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Css_ManImplyNode_rec( Css_Man_t * p, Css_Obj_t * pVar )
+{
+    Css_Obj_t * pFan0, * pFan1;
+    if ( Css_ObjIsCi(pVar) )
+        return 0;
+    pFan0 = Css_ObjFanin(pVar, 0);
+    pFan1 = Css_ObjFanin(pVar, 1);
+    if ( !Css_VarIsAssigned(pVar) )
+    {
+        if ( Css_VarIsAssigned(pFan0) )
+        {
+            if ( Css_VarValue(pFan0) == Css_ObjFaninC(pVar,0) ) // negative -> propagate
+                return Css_ManImplyNet_rec(p, pVar, 0);
+            // assigned positive
+            if ( Css_VarIsAssigned(pFan1) )
+            {
+                if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> propagate
+                    return Css_ManImplyNet_rec(p, pVar, 0);
+                // asigned positive -> propagate
+                return Css_ManImplyNet_rec(p, pVar, 1);
+            }
+            return 0;
+        }
+        if ( Css_VarIsAssigned(pFan1) )
+        {
+            if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> propagate
+                return Css_ManImplyNet_rec(p, pVar, 0);
+            return 0;
+        }
+        assert( 0 );
+        return 0;
+    }
+    if ( Css_VarValue(pVar) ) // positive
+    {
+        if ( Css_VarIsAssigned(pFan0) )
+        {
+            if ( Css_VarValue(pFan0) == Css_ObjFaninC(pVar,0) ) // negative -> conflict
+                return 1;
+            // check second var
+            if ( Css_VarIsAssigned(pFan1) )
+            {
+                if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> conflict
+                    return 1;
+                // positive + positive -> nothing to do
+                return 0;
+            }
+        }
+        else
+        {
+            // pFan0 unassigned -> enqueue first var
+//            Css_ManEnqueue( p, pFan0, !Css_ObjFaninC(pVar,0) );
+            if ( Css_ManImplyNet_rec( p, pFan0, !Css_ObjFaninC(pVar,0) ) )
+                return 1;
+            // check second var
+            if ( Css_VarIsAssigned(pFan1) )
+            {
+                if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> conflict
+                    return 1;
+                // positive + positive -> nothing to do
+                return 0;
+            }
+        }
+        // unassigned -> enqueue second var
+//        Css_ManEnqueue( p, pFan1, !Css_ObjFaninC(pVar,1) );
+        return Css_ManImplyNet_rec( p, pFan1, !Css_ObjFaninC(pVar,1) );
+    }
+    else // negative
+    {
+        if ( Css_VarIsAssigned(pFan0) )
+        {
+            if ( Css_VarValue(pFan0) == Css_ObjFaninC(pVar,0) ) // negative -> nothing to do
+                return 0;
+            if ( Css_VarIsAssigned(pFan1) )
+            {
+                if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> nothing to do
+                    return 0;
+                // positive + positive -> conflict
+                return 1;
+            }
+            // positive + unassigned -> enqueue second var
+//            Css_ManEnqueue( p, pFan1, Css_ObjFaninC(pVar,1) );
+            return Css_ManImplyNet_rec( p, pFan1, Css_ObjFaninC(pVar,1) );
+        }
+        else
+        {
+            if ( Css_VarIsAssigned(pFan1) )
+            {
+                if ( Css_VarValue(pFan1) == Css_ObjFaninC(pVar,1) ) // negative -> nothing to do
+                    return 0;
+                // unassigned + positive -> enqueue first var
+//                Css_ManEnqueue( p, pFan0, Css_ObjFaninC(pVar,0) );
+                return Css_ManImplyNet_rec( p, pFan0, Css_ObjFaninC(pVar,0) );
+            }
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Css_ManCancelUntil( Css_Man_t * p, int iBound, Vec_Int_t * vCex )
+{
+    Css_Obj_t * pVar;
+    int i;
+    Css_ManForEachObjVecStart( p->vTrail, p, pVar, i, iBound )
+    {
+        if ( vCex )  
+            Vec_IntPush( vCex, Gia_Var2Lit(Css_ObjId(pVar), !pVar->fValue) );
+        Css_VarUnassign( pVar );
+    }
+    Vec_IntShrink( p->vTrail, iBound );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Justifies assignments.]
+
+  Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Css_ManJustify( Css_Man_t * p, int iBegin )
+{
+    Css_Obj_t * pVar, * pFan0, * pFan1;
+    int iState, iThis;
+    if ( p->nConfsMax == 0 )
+        return 1;
+    // get the next variable to justify
+    Css_ManForEachObjVecStart( p->vTrail, p, pVar, iThis, iBegin )
+    {
+        assert( Css_VarIsAssigned(pVar) );
+        if ( Css_VarValue(pVar) || Css_ObjIsCi(pVar) )
+            continue;
+        pFan0 = Css_ObjFanin(pVar,0);
+        pFan1 = Css_ObjFanin(pVar,0);
+        if ( !Css_VarIsAssigned(pFan0) && !Css_VarIsAssigned(pFan1) )
+            break;
+    }
+    if ( iThis == Vec_IntSize(p->vTrail) ) // could not find
+        return 0;
+    // found variable to justify
+    assert( !Css_VarValue(pVar) && !Css_VarIsAssigned(pFan0) && !Css_VarIsAssigned(pFan1) );
+    // remember the state of the stack
+    iState = Vec_IntSize( p->vTrail );
+    // try to justify by setting first fanin to 0
+    if ( !Css_ManImplyNet_rec(p, pFan0, 0) && !Css_ManJustify(p, iThis) )
+        return 0;
+    Css_ManCancelUntil( p, iState, NULL );
+    if ( p->nConfsMax == 0 )
+        return 1;
+    // try to justify by setting second fanin to 0
+    if ( !Css_ManImplyNet_rec(p, pFan1, 0) && !Css_ManJustify(p, iThis) )
+        return 0;
+    Css_ManCancelUntil( p, iState, NULL );
+    if ( p->nConfsMax == 0 )
+        return 1;
+    p->nConfsMax--;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marsk logic cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Css_ManMarkCone_rec( Css_Man_t * p, Css_Obj_t * pVar )
+{
+    if ( Css_ObjIsTravIdCurrent(p, pVar) )
+        return;
+    Css_ObjSetTravIdCurrent(p, pVar);
+    assert( !Css_VarIsAssigned(pVar) );
+    if ( Css_ObjIsCi(pVar) )
+        return;
+    else
+    {
+        Css_Obj_t * pNext;
+        int i;
+        Css_ObjForEachFanin( pVar, pNext, i )
+            Css_ManMarkCone_rec( p, pNext );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Runs one call to the SAT solver.]
+
+  Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Css_ManPrepare( Css_Man_t * p, int * pLits, int nLits )
+{
+    Css_Obj_t * pVar;
+    int i;
+    // mark the cone
+    Css_ManIncrementTravId( p );
+    for ( i = 0; i < nLits; i++ )
+    {
+        pVar = Css_ManObj( p, Gia_Lit2Var(pLits[i]) );
+        Css_ManMarkCone_rec( p, pVar );
+    }
+    // assign literals
+    Vec_IntClear( p->vTrail );
+    for ( i = 0; i < nLits; i++ )
+    {
+        pVar = Css_ManObj( p, Gia_Lit2Var(pLits[i]) );
+        if ( Css_ManImplyNet_rec( p, pVar, !Gia_LitIsCompl(pLits[i]) ) )
+        {
+            Css_ManCancelUntil( p, 0, NULL );
+            return 1;
+        }
+    }
+    return 0;
+}
+ 
+
+/**Function*************************************************************
+
+  Synopsis    [Runs one call to the SAT solver.]
+
+  Description [Returns 1 for UNSAT, 0 for SAT, -1 for UNDECIDED.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Css_ManSolve( Css_Man_t * p, int * pLits, int nLits, int nConfsMax, Vec_Int_t * vCex )
+{
+    // propagate the assignments
+    if ( Css_ManPrepare( p, pLits, nLits ) )
+        return 1;
+    // justify the assignments
+    p->nConfsMax = nConfsMax;
+    if ( Css_ManJustify( p, 0 ) )
+        return p->nConfsMax? 1 : -1;
+    // derive model and return the solver to the initial state
+    Vec_IntClear( vCex );
+    Css_ManCancelUntil( p, 0, vCex );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure to test the new SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_SatSolveTest2( Gia_Man_t * pGia )
+{
+    extern void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, Vec_Int_t * vVisit );
+    int nConfsMax = 1000;
+    int CountUnsat, CountSat, CountUndec;
+    Css_Man_t * p; 
+    Vec_Int_t * vCex;
+    Vec_Int_t * vVisit;
+    Gia_Obj_t * pRoot; 
+    int i, RetValue, iLit, clk = clock();
+    // create logic network
+    p = Css_ManCreateLogicSimple( pGia );
+    // prepare AIG
+    Gia_ManCleanValue( pGia );
+    Gia_ManCleanMark0( pGia );
+    Gia_ManCleanMark1( pGia );
+    vCex   = Vec_IntAlloc( 100 );
+    vVisit = Vec_IntAlloc( 100 );
+    // solve for each output
+    CountUnsat = CountSat = CountUndec = 0;
+    Gia_ManForEachCo( pGia, pRoot, i )
+    {
+        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
+            continue;
+//printf( "Output %6d : ", i );
+        iLit = Gia_Var2Lit( Gia_ObjHandle(Gia_ObjFanin0(pRoot)), Gia_ObjFaninC0(pRoot) );
+        RetValue = Css_ManSolve( p, &iLit, 1, nConfsMax, vCex );
+        if ( RetValue == 1 )
+            CountUnsat++;
+        else if ( RetValue == -1 )
+            CountUndec++;
+        else 
+        {
+//            Gia_Obj_t * pTemp;
+//            int k;
+            assert( RetValue == 0 );
+            CountSat++;
+/*
+            Vec_PtrForEachEntry( vCex, pTemp, k )
+//                printf( "%s%d ", Gia_IsComplement(pTemp)? "!": "", Gia_ObjCioId(Gia_Regular(pTemp)) );
+                printf( "%s%d ", Gia_IsComplement(pTemp)? "!": "", Gia_ObjId(p,Gia_Regular(pTemp)) );
+            printf( "\n" );
+*/
+            Gia_SatVerifyPattern( pGia, pRoot, vCex, vVisit );
+        }
+//        Gia_ManCheckMark0( p );
+//        Gia_ManCheckMark1( p );
+    }
+    Css_ManStop( p );
+    Vec_IntFree( vCex );
+    Vec_IntFree( vVisit );
+    printf( "Unsat = %d. Sat = %d. Undec = %d.  ", CountUnsat, CountSat, CountUndec );
+    ABC_PRT( "Time", clock() - clk );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+