Experiments with CEC for arithmetic circuits.

11 files changed, 169 insertions, 74 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index ab6870d8..1877821a 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -156,6 +156,7 @@ struct Gia_Man_t_
     Vec_Int_t *    vRegInits;     // initial state
     Vec_Int_t *    vDoms;         // dominators
     Vec_Int_t *    vBarBufs;      // barrier buffers
+    Vec_Int_t *    vXors;         // temporary XORs
     unsigned char* pSwitching;    // switching activity for each object
     Gia_Plc_t *    pPlacement;    // placement of the objects
     Gia_Man_t *    pAigExtra;     // combinational logic of holes
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index a01c93fd..dbfe38f3 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -2995,7 +2995,12 @@ Gia_Man_t * Gia_ManDupAndCones( Gia_Man_t * p, int * pAnds, int nAnds, int fTrim
 //        Gia_ObjRiToRo(p, pObj)->Value = Gia_ManAppendCi( pNew );
     // create internal nodes
     Vec_PtrForEachEntry( Gia_Obj_t *, vNodes, pObj, i )
-        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        if ( Gia_ObjIsMux(p, pObj) )
+            pObj->Value = Gia_ManAppendMux( pNew, Gia_ObjFanin2Copy(p, pObj), Gia_ObjFanin1Copy(pObj), Gia_ObjFanin0Copy(pObj) );
+        else if ( Gia_ObjIsXor(pObj) )
+            pObj->Value = Gia_ManAppendXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else 
+            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
     // create COs
     Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pObj, i )
 //        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 27dff3ad..d9e878a7 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -109,6 +109,7 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFreeP( &p->vRegInits );
     Vec_IntFreeP( &p->vDoms );
     Vec_IntFreeP( &p->vBarBufs );
+    Vec_IntFreeP( &p->vXors );
     Vec_IntFreeP( &p->vLevels );
     Vec_IntFreeP( &p->vTruths );
     Vec_IntErase( &p->vCopies );
diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c
index 91edbaa5..9d585d6d 100644
--- a/src/aig/gia/giaShow.c
+++ b/src/aig/gia/giaShow.c
@@ -156,7 +156,7 @@ int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds,
             Vec_IntWriteEntry( vRemap, pFanins[0], pFanins[1] );
             //printf( "Making HA output %d.\n", pFanins[1] );
         }
-        else
+        else // if ( Attr == 3 || Attr == 0 )
         {
             Gia_Obj_t * pObj = Gia_ManObj( p, Node );
             int pFaninsIn[2] = { Gia_ObjFaninId0(pObj, Node), Gia_ObjFaninId1(pObj, Node) };
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 11d61c14..5abc941b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -39306,15 +39306,18 @@ usage:
 int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Vec_Int_t * vOrder = NULL;
-    int c, fSimple = 0, fVerbose = 0, fVeryVerbose = 0;
+    int c, fSimple = 0, fSigned = 0, fVerbose = 0, fVeryVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "svwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "asvwh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 's':
+        case 'a':
             fSimple ^= 1;
             break;
+        case 's':
+            fSigned ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -39333,14 +39336,15 @@ int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     vOrder = fSimple ? NULL : Gia_PolynReorder( pAbc->pGia, fVerbose, fVeryVerbose );
-    Gia_PolynBuild( pAbc->pGia, vOrder, fVerbose, fVeryVerbose );
+    Gia_PolynBuild( pAbc->pGia, vOrder, fSigned, fVerbose, fVeryVerbose );
     Vec_IntFreeP( &vOrder );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &polyn [-svwh]\n" );
+    Abc_Print( -2, "usage: &polyn [-asvwh]\n" );
     Abc_Print( -2, "\t         derives algebraic polynomial from AIG\n" );
-    Abc_Print( -2, "\t-s     : toggles simple computation [default = %s]\n",  fSimple? "yes": "no" );
+    Abc_Print( -2, "\t-a     : toggles simple computation [default = %s]\n",  fSimple? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggles signed computation [default = %s]\n",  fSigned? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggles printing very verbose information [default = %s]\n",  fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
diff --git a/src/proof/acec/acec.h b/src/proof/acec/acec.h
index fd7814d8..f39041c8 100644
--- a/src/proof/acec/acec.h
+++ b/src/proof/acec/acec.h
@@ -59,7 +59,7 @@ extern Vec_Int_t *   Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose );
 extern Vec_Int_t *   Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVeryVerbose );
 extern Vec_Int_t *   Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int fVerbose, int fVeryVerbose );
 /*=== acecPolyn.c ========================================================*/
