Merged alanmi/abc into default

abclib.dsp

@@ -1743,6 +1743,14 @@ SOURCE=.\src\sat\bsat\satSolver2i.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\bsat\satSolver3.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\sat\bsat\satSolver3.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\bsat\satStore.c
 # End Source File
 # Begin Source File

src/aig/gia/giaIso.c

@@ -24,7 +24,7 @@ ABC_NAMESPACE_IMPL_START
  
 
 #define ISO_MASK 0xFF
-static int s_256Primes[ISO_MASK+1] = 
+static unsigned int s_256Primes[ISO_MASK+1] = 
 {
     0x984b6ad9,0x18a6eed3,0x950353e2,0x6222f6eb,0xdfbedd47,0xef0f9023,0xac932a26,0x590eaf55,
     0x97d0a034,0xdc36cd2e,0x22736b37,0xdc9066b0,0x2eb2f98b,0x5d9c7baf,0x85747c9e,0x8aca1055,

src/aig/gia/giaIso2.c

@@ -27,7 +27,7 @@ ABC_NAMESPACE_IMPL_START
 
 
 #define ISO_MASK 0xFF
-static int s_256Primes[ISO_MASK+1] = 
+static unsigned int s_256Primes[ISO_MASK+1] = 
 {
     0x984b6ad9,0x18a6eed3,0x950353e2,0x6222f6eb,0xdfbedd47,0xef0f9023,0xac932a26,0x590eaf55,
     0x97d0a034,0xdc36cd2e,0x22736b37,0xdc9066b0,0x2eb2f98b,0x5d9c7baf,0x85747c9e,0x8aca1055,

src/aig/gia/giaSat3.c

+/**CFile****************************************************************
+
+  FileName    [giaSatoko.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Interface to Satoko solver.]
+
+  Author      [Alan Mishchenko, Bruno Schmitt]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaSatoko.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "sat/cnf/cnf.h"
+#include "sat/bsat/satSolver3.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+sat_solver3 * Gia_ManSat3Init( Cnf_Dat_t * pCnf )
+{
+    sat_solver3 * pSat = sat_solver3_new();
+    int i;
+    //sat_solver_setnvars( pSat, p->nVars );
+    for ( i = 0; i < pCnf->nClauses; i++ )
+    {
+        if ( !sat_solver3_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+        {
+            sat_solver3_delete( pSat );
+            return NULL;
+        }
+    }
+    return pSat;
+}
+void Gia_ManSat3Report( int iOutput, int status, abctime clk )
+{
+    if ( iOutput >= 0 )
+        Abc_Print( 1, "Output %6d : ", iOutput );
+    else
+        Abc_Print( 1, "Total: " );
+
+    if ( status == l_Undef )
+        Abc_Print( 1, "UNDECIDED      " );
+    else if ( status == l_True )
+        Abc_Print( 1, "SATISFIABLE    " );
+    else
+        Abc_Print( 1, "UNSATISFIABLE  " );
+
+    Abc_PrintTime( 1, "Time", clk );
+}
+sat_solver3 * Gia_ManSat3Create( Gia_Man_t * p )
+{
+    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 1, 0, 0 );
+    sat_solver3 * pSat = Gia_ManSat3Init( pCnf );
+    int status = pSat ? sat_solver3_simplify(pSat) : 0;
+    Cnf_DataFree( pCnf );
+    if ( status )
+        return pSat;
+    if ( pSat )
+        sat_solver3_delete( pSat );
+    return NULL;
+}
+int Gia_ManSat3CallOne( Gia_Man_t * p, int iOutput )
+{
+    abctime clk = Abc_Clock();
+    sat_solver3 * pSat;
+    int status, Cost = 0;
+
+    pSat = Gia_ManSat3Create( p );
+    if ( pSat )
+    {
+        status = sat_solver3_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
+        Cost = (unsigned)pSat->stats.conflicts;
+        sat_solver3_delete( pSat );
+    }
+    else 
+        status = l_False;
+
+    Gia_ManSat3Report( iOutput, status, Abc_Clock() - clk );
+    return Cost;
+}
+void Gia_ManSat3Call( Gia_Man_t * p, int fSplit )
+{
+    Gia_Man_t * pOne;
+    Gia_Obj_t * pRoot;
+    int i;
+    if ( fSplit )
+    {
+        abctime clk = Abc_Clock();
+        Gia_ManForEachCo( p, pRoot, i )
+        {
+            pOne = Gia_ManDupDfsCone( p, pRoot );
+            Gia_ManSat3CallOne( pOne, i );
+            Gia_ManStop( pOne );
+        }
+        Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
+        return;
+    }
+    Gia_ManSat3CallOne( p, -1 );
+}    
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/aig/gia/module.make

@@ -60,6 +60,7 @@ SRC +=    src/aig/gia/giaAig.c \
     src/aig/gia/giaSatLut.c \
     src/aig/gia/giaSatMap.c \
     src/aig/gia/giaSatoko.c \
+    src/aig/gia/giaSat3.c \
     src/aig/gia/giaScl.c \
     src/aig/gia/giaScript.c \
     src/aig/gia/giaShow.c \

src/aig/saig/saigIsoSlow.c

@@ -120,7 +120,7 @@ static int s_1kPrimes[ISO_MASK+1] = {
 */
 
 #define ISO_MASK 0x3FF
-static int s_1kPrimes[ISO_MASK+1] = 
+static unsigned int s_1kPrimes[ISO_MASK+1] = 
 //#define ISO_MASK 0xFF
 //static int s_1kPrimes[0x3FF+1] = 
 {

src/base/abci/abc.c

@@ -313,6 +313,7 @@ static int Abc_CommandDSat                   ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandXSat                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSatoko                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Satoko             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Sat3               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPSat                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandProve                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIProve                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -965,6 +966,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "xsat",          Abc_CommandXSat,             0 );
     Cmd_CommandAdd( pAbc, "Verification", "satoko",        Abc_CommandSatoko,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "&satoko",       Abc_CommandAbc9Satoko,       0 );
+    Cmd_CommandAdd( pAbc, "Verification", "&sat3",         Abc_CommandAbc9Sat3,         0 );
     Cmd_CommandAdd( pAbc, "Verification", "psat",          Abc_CommandPSat,             0 );
     Cmd_CommandAdd( pAbc, "Verification", "prove",         Abc_CommandProve,            1 );
     Cmd_CommandAdd( pAbc, "Verification", "iprove",        Abc_CommandIProve,           1 );
@@ -23565,6 +23567,74 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Sat3( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Gia_ManSat3Call( Gia_Man_t * p, int fSplit );
+    int c, fSplit = 0, fIncrem = 0;
+
+    satoko_opts_t opts;
+    satoko_default_opts(&opts);
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Csivh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            opts.conf_limit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( opts.conf_limit < 0 )
+                goto usage;
+            break;
+        case 's':
+            fSplit ^= 1;
+            break;
+        case 'i':
+            fIncrem ^= 1;
+            break;
+        case 'v':
+            opts.verbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Sat3(): There is no AIG.\n" );
+        return 1;
+    }
+    Gia_ManSat3Call( pAbc->pGia, fSplit );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &sat3 [-C num] [-sivh]\n" );
+    Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", opts.conf_limit );
+    Abc_Print( -2, "\t-s     : split multi-output miter into individual outputs [default = %s]\n", fSplit? "yes": "no" );
+    Abc_Print( -2, "\t-i     : split multi-output miter and solve incrementally [default = %s]\n", fIncrem? "yes": "no" );
+    Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", opts.verbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandPSat( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);

src/base/main/abcapis.h

@@ -33,6 +33,8 @@
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
+ABC_NAMESPACE_HEADER_START
+
 typedef struct Abc_Frame_t_      Abc_Frame_t;
 
 ////////////////////////////////////////////////////////////////////////
@@ -93,6 +95,7 @@ extern ABC_DLL void   Abc_NtkPrintMiniMapping( int * pArray );
 extern ABC_DLL int    Abc_FrameReadProbStatus( Abc_Frame_t * pAbc );   
 extern ABC_DLL void * Abc_FrameReadCex( Abc_Frame_t * pAbc );    
 
+ABC_NAMESPACE_HEADER_END
 
 #endif
 

src/base/wlc/wlc.h

@@ -177,6 +177,7 @@ struct Wlc_Par_t_
     int                    fPdra;              // Use pdr -nct
     int                    fProofRefine;       // Use proof-based refinement
     int                    fHybrid;            // Use a hybrid of CBR and PBR
+    int                    fCheckCombUnsat;    // Check if ABS becomes comb. unsat
     int                    fVerbose;           // verbose output
     int                    fPdrVerbose;        // verbose output
 };

src/base/wlc/wlcAbs.c

@@ -21,6 +21,7 @@
 #include "wlc.h"
 #include "proof/pdr/pdr.h"
 #include "proof/pdr/pdrInt.h"
+#include "proof/ssw/ssw.h"
 #include "aig/gia/giaAig.h"
 #include "sat/bmc/bmc.h"
 
@@ -33,6 +34,9 @@ ABC_NAMESPACE_IMPL_START
 extern Vec_Vec_t *   IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast );
 extern int           IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap );
 extern int           IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses );
+extern int           IPdr_ManCheckCombUnsat( Pdr_Man_t * p );
+extern int           IPdr_ManReduceClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses );
+extern void          IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs );
 
 typedef struct Int_Pair_t_       Int_Pair_t;
 struct Int_Pair_t_
@@ -302,6 +306,40 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
     return pNew;
 }
 
+static int Wlc_NtkCexIsReal( Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex ) 
+{
+    Gia_Man_t * pGiaOrig = Wlc_NtkBitBlast( pOrig, NULL, -1, 0, 0, 0, 0 );
+    int f, i;
+    Gia_Obj_t * pObj, * pObjRi;
+
+    Gia_ManConst0(pGiaOrig)->Value = 0;
+    Gia_ManForEachRi( pGiaOrig, pObj, i )
+        pObj->Value = 0;
+    for ( f = 0; f <= pCex->iFrame; f++ ) 
+    {
+        for( i = 0; i < Gia_ManPiNum( pGiaOrig ); i++ ) 
+            Gia_ManPi(pGiaOrig, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i);
+        Gia_ManForEachRiRo( pGiaOrig, pObjRi, pObj, i )
+            pObj->Value = pObjRi->Value;
+        Gia_ManForEachAnd( pGiaOrig, pObj, i )
+            pObj->Value = Gia_ObjFanin0Copy(pObj) & Gia_ObjFanin1Copy(pObj);
+        Gia_ManForEachCo( pGiaOrig, pObj, i )
+            pObj->Value = Gia_ObjFanin0Copy(pObj);
+        Gia_ManForEachPo( pGiaOrig, pObj, i ) 
+        {
+            if (pObj->Value==1) {
+                Abc_Print( 1, "CEX is real on the original model.\n" );
+                Gia_ManStop(pGiaOrig);
+                return 1;
+            }
+        }
+    }
+
+    // Abc_Print( 1, "CEX is spurious.\n" );
+    Gia_ManStop(pGiaOrig);
+    return 0;
+}
+
 static Wlc_Ntk_t * Wlc_NtkAbs2( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_Int_t ** pvFlops )
 {
     Vec_Int_t * vFlops  = Vec_IntAlloc( 100 );
@@ -1077,20 +1115,83 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
             Gia_ManPrintStats( pGia, NULL );
         }
         Wlc_NtkFree( pAbs );
