Improvements to inductive generalization in IC3/PDR by Zyad Hassan.

6 files changed, 342 insertions, 9 deletions

diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index 529a161f..b73a54df 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -49,6 +49,7 @@ struct Pdr_Par_t_
     int nTimeOut;         // timeout in seconds
     int nTimeOutGap;      // approximate timeout in seconds since the last change
     int nTimeOutOne;      // approximate timeout in seconds per one output
+    int nRandomSeed;      // value to seed the SAT solver with
     int fTwoRounds;       // use two rounds for generalization
     int fMonoCnf;         // monolythic CNF
     int fDumpInv;         // dump inductive invariant
@@ -57,6 +58,8 @@ struct Pdr_Par_t_
     int fShiftStart;      // allows clause pushing to start from an intermediate frame
     int fReuseProofOblig; // reuses proof-obligationgs in the last timeframe
     int fSkipGeneral;     // skips expensive generalization step
+    int fSkipDown;        // skips the application of down
+    int fCtgs;            // handle CTGs in down
     int fVerbose;         // verbose output`
     int fVeryVerbose;     // very verbose output
     int fNotVerbose;      // not printing line by line progress
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index b81a1a2a..71a61c81 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -20,6 +20,7 @@
 
 #include "pdrInt.h"
 #include "base/main/main.h"
+#include "misc/hash/hash.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -57,7 +58,10 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
     pPars->nConfLimit     =       0;  // limit on SAT solver conflicts
     pPars->nConfGenLimit  =       0;  // limit on SAT solver conflicts during generalization
     pPars->nRestLimit     =       0;  // limit on the number of proof-obligations
+    pPars->nRandomSeed   = 91648253;  // value to seed the SAT solver with
     pPars->fTwoRounds     =       0;  // use two rounds for generalization
+    pPars->fSkipDown      =       1;  // apply down in generalization
+    pPars->fCtgs          =       0;  // handle CTGs in down
     pPars->fMonoCnf       =       0;  // monolythic CNF
     pPars->fDumpInv       =       0;  // dump inductive invariant
     pPars->fUseSupp       =       1;  // using support variables in the invariant