-extern void          Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose, int fVeryVerbose );
+extern void          Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fSigned, int fVerbose, int fVeryVerbose );
 
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c
index 991067d8..ac7ee67b 100644
--- a/src/proof/acec/acecCore.c
+++ b/src/proof/acec/acecCore.c
@@ -46,8 +46,8 @@ int Gia_PolynCec( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Cec_ParCec_t * pPars )
 {
     Vec_Int_t * vOrder0 = Gia_PolynReorder( pGia0, pPars->fVerbose, pPars->fVeryVerbose );
     Vec_Int_t * vOrder1 = Gia_PolynReorder( pGia1, pPars->fVerbose, pPars->fVeryVerbose );
-    Gia_PolynBuild( pGia0, vOrder0, pPars->fVerbose, pPars->fVeryVerbose );
-    Gia_PolynBuild( pGia1, vOrder1, pPars->fVerbose, pPars->fVeryVerbose );
+    Gia_PolynBuild( pGia0, vOrder0, 0, pPars->fVerbose, pPars->fVeryVerbose );
+    Gia_PolynBuild( pGia1, vOrder1, 0, pPars->fVerbose, pPars->fVeryVerbose );
     Vec_IntFree( vOrder0 );
     Vec_IntFree( vOrder1 );
     return 1;
diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h
index 7f70658e..e761e56e 100644
--- a/src/proof/acec/acecInt.h
+++ b/src/proof/acec/acecInt.h
@@ -56,6 +56,7 @@ ABC_NAMESPACE_HEADER_START
 
 /*=== acecUtil.c ========================================================*/
 extern void          Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose );
+extern Vec_Int_t *   Gia_PolynCollectLastXor( Gia_Man_t * pGia, int fVerbose );
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/proof/acec/acecOrder.c b/src/proof/acec/acecOrder.c
index fbce0835..9b2242d0 100644
--- a/src/proof/acec/acecOrder.c
+++ b/src/proof/acec/acecOrder.c
@@ -44,20 +44,41 @@ ABC_NAMESPACE_IMPL_START
 ***********************************************************************/
 Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int fVerbose, int fVeryVerbose )
 {
+    int fDumpLeftOver = 0;
     int i, iXor, iMaj, iAnd, Entry, Iter, fFound, fFoundAll = 1;
-    Vec_Int_t * vRecord = Vec_IntAlloc( 100 );
+    Vec_Int_t * vRecord = Vec_IntAlloc( 100 ), * vLeft, * vRecord2;
     Vec_Int_t * vMap = Vec_IntStart( Gia_ManObjNum(pGia) );
     Gia_ManForEachCoDriverId( pGia, iAnd, i )
         Vec_IntWriteEntry( vMap, iAnd, 1 );
+
+    // collect the last XOR
+    Vec_IntFreeP( &pGia->vXors );
+    pGia->vXors = Gia_PolynCollectLastXor( pGia, fVerbose );
+    printf( "Collected %d topmost XORs\n", Vec_IntSize(pGia->vXors) );
+    //Vec_IntPrint( p->vXors );
+    Vec_IntForEachEntry( pGia->vXors, iAnd, i )
+    {
+        Gia_Obj_t * pAnd = Gia_ManObj( pGia, iAnd );
+        assert( Vec_IntEntry(vMap, iAnd) );
+        Vec_IntWriteEntry( vMap, iAnd, 0 );
+        Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iAnd), 1 );
+        Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iAnd), 1 );
+        Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 3) );
+        if ( fVeryVerbose )
+            printf( "Recognizing %d => XXXOR(%d %d)\n", iAnd, Gia_ObjFaninId0(pAnd, iAnd), Gia_ObjFaninId1(pAnd, iAnd) );
+    }
+
+    // detect FAs and HAs
     for ( Iter = 0; fFoundAll; Iter++ )
     {
         if ( fVeryVerbose )
             printf( "Iteration %d\n", Iter );
+
         // check if we can extract FADDs
         fFoundAll = 0;
         do {
             fFound = 0;
-            for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ )
+            for ( i = Vec_IntSize(vFadds)/5 - 1; i >= 0; i-- )
             {
                 iXor = Vec_IntEntry(vFadds, 5*i+3);
                 iMaj = Vec_IntEntry(vFadds, 5*i+4);
@@ -68,8 +89,6 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
                     Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+0), 1 );
                     Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+1), 1 );
                     Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+2), 1 );