+        // Gia_AigerWrite( pGia, "abs.aig", 0, 0 );
 
         // try to prove abstracted GIA by converting it to AIG and calling PDR
         pAig = Gia_ManToAigSimple( pGia );
 
-        pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
-        clk2 = Abc_Clock();
 
+        if ( vClauses && pPars->fCheckCombUnsat )
+        {
+            Pdr_Man_t * pPdr2;
+            
+            if ( Aig_ManAndNum( pAig ) <= 20000 )
+            { 
+                Aig_Man_t * pAigScorr;
+                Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars;
+                int nAnds;
+
+                clk2 = Abc_Clock();
+
+                Ssw_ManSetDefaultParams( pScorrPars );
+                pScorrPars->fStopWhenGone = 1;
+                pScorrPars->nFramesK = 1;
+                pAigScorr = Ssw_SignalCorrespondence( pAig, pScorrPars );
+                assert ( pAigScorr );
+                nAnds = Aig_ManAndNum( pAigScorr); 
+                Aig_ManStop( pAigScorr );
+
+                if ( nAnds == 0 )
+                {
+                    if ( pPars->fVerbose )
+                        Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk2 );
+                    RetValue = 1;
+                    Gia_ManStop( pGia );
+                    Vec_IntFree( vPisNew );
+                    Aig_ManStop( pAig );
+                    break;
+                }
+                else if ( pPars->fVerbose )
+                {
+                    Abc_Print( 1, "SCORR failed with %d ANDs. ", nAnds);
+                    Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
+                }
+            }
+
+            clk2 = Abc_Clock();
+
+            pPdrPars->fVerbose = 0;
+            pPdr2 = Pdr_ManStart( pAig, pPdrPars, NULL );
+            RetValue = IPdr_ManCheckCombUnsat( pPdr2 );
+            Pdr_ManStop( pPdr2 );
+            pPdrPars->fVerbose = pPars->fPdrVerbose;
+
+            tPdr += Abc_Clock() - clk2;
+
+            if ( RetValue == 1 )
+            {
+                if ( pPars->fVerbose )
+                    Abc_PrintTime( 1,  "ABS becomes combinationally UNSAT. Time", Abc_Clock() - clk2 );
+                Gia_ManStop( pGia );
+                Vec_IntFree( vPisNew );
+                Aig_ManStop( pAig );
+                break;
+            }
+            
+            if ( pPars->fVerbose )
+                Abc_PrintTime( 1, "Check comb. unsat failed. Time", Abc_Clock() - clk2 );
+        }
+
+        clk2 = Abc_Clock();
+        pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
         if ( vClauses ) {
             assert( Vec_VecSize( vClauses) >= 2 ); 
             IPdr_ManRestore( pPdr, vClauses, vMap );
         }
         Vec_IntFreeP( &vMap );
 
