Version abc80315

7 files changed, 91 insertions, 23 deletions

diff --git a/src/aig/aig/aigInter.c b/src/aig/aig/aigInter.c
index d6b724c7..b58b758d 100644
--- a/src/aig/aig/aigInter.c
+++ b/src/aig/aig/aigInter.c
@@ -143,7 +143,7 @@ void Aig_ManInterFast( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose )
+Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation, int fVerbose )
 {
     void * pSatCnf = NULL;
     Inta_Man_t * pManInter; 
@@ -187,9 +187,10 @@ clk = clock();
     sat_solver_store_mark_clauses_a( pSat );
 
     // update the last clause
+    if ( fRelation )
     {
         extern int sat_solver_store_change_last( sat_solver * pSat );
-//        iLast = sat_solver_store_change_last( pSat );
+        iLast = sat_solver_store_change_last( pSat );
     }
 
     // add clauses of B
@@ -207,7 +208,8 @@ clk = clock();
     // add PI clauses
     // collect the common variables
     vVarsAB = Vec_IntAlloc( Aig_ManPiNum(pManOn) );
-//    Vec_IntPush( vVarsAB, iLast );
+    if ( fRelation )
+        Vec_IntPush( vVarsAB, iLast );
 
     Aig_ManForEachPi( pManOn, pObj, i )
     {
diff --git a/src/aig/bdc/bdcCore.c b/src/aig/bdc/bdcCore.c
index 13275377..67b6bcdc 100644
--- a/src/aig/bdc/bdcCore.c
+++ b/src/aig/bdc/bdcCore.c
@@ -44,7 +44,7 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
     Bdc_Man_t * p;
     p = ALLOC( Bdc_Man_t, 1 );
     memset( p, 0, sizeof(Bdc_Man_t) );
-    assert( pPars->nVarsMax > 3 && pPars->nVarsMax < 16 );
+    assert( pPars->nVarsMax > 2 && pPars->nVarsMax < 16 );
     p->pPars = pPars;
     p->nWords = Kit_TruthWordNum( pPars->nVarsMax );
     p->nDivsLimit = 200;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4262cd0d..204525d9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -6809,24 +6809,29 @@ usage:
 int Abc_CommandInter( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes, * pNtk1, * pNtk2;
+    Abc_Ntk_t * pNtk, * pNtk1, * pNtk2, * pNtkRes = NULL;
     char ** pArgvNew;
     int nArgcNew;
     int c, fDelete1, fDelete2;
+    int fRelation;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fVerbose   =  0;
+    fRelation = 0;
+    fVerbose  = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "rvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'r':
+            fRelation ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -6843,10 +6848,19 @@ int Abc_CommandInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     if ( nArgcNew == 0 )
     {
+        Abc_Obj_t * pObj;
+        int i;
         printf( "Deriving new circuit structure for the current network.\n" );
-        Abc_ObjXorFaninC( Abc_NtkPo(pNtk2,0), 0 );
+        Abc_NtkForEachPo( pNtk2, pObj, i )
+            Abc_ObjXorFaninC( pObj, 0 );
+    }
+    if ( fRelation && Abc_NtkCoNum(pNtk1) != 1 )
+    {
+        printf( "Computation of interplants as a relation only works for single-output functions.\n" );
+        printf( "Use command \"cone\" to extract one output cone from the multi-output network.\n" );
     }
-    pNtkRes = Abc_NtkInter( pNtk1, pNtk2, fVerbose );
+    else
+        pNtkRes = Abc_NtkInter( pNtk1, pNtk2, fRelation, fVerbose );
     if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
     if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
 
@@ -6859,10 +6873,26 @@ int Abc_CommandInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: inter [-vh] <fileOnSet> <fileOffSet>\n" );
-    fprintf( pErr, "\t         derives interpolant of two networks (onset and offset)\n" );
+    fprintf( pErr, "usage: inter [-rvh] <onset.blif> <offset.blif>\n" );
+    fprintf( pErr, "\t         derives interpolant of two networks representing onset and offset;\n" );
+    fprintf( pErr, "\t-r     : toggle computing interpolant as a relation [default = %s]\n", fRelation? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\t         \n" );
+    fprintf( pErr, "\t         Comments:\n" );
+    fprintf( pErr, "\t         \n" );
+    fprintf( pErr, "\t         The networks given on the command line should have the same CIs/COs.\n" );
+    fprintf( pErr, "\t         If only one network is given on the command line, this network\n" );
+    fprintf( pErr, "\t         is assumed to be the offset, while the current network is the onset.\n" );
+    fprintf( pErr, "\t         If no network is given on the command line, the current network is\n" );
+    fprintf( pErr, "\t         assumed to be the onset and its complement is taken to be the offset.\n" );
+    fprintf( pErr, "\t         The resulting interpolant is stored as the current network.\n" );
+    fprintf( pErr, "\t         To verify that the interpolant agrees with the onset and the offset,\n" );
+    fprintf( pErr, "\t         save it in file \"inter.blif\" and run the following:\n" );
+    fprintf( pErr, "\t         (a) \"miter -i <onset.blif> <inter.blif>; iprove\"\n" );
+    fprintf( pErr, "\t         (b) \"miter -i <inter.blif> <offset_inv.blif>; iprove\"\n" );
+    fprintf( pErr, "\t         where <offset_inv.blif> is the network derived by complementing the\n" );
+    fprintf( pErr, "\t         outputs of <offset.blif>: \"r <onset.blif>; st -i; w <offset_inv.blif>\"\n" ); 
     return 1;
 }
 
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index adf1f6e6..367ba727 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1530,14 +1530,14 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
+Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation, int fVerbose )
 {
-    extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose );
+    extern Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fRelation, int fVerbose );
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pManOn, * pManOff, * pManAig;
     if ( Abc_NtkCoNum(pNtkOn) != 1 || Abc_NtkCoNum(pNtkOff) != 1 )
     {
-        printf( "Currently works only for single output networks.\n" );
+        printf( "Currently works only for single-output networks.\n" );
         return NULL;
     }
     if ( Abc_NtkCiNum(pNtkOn) != Abc_NtkCiNum(pNtkOff) )
@@ -1553,7 +1553,7 @@ Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbo
     if ( pManOff == NULL )
         return NULL;
     // derive the interpolant
-    pManAig = Aig_ManInter( pManOn, pManOff, fVerbose );
+    pManAig = Aig_ManInter( pManOn, pManOff, fRelation, fVerbose );
     if ( pManAig == NULL )
     {
         printf( "Interpolant computation failed.\n" );
@@ -1561,8 +1561,15 @@ Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbo
     }
     Aig_ManStop( pManOn );
     Aig_ManStop( pManOff );
+    // for the relation, add an extra input
+    if ( fRelation )
+    {
+        Abc_Obj_t * pObj;
+        pObj = Abc_NtkCreatePi( pNtkOff );
+        Abc_ObjAssignName( pObj, "New", NULL );
+    }
     // create logic network
-    pNtkAig = Abc_NtkFromDar( pNtkOn, pManAig );
+    pNtkAig = Abc_NtkFromDar( pNtkOff, pManAig );
     Aig_ManStop( pManAig );
     return pNtkAig;
 }