@@ -296,6 +300,190 @@ int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int ZPdr_ManSimpleMic( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube )
+{
+    int * pOrder;
+    int i, j, n, Lit, RetValue;
+    Pdr_Set_t * pCubeTmp;
+    // perform generalization
+    if ( p->pPars->fSkipGeneral )
+      return 0;
+
+    // sort literals by their occurences
+    pOrder = Pdr_ManSortByPriority( p, *ppCube );
+    // try removing literals
+    for ( j = 0; j < (*ppCube)->nLits; j++ )
+    {
+        // use ordering
+    //        i = j;
+        i = pOrder[j];
+
+        assert( (*ppCube)->Lits[i] != -1 );
+        // check init state
+        if ( Pdr_SetIsInit(*ppCube, i) )
+            continue;
+        // try removing this literal
+        Lit = (*ppCube)->Lits[i]; (*ppCube)->Lits[i] = -1; 
+        RetValue = Pdr_ManCheckCube( p, k, *ppCube, NULL, p->pPars->nConfLimit, 0 );
+        if ( RetValue == -1 )
+            return -1;
+        (*ppCube)->Lits[i] = Lit;
+        if ( RetValue == 0 )
+            continue;
+
+        // remove j-th entry
+        for ( n = j; n < (*ppCube)->nLits-1; n++ )
+            pOrder[n] = pOrder[n+1];
+        j--;
+
+        // success - update the cube
+        *ppCube = Pdr_SetCreateFrom( pCubeTmp = *ppCube, i );
+        Pdr_SetDeref( pCubeTmp );
+        assert( (*ppCube)->nLits > 0 );
+        i--;
+
+        // get the ordering by decreasing priorit
+        pOrder = Pdr_ManSortByPriority( p, *ppCube );
+    }
+    return 0;
+}
+
+
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, Hash_Int_t * keep, Pdr_Set_t * pIndCube, int * added )
+{
+    int RetValue = 0, CtgRetValue, i, ctgAttempts, l, micResult;
+    int kMax = Vec_PtrSize(p->vSolvers)-1;
+    Pdr_Set_t * pCubeTmp, * pCubeMin, * pCtg;
+    while ( RetValue == 0 )
+    {
+        ctgAttempts = 0;
+        while ( p->pPars->fCtgs && RetValue == 0 && k > 1 && ctgAttempts < 3 )
+        {
+            pCtg = Pdr_SetDup ( pPred );
+            //Check CTG for inductiveness
+            if ( Pdr_SetIsInit( pCtg, -1 ) )
+            {
+                Pdr_SetDeref( pCtg );
+                break;
+            }
+            if (*added == 0)
+            {
+                for ( i = 1; i <= k; i++ )
+                    Pdr_ManSolverAddClause( p, i, pIndCube);
+                *added = 1;
+            }
+            ctgAttempts++;
+            CtgRetValue = Pdr_ManCheckCube ( p, k-1, pCtg, NULL, p->pPars->nConfLimit, 0 );
+            if ( CtgRetValue != 1 )
+            {
+                Pdr_SetDeref( pCtg );
+                break;
+            }
+            pCubeMin = Pdr_ManReduceClause( p, k-1, pCtg );
+            if ( pCubeMin == NULL )
+                pCubeMin = Pdr_SetDup ( pCtg );
+
+            for ( l = k; l < kMax; l++ )
+                if ( !Pdr_ManCheckCube( p, l, pCubeMin, NULL, 0, 0 ) )
+                    break;
+            micResult = ZPdr_ManSimpleMic( p, l-1, &pCubeMin );
+            assert ( micResult != -1 );
+
+            // add new clause
+            if ( p->pPars->fVeryVerbose )
+            {
+                Abc_Print( 1, "Adding cube " );
+                Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL );
+                Abc_Print( 1, " to frame %d.\n", l );
+            }
+            // set priority flops
+            for ( i = 0; i < pCubeMin->nLits; i++ )
+            {
+                assert( pCubeMin->Lits[i] >= 0 );
+                assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
+                Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 );
+            }
+
+            Vec_VecPush( p->vClauses, l, pCubeMin );   // consume ref
+            p->nCubes++;
+            // add clause
+            for ( i = 1; i <= l; i++ )
+                Pdr_ManSolverAddClause( p, i, pCubeMin );
+            RetValue = Pdr_ManCheckCube ( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0 );
+            assert( RetValue >= 0 );
+            Pdr_SetDeref( pCtg );
+            if ( RetValue == 1 )
+            {
+                //printf ("IT'S A ONE\n");
+                return 1;
+            }
+        }
+
+        //join
+        if ( p->pPars->fVeryVerbose )
+        {
+            printf("Cube:\n");
+            ZPdr_SetPrint( *ppCube );
+            printf("\nPred:\n");
+            ZPdr_SetPrint( pPred );
+        }
+        *ppCube = ZPdr_SetIntersection( pCubeTmp = *ppCube, pPred, keep );
+        Pdr_SetDeref( pCubeTmp );
+        Pdr_SetDeref( pPred );
+        if ( *ppCube == NULL )
+            return 0;
+        if ( p->pPars->fVeryVerbose )
+        {
+          printf("Intersection:\n");
+          ZPdr_SetPrint( *ppCube );
+        }
+        if ( Pdr_SetIsInit( *ppCube, -1 ) )
+        {
+          if ( p->pPars->fVeryVerbose )
+            printf ("Failed initiation\n");
+          return 0;
+        }
+        RetValue = Pdr_ManCheckCube ( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0 );
+        if ( RetValue == -1 )
+            return -1;
+        if ( RetValue == 1 )
+        {
+            //printf ("*********IT'S A ONE\n");
+            break;
+        }
+        if ( RetValue == 0 && (*ppCube)->nLits == 1)
+        {
+            Pdr_SetDeref( pPred ); // fixed memory leak
+            // A workaround for the incomplete assignment returned by the SAT
+            // solver
+            return 0;
+        }
+    }
+    return 1;
+}
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if the state could be blocked.]
 
   Description []
@@ -307,10 +495,12 @@ int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
 ***********************************************************************/
 int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, Pdr_Set_t ** ppCubeMin )
 {
-    Pdr_Set_t * pCubeMin, * pCubeTmp = NULL;
+    Pdr_Set_t * pCubeMin, * pCubeTmp = NULL, * pPred = NULL, * pCubeCpy = NULL;
     int i, j, n, Lit, RetValue;
     abctime clk = Abc_Clock();
     int * pOrder;
+    int added = 0;
+    Hash_Int_t * keep = NULL;
     // if there is no induction, return
     *ppCubeMin = NULL;
     RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit, 0 );
