summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abci/abc.c8
-rw-r--r--src/base/wlc/wlcReadSmt.c370
2 files changed, 376 insertions, 2 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index da3a2d96..259c1b14 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -23269,7 +23269,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Saig_ParBmcSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdruvzh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdurvzh" ) ) != EOF )
{
switch ( c )
{
@@ -23435,6 +23435,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'u':
fOrDecomp ^= 1;
break;
+ case 'r':
+ pPars->fNoRestarts ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -23501,7 +23504,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-LW file] [-axduvzh]\n" );
+ Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-LW file] [-axdurvzh]\n" );
Abc_Print( -2, "\t performs bounded model checking with dynamic unrolling\n" );
Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", pPars->nFramesMax );
@@ -23521,6 +23524,7 @@ usage:
Abc_Print( -2, "\t-x : toggle storing CEXes when solving all outputs [default = %s]\n", pPars->fStoreCex? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dropping (replacing by 0) SAT outputs [default = %s]\n", pPars->fDropSatOuts? "yes": "no" );
Abc_Print( -2, "\t-u : toggle performing structural OR-decomposition [default = %s]\n", fOrDecomp? "yes": "not" );
+ Abc_Print( -2, "\t-r : toggle disabling periodic restarts [default = %s]\n", pPars->fNoRestarts? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c
index 4ef0f537..0a8913fe 100644
--- a/src/base/wlc/wlcReadSmt.c
+++ b/src/base/wlc/wlcReadSmt.c
@@ -41,6 +41,9 @@ struct Smt_Prs_t_
Vec_Int_t vStack; // current node on each level
//Vec_Wec_t vDepth; // objects on each level
Vec_Wec_t vObjs; // objects
+ int NameCount;
+ int nDigits;
+ Vec_Int_t vTempFans;
// error handling
char ErrorStr[1000];
};
@@ -671,6 +674,371 @@ finish:
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Smt_PrsGenName( Smt_Prs_t * p )
+{
+ static char Buffer[16];
+ sprintf( Buffer, "_%0*X_", p->nDigits, ++p->NameCount );
+ return Buffer;
+}
+int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode )
+{
+ if ( Smt_EntryIsName(iNode) )
+ {
+ int fFound, iObj;
+ char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode));
+ if ( pStr[0] == '#' )
+ {
+ int i, nDigits, nBits = -1, iObj = -1;
+ Vec_IntClear( &p->vTempFans );
+ if ( pStr[1] == 'b' ) // binary
+ {
+ nBits = strlen(pStr+2);
+ Vec_IntFill( &p->vTempFans, Abc_BitWordNum(nBits), 0 );
+ for ( i = 0; i < nBits; i++ )
+ if ( pStr[2+i] == '1' )
+ Abc_InfoSetBit( (unsigned *)Vec_IntArray(&p->vTempFans), nBits-1-i );
+ else if ( pStr[2+i] != '0' )
+ return 0;
+ }
+ else if ( pStr[1] == 'x' ) // hexadecimal
+ {
+ nBits = strlen(pStr+2)*4;
+ Vec_IntFill( &p->vTempFans, Abc_BitWordNum(nBits), 0 );
+ nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(&p->vTempFans), pStr+2 );
+ if ( nDigits != (nBits + 3)/4 )
+ return 0;
+ }
+ else return 0;
+ // create constant node
+ iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_CONST, 0, nBits, &p->vTempFans, Smt_PrsGenName(p) );
+ return iObj;
+ }
+ iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound );
+ assert( fFound );
+ return iObj;
+ }
+ else
+ {
+ Vec_Int_t * vRoots, * vRoots1, * vFans3;
+ int iRoot0, iRoot1, Fan, Fan3, k;
+ assert( !Smt_EntryIsName(iNode) );
+ vRoots = Smt_EntryNode( p, iNode );
+ iRoot0 = Vec_IntEntry( vRoots, 0 );
+ if ( Smt_EntryIsName(iRoot0) )
+ {
+ char * pName, * pStr0 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot0));
+ int iObj;
+ if ( pStr0[0] == 'l' && pStr0[1] == 'e' && pStr0[2] == 't' && pStr0[3] == '\0' )
+ {
+ // let ((s35550 (bvor s48 s35549)))
+ assert( Vec_IntSize(vRoots) == 3 );
+ assert( Smt_VecEntryIsType(vRoots, 0, SMT_PRS_LET) );
+ // get parts
+ iRoot1 = Vec_IntEntry(vRoots, 1);
+ assert( !Smt_EntryIsName(iRoot1) );
+ vRoots1 = Smt_EntryNode(p, iRoot1);
+ //if ( Smt_VecEntryIsType(vRoots1, 0, SMT_PRS_LET) )
+ // continue;
+
+ // iterate through the parts
+ Vec_IntForEachEntry( vRoots1, Fan, k )
+ {
+ // s35550 (bvor s48 s35549)
+ Fan = Vec_IntEntry(vRoots1, 0);
+ assert( !Smt_EntryIsName(Fan) );
+ vFans3 = Smt_EntryNode(p, Fan);
+ // get the name
+ Fan3 = Vec_IntEntry(vFans3, 0);
+ assert( Smt_EntryIsName(Fan3) );
+ pName = Smt_EntryName(p, Fan3);
+ // get function
+ Fan3 = Vec_IntEntry(vFans3, 1);
+ assert( !Smt_EntryIsName(Fan3) );
+ // solve the problem
+ iObj = Smt_PrsBuild2_rec( pNtk, p, Fan3 );
+ if ( iObj == 0 )
+ return 0;
+ // create buffer
+ Vec_IntFill( &p->vTempFans, 1, iObj );
+ return Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, &p->vTempFans, pName );
+ }
+ }
+ else if ( pStr0[0] == '_' )
+ {
+ int iRoot1 = Vec_IntEntry( vRoots, 1 );
+ char * pStr1 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot1));
+ if ( pStr1[0] == 'b' && pStr1[1] == 'v' )
+ {
+ int iObj = 0;
+ return iObj;
+ }
+ else
+ {
+ int Type1, Range = -1, fSigned = 0;
+ // call the other branch
+ assert( Vec_IntSize(vRoots) == 2 );
+ iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vRoots, 1) );
+ if ( iObj == 0 )
+ return 0;
+ Vec_IntFill( &p->vTempFans, 1, iObj );
+ // find out this branch
+ Type1 = Abc_Lit2Var(iRoot1);
+ if ( Type1 == WLC_OBJ_BIT_SIGNEXT || Type1 == WLC_OBJ_BIT_ZEROPAD || Type1 == WLC_OBJ_ROTATE_R || Type1 == WLC_OBJ_ROTATE_L )
+ {
+ int iRoot2 = Vec_IntEntry( vRoots, 2 );
+ char * pStr2 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot2));
+ int Num = atoi( pStr2 );
+ fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT);
+ Range = Num + Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) );
+ Vec_IntPush( &p->vTempFans, Num );
+ }
+ else if ( Type1 == WLC_OBJ_BIT_SELECT )
+ {
+ int iRoot2 = Vec_IntEntry( vRoots, 2 );
+ int iRoot3 = Vec_IntEntry( vRoots, 3 );
+ char * pStr2 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot2));
+ char * pStr3 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot3));
+ int Num1 = atoi( pStr2 );
+ int Num2 = atoi( pStr3 );
+ assert( Num1 >= Num2 );
+ fSigned = (Type1 == WLC_OBJ_BIT_SIGNEXT);
+ Range = (Num1 - Num2 + 1) + Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) );
+ Vec_IntPushTwo( &p->vTempFans, Num1, Num2 );
+ }
+ else assert( 0 );
+ iObj = Smt_PrsCreateNode( pNtk, Type1, fSigned, Range, &p->vTempFans, Smt_PrsGenName(p) );
+ return iObj;
+ }
+ }
+ else
+ {
+ Vec_Int_t * vFanins;
+ int i, Fan, fSigned = 0, Range, Type0;
+ int iObj = Abc_NamStrFind( pNtk->pManName, pStr0 );
+ if ( iObj > 0 )
+ return iObj;
+ Type0 = Smt_StrToType( pStr0, &fSigned );
+
+ // collect fanins
+ vFanins = Vec_IntAlloc( 100 );
+ Vec_IntForEachEntryStart( vRoots, Fan, i, 1 )
+ {
+ iObj = Smt_PrsBuild2_rec( pNtk, p, Fan );
+ if ( iObj == 0 )
+ {
+ Vec_IntFree( vFanins );
+ return 0;
+ }
+ Vec_IntPush( vFanins, iObj );
+ }
+ // update specialized nodes
+ assert( Type0 != WLC_OBJ_BIT_SIGNEXT && Type0 != WLC_OBJ_BIT_ZEROPAD && Type0 != WLC_OBJ_BIT_SELECT && Type0 != WLC_OBJ_ROTATE_R && Type0 != WLC_OBJ_ROTATE_L );
+ // find range
+ Range = 0;
+ if ( Type0 >= WLC_OBJ_LOGIC_NOT && Type0 <= WLC_OBJ_REDUCT_XOR )
+ Range = 1;
+ else if ( Type0 == WLC_OBJ_BIT_CONCAT )
+ {
+ Vec_IntForEachEntry( vFanins, Fan, i )
+ Range += Wlc_ObjRange( Wlc_NtkObj(pNtk, Fan) );
+ }
+ else if ( Type0 == WLC_OBJ_MUX )
+ {
+ int * pArray = Vec_IntArray(vFanins);
+ assert( Vec_IntSize(vFanins) == 3 );
+ ABC_SWAP( int, pArray[1], pArray[2] );
+ iObj = Vec_IntEntry(vFanins, 1);
+ Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) );
+ }
+ else // to determine range, look at the first argument
+ {
+ iObj = Vec_IntEntry(vFanins, 0);
+ Range = Wlc_ObjRange( Wlc_NtkObj(pNtk, iObj) );
+ }
+ // create node
+ assert( Range > 0 );
+ iObj = Smt_PrsCreateNode( pNtk, Type0, fSigned, Range, vFanins, Smt_PrsGenName(p) );
+ Vec_IntFree( vFanins );
+ return iObj;
+ }
+ }
+ else assert( 0 ); // return Smt_PrsBuild2_rec( pNtk, p, iRoot0 );
+ return 0;
+ }
+}
+Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
+{
+ Wlc_Ntk_t * pNtk;
+ Vec_Int_t * vFansRoot, * vFans, * vFans2;
+ Vec_Int_t * vAsserts = Vec_IntAlloc(100);
+ int i, Fan, iObj, NameId, Range, Status, nBits = 0;
+ char * pName, * pRange, * pValue;
+ // start network and create primary inputs
+ pNtk = Wlc_NtkAlloc( p->pName, 1000 );
+ pNtk->pManName = Abc_NamStart( 1000, 24 );
+ // collect top-level asserts
+ vFansRoot = Vec_WecEntry( &p->vObjs, 0 );
+ Vec_IntForEachEntry( vFansRoot, Fan, i )
+ {
+ assert( !Smt_EntryIsName(Fan) );
+ vFans = Smt_VecEntryNode( p, vFansRoot, i );
+ Fan = Vec_IntEntry(vFans, 0);
+ assert( Smt_EntryIsName(Fan) );
+ // create variables
+ if ( Abc_Lit2Var(Fan) == SMT_PRS_DECLARE_FUN )
+ {
+ assert( Vec_IntSize(vFans) == 4 );
+ assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DECLARE_FUN) );
+ // get name
+ Fan = Vec_IntEntry(vFans, 1);
+ assert( Smt_EntryIsName(Fan) );
+ pName = Smt_EntryName(p, Fan);
+ // skip ()
+ Fan = Vec_IntEntry(vFans, 2);
+ assert( !Smt_EntryIsName(Fan) );
+ // check type (Bool or BitVec)
+ Fan = Vec_IntEntry(vFans, 3);
+ if ( Smt_EntryIsName(Fan) )
+ {
+ //(declare-fun s1 () Bool)
+ assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) );
+ Range = 1;
+ }
+ else
+ {
+ // (declare-fun s1 () (_ BitVec 64))
+ // get range
+ Fan = Vec_IntEntry(vFans, 3);
+ assert( !Smt_EntryIsName(Fan) );
+ vFans2 = Smt_EntryNode(p, Fan);
+ assert( Vec_IntSize(vFans2) == 3 );
+ assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) );
+ assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) );
+ Fan = Vec_IntEntry(vFans2, 2);
+ assert( Smt_EntryIsName(Fan) );
+ pRange = Smt_EntryName(p, Fan);
+ Range = atoi(pRange);
+ }
+ // create node
+ iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_PI, 0, Range-1, 0 );
+ NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, NULL );
+ assert( iObj == NameId );
+ // save values
+ Vec_IntPush( &pNtk->vValues, NameId );
+ Vec_IntPush( &pNtk->vValues, nBits );
+ Vec_IntPush( &pNtk->vValues, Range );
+ nBits += Range;
+ }
+ // create constants
+ else if ( Abc_Lit2Var(Fan) == SMT_PRS_DEFINE_FUN )
+ {
+ assert( Vec_IntSize(vFans) == 5 );
+ assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) );
+ // get name
+ Fan = Vec_IntEntry(vFans, 1);
+ assert( Smt_EntryIsName(Fan) );
+ pName = Smt_EntryName(p, Fan);
+ // skip ()
+ Fan = Vec_IntEntry(vFans, 2);
+ assert( !Smt_EntryIsName(Fan) );
+ // check type (Bool or BitVec)
+ Fan = Vec_IntEntry(vFans, 3);
+ if ( Smt_EntryIsName(Fan) )
+ {
+ // (define-fun s_2 () Bool false)
+ assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) );
+ Range = 1;
+ pValue = Smt_VecEntryName(p, vFans, 4);
+ if ( !strcmp("false", pValue) )
+ pValue = "#b0";
+ else if ( !strcmp("true", pValue) )
+ pValue = "#b1";
+ else assert( 0 );
+ Status = Smt_PrsBuildConstant( pNtk, pValue, Range, pName );
+ }
+ else
+ {
+ // (define-fun s702 () (_ BitVec 4) #xe)
+ // (define-fun s1 () (_ BitVec 8) (bvneg #x7f))
+ // get range
+ Fan = Vec_IntEntry(vFans, 3);
+ assert( !Smt_EntryIsName(Fan) );
+ vFans2 = Smt_VecEntryNode(p, vFans, 3);
+ assert( Vec_IntSize(vFans2) == 3 );
+ assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) );
+ assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) );
+ // get range
+ Fan = Vec_IntEntry(vFans2, 2);
+ assert( Smt_EntryIsName(Fan) );
+ pRange = Smt_EntryName(p, Fan);
+ Range = atoi(pRange);
+ // get constant
+ Fan = Vec_IntEntry(vFans, 4);
+ Status = Smt_PrsBuildNode( pNtk, p, Fan, Range, pName );
+ }
+ if ( !Status )
+ {
+ Wlc_NtkFree( pNtk ); pNtk = NULL;
+ goto finish;
+ }
+ }
+ // collect assertion outputs
+ else if ( Abc_Lit2Var(Fan) == SMT_PRS_ASSERT )
+ {
+ //(assert ; no quantifiers
+ // (let ((s2 (bvsge s0 s1)))
+ // (not s2)))
+ //(assert (not (= s0 #x00)))
+ assert( Vec_IntSize(vFans) == 2 );
+ assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_ASSERT) );
+ iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 1) );
+ if ( iObj == 0 )
+ {
+ Wlc_NtkFree( pNtk ); pNtk = NULL;
+ goto finish;
+ }
+ Vec_IntPush( vAsserts, iObj );
+ }
+ // issue warnings about unknown dirs
+ else if ( Abc_Lit2Var(Fan) >= SMT_PRS_END )
+ {
+ printf( "Ignoring directive \"%s\".\n", Smt_EntryName(p, Fan) );
+ continue;
+ }
+ }
+ // build AND of asserts
+ if ( Vec_IntSize(vAsserts) == 1 )
+ iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, vAsserts, "miter_output" );
+ else
+ {
+ iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vAsserts), vAsserts, NULL );
+ Vec_IntFill( vAsserts, 1, iObj );
+ iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_REDUCT_AND, 0, 1, vAsserts, "miter_output" );
+ }
+ Wlc_ObjSetCo( pNtk, Wlc_NtkObj(pNtk, iObj), 0 );
+ // create nameIDs
+ vFans = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) );
+ Vec_IntAppend( &pNtk->vNameIds, vFans );
+ Vec_IntFree( vFans );
+ //Wlc_NtkReport( pNtk, NULL );
+finish:
+ // cleanup
+ Vec_IntFree(vAsserts);
+ return pNtk;
+}
+
+
/**Function*************************************************************
@@ -767,6 +1135,7 @@ static inline void Smt_PrsFree( Smt_Prs_t * p )
if ( p->pStrs )
Abc_NamDeref( p->pStrs );
Vec_IntErase( &p->vStack );
+ Vec_IntErase( &p->vTempFans );
//Vec_WecErase( &p->vDepth );
Vec_WecErase( &p->vObjs );
ABC_FREE( p );
@@ -865,6 +1234,7 @@ void Smt_PrsPrintParser( Smt_Prs_t * p )
{
// Vec_WecPrint( &p->vDepth, 0 );
Smt_PrsPrintParser_rec( p, 0, 0 );
+ p->nDigits = Abc_Base16Log( Vec_WecSize(&p->vObjs) );
}
/**Function*************************************************************