Various changes.

2 files changed, 56 insertions, 38 deletions

diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index 1bc037c4..7c101570 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -101,6 +101,7 @@ struct Cec_ParFra_t_
     int              nRounds;       // the number of simulation rounds
     int              nItersMax;     // the maximum number of iterations of SAT sweeping
     int              nBTLimit;      // conflict limit at a node
+    int              nBTLimitPo;    // conflict limit at an output
     int              TimeLimit;     // the runtime limit in seconds
     int              nLevelMax;     // restriction on the level nodes to be swept
     int              nDepthMax;     // the depth in terms of steps of speculative reduction
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index b58aada8..ce299c66 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -98,13 +98,12 @@ struct Cec4_Man_t_
     Vec_Int_t *      vCands;
     Vec_Int_t *      vVisit;
     Vec_Int_t *      vPat;
-    Vec_Int_t *      vPats;
     Vec_Int_t *      vDisprPairs;
     Vec_Bit_t *      vFails;
+    Vec_Bit_t *      vCoDrivers;
     int              iPosRead;       // candidate reading position
     int              iPosWrite;      // candidate writing position
     int              iLastConst;     // last const node proved
-    int              nPatsAll;
     // refinement
     Vec_Int_t *      vRefClasses;
     Vec_Int_t *      vRefNodes;
@@ -162,25 +161,16 @@ Vec_Wrd_t * Cec4_EvalCombine( Vec_Int_t * vPats, int nPats, int nInputs, int nWo
 {
     //Vec_Wrd_t * vSimsPi = Vec_WrdStart( nInputs * nWords );
     Vec_Wrd_t * vSimsPi = Vec_WrdStartRandom( nInputs * nWords );
-    int i, k, iPat = 0; 
-    for ( i = 0; i < Vec_IntSize(vPats); )
-    {
-        int Size = Vec_IntEntry(vPats, i);
-        assert( Size > 0 );
-        for ( k = 1; k <= Size; k++ )
-        {
-            int iLit = Vec_IntEntry( vPats, i+k );
-            word * pSim;
-            if ( iLit == 0 )
-                continue;
-            assert( Abc_Lit2Var(iLit) > 0 && Abc_Lit2Var(iLit) <= nInputs );
-            pSim = Vec_WrdEntryP( vSimsPi, (Abc_Lit2Var(iLit)-1)*nWords );
-            if ( Abc_InfoHasBit( (unsigned*)pSim, iPat ) != Abc_LitIsCompl(iLit) )
-                Abc_InfoXorBit( (unsigned*)pSim, iPat );
-        }
-        iPat++;
-        i += Size + 1;
-    }
+    int i, k, iLit, iPat = 0; word * pSim;
+    for ( i = 0; i < Vec_IntSize(vPats); i += Vec_IntEntry(vPats, i), iPat++ )
+        for ( k = 1; k < Vec_IntEntry(vPats, i)-1; k++ )
+            if ( (iLit = Vec_IntEntry(vPats, i+k)) )
+            {
+                assert( Abc_Lit2Var(iLit) > 0 && Abc_Lit2Var(iLit) <= nInputs );
+                pSim = Vec_WrdEntryP( vSimsPi, (Abc_Lit2Var(iLit)-1)*nWords );
+                if ( Abc_InfoHasBit( (unsigned*)pSim, iPat ) != Abc_LitIsCompl(iLit) )
+                    Abc_InfoXorBit( (unsigned*)pSim, iPat );
+            }
     assert( iPat == nPats );
     return vSimsPi;
 }
@@ -224,6 +214,7 @@ void Cec4_ManSetParams( Cec_ParFra_t * pPars )
     pPars->nRounds        =      10;    // simulation rounds
     pPars->nItersMax      =    2000;    // this is a miter
     pPars->nBTLimit       = 1000000;    // use logic cones
+    pPars->nBTLimitPo     =       0;    // use logic outputs
     pPars->nSatVarMax     =    1000;    // the max number of SAT variables before recycling SAT solver
     pPars->nCallsRecycle  =     500;    // calls to perform before recycling SAT solver
     pPars->nGenIters      =     100;    // pattern generation iterations
@@ -257,10 +248,18 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
     p->vCands        = Vec_IntAlloc( 100 );
     p->vVisit        = Vec_IntAlloc( 100 );
     p->vPat          = Vec_IntAlloc( 100 );
-    p->vPats         = Vec_IntAlloc( 10000 );
     p->vDisprPairs   = Vec_IntAlloc( 100 );
     p->vFails        = Vec_BitStart( Gia_ManObjNum(pAig) );
     //pAig->pData     = p->pSat; // point AIG manager to the solver
+    //Vec_IntFreeP( &p->pAig->vPats );
+    //p->pAig->vPats = Vec_IntAlloc( 1000 );
+    if ( pPars->nBTLimitPo )
+    {
+        int i, Driver;
+        p->vCoDrivers = Vec_BitStart( Gia_ManObjNum(pAig) );
+        Gia_ManForEachCoDriverId( pAig, Driver, i )
+            Vec_BitWriteEntry( p->vCoDrivers, Driver, 1 );
+    }
     return p;
 }
 void Cec4_ManDestroy( Cec4_Man_t * p )