@@ -1609,7 +1616,7 @@ int timeInt;
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
+Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fRelation, int fVerbose )
 {
     Abc_Ntk_t * pNtkOn1, * pNtkOff1, * pNtkInter1, * pNtkInter;
     Abc_Obj_t * pObj;
@@ -1623,7 +1630,7 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose
 //    Abc_NtkInterFast( pNtkOn, pNtkOff, fVerbose );
     // consider the case of one output
     if ( Abc_NtkCoNum(pNtkOn) == 1 )
-        return Abc_NtkInterOne( pNtkOn, pNtkOff, fVerbose );
+        return Abc_NtkInterOne( pNtkOn, pNtkOff, fRelation, fVerbose );
     // start the new newtork
     pNtkInter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     pNtkInter->pName = Extra_UtilStrsav(pNtkOn->pName);
@@ -1652,7 +1659,7 @@ timeInt = 0;
             Abc_ObjXorFaninC( Abc_NtkPo(pNtkInter1, 0), 0 );
         }
         else
-            pNtkInter1 = Abc_NtkInterOne( pNtkOn1, pNtkOff1, fVerbose );
+            pNtkInter1 = Abc_NtkInterOne( pNtkOn1, pNtkOff1, 0, fVerbose );
         if ( pNtkInter1 )
         {
             Abc_NtkAppend( pNtkInter, pNtkInter1, 1 );
diff --git a/src/base/abci/abcDelay.c b/src/base/abci/abcDelay.c
index 553bb2fc..847f1c75 100644
--- a/src/base/abci/abcDelay.c
+++ b/src/base/abci/abcDelay.c
@@ -566,7 +566,7 @@ Abc_Ntk_t * Abc_NtkSpeedup( Abc_Ntk_t * pNtk, int fUseLutLib, int Percentage, in
         if ( !fVeryVerbose && nTimeCris == 0 )
             continue;
         Counter++;
-        // count the total number of timingn critical second-generation nodes
+        // count the total number of timing critical second-generation nodes
         Vec_PtrClear( vTimeCries );
         if ( nTimeCris )
         {
@@ -602,6 +602,35 @@ Abc_Ntk_t * Abc_NtkSpeedup( Abc_Ntk_t * pNtk, int fUseLutLib, int Percentage, in
         // add the node to choices
         if ( Vec_PtrSize(vTimeCries) == 0 || Vec_PtrSize(vTimeCries) > Degree )
             continue;
+        // order the fanins in the increasing order of criticalily
+        if ( Vec_PtrSize(vTimeCries) > 1 )
+        {
+            pFanin = Vec_PtrEntry( vTimeCries, 0 );
+            pFanin2 = Vec_PtrEntry( vTimeCries, 1 );
+            if ( Abc_ObjSlack(pFanin) < Abc_ObjSlack(pFanin2) )
+            {
+                Vec_PtrWriteEntry( vTimeCries, 0, pFanin2 );
+                Vec_PtrWriteEntry( vTimeCries, 1, pFanin );
+            }
+        }
+        if ( Vec_PtrSize(vTimeCries) > 2 )
+        {
+            pFanin = Vec_PtrEntry( vTimeCries, 1 );
+            pFanin2 = Vec_PtrEntry( vTimeCries, 2 );
+            if ( Abc_ObjSlack(pFanin) < Abc_ObjSlack(pFanin2) )
+            {
+                Vec_PtrWriteEntry( vTimeCries, 1, pFanin2 );
+                Vec_PtrWriteEntry( vTimeCries, 2, pFanin );
+            }
+            pFanin = Vec_PtrEntry( vTimeCries, 0 );
+            pFanin2 = Vec_PtrEntry( vTimeCries, 1 );
+            if ( Abc_ObjSlack(pFanin) < Abc_ObjSlack(pFanin2) )
+            {
+                Vec_PtrWriteEntry( vTimeCries, 0, pFanin2 );
+                Vec_PtrWriteEntry( vTimeCries, 1, pFanin );
+            }
+        }
+        // add choice
         Abc_NtkSpeedupNode( pNtk, pNtkNew, pNode, vTimeFanins, vTimeCries );
     }
     Vec_PtrFree( vTimeCries );
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 551feb0b..e1ff3b08 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -825,7 +825,7 @@ int IoCommandReadTruth( Abc_Frame_t * pAbc, int argc, char ** argv )
         pSopCover = Abc_SopFromTruthHex(argv[globalUtilOptind]);
     else
         pSopCover = Abc_SopFromTruthBin(argv[globalUtilOptind]);
-    if ( pSopCover == NULL )
+    if ( pSopCover == NULL || pSopCover[0] == 0 )
     {
         fprintf( pAbc->Err, "Reading truth table has failed.\n" );
         return 1;
diff --git a/src/sat/bsat/satInterA.c b/src/sat/bsat/satInterA.c
index 513a9044..62d0f43c 100644
--- a/src/sat/bsat/satInterA.c
+++ b/src/sat/bsat/satInterA.c
@@ -947,7 +947,7 @@ void * Inta_ManInterpolate( Inta_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, in
 
     if ( fVerbose )
     {
-        PRT( "Interpo", clock() - clkTotal );
+//        PRT( "Interpo", clock() - clkTotal );
     printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f Mb\n", 
         p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
         1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots),