Prepared &gla to try abstracting and proving concurrently.

abclib.dsp

@@ -2383,6 +2383,10 @@ SOURCE=.\src\map\scl\sclTime.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\map\scl\sclUpsize.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\map\scl\sclUtil.c
 # End Source File
 # End Group
@@ -3423,6 +3427,10 @@ SOURCE=.\src\aig\gia\giaAbsOut.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaAbsPth.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaAbsRef.c
 # End Source File
 # Begin Source File

src/aig/gia/gia.h

@@ -233,12 +233,14 @@ struct Gia_ParVta_t_
     int            fUseFullProof; // use full proof for UNSAT cores
     int            fDumpVabs;     // dumps the abstracted model
     int            fDumpMabs;     // dumps the original AIG with abstraction map
+    int            fCallProver;   // calls the prover
     char *         pFileVabs;     // dumps the abstracted model into this file
     int            fVerbose;      // verbose flag
     int            fVeryVerbose;  // print additional information
     int            iFrame;        // the number of frames covered
     int            iFrameProved;  // the number of frames proved
     int            nFramesNoChange; // the number of last frames without changes
+    int            nFramesNoChangeLim; // the number of last frames without changes to dump abstraction
 };
 
 static inline unsigned     Gia_ObjCutSign( unsigned ObjId )       { return (1 << (ObjId & 31));                                 }

src/aig/gia/giaAbsGla2.c

@@ -125,6 +125,12 @@ static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
     return Lit;
 }
 