@@ -318,9 +508,11 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
         return -1;
     if ( RetValue == 0 )
     {
-        p->tGeneral += Abc_Clock() - clk;
+        p->tGeneral += clock() - clk;
         return 0;
     }
+    
+    keep = p->pPars->fSkipDown ? NULL : Hash_IntAlloc( 1 );
 
     // reduce clause using assumptions
 //    pCubeMin = Pdr_SetDup( pCube );
@@ -340,13 +532,22 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
     //        i = j;
             i = pOrder[j];
 
-            // check init state
             assert( pCubeMin->Lits[i] != -1 );
+            if ( keep && Hash_IntExists( keep, pCubeMin->Lits[i] ) )
+            {
+                //printf("Undroppable\n");
+                continue;
+            }
+
+            // check init state
             if ( Pdr_SetIsInit(pCubeMin, i) )
                 continue;
             // try removing this literal
-            Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
-            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1 );
+            Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; 
+            if ( p->pPars->fSkipDown )
+              RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 1 );
+            else
+              RetValue = Pdr_ManCheckCube( p, k, pCubeMin, &pPred, p->pPars->nConfLimit, 1 );
             if ( RetValue == -1 )
             {
                 Pdr_SetDeref( pCubeMin );
@@ -354,7 +555,39 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
             }
             pCubeMin->Lits[i] = Lit;
             if ( RetValue == 0 )
+            {
+              if ( p->pPars->fSkipDown )
+                  continue;
+              pCubeCpy = Pdr_SetCreateFrom ( pCubeMin, i );
+              RetValue = ZPdr_ManDown ( p, k, &pCubeCpy, pPred, keep, pCubeMin, &added );
+              if ( p->pPars->fCtgs )
+                //CTG handling code messes up with the internal order array
+                pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+              if ( RetValue == -1 )
+              {
+                  Pdr_SetDeref( pCubeMin );
+                  Pdr_SetDeref( pCubeCpy );
+                  Pdr_SetDeref( pPred );
+                  return -1;
+              }
+              if ( RetValue == 0 )
+              {
+                if ( keep ) 
+                  Hash_IntWriteEntry( keep, pCubeMin->Lits[i], 0 );
+                if ( pCubeCpy )
+                  Pdr_SetDeref( pCubeCpy );
                 continue;
+              }
+              //Inductive subclause
+              added = 0;
+              Pdr_SetDeref( pCubeMin );
+              pCubeMin = pCubeCpy;
+              assert( pCubeMin->nLits > 0 );
+              pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+              j = -1;
+              continue;
+            }
+            added = 0;
 
             // remove j-th entry
             for ( n = j; n < pCubeMin->nLits-1; n++ )
@@ -383,7 +616,7 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
             if ( Pdr_SetIsInit(pCubeMin, i) )
                 continue;
             // try removing this literal
-            Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
+            Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; 
             RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit, 0 );
             if ( RetValue == -1 )
             {
@@ -411,8 +644,18 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
     }
 
     assert( ppCubeMin != NULL );
+    if ( p->pPars->fVeryVerbose )
+    {
+        printf("Cube:\n");
+        for ( i = 0; i < pCubeMin->nLits; i++)
+        {
+          printf ("%d ", pCubeMin->Lits[i]);
+        }
+        printf("\n");
+    }
     *ppCubeMin = pCubeMin;
     p->tGeneral += Abc_Clock() - clk;
+    if ( keep ) Hash_IntFree( keep );
     return 1;
 }
 
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index 6a08a150..9c1e9840 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -30,6 +30,7 @@
 #include "sat/cnf/cnf.h"
 #include "sat/bsat/satSolver.h"
 #include "pdr.h" 
+#include "misc/hash/hashInt.h"
 
 ABC_NAMESPACE_HEADER_START
 
@@ -196,10 +197,13 @@ extern Pdr_Set_t *     Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int n
 extern Pdr_Set_t *     Pdr_SetDup( Pdr_Set_t * pSet );
 extern Pdr_Set_t *     Pdr_SetRef( Pdr_Set_t * p );
 extern void            Pdr_SetDeref( Pdr_Set_t * p );
