From 91a0a0fc3b5dfd5aa71122106dbdacf6268e51fb Mon Sep 17 00:00:00 2001
From: Yen-Sheng Ho <ysho@berkeley.edu>
Date: Sat, 18 Feb 2017 10:28:16 -0800
Subject: copied pdr_mansolve

---
 src/proof/pdr/pdrIncr.c | 41 ++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 40 insertions(+), 1 deletion(-)

(limited to 'src/proof/pdr/pdrIncr.c')

diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c
index a2329870..2276384c 100644
--- a/src/proof/pdr/pdrIncr.c
+++ b/src/proof/pdr/pdrIncr.c
@@ -27,6 +27,7 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -45,7 +46,45 @@ ABC_NAMESPACE_IMPL_START
 ***********************************************************************/
 int IPdr_ManSolve( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
 {
-    return 0;
+    int RetValue = -1;
+    abctime clk = Abc_Clock();
+    Aig_Man_t * pMan;
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+
+    RetValue = Pdr_ManSolve( pMan, pPars );
+ 
+    if ( RetValue == 1 )
+        Abc_Print( 1, "Property proved.  " );
+    else 
+    {
+        if ( RetValue == 0 )
+        {
+            if ( pMan->pSeqModel == NULL )
+                Abc_Print( 1, "Counter-example is not available.\n" );
+            else
+            {
+                Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame );
+                if ( !Saig_ManVerifyCex( pMan, pMan->pSeqModel ) )
+                    Abc_Print( 1, "Counter-example verification has FAILED.\n" );
+            }
+        }
+        else if ( RetValue == -1 )
+            Abc_Print( 1, "Property UNDECIDED.  " );
+        else
+            assert( 0 );
+    }
+    ABC_PRT( "Time", Abc_Clock() - clk );
+
+
+    ABC_FREE( pNtk->pSeqModel );
+    pNtk->pSeqModel = pMan->pSeqModel;
+    pMan->pSeqModel = NULL;
+    if ( pNtk->vSeqModelVec )
+        Vec_PtrFreeFree( pNtk->vSeqModelVec );
+    pNtk->vSeqModelVec = pMan->vSeqModelVec;
+    pMan->vSeqModelVec = NULL;
+    Aig_ManStop( pMan );
+    return RetValue;
 }
 
 ////////////////////////////////////////////////////////////////////////
-- 
cgit v1.2.3