From e69854f5400a51651ac00bfdb32ee95a1881032b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 2 Jun 2014 09:55:17 -0700 Subject: Adding CEC command &splitprove. --- src/aig/gia/gia.h | 2 +- src/aig/gia/giaDup.c | 4 +- src/base/abci/abc.c | 64 +++++++++++++++++ src/proof/cec/cecSplit.c | 180 +++++++++++++++++++++++++++++++++++++++++------ 4 files changed, 227 insertions(+), 23 deletions(-) (limited to 'src') 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 ); @@ -32861,6 +32863,68 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + 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 [] 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; } //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3