Scalable gate-level abstraction.

2 files changed, 108 insertions, 102 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 6abda070..e206993f 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -292,31 +292,31 @@ static inline void Gia_ManTruthNot( unsigned * pOut, unsigned * pIn, int nVars )
         pOut[w] = ~pIn[w];
 }
 
-static inline Gia_Obj_t *  Gia_Regular( Gia_Obj_t * p )        { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }
-static inline Gia_Obj_t *  Gia_Not( Gia_Obj_t * p )            { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^  01); }
-static inline Gia_Obj_t *  Gia_NotCond( Gia_Obj_t * p, int c ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); }
-static inline int          Gia_IsComplement( Gia_Obj_t * p )   { return (int)((ABC_PTRUINT_T)(p) & 01);          }
-
-static inline int          Gia_ManCiNum( Gia_Man_t * p )       { return Vec_IntSize(p->vCis);  }
-static inline int          Gia_ManCoNum( Gia_Man_t * p )       { return Vec_IntSize(p->vCos);  }
-static inline int          Gia_ManPiNum( Gia_Man_t * p )       { return Vec_IntSize(p->vCis) - p->nRegs;  }
-static inline int          Gia_ManPoNum( Gia_Man_t * p )       { return Vec_IntSize(p->vCos) - p->nRegs;  }
-static inline int          Gia_ManRegNum( Gia_Man_t * p )      { return p->nRegs;              }
-static inline int          Gia_ManObjNum( Gia_Man_t * p )      { return p->nObjs;              }
-static inline int          Gia_ManAndNum( Gia_Man_t * p )      { return p->nObjs - Vec_IntSize(p->vCis) - Vec_IntSize(p->vCos) - 1;  }
-static inline int          Gia_ManCandNum( Gia_Man_t * p )     { return Gia_ManCiNum(p) + Gia_ManAndNum(p);                          }
-static inline int          Gia_ManConstrNum( Gia_Man_t * p )   { return p->nConstrs;           }
-static inline void         Gia_ManFlipVerbose( Gia_Man_t * p ) { p->fVerbose ^= 1;             } 
-
-static inline Gia_Obj_t *  Gia_ManConst0( Gia_Man_t * p )      { return p->pObjs;                                               }
-static inline Gia_Obj_t *  Gia_ManConst1( Gia_Man_t * p )      { return Gia_Not(Gia_ManConst0(p));                              }
-static inline Gia_Obj_t *  Gia_ManObj( Gia_Man_t * p, int v )  { assert( v < p->nObjs ); return p->pObjs + v;                   }
-static inline Gia_Obj_t *  Gia_ManCi( Gia_Man_t * p, int v )   { return Gia_ManObj( p, Vec_IntEntry(p->vCis,v) );  }
-static inline Gia_Obj_t *  Gia_ManCo( Gia_Man_t * p, int v )   { return Gia_ManObj( p, Vec_IntEntry(p->vCos,v) );  }
-static inline Gia_Obj_t *  Gia_ManPi( Gia_Man_t * p, int v )   { assert( v < Gia_ManPiNum(p) );  return Gia_ManCi( p, v );      }
-static inline Gia_Obj_t *  Gia_ManPo( Gia_Man_t * p, int v )   { assert( v < Gia_ManPoNum(p) );  return Gia_ManCo( p, v );      }
-static inline Gia_Obj_t *  Gia_ManRo( Gia_Man_t * p, int v )   { assert( v < Gia_ManRegNum(p) ); return Gia_ManCi( p, Gia_ManPiNum(p)+v );      }
-static inline Gia_Obj_t *  Gia_ManRi( Gia_Man_t * p, int v )   { assert( v < Gia_ManRegNum(p) ); return Gia_ManCo( p, Gia_ManPoNum(p)+v );      }
+static inline Gia_Obj_t *  Gia_Regular( Gia_Obj_t * p )        { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) & ~01);                           }
+static inline Gia_Obj_t *  Gia_Not( Gia_Obj_t * p )            { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^  01);                           }
+static inline Gia_Obj_t *  Gia_NotCond( Gia_Obj_t * p, int c ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c));                           }
+static inline int          Gia_IsComplement( Gia_Obj_t * p )   { return (int)((ABC_PTRUINT_T)(p) & 01);                                    }
+
+static inline int          Gia_ManCiNum( Gia_Man_t * p )       { return Vec_IntSize(p->vCis);                                              }
+static inline int          Gia_ManCoNum( Gia_Man_t * p )       { return Vec_IntSize(p->vCos);                                              }
+static inline int          Gia_ManPiNum( Gia_Man_t * p )       { return Vec_IntSize(p->vCis) - p->nRegs;                                   }
+static inline int          Gia_ManPoNum( Gia_Man_t * p )       { return Vec_IntSize(p->vCos) - p->nRegs;                                   }
+static inline int          Gia_ManRegNum( Gia_Man_t * p )      { return p->nRegs;                                                          }
+static inline int          Gia_ManObjNum( Gia_Man_t * p )      { return p->nObjs;                                                          }
+static inline int          Gia_ManAndNum( Gia_Man_t * p )      { return p->nObjs - Vec_IntSize(p->vCis) - Vec_IntSize(p->vCos) - 1;        }
+static inline int          Gia_ManCandNum( Gia_Man_t * p )     { return Gia_ManCiNum(p) + Gia_ManAndNum(p);                                }
+static inline int          Gia_ManConstrNum( Gia_Man_t * p )   { return p->nConstrs;                                                       }
+static inline void         Gia_ManFlipVerbose( Gia_Man_t * p ) { p->fVerbose ^= 1;                                                         } 
+
+static inline Gia_Obj_t *  Gia_ManConst0( Gia_Man_t * p )      { return p->pObjs;                                                          }
+static inline Gia_Obj_t *  Gia_ManConst1( Gia_Man_t * p )      { return Gia_Not(Gia_ManConst0(p));                                         }
+static inline Gia_Obj_t *  Gia_ManObj( Gia_Man_t * p, int v )  { assert( v >= 0 && v < p->nObjs ); return p->pObjs + v;                    }
+static inline Gia_Obj_t *  Gia_ManCi( Gia_Man_t * p, int v )   { return Gia_ManObj( p, Vec_IntEntry(p->vCis,v) );                          }
+static inline Gia_Obj_t *  Gia_ManCo( Gia_Man_t * p, int v )   { return Gia_ManObj( p, Vec_IntEntry(p->vCos,v) );                          }
+static inline Gia_Obj_t *  Gia_ManPi( Gia_Man_t * p, int v )   { assert( v < Gia_ManPiNum(p) );  return Gia_ManCi( p, v );                 }
+static inline Gia_Obj_t *  Gia_ManPo( Gia_Man_t * p, int v )   { assert( v < Gia_ManPoNum(p) );  return Gia_ManCo( p, v );                 }
+static inline Gia_Obj_t *  Gia_ManRo( Gia_Man_t * p, int v )   { assert( v < Gia_ManRegNum(p) ); return Gia_ManCi( p, Gia_ManPiNum(p)+v ); }
+static inline Gia_Obj_t *  Gia_ManRi( Gia_Man_t * p, int v )   { assert( v < Gia_ManRegNum(p) ); return Gia_ManCo( p, Gia_ManPoNum(p)+v ); }
 
 static inline int          Gia_ObjIsTerm( Gia_Obj_t * pObj )                   { return pObj->fTerm;                             } 
 static inline int          Gia_ObjIsAndOrConst0( Gia_Obj_t * pObj )            { return!pObj->fTerm;                             } 
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c
index 65bc472f..da36b849 100644
--- a/src/aig/gia/giaAbsGla2.c
+++ b/src/aig/gia/giaAbsGla2.c
@@ -44,9 +44,9 @@ struct Ga2_Man_t_
     Vec_Ptr_t *    vCnfs;        // for each object: CNF0, CNF1
     // abstraction
     Vec_Int_t *    vIds;         // abstraction ID for each GIA object
