initial commit of public abc

1 files changed, 1001 insertions, 0 deletions

diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c
new file mode 100644
index 00000000..a5a575fd
--- /dev/null
+++ b/src/aig/saig/saigConstr2.c
@@ -0,0 +1,1001 @@
+/**CFile****************************************************************
+
+  FileName    [saigConstr2.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Functional constraint detection.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigConstr2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "cnf.h"
+#include "satSolver.h"
+#include "kit.h"
+#include "bar.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Aig_Obj_t * Aig_ObjFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i )                       { return pObjMap[nFs*pObj->Id + i];  }
+static inline void        Aig_ObjSetFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { pObjMap[nFs*pObj->Id + i] = pNode; }
+
+static inline Aig_Obj_t * Aig_ObjChild0Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin0(pObj)? Aig_NotCond(Aig_ObjFrames(pObjMap,nFs,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL;  }
+static inline Aig_Obj_t * Aig_ObjChild1Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin1(pObj)? Aig_NotCond(Aig_ObjFrames(pObjMap,nFs,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL;  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+ 
+/**Function*************************************************************
+
+  Synopsis    [Returns the probability of POs being 1 under rand seq sim.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ManProfileConstraints( Aig_Man_t * p, int nWords, int nFrames, int fVerbose )
+{
+    Vec_Ptr_t * vInfo;
+    Vec_Int_t * vProbs, * vProbs2;
+    Aig_Obj_t * pObj, * pObjLi;
+    unsigned * pInfo, * pInfo0, * pInfo1, * pInfoMask, * pInfoMask2;
+    int i, w, f, RetValue = 1, clk = clock();
+    if ( fVerbose )
+        printf( "Simulating %d nodes and %d flops for %d frames with %d words... ", 
+            Aig_ManNodeNum(p), Aig_ManRegNum(p), nFrames, nWords );
+    Aig_ManRandom( 1 );
+    vInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p)+2, nWords );
+    Vec_PtrCleanSimInfo( vInfo, 0, nWords );
+    vProbs  = Vec_IntStart( Saig_ManPoNum(p) );
+    vProbs2 = Vec_IntStart( Saig_ManPoNum(p) );
+    // start the constant
+    pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(Aig_ManConst1(p)) );
+    for ( w = 0; w < nWords; w++ )
+        pInfo[w] = ~0;
+    // start the flop inputs
+    Saig_ManForEachLi( p, pObj, i )
+    {
+        pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
+        for ( w = 0; w < nWords; w++ )
+            pInfo[w] = 0;
+    }
+    // get the info mask
+    pInfoMask  = (unsigned *)Vec_PtrEntry( vInfo, Aig_ManObjNumMax(p) );    // PO failed
+    pInfoMask2 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ManObjNumMax(p)+1 );  // constr failed
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // assign primary inputs
+        Saig_ManForEachPi( p, pObj, i )
+        {
+            pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
+            for ( w = 0; w < nWords; w++ )
+                pInfo[w] = Aig_ManRandom( 0 );
+        }
+        // move the flop values
+        Saig_ManForEachLiLo( p, pObjLi, pObj, i )
+        {
+            pInfo  = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
+            pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObjLi) );
+            for ( w = 0; w < nWords; w++ )
+                pInfo[w] = pInfo0[w];
+        }
+        // simulate the nodes
+        Aig_ManForEachNode( p, pObj, i )
+        {
+            pInfo  = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
+            pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjFaninId0(pObj) );
+            pInfo1 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjFaninId1(pObj) );
+            if ( Aig_ObjFaninC0(pObj) )
+            {
+                if (  Aig_ObjFaninC1(pObj) )
+                    for ( w = 0; w < nWords; w++ )
+                        pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
+                else 
+                    for ( w = 0; w < nWords; w++ )
+                        pInfo[w] = ~pInfo0[w] & pInfo1[w];
+            }
+            else 
+            {
+                if (  Aig_ObjFaninC1(pObj) )
+                    for ( w = 0; w < nWords; w++ )
+                        pInfo[w] = pInfo0[w] & ~pInfo1[w];
+                else 
+                    for ( w = 0; w < nWords; w++ )
+                        pInfo[w] = pInfo0[w] & pInfo1[w];
+            }
+        }
+        // clean the mask
+        for ( w = 0; w < nWords; w++ )
+            pInfoMask[w] = pInfoMask2[w] = 0;
+        // simulate the primary outputs
+        Aig_ManForEachPo( p, pObj, i )
+        {
+            pInfo  = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
+            pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjFaninId0(pObj) );
+            if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) || i >= Saig_ManPoNum(p) )
+            {
+                if ( Aig_ObjFaninC0(pObj) )
+                {
+                    for ( w = 0; w < nWords; w++ )
+                        pInfo[w] = ~pInfo0[w];
+                }
+                else 
+                {
+                    for ( w = 0; w < nWords; w++ )
+                        pInfo[w] = pInfo0[w];
+                }
+            }
+            else
+            {
+                if ( Aig_ObjFaninC0(pObj) )
+                {
+                    for ( w = 0; w < nWords; w++ )
+                        pInfo[w] |= ~pInfo0[w];
+                }
+                else 
+                {
+                    for ( w = 0; w < nWords; w++ )
+                        pInfo[w] |= pInfo0[w];
+                }
+            }
+            // collect patterns when one of the outputs fails
+            if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
+            {
+                for ( w = 0; w < nWords; w++ )
+                    pInfoMask[w] |= pInfo[w];
+            }
+            else if ( i < Saig_ManPoNum(p) )
+            {
+                for ( w = 0; w < nWords; w++ )
+                    pInfoMask2[w] |= pInfo[w];
+            }
+        }
+        // compare the PO values (mask=1 => out=0) or UNSAT(mask=1 & out=1)
+        Saig_ManForEachPo( p, pObj, i )
+        {
+            pInfo  = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
+            for ( w = 0; w < nWords; w++ )
+                Vec_IntAddToEntry( vProbs, i, Aig_WordCountOnes(pInfo[w]) );
+            if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
+            {
+                // chek the output
+                for ( w = 0; w < nWords; w++ )
+                    if ( pInfo[w] & ~pInfoMask2[w] ) 
+                        break;
+                if ( w == nWords )
+                    continue;
+                printf( "Primary output %d fails on some input patterns.\n", i );
+            }
+            else
+            {
+                // collect patterns that block the POs
+                for ( w = 0; w < nWords; w++ )
+                    Vec_IntAddToEntry( vProbs2, i, Aig_WordCountOnes(pInfo[w] & pInfoMask[w]) );
+            }
+        }
+    }
+    if ( fVerbose )
+        Abc_PrintTime( 1, "T", clock() - clk );
+    // print the state
+    if ( fVerbose )
+    {
+        Saig_ManForEachPo( p, pObj, i )
+        {
+            if ( i < Saig_ManPoNum(p) - Saig_ManConstrNum(p) )
+                printf( "Primary output :  ", i );
+            else
+                printf( "Constraint %3d :  ", i-(Saig_ManPoNum(p) - Saig_ManConstrNum(p))  );
+            printf( "ProbOne = %f  ",  (float)Vec_IntEntry(vProbs,  i)/(32*nWords*nFrames) );
+            printf( "ProbOneC = %f  ", (float)Vec_IntEntry(vProbs2, i)/(32*nWords*nFrames) );
+            printf( "AllZeroValue = %d ", Aig_ObjPhase(pObj) );
+            printf( "\n" );
+        }
+    }
+
+    // print the states
+    Vec_PtrFree( vInfo );
+    Vec_IntFree( vProbs );
+    Vec_IntFree( vProbs2 );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates COI of the property output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManCreateIndMiter( Aig_Man_t * pAig, Vec_Vec_t * vCands )
+{
+    int nFrames = 2;
+    Vec_Ptr_t * vNodes;
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
+    Aig_Obj_t ** pObjMap;
+    int i, f, k;
+
+    // create mapping for the frames nodes
+    pObjMap  = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
+
+    // start the fraig package
+    pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
+    pFrames->pName = Aig_UtilStrsav( pAig->pName );
+    pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec );
+    // map constant nodes
+    for ( f = 0; f < nFrames; f++ )
+        Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
+    // create PI nodes for the frames
+    for ( f = 0; f < nFrames; f++ )
+        Aig_ManForEachPiSeq( pAig, pObj, i )
+            Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreatePi(pFrames) );
+    // set initial state for the latches
+    Aig_ManForEachLoSeq( pAig, pObj, i )
+        Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreatePi(pFrames) );
+
+    // add timeframes
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+        {
+            pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Aig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
+            Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
+        }
+        // set the latch inputs and copy them into the latch outputs of the next frame
+        Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
+        {
+            pObjNew = Aig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
+            if ( f < nFrames - 1 )
+                Aig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
+        }
+    }
+
+    // go through the candidates
+    Vec_VecForEachLevel( vCands, vNodes, i )
+    {
+        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
+        {
+            Aig_Obj_t * pObjR  = Aig_Regular(pObj);
+            Aig_Obj_t * pNode0 = pObjMap[nFrames*Aig_ObjId(pObjR)+0];
+            Aig_Obj_t * pNode1 = pObjMap[nFrames*Aig_ObjId(pObjR)+1];
+            Aig_Obj_t * pFan0  = Aig_NotCond( pNode0,  Aig_IsComplement(pObj) );
+            Aig_Obj_t * pFan1  = Aig_NotCond( pNode1, !Aig_IsComplement(pObj) );
+            Aig_Obj_t * pMiter = Aig_And( pFrames, pFan0, pFan1 );
+            Aig_ObjCreatePo( pFrames, pMiter );
+        }
+    }
+    Aig_ManCleanup( pFrames );
+    ABC_FREE( pObjMap );
+
+//Aig_ManShow( pAig, 0, NULL );
+//Aig_ManShow( pFrames, 0, NULL );
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs inductive check for one of the constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManFilterUsingIndOne_new( Aig_Man_t * p, Aig_Man_t * pFrame, sat_solver * pSat, Cnf_Dat_t * pCnf, int nConfs, int nProps, int Counter )
+{
+    Aig_Obj_t * pObj;
+    int Lit, status;
+    pObj = Aig_ManPo( pFrame, Counter );
+    Lit  = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 );
+    status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 );
+    if ( status == l_False )
+        return 1;
+    if ( status == l_Undef )
+    {
+//        printf( "Solver returned undecided.\n" );
+        return 0;
+    }
+    assert( status == l_True );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Detects constraints functionally.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManFilterUsingInd( Aig_Man_t * p, Vec_Vec_t * vCands, int nConfs, int nProps, int fVerbose )
+{
+    Vec_Ptr_t * vNodes;
+    Aig_Man_t * pFrames;
+    sat_solver * pSat;
+    Cnf_Dat_t * pCnf;
+    Aig_Obj_t * pObj;
+    int i, k, k2, Counter;
+/*
+    Vec_VecForEachLevel( vCands, vNodes, i )
+        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
+            printf( "%d ", Aig_ObjId(Aig_Regular(pObj)) );
+    printf( "\n" );
+*/
+    // create timeframes
+//    pFrames = Saig_ManUnrollInd( p );
+    pFrames = Saig_ManCreateIndMiter( p, vCands );
+    assert( Aig_ManPoNum(pFrames) == Vec_VecSizeSize(vCands) );
+    // start the SAT solver
+    pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) );
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    // check candidates
+    if ( fVerbose )
+        printf( "Filtered cands:  " );
+    Counter = 0;
+    Vec_VecForEachLevel( vCands, vNodes, i )
+    {
+        k2 = 0;
+        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
+        {
+            if ( Saig_ManFilterUsingIndOne_new( p, pFrames, pSat, pCnf, nConfs, nProps, Counter++ ) )
+//            if ( Saig_ManFilterUsingIndOne_old( p, pSat, pCnf, nConfs, pObj ) )
+            {
+                Vec_PtrWriteEntry( vNodes, k2++, pObj );
+                if ( fVerbose )
+                    printf( "%d:%s%d  ", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+            }
+        }
+        Vec_PtrShrink( vNodes, k2 );
+    }
+    if ( fVerbose )
+        printf( "\n" );
+    // clean up
+    Cnf_DataFree( pCnf );
+    sat_solver_delete( pSat );
+    if ( fVerbose )
+        Aig_ManPrintStats( pFrames );
+    Aig_ManStop( pFrames );
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates COI of the property output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManUnrollCOI_( Aig_Man_t * p, int nFrames )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t ** pObjMap;
+    int i;
+//Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFrames, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t *** ppObjMap )
+    pFrames = Aig_ManFrames( p, nFrames, 0, 1, 1, 0, &pObjMap );
+    for ( i = 0; i < nFrames * Aig_ManObjNumMax(p); i++ )
+        if ( pObjMap[i] && Aig_ObjIsNone( Aig_Regular(pObjMap[i]) ) )
+            pObjMap[i] = NULL;
+    assert( p->pObjCopies == NULL );
+    p->pObjCopies = pObjMap;
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates COI of the property output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManUnrollCOI( Aig_Man_t * pAig, int nFrames )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
+    Aig_Obj_t ** pObjMap;
+    int i, f;
+    // create mapping for the frames nodes
+    pObjMap = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
+    // start the fraig package
+    pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
+    pFrames->pName = Aig_UtilStrsav( pAig->pName );
+    pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec );
+    // map constant nodes
+    for ( f = 0; f < nFrames; f++ )
+        Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
+    // create PI nodes for the frames
+    for ( f = 0; f < nFrames; f++ )
+        Aig_ManForEachPiSeq( pAig, pObj, i )
+            Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreatePi(pFrames) );
+    // set initial state for the latches
+    Aig_ManForEachLoSeq( pAig, pObj, i )
+        Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreatePi(pFrames) );
+    // add timeframes
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Aig_ManForEachNode( pAig, pObj, i )
+        {
+            pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Aig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
+            Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
+        }
+        // set the latch inputs and copy them into the latch outputs of the next frame
+        Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
+        {
+            pObjNew = Aig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
+            if ( f < nFrames - 1 )
+                Aig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
+        }
+    }
+    // create the only output
+    for ( f = nFrames-1; f < nFrames; f++ )
+    {
+        Aig_ManForEachPoSeq( pAig, pObj, i )
+        {
+            pObjNew = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f) );
+            Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
+        }
+    }
+    // created lots of dangling nodes - no sweeping!
+    //Aig_ManCleanup( pFrames );
+    assert( pAig->pObjCopies == NULL );
+    pAig->pObjCopies = pObjMap;
+    return pFrames;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collects and saves values of the SAT variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_CollectSatValues( sat_solver * pSat, Cnf_Dat_t * pCnf, Vec_Ptr_t * vInfo, int * piPat )
+{
+    Aig_Obj_t * pObj;
+    unsigned * pInfo;
+    int i;
+    Aig_ManForEachObj( pCnf->pMan, pObj, i )
+    {
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+            continue;
+        assert( pCnf->pVarNums[i] > 0 );
+        pInfo = (unsigned *)Vec_PtrEntry( vInfo, i );
+        if ( Aig_InfoHasBit(pInfo, *piPat) != sat_solver_var_value(pSat, pCnf->pVarNums[i]) )
+            Aig_InfoXorBit(pInfo, *piPat);
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Runs the SAT test for the node in one polarity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_DetectTryPolarity( sat_solver * pSat, int nConfs, int nProps, Cnf_Dat_t * pCnf, Aig_Obj_t * pObj, int iPol, Vec_Ptr_t * vInfo, int * piPat, int fVerbose )
+{
+    Aig_Obj_t * pOut = Aig_ManPo( pCnf->pMan, 0 );
+    int status, Lits[2];
+//    ABC_INT64_T nOldConfs = pSat->stats.conflicts;
+//    ABC_INT64_T nOldImps = pSat->stats.propagations;
+    Lits[0] = toLitCond( pCnf->pVarNums[Aig_ObjId(pOut)], 0 );
+    Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !iPol );
+    status = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nConfs, (ABC_INT64_T)nProps, 0, 0 );
+    if ( status == l_False )
+    {
+//        printf( "u%d(%d) ", (int)(pSat->stats.conflicts-nOldConfs), (int)(pSat->stats.propagations-nOldImps) );
+        return 1;
+    }
+    if ( status == l_Undef )
+    {
+//        printf( "Solver returned undecided.\n" );
+        return 0;
+    }
+//    printf( "s%d(%d) ", (int)(pSat->stats.conflicts-nOldConfs), (int)(pSat->stats.propagations-nOldImps) );
+    assert( status == l_True );
+    Saig_CollectSatValues( pSat, pCnf, vInfo, piPat );
+    (*piPat)++;
+    if ( *piPat == Vec_PtrReadWordsSimInfo(vInfo) * 32 )
+    {
+        if ( fVerbose )
+            printf( "Warning: Reached the limit on the number of patterns.\n" );
+        *piPat = 0;
+    }
+    return 0;
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of variables implied by the output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Ssw_ManFindDirectImplications( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fVerbose )
+{
+    Vec_Vec_t * vCands = NULL;
+    Vec_Ptr_t * vNodes;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pRepr, * pReprR;
+    int i, f, k, value;
+    vCands = Vec_VecAlloc( nFrames );
+
+    // perform unrolling
+    pFrames = Saig_ManUnrollCOI( p, nFrames );
+    assert( Aig_ManPoNum(pFrames) == 1 );
+    // start the SAT solver
+    pCnf = Cnf_DeriveSimple( pFrames, 0 );
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    if ( pSat != NULL )
+    {
+        Aig_ManIncrementTravId( p );
+        for ( f = 0; f < nFrames; f++ )
+        {
+            Aig_ManForEachObj( p, pObj, i )
+            {
+                if ( !Aig_ObjIsCand(pObj) )
+                    continue;
+                if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+                    continue;
+                // get the node from timeframes
+                pRepr  = p->pObjCopies[nFrames*i + nFrames-1-f];
+                pReprR = Aig_Regular(pRepr);
+                if ( pCnf->pVarNums[Aig_ObjId(pReprR)] < 0 )
+                    continue;
+                value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ];
+                if ( value == l_Undef )
+                    continue;
+                // label this node as taken
+                Aig_ObjSetTravIdCurrent(p, pObj);
+                if ( Saig_ObjIsLo(p, pObj) )
+                    Aig_ObjSetTravIdCurrent( p, Aig_ObjFanin0(Saig_ObjLoToLi(p, pObj)) );
+                // remember the node
+                Vec_VecPush( vCands, f, Aig_NotCond( pObj, (value == l_True) ^ Aig_IsComplement(pRepr) ) );
+        //        printf( "%s%d ", (value == l_False)? "":"!", i );
+            }
+        }
+    //    printf( "\n" );
+        sat_solver_delete( pSat );
+    }
+    Aig_ManStop( pFrames );
+    Cnf_DataFree( pCnf );
+
+    if ( fVerbose )
+    {
+        printf( "Found %3d candidates.\n", Vec_VecSizeSize(vCands) );
+        Vec_VecForEachLevel( vCands, vNodes, k )
+        {
+            printf( "Level %d. Cands  =%d    ", k, Vec_PtrSize(vNodes) );
+//            Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+//                printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+            printf( "\n" );
+        }
+    }
+
+    ABC_FREE( p->pObjCopies );
+    Saig_ManFilterUsingInd( p, vCands, nConfs, nProps, fVerbose );
+    if ( Vec_VecSizeSize(vCands) )
+        printf( "Found %3d constraints after filtering.\n", Vec_VecSizeSize(vCands) );
+    if ( fVerbose )
+    {
+        Vec_VecForEachLevel( vCands, vNodes, k )
+        {
+            printf( "Level %d. Constr =%d    ", k, Vec_PtrSize(vNodes) );
+//            Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+//                printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+            printf( "\n" );
+        }
+    }
+
+    return vCands;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Detects constraints functionally.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Saig_ManDetectConstrFunc( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fVerbose )
+{
+    int iPat = 0, nWordsAlloc = 16;
+    Bar_Progress_t * pProgress = NULL;
+    Vec_Vec_t * vCands = NULL;
+    Vec_Ptr_t * vInfo, * vNodes;
+    Aig_Obj_t * pObj, * pRepr, * pObjNew;
+    Aig_Man_t * pFrames;
+    sat_solver * pSat;
+    Cnf_Dat_t * pCnf;
+    unsigned * pInfo;
+    int i, j, k, Lit, status, nCands = 0;
+    assert( Saig_ManPoNum(p) == 1 );
+    if ( Saig_ManPoNum(p) != 1 )
+    {
+        printf( "The number of outputs is different from 1.\n" );
+        return NULL;
+    }
+//printf( "Implications = %d.\n", Ssw_ManCountImplications(p, nFrames) );
+
+    // perform unrolling
+    pFrames = Saig_ManUnrollCOI( p, nFrames );
+    assert( Aig_ManPoNum(pFrames) == 1 );
+    if ( fVerbose )
+    {
+        printf( "Detecting constraints with %d frames, %d conflicts, and %d propagations.\n", nFrames, nConfs, nProps );
+        printf( "Frames: " );
+        Aig_ManPrintStats( pFrames );
+    }
+//    Aig_ManShow( pFrames, 0, NULL );
+
+    // start the SAT solver
+    pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) );
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+//printf( "Implications = %d.\n", pSat->qhead );
+
+    // solve the original problem
+    Lit = toLitCond( pCnf->pVarNums[Aig_ObjId(Aig_ManPo(pFrames,0))], 0 );
+    status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 );
+    if ( status == l_False )
+    {
+        printf( "The problem is trivially UNSAT (inductive with k=%d).\n", nFrames-1 );
+        Cnf_DataFree( pCnf );
+        sat_solver_delete( pSat );
+        Aig_ManStop( pFrames );
+        return NULL;
+    }
+    if ( status == l_Undef )
+    {
+        printf( "Solver could not solve the original problem.\n" );
+        Cnf_DataFree( pCnf );
+        sat_solver_delete( pSat );
+        Aig_ManStop( pFrames );
+        return NULL;
+    }
+    assert( status == l_True );
+
+    // create simulation info
+    vInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pFrames), nWordsAlloc );
+    Vec_PtrCleanSimInfo( vInfo, 0, nWordsAlloc );
+    Saig_CollectSatValues( pSat, pCnf, vInfo, &iPat );
+    Aig_ManForEachObj( pFrames, pObj, i )
+    {
+        pInfo = (unsigned *)Vec_PtrEntry( vInfo, i );
+        if ( pInfo[0] & 1 )
+            memset( (char*)pInfo, 0xff, 4*nWordsAlloc );
+    }
+//    Aig_ManShow( pFrames, 0, NULL );
+//    Aig_ManShow( p, 0, NULL );
+
+    // consider the nodes for ci=>!Out and label when it holds
+    pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pFrames) );
+    Aig_ManCleanMarkAB( pFrames );
+    Aig_ManForEachObj( pFrames, pObj, i )
+    {
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+            continue;
+        Bar_ProgressUpdate( pProgress, i, NULL );
+        // check if the node is available in both polarities
+        pInfo = (unsigned *)Vec_PtrEntry( vInfo, i );
+        for ( k = 0; k < nWordsAlloc; k++ )
+            if ( pInfo[k] != ~0 )
+                break;
+        if ( k == nWordsAlloc )
+        {
+            if ( Saig_DetectTryPolarity(pSat, nConfs, nProps, pCnf, pObj, 0, vInfo, &iPat, fVerbose) ) // !pObj is a constr
+            {
+                pObj->fMarkA = 1, nCands++;
+//                printf( "!%d  ", Aig_ObjId(pObj) );
+            }
+            continue;
+        }
+        for ( k = 0; k < nWordsAlloc; k++ )
+            if ( pInfo[k] != 0 )
+                break;
+        if ( k == nWordsAlloc )
+        {
+            if ( Saig_DetectTryPolarity(pSat, nConfs, nProps, pCnf, pObj, 1, vInfo, &iPat, fVerbose) ) //  pObj is a constr
+            {
+                pObj->fMarkB = 1, nCands++;
+//                printf( "%d  ", Aig_ObjId(pObj) );
+            }
+            continue;
+        }
+    }
+    Bar_ProgressStop( pProgress );
+    if ( nCands )
+    {
+
+//        printf( "\n" );
+        if ( fVerbose )
+            printf( "Found %3d classes of candidates.\n", nCands );
+        vCands = Vec_VecAlloc( nFrames );
+        for ( k = 0; k < nFrames; k++ )
+        {
+            Aig_ManForEachObj( p, pObj, i )
+            {
+                if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+                    continue;
+                pRepr = p->pObjCopies[nFrames*i + nFrames-1-k];
+//                pRepr = p->pObjCopies[nFrames*i + k];
+                if ( pRepr == NULL )
+                    continue;
+                if ( Aig_Regular(pRepr)->fMarkA ) // !pObj is a constr
+                {
+                    pObjNew = Aig_NotCond(pObj, !Aig_IsComplement(pRepr));
+
+                    for ( j = 0; j < k; j++ )
+                        if ( Vec_PtrFind( (Vec_Ptr_t *)Vec_VecEntry(vCands, j), pObjNew ) >= 0 )
+                            break;
+                    if ( j == k )
+                        Vec_VecPush( vCands, k, pObjNew );
+//                    printf( "%d->!%d ", Aig_ObjId(Aig_Regular(pRepr)), Aig_ObjId(pObj) );
+                }
+                else if ( Aig_Regular(pRepr)->fMarkB ) //  pObj is a constr
+                {
+                    pObjNew = Aig_NotCond(pObj,  Aig_IsComplement(pRepr));
+
+                    for ( j = 0; j < k; j++ )
+                        if ( Vec_PtrFind( (Vec_Ptr_t *)Vec_VecEntry(vCands, j), pObjNew ) >= 0  )
+                            break;
+                    if ( j == k )
+                        Vec_VecPush( vCands, k, pObjNew );
+//                    printf( "%d->%d ", Aig_ObjId(Aig_Regular(pRepr)), Aig_ObjId(pObj) );
+                }
+            }
+        }
+
+//        printf( "\n" );
+        if ( fVerbose )
+        {
+            printf( "Found %3d candidates.\n", Vec_VecSizeSize(vCands) );
+            Vec_VecForEachLevel( vCands, vNodes, k )
+            {
+                printf( "Level %d. Cands  =%d    ", k, Vec_PtrSize(vNodes) );
+//                Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+//                    printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+                printf( "\n" );
+            }
+        }
+
+        ABC_FREE( p->pObjCopies );
+        Saig_ManFilterUsingInd( p, vCands, nConfs, nProps, fVerbose );
+        if ( Vec_VecSizeSize(vCands) )
+            printf( "Found %3d constraints after filtering.\n", Vec_VecSizeSize(vCands) );
+        if ( fVerbose )
+        {
+            Vec_VecForEachLevel( vCands, vNodes, k )
+            {
+                printf( "Level %d. Constr =%d    ", k, Vec_PtrSize(vNodes) );
+//                Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+//                    printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
+                printf( "\n" );
+            }
+        }
+    }
+    Vec_PtrFree( vInfo );
+    Cnf_DataFree( pCnf );
+    sat_solver_delete( pSat );
+    Aig_ManCleanMarkAB( pFrames );
+    Aig_ManStop( pFrames );
+    return vCands;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Experimental procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose )
+{
+    Vec_Vec_t * vCands;
+    if ( fOldAlgo )
+        vCands = Saig_ManDetectConstrFunc( p, nFrames, nConfs, nProps, fVerbose );
+    else
+        vCands = Ssw_ManFindDirectImplications( p, nFrames, nConfs, nProps, fVerbose );
+    Vec_VecFreeP( &vCands );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG while unfolding constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose )
+{
+    Aig_Man_t * pNew;
+    Vec_Vec_t * vCands;
+    Vec_Ptr_t * vNodes, * vNewFlops;
+    Aig_Obj_t * pObj;
+    int i, j, k, nNewFlops;
+    if ( fOldAlgo )
+        vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose );
+    else
+        vCands = Ssw_ManFindDirectImplications( pAig, nFrames, nConfs, nProps, fVerbose );
+    if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 )
+    {
+        Vec_VecFreeP( &vCands );
+        return Aig_ManDupDfs( pAig );
+    }
+    // create new manager
+    pNew = Aig_ManDupWithoutPos( pAig );
+    pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands);
+    // add normal POs
+    Saig_ManForEachPo( pAig, pObj, i )
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    // create constraint outputs
+    vNewFlops = Vec_PtrAlloc( 100 );
+    Vec_VecForEachLevel( vCands, vNodes, i )
+    {
+        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
+        {
+            Vec_PtrPush( vNewFlops, Aig_ObjRealCopy(pObj) );
+            for ( j = 0; j < i; j++ )
+                Vec_PtrPush( vNewFlops, Aig_ObjCreatePi(pNew) );
+            Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Vec_PtrPop(vNewFlops) );
+        }
+    }
+    // add latch outputs
+    Saig_ManForEachLi( pAig, pObj, i )
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    // add new latch outputs
+    nNewFlops = 0;
+    Vec_VecForEachLevel( vCands, vNodes, i )
+    {
+        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
+        {
+            for ( j = 0; j < i; j++ )
+                Aig_ObjCreatePo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vNewFlops, nNewFlops++) );
+        }
+    }
+    assert( nNewFlops == Vec_PtrSize(vNewFlops) );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops );
+    Vec_VecFreeP( &vCands );
+    Vec_PtrFree( vNewFlops );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG while unfolding constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose )
+{
+    Aig_Man_t * pAigNew;
+    Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
+    int i;
+    assert( Saig_ManRegNum(pAig) > 0 );
+    if ( Aig_ManConstrNum(pAig) == 0 )
+        return Aig_ManDupDfs( pAig );
+    assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) );
+    // start the new manager
+    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+    pAigNew->pName = Aig_UtilStrsav( pAig->pName );
+    pAigNew->pSpec = Aig_UtilStrsav( pAig->pSpec );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+    // create variables for PIs
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pAigNew );
+    // add internal nodes of this frame
+    Aig_ManForEachNode( pAig, pObj, i )
+        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+
+    // OR the constraint outputs
+    pMiter = Aig_ManConst0( pAigNew );
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
+            continue;
+        pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
+    }
+    // create additional flop
+    pFlopOut = Aig_ObjCreatePi( pAigNew );
+    pFlopIn  = Aig_Or( pAigNew, pMiter, pFlopOut );
+
+    // create primary output
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        if ( i >= Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
+            continue;
+        pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
+        Aig_ObjCreatePo( pAigNew, pMiter );
+    }
+
+    // transfer to register outputs
+    Saig_ManForEachLi( pAig, pObj, i )
+        Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+    // create additional flop 
+    Aig_ObjCreatePo( pAigNew, pFlopIn );
+
+    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 );
+    Aig_ManCleanup( pAigNew );
+    Aig_ManSeqCleanup( pAigNew );
+    return pAigNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+