initial commit of public abc

12 files changed, 131 insertions, 28 deletions

diff --git a/src/aig/int/int.h b/src/aig/int/int.h
index 1487b9bf..907691ed 100644
--- a/src/aig/int/int.h
+++ b/src/aig/int/int.h
@@ -21,6 +21,7 @@
 #ifndef __INT_H__
 #define __INT_H__
 
+
 /* 
     The interpolation algorithm implemented here was introduced in the paper:
     K. L. McMillan. Interpolation and SAT-based model checking. CAV’03, pp. 1-13.
@@ -34,9 +35,10 @@
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef __cplusplus
-extern "C" {
-#endif
+
+
+ABC_NAMESPACE_HEADER_START
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
@@ -48,6 +50,7 @@ struct Inter_ManParams_t_
 {
     int  nBTLimit;      // limit on the number of conflicts
     int  nFramesMax;    // the max number timeframes to unroll
+    int  nSecLimit;     // time limit in seconds
     int  nFramesK;      // the number of timeframes to use in induction
     int  fRewrite;      // use additional rewriting to simplify timeframes
     int  fTransLoop;    // add transition into the init state under new PI var
@@ -58,7 +61,9 @@ struct Inter_ManParams_t_
     int  fUseBias;      // bias decisions to global variables
     int  fUseBackward;  // perform backward interpolation
     int  fUseSeparate;  // solve each output separately
+    int  fDropSatOuts;  // replace by 1 the solved outputs
     int  fVerbose;      // print verbose statistics
+    int  iFrameMax;     // the time frame reached
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -74,9 +79,11 @@ extern void       Inter_ManSetDefaultParams( Inter_ManParams_t * p );
 extern int        Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * piFrame );
 
 
-#ifdef __cplusplus
-}
-#endif
+
+
+ABC_NAMESPACE_HEADER_END
+
+
 
 #endif
 
diff --git a/src/aig/int/intContain.c b/src/aig/int/intContain.c
index 3c16629f..4cc8577e 100644
--- a/src/aig/int/intContain.c
+++ b/src/aig/int/intContain.c
@@ -21,6 +21,8 @@
 #include "intInt.h"
 #include "fra.h"
 
+ABC_NAMESPACE_IMPL_START
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -219,7 +221,7 @@ int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter,
 
     // convert to CNF
     pCnf = Cnf_Derive( pFrames, 0 ); 
-    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
 //    Cnf_DataFree( pCnf );
 //    Aig_ManStop( pFrames );
 
@@ -241,9 +243,13 @@ int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter,
     sat_solver_delete( pSat );
     return status == l_False;
 }
+ABC_NAMESPACE_IMPL_END
 
 #include "fra.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 /**Function*************************************************************
 
   Synopsis    [Check if cex satisfies uniqueness constraints.]
@@ -326,3 +332,5 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
index d1f89c07..c0df48fb 100644
--- a/src/aig/int/intCore.c
+++ b/src/aig/int/intCore.c
@@ -20,6 +20,9 @@
 
 #include "intInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -44,6 +47,7 @@ void Inter_ManSetDefaultParams( Inter_ManParams_t * p )
     memset( p, 0, sizeof(Inter_ManParams_t) );
     p->nBTLimit     = 10000; // limit on the number of conflicts
     p->nFramesMax   = 40;    // the max number timeframes to unroll
+    p->nSecLimit    = 0;     // time limit in seconds
     p->nFramesK     = 1;     // the number of timeframes to use in induction
     p->fRewrite     = 0;     // use additional rewriting to simplify timeframes
     p->fTransLoop   = 1;     // add transition into the init state under new PI var
@@ -54,7 +58,9 @@ void Inter_ManSetDefaultParams( Inter_ManParams_t * p )
     p->fUseBias     = 0;     // bias decisions to global variables
     p->fUseBackward = 0;     // perform backward interpolation
     p->fUseSeparate = 0;     // solve each output separately
+    p->fDropSatOuts = 0;     // replace by 1 the solved outputs
     p->fVerbose     = 0;     // print verbose statistics
+    p->iFrameMax    =-1;
 }
 
 /**Function*************************************************************
@@ -77,7 +83,9 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars,
     // sanity checks
     assert( Saig_ManRegNum(pAig) > 0 );
     assert( Saig_ManPiNum(pAig) > 0 );
-    assert( Saig_ManPoNum(pAig) == 1 );
+    assert( Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) == 1 );
+    if ( pPars->fVerbose && Saig_ManConstrNum(pAig) )
+        printf( "Performing interpolation with %d constraints...\n", Saig_ManConstrNum(pAig) );
 /*
     if ( Inter_ManCheckInitialState(pAig) )
     {
@@ -179,6 +187,8 @@ p->timeCnf += clock() - clk;
                     i+1, i + 1 + p->nFrames, Aig_ManNodeNum(p->pInter), Aig_ManLevelNum(p->pInter), p->nConfCur );
                 ABC_PRT( "Time", clock() - clk );
             }
+            // remember the number of timeframes completed
+            pPars->iFrameMax = i + 1 + p->nFrames;
             if ( RetValue == 0 ) // found a (spurious?) counter-example
             {
                 if ( i == 0 ) // real counterexample
@@ -187,7 +197,7 @@ p->timeCnf += clock() - clk;
                         printf( "Found a real counterexample in frame %d.\n", p->nFrames );
                     p->timeTotal = clock() - clkTotal;
                     *piFrame = p->nFrames;
-                    pAig->pSeqModel = Inter_ManGetCounterExample( pAig, p->nFrames+1, pPars->fVerbose );
+                    pAig->pSeqModel = (Abc_Cex_t *)Inter_ManGetCounterExample( pAig, p->nFrames+1, pPars->fVerbose );
                     Inter_ManStop( p );
                     return 0;
                 }
@@ -211,6 +221,7 @@ clk = clock();
             if ( p->pInterNew )
             {
                 p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 );
+//                p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 0, 0 );
                 Aig_ManStop( pAigTemp );
             }
 p->timeRwr += clock() - clk;
@@ -251,6 +262,13 @@ p->timeEqu += clock() - clk;
                 Inter_ManStop( p );
                 return 1;
             }
+            if ( pPars->nSecLimit && ((float)pPars->nSecLimit <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
+            {
+                printf( "Reached timeout (%d seconds).\n",  pPars->nSecLimit );
+                p->timeTotal = clock() - clkTotal;
+                Inter_ManStop( p );
+                return -1;
+            }
             // save interpolant and convert it into CNF
             if ( pPars->fTransLoop )
             {
@@ -286,3 +304,5 @@ p->timeCnf += clock() - clk;
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/int/intCtrex.c b/src/aig/int/intCtrex.c
index ddb0bce6..28b1e293 100644
--- a/src/aig/int/intCtrex.c
+++ b/src/aig/int/intCtrex.c
@@ -21,6 +21,9 @@
 #include "intInt.h"
 #include "ssw.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -92,7 +95,7 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
 void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
 {
     int nConfLimit = 1000000;
-    Ssw_Cex_t * pCtrex = NULL;
+    Abc_Cex_t * pCtrex = NULL;
     Aig_Man_t * pFrames;
     sat_solver * pSat;
     Cnf_Dat_t * pCnf;
@@ -107,7 +110,7 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
     vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
     Aig_ManStop( pFrames );
     // convert into SAT solver
-    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     Cnf_DataFree( pCnf );
     if ( pSat == NULL )
     {
@@ -160,3 +163,5 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/int/intDup.c b/src/aig/int/intDup.c
index 4c5b7ab6..800375a9 100644
--- a/src/aig/int/intDup.c
+++ b/src/aig/int/intDup.c
@@ -20,6 +20,9 @@
 
 #include "intInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -83,12 +86,21 @@ Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p )
     Aig_ManForEachPi( p, pObj, i )
         pObj->pData = Aig_ObjCreatePi( pNew );
     // set registers
-    pNew->nRegs    = p->nRegs;
     pNew->nTruePis = p->nTruePis;
-    pNew->nTruePos = 0;
+    pNew->nTruePos = Saig_ManConstrNum(p);
+    pNew->nRegs    = p->nRegs;
     // duplicate internal nodes
     Aig_ManForEachNode( p, pObj, i )
         pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+
+    // create constraint outputs
+    Saig_ManForEachPo( p, pObj, i )
+    {
+        if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
+            continue;
+        Aig_ObjCreatePo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
+    }
+
     // create register inputs with MUXes
     Saig_ManForEachLi( p, pObj, i )
         Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
@@ -130,10 +142,19 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
     // set registers
     pNew->nRegs    = fAddFirstPo? 0 : p->nRegs;
     pNew->nTruePis = fAddFirstPo? Aig_ManPiNum(p) + 1 : p->nTruePis + 1;
-    pNew->nTruePos = fAddFirstPo;
+    pNew->nTruePos = fAddFirstPo + Saig_ManConstrNum(p);
     // duplicate internal nodes
     Aig_ManForEachNode( p, pObj, i )
         pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+
+    // create constraint outputs
+    Saig_ManForEachPo( p, pObj, i )
+    {
+        if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
+            continue;
+        Aig_ObjCreatePo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
+    }
+
     // add the PO
     if ( fAddFirstPo )
     {
@@ -145,7 +166,7 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
         // create register inputs with MUXes
         Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
         {
-            pObj = Aig_Mux( pNew, pCtrl, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
+            pObj = Aig_Mux( pNew, pCtrl, (Aig_Obj_t *)pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
     //        pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) );
             Aig_ObjCreatePo( pNew, pObj );
         }
@@ -159,3 +180,5 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/int/intFrames.c b/src/aig/int/intFrames.c
index 809cb06b..0fbab6cb 100644
--- a/src/aig/int/intFrames.c
+++ b/src/aig/int/intFrames.c
@@ -20,6 +20,9 @@
 
 #include "intInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -47,7 +50,7 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
     int i, f;
     assert( Saig_ManRegNum(pAig) > 0 );
-    assert( Saig_ManPoNum(pAig) == 1 );
+    assert( Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) == 1 );
     pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
     // map the constant node
     Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
@@ -71,6 +74,13 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
         // add internal nodes of this frame
         Aig_ManForEachNode( pAig, pObj, i )
             pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        // add outputs for constraints
+        Saig_ManForEachPo( pAig, pObj, i )
+        {
+            if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) )
+                continue;
+            Aig_ObjCreatePo( pFrames, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
+        }
         if ( f == nFrames - 1 )
             break;
         // save register inputs
@@ -101,3 +111,5 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h
index 2d571f09..72079a49 100644
--- a/src/aig/int/intInt.h
+++ b/src/aig/int/intInt.h
@@ -21,6 +21,7 @@
 #ifndef __INT_INT_H__
 #define __INT_INT_H__
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -35,9 +36,10 @@
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#ifdef __cplusplus
-extern "C" {
-#endif
+
+
+ABC_NAMESPACE_HEADER_START
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
@@ -118,9 +120,11 @@ extern int           Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudl
 extern int           Inter_ManCheckInitialState( Aig_Man_t * p );
 extern int           Inter_ManCheckAllStates( Aig_Man_t * p );
 
-#ifdef __cplusplus
-}
-#endif
+
+
+ABC_NAMESPACE_HEADER_END
+
+
 
 #endif
 
diff --git a/src/aig/int/intInter.c b/src/aig/int/intInter.c
index 592eedcf..ef32294b 100644
--- a/src/aig/int/intInter.c
+++ b/src/aig/int/intInter.c
@@ -20,6 +20,9 @@
 
 #include "intInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -138,3 +141,5 @@ void Inter_ManVerifyInterpolant2( Intb_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/int/intM114.c b/src/aig/int/intM114.c
index 359d5458..c1718eae 100644
--- a/src/aig/int/intM114.c
+++ b/src/aig/int/intM114.c
@@ -20,6 +20,9 @@
 
 #include "intInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -296,11 +299,11 @@ clk = clock();
 */
 
     pManInterA = Inta_ManAlloc();