+    Vec_Int_t *    vProofIds;    // mapping of GIA objects into their proof IDs
     Vec_Int_t *    vAbs;         // array of abstracted objects
     Vec_Int_t *    vValues;      // array of objects with abstraction ID assigned
-    Vec_Int_t *    vProofIds;    // mapping of GIA objects into their proof IDs
     int            nProofIds;    // the counter of proof IDs
     int            LimAbs;       // limit value for starting abstraction objects
     int            LimPpi;       // limit value for starting PPI objects
@@ -82,13 +82,13 @@ static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj )
 static inline int         Ga2_ObjId( Ga2_Man_t * p, Gia_Obj_t * pObj )           { return Vec_IntEntry(p->vIds, Gia_ObjId(p->pGia, pObj));                                                  }
 static inline void        Ga2_ObjSetId( Ga2_Man_t * p, Gia_Obj_t * pObj, int i ) { Vec_IntWriteEntry(p->vIds, Gia_ObjId(p->pGia, pObj), i);                                                 }
 
-static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj )         { assert(Ga2_ObjId(p,pObj)); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)   );                       }
-static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj )         { assert(Ga2_ObjId(p,pObj)); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)+1 );                       }
+static inline Vec_Int_t * Ga2_ObjCnf0( Ga2_Man_t * p, Gia_Obj_t * pObj )         { assert(Ga2_ObjId(p,pObj) >= 0); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)   );                  }
+static inline Vec_Int_t * Ga2_ObjCnf1( Ga2_Man_t * p, Gia_Obj_t * pObj )         { assert(Ga2_ObjId(p,pObj) >= 0); return Vec_PtrEntry( p->vCnfs, 2*Ga2_ObjId(p,pObj)+1 );                  }
 
-static inline int         Ga2_ObjIsAbs0( Ga2_Man_t * p, Gia_Obj_t * pObj )       { assert(Ga2_ObjId(p,pObj)); return Ga2_ObjId(p,pObj) <  p->LimAbs;                                        }
-static inline int         Ga2_ObjIsLeaf0( Ga2_Man_t * p, Gia_Obj_t * pObj )      { assert(Ga2_ObjId(p,pObj)); return Ga2_ObjId(p,pObj) >= p->LimAbs && Ga2_ObjId(p,pObj) < p->LimPpi;       }
-static inline int         Ga2_ObjIsAbs( Ga2_Man_t * p, Gia_Obj_t * pObj )        { return Ga2_ObjId(p,pObj) && Ga2_ObjCnf0(p,pObj);                                                         }
-static inline int         Ga2_ObjIsLeaf( Ga2_Man_t * p, Gia_Obj_t * pObj )       { return Ga2_ObjId(p,pObj) && !Ga2_ObjCnf0(p,pObj);                                                        }
+static inline int         Ga2_ObjIsAbs0( Ga2_Man_t * p, Gia_Obj_t * pObj )       { assert(Ga2_ObjId(p,pObj) >= 0); return Ga2_ObjId(p,pObj) >= 0         && Ga2_ObjId(p,pObj) < p->LimAbs;  }
+static inline int         Ga2_ObjIsLeaf0( Ga2_Man_t * p, Gia_Obj_t * pObj )      { assert(Ga2_ObjId(p,pObj) >= 0); return Ga2_ObjId(p,pObj) >= p->LimAbs && Ga2_ObjId(p,pObj) < p->LimPpi;  }
+static inline int         Ga2_ObjIsAbs( Ga2_Man_t * p, Gia_Obj_t * pObj )        { return Ga2_ObjId(p,pObj) >= 0 &&  Ga2_ObjCnf0(p,pObj);                                                   }
+static inline int         Ga2_ObjIsLeaf( Ga2_Man_t * p, Gia_Obj_t * pObj )       { return Ga2_ObjId(p,pObj) >= 0 && !Ga2_ObjCnf0(p,pObj);                                                   }
 
 static inline Vec_Int_t * Ga2_MapFrameMap( Ga2_Man_t * p, int f )                { return (Vec_Int_t *)Vec_PtrEntry( p->vId2Lit, f );                                                       }
 
