Added new refinement manager for &gla and &abs_refine.

4 files changed, 727 insertions, 8 deletions

diff --git a/src/aig/gia/giaAbsGla.c b/src/aig/gia/giaAbsGla.c
index 117ad3e0..bc9a0505 100644
--- a/src/aig/gia/giaAbsGla.c
+++ b/src/aig/gia/giaAbsGla.c
@@ -20,6 +20,7 @@
 
 #include "gia.h"
 #include "giaAig.h"
+#include "giaAbsRef.h"
 #include "sat/cnf/cnf.h"
 #include "sat/bsat/satSolver2.h"
 #include "base/main/main.h"
@@ -85,6 +86,9 @@ struct Gla_Man_t_
     Vec_Int_t *    vCoreCounts;     // counts how many times each object appears in the core
     // refinement
     Vec_Int_t *    pvRefis;         // vectors of each object
+    // refinement manager
+    Gia_Man_t *    pGia2;
+    Rnm_Man_t *    pRnm;
     // statistics  
     clock_t        timeInit;
     clock_t        timeSat;
@@ -335,7 +339,44 @@ int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose
 
 
 
+/**Function*************************************************************
+
+  Synopsis    [Prepares CEX and vMap for refinement.]
 
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_GlaPrepareCexAndMap( Gla_Man_t * p, Abc_Cex_t ** ppCex, Vec_Int_t ** pvMap )
+{
+    Abc_Cex_t * pCex;
+    Vec_Int_t * vMap;
+    Gla_Obj_t * pObj, * pFanin;
+    Gia_Obj_t * pGiaObj;
+    int f, i, k;
+    // find PIs and PPIs
+    vMap = Vec_IntAlloc( 1000 );
+    Gla_ManForEachObjAbs( p, pObj, i )
+    {
+        assert( pObj->fConst || pObj->fRo || pObj->fAnd );
+        Gla_ObjForEachFanin( p, pObj, pFanin, k )
+            if ( !pFanin->fAbs )
+                Vec_IntPush( vMap, pFanin->iGiaObj );
+    }
+    Vec_IntUniqify( vMap );
+    // derive counter-example
+    pCex = Abc_CexAlloc( 0, Vec_IntSize(vMap), p->pPars->iFrame+1 );
+    pCex->iFrame = p->pPars->iFrame;
+    for ( f = 0; f <= p->pPars->iFrame; f++ )
+        Gia_ManForEachObjVec( vMap, p->pGia, pGiaObj, k )
+            if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pGiaObj), f ) )
+                Abc_InfoSetBit( pCex->pData, f * Vec_IntSize(vMap) + k );
+    *pvMap = vMap;
+    *ppCex = pCex;
+}
 
 /**Function*************************************************************
 
@@ -358,6 +399,8 @@ Abc_Cex_t * Gla_ManDeriveCex( Gla_Man_t * p, Vec_Int_t * vPis )
     pCex->iFrame = p->pPars->iFrame;
     Gia_ManForEachObjVec( vPis, p->pGia, pObj, i )
     {
+        if ( !Gia_ObjIsPi(p->pGia, pObj) )
+            continue;
         assert( Gia_ObjIsPi(p->pGia, pObj) );
         for ( f = 0; f <= pCex->iFrame; f++ )
             if ( Gla_ObjSatValue( p, Gia_ObjId(p->pGia, pObj), f ) )
@@ -659,6 +702,42 @@ void Gla_ManVerifyUsingTerSim( Gla_Man_t * p, Vec_Int_t * vPis, Vec_Int_t * vPPi
 ***********************************************************************/
 Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
 {
+    Abc_Cex_t * pCex;
+    Vec_Int_t * vMap, * vVec;
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_GlaPrepareCexAndMap( p, &pCex, &vMap );
+    vVec = Rnm_ManRefine( p->pRnm, pCex, vMap, p->pPars->fPropFanout, 1 );
+    Abc_CexFree( pCex );
+    if ( Vec_IntSize(vVec) == 0 )
+    {
+        Vec_IntFree( vVec );
+        Abc_CexFreeP( &p->pGia->pCexSeq );
+        p->pGia->pCexSeq = Gla_ManDeriveCex( p, vMap );
+        Vec_IntFree( vMap );
+        return NULL;
+    }
+    Vec_IntFree( vMap );
+    // remap them into GLA objects
+    Gia_ManForEachObjVec( vVec, p->pGia, pObj, i )
+        Vec_IntWriteEntry( vVec, i, p->pObj2Obj[Gia_ObjId(p->pGia, pObj)] );
+    p->nObjAdded += Vec_IntSize(vVec);
+    return vVec;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs refinement.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gla_ManRefinement2( Gla_Man_t * p )
+{
     int fVerify = 1;
     static int Sign = 0;
     Vec_Int_t * vPis, * vPPis, * vCos, * vRoAnds, * vSelect = NULL;
@@ -795,7 +874,7 @@ Vec_Int_t * Gla_ManRefinement( Gla_Man_t * p )
         Vec_IntFree( vPPis );
         Vec_IntFree( vRoAnds );
         Vec_IntFree( vCos );
-        return 0;
+        return NULL;
     }
 
     // select objects
@@ -1043,7 +1122,7 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
     // create objects 
     p->pObjs    = ABC_CALLOC( Gla_Obj_t, p->nObjs );
     p->pObj2Obj = ABC_FALLOC( unsigned, Gia_ManObjNum(p->pGia) );
-    p->pvRefis  = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(p->pGia) );
+//    p->pvRefis  = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(p->pGia) );
     Gia_ManForEachObj( p->pGia, pObj, i )
     {
         p->pObj2Obj[i] = pObj->Value;
@@ -1103,6 +1182,9 @@ Gla_Man_t * Gla_ManStart( Gia_Man_t * pGia0, Gia_ParVta_t * pPars )
     p->pSat->nLearntRatio = p->pPars->nLearnedPerce;
     p->pSat->nLearntMax   = p->pSat->nLearntStart;
     p->nSatVars  = 1;
+    // start the refinement manager
+//    p->pGia2 = Gia_ManDup( p->pGia );
+    p->pRnm = Rnm_ManStart( p->pGia );
     return p;
 }
 