+extern Pdr_Set_t *     ZPdr_SetIntersection( Pdr_Set_t * p1, Pdr_Set_t * p2, Hash_Int_t * keep );
 extern int             Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
 extern int             Pdr_SetContainsSimple( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
 extern int             Pdr_SetIsInit( Pdr_Set_t * p, int iRemove );
+extern int             ZPdr_SetIsInit( Pdr_Set_t * p );
 extern void            Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
+extern void            ZPdr_SetPrint( Pdr_Set_t * p );
 extern void            Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
 extern int             Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 );
 extern Pdr_Obl_t *     Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext );
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index 2e6130aa..eb94a826 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -51,7 +51,8 @@ sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k )
     assert( Vec_VecSize(p->vClauses) == k );
     assert( Vec_IntSize(p->vActVars) == k );
     // create new solver
-    pSat = sat_solver_new();
+//    pSat = sat_solver_new();
+    pSat = zsat_solver_new_seed(p->pPars->nRandomSeed);
     pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
     Vec_PtrPush( p->vSolvers, pSat );
     Vec_VecExpand( p->vClauses, k );
@@ -86,7 +87,8 @@ sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k )
     p->nStarts++;
 //    sat_solver_delete( pSat );
 //    pSat = sat_solver_new();
-    sat_solver_restart( pSat );
+//    sat_solver_restart( pSat );
+    zsat_solver_restart_seed( pSat, p->pPars->nRandomSeed );
     // create new SAT solver
     pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
     // write new SAT solver
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index 32d1c857..37f84667 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -476,7 +476,9 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
     assert( Vec_IntSize(vRes) > 0 );
     p->tTsim += Abc_Clock() - clk;
     pRes = Pdr_SetCreate( vRes, vPiLits );
-    assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
+    //ZH: Disabled assertion because this invariant doesn't hold with down
+    //because of the join operation which can bring in initial states
+    //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
     return pRes;
 }
 
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index 32e97772..8fb83fd2 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -260,6 +260,85 @@ void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCoun
   SeeAlso     []
 
 ***********************************************************************/
+void ZPdr_SetPrint( Pdr_Set_t * p )
+{
+    int i;
+    for ( i = 0; i < p->nLits; i++)
+        printf ("%d ", p->Lits[i]);
+    printf ("\n");
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Return the intersection of p1 and p2.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Pdr_Set_t * ZPdr_SetIntersection( Pdr_Set_t * p1, Pdr_Set_t * p2, Hash_Int_t * keep )
+{
+    Pdr_Set_t * pIntersection;
+    Vec_Int_t * vCommonLits, * vPiLits;
+    int i, j, nLits;
+    nLits = p1->nLits;
+    if ( p2->nLits < nLits )
+        nLits = p2->nLits;
+    vCommonLits = Vec_IntAlloc( nLits );
+    vPiLits = Vec_IntAlloc( 1 );
+    for ( i = 0, j = 0; i < p1->nLits && j < p2->nLits; )
+    {
+        if ( p1->Lits[i] > p2->Lits[j] )
+        {
+            if ( Hash_IntExists( keep, p2->Lits[j] ) )
+            {
+                //about to drop a literal that should not be dropped
+                Vec_IntFree( vCommonLits );
+                Vec_IntFree( vPiLits );
+                return NULL;
+            }
+            j++;
+        }
+        else if ( p1->Lits[i] < p2->Lits[j] )
+        {
+            if ( Hash_IntExists( keep, p1->Lits[i] ) )
+            {
+                //about to drop a literal that should not be dropped
+                Vec_IntFree( vCommonLits );
+                Vec_IntFree( vPiLits );
+                return NULL;
+            }
+            i++;
+        }
+        else
+        {
+          Vec_IntPush( vCommonLits, p1->Lits[i] );
+          i++;
+          j++;
+        }
+    }
+    pIntersection = Pdr_SetCreate( vCommonLits, vPiLits );
+    Vec_IntFree( vCommonLits );
+    Vec_IntFree( vPiLits );
+    return pIntersection;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Pdr_SetPrintStr( Vec_Str_t * vStr, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts )
 {
     char * pBuff;