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

src/base/abci/abc.c

@@ -26008,7 +26008,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Pdr_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDRTHGaxrmsipdegovwzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDRTHGSaxrmsipdegoncvwzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -26100,6 +26100,17 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nTimeOutGap < 0 )
                 goto usage;
             break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nRandomSeed = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nRandomSeed < 0 )
+                goto usage;
+            break;
         case 'a':
             pPars->fSolveAll ^= 1;
             break;
@@ -26133,6 +26144,12 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'o':
             pPars->fUsePropOut ^= 1;
             break;
+        case 'n':
+            pPars->fSkipDown ^= 1;
+            break;
+        case 'c':
+            pPars->fCtgs ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -26174,9 +26191,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: pdr [-MFCDRTHG <num>] [-axrmsipdegovwzh]\n" );
+    Abc_Print( -2, "usage: pdr [-MFCDRTHGS <num>] [-axrmsipdegoncvwzh]\n" );
     Abc_Print( -2, "\t         model checking using property directed reachability (aka IC3)\n" );
-    Abc_Print( -2, "\t         pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\n" );
+    Abc_Print( -2, "\t         pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" );
     Abc_Print( -2, "\t         with improvements by Niklas Een (http://een.se/niklas/)\n" );
     Abc_Print( -2, "\t-M num : limit on unused vars to trigger SAT solver recycling [default = %d]\n",       pPars->nRecycle );
     Abc_Print( -2, "\t-F num : limit on timeframes explored to stop computation [default = %d]\n",           pPars->nFrameMax );
@@ -26186,6 +26203,7 @@ usage:
     Abc_Print( -2, "\t-T num : runtime limit, in seconds (0 = no limit) [default = %d]\n",                   pPars->nTimeOut );
     Abc_Print( -2, "\t-H num : runtime limit per output, in miliseconds (with \"-a\") [default = %d]\n",     pPars->nTimeOutOne );
     Abc_Print( -2, "\t-G num : runtime gap since the last CEX (0 = no limit) [default = %d]\n",              pPars->nTimeOutGap );
+    Abc_Print( -2, "\t-S num : * value to seed the SAT solver with [default = %d]\n",                          pPars->nRandomSeed );
     Abc_Print( -2, "\t-a     : toggle solving all outputs even if one of them is SAT [default = %s]\n",      pPars->fSolveAll? "yes": "no" );
     Abc_Print( -2, "\t-x     : toggle storing CEXes when solving all outputs [default = %s]\n",              pPars->fStoreCex? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle using more effort in generalization [default = %s]\n",                 pPars->fTwoRounds? "yes": "no" );
@@ -26197,10 +26215,19 @@ usage:
     Abc_Print( -2, "\t-e     : toggle using only support variables in the invariant [default = %s]\n",       pPars->fUseSupp? "yes": "no" );
     Abc_Print( -2, "\t-g     : toggle skipping expensive generalization step [default = %s]\n",              pPars->fSkipGeneral? "yes": "no" );
     Abc_Print( -2, "\t-o     : toggle using property output as inductive hypothesis [default = %s]\n",       pPars->fUsePropOut? "yes": "no" );
+    Abc_Print( -2, "\t-n     : * toggle skipping \'down\' in generalization [default = %s]\n",                 pPars->fSkipDown? "yes": "no" );
+    Abc_Print( -2, "\t-c     : * toggle handling CTGs in \'down\' [default = %s]\n",                           pPars->fCtgs? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing optimization summary [default = %s]\n",                       pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing detailed stats default = %s]\n",                              pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-z     : toggle suppressing report about solved outputs [default = %s]\n",             pPars->fNotVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
+    Abc_Print( -2, "\t-h     : print the command usage\n\n");
+    Abc_Print( -2, "\t* Implementation of switches -S, -n, and -c is contributed by Zyad Hassan.\n");
+    Abc_Print( -2, "\t  The theory and experiments supporting this work can be found in the following paper:\n");
+    Abc_Print( -2, "\t  Zyad Hassan, Aaron R. Bradley, Fabio Somenzi, \"Better Generalization in IC3\", FMCAD 2013.\n");
+    Abc_Print( -2, "\t  (http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD13/papers/85-Better-Generalization-IC3.pdf)\n");
+
+    
+
     return 1;
 }
 

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

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 );

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

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;
 }
 

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;

src/sat/bsat/satSolver.c

@@ -1085,6 +1085,77 @@ sat_solver* sat_solver_new(void)
     return s;
 }
 