-                    //Vec_IntPush( vRecord, iXor );
-                    //Vec_IntPush( vRecord, iMaj );
                     Vec_IntPush( vRecord, Abc_Var2Lit2(i, 2) );
                     fFound = 1;
                     fFoundAll = 1;
@@ -81,7 +100,7 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
         // check if we can extract HADDs
         do {
             fFound = 0; 
-            for ( i = 0; i < Vec_IntSize(vHadds)/2; i++ )
+            for ( i = Vec_IntSize(vHadds)/2 - 1; i >= 0; i-- )
             {
                 iXor = Vec_IntEntry(vHadds, 2*i+0);
                 iMaj = Vec_IntEntry(vHadds, 2*i+1);
@@ -92,8 +111,6 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
                     Vec_IntWriteEntry( vMap, iMaj, 0 );
                     Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iMaj), 1 );
                     Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iMaj), 1 );
-                    //Vec_IntPush( vRecord, iXor );
-                    //Vec_IntPush( vRecord, iMaj );
                     Vec_IntPush( vRecord, Abc_Var2Lit2(i, 1) );
                     fFound = 1;
                     fFoundAll = 1;
@@ -105,6 +122,7 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
         } while ( fFound );
         if ( fFoundAll )
             continue;
+/*
         // find the last one
         Vec_IntForEachEntryReverse( vMap, Entry, iAnd )
             if ( Entry && Gia_ObjIsAnd(Gia_ManObj(pGia, iAnd)) )//&& Vec_IntFind(vFadds, iAnd) == -1 )//&& Vec_IntFind(vHadds, iAnd) == -1 )
@@ -115,7 +133,6 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
                     Vec_IntWriteEntry( vMap, iAnd, 0 );
                     Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iAnd), 1 );
                     Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iAnd), 1 );
-                    //Vec_IntPush( vRecord, iAnd );
                     Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 0) );
                 }
                 else
@@ -123,7 +140,6 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
                     Vec_IntWriteEntry( vMap, iAnd, 0 );
                     Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan0), 1 );
                     Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan1), 1 );
-                    //Vec_IntPush( vRecord, iAnd );
                     Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 0) );
                     Vec_IntPush( vRecord, Abc_Var2Lit2(Gia_ObjFaninId0(pAnd, iAnd), 0) );
                     Vec_IntPush( vRecord, Abc_Var2Lit2(Gia_ObjFaninId1(pAnd, iAnd), 0) );
@@ -134,21 +150,39 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
                     printf( "Recognizing %d => AND(%d %d)\n", iAnd, Gia_ObjFaninId0(pAnd, iAnd), Gia_ObjFaninId1(pAnd, iAnd) );
                 break;
             }
+*/
     }
     //Vec_IntPrint( vMap );
 
-/*
+    // collect remaining ones
+    vLeft = Vec_IntAlloc( 100 );
+    Vec_IntForEachEntry( vMap, Entry, i )
+        if ( Entry && Gia_ObjIsAnd(Gia_ManObj(pGia, i)) )
+            Vec_IntPush( vLeft, i );
+    Vec_IntFree( vMap );
+
+    // collect them in the topo order
+    vRecord2 = Vec_IntAlloc( 100 );
+    Gia_ManIncrementTravId( pGia );
+    Gia_ManCollectAnds( pGia, Vec_IntArray(vLeft), Vec_IntSize(vLeft), vRecord2, NULL );
+    Vec_IntForEachEntry( vRecord2, iAnd, i )
+        Vec_IntWriteEntry( vRecord2, i, Abc_Var2Lit2(iAnd, 0) );
+
     // dump remaining nodes as an AIG
     if ( fDumpLeftOver )
     {        
-        Gia_Man_t * pNew = Gia_ManDupAndCones( pGia, Vec_IntArray(vMap), Vec_IntSize(vMap), 0 );
+        Gia_Man_t * pNew;
+        pNew = Gia_ManDupAndCones( pGia, Vec_IntArray(vLeft), Vec_IntSize(vLeft), 0 );
         Gia_AigerWrite( pNew, "leftover.aig", 0, 0 );
+        printf( "Leftover AIG with %d nodes is dumped into file \"%s\".\n", Gia_ManAndNum(pNew), "leftover.aig" );
         Gia_ManStop( pNew );
     }
-*/
-    Vec_IntFree( vMap );
+    Vec_IntFree( vLeft );
+
     Vec_IntReverseOrder( vRecord );
