Adding CEC command &splitprove.

4 files changed, 227 insertions, 23 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 8b945d46..870ac85c 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1013,7 +1013,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 );  
+extern Gia_Man_t *         Gia_ManDupDfsRehash( Gia_Man_t * p, int nSteps, 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 acf151f3..2d294433 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1210,7 +1210,7 @@ void Gia_ManDupDfsRehash_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj
     Gia_ManDupDfsRehash_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 )
+Gia_Man_t * Gia_ManDupDfsRehash( Gia_Man_t * p, int nSteps, int Value )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj;
@@ -1221,7 +1221,7 @@ Gia_Man_t * Gia_ManDupDfsRehash( Gia_Man_t * p, int nSteps )
     Gia_ManFillValue( p );
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
-        pObj->Value = i < nSteps ? 1 : Gia_ManAppendCi(pNew);
+        pObj->Value = i < nSteps ? Value : Gia_ManAppendCi(pNew);
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManDupDfsRehash_rec( pNew, p, Gia_ObjFanin0(pObj) );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 44d40026..d4dede6d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -399,6 +399,7 @@ static int Abc_CommandAbc9Slice              ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9PoPart             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GroupProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9MultiProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9SplitProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Bmc                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9BCore              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9ICheck             ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -971,6 +972,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&popart",       Abc_CommandAbc9PoPart,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&gprove",       Abc_CommandAbc9GroupProve,   0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mprove",       Abc_CommandAbc9MultiProve,   0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&splitprove",   Abc_CommandAbc9SplitProve,   0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&bmc",          Abc_CommandAbc9Bmc,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&bcore",        Abc_CommandAbc9BCore,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&icheck",       Abc_CommandAbc9ICheck,       0 );
@@ -32872,6 +32874,68 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9SplitProve( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Cec_GiaSplitTest( Gia_Man_t * p, int nTimeOut, int fVerbose );
+    int c, nTimeOut = 1, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Tvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nTimeOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nTimeOut <= 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9SplitProve(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) > 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9SplitProve(): The problem is sequential.\n" );
+        return 1;
+    }
+    Cec_GiaSplitTest( pAbc->pGia, nTimeOut, fVerbose );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &splitprove [-T num] [-vh]\n" );
+    Abc_Print( -2, "\t         proves CEC problem by case-splitting\n" );
+    Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     int c;
diff --git a/src/proof/cec/cecSplit.c b/src/proof/cec/cecSplit.c
index 05bfd9f4..0f3f84c2 100644
--- a/src/proof/cec/cecSplit.c
+++ b/src/proof/cec/cecSplit.c
@@ -19,7 +19,10 @@
 ***********************************************************************/
 
 #include "aig/gia/gia.h"
+#include "aig/gia/giaAig.h"
 #include "bdd/cudd/cuddInt.h"
+#include "sat/cnf/cnf.h"
+#include "sat/bsat/satStore.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -167,6 +170,8 @@ void Cec_GiaSplitExplore( Gia_Man_t * p )
     }
 }
 
