Adding CEC command &splitprove.

1 files changed, 42 insertions, 9 deletions

diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c
index 6dedbe0f..7b33efc6 100644
--- a/src/proof/cec/cecSplit.c
+++ b/src/proof/cec/cecSplit.c
@@ -148,7 +148,7 @@ void Cec_GiaSplitExplore( Gia_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Permute primary inputs.]
+  Synopsis    [Find cofactoring variable.]
 
   Description []
                
@@ -195,6 +195,41 @@ Gia_Man_t * Gia_PermuteSpecial( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Find cofactoring variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_SplitCofVar2( Gia_Man_t * p )
+{
+    Gia_Man_t * pPart;
+    int * pOrder = Gia_PermuteSpecialOrder( p );
+    int Cost0, Cost1, CostBest = ABC_INFINITY;
+    int i, iBest = -1, LookAhead = 10;
+    for ( i = 0; i < LookAhead; i++ )
+    {
+        pPart = Gia_ManDupCofactor( p, pOrder[i], 0 );
+        Cost0 = Gia_ManAndNum(pPart);
+        Gia_ManStop( pPart );
+
+        pPart = Gia_ManDupCofactor( p, pOrder[i], 1 );
+        Cost1 = Gia_ManAndNum(pPart);
+        Gia_ManStop( pPart );
+
+        if ( CostBest > Cost0 + Cost1 )
+            CostBest = Cost0 + Cost1, iBest = pOrder[i];
+    }
+    ABC_FREE( pOrder );
+    assert( iBest >= 0 );
+    return iBest;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -295,10 +330,10 @@ void Cec_GiaSplitPrint( int nIter, int Depth, int nVars, int nConfs, int fSatUns
 {
     printf( "%6d : ",            nIter );
     printf( "Depth =%3d  ",      Depth );
-    printf( "SatVar =%10d  ",    nVars );
+    printf( "SatVar =%7d  ",     nVars );
     printf( "SatConf =%7d  ",    nConfs );
-    printf( "%s  ",              fSatUnsat ? "UNSAT    " : "UNDECIDED" );
-    printf( "Progress = %.10f  ", Prog );
+    printf( "%s   ",             fSatUnsat ? "UNSAT    " : "UNDECIDED" );
+    printf( "Progress = %.10f   ", Prog );
     Abc_PrintTime( 1, "Time", clk );
     //ABC_PRTr( "Time", Abc_Clock()-clk );
 }
@@ -351,8 +386,8 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose )
             // get the last AIG
             pLast = (Gia_Man_t *)Vec_PtrPop( vStack );
             // determine cofactoring variable
-            iVar = Gia_SplitCofVar( pLast );
             Depth = Vec_IntSize(pLast->vCofVars);
+            iVar = Gia_SplitCofVar2( pLast );
             // cofactor
             pPart0 = Gia_ManDupCofactor( pLast, iVar, 0 );
             // create variable
@@ -371,8 +406,6 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose )
             fSatUnsat = (fSatUnsat == Vec_PtrSize(vStack));
             if ( fSatUnsat )
                 Progress += 1.0 / pow(2, Depth + 1);
-            else
-                Cec_GiaSplitPrintRefs( pPart0 );
             if ( fVerbose ) 
                 Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk );
             // cofactor
@@ -395,8 +428,8 @@ int Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose )
                 Progress += 1.0 / pow(2, Depth + 1);
             if ( fVerbose )
                 Cec_GiaSplitPrint( nIter, Depth, nSatVars, nSatConfs, fSatUnsat, Progress, Abc_Clock() - clk );
-//            if ( Vec_PtrSize(vStack) > 5 )
-//                break;
+            if ( Vec_PtrSize(vStack) > 3 )
+                break;
         }
         if ( Vec_PtrSize(vStack) == 0 )
             RetValue = 1;