+sat_solver* zsat_solver_new_seed(double seed)
+{
+    sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver));
+
+//    Vec_SetAlloc_(&s->Mem, 15);
+    Sat_MemAlloc_(&s->Mem, 15);
+    s->hLearnts = -1;
+    s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
+    s->binary = clause_read( s, s->hBinary );
+
+    s->nLearntStart = LEARNT_MAX_START_DEFAULT;  // starting learned clause limit
+    s->nLearntDelta = LEARNT_MAX_INCRE_DEFAULT;  // delta of learned clause limit
+    s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT;  // ratio of learned clause limit
+    s->nLearntMax   = s->nLearntStart;
+
+    // initialize vectors
+    veci_new(&s->order);
+    veci_new(&s->trail_lim);
+    veci_new(&s->tagged);
+//    veci_new(&s->learned);
+    veci_new(&s->act_clas);
+    veci_new(&s->stack);
+//    veci_new(&s->model);
+    veci_new(&s->act_vars);
+    veci_new(&s->unit_lits);
+    veci_new(&s->temp_clause);
+    veci_new(&s->conf_final);
+
+    // initialize arrays
+    s->wlists    = 0;
+    s->activity  = 0;
+    s->orderpos  = 0;
+    s->reasons   = 0;
+    s->trail     = 0;
+
+    // initialize other vars
+    s->size                   = 0;
+    s->cap                    = 0;
+    s->qhead                  = 0;
+    s->qtail                  = 0;
+#ifdef USE_FLOAT_ACTIVITY
+    s->var_inc                = 1;
+    s->cla_inc                = 1;
+    s->var_decay              = (float)(1 / 0.95 );
+    s->cla_decay              = (float)(1 / 0.999);
+#else
+    s->var_inc                = (1 <<  5);
+    s->cla_inc                = (1 << 11);
+#endif
+    s->root_level             = 0;
+//    s->simpdb_assigns         = 0;
+//    s->simpdb_props           = 0;
+    s->random_seed            = seed;
+    s->progress_estimate      = 0;
+//    s->binary                 = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
+//    s->binary->size_learnt    = (2 << 1);
+    s->verbosity              = 0;
+
+    s->stats.starts           = 0;
+    s->stats.decisions        = 0;
+    s->stats.propagations     = 0;
+    s->stats.inspects         = 0;
+    s->stats.conflicts        = 0;
+    s->stats.clauses          = 0;
+    s->stats.clauses_literals = 0;
+    s->stats.learnts          = 0;
+    s->stats.learnts_literals = 0;
+    s->stats.tot_literals     = 0;
+    return s;
+}
+
 void sat_solver_setnvars(sat_solver* s,int n)
 {
     int var;
@@ -1248,6 +1319,55 @@ void sat_solver_restart( sat_solver* s )
     s->stats.tot_literals     = 0;
 }
 
+void zsat_solver_restart_seed( sat_solver* s, double seed )
+{
+    int i;
+    Sat_MemRestart( &s->Mem );
+    s->hLearnts = -1;
+    s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
+    s->binary = clause_read( s, s->hBinary );
+
+    veci_resize(&s->act_clas, 0);
+    veci_resize(&s->trail_lim, 0);
+    veci_resize(&s->order, 0);
+    for ( i = 0; i < s->size*2; i++ )
+        s->wlists[i].size = 0;
+
+    s->nDBreduces = 0;
+
+    // initialize other vars
+    s->size                   = 0;
+//    s->cap                    = 0;
+    s->qhead                  = 0;
+    s->qtail                  = 0;
+#ifdef USE_FLOAT_ACTIVITY
+    s->var_inc                = 1;
+    s->cla_inc                = 1;
+    s->var_decay              = (float)(1 / 0.95  );
+    s->cla_decay              = (float)(1 / 0.999 );
+#else
+    s->var_inc                = (1 <<  5);
+    s->cla_inc                = (1 << 11);
+#endif
+    s->root_level             = 0;
+//    s->simpdb_assigns         = 0;
+//    s->simpdb_props           = 0;
+    s->random_seed            = seed;
+    s->progress_estimate      = 0;
+    s->verbosity              = 0;
+
+    s->stats.starts           = 0;
+    s->stats.decisions        = 0;
+    s->stats.propagations     = 0;
+    s->stats.inspects         = 0;
+    s->stats.conflicts        = 0;
+    s->stats.clauses          = 0;
+    s->stats.clauses_literals = 0;
+    s->stats.learnts          = 0;
+    s->stats.learnts_literals = 0;
+    s->stats.tot_literals     = 0;
+}
+
 // returns memory in bytes used by the SAT solver
 double sat_solver_memory( sat_solver* s )
 {

src/sat/bsat/satSolver.h

@@ -42,6 +42,7 @@ struct sat_solver_t;
 typedef struct sat_solver_t sat_solver;
 
 extern sat_solver* sat_solver_new(void);
+extern sat_solver* zsat_solver_new_seed(double seed);
 extern void        sat_solver_delete(sat_solver* s);
 
 extern int         sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
@@ -54,6 +55,7 @@ extern int         sat_solver_push(sat_solver* s, int p);
 extern void        sat_solver_pop(sat_solver* s);
 extern void        sat_solver_set_resource_limits(sat_solver* s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
 extern void        sat_solver_restart( sat_solver* s );
+extern void        zsat_solver_restart_seed( sat_solver* s, double seed );
 extern void        sat_solver_rollback( sat_solver* s );
 
 extern int         sat_solver_nvars(sat_solver* s);