Skip to content

A
abc
Commit e69854f5 by Alan Mishchenko
Options

Adding CEC command &splitprove.

parent 9030f461
Showing with 227 additions and 23 deletions
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 );
......
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) );
......
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;
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;
}
////////////////////////////////////////////////////////////////////////
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment