summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c28
-rw-r--r--src/base/cba/cbaCom.c6
-rw-r--r--src/base/wlc/wlc.h39
-rw-r--r--src/base/wlc/wlcBlast.c8
-rw-r--r--src/base/wlc/wlcCom.c36
-rw-r--r--src/base/wlc/wlcNtk.c47
-rw-r--r--src/base/wlc/wlcReadSmt.c154
7 files changed, 237 insertions, 81 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8b42ccfa..7ac54f38 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -21448,6 +21448,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
int fAlignPol;
int fAndOuts;
int fNewSolver;
+ int fSilent;
int fVerbose;
int nConfLimit;
int nLearnedStart;
@@ -21461,6 +21462,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
fAlignPol = 0;
fAndOuts = 0;
fNewSolver = 0;
+ fSilent = 0;
fVerbose = 0;
nConfLimit = 0;
nInsLimit = 0;
@@ -21468,7 +21470,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
nLearnedDelta = 0;
nLearnedPerce = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "CILDEpanvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CILDEpansvh" ) ) != EOF )
{
switch ( c )
{
@@ -21536,6 +21538,9 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'n':
fNewSolver ^= 1;
break;
+ case 's':
+ fSilent ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -21596,18 +21601,20 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
pAbc->pCex = Abc_CexCreate( 0, Abc_NtkPiNum(pNtk), pNtk->pModel, 0, 0, 0 );
}
pAbc->Status = RetValue;
- if ( RetValue == -1 )
- Abc_Print( 1, "UNDECIDED " );
- else if ( RetValue == 0 )
- Abc_Print( 1, "SATISFIABLE " );
- else
- Abc_Print( 1, "UNSATISFIABLE " );
- //Abc_Print( -1, "\n" );
- Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ if ( !fSilent )
+ {
+ if ( RetValue == -1 )
+ Abc_Print( 1, "UNDECIDED " );
+ else if ( RetValue == 0 )
+ Abc_Print( 1, "SATISFIABLE " );
+ else
+ Abc_Print( 1, "UNSATISFIABLE " );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ }
return 0;
usage:
- Abc_Print( -2, "usage: dsat [-CILDE num] [-panvh]\n" );
+ Abc_Print( -2, "usage: dsat [-CILDE num] [-pansvh]\n" );
Abc_Print( -2, "\t solves the combinational miter using SAT solver MiniSat-1.14\n" );
Abc_Print( -2, "\t derives CNF from the current network and leaves it unchanged\n" );
Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
@@ -21618,6 +21625,7 @@ usage:
Abc_Print( -2, "\t-p : align polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" );
Abc_Print( -2, "\t-a : toggle ANDing/ORing of miter outputs [default = %s]\n", fAndOuts? "ANDing": "ORing" );
Abc_Print( -2, "\t-n : toggle using new solver [default = %s]\n", fNewSolver? "yes": "no" );
+ Abc_Print( -2, "\t-s : enable silent computation (no reporting) [default = %s]\n", fSilent? "yes": "no" );
Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
diff --git a/src/base/cba/cbaCom.c b/src/base/cba/cbaCom.c
index af2af606..a3efe3b0 100644
--- a/src/base/cba/cbaCom.c
+++ b/src/base/cba/cbaCom.c
@@ -218,7 +218,11 @@ int Cba_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
{
p = Cba_ManReadCba( pFileName );
}
- else assert( 0 );
+ else
+ {
+ printf( "Unrecognized input file extension.\n" );
+ return 0;
+ }
Cba_AbcUpdateMan( pAbc, p );
return 0;
usage:
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index f789c03c..4e6c2255 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -68,24 +68,25 @@ typedef enum {
WLC_OBJ_LOGIC_NOT, // 23: logic NOT
WLC_OBJ_LOGIC_AND, // 24: logic AND
WLC_OBJ_LOGIC_OR, // 25: logic OR
- WLC_OBJ_COMP_EQU, // 26: compare equal
- WLC_OBJ_COMP_NOTEQU, // 27: compare not equal
- WLC_OBJ_COMP_LESS, // 28: compare less
- WLC_OBJ_COMP_MORE, // 29: compare more
- WLC_OBJ_COMP_LESSEQU, // 30: compare less or equal
- WLC_OBJ_COMP_MOREEQU, // 31: compare more or equal
- WLC_OBJ_REDUCT_AND, // 32: reduction AND
- WLC_OBJ_REDUCT_OR, // 33: reduction OR
- WLC_OBJ_REDUCT_XOR, // 34: reduction XOR
- WLC_OBJ_ARI_ADD, // 35: arithmetic addition
- WLC_OBJ_ARI_SUB, // 36: arithmetic subtraction
- WLC_OBJ_ARI_MULTI, // 37: arithmetic multiplier
- WLC_OBJ_ARI_DIVIDE, // 38: arithmetic division
- WLC_OBJ_ARI_MODULUS, // 39: arithmetic modulus
- WLC_OBJ_ARI_POWER, // 40: arithmetic power
- WLC_OBJ_ARI_MINUS, // 41: arithmetic minus
- WLC_OBJ_TABLE, // 42: bit table
- WLC_OBJ_NUMBER // 43: unused
+ WLC_OBJ_LOGIC_XOR, // 26: logic XOR
+ WLC_OBJ_COMP_EQU, // 27: compare equal
+ WLC_OBJ_COMP_NOTEQU, // 28: compare not equal
+ WLC_OBJ_COMP_LESS, // 29: compare less
+ WLC_OBJ_COMP_MORE, // 30: compare more
+ WLC_OBJ_COMP_LESSEQU, // 31: compare less or equal
+ WLC_OBJ_COMP_MOREEQU, // 32: compare more or equal
+ WLC_OBJ_REDUCT_AND, // 33: reduction AND
+ WLC_OBJ_REDUCT_OR, // 34: reduction OR
+ WLC_OBJ_REDUCT_XOR, // 35: reduction XOR
+ WLC_OBJ_ARI_ADD, // 36: arithmetic addition
+ WLC_OBJ_ARI_SUB, // 37: arithmetic subtraction
+ WLC_OBJ_ARI_MULTI, // 38: arithmetic multiplier
+ WLC_OBJ_ARI_DIVIDE, // 39: arithmetic division
+ WLC_OBJ_ARI_MODULUS, // 40: arithmetic modulus
+ WLC_OBJ_ARI_POWER, // 41: arithmetic power
+ WLC_OBJ_ARI_MINUS, // 42: arithmetic minus
+ WLC_OBJ_TABLE, // 43: bit table
+ WLC_OBJ_NUMBER // 44: unused
} Wlc_ObjType_t;
@@ -135,6 +136,7 @@ struct Wlc_Ntk_t_
// object names
Abc_Nam_t * pManName; // object names
Vec_Int_t vNameIds; // object name IDs
+ Vec_Int_t vValues; // value objects
// object attributes
int nTravIds; // counter of traversal IDs
Vec_Int_t vTravIds; // trav IDs of the objects
@@ -257,6 +259,7 @@ extern void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type );
extern void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose );
extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p );
extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
+extern void Wlc_NtkReport( Wlc_Ntk_t * p, Vec_Int_t * vAssign );
/*=== wlcReadSmt.c ========================================================*/
extern Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit );
extern Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName );
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 333b64de..4a935f6b 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -658,6 +658,14 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds )
for ( k = 1; k < nRange; k++ )
Vec_IntPush( vRes, 0 );
}
+ else if ( pObj->Type == WLC_OBJ_LOGIC_XOR )
+ {
+ int iLit0 = Wlc_BlastReduction( pNew, pFans0, nRange0, WLC_OBJ_REDUCT_OR );
+ int iLit1 = Wlc_BlastReduction( pNew, pFans1, nRange1, WLC_OBJ_REDUCT_OR );
+ Vec_IntFill( vRes, 1, Gia_ManHashXor(pNew, iLit0, iLit1) );
+ for ( k = 1; k < nRange; k++ )
+ Vec_IntPush( vRes, 0 );
+ }
else if ( pObj->Type == WLC_OBJ_COMP_EQU || pObj->Type == WLC_OBJ_COMP_NOTEQU )
{
int iLit = 0, nRangeMax = Abc_MaxInt( nRange0, nRange1 );
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 84afb394..6d437f55 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -115,21 +115,34 @@ static inline int Wlc_GenerateStop( Vec_Str_t * vInput, char * pLine, int LineSi
}
Vec_Str_t * Wlc_GenerateSmtStdin()
{
- char * pLine = "(check-sat)";
- int c, LineSize = strlen(pLine);
- Vec_Str_t * vInput = Vec_StrAlloc( 1000 );
+ //char * pLine = "(check-sat)";
+ //int c, LineSize = strlen(pLine);
+ Vec_Str_t * vInput = Vec_StrAlloc( 1000 ); int c;
while ( (c = fgetc(stdin)) != EOF )
- {
Vec_StrPush( vInput, (char)c );
- if ( c == ')' && Wlc_GenerateStop(vInput, pLine, LineSize) )
- break;
- }
Vec_StrPush( vInput, '\0' );
return vInput;
}
void Wlc_GenerateSmtStdout( Abc_Frame_t * pAbc )
{
- printf( "Output produced by SMT solver will be here.\n" );
+ if ( Abc_FrameReadProbStatus(pAbc) == -1 )
+ printf( "undecided\n" );
+ else if ( Abc_FrameReadProbStatus(pAbc) == 1 )
+ printf( "unsat\n" );
+ else if ( Abc_FrameReadProbStatus(pAbc) == 0 )
+ {
+ Vec_Int_t * vAssign = Vec_IntAlloc( 100 );
+ Abc_Cex_t * pCex = Abc_FrameReadCex( pAbc ); int i;
+ if ( pCex == NULL )
+ {
+ printf( "CEX is not found\n" );
+ return;
+ }
+ for ( i = 0; i < pCex->nPis; i++ )
+ Vec_IntPush( vAssign, Abc_InfoHasBit(pCex->pData, i) );
+ Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, vAssign );
+ Vec_IntFree( vAssign );
+ }
}
/**Function********************************************************************
@@ -417,9 +430,10 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// transform
- pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
- pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
- Wlc_AbcUpdateNtk( pAbc, pNtk );
+ //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
+ //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
+ //Wlc_AbcUpdateNtk( pAbc, pNtk );
+ Wlc_GenerateSmtStdout( pAbc );
return 0;
usage:
Abc_Print( -2, "usage: %%test [-vh]\n" );
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 48171c35..1576ef45 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -209,6 +209,7 @@ void Wlc_NtkFree( Wlc_Ntk_t * p )
Vec_IntFreeP( &p->vInits );
ABC_FREE( p->vTravIds.pArray );
ABC_FREE( p->vNameIds.pArray );
+ ABC_FREE( p->vValues.pArray );
ABC_FREE( p->vCopies.pArray );
ABC_FREE( p->pInits );
ABC_FREE( p->pObjs );
@@ -496,6 +497,52 @@ void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p )
pNew->vTables = p->vTables; p->vTables = NULL;
}
+/**Function*************************************************************
+
+ Synopsis [Report results.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Wlc_NtkReport( Wlc_Ntk_t * p, Vec_Int_t * vAssign )
+{
+ //sat
+//((s0 #x12000000070000000000c0000085006b))
+//((s1 #x0e008f00ff0000000000ff0000ed0040))
+//((s2 #x96008f00ff0000000000ff0000ed0040))
+
+ int i, Name, Start, nBits, k;
+ Vec_Str_t * vNum = Vec_StrAlloc( 100 );
+// Vec_IntForEachEntryTriple( &p->vValues, Name, Start, nBits, i )
+// printf( "Variable %s : %d %d\n", Abc_NamStr(p->pManName, Name), Start, nBits );
+ printf( "sat\n" );
+ Vec_IntForEachEntryTriple( &p->vValues, Name, Start, nBits, i )
+ {
+ Vec_StrClear( vNum );
+ for ( k = Start; k < Start + nBits; )
+ {
+ int j, Digit = 0;
+ for ( j = 0; j < 4 && k < Start + nBits; j++, k++ )
+ Digit += (1 << j) * Vec_IntEntry(vAssign, k);
+ assert( Digit >= 0 && Digit < 16 );
+ if ( Digit >= 0 && Digit <= 9 )
+ Vec_StrPush( vNum, (char)('0' + Digit) );
+ else
+ Vec_StrPush( vNum, (char)('a' + Digit - 10) );
+ }
+ Vec_StrPush( vNum, 'x' );
+ Vec_StrPush( vNum, '#' );
+ Vec_StrReverseOrder( vNum );
+ Vec_StrPush( vNum, '\0' );
+ printf( "((%s %s))\n", Abc_NamStr(p->pManName, Name), Vec_StrArray(vNum) );
+ }
+ Vec_StrFree( vNum );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c
index 52d5e887..3a249ec6 100644
--- a/src/base/wlc/wlcReadSmt.c
+++ b/src/base/wlc/wlcReadSmt.c
@@ -32,7 +32,8 @@ typedef enum {
PRS_SMT_INPUT,
PRS_SMT_CONST,
PRS_SMT_LET,
- PRS_SMT_ASSERT
+ PRS_SMT_ASSERT,
+ PRS_SMT_VALUE
} Prs_ManType_t;
// parser
@@ -46,7 +47,8 @@ struct Prs_Smt_t_
char * pCur; // current position
Abc_Nam_t * pStrs; // string manager
// network structure
- Vec_Int_t vData;
+ Vec_Int_t vData;
+ Vec_Int_t vValues;
// error handling
char ErrorStr[1000];
};
@@ -117,6 +119,7 @@ static inline void Prs_SmtFree( Prs_Smt_t * p )
if ( p->pStrs )
Abc_NamDeref( p->pStrs );
Vec_IntErase( &p->vData );
+ Vec_IntErase( &p->vValues );
ABC_FREE( p );
}
@@ -234,8 +237,24 @@ static inline int Prs_SmtParseFun( Prs_Smt_t * p, char * pLimit, int Type )
p->pCur = pLimit;
return 1;
}
+static inline int Prs_SmtParseValue( Prs_Smt_t * p, char * pLimit, int Type )
+{
+ char * pToken;
+ assert( *pLimit == ')' );
+ *pLimit = 0;
+ pToken = strtok( p->pCur, " ()" );
+ assert( pToken != NULL );
+ Vec_IntPush( &p->vValues, Abc_NamStrFindOrAdd(p->pStrs, pToken, NULL) );
+ pToken = strtok( NULL, " ()" );
+ assert( pToken == NULL );
+ assert( *pLimit == 0 );
+ *pLimit = ')';
+ p->pCur = pLimit;
+ return 1;
+}
int Prs_SmtReadLines( Prs_Smt_t * p )
{
+ int fAssert = 0;
Prs_SmtSkipSpaces( p );
while ( *p->pCur == '(' )
{
@@ -263,25 +282,35 @@ int Prs_SmtReadLines( Prs_Smt_t * p )
assert( *p->pCur == ')' );
p->pCur++;
}
- else if ( Prs_SmtIsWord(p, "check-sat") )
+ else if ( Prs_SmtIsWord(p, "get-value") )
{
- Vec_IntPush( &p->vData, 0 );
- return 1;
+ if ( !Prs_SmtParseValue( p, Prs_SmtFindNextPar(p), PRS_SMT_VALUE ) )
+ return 0;
+ assert( *p->pCur == ')' );
+ p->pCur++;
}
else if ( Prs_SmtIsWord(p, "assert") )
- {}
- else if ( Prs_SmtIsWord(p, "set-option") || Prs_SmtIsWord(p, "set-logic") )
+ fAssert = 1;
+ else if ( Prs_SmtIsWord(p, "set-option") || Prs_SmtIsWord(p, "set-logic") || Prs_SmtIsWord(p, "check-sat") )
p->pCur = Prs_SmtFindNextPar(p) + 1;
- else
- break;
+// else
//return Prs_SmtErrorSet(p, "Unsupported directive.", 0);
Prs_SmtSkipSpaces( p );
+ if ( *p->pCur != '(' && fAssert == 1 )
+ {
+ fAssert = 0;
+ // finish parsing assert
+ if ( !Prs_SmtParseLet( p, Prs_SmtFindNextPar(p), PRS_SMT_ASSERT ) )
+ return 0;
+ assert( *p->pCur == ')' );
+ Vec_IntPush( &p->vData, 0 );
+ // skip closing
+ while ( *p->pCur == ')' )
+ p->pCur++;
+ Prs_SmtSkipSpaces( p );
+ }
}
- // finish parsing assert
- if ( !Prs_SmtParseLet( p, Prs_SmtFindNextPar(p), PRS_SMT_ASSERT ) )
- return 0;
- assert( *p->pCur == ')' );
- Vec_IntPush( &p->vData, 0 );
+ assert( fAssert == 0 );
return 1;
}
@@ -320,6 +349,8 @@ void Prs_SmtPrintParser( Prs_Smt_t * p )
}
printf( " %s", Abc_NamStr(p->pStrs, Entry) );
}
+ Vec_IntForEachEntry( &p->vValues, Entry, i )
+ printf( "get-value %s\n", Abc_NamStr(p->pStrs, Entry) );
}
@@ -404,9 +435,9 @@ static inline int Prs_SmtReadName( Wlc_Ntk_t * pNtk, char * pStr, int nBits, Vec
return 1;
}
}
-static inline int Prs_SmtStrToType( char * pName )
+static inline int Prs_SmtStrToType( char * pName, int * pfSigned )
{
- int Type = 0;
+ int Type = 0; *pfSigned = 0;
if ( !strcmp(pName, "ite") )
Type = WLC_OBJ_MUX; // 08: multiplexer
else if ( !strcmp(pName, "bvlshr") )
@@ -436,56 +467,77 @@ static inline int Prs_SmtStrToType( char * pName )
else if ( !strcmp(pName, "zero_extend") )
Type = WLC_OBJ_BIT_ZEROPAD; // 21: zero padding
else if ( !strcmp(pName, "sign_extend") )
- Type = WLC_OBJ_BIT_SIGNEXT; // 22: sign extension
+ Type = WLC_OBJ_BIT_SIGNEXT, *pfSigned = 1; // 22: sign extension
else if ( !strcmp(pName, "not") )
Type = WLC_OBJ_LOGIC_NOT; // 23: logic NOT
else if ( !strcmp(pName, "and") )
Type = WLC_OBJ_LOGIC_AND; // 24: logic AND
else if ( !strcmp(pName, "or") )
Type = WLC_OBJ_LOGIC_OR; // 25: logic OR
+ else if ( !strcmp(pName, "xor") )
+ Type = WLC_OBJ_LOGIC_XOR; // 26: logic OR
else if ( !strcmp(pName, "bvcomp") )
- Type = WLC_OBJ_COMP_EQU; // 26: compare equal
+ Type = WLC_OBJ_COMP_EQU; // 27: compare equal
// else if ( !strcmp(pName, "") )
-// Type = WLC_OBJ_COMP_NOTEQU; // 27: compare not equal
+// Type = WLC_OBJ_COMP_NOTEQU; // 28: compare not equal
else if ( !strcmp(pName, "bvult") )
- Type = WLC_OBJ_COMP_LESS; // 28: compare less
+ Type = WLC_OBJ_COMP_LESS; // 29: compare less
else if ( !strcmp(pName, "bvugt") )
- Type = WLC_OBJ_COMP_MORE; // 29: compare more
+ Type = WLC_OBJ_COMP_MORE; // 30: compare more
else if ( !strcmp(pName, "bvule") )
- Type = WLC_OBJ_COMP_LESSEQU; // 30: compare less or equal
+ Type = WLC_OBJ_COMP_LESSEQU; // 31: compare less or equal
else if ( !strcmp(pName, "bvuge") )
- Type = WLC_OBJ_COMP_MOREEQU; // 31: compare more or equal
+ Type = WLC_OBJ_COMP_MOREEQU; // 32: compare more or equal
+ else if ( !strcmp(pName, "bvslt") )
+ Type = WLC_OBJ_COMP_LESS, *pfSigned = 1; // 29: compare less
+ else if ( !strcmp(pName, "bvsgt") )
+ Type = WLC_OBJ_COMP_MORE, *pfSigned = 1; // 30: compare more
+ else if ( !strcmp(pName, "bvsle") )
+ Type = WLC_OBJ_COMP_LESSEQU, *pfSigned = 1; // 31: compare less or equal
+ else if ( !strcmp(pName, "bvsge") )
+ Type = WLC_OBJ_COMP_MOREEQU, *pfSigned = 1; // 32: compare more or equal
else if ( !strcmp(pName, "bvredand") )
- Type = WLC_OBJ_REDUCT_AND; // 32: reduction AND
+ Type = WLC_OBJ_REDUCT_AND; // 33: reduction AND
else if ( !strcmp(pName, "bvredor") )
- Type = WLC_OBJ_REDUCT_OR; // 33: reduction OR
+ Type = WLC_OBJ_REDUCT_OR; // 34: reduction OR
else if ( !strcmp(pName, "bvredxor") )
- Type = WLC_OBJ_REDUCT_XOR; // 34: reduction XOR
+ Type = WLC_OBJ_REDUCT_XOR; // 35: reduction XOR
else if ( !strcmp(pName, "bvadd") )
- Type = WLC_OBJ_ARI_ADD; // 35: arithmetic addition
+ Type = WLC_OBJ_ARI_ADD; // 36: arithmetic addition
else if ( !strcmp(pName, "bvsub") )
- Type = WLC_OBJ_ARI_SUB; // 36: arithmetic subtraction
+ Type = WLC_OBJ_ARI_SUB; // 37: arithmetic subtraction
else if ( !strcmp(pName, "bvmul") )
- Type = WLC_OBJ_ARI_MULTI; // 37: arithmetic multiplier
- else if ( !strcmp(pName, "bvdiv") )
- Type = WLC_OBJ_ARI_DIVIDE; // 38: arithmetic division
+ Type = WLC_OBJ_ARI_MULTI; // 38: arithmetic multiplier
+ else if ( !strcmp(pName, "bvudiv") )
+ Type = WLC_OBJ_ARI_DIVIDE; // 39: arithmetic division
else if ( !strcmp(pName, "bvurem") )
- Type = WLC_OBJ_ARI_MODULUS; // 39: arithmetic modulus
+ Type = WLC_OBJ_ARI_MODULUS; // 40: arithmetic modulus
+ else if ( !strcmp(pName, "bvsdiv") )
+ Type = WLC_OBJ_ARI_DIVIDE, *pfSigned = 1; // 39: arithmetic division
+ else if ( !strcmp(pName, "bvsrem") )
+ Type = WLC_OBJ_ARI_MODULUS, *pfSigned = 1; // 40: arithmetic modulus
+ else if ( !strcmp(pName, "bvsmod") )
+ Type = WLC_OBJ_ARI_MODULUS, *pfSigned = 1; // 40: arithmetic modulus
// else if ( !strcmp(pName, "") )
-// Type = WLC_OBJ_ARI_POWER; // 40: arithmetic power
+// Type = WLC_OBJ_ARI_POWER; // 41: arithmetic power
else if ( !strcmp(pName, "bvneg") )
- Type = WLC_OBJ_ARI_MINUS; // 41: arithmetic minus
+ Type = WLC_OBJ_ARI_MINUS; // 42: arithmetic minus
// else if ( !strcmp(pName, "") )
-// Type = WLC_OBJ_TABLE; // 42: bit table
- else assert( 0 );
+// Type = WLC_OBJ_TABLE; // 43: bit table
+ else
+ {
+ printf( "The following operations is currently not supported (%s)\n", pName );
+ fflush( stdout );
+ assert( 0 );
+ }
return Type;
}
-static inline int Prs_SmtReadNode( Prs_Smt_t * p, Wlc_Ntk_t * pNtk, Vec_Int_t * vData, int i, Vec_Int_t * vFanins, int * pRange )
+static inline int Prs_SmtReadNode( Prs_Smt_t * p, Wlc_Ntk_t * pNtk, Vec_Int_t * vData, int i, Vec_Int_t * vFanins, int * pRange, int * pfSigned )
{
int Type, NameId;
char * pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, i) );
// read type
- Type = Prs_SmtStrToType( pName );
+ Type = Prs_SmtStrToType( pName, pfSigned );
if ( Type == 0 )
return 0;
*pRange = 0;
@@ -499,7 +551,7 @@ static inline int Prs_SmtReadNode( Prs_Smt_t * p, Wlc_Ntk_t * pNtk, Vec_Int_t *
}
else if ( Type == WLC_OBJ_LOGIC_NOT )
{
- pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) );
+ pName = Abc_NamStr( p->pStrs, Vec_IntEntry(vData, ++i) );
if ( !strcmp(pName, "bvcomp") )
{
*pRange = 1;
@@ -558,7 +610,7 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p )
Wlc_Ntk_t * pNtk;
char * pName, * pBits, * pConst;
Vec_Int_t * vFanins = Vec_IntAlloc( 100 );
- int i, iObj, Type, Entry, NameId, fFound, Range;
+ int i, k, iObj, Type, Entry, NameId, fFound, Range, fSigned, nBits = 0;
// start network and create primary inputs
pNtk = Wlc_NtkAlloc( p->pName, Vec_IntCountEntry(&p->vData, 0) + 100 );
pNtk->pManName = Abc_NamStart( 1000, 24 );
@@ -567,12 +619,23 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p )
assert( Vec_IntEntry(&p->vData, i) == 0 );
if ( Vec_IntEntry(&p->vData, ++i) == PRS_SMT_INPUT )
{
+ int NameOld = Vec_IntEntry(&p->vData, i+1);
pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
pBits = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
iObj = Wlc_ObjAlloc( pNtk, WLC_OBJ_PI, 0, atoi(pBits)-1, 0 );
NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
assert( !fFound );
assert( iObj == NameId );
+ // save values
+ Vec_IntForEachEntry( &p->vValues, Entry, k )
+ if ( Entry == NameOld )
+ {
+ Vec_IntPush( &pNtk->vValues, NameId );
+ Vec_IntPush( &pNtk->vValues, nBits );
+ Vec_IntPush( &pNtk->vValues, atoi(pBits) );
+ break;
+ }
+ nBits += atoi(pBits);
}
while ( Vec_IntEntry(&p->vData, ++i) );
}
@@ -595,13 +658,21 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p )
else if ( Entry == PRS_SMT_LET )
{
pName = Abc_NamStr( p->pStrs, Vec_IntEntry(&p->vData, ++i) );
- Type = Prs_SmtReadNode( p, pNtk, &p->vData, ++i, vFanins, &Range );
+ Type = Prs_SmtReadNode( p, pNtk, &p->vData, ++i, vFanins, &Range, &fSigned );
if ( Type == WLC_OBJ_NONE )
return NULL;
assert( Range > 0 );
// create new node
iObj = Wlc_ObjAlloc( pNtk, Type, 0, Range-1, 0 );
Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins );
+ if ( fSigned )
+ {
+ Wlc_NtkObj(pNtk, iObj)->Signed = fSigned;
+ if ( Vec_IntSize(vFanins) > 0 )
+ Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 0))->Signed = fSigned;
+ if ( Vec_IntSize(vFanins) > 1 )
+ Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 1))->Signed = fSigned;
+ }
// add node's name
NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
assert( !fFound );
@@ -648,6 +719,7 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p )
vFanins = Vec_IntStartNatural( Wlc_NtkObjNumMax(pNtk) );
Vec_IntAppend( &pNtk->vNameIds, vFanins );
Vec_IntFree( vFanins );
+ //Wlc_NtkReport( pNtk, NULL );
return pNtk;
}
Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit )
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 19:19:37 +0000