Merged alanmi/abc into default

src/base/abci/abc.c

@@ -25838,7 +25838,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, "MFCDRTHGaxrmsipdgovwzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDRTHGaxrmsipdegovwzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -25954,6 +25954,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             pPars->fDumpInv ^= 1;
             break;
+        case 'e':
+            pPars->fUseSupp ^= 1;
+            break;
         case 'g':
             pPars->fSkipGeneral ^= 1;
             break;
@@ -26001,7 +26004,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: pdr [-MFCDRTHG <num>] [-axrmsipdgovwzh]\n" );
+    Abc_Print( -2, "usage: pdr [-MFCDRTHG <num>] [-axrmsipdegovwzh]\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         with improvements by Niklas Een (http://een.se/niklas/)\n" );
@@ -26021,6 +26024,7 @@ usage:
     Abc_Print( -2, "\t-i     : toggle clause pushing from an intermediate timeframe [default = %s]\n",       pPars->fShiftStart? "yes": "no" );
     Abc_Print( -2, "\t-p     : toggle reusing proof-obligations in the last timeframe [default = %s]\n",     pPars->fReuseProofOblig? "yes": "no" );
     Abc_Print( -2, "\t-d     : toggle dumping invariant (valid if init state is all-0) [default = %s]\n",    pPars->fDumpInv? "yes": "no" );
+    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-v     : toggle printing optimization summary [default = %s]\n",                       pPars->fVerbose? "yes": "no" );

src/base/wlc/wlcReadSmt.c

@@ -981,12 +981,25 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
                 assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) );
                 Range = 1;
                 pValue = Smt_VecEntryName(p, vFans, 4);
-                if ( !strcmp("false", pValue) )
-                    pValue = "#b0";
-                else if ( !strcmp("true", pValue) )
-                    pValue = "#b1";
-                else assert( 0 );
-                Status = Smt_PrsBuildConstant( pNtk, pValue, Range, pName );
+                if ( pValue != NULL )
+                {
+                    if ( !strcmp("false", pValue) )
+                        pValue = "#b0";
+                    else if ( !strcmp("true", pValue) )
+                        pValue = "#b1";
+                    else assert( 0 );
+                    Status = Smt_PrsBuildConstant( pNtk, pValue, Range, pName );
+                }
+                else
+                {
+                    iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 4), -1, pName );
+                    if ( iObj == 0 )
+                    {
+                        Wlc_NtkFree( pNtk ); pNtk = NULL;
+                        goto finish;
+                    }
+                    continue;
+                }
             }
             else
             {

src/proof/pdr/pdr.h

@@ -52,6 +52,7 @@ struct Pdr_Par_t_
     int fTwoRounds;       // use two rounds for generalization
     int fMonoCnf;         // monolythic CNF
     int fDumpInv;         // dump inductive invariant
+    int fUseSupp;         // use support in the invariant
     int fShortest;        // forces bug traces to be shortest
     int fShiftStart;      // allows clause pushing to start from an intermediate frame
     int fReuseProofOblig; // reuses proof-obligationgs in the last timeframe

src/proof/pdr/pdrCore.c

@@ -60,6 +60,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
     pPars->fTwoRounds     =       0;  // use two rounds for generalization
     pPars->fMonoCnf       =       0;  // monolythic CNF
     pPars->fDumpInv       =       0;  // dump inductive invariant
+    pPars->fUseSupp       =       1;  // using support variables in the invariant
     pPars->fShortest      =       0;  // forces bug traces to be shortest
     pPars->fUsePropOut    =       1;  // use property output
     pPars->fVerbose       =       0;  // verbose output

src/proof/pdr/pdrInv.c

@@ -339,7 +339,6 @@ void Pdr_ManDumpAig( Aig_Man_t * p, Vec_Ptr_t * vCubes )
 ***********************************************************************/
 void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
 {
-    int fUseSupp = 1;
     FILE * pFile;
     Vec_Int_t * vFlopCounts;
     Vec_Ptr_t * vCubes;
@@ -370,14 +369,14 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
         Count++;
     }
     // collect variable appearances
-    vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
+    vFlopCounts = p->pPars->fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
     // output the header
     if ( fProved )
         fprintf( pFile, "# Inductive invariant for \"%s\"\n", p->pAig->pName );
     else
         fprintf( pFile, "# Clauses of the last timeframe for \"%s\"\n", p->pAig->pName );
     fprintf( pFile, "# generated by PDR in ABC on %s\n", Aig_TimeStamp() );
-    fprintf( pFile, ".i %d\n", fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) );
+    fprintf( pFile, ".i %d\n", p->pPars->fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) );
     fprintf( pFile, ".o 1\n" );
     fprintf( pFile, ".p %d\n", Count );
     // output flop names
@@ -386,7 +385,7 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
     {
         fprintf( pFile, ".ilb" );
         for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
-            if ( !fUseSupp || Vec_IntEntry( vFlopCounts, i ) )
+            if ( !p->pPars->fUseSupp || Vec_IntEntry( vFlopCounts, i ) )
                 fprintf( pFile, " %s", pNamesCi[Saig_ManPiNum(p->pAig) + i] );
         fprintf( pFile, "\n" );
         ABC_FREE( pNamesCi );
@@ -423,7 +422,6 @@ void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName, int fProved )
 ***********************************************************************/
 Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p )
 {
-    int fUseSupp = 1;
     Vec_Str_t * vStr;
     Vec_Int_t * vFlopCounts;
     Vec_Ptr_t * vCubes;
@@ -438,7 +436,7 @@ Vec_Str_t * Pdr_ManDumpString( Pdr_Man_t * p )
         vCubes = Vec_PtrDup( p->vInfCubes );
     Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
     // collect variable appearances
-    vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
+    vFlopCounts = p->pPars->fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL; 
     // output cubes
     Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
     {