-        RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses );
+        if ( !vClauses || RetValue != 1 )
+            RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses );
         pPdr->tTotal += Abc_Clock() - clk2;
         tPdr += pPdr->tTotal;
 
@@ -1107,6 +1208,16 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
             break;
         }
 
+        // verify CEX
+        if ( Wlc_NtkCexIsReal( p, pCex ) )
+        {
+            vRefine = NULL;
+            Abc_CexFree( pCex ); // return CEX in the future
+            Pdr_ManStop( pPdr );
+            Aig_ManStop( pAig );
+            break;
+        }
+
         // perform refinement
         if ( pPars->fHybrid || !pPars->fProofRefine )
         {

src/base/wlc/wlcCom.c

@@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Wlc_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcpmxvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcpmuxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -553,6 +553,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'm':
             pPars->fMFFC ^= 1;
             break;
+        case 'u':
+            pPars->fCheckCombUnsat ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -573,7 +576,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     Wlc_NtkPdrAbs( pNtk, pPars );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcpmxvwh]\n" );
+    Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcpmxuvwh]\n" );
     Abc_Print( -2, "\t         abstraction for word-level networks\n" );
     Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
     Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n",        pPars->nBitsMul );
@@ -586,6 +589,7 @@ usage:
     Abc_Print( -2, "\t-b     : toggle using proof-based refinement [default = %s]\n",                  pPars->fProofRefine? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle using both cex-based and proof-based refinement [default = %s]\n",                  pPars->fHybrid? "yes": "no" );
     Abc_Print( -2, "\t-c     : toggle checking clauses in the reloaded trace [default = %s]\n",        pPars->fCheckClauses? "yes": "no" );
+    Abc_Print( -2, "\t-u     : toggle checking combinationally unsat [default = %s]\n",                pPars->fCheckCombUnsat? "yes": "no" );
     Abc_Print( -2, "\t-p     : toggle pushing clauses in the reloaded trace [default = %s]\n",         pPars->fPushClauses? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle refining the whole MFFC of a PPI [default = %s]\n",              pPars->fMFFC? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",                  pPars->fVerbose? "yes": "no" );

src/base/wlc/wlcNtk.c

@@ -121,6 +121,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
     pPars->fPdra         =            0;   // Use pdr -nct 
     pPars->fProofRefine  =            0;   // Use proof-based refinement
     pPars->fHybrid       =            1;   // Use a hybrid of CBR and PBR
+    pPars->fCheckCombUnsat =          0;   // Check if ABS becomes comb. unsat
     pPars->fVerbose      =            0;   // verbose output`
     pPars->fPdrVerbose   =            0;   // show verbose PDR output
 }