@@ -96,7 +96,7 @@ static inline Vec_Int_t * Ga2_MapFrameMap( Ga2_Man_t * p, int f )
 static inline int Ga2_ObjFindLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )  
 { 
     int Id = Ga2_ObjId(p,pObj);
-    assert( Ga2_ObjId(p,pObj) && Ga2_ObjId(p,pObj) < Vec_IntSize(p->vValues) );
+    assert( Ga2_ObjId(p,pObj) >= 0 && Ga2_ObjId(p,pObj) < Vec_IntSize(p->vValues) );
     if ( f == Vec_PtrSize(p->vId2Lit) )
         Vec_PtrPush( p->vId2Lit, Vec_IntStartFull(Vec_IntSize(p->vValues)) );
     assert( f < Vec_PtrSize(p->vId2Lit) );
@@ -105,6 +105,7 @@ static inline int Ga2_ObjFindLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
 // inserts literal of this object
 static inline void Ga2_ObjAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int Lit )  
 { 
+//    assert( Lit > 1 || Gia_ObjIsConst0(pObj) );
     assert( Lit > 1 );
     assert( Ga2_ObjFindLit(p, pObj, f) == -1 );
     Vec_IntSetEntry( Ga2_MapFrameMap(p, f), Ga2_ObjId(p,pObj), Lit );
@@ -118,6 +119,7 @@ static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
         Lit = toLitCond( p->nSatVars++, 0 );
         Ga2_ObjAddLit( p, pObj, f, Lit );
     }
+//    assert( Lit > 1 || Gia_ObjIsConst0(pObj)  );
     assert( Lit > 1 );
     return Lit;
 }
@@ -280,9 +282,21 @@ int Ga2_ManMarkup( Gia_Man_t * p, int N )
             Ga2_ManBreakTree_rec( p, pObj, 1, N );
     }
     // verify that the tree is split correctly
-    CountMarks = 0;
     Vec_IntFreeP( &p->vMapping );
     p->vMapping = Vec_IntStart( Gia_ManObjNum(p) );
+    Gia_ManForEachRo( p, pObj, i )
+    {
+        Gia_Obj_t * pObjRi = Gia_ObjRoToRi(p, pObj);
+        assert( pObj->fPhase );
+        assert( Gia_ObjFanin0(pObjRi)->fPhase );
+        // create map
+        Vec_IntWriteEntry( p->vMapping, Gia_ObjId(p, pObj), Vec_IntSize(p->vMapping) );
+        Vec_IntPush( p->vMapping, 1 );
+        Vec_IntPush( p->vMapping, Gia_ObjFaninId0p(p, pObjRi) );
+        Vec_IntPush( p->vMapping, Gia_ObjFaninC0(pObjRi) ? 0x55555555 : 0xAAAAAAAA );
+        Vec_IntPush( p->vMapping, -1 );  // placeholder for ref counter
+    }
+    CountMarks = Gia_ManRegNum(p);
     Gia_ManForEachAnd( p, pObj, i )
     {
         if ( !pObj->fPhase )
@@ -352,16 +366,18 @@ Ga2_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
     p->pGia      = pGia;
     p->pPars     = pPars;
     // markings 
-    p->nMarked   = Ga2_ManMarkup( pGia, 5 ) + Gia_ManRegNum( p->pGia );
+    p->nMarked   = Ga2_ManMarkup( pGia, 5 );
     p->vCnfs     = Vec_PtrAlloc( 1000 );
     Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) );
     Vec_PtrPush( p->vCnfs, Vec_IntAlloc(0) );
     // abstraction
-    p->vIds      = Vec_IntStart( Gia_ManObjNum(pGia) );
+    p->vIds      = Vec_IntStartFull( Gia_ManObjNum(pGia) );
+    p->vProofIds = Vec_IntAlloc(0);
     p->vAbs      = Vec_IntAlloc( 1000 );
     p->vValues   = Vec_IntAlloc( 1000 );
-    p->vProofIds = Vec_IntAlloc(0);
-    Vec_IntPush( p->vValues, -1 );
+    // add constant
+    Ga2_ObjSetId( p, Gia_ManConst0(pGia), 0 );
+    Vec_IntPush( p->vValues, 0 );
     // refinement
     p->pRnm      = Rnm_ManStart( pGia );
     // SAT solver and variables
@@ -383,9 +399,9 @@ void Ga2_ManReportMemory( Ga2_Man_t * p )
     double memOth = sizeof(Ga2_Man_t);
     memOth += Vec_VecMemoryInt( (Vec_Vec_t *)p->vCnfs );
     memOth += Vec_IntMemory( p->vIds );
+    memOth += Vec_IntMemory( p->vProofIds );
     memOth += Vec_IntMemory( p->vAbs );
     memOth += Vec_IntMemory( p->vValues );
-    memOth += Vec_IntMemory( p->vProofIds );
     memOth += Vec_IntMemory( p->vLits );
     memOth += Vec_IntMemory( p->vIsopMem );
     memOth += 336450 + (sizeof(char) + sizeof(char*)) * 65536;
@@ -411,8 +427,8 @@ void Ga2_ManStop( Ga2_Man_t * p )
     Vec_VecFree( (Vec_Vec_t *)p->vCnfs );
     Vec_VecFree( (Vec_Vec_t *)p->vId2Lit );
     Vec_IntFree( p->vIds );
-    Vec_IntFree( p->vAbs );
     Vec_IntFree( p->vProofIds );
+    Vec_IntFree( p->vAbs );
     Vec_IntFree( p->vValues );
     Vec_IntFree( p->vLits );
     Vec_IntFree( p->vIsopMem );
@@ -631,7 +647,7 @@ void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs )
         int s = 0;
     }
     // assign abstraction ID to the node
-    if ( Ga2_ObjId(p,pObj) == 0 )
+    if ( Ga2_ObjId(p,pObj) == -1 )
     {
         Ga2_ObjSetId( p, pObj, Vec_IntSize(p->vValues) );
         Vec_IntPush( p->vValues, Gia_ObjId(p->pGia, pObj) );
@@ -643,9 +659,7 @@ void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs )
         return;
     assert( Vec_IntFind(p->vAbs, Gia_ObjId(p->pGia, pObj)) == -1 );
     Vec_IntPush( p->vAbs, Gia_ObjId(p->pGia, pObj) );
-    if ( Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsConst0(pObj) )
-        return;
-    assert( Gia_ObjIsAnd(pObj) );
+    assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
     // compute parameters
     nLeaves = Ga2_ObjLeaveNum(p->pGia, pObj);
     uTruth = Ga2_ObjTruth( p->pGia, pObj );
@@ -654,11 +668,47 @@ void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int fAbs )
     Vec_PtrWriteEntry( p->vCnfs, 2 * Ga2_ObjId(p,pObj) + 1, Ga2_ManCnfCompute(~uTruth, nLeaves, p->vIsopMem) );
 }
 