@@ -1153,7 +1235,7 @@ Gla_Man_t * Gla_ManStart2( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     // create objects 
     p->pObjs    = ABC_CALLOC( Gla_Obj_t, p->nObjs );
     p->pObj2Obj = ABC_FALLOC( unsigned, Gia_ManObjNum(p->pGia) );
-    p->pvRefis  = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(p->pGia) );
+//    p->pvRefis  = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(p->pGia) );
     Gia_ManForEachObj( p->pGia, pObj, i )
     {
         p->pObj2Obj[i] = pObj->Value;
@@ -1213,10 +1295,17 @@ void Gla_ManStop( Gla_Man_t * p )
 {
     Gla_Obj_t * pGla;
     int i;
+
 //    if ( p->pPars->fVerbose )
         Abc_Print( 1, "SAT solver:  Var = %d  Cla = %d  Conf = %d  Lrn = %d  Reduce = %d  Cex = %d  Objs+ = %d\n", 
             sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), 
             sat_solver2_nlearnts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded );
+
+    // stop the refinement manager
+//    Gia_ManStopP( &p->pGia2 );
+    Rnm_ManStop( p->pRnm, 1 );
+
+    if ( p->pvRefis )
     for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
         ABC_FREE( p->pvRefis[i].pArray );
     Gla_ManForEachObj( p, pGla )
@@ -1632,18 +1721,19 @@ void Gla_ManAbsPrintFrame( Gla_Man_t * p, int nCoreSize, int nFrames, int nConfl
 void Gla_ManReportMemory( Gla_Man_t * p )
 {
     Gla_Obj_t * pGla;
-    int i;
+//    int i;
     double memTot = 0;
     double memAig = Gia_ManObjNum(p->pGia) * sizeof(Gia_Obj_t);
     double memSat = sat_solver2_memory( p->pSat, 1 );
     double memPro = sat_solver2_memory_proof( p->pSat );
     double memMap = p->nObjs * sizeof(Gla_Obj_t) + Gia_ManObjNum(p->pGia) * sizeof(int);
-    double memRef = Gia_ManObjNum(p->pGia) * sizeof(Vec_Int_t);
+//    double memRef = Gia_ManObjNum(p->pGia) * sizeof(Vec_Int_t);
+    double memRef = Rnm_ManMemoryUsage( p->pRnm );
     double memOth = sizeof(Gla_Man_t);
     for ( pGla = p->pObjs; pGla < p->pObjs + p->nObjs; pGla++ )
         memMap += Vec_IntCap(&pGla->vFrames) * sizeof(int);
-    for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
-        memRef += Vec_IntCap(&p->pvRefis[i]) * sizeof(int);
+//    for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
+//        memRef += Vec_IntCap(&p->pvRefis[i]) * sizeof(int);
     memOth += Vec_IntCap(p->vAddedNew) * sizeof(int);
     memOth += Vec_IntCap(p->vTemp) * sizeof(int);
     memOth += Vec_IntCap(p->vAbs) * sizeof(int);
@@ -1677,7 +1767,7 @@ void Gia_GlaSendAbsracted( Gla_Man_t * p, int fVerbose )
     assert( Abc_FrameIsBridgeMode() );
 //    if ( fVerbose )
 //        Abc_Print( 1, "Sending abstracted model...\n" );
-    // create abstraction
+    // create abstraction (value of p->pGia is not used here)
     vGateClasses = Gla_ManTranslate( p );
     pAbs = Gia_ManDupAbsGates( p->pGia0, vGateClasses );
     Vec_IntFreeP( &vGateClasses );
diff --git a/src/aig/gia/giaAbsRef.c b/src/aig/gia/giaAbsRef.c
new file mode 100644
index 00000000..2cf90562
--- /dev/null
+++ b/src/aig/gia/giaAbsRef.c
@@ -0,0 +1,561 @@
+/**CFile****************************************************************
+
+  FileName    [giaAbsRef.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Refinement manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaAbsRef.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "giaAbsRef.h"
+
+ABC_NAMESPACE_IMPL_START
+
+/*
+    Description of the refinement manager
+
+    This refinement manager should be 
+    * started by calling Rnm_ManStart()
+       this procedure takes one argument, the user's seq miter as a GIA manager
+       - this manager should not change while the refinement manager is alive
+       - it cannot be used by external applications for any purpose
+       - when the refinement manager stop, GIA manager is the same as at the beginning
+       - in the meantime, it will have some data-structures attached to its nodes...
+    * stopped by calling Rnm_ManStop()
+    * between starting and stopping, refinements are obtained by calling Rnm_ManRefine()
+
+    Procedure Rnm_ManRefine() takes the following arguments:
+    * the refinement manager previously started by Rnm_ManStart()
+    * counter-example (CEX) obtained by abstracting some logic of GIA
+    * mapping (vMap) of inputs of the CEX into the object IDs of the GIA manager
+       - only PI, flop outputs, and internal AND nodes can be used in vMap
+       - the ordering of objects in vMap is not important
+       - however, the index of a non-PI object in vMap is used as its priority
+         (the smaller the index, the more likely this non-PI object apears in a refinement)
+       - only the logic between PO and the objects listed in vMap is traversed by the manager
+         (as a result, GIA can be arbitrarily large, but only objects used in the abstraction
+         and the pseudo-PI, that is, objects in the cut, will be visited by the manager)
+    * flag fPropFanout defines whether value propagation is done through the fanout
+       - it this flag is enabled, theoretically refinement should be better (the result smaller)
+    * flag fVerbose may print some statistics
+
+    The refinement manager returns a minimal-size array of integer IDs of GIA objects
+    which should be added to the abstraction to possibly prevent the given counter-example
+       - only flop output and internal AND nodes from vMap may appear in the resulting array
+       - if the resulting array is empty, the CEX is a true CEX 
+         (in other words, non-PI objects are not needed to set the PO value to 1)
+
+    Verification of the selected refinement is performed by 
+       - initializing all PI objects in vMap to value 0 or 1 they have in the CEX
+       - initializing all remaining objects in vMap to value X
+       - initializing objects used in the refiment to value 0 or 1 they have in the CEX
+       - simulating through as many timeframes as required by the CEX
+       - if the PO value in the last frame is 1, the refinement is correct
+         (however, the minimality of the refinement is not currently checked)
+        
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Rnm_Obj_t_ Rnm_Obj_t; // refinement object
+struct Rnm_Obj_t_
+{
+    unsigned       Value     :  1;  // binary value
+    unsigned       fVisit    :  1;  // visited object
+    unsigned       fPPi      :  1;  // PPI object
+    unsigned       Prio      : 24;  // priority (0 - highest)
+};
+
+struct Rnm_Man_t_
+{
+    // user data
+    Gia_Man_t *    pGia;            // working AIG manager (it is completely owned by this package)
+    Abc_Cex_t *    pCex;            // counter-example
+    Vec_Int_t *    vMap;            // mapping of CEX inputs into objects (PI + PPI, in any order)
+    int            fPropFanout;     // propagate fanouts
+    int            fVerbose;        // verbose flag
+    // traversing data
+    Vec_Int_t *    vObjs;           // internal objects used in value propagation
+    // internal data
+    Rnm_Obj_t *    pObjs;           // refinement objects
+    int            nObjs;           // the number of used objects
+    int            nObjsAlloc;      // the number of allocated objects
+    int            nObjsFrame;      // the number of used objects in each frame
+    int            nCalls;          // total number of calls
+    int            nRefines;        // total refined objects
+    // statistics  
+    clock_t        timeFwd;         // forward propagation
+    clock_t        timeBwd;         // backward propagation
+    clock_t        timeVer;         // ternary simulation
+    clock_t        timeTotal;       // other time
+};
+
+// accessing the refinement object
+static inline Rnm_Obj_t * Rnm_ManObj( Rnm_Man_t * p, Gia_Obj_t * pObj, int f )  
+{ 
+    assert( Gia_ObjIsConst0(pObj) || pObj->Value );
+    assert( (int)pObj->Value < p->nObjsFrame );
+    assert( f >= 0 && f <= p->pCex->iFrame ); 
+    return p->pObjs + f * p->nObjsFrame + pObj->Value;  
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates a new manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia )
+{
+    Rnm_Man_t * p;
+    p = ABC_CALLOC( Rnm_Man_t, 1 );
+    p->pGia = pGia;
+    p->vObjs = Vec_IntAlloc( 100 );
+    p->nObjsAlloc = 10000;
+    p->pObjs = ABC_ALLOC( Rnm_Obj_t, p->nObjsAlloc );
+    Gia_ManStaticFanoutStart( p->pGia );
+    Gia_ManCleanValue(pGia);
+    Gia_ManCleanMark0(pGia);
+    Gia_ManCleanMark1(pGia);
+    return p;
+}
+void Rnm_ManStop( Rnm_Man_t * p, int fProfile )
+{
+    if ( !p ) return;
+    // print runtime statistics
+    if ( fProfile && p->nCalls )
+    {
+        double MemGia = sizeof(Gia_Man_t) + sizeof(Gia_Obj_t) * p->pGia->nObjsAlloc + sizeof(int) * p->pGia->nTravIdsAlloc;
+        double MemOther = sizeof(Rnm_Man_t) + sizeof(Rnm_Obj_t) * p->nObjsAlloc + sizeof(int) * Vec_IntCap(p->vObjs);
+        clock_t timeOther = p->timeTotal - p->timeFwd - p->timeBwd - p->timeVer;
+        printf( "Abstraction refinement runtime statistics:\n" );
+        ABC_PRTP( "Sensetization", p->timeFwd,   p->timeTotal );
+        ABC_PRTP( "Justification", p->timeBwd,   p->timeTotal );
+        ABC_PRTP( "Verification ", p->timeVer,   p->timeTotal );
+        ABC_PRTP( "Other        ", timeOther,    p->timeTotal );
+        ABC_PRTP( "TOTAL        ", p->timeTotal, p->timeTotal );
+        printf( "Total calls = %d.  Average refine = %.1f. GIA mem = %.3f MB.  Other mem = %.3f MB.\n", 
+            p->nCalls, 1.0*p->nRefines/p->nCalls, MemGia/(1<<20), MemOther/(1<<20) );
+    }
+
+    Gia_ManCleanMark0(p->pGia);
+    Gia_ManCleanMark1(p->pGia);
+    Gia_ManStaticFanoutStop(p->pGia);
+    Gia_ManSetPhase(p->pGia);
+    Vec_IntFree( p->vObjs );
+    ABC_FREE( p->pObjs );
+    ABC_FREE( p );
+}
+double Rnm_ManMemoryUsage( Rnm_Man_t * p )
+{
+    return (double)(sizeof(Rnm_Man_t) + sizeof(Rnm_Obj_t) * p->nObjsAlloc + sizeof(int) * Vec_IntCap(p->vObjs));
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Collect internal objects to be used in value propagation.]
+
+  Description [Resulting array vObjs contains RO, AND, PO/RI in a topo order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rnm_ManCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vObjs, int nAddOn )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( Gia_ObjIsCo(pObj) )
+        Rnm_ManCollect_rec( p, Gia_ObjFanin0(pObj), vObjs, nAddOn );
+    else if ( Gia_ObjIsAnd(pObj) )
+    {
+        Rnm_ManCollect_rec( p, Gia_ObjFanin0(pObj), vObjs, nAddOn );
+        Rnm_ManCollect_rec( p, Gia_ObjFanin1(pObj), vObjs, nAddOn );
+    }
+    else if ( !Gia_ObjIsRo(p, pObj) )
+        assert( 0 );
+    pObj->Value = Vec_IntSize(vObjs) + nAddOn;
+    Vec_IntPush( vObjs, Gia_ObjId(p, pObj) );
+}
+void Rnm_ManCollect( Rnm_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    // mark const/PIs/PPIs
+    Gia_ManIncrementTravId( p->pGia );
+    Gia_ObjSetTravIdCurrent( p->pGia, Gia_ManConst0(p->pGia) );
+    Gia_ManConst0(p->pGia)->Value = 0;
+    Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
+    {
+        assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
+        Gia_ObjSetTravIdCurrent( p->pGia, pObj );
+        pObj->Value = 1 + i;
+    }
+    // collect objects
+    Vec_IntClear( p->vObjs );
+    Rnm_ManCollect_rec( p->pGia, Gia_ManPo(p->pGia, 0), p->vObjs, 1 + Vec_IntSize(p->vMap) );
+    Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i )
+        if ( Gia_ObjIsRo(p->pGia, pObj) )
+            Rnm_ManCollect_rec( p->pGia, Gia_ObjRoToRi(p->pGia, pObj), p->vObjs, 1 + Vec_IntSize(p->vMap) );
+    // the last object should be a CO
+    assert( Gia_ObjIsCo(pObj) );
+    assert( (int)pObj->Value == Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) );
+}
+void Rnm_ManCleanValues( Rnm_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
+        pObj->Value = 0;
+    Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i )
+        pObj->Value = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs sensitization analysis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Rnm_ManSensitize( Rnm_Man_t * p )
+{
+    Rnm_Obj_t * pRnm, * pRnm0, * pRnm1;
+    Gia_Obj_t * pObj;
+    int f, i, iBit = p->pCex->nRegs;
+    // const0 is initialized automatically in all timeframes
+    for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis )
+    {
+        Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
+        {
+            assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
+            pRnm = Rnm_ManObj( p, pObj, f );
+            pRnm->Value = Abc_InfoHasBit( p->pCex->pData, iBit + i );
+            if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI
+            {
+                assert( pObj->Value > 0 );
+                pRnm->Prio = pObj->Value;
+                pRnm->fPPi = 1;
+            }
+        }
+        Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i )
+        {
+            assert( Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) );
+            pRnm = Rnm_ManObj( p, pObj, f );
+            assert( !pRnm->fPPi );
+            if ( Gia_ObjIsRo(p->pGia, pObj) )
+            {
+                if ( f == 0 )
+                    continue;
+                pRnm0 = Rnm_ManObj( p, Gia_ObjRoToRi(p->pGia, pObj), f-1 );
+                pRnm->Value = pRnm0->Value;
+                pRnm->Prio  = pRnm0->Prio;
+                continue;
+            }
+            if ( Gia_ObjIsCo(pObj) )
+            {
+                pRnm0 = Rnm_ManObj( p, Gia_ObjFanin0(pObj), f );
+                pRnm->Value = (pRnm0->Value ^ Gia_ObjFaninC0(pObj));
+                pRnm->Prio  = pRnm0->Prio;
+                continue;
+            }
+            assert( Gia_ObjIsAnd(pObj) );
+            pRnm0 = Rnm_ManObj( p, Gia_ObjFanin0(pObj), f );
+            pRnm1 = Rnm_ManObj( p, Gia_ObjFanin1(pObj), f );
+            pRnm->Value = (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) & (pRnm1->Value ^ Gia_ObjFaninC1(pObj));
+            if ( pRnm->Value == 1 )
+                pRnm->Prio  = Abc_MaxInt( pRnm0->Prio, pRnm1->Prio );
+            else if ( (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRnm1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
+                pRnm->Prio  = Abc_MinInt( pRnm0->Prio, pRnm1->Prio ); // choice
+            else if ( (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) == 0 )
+                pRnm->Prio  = pRnm0->Prio;
+            else 
+                pRnm->Prio  = pRnm1->Prio;
+        }
+    }
+    assert( iBit == p->pCex->nBits );
+    pRnm = Rnm_ManObj( p, Gia_ManPo(p->pGia, 0), p->pCex->iFrame );
+    if ( pRnm->Value != 1 )
+        printf( "Output value is incorrect.\n" );
+    return pRnm->Prio;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Drive implications of the given node towards primary outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rnm_ManJustifyPropFanout_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect )
+{
+    Rnm_Obj_t * pRnm0, * pRnm1, * pRnm = Rnm_ManObj( p, pObj, f );
+    Gia_Obj_t * pFanout;
+    int i, k;//, Id = Gia_ObjId(p->pGia, pObj);
+    assert( pRnm->fVisit == 0 );
+    pRnm->fVisit = 1;
+    if ( pRnm->fPPi )
+    {
+        assert( (int)pRnm->Prio > 0 );
+        for ( i = p->pCex->iFrame; i >= 0; i-- )
+            if ( !Rnm_ManObj(p, pObj, i)->fVisit )
+                Rnm_ManJustifyPropFanout_rec( p, pObj, i, vSelect );
+        Vec_IntPush( vSelect, Gia_ObjId(p->pGia, pObj) );
+        return;
+    }
+    if ( (Gia_ObjIsCo(pObj) && f == p->pCex->iFrame) || Gia_ObjIsPo(p->pGia, pObj) )
+        return;
+    if ( Gia_ObjIsRi(p->pGia, pObj) )
+    {
+        pFanout = Gia_ObjRiToRo(p->pGia, pObj);
+        if ( !Rnm_ManObj(p, pFanout, f+1)->fVisit )
+            Rnm_ManJustifyPropFanout_rec( p, pFanout, f+1, vSelect );
+        return;
+    }
+    assert( Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) );
+    Gia_ObjForEachFanoutStatic( p->pGia, pObj, pFanout, k )
+    {
+        Rnm_Obj_t * pRnmF;
+        if ( pFanout->Value == 0 )
+            continue;
+        pRnmF = Rnm_ManObj(p, pFanout, f);
+        if ( pRnmF->fPPi || pRnmF->fVisit )
+            continue;
+        if ( Gia_ObjIsCo(pFanout) )
+        {
+            Rnm_ManJustifyPropFanout_rec( p, pFanout, f, vSelect );
+            continue;
+        } 
+        assert( Gia_ObjIsAnd(pFanout) );
+        pRnm0 = Rnm_ManObj( p, Gia_ObjFanin0(pFanout), f );
+        pRnm1 = Rnm_ManObj( p, Gia_ObjFanin1(pFanout), f );
+        if ( ((pRnm0->Value ^ Gia_ObjFaninC0(pFanout)) == 0 && pRnm0->fVisit) ||
+             ((pRnm1->Value ^ Gia_ObjFaninC1(pFanout)) == 0 && pRnm1->fVisit) || 
+           ( ((pRnm0->Value ^ Gia_ObjFaninC0(pFanout)) == 1 && pRnm0->fVisit) && 
+             ((pRnm1->Value ^ Gia_ObjFaninC1(pFanout)) == 1 && pRnm1->fVisit) ) )
+           Rnm_ManJustifyPropFanout_rec( p, pFanout, f, vSelect );
+    }
+}
+void Rnm_ManJustify_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect )
+{ 
+    Rnm_Obj_t * pRnm = Rnm_ManObj( p, pObj, f );
+    int i;//, Id = Gia_ObjId(p->pGia, pObj);
+    if ( pRnm->fVisit )
+        return;
+    if ( p->fPropFanout )
+        Rnm_ManJustifyPropFanout_rec( p, pObj, f, vSelect );
+    else
+        pRnm->fVisit = 1;
+    if ( pRnm->fPPi )
+    {
+        assert( (int)pRnm->Prio > 0 );
+        if ( p->fPropFanout )
+        {
+            for ( i = p->pCex->iFrame; i >= 0; i-- )
+                if ( !Rnm_ManObj(p, pObj, i)->fVisit )
+                    Rnm_ManJustifyPropFanout_rec( p, pObj, i, vSelect );
+        }
+        else
+        {
+            Vec_IntPush( vSelect, Gia_ObjId(p->pGia, pObj) );
+//            for ( i = p->pCex->iFrame; i >= 0; i-- )
+//                Rnm_ManObj(p, pObj, i)->fVisit = 1;
+        }
+        return;
+    }
+    if ( Gia_ObjIsPi(p->pGia, pObj) || Gia_ObjIsConst0(pObj) )
+        return;
+    if ( Gia_ObjIsRo(p->pGia, pObj) )
+    {
+        if ( f > 0 )
+            Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj)), f-1, vSelect );
+        return;
+    }
+    if ( Gia_ObjIsAnd(pObj) )
+    {
+        Rnm_Obj_t * pRnm0 = Rnm_ManObj( p, Gia_ObjFanin0(pObj), f );
+        Rnm_Obj_t * pRnm1 = Rnm_ManObj( p, Gia_ObjFanin1(pObj), f );
+        if ( pRnm->Value == 1 )
+        {
+            if ( pRnm0->Prio > 0 )
+                Rnm_ManJustify_rec( p, Gia_ObjFanin0(pObj), f, vSelect );
+            if ( pRnm1->Prio > 0 )
+                Rnm_ManJustify_rec( p, Gia_ObjFanin1(pObj), f, vSelect );
+        }
+        else // select one value
+        {
+            if ( (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRnm1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
+            {
+                if ( pRnm0->Prio <= pRnm1->Prio ) // choice
+                {
+                    if ( pRnm0->Prio > 0 )
+                        Rnm_ManJustify_rec( p, Gia_ObjFanin0(pObj), f, vSelect );
+                }
+                else
+                {
+                    if ( pRnm1->Prio > 0 )
+                        Rnm_ManJustify_rec( p, Gia_ObjFanin1(pObj), f, vSelect );
+                }
+            }
+            else if ( (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) == 0 )
+            {
+                if ( pRnm0->Prio > 0 )
+                    Rnm_ManJustify_rec( p, Gia_ObjFanin0(pObj), f, vSelect );
+            }
+            else if ( (pRnm1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
+            {
+                if ( pRnm1->Prio > 0 )
+                    Rnm_ManJustify_rec( p, Gia_ObjFanin1(pObj), f, vSelect );
+            }
+            else assert( 0 );
+        }
+    }
+    else assert( 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs refinement.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Rnm_ManVerifyUsingTerSim( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, Vec_Int_t * vObjs, Vec_Int_t * vRes )
+{
+    Gia_Obj_t * pObj;
+    int i, f, iBit = pCex->nRegs;
+    Gia_ObjTerSimSet0( Gia_ManConst0(p) );
+    for ( f = 0; f <= pCex->iFrame; f++, iBit += pCex->nPis )
+    {
+        Gia_ManForEachObjVec( vMap, p, pObj, i )
+        {
+            pObj->fPhase = Abc_InfoHasBit( pCex->pData, iBit + i );
+            if ( !Gia_ObjIsPi(p, pObj) )
+                Gia_ObjTerSimSetX( pObj );
+            else if ( pObj->fPhase )
+                Gia_ObjTerSimSet1( pObj );
+            else
+                Gia_ObjTerSimSet0( pObj );
+        }
+        Gia_ManForEachObjVec( vRes, p, pObj, i )
+        {
+            if ( pObj->fPhase )
+                Gia_ObjTerSimSet1( pObj );
+            else
+                Gia_ObjTerSimSet0( pObj );
+        }
+        Gia_ManForEachObjVec( vObjs, p, pObj, i )
+        {
+            if ( Gia_ObjIsCo(pObj) )
+                Gia_ObjTerSimCo( pObj );
+            else if ( Gia_ObjIsAnd(pObj) )
+                Gia_ObjTerSimAnd( pObj );
+            else if ( f == 0 )
+                Gia_ObjTerSimSet0( pObj );
+            else
+                Gia_ObjTerSimRo( p, pObj );
+        }
+    }
+    pObj = Gia_ManPo( p, 0 );
+    if ( !Gia_ObjTerSimGet1(pObj) )
+        Abc_Print( 1, "\nRefinement verification has failed!!!\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the refinement for a given counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose )
+{
+    Vec_Int_t * vSelected = Vec_IntAlloc( 100 );
+    clock_t clk, clk2 = clock();
+    p->nCalls++;
+    // initialize
+    p->pCex = pCex;
+    p->vMap = vMap;
+    p->fPropFanout = fPropFanout;
+    p->fVerbose    = fVerbose;
+    // collects used objects
+    Rnm_ManCollect( p );
+    // initialize datastructure
+    p->nObjsFrame = 1 + Vec_IntSize(vMap) + Vec_IntSize(p->vObjs);
+    p->nObjs = p->nObjsFrame * (pCex->iFrame + 1);
+    if ( p->nObjs > p->nObjsAlloc )
+        p->pObjs = ABC_REALLOC( Rnm_Obj_t, p->pObjs, (p->nObjsAlloc = p->nObjs + 10000) );
+    memset( p->pObjs, 0, sizeof(Rnm_Obj_t) * p->nObjs );
+    // propagate priorities
+    clk = clock();
+    if ( Rnm_ManSensitize( p ) ) // the CEX is not a true CEX
+    {
+        p->timeFwd += clock() - clk;
+        // select refinement
+        clk = clock();
+        Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), pCex->iFrame, vSelected );
+        p->timeBwd += clock() - clk;
+    }
+    // clean values
+    Rnm_ManCleanValues( p );
+    // verify (empty) refinement
+    clk = clock();
+    Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected );
+    Vec_IntUniqify( vSelected );
+//    Vec_IntReverseOrder( vSelected );
+    p->timeVer += clock() - clk;
+    p->timeTotal += clock() - clk2;
+    p->nRefines += Vec_IntSize(vSelected);
+    return vSelected;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaAbsRef.h b/src/aig/gia/giaAbsRef.h
new file mode 100644
index 00000000..26992dac
--- /dev/null
+++ b/src/aig/gia/giaAbsRef.h
@@ -0,0 +1,67 @@
+/**CFile****************************************************************
+
+  FileName    [giaAbsRef.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Refinement manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaAbsRef.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__aig__gia__giaAbsRef_h
+#define ABC__aig__gia__giaAbsRef_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Rnm_Man_t_ Rnm_Man_t; // refinement manager
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== giaAbsRef.c ===========================================================*/
+extern Rnm_Man_t *  Rnm_ManStart( Gia_Man_t * pGia );
+extern void         Rnm_ManStop( Rnm_Man_t * p, int fProfile );
+extern double       Rnm_ManMemoryUsage( Rnm_Man_t * p );
+extern Vec_Int_t *  Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fVerbose );
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index e54a30d4..dc5ec192 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -1,6 +1,7 @@
 SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaAbs.c \
     src/aig/gia/giaAbsGla.c \
+    src/aig/gia/giaAbsRef.c \
     src/aig/gia/giaAbsVta.c \
     src/aig/gia/giaAig.c \
     src/aig/gia/giaAiger.c \