+
+// calling pthreads
+extern void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose );
+extern void Gia_Ga2ProveCancel( int fVerbose );
+extern int  Gia_Ga2ProveCheck( int fVerbose );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -1423,26 +1429,33 @@ char * Ga2_GlaGetFileName( Ga2_Man_t * p, int fAbs )
 
 void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
 {
-//    if ( fVerbose )
-//        Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
-    if ( p->pPars->fDumpVabs )
+    char * pFileName;
+    assert( p->pPars->fDumpMabs || p->pPars->fDumpVabs || p->pPars->fCallProver );
+    if ( p->pPars->fDumpMabs )
+    {
+        pFileName = Ga2_GlaGetFileName(p, 0);
+        if ( fVerbose )
+            Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
+        // dump abstraction map
+        Vec_IntFreeP( &p->pGia->vGateClasses );
+        p->pGia->vGateClasses = Ga2_ManAbsTranslate( p );
+        Gia_WriteAiger( p->pGia, pFileName, 0, 0 );
+    }
+    if ( p->pPars->fDumpVabs || p->pPars->fCallProver )
     {
+        Vec_Int_t * vGateClasses;
+        Gia_Man_t * pAbs;
+        pFileName = Ga2_GlaGetFileName(p, 1);
+        if ( fVerbose )
+            Abc_Print( 1, "Dumping abstracted model into file \"%s\"...\n", pFileName );
         // dump absracted model
-        Vec_Int_t * vGateClasses = Ga2_ManAbsTranslate( p );
-        Gia_Man_t * pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
+        vGateClasses = Ga2_ManAbsTranslate( p );
+        pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
         Gia_ManCleanValue( p->pGia );
-        Gia_WriteAiger( pAbs, Ga2_GlaGetFileName(p, 1), 0, 0 );
+        Gia_WriteAiger( pAbs, pFileName, 0, 0 );
         Gia_ManStop( pAbs );
         Vec_IntFreeP( &vGateClasses );
     }
-    else if ( p->pPars->fDumpMabs )
-    {
-        // dump abstraction map
-        Vec_IntFreeP( &p->pGia->vGateClasses );
-        p->pGia->vGateClasses = Ga2_ManAbsTranslate( p );
-        Gia_WriteAiger( p->pGia, Ga2_GlaGetFileName(p, 0), 0, 0 );
-    }
-    else assert( 0 );
 }
 
 /**Function*************************************************************
@@ -1499,7 +1512,7 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
     Ga2_Man_t * p;
     Vec_Int_t * vCore, * vPPis;
     clock_t clk2, clk = clock();
-    int Status = l_Undef, RetValue = -1, fOneIsSent = 0;
+    int Status = l_Undef, RetValue = -1, iFrameTryProve = -1, fOneIsSent = 0;
     int i, c, f, Lit;
     // check trivial case 
     assert( Gia_ManPoNum(pAig) == 1 ); 
@@ -1618,6 +1631,11 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                         Gia_Ga2SendCancel( p, pPars->fVerbose );
                         fOneIsSent = 0;
                     }
+                    if ( iFrameTryProve >= 0 )
+                    {
+                        Gia_Ga2ProveCancel( pPars->fVerbose );
+                        iFrameTryProve = -1;
+                    }
 
                     if ( c == 0 )
                     {
@@ -1723,8 +1741,16 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
             // print statistics
             if ( pPars->fVerbose )
                 Ga2_ManAbsPrintFrame( p, f, sat_solver2_nconflicts(p->pSat)-nConflsBeg, c, clock() - clk, 1 );
+            // check if abstraction was proved
+            if ( Gia_Ga2ProveCheck( pPars->fVerbose ) )
+            {
+                RetValue = 1;
+                goto finish;
+            }
             if ( c > 0 ) 
             {
+                if ( p->pPars->fVeryVerbose )
+                    Abc_Print( 1, "\n" );
                 // recompute the abstraction
                 Vec_IntFreeP( &pAig->vGateClasses );
                 pAig->vGateClasses = Ga2_ManAbsTranslate( p );
@@ -1734,18 +1760,12 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                     Status = l_Undef;
                     goto finish;
                 }
-                // speak to the bridge
-                if ( Abc_FrameIsBridgeMode() )
-                {
-                    // cancel old one if it was sent
-                    if ( fOneIsSent )
-                        Gia_Ga2SendCancel( p, pPars->fVerbose );
-                    // send new one 
-                    Gia_Ga2SendAbsracted( p, pPars->fVerbose );
-                    fOneIsSent = 1;
             }
+            // check the number of stable frames
+            if ( p->pPars->nFramesNoChange == p->pPars->nFramesNoChangeLim )
+            {
                 // dump the model into file
-                if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs )
+                if ( p->pPars->fDumpVabs || p->pPars->fDumpMabs || p->pPars->fCallProver )
                 {
                     char Command[1000];
                     Abc_FrameSetStatus( -1 );
@@ -1755,12 +1775,31 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
                     Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
                     Ga2_GlaDumpAbsracted( p, pPars->fVerbose );
                 }
-                if ( p->pPars->fVeryVerbose )
-                    Abc_Print( 1, "\n" );
+                // call the prover
+                if ( p->pPars->fCallProver )
+                {
+                    // cancel old one if it is proving
+                    if ( iFrameTryProve >= 0 )
+                        Gia_Ga2ProveCancel( pPars->fVerbose );
+                    // prove new one
+                    Gia_Ga2ProveAbsracted( Ga2_GlaGetFileName(p, 1), pPars->fVerbose );
+                    iFrameTryProve = f;
+                }
+                // speak to the bridge
+                if ( Abc_FrameIsBridgeMode() )
+                {
+                    // cancel old one if it was sent
+                    if ( fOneIsSent )
+                        Gia_Ga2SendCancel( p, pPars->fVerbose );
+                    // send new one 
+                    Gia_Ga2SendAbsracted( p, pPars->fVerbose );
+                    fOneIsSent = 1;
+                }
+            }
             // if abstraction grew more than a certain percentage, force a restart
             if ( pPars->nRatioMax == 0 )
                 break;
-                if ( (f > 20 || Vec_IntSize(p->vAbs) > 100) && Vec_IntSize(p->vAbs) - nAbsOld >= nAbsOld * pPars->nRatioMax / 100 )
+            if ( c > 0 && (f > 20 || Vec_IntSize(p->vAbs) > 100) && Vec_IntSize(p->vAbs) - nAbsOld >= nAbsOld * pPars->nRatioMax / 100 )
             {
                 if ( p->pPars->fVerbose )
                 Abc_Print( 1, "Forcing restart because abstraction grew from %d to %d (more than %d %%).\n", 
@@ -1769,11 +1808,12 @@ int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
             }
         }
     }
-    }
 finish:
     Prf_ManStopP( &p->pSat->pPrf2 );
     // analize the results
-    if ( pAig->pCexSeq == NULL )
+    if ( RetValue == 1 )
+        Abc_Print( 1, "GLA completed %d frames and proved abstraction derived in frame %d.  ", p->pPars->iFrameProved+1, iFrameTryProve );
+    else if ( pAig->pCexSeq == NULL )
     {
 //        if ( pAig->vGateClasses != NULL )
 //            Abc_Print( 1, "Replacing the old abstraction by a new one.\n" );

src/aig/gia/giaAbsPth.c

+/**CFile****************************************************************
+
+  FileName    [giaAbsPth.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Interface to pthreads.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaAbsPth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#include "gia.h"
+
+// comment this out to disable pthreads
+//#define ABC_USE_PTHREADS
+
+#ifdef ABC_USE_PTHREADS
+
+#ifdef WIN32
+#include "../lib/pthread.h"
+#else
+#include <pthread.h>
+#include <unistd.h>
+#endif
+
+#endif
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Start and stop proving abstracted model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+#ifndef ABC_USE_PTHREADS
+
+void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose ) {}
+void Gia_Ga2ProveCancel( int fVerbose )                      {}
+int  Gia_Ga2ProveCheck( int fVerbose )                       { return 0; }
+
+#else // pthreads are used
+
+void Gia_Ga2ProveAbsracted( char * pFileName, int fVerbose )
+{
+    Abc_Print( 1, "Trying to prove abstraction.\n" );
+}
+void Gia_Ga2ProveCancel( int fVerbose )
+{
+    Abc_Print( 1, "Canceling attempt to prove abstraction.\n" );
+}
+int Gia_Ga2ProveCheck( int fVerbose )
+{
+    return 0;
+}
+
+#endif
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/aig/gia/giaAbsVta.c

@@ -157,7 +157,7 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
     p->nLearnedDelta      =    200;   // max number of learned clauses
     p->nLearnedPerce      =     70;   // max number of learned clauses
     p->nTimeOut           =      0;   // timeout in seconds
-    p->nRatioMin     =     20;   // stop when less than this % of object is abstracted
+    p->nRatioMin          =      0;   // stop when less than this % of object is abstracted
     p->nRatioMax          =     30;   // restart when more than this % of object is abstracted
     p->fUseTermVars       =      0;   // use terminal variables
     p->fUseRollback       =      0;   // use rollback to the starting number of frames
@@ -165,6 +165,7 @@ void Gia_VtaSetDefaultParams( Gia_ParVta_t * p )
     p->fVerbose           =      0;   // verbose flag
     p->iFrame             =     -1;   // the number of frames covered 
     p->iFrameProved       =     -1;   // the number of frames proved
+    p->nFramesNoChangeLim =      1;   // the number of frames without change to dump abstraction
 }
 
 /**Function*************************************************************

src/aig/gia/module.make

@@ -4,6 +4,7 @@ SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaAbsGla2.c \
     src/aig/gia/giaAbsIter.c \
     src/aig/gia/giaAbsOut.c \
+    src/aig/gia/giaAbsPth.c \
     src/aig/gia/giaAbsRef.c \
     src/aig/gia/giaAbsRef2.c \
     src/aig/gia/giaAbsVta.c \

src/base/abci/abc.c

@@ -28342,7 +28342,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c, fStartVta = 0, fNewAlgo = 1;
     Gia_VtaSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPAtrfkadmnscbpwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPBAtrfkadmnscbpqwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -28445,6 +28445,17 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nRatioMax < 0 ) 
                 goto usage;
             break;
+        case 'B':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesNoChangeLim = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesNoChangeLim < 0 ) 
+                goto usage;
+            break;
         case 'A':
             if ( globalUtilOptind >= argc )
             {
@@ -28490,6 +28501,9 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             pPars->fUseFullProof ^= 1;
             break;
+        case 'q':
+            pPars->fCallProver ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -28538,7 +28552,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &gla [-FSCLDETRP num] [-A file] [-fkadmnscbpwvh]\n" );
+    Abc_Print( -2, "usage: &gla [-FSCLDETRPB num] [-A file] [-fkadmnscbpqwvh]\n" );
     Abc_Print( -2, "\t          fixed-time-frame gate-level proof- and cex-based abstraction\n" );
     Abc_Print( -2, "\t-F num  : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
     Abc_Print( -2, "\t-S num  : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
@@ -28549,6 +28563,7 @@ usage:
     Abc_Print( -2, "\t-T num  : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
     Abc_Print( -2, "\t-R num  : minimum percentage of abstracted objects (0<=num<=100) [default = %d]\n", pPars->nRatioMin );
     Abc_Print( -2, "\t-P num  : maximum percentage of added objects before a restart (0<=num<=100) [default = %d]\n", pPars->nRatioMax );
+    Abc_Print( -2, "\t-B num  : the number of stable frames to dump abstraction or call prover (0<=num<=100) [default = %d]\n", pPars->nFramesNoChangeLim );
     Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" );
     Abc_Print( -2, "\t-f      : toggle propagating fanout implications [default = %s]\n", pPars->fPropFanout? "yes": "no" );
     Abc_Print( -2, "\t-k      : toggle using VTA to kick start GLA for starting frames [default = %s]\n", fStartVta? "yes": "no" );
@@ -28560,6 +28575,7 @@ usage:
     Abc_Print( -2, "\t-c      : toggle using naive (2-input AND node) CNF encoding [default = %s]\n", pPars->fUseSimple? "yes": "no" );
     Abc_Print( -2, "\t-b      : toggle CNF construction without hashing [default = %s]\n", pPars->fSkipHash? "yes": "no" );
     Abc_Print( -2, "\t-p      : toggle using full-proof for UNSAT cores [default = %s]\n", pPars->fUseFullProof? "yes": "no" );
+    Abc_Print( -2, "\t-q      : toggle calling the prover [default = %s]\n", pPars->fCallProver? "yes": "no" );
     Abc_Print( -2, "\t-v      : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w      : toggle printing more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h      : print the command usage\n");