Added command 'cexsave' and 'cexload'.

src/base/abci/abc.c

@@ -294,7 +294,9 @@ static int Abc_CommandBm                     ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandTestCex                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPdr                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandReconcile              ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandCexMin                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCexSave                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCexLoad                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandCexMin                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDualRail               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBlockPo                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIso                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -362,7 +364,8 @@ static int Abc_CommandAbc9ReachN             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9ReachY             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Undo               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Iso                ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9CexMin             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9CexCut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandAbc9CexMin             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandAbc9AbsDerive          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9AbsRefine          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -749,7 +752,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "testcex",       Abc_CommandTestCex,          0 );
     Cmd_CommandAdd( pAbc, "Verification", "pdr",           Abc_CommandPdr,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "reconcile",     Abc_CommandReconcile,        1 );
-    Cmd_CommandAdd( pAbc, "Verification", "cexmin",        Abc_CommandCexMin,           0 );
+    Cmd_CommandAdd( pAbc, "Verification", "cexsave",       Abc_CommandCexSave,          0 );
+    Cmd_CommandAdd( pAbc, "Verification", "cexload",       Abc_CommandCexLoad,          0 );
+//    Cmd_CommandAdd( pAbc, "Verification", "cexmin",        Abc_CommandCexMin,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "dualrail",      Abc_CommandDualRail,         1 );
     Cmd_CommandAdd( pAbc, "Verification", "blockpo",       Abc_CommandBlockPo,          1 );
     Cmd_CommandAdd( pAbc, "Verification", "iso",           Abc_CommandIso,              1 );
@@ -814,7 +819,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&reachy",       Abc_CommandAbc9ReachY,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&undo",         Abc_CommandAbc9Undo,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&iso",          Abc_CommandAbc9Iso,          0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmin",       Abc_CommandAbc9CexMin,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
+//    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmin",       Abc_CommandAbc9CexMin,       0 );
 
     Cmd_CommandAdd( pAbc, "Abstraction",  "&abs_derive",   Abc_CommandAbc9AbsDerive,    0 );
     Cmd_CommandAdd( pAbc, "Abstraction",  "&abs_refine",   Abc_CommandAbc9AbsRefine,    0 );
@@ -22480,6 +22486,90 @@ usage:
     return 1;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandCexSave( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pCex == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    ABC_FREE( pAbc->pCex2 );
+    pAbc->pCex2 = Abc_CexDup( pAbc->pCex, -1 );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: cexsave [-h]\n" );
+    Abc_Print( -2, "\t        saves the current CEX into the internal storage\n" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandCexLoad( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pCex == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    ABC_FREE( pAbc->pCex );
+    pAbc->pCex = Abc_CexDup( pAbc->pCex2, -1 );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: cexload [-h]\n" );
+    Abc_Print( -2, "\t        loads the current CEX from the internal storage\n" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -28514,6 +28604,99 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pGiaNew;
+    int c;
+    int iFrStart = 0;
+    int iFrStop  = ABC_INFINITY;
+    int fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FGvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            iFrStart = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( iFrStart < 0 )
+                goto usage;
+            break;
+        case 'G':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            iFrStop = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( iFrStop < 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            Abc_Print( -2, "Unknown switch.\n");
+            goto usage;
+        }
+    }
+
+    if ( pAbc->pCex == NULL )
+    {
+        Abc_Print( 1, "There is no current cex.\n");
+        return 0;
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( 1, "There is no AIG in the &-space.\n");
+        return 0;
+    }
+    if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) )
+    {
+        Abc_Print( 1, "Current counter-example is not a valid counter-example for &-space AIG \"%s\".\n", Gia_ManName(pAbc->pGia) );
+        return 0;
+    }
+    if ( iFrStop == ABC_INFINITY )
+        iFrStop = pAbc->pCex->iFrame;
+
+    pGiaNew = Bmc_GiaTargetStates( pAbc->pGia, pAbc->pCex, iFrStart, iFrStop, fVerbose );
+    if ( pGiaNew == NULL )
+    {
+        Abc_Print( 1, "Command has failed.\n");
+        return 0;
+    }
+    Abc_CommandUpdate9( pAbc, pGiaNew );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &cexcut [-FG num] [-vh]\n" );
+    Abc_Print( -2, "\t         extract logic representation of bad states\n" );
+    Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart );
+    Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n",   iFrStop );
+    Abc_Print( -2, "\t-v     : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9CexMin( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int nRealPis, int fJustMax, int fUseAll, int fVerbose );

src/base/main/mainFrame.c

@@ -190,6 +190,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     }
     Vec_PtrFreeP( &p->vLTLProperties_global );
     Abc_FrameDeleteAllNetworks( p );
+    ABC_FREE( p->pCex2 );
     ABC_FREE( p->pCex );
     ABC_FREE( p );
     s_GlobalFrame = NULL;

src/base/main/mainInt.h

@@ -97,6 +97,7 @@ struct Abc_Frame_t_
     Gia_Man_t *     pGia;          // alternative current network as a light-weight AIG
     Gia_Man_t *     pGia2;         // copy of the above
     Abc_Cex_t *     pCex;          // a counter-example to fail the current network
+    Abc_Cex_t *     pCex2;         // copy of the above
     Vec_Ptr_t *     vCexVec;       // a vector of counter-examples if more than one PO fails
     Vec_Ptr_t *     vPoEquivs;     // equivalence classes of isomorphic primary outputs
     int             Status;                // the status of verification problem (proved=1, disproved=0, undecided=-1)

src/sat/bmc/bmc.h

@@ -27,6 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 #include "aig/saig/saig.h"
+#include "aig/gia/gia.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -66,13 +67,16 @@ struct Saig_ParBmc_t_
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== saigBmc.c ==========================================================*/
+/*=== bmcBmc.c ==========================================================*/
 extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
+/*=== bmcBmc2.c ==========================================================*/
 extern int               Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent );
-/*=== saigBmc3.c ==========================================================*/
+/*=== bmcBmc3.c ==========================================================*/
 extern void              Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
 extern int               Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
-/*=== saigCexMin.c ==========================================================*/
+/*=== bmcCexCut.c ==========================================================*/
+extern Gia_Man_t *       Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fVerbose );
+/*=== bmcCexMin.c ==========================================================*/
 extern Abc_Cex_t *       Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
 
 

src/sat/bmc/bmcBmc.c

@@ -18,7 +18,6 @@
 
 ***********************************************************************/
 
-#include "aig/saig/saig.h"
 #include "proof/fra/fra.h"
 #include "sat/cnf/cnf.h"
 #include "sat/bsat/satStore.h"

src/sat/bmc/bmcBmc2.c

@@ -18,7 +18,6 @@
 
 ***********************************************************************/
 
-#include "aig/saig/saig.h"
 #include "sat/cnf/cnf.h"
 #include "sat/bsat/satStore.h"
 #include "proof/ssw/ssw.h"

src/sat/bmc/bmcBmc3.c

@@ -18,7 +18,6 @@
 
 ***********************************************************************/
 
-#include "aig/saig/saig.h"
 #include "proof/fra/fra.h"
 #include "sat/cnf/cnf.h"
 #include "sat/bsat/satStore.h"

src/sat/bmc/bmcCexCut.c

@@ -33,7 +33,7 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Generate GIA for target bad states.]
 
   Description []
                
@@ -42,6 +42,10 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd )
+{
+    return NULL;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/sat/bmc/bmcCexMin1.c

@@ -18,7 +18,6 @@
 
 ***********************************************************************/
 
-#include "aig/saig/saig.h"
 #include "aig/ioa/ioa.h"
 #include "bmc.h"