src/map/scl/sclCon.h

@@ -56,8 +56,8 @@ struct Scl_Con_t_
 #define SCL_OUTPUT_REQ   "output_required"
 #define SCL_OUTPUT_LOAD  "output_load"
 
-#define SCL_DIRECTIVE(ITEM)     "."ITEM
-#define SCL_DEF_DIRECTIVE(ITEM) ".default_"ITEM
+#define SCL_DIRECTIVE(ITEM)     "."#ITEM
+#define SCL_DEF_DIRECTIVE(ITEM) ".default_"#ITEM
 
 #define SCL_NUM          1000
 #define SCL_INFINITY    (0x3FFFFFFF)

src/proof/pdr/pdrIncr.c

@@ -59,8 +59,9 @@ void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs )
         Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
         Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
         {
-            Abc_Print( 1, "C=%4d. F=%4d ", Counter++, k );
-            Pdr_SetPrint( stdout, pCube, nRegs, NULL );  
+            Abc_Print( 1, "Frame[%4d]Cube[%4d] = ", k, Counter++ );
+            // Pdr_SetPrint( stdout, pCube, nRegs, NULL );  
+            ZPdr_SetPrint( pCube );  
             Abc_Print( 1, "\n" ); 
         }
     }
@@ -738,6 +739,121 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
     return RetValue;
 }
 