-    p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
+    p->pInterNew = (Aig_Man_t *)Inta_ManInterpolate( pManInterA, (Sto_Man_t *)pSatCnf, p->vVarsAB, 0 );
     Inta_ManFree( pManInterA );
 
 p->timeInt += clock() - clk;
-    Sto_ManFree( pSatCnf );
+    Sto_ManFree( (Sto_Man_t *)pSatCnf );
     return RetValue;
 }
 
@@ -309,3 +312,5 @@ p->timeInt += clock() - clk;
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/int/intM114p.c b/src/aig/int/intM114p.c
index 6818fdce..0ad0552f 100644
--- a/src/aig/int/intM114p.c
+++ b/src/aig/int/intM114p.c
@@ -18,11 +18,13 @@
 
 ***********************************************************************/
 
-#ifdef ABC_USE_LIBRARIES
-
 #include "intInt.h"
 #include "m114p.h"
 
+#ifdef ABC_USE_LIBRARIES
+
+ABC_NAMESPACE_IMPL_START
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -433,6 +435,8 @@ p->timeInt += clock() - clk;
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
+ABC_NAMESPACE_IMPL_END
+
 #endif
 
 
diff --git a/src/aig/int/intMan.c b/src/aig/int/intMan.c
index 14a79f65..2faef198 100644
--- a/src/aig/int/intMan.c
+++ b/src/aig/int/intMan.c
@@ -20,6 +20,9 @@
 
 #include "intInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -126,3 +129,5 @@ void Inter_ManStop( Inter_Man_t * p )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/int/intUtil.c b/src/aig/int/intUtil.c
index c0dc9ddb..0d8beda5 100644
--- a/src/aig/int/intUtil.c
+++ b/src/aig/int/intUtil.c
@@ -20,6 +20,9 @@
 
 #include "intInt.h"
 
+ABC_NAMESPACE_IMPL_START
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -47,7 +50,7 @@ int Inter_ManCheckInitialState( Aig_Man_t * p )
     int status;
     int clk = clock();
     pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); 
-    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 1 );
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 1 );
     Cnf_DataFree( pCnf );
     if ( pSat == NULL )
         return 0;
@@ -75,7 +78,7 @@ int Inter_ManCheckAllStates( Aig_Man_t * p )
     int status;
     int clk = clock();
     pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); 
-    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
     Cnf_DataFree( pCnf );
     if ( pSat == NULL )
         return 1;
@@ -90,3 +93,5 @@ int Inter_ManCheckAllStates( Aig_Man_t * p )
 ////////////////////////////////////////////////////////////////////////
 
 
+ABC_NAMESPACE_IMPL_END
+