-    return vRecord;
+    Vec_IntAppend( vRecord2, vRecord );
+    Vec_IntFree( vRecord );
+    return vRecord2;
 }
 
 /**Function*************************************************************
@@ -191,7 +225,9 @@ Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVeryVerbose )
         }
         else
             Gia_ManCollectAnds_rec( pGia, Node, vOrder );
+        //printf( "Order = %d.  Node = %d.  Size = %d ", i, Node, Vec_IntSize(vOrder) );
     }
+    //printf( "\n" );
     //assert( Vec_IntSize(vOrder) == Gia_ManAndNum(pGia) );
 
     // remap order
diff --git a/src/proof/acec/acecPolyn.c b/src/proof/acec/acecPolyn.c
index 5e20ef30..2f98df73 100644
--- a/src/proof/acec/acecPolyn.c
+++ b/src/proof/acec/acecPolyn.c
@@ -54,7 +54,8 @@ struct Pln_Man_t_
     Vec_Int_t *    vTempC[2]; // polynomial representation
     Vec_Int_t *    vTempM[4]; // polynomial representation
     Vec_Int_t *    vOrder;    // order of collapsing
-    int            nBuilds;   // builds
+    int            nBuilds;   // built monomials
+    int            nUsed;     // used monomials
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -144,7 +145,10 @@ void Pln_ManPrintFinal( Pln_Man_t * p, int fVerbose, int fVeryVerbose )
 
         Count++;
 
-        if ( !fVeryVerbose )
+        if ( !fVerbose )
+            continue;
+
+        if ( Count > 25 )
             continue;
 
         vArray = Hsh_VecReadEntry( p->pHashC, iConst );
@@ -170,6 +174,25 @@ void Pln_ManPrintFinal( Pln_Man_t * p, int fVerbose, int fVeryVerbose )
   SeeAlso     []
 
 ***********************************************************************/