+void Ga2_ManAddToAbsOneStatic( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
+{
+    Vec_Int_t * vLeaves;
+    Gia_Obj_t * pFanin;
+    int k, iLitOut = Ga2_ObjFindOrAddLit( p, pObj, f );
+    assert( iLitOut > 1 );
+    assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(p->pGia, pObj) );
+    if ( f == 0 && Gia_ObjIsRo(p->pGia, pObj) )
+    {
+        iLitOut = Abc_LitNot( iLitOut );
+        sat_solver2_addclause( p->pSat, &iLitOut, &iLitOut + 1, Gia_ObjId(p->pGia, pObj) );
+    }
+    else
+    {
+        vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
+        Vec_IntClear( p->vLits );
+        Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
+            Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f - Gia_ObjIsRo(p->pGia, pObj) ) );
+        Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) );
+    }
+}
+
+void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
+{
+    Gia_Obj_t * pObj;
+    int i;
+//    Ga2_ObjAddLit( p, Gia_ManConst0(p->pGia), f, 0 );
+    int Lit = Ga2_ObjFindOrAddLit( p, Gia_ManConst0(p->pGia), f );
+    Lit = Abc_LitNot( Lit );
+    sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, 0 );
+
+    Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
+        if ( i >= p->LimAbs )
+            Ga2_ManAddToAbsOneStatic( p, pObj, f );
+}
+
 void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
 {
     Vec_Int_t * vLeaves, * vMap;
     Gia_Obj_t * pObj, * pFanin;
-    int f, i, k, iLitOut;
+    int f, i, k;
     // add abstraction objects
     Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
     {
@@ -669,6 +719,7 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
     // add PPI objects
     Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
     {
+/*
         if ( Gia_ObjIsRo(p->pGia, pObj) )
         {
             pFanin = Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj));
@@ -676,9 +727,10 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
                 Ga2_ManSetupNode( p, pFanin, 0 );
             continue;
         }
+*/
         vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
         Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
-            if ( !Ga2_ObjId( p, pFanin ) )
+            if ( Ga2_ObjId( p, pFanin ) == -1 )
                 Ga2_ManSetupNode( p, pFanin, 0 );
     }
     // clean mapping in the timeframes
@@ -686,51 +738,8 @@ void Ga2_ManAddToAbs( Ga2_Man_t * p, Vec_Int_t * vToAdd )
         Vec_IntFillExtra( vMap, Vec_IntSize(p->vValues), -1 );
     // add new clauses to the timeframes
     for ( f = 0; f <= p->pPars->iFrame; f++ )
-    Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
-    {
-        iLitOut =  Ga2_ObjFindOrAddLit( p, pObj, f );
-        assert( iLitOut > 1 );
-        if ( Gia_ObjIsRo(p->pGia, pObj) )
-        {
-            if ( f == 0 )
-            {
-                iLitOut = Abc_LitNot( iLitOut );
-                sat_solver2_addclause( p->pSat, &iLitOut, &iLitOut + 1, Gia_ObjId(p->pGia, pObj) );
-            }
-            else
-            {
-                Gia_Obj_t * pObjRi = Gia_ObjRoToRi( p->pGia, pObj );
-                int iFanLit = Ga2_ObjFindOrAddLit( p, Gia_ObjFanin0(pObjRi), f-1 );
-                int fCompl = Abc_LitIsCompl(iLitOut) ^ Abc_LitIsCompl(iFanLit) ^ Gia_ObjFaninC0(pObjRi);
-                sat_solver2_add_buffer( p->pSat, Abc_Lit2Var(iLitOut), Abc_Lit2Var(iFanLit), fCompl, 0, Gia_ObjId(p->pGia, pObj) );
-            }
-            continue;
-        }
-        assert( Gia_ObjIsAnd(pObj) );
-        vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
-        Vec_IntClear( p->vLits );
-        Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
-            Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f ) );
-        Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) );
-    }
-}
-
-void Ga2_ManAddAbsClauses( Ga2_Man_t * p, int f )
-{
-    Vec_Int_t * vLeaves;
-    Gia_Obj_t * pObj, * pFanin;
-    int i, k, iLitOut;
-    Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
-    {
-        if ( i < p->LimAbs )
-            continue;
-        vLeaves = Ga2_ObjLeaves( p->pGia, pObj );
-        Vec_IntClear( p->vLits );
-        Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k )
-            Vec_IntPush( p->vLits, Ga2_ObjFindOrAddLit( p, pFanin, f ) );
-        iLitOut =  Ga2_ObjFindOrAddLit( p, pObj, f );
-        Ga2_ManCnfAddStatic( p, Ga2_ObjCnf0(p, pObj), Ga2_ObjCnf1(p, pObj), Vec_IntArray(p->vLits), iLitOut, Gia_ObjId(p->pGia, pObj) );
-    }
+        Gia_ManForEachObjVec( vToAdd, p->pGia, pObj, i )
+            Ga2_ManAddToAbsOneStatic( p, pObj, f );
 }
 
 void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues )
@@ -756,11 +765,10 @@ void Ga2_ManShrinkAbs( Ga2_Man_t * p, int nAbs, int nValues )
     // shrink values
     Gia_ManForEachObjVec( p->vValues, p->pGia, pObj, i )
     {
-        if ( !i ) continue;
-        assert( Ga2_ObjId(p,pObj) );
+        assert( Ga2_ObjId(p,pObj) >= 0 );
         if ( i < nValues )
             continue;
-        Ga2_ObjSetId( p, pObj, 0 );
+        Ga2_ObjSetId( p, pObj, -1 );
     }
     Vec_IntShrink( p->vValues, nValues );
     Vec_PtrShrink( p->vCnfs, 2 * nValues );
@@ -799,14 +807,14 @@ Vec_Int_t * Ga2_ManAbsTranslate( Ga2_Man_t * p )
     Vec_IntWriteEntry( vGateClasses, 0, 1 );
     Gia_ManForEachObjVec( p->vAbs, p->pGia, pObj, i )
     {
-        if ( Gia_ObjIsRo(p->pGia, pObj) )
+        if ( Gia_ObjIsAnd(pObj) )
+            Ga2_ManAbsTranslate_rec( p->pGia, pObj, vGateClasses, 1 );
+        else if ( Gia_ObjIsRo(p->pGia, pObj) )
         {
             Vec_IntWriteEntry( vGateClasses, Gia_ObjId(p->pGia, pObj), 1 );
             pObj = Gia_ObjRoToRi( p->pGia, pObj );
             Vec_IntWriteEntry( vGateClasses, Gia_ObjFaninId0p(p->pGia, pObj), 1 );
         }
-        else if ( Gia_ObjIsAnd(pObj) )
-            Ga2_ManAbsTranslate_rec( p->pGia, pObj, vGateClasses, 1 );
         else if ( !Gia_ObjIsConst0(pObj) )
             assert( 0 );
     }
@@ -819,7 +827,7 @@ Vec_Int_t * Ga2_ManAbsDerive( Gia_Man_t * p )
     Gia_Obj_t * pObj;
     int i;
     vToAdd = Vec_IntAlloc( 1000 );
-    Vec_IntPush( vToAdd, 0 ); // const 0
+//    Vec_IntPush( vToAdd, 0 ); // const 0
     Gia_ManForEachRo( p, pObj, i )
         if ( pObj->fPhase && Vec_IntEntry(p->vGateClasses, Gia_ObjId(p, pObj)) )
             Vec_IntPush( vToAdd, Gia_ObjId(p, pObj) );
@@ -874,8 +882,6 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
     Gia_Obj_t * pLeaf;
     int nLeaves, * pLeaves;
     int i, Lit, pLits[5];
-    if ( Gia_ObjIsCo(pObj) )
-        return Abc_LitNotCond( Ga2_ManUnroll_rec(p, Gia_ObjFanin0(pObj), f), Gia_ObjFaninC0(pObj) );
     if ( Gia_ObjIsConst0(pObj) || (f==0 && Gia_ObjIsRo(p->pGia, pObj)) )
     {
         if ( fSimple )
@@ -888,6 +894,8 @@ int Ga2_ManUnroll_rec( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
         }
         return 0;
     }
+    if ( Gia_ObjIsCo(pObj) )
+        return Abc_LitNotCond( Ga2_ManUnroll_rec(p, Gia_ObjFanin0(pObj), f), Gia_ObjFaninC0(pObj) );
     assert( pObj->fPhase );
     if ( Ga2_ObjIsLeaf0(p, pObj) )
         return Ga2_ObjFindOrAddLit( p, pObj, f );
@@ -1014,8 +1022,6 @@ void Ga2_GlaPrepareCexAndMap( Ga2_Man_t * p, Abc_Cex_t ** ppCex, Vec_Int_t ** pv
         k = Gia_ObjId(p->pGia, pObj);
         if ( Ga2_ObjIsAbs(p, pObj) )
             continue;
-        if ( Gia_ObjIsConst0(pObj) )
-            continue;
         assert( pObj->fPhase );
         assert( Ga2_ObjIsLeaf(p, pObj) );
         assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCi(pObj) );