+int IPdr_ManCheckCombUnsat( Pdr_Man_t * p )
+{
+    int iFrame, RetValue = -1;
+
+    Pdr_ManCreateSolver( p, (iFrame = 0) );
+    Pdr_ManCreateSolver( p, (iFrame = 1) );
+
+    p->nFrames = iFrame;
+    p->iUseFrame = Abc_MaxInt(iFrame, 1);
+
+    RetValue = Pdr_ManCheckCube( p, iFrame, NULL, NULL, p->pPars->nConfLimit, 0, 1 );
+    return RetValue;
+}
+
+int IPdr_ManCheckCubeReduce( Pdr_Man_t * p, Vec_Ptr_t * vClauses, Pdr_Set_t * pCube, int nConfLimit )
+{ 
+    sat_solver * pSat;
+    Vec_Int_t * vLits, * vLitsA;
+    int Lit, RetValue = l_True;
+    int i;
+    Pdr_Set_t * pCla;
+    int iActVar = 0;
+    abctime clk = Abc_Clock();
+
+    pSat = Pdr_ManSolver( p, 1 );
+
+    if ( pCube == NULL ) // solve the property
+    {
+        Lit = toLit( Pdr_ObjSatVar(p, 1, 2, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails)
+        RetValue = sat_solver_addclause( pSat, &Lit, &Lit+1 );
+        assert( RetValue == 1 );
+
+        vLitsA = Vec_IntStart( Vec_PtrSize( vClauses ) );
+        iActVar = Pdr_ManFreeVar( p, 1 );
+        for ( i = 1; i < Vec_PtrSize( vClauses ); ++i )
+            Pdr_ManFreeVar( p, 1 );
+        Vec_PtrForEachEntry( Pdr_Set_t *, vClauses, pCla, i )
+        {
+            vLits = Pdr_ManCubeToLits( p, 1, pCla, 1, 0 );
+            Lit = Abc_Var2Lit( iActVar + i, 1 );
+            Vec_IntPush( vLits, Lit );
+
+            RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+            assert( RetValue == 1 );
+            Vec_IntWriteEntry( vLitsA, i, Abc_Var2Lit( iActVar + i, 0 )  );
+        }
+        sat_solver_compress( pSat );
+
+        // solve 
+        RetValue = sat_solver_solve( pSat, Vec_IntArray(vLitsA), Vec_IntArray(vLitsA) + Vec_IntSize(vLitsA), nConfLimit, 0, 0, 0 );
+        Vec_IntFree( vLitsA );
+
+        if ( RetValue == l_Undef )
+            return -1;
+    }
+
+    assert( RetValue != l_Undef );
+    if ( RetValue == l_False ) // UNSAT
+    {
+        int ncorelits, *pcorelits;
+        Vec_Ptr_t * vTemp = NULL;
+        Vec_Bit_t * vMark = NULL;
+
+        ncorelits = sat_solver_final(pSat, &pcorelits);
+        Abc_Print( 1, "UNSAT at the last frame. nCores = %d (out of %d).", ncorelits, Vec_PtrSize( vClauses ) );
+        Abc_PrintTime( 1, "    Time", Abc_Clock() - clk );
+
+        vTemp = Vec_PtrDup( vClauses );
+        vMark = Vec_BitStart( Vec_PtrSize( vClauses) );
+        Vec_PtrClear( vClauses );
+        for ( i = 0; i < ncorelits; ++i )
+        {
+            //Abc_Print( 1, "Core[%d] = lit(%d) = var(%d) = %d-th set\n", i, pcorelits[i], Abc_Lit2Var(pcorelits[i]), Abc_Lit2Var(pcorelits[i]) - iActVar );
+            Vec_BitWriteEntry( vMark, Abc_Lit2Var( pcorelits[i] ) - iActVar, 1 );
+        }
+        
+        Vec_PtrForEachEntry( Pdr_Set_t *, vTemp, pCla, i )
+        {
+            if ( Vec_BitEntry( vMark, i ) )
+            { 
+                Vec_PtrPush( vClauses, pCla );
+                continue;
+            }
+            Pdr_SetDeref( pCla );
+        }
+
+        Vec_PtrFree( vTemp );
+        Vec_BitFree( vMark );
+        RetValue = 1;
+    }
+    else // SAT
+    {
+        Abc_Print( 1, "SAT at the last frame." );
+        Abc_PrintTime( 1, "    Time", Abc_Clock() - clk );
+        RetValue = 0;
+    }
+
+    return RetValue;
+}
+
+int IPdr_ManReduceClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses )
+{
+    int iFrame, RetValue = -1;
+    Vec_Ptr_t * vLast = NULL;
+
+    Pdr_ManCreateSolver( p, (iFrame = 0) );
+    Pdr_ManCreateSolver( p, (iFrame = 1) );
+
+    p->nFrames = iFrame;
+    p->iUseFrame = Abc_MaxInt(iFrame, 1);
+
+    vLast = Vec_VecEntry( vClauses, Vec_VecSize( vClauses ) - 1 );
+    RetValue = IPdr_ManCheckCubeReduce( p, vLast, NULL, p->pPars->nConfLimit );
+    return RetValue;
+}
 
 /**Function*************************************************************
 

src/sat/bsat/module.make

@@ -7,6 +7,7 @@ SRC +=  src/sat/bsat/satMem.c \
     src/sat/bsat/satSolver.c \
     src/sat/bsat/satSolver2.c \
     src/sat/bsat/satSolver2i.c \
+    src/sat/bsat/satSolver3.c \
     src/sat/bsat/satStore.c \
     src/sat/bsat/satTrace.c \
     src/sat/bsat/satTruth.c \