summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h1
-rw-r--r--src/aig/gia/giaAbsVta.c73
-rw-r--r--src/aig/gia/giaMan.c2
-rw-r--r--src/base/abci/abc.c61
4 files changed, 109 insertions, 28 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 4fbff031..14fd4d6e 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -205,6 +205,7 @@ struct Gia_ParVta_t_
int nFramesMax; // maximum frames
int nConfLimit; // conflict limit
int nTimeOut; // timeout in seconds
+ int fUseTermVars; // use terminal variables
int fVerbose; // verbose flag
int iFrame; // the number of frames covered
};
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index c3574e26..fe30d0f0 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -23,7 +23,7 @@
ABC_NAMESPACE_IMPL_START
-#define VTA_LARGE 0xFFFFFF
+#define VTA_LARGE 0xFFFFFFF
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -35,7 +35,7 @@ struct Vta_Obj_t_
int iObj;
int iFrame;
int iNext;
- unsigned Prio : 24; // related to VTA_LARGE
+ unsigned Prio : 28; // related to VTA_LARGE
unsigned Value : 2;
unsigned fAdded : 1;
unsigned fNew : 1;
@@ -60,6 +60,8 @@ struct Vta_Man_t_
Vec_Ptr_t * vFrames; // start abstraction for each frame
int nWords; // the number of words in the record
Vec_Int_t * vSeens; // seen objects
+ Vec_Bit_t * vSeenGla; // seen objects in all frames
+ int nSeenGla; // seen objects in all frames
// other data
Vec_Int_t * vCla2Var; // map clauses into variables
Vec_Ptr_t * vCores; // unsat core for each frame
@@ -202,6 +204,7 @@ Vec_Int_t * Gia_VtaFramesToAbs( Vec_Vec_t * vFrames )
***********************************************************************/
Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs )
{
+ Gia_Obj_t * pObj;
Vec_Int_t * vPresent;
int nObjMask, nObjs = Gia_ManObjNum(p);
int i, Entry, nFrames = Vec_IntEntry( vAbs, 0 );
@@ -210,9 +213,14 @@ Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs )
nObjMask = (1 << Gia_Base2Log(nObjs)) - 1;
assert( nObjs <= nObjMask );
// go through objects
- vPresent = Vec_IntAlloc( nObjs );
+ vPresent = Vec_IntStart( nObjs );
+ Vec_IntWriteEntry( vPresent, 0, 1 );
Vec_IntForEachEntryStart( vAbs, Entry, i, nFrames+2 )
+ {
+ pObj = Gia_ManObj( p, (Entry & nObjMask) );
+ assert( Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsConst0(pObj) );
Vec_IntWriteEntry( vPresent, (Entry & nObjMask), 1 );
+ }
return vPresent;
}
@@ -773,6 +781,8 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
assert( Gia_ManObjNum(pGia) <= (int)p->nObjMask );
p->nWords = 1;
p->vSeens = Vec_IntStart( Gia_ManObjNum(pGia) * p->nWords );
+ p->vSeenGla = Vec_BitStart( Gia_ManObjNum(pGia) );
+ p->nSeenGla = 1;
// start the abstraction
if ( pGia->vObjClasses == NULL )
p->vFrames = Gia_ManUnrollAbs( pGia, pPars->nFramesStart );
@@ -811,8 +821,13 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars )
***********************************************************************/
void Vga_ManStop( Vta_Man_t * p )
{
+ if ( p->pPars->fVerbose )
+ printf( "SAT solver: Variables = %d. Clauses = %d. Conflicts = %d.\n",
+ sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat) );
+
Vec_VecFreeP( (Vec_Vec_t **)&p->vCores );
Vec_VecFreeP( (Vec_Vec_t **)&p->vFrames );
+ Vec_BitFreeP( &p->vSeenGla );
Vec_IntFreeP( &p->vSeens );
Vec_IntFreeP( &p->vOrder );
Vec_IntFreeP( &p->vCla2Var );
@@ -845,16 +860,12 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat
RetValue = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( RetValue == l_Undef )
{
-// if ( fVerbose )
- printf( "Conflict limit is reached.\n" );
if ( piRetValue )
*piRetValue = -1;
return NULL;
}
if ( RetValue == l_True )
{
-// if ( fVerbose )
- printf( "The BMC problem is SAT.\n" );
if ( piRetValue )
*piRetValue = 0;
return NULL;
@@ -930,13 +941,20 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames )
}
pCountAll[iFrame+1]++;
pCountAll[0]++;
+ if ( !Vec_BitEntry(p->vSeenGla, iObj) )
+ {
+ Vec_BitWriteEntry(p->vSeenGla, iObj, 1);
+ p->nSeenGla++;
+ }
}
// printf( "%5d%5d", pCountAll[0], pCountUni[0] );
- printf( "%7d", pCountAll[0] );
+ printf( "%6d", p->nSeenGla );
+ printf( "%6d", pCountAll[0] );
for ( k = 0; k < nFrames; k++ )
// printf( "%5d%5d ", pCountAll[k+1], pCountUni[k+1] );
printf( "%4d", pCountAll[k+1] );
printf( "\n" );
+ fflush( stdout );
ABC_FREE( pCountAll );
ABC_FREE( pCountUni );
}
@@ -953,13 +971,14 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames )
***********************************************************************/
void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame )
-{
+{
Vta_Obj_t * pThis0, * pThis1;
Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
Vta_Obj_t * pThis = Vga_ManFindOrAdd( p, iObj, iFrame );
int iMainVar = Vta_ObjId(p, pThis);
assert( pThis->iObj == iObj && pThis->iFrame == iFrame );
- assert( pThis->fAdded == 0 );
+ if ( pThis->fAdded )
+ return;
pThis->fAdded = 1;
if ( Gia_ObjIsAnd(pObj) )
{
@@ -977,14 +996,18 @@ void Vga_ManAddClausesOne( Vta_Man_t * p, int iObj, int iFrame )
//printf( "Adding flop %d (var %d)\n", iObj, iMainVar );
if ( iFrame == 0 )
{
- /*
- pThis0 = Vga_ManFindOrAdd( p, iObj, -1 );
- sat_solver2_add_constraint( p->pSat, iMainVar, Vta_ObjId(p, pThis0), 1, 0 );
- Vec_IntPush( p->vCla2Var, iMainVar );
- Vec_IntPush( p->vCla2Var, iMainVar );
- */
- sat_solver2_add_const( p->pSat, iMainVar, 1, 0 );
- Vec_IntPush( p->vCla2Var, iMainVar );
+ if ( p->pPars->fUseTermVars )
+ {
+ pThis0 = Vga_ManFindOrAdd( p, iObj, -1 );
+ sat_solver2_add_constraint( p->pSat, iMainVar, Vta_ObjId(p, pThis0), 1, 0 );
+ Vec_IntPush( p->vCla2Var, iMainVar );
+ Vec_IntPush( p->vCla2Var, iMainVar );
+ }
+ else
+ {
+ sat_solver2_add_const( p->pSat, iMainVar, 1, 0 );
+ Vec_IntPush( p->vCla2Var, iMainVar );
+ }
}
else
{
@@ -1061,6 +1084,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Abc_Cex_t * pCex = NULL;
Gia_Obj_t * pObj;
int i, f, Status, RetValue = -1;
+ int clk = clock();
// preconditions
assert( Gia_ManPoNum(pAig) == 1 );
assert( pPars->nFramesMax == 0 || pPars->nFramesStart <= pPars->nFramesMax );
@@ -1068,12 +1092,11 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
p = Vga_ManStart( pAig, pPars );
// perform initial abstraction
if ( p->pPars->fVerbose )
- printf( "Frame Confl All F0 F1 F2 F3 ...\n" );
+ printf( "Frame Confl One All F0 F1 F2 F3 ...\n" );
for ( f = 0; !p->pPars->nFramesMax || f < p->pPars->nFramesMax; f++ )
{
if ( p->pPars->fVerbose )
printf( "%3d :", f );
-//printf( "\n" );
p->pPars->iFrame = f;
// realloc storage for abstraction marks
if ( f == p->nWords * 32 )
@@ -1083,7 +1106,6 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{
// load this timeframe
Vga_ManLoadSlice( p, Vec_PtrEntry(p->vFrames, f), 0 );
-// Vga_ManAddClausesOne( p, 0, f );
// run SAT solver
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status );
assert( (vCore != NULL) == (Status == 1) );
@@ -1109,10 +1131,9 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
{
/*
// load the time frame
- int Limit = Abc_MinInt(3, p->pPars->nFramesStart);
+ int Limit = Abc_MinInt(5, p->pPars->nFramesStart);
for ( i = 1; i <= Limit; i++ )
Vga_ManLoadSlice( p, Vec_PtrEntry(p->vCores, f-i), i );
-// Vga_ManAddClausesOne( p, 0, f );
// iterate as long as there are counter-examples
do {
vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status );
@@ -1163,9 +1184,9 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
Vec_IntFreeP( &pAig->vObjClasses );
pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
if ( Status == -1 )
- printf( "SAT solver ran out of resources at %d conflicts in frame %d.\n", pPars->nConfLimit, f );
+ printf( "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f );
else
- printf( "SAT solver completed %d frames and produced an abstraction.\n", f+1 );
+ printf( "SAT solver completed %d frames and produced an abstraction. ", f+1 );
}
else
{
@@ -1173,7 +1194,9 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
p->pGia->pCexSeq = pCex;
if ( !Gia_ManVerifyCex( p->pGia, pCex, 0 ) )
printf( "Gia_VtaPerform(): CEX verification has failed!\n" );
+ printf( "Counter-example detected in frame %d. ", f );
}
+ Abc_PrintTime( 1, "Time", clock() - clk );
Vga_ManStop( p );
return RetValue;
}
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 769006c2..39b0059d 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -277,7 +277,7 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p )
nObjMask = (1 << nObjBits) - 1;
assert( Gia_ManObjNum(p) <= nObjMask );
// print info about frames
- printf( "Frame All F0 F1 F2 F3 ...\n" );
+ printf( "Frame All F0 F1 F2 F3 ...\n" );
for ( i = 0; i < nFrames; i++ )
{
iStart = Vec_IntEntry( vAbs, i+1 );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 6022a540..d39b535d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -385,6 +385,7 @@ static int Abc_CommandAbc9GlaDerive ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9GlaCba ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GlaPba ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Vta ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Vta2Gla ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Reparam ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9BackReach ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Posplit ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -845,6 +846,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&gla_cba", Abc_CommandAbc9GlaCba, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&gla_pba", Abc_CommandAbc9GlaPba, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&vta", Abc_CommandAbc9Vta, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&vta_gla", Abc_CommandAbc9Vta2Gla, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&reparam", Abc_CommandAbc9Reparam, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&back_reach", Abc_CommandAbc9BackReach, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&posplit", Abc_CommandAbc9Posplit, 0 );
@@ -29573,7 +29575,7 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Gia_VtaSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTtvh" ) ) != EOF )
{
switch ( c )
{
@@ -29621,6 +29623,9 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nTimeOut < 0 )
goto usage;
break;
+ case 't':
+ pPars->fUseTermVars ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -29661,12 +29666,13 @@ int Abc_CommandAbc9Vta( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &vta [-SFCT num] [-vh]\n" );
+ Abc_Print( -2, "usage: &vta [-SFCT num] [-tvh]\n" );
Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" );
Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart );
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
+ Abc_Print( -2, "\t-t : toggle using terminal variables [default = %s]\n", pPars->fUseTermVars? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -29683,6 +29689,57 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9Vta2Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Vta2Gla(): There is no AIG.\n" );
+ return 1;
+ }
+ if ( pAbc->pGia->vObjClasses == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Vta2Gla(): There is no variable-time-frame abstraction defines.\n" );
+ return 1;
+ }
+ Vec_IntFreeP( &pAbc->pGia->vGateClasses );
+ pAbc->pGia->vGateClasses = Gia_VtaConvertToGla( pAbc->pGia, pAbc->pGia->vObjClasses );
+ Vec_IntFreeP( &pAbc->pGia->vObjClasses );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &vta_gla [-vh]\n" );
+ Abc_Print( -2, "\t maps variable- into fixed-time-frame abstraction\n" );
+ 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_CommandAbc9Reparam( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp = NULL;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 15:34:50 +0000