@@ -287,11 +286,9 @@ void Cec4_ManDestroy( Cec4_Man_t * p )
         fflush( stdout );
     }
     //printf( "Recorded %d patterns with %d literals (average %.2f).\n", 
-    //    p->nPatsAll, Vec_IntSize(p->vPats) - p->nPatsAll, 1.0*Vec_IntSize(p->vPats)/Abc_MaxInt(1, p->nPatsAll)-1 );
-    //Cec4_EvalPatterns( p->pAig, p->vPats, p->nPatsAll );
-    //Vec_IntFreeP( &p->vPats );
-    Vec_IntFreeP( &p->pAig->vPats );
-    p->pAig->vPats = p->vPats;
+    //    p->pAig->nBitPats, Vec_IntSize(p->pAig->vPats) - 2*p->pAig->nBitPats, 1.0*Vec_IntSize(p->pAig->vPats)/Abc_MaxInt(1, p->pAig->nBitPats)-2 );
+    //Cec4_EvalPatterns( p->pAig, p->pAig->vPats, p->pAig->nBitPats );
+    //Vec_IntFreeP( &p->pAig->vPats );
     Vec_WrdFreeP( &p->pAig->vSims );
     Vec_WrdFreeP( &p->pAig->vSimsPi );
     Gia_ManCleanMark01( p->pAig );
@@ -307,6 +304,7 @@ void Cec4_ManDestroy( Cec4_Man_t * p )
     Vec_IntFreeP( &p->vPat );
     Vec_IntFreeP( &p->vDisprPairs );
     Vec_BitFreeP( &p->vFails );
+    Vec_BitFreeP( &p->vCoDrivers );
     Vec_IntFreeP( &p->vRefClasses );
     Vec_IntFreeP( &p->vRefNodes );
     Vec_IntFreeP( &p->vRefBins );
@@ -1458,9 +1456,12 @@ int Cec4_ManGeneratePatterns( Cec4_Man_t * p )
             if ( Res )
             {
                 int Ret = Cec4_ManPackAddPattern( p->pAig, p->vPat, 1 );
-                Vec_IntPush( p->vPats, Vec_IntSize(p->vPat) );
-                Vec_IntAppend( p->vPats, p->vPat );
-                p->nPatsAll++;
+                if ( p->pAig->vPats )
+                {
+                    Vec_IntPush( p->pAig->vPats, Vec_IntSize(p->vPat)+2 );
+                    Vec_IntAppend( p->pAig->vPats, p->vPat );
+                    Vec_IntPush( p->pAig->vPats, -1 );
+                }
                 //Vec_IntPushTwo( p->vDisprPairs, iRepr, iCand );
                 Packs += Ret;
                 if ( Ret == 64 * p->pAig->nSimWords )
@@ -1506,12 +1507,13 @@ void Cec4_ManSatSolverRecycle( Cec4_Man_t * p )
     Vec_IntClear( &p->pNew->vCopiesTwo );  // pairs (CiAigId, SatId)
     Vec_IntClear( &p->pNew->vVarMap    );  // mapping of SatId into AigId
 }
