started pdrIncr.c

src/base/abci/abc.c

@@ -26434,6 +26434,7 @@ usage:
 int Abc_CommandIPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars );
+    extern int IPdr_ManSolve( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars );
     Pdr_Par_t Pars, * pPars = &Pars;
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int c;
@@ -26629,6 +26630,7 @@ int Abc_CommandIPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     // run the procedure
+    IPdr_ManSolve( pNtk, pPars );
     pPars->fUseBridge = pAbc->fBridgeMode;
     pAbc->Status  = Abc_NtkDarPdr( pNtk, pPars );
     pAbc->nFrames = pNtk->vSeqModelVec ? -1 : pPars->iFrame;

src/proof/pdr/module.make

@@ -5,4 +5,5 @@ SRC +=    src/proof/pdr/pdrCnf.c \
     src/proof/pdr/pdrSat.c \
     src/proof/pdr/pdrTsim.c \
     src/proof/pdr/pdrTsim2.c \
-    src/proof/pdr/pdrUtil.c 
+    src/proof/pdr/pdrUtil.c \
+    src/proof/pdr/pdrIncr.c

src/proof/pdr/pdrIncr.c

@@ -0,0 +1,56 @@
+/**CFile****************************************************************
+
+  FileName    [pdrIncr.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Property driven reachability.]
+
+  Synopsis    [PDR with incremental solving.]
+
+  Author      [Yen-Sheng Ho, Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Feb. 17, 2017.]
+
+  Revision    [$Id: pdrIncr.c$]
+
+***********************************************************************/
+
+#include "pdrInt.h"
+#include "base/main/main.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IPdr_ManSolve( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
+{
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END