+static inline void Vec_IntAppendMinus2x( Vec_Int_t * vVec1, Vec_Int_t * vVec2 )
+{
+    int Entry, i;
+    Vec_IntClear( vVec1 );
+    Vec_IntForEachEntry( vVec2, Entry, i )
+        Vec_IntPush( vVec1, Entry > 0 ? -Entry-1 : -Entry+1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline void Gia_PolynMergeConstOne( Vec_Int_t * vConst, int New )
 {
     int i, Old;
@@ -210,7 +233,7 @@ static inline void Gia_PolynMergeConst( Vec_Int_t * vConst, Pln_Man_t * p, int i
 }
 static inline void Gia_PolynBuildAdd( Pln_Man_t * p, Vec_Int_t * vTempC, Vec_Int_t * vTempM )
 {
-    int iConst, iMono = vTempM ? Hsh_VecManAdd(p->pHashM, vTempM) : 0;
+    int iConst, iConstNew, iMono = vTempM ? Hsh_VecManAdd(p->pHashM, vTempM) : 0;
     p->nBuilds++;
     if ( iMono == Vec_IntSize(p->vCoefs) ) // new monomial
     {
@@ -220,14 +243,21 @@ static inline void Gia_PolynBuildAdd( Pln_Man_t * p, Vec_Int_t * vTempC, Vec_Int
         Vec_FltPush( p->vCounts, (float)Vec_IntEntry(p->vOrder, Vec_IntEntryLast(vTempM)) );
         Vec_QuePush( p->vQue, iMono );
 //        Vec_QueUpdate( p->vQue, iMono );
+        if ( iConst )
+            p->nUsed++;
         return;
     }
     // this monomial exists
     iConst = Vec_IntEntry( p->vCoefs, iMono );
     if ( iConst )
         Gia_PolynMergeConst( vTempC, p, iConst );
-    iConst = Hsh_VecManAdd( p->pHashC, vTempC );
-    Vec_IntWriteEntry( p->vCoefs, iMono, iConst );
+    iConstNew = Hsh_VecManAdd( p->pHashC, vTempC );
+    Vec_IntWriteEntry( p->vCoefs, iMono, iConstNew );
+    if ( iConst && !iConstNew )
+        p->nUsed--;
+    else if ( !iConst && iConstNew )
+        p->nUsed++;
+    //assert( p->nUsed == Vec_IntSize(p->vCoefs) - Vec_IntCountZero(p->vCoefs) );
 }
 void Gia_PolynBuildOne( Pln_Man_t * p, int iMono )
 {
@@ -242,11 +272,13 @@ void Gia_PolynBuildOne( Pln_Man_t * p, int iMono )
     pObj    = Gia_ManObj( p->pGia, iDriver );
     if ( !Gia_ObjIsAnd(pObj) )
         return;
+    assert( !Gia_ObjIsMux(p->pGia, pObj) );
 
     iConst = Vec_IntEntry( p->vCoefs, iMono );
     if ( iConst == 0 )
         return;
     Vec_IntWriteEntry( p->vCoefs, iMono, 0 );
+    p->nUsed--;
 
     iFan0 = Gia_ObjFaninId0p(p->pGia, pObj);
     iFan1 = Gia_ObjFaninId1p(p->pGia, pObj);
@@ -264,10 +296,29 @@ void Gia_PolynBuildOne( Pln_Man_t * p, int iMono )
     }
 
     vConst = Hsh_VecReadEntry( p->pHashC, iConst );
-    for ( k = 0; k < 2; k++ )
-        Vec_IntAppendMinus( p->vTempC[k], vConst, k );
 
-    if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )       //  C * (1 - x) * (1 - y)
+    if ( !Gia_ObjIsXor(pObj) )
+        for ( k = 0; k < 2; k++ )
+            Vec_IntAppendMinus( p->vTempC[k], vConst, k );
+
+    if ( Gia_ObjIsXor(pObj) )
+    {
+        vConst = Hsh_VecReadEntry( p->pHashC, iConst );
+        Vec_IntAppendMinus( p->vTempC[0], vConst, 0 );
+        Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[1] );   //  C * x 
+
+        vConst = Hsh_VecReadEntry( p->pHashC, iConst );
+        Vec_IntAppendMinus( p->vTempC[0], vConst, 0 );
+        Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[2] );   //  C * y 
+
+        //if ( !p->pGia->vXors || Vec_IntFind(p->pGia->vXors, iDriver) > 0 )
+        {
+            vConst = Hsh_VecReadEntry( p->pHashC, iConst );
+            Vec_IntAppendMinus2x( p->vTempC[0], vConst );
+            Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[3] );   // -C * x * y 
+        }
+    }
+    else if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )  //  C * (1 - x) * (1 - y)
     {
         Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] );   //  C * 1
         Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[1] );   // -C * x
@@ -290,36 +341,7 @@ void Gia_PolynBuildOne( Pln_Man_t * p, int iMono )
     else   
         Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[3] );   //  C * x * y
 }
-int Gia_PolyFindNext2( Pln_Man_t * p )
-{
-    Gia_Obj_t * pObj; 
-    Vec_Int_t * vArray;
-    int Max = 0, iBest = 0, iConst, iMono, iDriver;
-    Vec_IntForEachEntryStart( p->vCoefs, iConst, iMono, 1 )
-    {
-        if ( iConst == 0 ) 
-            continue;
-        vArray  = Hsh_VecReadEntry( p->pHashM, iMono );
-        iDriver = Vec_IntEntryLast( vArray );
-        pObj    = Gia_ManObj( p->pGia, iDriver );
-        if ( !Gia_ObjIsAnd(pObj) )
-            continue;
-        if ( Max < Vec_IntEntryLast(vArray) )
-        {
-            Max   = Vec_IntEntryLast(vArray);
-            iBest = iMono;
-        }
-    }
-    //Vec_IntPrint( Hsh_VecReadEntry(p->pHashM, iBest) );
-    return iBest;
-}
-int Gia_PolyFindNext( Pln_Man_t * p )
-{
-    int iBest = Vec_QueSize(p->vQue) ?  Vec_QuePop(p->vQue) : 0;
-    //Vec_IntPrint( Hsh_VecReadEntry(p->pHashM, iBest) );
-    return iBest;
-}
-void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose, int fVeryVerbose )
+void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fSigned, int fVerbose, int fVeryVerbose )
 {
     abctime clk = Abc_Clock();//, clk2 = 0;
     Gia_Obj_t * pObj; 
@@ -334,22 +356,35 @@ void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose, int fVe
         iDriver = Gia_ObjFaninId0p( pGia, pObj );
         Vec_IntFill( p->vTempM[0], 1, iDriver );   //  Driver
 
-        if ( Gia_ObjFaninC0(pObj) )
+        if ( fSigned && i == Gia_ManCoNum(pGia)-1 )
         {
-            Gia_PolynBuildAdd( p, p->vTempC[0], NULL );           //  C
-            Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[0] );   // -C * Driver
+            if ( Gia_ObjFaninC0(pObj) )
+            {
+                Gia_PolynBuildAdd( p, p->vTempC[1], NULL );           // -C
+                Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] );   //  C * Driver
+            }
+            else
+                Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[0] );   // -C * Driver
+        }
+        else 
+        {
+            if ( Gia_ObjFaninC0(pObj) )
+            {
+                Gia_PolynBuildAdd( p, p->vTempC[0], NULL );           //  C
+                Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[0] );   // -C * Driver
+            }
+            else
+                Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] );   //  C * Driver
         }
-        else
-            Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] );   //  C * Driver
     }
     LevPrev = -1;
     for ( Iter = 0; ; Iter++ )
     {
         Vec_Int_t * vTempM;
         //abctime temp = Abc_Clock();
-        iMono = Gia_PolyFindNext(p);
-        if ( !iMono )
+        if ( Vec_QueSize(p->vQue) == 0 )
             break;
+        iMono = Vec_QuePop(p->vQue);
 
         // report
         vTempM = Hsh_VecReadEntry( p->pHashM, iMono );
@@ -366,8 +401,8 @@ void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose, int fVe
                 Vec_BitSetEntry( vPres, LevCur, 1 );
 
             if ( fVerbose )
-                printf( "Line%5d   Iter%10d : Obj =%6d.  Order =%6d.  HashC =%6d. HashM =%10d.  Total =%10d. Used =%6d.\n", 
-                    Line++, Iter, LevCur, Vec_IntEntry(p->vOrder, LevCur), Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, -1 );
+                printf( "Line%5d   Iter%10d : Obj =%6d.  Order =%6d.  HashC =%6d. HashM =%10d.  Total =%10d. Used =%10d.\n", 
+                    Line++, Iter, LevCur, Vec_IntEntry(p->vOrder, LevCur), Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, p->nUsed );
         }
         LevPrev = LevCur;
 
diff --git a/src/proof/acec/acecUtil.c b/src/proof/acec/acecUtil.c
index 26087f92..191856cf 100644
--- a/src/proof/acec/acecUtil.c
+++ b/src/proof/acec/acecUtil.c
@@ -48,11 +48,23 @@ void Gia_PolynCollectXors_rec( Gia_Man_t * pGia, int iObj, Vec_Int_t * vXors )
     if ( Gia_ObjIsTravIdCurrent(pGia, pObj) )
         return;
     Gia_ObjSetTravIdCurrent(pGia, pObj);
-    if ( !Gia_ObjIsAnd(pObj) || !Gia_ObjIsXor(pObj) )
+    if ( !Gia_ObjIsAnd(pObj) || !Gia_ObjIsXor(pObj) || Gia_ObjRefNum(pGia, pObj) > 1 )
         return;
-    Vec_IntPush( vXors, iObj );
     Gia_PolynCollectXors_rec( pGia, Gia_ObjFaninId0(pObj, iObj), vXors );
     Gia_PolynCollectXors_rec( pGia, Gia_ObjFaninId1(pObj, iObj), vXors );
+    Vec_IntPushUnique( vXors, iObj );
+}
+Vec_Int_t * Gia_PolynCollectLastXor( Gia_Man_t * pGia, int fVerbose )
+{
+    Vec_Int_t * vXors = Vec_IntAlloc( 100 );
+    Gia_Obj_t * pObj = Gia_ManCo( pGia, Gia_ManCoNum(pGia)-1 );
+    ABC_FREE( pGia->pRefs );
+    Gia_ManCreateRefs( pGia );
+    Gia_ManIncrementTravId( pGia );
+    Gia_PolynCollectXors_rec( pGia, Gia_ObjFaninId0p(pGia, pObj), vXors );
+    Vec_IntReverseOrder( vXors );
+    ABC_FREE( pGia->pRefs );
+    return vXors;
 }
 void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose )
 {