Adding CEC command &splitprove.

4 files changed, 120 insertions, 53 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 870ac85c..bdb07c4c 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -156,6 +156,7 @@ struct Gia_Man_t_
     Vec_Int_t *    vUserFfIds;    // numbers assigned to FFs by the user
     Vec_Int_t *    vCiNumsOrig;   // original CI names
     Vec_Int_t *    vCoNumsOrig;   // original CO names
+    Vec_Int_t *    vCofVars;      // cofactoring variables
     Vec_Vec_t *    vClockDoms;    // clock domains
     Vec_Flt_t *    vTiming;       // arrival/required/slack
     void *         pManTime;      // the timing manager
@@ -1013,7 +1014,7 @@ extern Gia_Man_t *         Gia_ManDupFlopClass( Gia_Man_t * p, int iClass );
 extern Gia_Man_t *         Gia_ManDupMarked( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupTimes( Gia_Man_t * p, int nTimes );  
 extern Gia_Man_t *         Gia_ManDupDfs( Gia_Man_t * p );  
-extern Gia_Man_t *         Gia_ManDupDfsRehash( Gia_Man_t * p, int nSteps, int Value );  
+extern Gia_Man_t *         Gia_ManDupCofactor( Gia_Man_t * p, int iVar, int Value );  
 extern Gia_Man_t *         Gia_ManDupDfsSkip( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern Gia_Man_t *         Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 2d294433..0939c091 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1201,30 +1201,33 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManDupDfsRehash_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+void Gia_ManDupCofactor_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
 {
     if ( ~pObj->Value )
         return;
     assert( Gia_ObjIsAnd(pObj) );
-    Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin0(pObj) );
-    Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin1(pObj) );
     pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
 }
-Gia_Man_t * Gia_ManDupDfsRehash( Gia_Man_t * p, int nSteps, int Value )
+Gia_Man_t * Gia_ManDupCofactor( Gia_Man_t * p, int iVar, int Value )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
     int i;
+    assert( iVar >= 0 && iVar < Gia_ManPiNum(p) );
+    assert( Value == 0 || Value == 1 );
     pNew = Gia_ManStart( Gia_ManObjNum(p) );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
-        pObj->Value = i < nSteps ? Value : Gia_ManAppendCi(pNew);
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManPi( p, iVar )->Value = Value; // modification!
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachCo( p, pObj, i )
-        Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin0(pObj) );
+        Gia_ManDupCofactor_rec( pNew, p, Gia_ObjFanin0(pObj) );
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 710886ae..6d5a8e92 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -92,6 +92,7 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_WrdFreeP( &p->vSimsPi );
     Vec_FltFreeP( &p->vTiming );
     Vec_VecFreeP( &p->vClockDoms );
+    Vec_IntFreeP( &p->vCofVars );
     Vec_IntFreeP( &p->vLutConfigs );
     Vec_IntFreeP( &p->vUserPiIds );
     Vec_IntFreeP( &p->vUserPoIds );
diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c
index 6046df37..352b94e4 100644
--- a/src/proof/cec/cecSplit.c
+++ b/src/proof/cec/cecSplit.c
@@ -18,11 +18,13 @@
 
 ***********************************************************************/
 
+#include <math.h>
 #include "aig/gia/gia.h"
 #include "aig/gia/giaAig.h"
-#include "bdd/cudd/cuddInt.h"
+//#include "bdd/cudd/cuddInt.h"
 #include "sat/cnf/cnf.h"
-#include "sat/bsat/satStore.h"
+#include "sat/bsat/satSolver.h"
+#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -35,6 +37,8 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#if 0 // BDD code
+
 /**Function*************************************************************
 
   Synopsis    [Permute primary inputs.]
@@ -109,6 +113,8 @@ void Gia_ManBuildBddTest( Gia_Man_t * p )
     Gia_ManDerefBdd( dd, vNodes );
 }
 
+#endif // BDD code
+
 /**Function*************************************************************
 
   Synopsis    [Permute primary inputs.]
@@ -120,10 +126,9 @@ void Gia_ManBuildBddTest( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p )
+int * Gia_PermuteSpecialOrder( Gia_Man_t * p )
 {
     Vec_Int_t * vPerm;
-    Gia_Man_t * pNew;
     Gia_Obj_t * pObj;
     int i, * pOrder;
     Gia_ManCreateRefs( p );
@@ -132,6 +137,13 @@ Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p )
         Vec_IntPush( vPerm, Gia_ObjRefNum(p, pObj) );
     pOrder = Abc_QuickSortCost( Vec_IntArray(vPerm), Vec_IntSize(vPerm), 1 );
     Vec_IntFree( vPerm );
+    return pOrder;
+}
+Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Vec_Int_t * vPerm;
+    int * pOrder = Gia_PermuteSpecialOrder( p );
     vPerm = Vec_IntAllocArray( pOrder, Gia_ManPiNum(p) );
     pNew = Gia_ManDupPerm( p, vPerm );
     Vec_IntFree( vPerm );
@@ -207,29 +219,13 @@ static inline sat_solver * Cec_GiaDeriveSolver( Gia_Man_t * p, int nTimeOut )
     Cnf_DataFree( pCnf );
     return pSat;
 }
-static inline int Cnf_GiaSolveOne( Gia_Man_t * p, int nTimeOut, int nSize, int fVerbose )
+static inline int Cnf_GiaSolveOne( Gia_Man_t * p, int nTimeOut, int fVerbose, int * pnVars, int * pnConfs )
 {
     static int Counter = 0;
-    abctime clk = Abc_Clock();
     sat_solver * pSat = Cec_GiaDeriveSolver( p, nTimeOut );
     int status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-    if ( fVerbose )
-    {
-        printf( "Iter%6d : ",       Counter++ );
-        printf( "Size =%7d  ",      nSize );
-        printf( "Input = %3d  ",    Gia_ManPiNum(p) );
-        printf( "Var =%10d  ",      sat_solver_nvars(pSat) );
-        printf( "Clause =%10d  ",   sat_solver_nclauses(pSat) );
-        printf( "Conflict =%10d  ", sat_solver_nconflicts(pSat) );
-        if ( status == l_Undef )
-            printf( "UNDECIDED  " );
-        else if ( status == l_False )
-            printf( "UNSAT      " );
-        else
-            printf( "SAT        " );
-        Abc_PrintTime( 1, "Time", Abc_Clock()-clk );
-        //ABC_PRTr( "Time", Abc_Clock()-clk );
-    }
+    *pnVars    = sat_solver_nvars( pSat );
+    *pnConfs   = sat_solver_nconflicts( pSat );
     sat_solver_delete( pSat );
     if ( status == l_Undef )
         return -1;
@@ -253,9 +249,9 @@ static inline int Cnf_GiaSolveOne( Gia_Man_t * p, int nTimeOut, int nSize, int f
     }
 */
 }
-static inline int Cnf_GiaCheckOne( Vec_Ptr_t * vStack, Gia_Man_t * p, int nTimeOut, int nSize, int fVerbose )
+static inline int Cnf_GiaCheckOne( Vec_Ptr_t * vStack, Gia_Man_t * p, int nTimeOut, int fVerbose, int * pnVars, int * pnConfs )
 {
-    int status = Cnf_GiaSolveOne( p, nTimeOut, nSize, fVerbose );
+    int status = Cnf_GiaSolveOne( p, nTimeOut, fVerbose, pnVars, pnConfs );
     if ( status == -1 )
     {
         Vec_PtrPush( vStack, p );
@@ -287,47 +283,111 @@ static inline void Cec_GiaSplitClean( Vec_Ptr_t * vStack )
   SeeAlso     []
 
 ***********************************************************************/
+void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fSatUnsat, double Prog, abctime clk )
+{
+    printf( "%6d : ",            nIter );
+    printf( "Depth =%3d  ",      Depth );
+    printf( "SatVar =%10d  ",    nVars );
+    printf( "SatConf =%7d  ",    nConfs );
+    printf( "%s  ",              fSatUnsat ? "UNSAT    " : "UNDECIDED" );
+    printf( "Progress = %.9f  ", Prog );
+    Abc_PrintTime( 1, "Time", clk );
+    //ABC_PRTr( "Time", Abc_Clock()-clk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose )
 {
-    Gia_Man_t * pNew;
-    Vec_Ptr_t * vStack;
-    Gia_Man_t * pPart0, * pPart1;
+    abctime clk, clkTotal = Abc_Clock();
+    Gia_Man_t * pPart0, * pPart1, * pLast;
     Gia_Obj_t * pObj;
-    int i, RetValue = -1;
+    Vec_Ptr_t * vStack;
+    int * pOrder, RetValue = -1;
+    int nSatVars, nSatConfs, fSatUnsat;
+    int i, nIter, iVar, Depth;
+    double Progress = 0;
+    // create local copy
+    p = Gia_ManDup( p );
     // reorder variables
-    pNew = Gia_PermuteSpecial( p );
-    if ( fVerbose )
+    pOrder = Gia_PermuteSpecialOrder( p );
+    if ( fVerbose ) 
     {
-        Gia_ManCreateRefs( pNew );
-        Gia_ManForEachPi( pNew, pObj, i )
-            printf( "%d ", Gia_ObjRefNum(pNew, pObj) );
+        Gia_ManForEachPi( p, pObj, i )
+            printf( "%d ", Gia_ObjRefNum(p, pObj) );
+        printf( "\n" );
+        Gia_ManForEachPi( p, pObj, i )
+            printf( "%d ", Gia_ObjRefNum(p, Gia_ManPi(p, pOrder[i])) );
         printf( "\n" );
     }
+    // start cofactored variables
+    assert( p->vCofVars == NULL );
+    p->vCofVars = Vec_IntAlloc( 100 );
     // start with the current problem
     vStack = Vec_PtrAlloc( 1000 );
-    if ( !Cnf_GiaCheckOne(vStack, pNew, nTimeOut, Vec_PtrSize(vStack), fVerbose) )
+    clk = Abc_Clock();
+    if ( !Cnf_GiaCheckOne(vStack, p, nTimeOut, fVerbose, &nSatVars, &nSatConfs) )
         RetValue = 0;
     else
     {
-        while ( Vec_PtrSize(vStack) > 0 )
+        if ( fVerbose )
+            Cec_GiaSplitPrint( 0, 0, nSatVars, nSatConfs, 0, 0, Abc_Clock() - clk );
+        for ( nIter = 1; Vec_PtrSize(vStack) > 0; nIter++ )
         {
-            pNew = (Gia_Man_t *)Vec_PtrPop( vStack );
+            // get the last AIG
+            pLast = (Gia_Man_t *)Vec_PtrPop( vStack );
+            // determine cofactoring variable
+            Depth = Vec_IntSize(pLast->vCofVars);
+            iVar = pOrder[Depth];
             // cofactor
-            pPart0 = Gia_ManDupDfsRehash( pNew, 1, 0 );
-            if ( !Cnf_GiaCheckOne(vStack, pPart0, nTimeOut, Vec_PtrSize(vStack), fVerbose) )
+            pPart0 = Gia_ManDupCofactor( pLast, iVar, 0 );
+            // create variable
+            pPart0->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
+            Vec_IntAppend( pPart0->vCofVars, pLast->vCofVars );
+            Vec_IntPush( pPart0->vCofVars, Abc_Var2Lit(iVar, 1) );
+            // check this AIG
+            fSatUnsat = Vec_PtrSize(vStack);
+            clk = Abc_Clock();
+            if ( !Cnf_GiaCheckOne(vStack, pPart0, nTimeOut, fVerbose, &nSatVars, &nSatConfs) )
             {
-                Gia_ManStop( pNew );
+                Gia_ManStop( pLast );
                 RetValue = 0;
                 break;
             }
+            fSatUnsat = (fSatUnsat == Vec_PtrSize(vStack));
+            if ( fSatUnsat )
+                Progress += 1.0 / pow(0.5, Depth + 1);
+            if ( fVerbose ) 
+                Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk );
             // cofactor
-            pPart1 = Gia_ManDupDfsRehash( pNew, 1, 1 );
-            Gia_ManStop( pNew );
-            if ( !Cnf_GiaCheckOne(vStack, pPart1, nTimeOut, Vec_PtrSize(vStack), fVerbose) )
+            pPart1 = Gia_ManDupCofactor( pLast, iVar, 1 );
+            // create variable
+            pPart1->vCofVars = Vec_IntAlloc( Vec_IntSize(pLast->vCofVars) + 1 );
+            Vec_IntAppend( pPart1->vCofVars, pLast->vCofVars );
+            Vec_IntPush( pPart1->vCofVars, Abc_Var2Lit(iVar, 0) );
+            Gia_ManStop( pLast );
+            // check this AIG
+            fSatUnsat = Vec_PtrSize(vStack);
+            clk = Abc_Clock();
+            if ( !Cnf_GiaCheckOne(vStack, pPart1, nTimeOut, fVerbose, &nSatVars, &nSatConfs) )
             {
                 RetValue = 0;
                 break;
             }
+            fSatUnsat = (fSatUnsat == Vec_PtrSize(vStack));
+            if ( fSatUnsat )
+                Progress += 1.0 / (Depth + 1);
+            if ( fVerbose )
+                Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk );
 //            if ( Vec_PtrSize(vStack) > 2 )
 //                break;
         }
@@ -336,12 +396,14 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose )
     }
     Cec_GiaSplitClean( vStack );
     if ( RetValue == 0 )
-        printf( "Problem is SAT\n" );
+        printf( "Problem is SAT  " );
     else if ( RetValue == 1 )
-        printf( "Problem is UNSAT\n" );
+        printf( "Problem is UNSAT  " );
     else if ( RetValue == -1 )
-        printf( "Problem is UNDECIDED\n" );
+        printf( "Problem is UNDECIDED  " );
     else assert( 0 );
+    ABC_FREE( pOrder );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
     return RetValue;
 }