+
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -178,30 +183,165 @@ void Cec_GiaSplitExplore( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Cec_GiaSplitTest( Gia_Man_t * p )
+static inline Cnf_Dat_t * Cec_GiaDeriveGiaRemapped( Gia_Man_t * p )
 {
-    Gia_Man_t * pNew;
-//    Gia_Man_t * pMuxes;
-    Gia_Man_t * pCof;
-    Gia_Obj_t * pObj;
+    Cnf_Dat_t * pCnf;
+    Aig_Man_t * pAig = Gia_ManToAigSimple( p );
+    pAig->nRegs = 0;
+    pCnf = Cnf_Derive( pAig, 0 );//Aig_ManCoNum(pAig) );
+    Aig_ManStop( pAig );
+    return pCnf;
+}
+static inline sat_solver * Cec_GiaDeriveSolver( Gia_Man_t * p, int nTimeOut )
+{
+    sat_solver * pSat;
+    Cnf_Dat_t * pCnf;
     int i;
-    pNew = Gia_PermuteSpecial( p );
-    Gia_ManCreateRefs( pNew );
-    Gia_ManForEachPi( pNew, pObj, i )
-        printf( "%d ", Gia_ObjRefNum(pNew, pObj) );
-    printf( "\n" );
-//    Cec_GiaSplitExplore( pNew );
-//    Gia_ManBuildBddTest( p );
+    pCnf = Cec_GiaDeriveGiaRemapped( p );
+    pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, pCnf->nVars );
+    for ( i = 0; i < pCnf->nClauses; i++ )
+        if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+            assert( 0 );
+    sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
+    Cnf_DataFree( pCnf );
+    return pSat;
+}
+static inline int Cnf_GiaSolveOne( Gia_Man_t * p, int nTimeOut, int fVerbose )
+{
+    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( "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 );
+    }
+    sat_solver_delete( pSat );
+    if ( status == l_Undef )
+        return -1;
+    if ( status == l_False )
+        return 1;
+    return 0;
 /*
-    // derive muxes
-    pMuxes = Gia_ManDupMuxes( pNew );
-    printf( "GIA manager has %d ANDs, %d XORs, %d MUXes.\n", 
-        Gia_ManAndNum(pMuxes) - Gia_ManXorNum(pMuxes) - Gia_ManMuxNum(pMuxes), Gia_ManXorNum(pMuxes), Gia_ManMuxNum(pMuxes) ); 
-    Gia_ManStop( pMuxes );
+    // get pattern
+    Vec_IntClear( vLits );
+    for ( i = 0; i < nFuncVars; i++ )
+        Vec_IntPush( vLits, Vec_IntEntry(vTests, Iter*nFuncVars + i) );
+    Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars );
+    if ( pPars->fVerbose )
+    {
+        printf( "Iter%6d : ",       Iter );
+        printf( "Var =%10d  ",      sat_solver_nvars(pSat) );
+        printf( "Clause =%10d  ",   sat_solver_nclauses(pSat) );
+        printf( "Conflict =%10d  ", sat_solver_nconflicts(pSat) );
+        //Abc_PrintTime( 1, "Time", clkSat );
+        ABC_PRTr( "Solver time", clkSat );
+    }
 */
-    pCof = Gia_ManDupDfsRehash( pNew, 20 );
-    Gia_ManStop( pNew );
-    return pCof;
+}
+static inline int Cnf_GiaCheckOne( Vec_Ptr_t * vStack, Gia_Man_t * p, int nTimeOut, int fVerbose )
+{
+    int status = Cnf_GiaSolveOne( p, nTimeOut, fVerbose );
+    if ( status == -1 )
+    {
+        Vec_PtrPush( vStack, p );
+        return 1;
+    }
+    Gia_ManStop( p );
+    if ( status == 1 )
+        return 1;
+    // satisfiable
+    return 0;
+}
+static inline void Cec_GiaSplitClean( Vec_Ptr_t * vStack )
+{
+    Gia_Man_t * pNew;
+    int i;
+    Vec_PtrForEachEntry( Gia_Man_t *, vStack, pNew, i )
+        Gia_ManStop( pNew );
+    Vec_PtrFree( vStack );
+}
+
+/**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;
+    Gia_Obj_t * pObj;
+    int i, RetValue = -1;
+    // reorder variables
+    pNew = Gia_PermuteSpecial( p );
+    if ( fVerbose )
+    {
+        Gia_ManCreateRefs( pNew );
+        Gia_ManForEachPi( pNew, pObj, i )
+            printf( "%d ", Gia_ObjRefNum(pNew, pObj) );
+        printf( "\n" );
+    }
+    // start with the current problem
+    vStack = Vec_PtrAlloc( 1000 );
+    if ( !Cnf_GiaCheckOne(vStack, pNew, nTimeOut, fVerbose) )
+        RetValue = 0;
+    else
+    {
+        while ( Vec_PtrSize(vStack) > 0 )
+        {
+            pNew = (Gia_Man_t *)Vec_PtrPop( vStack );
+            // cofactor
+            pPart0 = Gia_ManDupDfsRehash( pNew, 1, 0 );
+            if ( !Cnf_GiaCheckOne(vStack, pPart0, nTimeOut, fVerbose) )
+            {
+                Gia_ManStop( pNew );
+                RetValue = 0;
+                break;
+            }
+            // cofactor
+            pPart1 = Gia_ManDupDfsRehash( pNew, 1, 1 );
+            Gia_ManStop( pNew );
+            if ( !Cnf_GiaCheckOne(vStack, pPart1, nTimeOut, fVerbose) )
+            {
+                RetValue = 0;
+                break;
+            }
+            if ( Vec_PtrSize(vStack) > 2 )
+                break;
+        }
+        if ( Vec_PtrSize(vStack) == 0 )
+            RetValue = 1;
+    }
+    Cec_GiaSplitClean( vStack );
+    if ( RetValue == 0 )
+        printf( "Problem is SAT\n" );
+    else if ( RetValue == 1 )
+        printf( "Problem is UNSAT\n" );
+    else if ( RetValue == -1 )
+        printf( "Problem is UNDECIDED\n" );
+    else assert( 0 );
+    return RetValue;
 }
 
 ////////////////////////////////////////////////////////////////////////