-int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pfEasy, int fVerbose )
+int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pfEasy, int fVerbose, int fEffort )
 {
     abctime clk;
-    int nBTLimit = Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1) ? Abc_MaxInt(1, p->pPars->nBTLimit/10) : p->pPars->nBTLimit;
+    int nBTLimit = fEffort ? p->pPars->nBTLimitPo : (Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1)) ? Abc_MaxInt(1, p->pPars->nBTLimit/10) : p->pPars->nBTLimit;
     int nConfEnd, nConfBeg, status, iVar0, iVar1, Lits[2];
     int UnsatConflicts[3] = {0};
+    //printf( "%d ", nBTLimit );
     if ( iObj1 <  iObj0 ) 
          iObj1 ^= iObj0, iObj0 ^= iObj1, iObj1 ^= iObj0;
     assert( iObj0 < iObj1 );    
@@ -1567,8 +1569,6 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf
                 *pfEasy = nConfEnd == nConfBeg;
             }
         }
-        else 
-            return status;
     }
     if ( status == GLUCOSE_UNSAT && iObj0 > 0 )
     {
@@ -1601,6 +1601,8 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf
             }
         }
     }
+    //if ( status == GLUCOSE_UNDEC )
+    //    printf( "*  " );
     return status;
 }
 int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
@@ -1610,7 +1612,8 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
     Gia_Obj_t * pObj = Gia_ManObj( p->pAig, iObj );
     Gia_Obj_t * pRepr = Gia_ManObj( p->pAig, iRepr );
     int fCompl = Abc_LitIsCompl(pObj->Value) ^ Abc_LitIsCompl(pRepr->Value) ^ pObj->fPhase ^ pRepr->fPhase;
-    status = Cec4_ManSolveTwo( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, &fEasy, p->pPars->fVerbose );
+    int fEffort = p->vCoDrivers ? Vec_BitEntry(p->vCoDrivers, iObj) || Vec_BitEntry(p->vCoDrivers, iRepr) : 0;
+    status = Cec4_ManSolveTwo( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, &fEasy, p->pPars->fVerbose, fEffort );
     if ( status == GLUCOSE_SAT )
     {
         int iLit;
@@ -1635,9 +1638,12 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
         p->pAig->iPatsPi++;
         Vec_IntForEachEntry( p->vPat, iLit, i )
             Cec4_ObjSimSetInputBit( p->pAig, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) );
-        Vec_IntPush( p->vPats, Vec_IntSize(p->vPat) );
-        Vec_IntAppend( p->vPats, p->vPat );
-        p->nPatsAll++;
+        if ( p->pAig->vPats )
+        {
+            Vec_IntPush( p->pAig->vPats, Vec_IntSize(p->vPat)+2 );
+            Vec_IntAppend( p->pAig->vPats, p->vPat );
+            Vec_IntPush( p->pAig->vPats, -1 );
+        }
         //Cec4_ManPackAddPattern( p->pAig, p->vPat, 0 );
         //assert( iPatsOld + 1 == p->pAig->iPatsPi );
         if ( fEasy )
@@ -1887,6 +1893,17 @@ Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose )
     Cec4_ManPerformSweeping( p, pPars, &pNew, 0 );
     return pNew;
 }
+Gia_Man_t * Cec4_ManSimulateTest4( Gia_Man_t * p, int nBTLimit, int nBTLimitPo, int fVerbose )
+{
+    Gia_Man_t * pNew = NULL;
+    Cec_ParFra_t ParsFra, * pPars = &ParsFra;
+    Cec4_ManSetParams( pPars );
+    pPars->fVerbose = fVerbose;
+    pPars->nBTLimit = nBTLimit;
+    pPars->nBTLimitPo = nBTLimitPo;
+    Cec4_ManPerformSweeping( p, pPars, &pNew, 0 );
+    return pNew;
+}
 int Cec4_ManSimulateOnlyTest( Gia_Man_t * p, int fVerbose )
 {
     Cec_ParFra_t ParsFra, * pPars = &ParsFra;