diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-10-02 11:11:10 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-10-02 11:11:10 -0700 |
| commit | 7f3842e1861c12fdd1827ea7fda96f6c8b7fc8ca (patch) | |
| tree | eb1f87a9aed41dc50832435043e8125d6f8fd9f0 /src/base/wlc | |
| parent | 44550a67fa60534cef92bfc7b2f0f07d9b18b09a (diff) | |
| download | abc-7f3842e1861c12fdd1827ea7fda96f6c8b7fc8ca.tar.gz abc-7f3842e1861c12fdd1827ea7fda96f6c8b7fc8ca.tar.bz2 abc-7f3842e1861c12fdd1827ea7fda96f6c8b7fc8ca.zip | |
Bug fix in SMT parser.
Diffstat (limited to 'src/base/wlc')
| -rw-r--r-- | src/base/wlc/wlcReadSmt.c | 32 |
1 files changed, 12 insertions, 20 deletions
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c index 0791154a..d07a54c4 100644 --- a/src/base/wlc/wlcReadSmt.c +++ b/src/base/wlc/wlcReadSmt.c @@ -648,6 +648,12 @@ int Smt_PrsBuildNode( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int RangeOut, // s3087 int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound ); assert( fFound ); + // create buffer if the name of the fanin has different name + if ( pName && strcmp(pStr, pName) ) + { + Vec_IntFill( &p->vTempFans, 1, iObj ); + iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, RangeOut, &p->vTempFans, pName ); + } return iObj; } } @@ -1192,7 +1198,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) Vec_Int_t * vFansRoot, * vFans, * vFans2; Vec_Int_t * vAsserts = Vec_IntAlloc(100); int i, Root, Fan, iObj, NameId, Range, Status, nBits = 0; - char * pName, * pRange, * pValue; + char * pName, * pRange; // start network and create primary inputs pNtk = Wlc_NtkAlloc( p->pName, 1000 ); pNtk->pManName = Abc_NamStart( 1000, 24 ); @@ -1272,27 +1278,13 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p ) { // (define-fun s_2 () Bool false) assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) ); - Range = 1; - pValue = Smt_VecEntryName(p, vFans, 4); - if ( pValue != NULL ) + iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 4), -1, pName ); + if ( iObj == 0 ) { - if ( !strcmp("false", pValue) ) - pValue = "#b0"; - else if ( !strcmp("true", pValue) ) - pValue = "#b1"; - else assert( 0 ); - Status = Smt_PrsBuildConstant( pNtk, pValue, Range, pName ); - } - else - { - iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 4), -1, pName ); - if ( iObj == 0 ) - { - Wlc_NtkFree( pNtk ); pNtk = NULL; - goto finish; - } - continue; + Wlc_NtkFree( pNtk ); pNtk = NULL; + goto finish; } + continue; } else { |