summaryrefslogtreecommitdiffstats
path: root/src/misc
diff options
context:
space:
mode:
Diffstat (limited to 'src/misc')
-rw-r--r--src/misc/extra/extraUtilUtil.c54
-rw-r--r--src/misc/util/abc_global.h2
-rw-r--r--src/misc/util/utilCex.c25
-rw-r--r--src/misc/util/utilDouble.h222
-rw-r--r--src/misc/util/utilFloat.h226
-rw-r--r--src/misc/util/utilTruth.h22
-rw-r--r--src/misc/vec/vecInt.h18
-rw-r--r--src/misc/vec/vecPtr.h2
-rw-r--r--src/misc/vec/vecWec.h29
-rw-r--r--src/misc/zlib/inflate.c2
10 files changed, 568 insertions, 34 deletions
diff --git a/src/misc/extra/extraUtilUtil.c b/src/misc/extra/extraUtilUtil.c
index 253d9e3c..2f0f4559 100644
--- a/src/misc/extra/extraUtilUtil.c
+++ b/src/misc/extra/extraUtilUtil.c
@@ -102,35 +102,45 @@ int Extra_UtilGetopt( int argc, char *argv[], const char *optstring )
globalUtilOptarg = NULL;
- if (pScanStr == NULL || *pScanStr == '\0') {
- if (globalUtilOptind == 0) globalUtilOptind++;
- if (globalUtilOptind >= argc) return EOF;
- place = argv[globalUtilOptind];
- if (place[0] != '-' || place[1] == '\0') return EOF;
- globalUtilOptind++;
- if (place[1] == '-' && place[2] == '\0') return EOF;
- pScanStr = place+1;
+ if (pScanStr == NULL || *pScanStr == '\0')
+ {
+ if (globalUtilOptind == 0)
+ globalUtilOptind++;
+ if (globalUtilOptind >= argc)
+ return EOF;
+ place = argv[globalUtilOptind];
+ if (place[0] != '-' || place[1] == '\0')
+ return EOF;
+ globalUtilOptind++;
+ if (place[1] == '-' && place[2] == '\0')
+ return EOF;
+ pScanStr = place+1;
}
c = *pScanStr++;
place = strchr(optstring, c);
if (place == NULL || c == ':') {
- (void) fprintf(stderr, "%s: unknown option %c\n", argv[0], c);
- return '?';
- }
- if (*++place == ':') {
- if (*pScanStr != '\0') {
- globalUtilOptarg = pScanStr;
- pScanStr = NULL;
- } else {
- if (globalUtilOptind >= argc) {
- (void) fprintf(stderr, "%s: %c requires an argument\n",
- argv[0], c);
+ (void) fprintf(stderr, "%s: unknown option %c\n", argv[0], c);
return '?';
- }
- globalUtilOptarg = argv[globalUtilOptind];
- globalUtilOptind++;
}
+ if (*++place == ':')
+ {
+ if (*pScanStr != '\0')
+ {
+ globalUtilOptarg = pScanStr;
+ pScanStr = NULL;
+ }
+ else
+ {
+ if (globalUtilOptind >= argc)
+ {
+ (void) fprintf(stderr, "%s: %c requires an argument\n",
+ argv[0], c);
+ return '?';
+ }
+ globalUtilOptarg = argv[globalUtilOptind];
+ globalUtilOptind++;
+ }
}
return c;
}
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index 00d5d514..9e906816 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -225,6 +225,8 @@ static inline double Abc_MinDouble( double a, double b ) { return a < b ?
static inline int Abc_Float2Int( float Val ) { union { int x; float y; } v; v.y = Val; return v.x; }
static inline float Abc_Int2Float( int Num ) { union { int x; float y; } v; v.x = Num; return v.y; }
+static inline word Abc_Dbl2Word( double Dbl ) { union { word x; double y; } v; v.y = Dbl; return v.x; }
+static inline double Abc_Word2Dbl( word Num ) { union { word x; double y; } v; v.x = Num; return v.y; }
static inline int Abc_Base2Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ) {}; return r; }
static inline int Abc_Base10Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ) {}; return r; }
static inline int Abc_Base16Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 16, r++ ) {}; return r; }
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
index 3acd7f77..59107dc9 100644
--- a/src/misc/util/utilCex.c
+++ b/src/misc/util/utilCex.c
@@ -272,9 +272,9 @@ void Abc_CexPrintStats( Abc_Cex_t * p )
p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits,
Counter, 100.0 * Counter / (p->nBits - p->nRegs) );
}
-void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs )
+void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nRealPis )
{
- int k, Counter = 0, Counter2 = 0;
+ int k, Counter = 0, CounterPi = 0, CounterPpi = 0;
if ( p == NULL )
{
printf( "The counter example is NULL.\n" );
@@ -285,16 +285,27 @@ void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs )
printf( "The counter example is present but not available (pointer has value \"1\").\n" );
return;
}
+ assert( nRealPis <= p->nPis );
for ( k = 0; k < p->nBits; k++ )
{
Counter += Abc_InfoHasBit(p->pData, k);
- if ( (k - p->nRegs) % p->nPis < nInputs )
- Counter2 += Abc_InfoHasBit(p->pData, k);
+ if ( nRealPis == p->nPis )
+ continue;
+ if ( (k - p->nRegs) % p->nPis < nRealPis )
+ CounterPi += Abc_InfoHasBit(p->pData, k);
+ else
+ CounterPpi += Abc_InfoHasBit(p->pData, k);
}
- printf( "CEX: Po =%4d Frame =%4d FF = %d PI = %d Bit =%8d 1s =%8d (%5.2f %%) 1sIn =%8d (%5.2f %%)\n",
+ printf( "CEX: Po =%4d Fr =%4d FF = %d PI = %d Bit =%7d 1 =%8d (%5.2f %%)",
p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits,
- Counter, 100.0 * Counter / (p->nBits - p->nRegs),
- Counter2, 100.0 * Counter2 / (p->nBits - p->nRegs - (p->iFrame + 1) * (p->nPis - nInputs)) );
+ Counter, 100.0 * Counter / ((p->iFrame + 1) * p->nPis ) );
+ if ( nRealPis < p->nPis )
+ {
+ printf( " 1pi =%8d (%5.2f %%) 1ppi =%8d (%5.2f %%)",
+ CounterPi, 100.0 * CounterPi / ((p->iFrame + 1) * nRealPis ),
+ CounterPpi, 100.0 * CounterPpi / ((p->iFrame + 1) * (p->nPis - nRealPis)) );
+ }
+ printf( "\n" );
}
/**Function*************************************************************
diff --git a/src/misc/util/utilDouble.h b/src/misc/util/utilDouble.h
new file mode 100644
index 00000000..0d023781
--- /dev/null
+++ b/src/misc/util/utilDouble.h
@@ -0,0 +1,222 @@
+/**CFile****************************************************************
+
+ FileName [utilDouble.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName []
+
+ Synopsis [Double floating point number implementation.]
+
+ Author [Alan Mishchenko, Bruno Schmitt]
+
+ Affiliation [UC Berkeley / UFRGS]
+
+ Date [Ver. 1.0. Started - February 11, 2017.]
+
+ Revision []
+
+***********************************************************************/
+
+#ifndef ABC__sat__Xdbl__Xdbl_h
+#define ABC__sat__Xdbl__Xdbl_h
+
+#include "misc/util/abc_global.h"
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+/// STRUCTURE DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*
+ The xdbl floating-point number is represented as a 64-bit unsigned int.
+ The number is (2^Exp)*Mnt, where Exp is a 16-bit exponent and Mnt is a
+ 48-bit mantissa. The decimal point is located between the MSB of Mnt,
+ which is always 1, and the remaining 15 digits of Mnt.
+
+ Currently, only positive numbers are represented.
+
+ The range of possible values is [1.0; 2^(2^16-1)*1.111111111111111]
+ that is, the smallest possible number is 1.0 and the largest possible
+ number is 2^(---16 ones---).(1.---47 ones---)
+
+ Comparison of numbers can be done by comparing the underlying unsigned ints.
+
+ Only addition, multiplication, and division by 2^n are currently implemented.
+*/
+
+typedef word xdbl;
+
+static inline word Xdbl_Exp( xdbl a ) { return a >> 48; }
+static inline word Xdbl_Mnt( xdbl a ) { return (a << 16) >> 16; }
+
+static inline xdbl Xdbl_Create( word Exp, word Mnt ) { assert(!(Exp>>16) && (Mnt>>47)==(word)1); return (Exp<<48) | Mnt; }
+
+static inline xdbl Xdbl_Const1() { return Xdbl_Create( (word)0, (word)1 << 47 ); }
+static inline xdbl Xdbl_Const2() { return Xdbl_Create( (word)1, (word)1 << 47 ); }
+static inline xdbl Xdbl_Const3() { return Xdbl_Create( (word)1, (word)3 << 46 ); }
+static inline xdbl Xdbl_Const12() { return Xdbl_Create( (word)3, (word)3 << 46 ); }
+static inline xdbl Xdbl_Const1point5() { return Xdbl_Create( (word)0, (word)3 << 46 ); }
+static inline xdbl Xdbl_Const2point5() { return Xdbl_Create( (word)1, (word)5 << 45 ); }
+static inline xdbl Xdbl_Maximum() { return ~(word)0; }
+
+static inline double Xdbl_ToDouble( xdbl a ) { assert(Xdbl_Exp(a) < 1023); return Abc_Word2Dbl(((Xdbl_Exp(a) + 1023) << 52) | (((a<<17)>>17) << 5)); }
+static inline xdbl Xdbl_FromDouble( double a ) { word A = Abc_Dbl2Word(a); assert(a >= 1.0); return Xdbl_Create((A >> 52)-1023, (((word)1) << 47) | ((A << 12) >> 17)); }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Adding two floating-point numbers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline xdbl Xdbl_Add( xdbl a, xdbl b )
+{
+ word Exp, Mnt;
+ if ( a < b ) a ^= b, b ^= a, a ^= b;
+ assert( a >= b );
+ Mnt = Xdbl_Mnt(a) + (Xdbl_Mnt(b) >> (Xdbl_Exp(a) - Xdbl_Exp(b)));
+ Exp = Xdbl_Exp(a);
+ if ( Mnt >> 48 ) // new MSB is created
+ Exp++, Mnt >>= 1;
+ if ( Exp >> 16 ) // overflow
+ return Xdbl_Maximum();
+ return Xdbl_Create( Exp, Mnt );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Multiplying two floating-point numbers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline xdbl Xdbl_Mul( xdbl a, xdbl b )
+{
+ word Exp, Mnt, MntA, MntB, MntAh, MntBh, MntAl, MntBl;
+ if ( a < b ) a ^= b, b ^= a, a ^= b;
+ assert( a >= b );
+ MntA = Xdbl_Mnt(a);
+ MntB = Xdbl_Mnt(b);
+ MntAh = MntA>>32;
+ MntBh = MntB>>32;
+ MntAl = (MntA<<32)>>32;
+ MntBl = (MntB<<32)>>32;
+ Mnt = ((MntAh * MntBh) << 17) + ((MntAl * MntBl) >> 47) + ((MntAl * MntBh) >> 15) + ((MntAh * MntBl) >> 15);
+ Exp = Xdbl_Exp(a) + Xdbl_Exp(b);
+ if ( Mnt >> 48 ) // new MSB is created
+ Exp++, Mnt >>= 1;
+ if ( Exp >> 16 ) // overflow
+ return Xdbl_Maximum();
+ return Xdbl_Create( Exp, Mnt );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Dividing floating point number by a degree of 2.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline xdbl Xdbl_Div( xdbl a, unsigned Deg2 )
+{
+ if ( Xdbl_Exp(a) >= (word)Deg2 )
+ return Xdbl_Create( Xdbl_Exp(a) - Deg2, Xdbl_Mnt(a) );
+ return Xdbl_Const1(); // underflow
+}
+
+/**Function*************************************************************
+
+ Synopsis [Testing procedure.]
+
+ Description [Helpful link https://www.h-schmidt.net/FloatConverter/IEEE754.html]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Xdbl_Test()
+{
+ xdbl c1 = Xdbl_Const1();
+ xdbl c2 = Xdbl_Const2();
+ xdbl c3 = Xdbl_Const3();
+ xdbl c12 = Xdbl_Const12();
+ xdbl c1p5 = Xdbl_Const1point5();
+ xdbl c2p5 = Xdbl_Const2point5();
+
+ xdbl c1_ = Xdbl_FromDouble(1.0);
+ xdbl c2_ = Xdbl_FromDouble(2.0);
+ xdbl c3_ = Xdbl_FromDouble(3.0);
+ xdbl c12_ = Xdbl_FromDouble(12.0);
+ xdbl c1p5_ = Xdbl_FromDouble(1.5);
+ xdbl c2p5_ = Xdbl_FromDouble(2.5);
+
+ xdbl sum1 = Xdbl_Add(c1, c1p5);
+ xdbl mul1 = Xdbl_Mul(c2, c1p5);
+
+ xdbl sum2 = Xdbl_Add(c1p5, c2p5);
+ xdbl mul2 = Xdbl_Mul(c1p5, c2p5);
+
+ xdbl a = Xdbl_FromDouble(1.2929725);
+ xdbl b = Xdbl_FromDouble(10.28828287);
+ xdbl ab = Xdbl_Mul(a, b);
+
+ xdbl ten100 = Xdbl_FromDouble( 1e100 );
+ xdbl ten100_ = ABC_CONST(0x014c924d692ca61b);
+
+ assert( ten100 == ten100_ );
+
+// float f1 = Xdbl_ToDouble(c1);
+// Extra_PrintBinary( stdout, (int *)&c1, 32 ); printf( "\n" );
+// Extra_PrintBinary( stdout, (int *)&f1, 32 ); printf( "\n" );
+
+ printf( "1 = %lf\n", Xdbl_ToDouble(c1) );
+ printf( "2 = %lf\n", Xdbl_ToDouble(c2) );
+ printf( "3 = %lf\n", Xdbl_ToDouble(c3) );
+ printf( "12 = %lf\n", Xdbl_ToDouble(c12) );
+ printf( "1.5 = %lf\n", Xdbl_ToDouble(c1p5) );
+ printf( "2.5 = %lf\n", Xdbl_ToDouble(c2p5) );
+
+ printf( "Converted 1 = %lf\n", Xdbl_ToDouble(c1_) );
+ printf( "Converted 2 = %lf\n", Xdbl_ToDouble(c2_) );
+ printf( "Converted 3 = %lf\n", Xdbl_ToDouble(c3_) );
+ printf( "Converted 12 = %lf\n", Xdbl_ToDouble(c12_) );
+ printf( "Converted 1.5 = %lf\n", Xdbl_ToDouble(c1p5_) );
+ printf( "Converted 2.5 = %lf\n", Xdbl_ToDouble(c2p5_) );
+
+ printf( "1.0 + 1.5 = %lf\n", Xdbl_ToDouble(sum1) );
+ printf( "2.0 * 1.5 = %lf\n", Xdbl_ToDouble(mul1) );
+
+ printf( "1.5 + 2.5 = %lf\n", Xdbl_ToDouble(sum2) );
+ printf( "1.5 * 2.5 = %lf\n", Xdbl_ToDouble(mul2) );
+ printf( "12 / 2^2 = %lf\n", Xdbl_ToDouble(Xdbl_Div(c12, 2)) );
+
+ printf( "12 / 2^2 = %lf\n", Xdbl_ToDouble(Xdbl_Div(c12, 2)) );
+
+ printf( "%.16lf * %.16lf = %.16lf (%.16lf)\n", Xdbl_ToDouble(a), Xdbl_ToDouble(b), Xdbl_ToDouble(ab), 1.2929725 * 10.28828287 );
+
+ assert( sum1 == c2p5 );
+ assert( mul1 == c3 );
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
diff --git a/src/misc/util/utilFloat.h b/src/misc/util/utilFloat.h
new file mode 100644
index 00000000..f0739a92
--- /dev/null
+++ b/src/misc/util/utilFloat.h
@@ -0,0 +1,226 @@
+/**CFile****************************************************************
+
+ FileName [utilFloat.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName []
+
+ Synopsis [Floating point number implementation.]
+
+ Author [Alan Mishchenko, Bruno Schmitt]
+
+ Affiliation [UC Berkeley / UFRGS]
+
+ Date [Ver. 1.0. Started - January 28, 2017.]
+
+ Revision []
+
+***********************************************************************/
+#ifndef ABC__sat__xSAT__xsatFloat_h
+#define ABC__sat__xSAT__xsatFloat_h
+
+#include "misc/util/abc_global.h"
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+/// STRUCTURE DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/*
+ The xFloat_t floating-point number is represented as a 32-bit unsigned int.
+ The number is (2^Exp)*Mnt, where Exp is a 16-bit exponent and Mnt is a
+ 16-bit mantissa. The decimal point is located between the MSB of Mnt,
+ which is always 1, and the remaining 15 digits of Mnt.
+
+ Currently, only positive numbers are represented.
+
+ The range of possible values is [1.0; 2^(2^16-1)*1.111111111111111]
+ that is, the smallest possible number is 1.0 and the largest possible
+ number is 2^(---16 ones---).(1.---15 ones---)
+
+ Comparison of numbers can be done by comparing the underlying unsigned ints.
+
+ Only addition, multiplication, and division by 2^n are currently implemented.
+*/
+
+typedef struct xFloat_t_ xFloat_t;
+struct xFloat_t_
+{
+ unsigned Mnt : 16;
+ unsigned Exp : 16;
+};
+
+static inline unsigned xSat_Float2Uint( xFloat_t f ) { union { xFloat_t f; unsigned u; } temp; temp.f = f; return temp.u; }
+static inline xFloat_t xSat_Uint2Float( unsigned u ) { union { xFloat_t f; unsigned u; } temp; temp.u = u; return temp.f; }
+static inline int xSat_LessThan( xFloat_t a, xFloat_t b ) { return a.Exp < b.Exp || (a.Exp == b.Exp && a.Mnt < b.Mnt); }
+static inline int xSat_Equal( xFloat_t a, xFloat_t b ) { return a.Exp == b.Exp && a.Mnt == b.Mnt; }
+
+static inline xFloat_t xSat_FloatCreate( unsigned Exp, unsigned Mnt ) { xFloat_t res; res.Exp = Exp; res.Mnt = Mnt; return res; }
+
+static inline xFloat_t xSat_FloatCreateConst1() { return xSat_FloatCreate( 0, 1 << 15 ); }
+static inline xFloat_t xSat_FloatCreateConst2() { return xSat_FloatCreate( 1, 1 << 15 ); }
+static inline xFloat_t xSat_FloatCreateConst3() { return xSat_FloatCreate( 1, 3 << 14 ); }
+static inline xFloat_t xSat_FloatCreateConst12() { return xSat_FloatCreate( 3, 3 << 14 ); }
+static inline xFloat_t xSat_FloatCreateConst1point5() { return xSat_FloatCreate( 0, 3 << 14 ); }
+static inline xFloat_t xSat_FloatCreateConst2point5() { return xSat_FloatCreate( 1, 5 << 13 ); }
+static inline xFloat_t xSat_FloatCreateMaximum() { return xSat_Uint2Float( 0xFFFFFFFF ); }
+
+static inline float xSat_Float2Float( xFloat_t a ) { assert(a.Exp < 127); return Abc_Int2Float(((a.Exp + 127) << 23) | ((a.Mnt & 0x7FFF) << 8)); }
+static inline xFloat_t xSat_FloatFromFloat( float a ) { int A = Abc_Float2Int(a); assert(a >= 1.0); return xSat_FloatCreate((A >> 23)-127, 0x8000 | ((A >> 8) & 0x7FFF)); }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Adding two floating-point numbers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline xFloat_t xSat_FloatAdd( xFloat_t a, xFloat_t b )
+{
+ unsigned Exp, Mnt;
+ if ( a.Exp < b.Exp )
+ return xSat_FloatAdd(b, a);
+ assert( a.Exp >= b.Exp );
+ // compute new mantissa
+ Mnt = a.Mnt + (b.Mnt >> (a.Exp - b.Exp));
+ // compute new exponent
+ Exp = a.Exp;
+ // update exponent and mantissa if new MSB is created
+ if ( Mnt & 0xFFFF0000 ) // new MSB bit is created
+ Exp++, Mnt >>= 1;
+ // check overflow
+ if ( Exp & 0xFFFF0000 ) // overflow
+ return xSat_Uint2Float( 0xFFFFFFFF );
+ assert( (Exp & 0xFFFF0000) == 0 );
+ assert( (Mnt & 0xFFFF0000) == 0 );
+ assert( Mnt & 0x00008000 );
+ return xSat_FloatCreate( Exp, Mnt );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Multiplying two floating-point numbers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline xFloat_t xSat_FloatMul( xFloat_t a, xFloat_t b )
+{
+ unsigned Exp, Mnt;
+ if ( a.Exp < b.Exp )
+ return xSat_FloatMul(b, a);
+ assert( a.Exp >= b.Exp );
+ // compute new mantissa
+ Mnt = (a.Mnt * b.Mnt) >> 15;
+ // compute new exponent
+ Exp = a.Exp + b.Exp;
+ // update exponent and mantissa if new MSB is created
+ if ( Mnt & 0xFFFF0000 ) // new MSB bit is created
+ Exp++, Mnt >>= 1;
+ // check overflow
+ if ( Exp & 0xFFFF0000 ) // overflow
+ return xSat_Uint2Float( 0xFFFFFFFF );
+ assert( (Exp & 0xFFFF0000) == 0 );
+ assert( (Mnt & 0xFFFF0000) == 0 );
+ assert( Mnt & 0x00008000 );
+ return xSat_FloatCreate( Exp, Mnt );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Dividing floating point number by a degree of 2.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline xFloat_t xSat_FloatDiv( xFloat_t a, unsigned Deg2 )
+{
+ assert( Deg2 < 0xFFFF );
+ if ( a.Exp >= Deg2 )
+ return xSat_FloatCreate( a.Exp - Deg2, a.Mnt );
+ return xSat_FloatCreateConst1(); // underflow
+}
+
+/**Function*************************************************************
+
+ Synopsis [Testing procedure.]
+
+ Description [Helpful link https://www.h-schmidt.net/FloatConverter/IEEE754.html]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void xSat_FloatTest()
+{
+ xFloat_t c1 = xSat_FloatCreateConst1();
+ xFloat_t c2 = xSat_FloatCreateConst2();
+ xFloat_t c3 = xSat_FloatCreateConst3();
+ xFloat_t c12 = xSat_FloatCreateConst12();
+ xFloat_t c1p5 = xSat_FloatCreateConst1point5();
+ xFloat_t c2p5 = xSat_FloatCreateConst2point5();
+
+ xFloat_t c1_ = xSat_FloatFromFloat(1.0);
+ xFloat_t c2_ = xSat_FloatFromFloat(2.0);
+ xFloat_t c3_ = xSat_FloatFromFloat(3.0);
+ xFloat_t c12_ = xSat_FloatFromFloat(12.0);
+ xFloat_t c1p5_ = xSat_FloatFromFloat(1.5);
+ xFloat_t c2p5_ = xSat_FloatFromFloat(2.5);
+
+ xFloat_t sum1 = xSat_FloatAdd(c1, c1p5);
+ xFloat_t mul1 = xSat_FloatMul(c2, c1p5);
+
+ xFloat_t sum2 = xSat_FloatAdd(c1p5, c2p5);
+ xFloat_t mul2 = xSat_FloatMul(c1p5, c2p5);
+
+// float f1 = xSat_Float2Float(c1);
+// Extra_PrintBinary( stdout, (int *)&c1, 32 ); printf( "\n" );
+// Extra_PrintBinary( stdout, (int *)&f1, 32 ); printf( "\n" );
+
+ printf( "1 = %f\n", xSat_Float2Float(c1) );
+ printf( "2 = %f\n", xSat_Float2Float(c2) );
+ printf( "3 = %f\n", xSat_Float2Float(c3) );
+ printf( "12 = %f\n", xSat_Float2Float(c12) );
+ printf( "1.5 = %f\n", xSat_Float2Float(c1p5) );
+ printf( "2.5 = %f\n", xSat_Float2Float(c2p5) );
+
+ printf( "Converted 1 = %f\n", xSat_Float2Float(c1_) );
+ printf( "Converted 2 = %f\n", xSat_Float2Float(c2_) );
+ printf( "Converted 3 = %f\n", xSat_Float2Float(c3_) );
+ printf( "Converted 12 = %f\n", xSat_Float2Float(c12_) );
+ printf( "Converted 1.5 = %f\n", xSat_Float2Float(c1p5_) );
+ printf( "Converted 2.5 = %f\n", xSat_Float2Float(c2p5_) );
+
+ printf( "1.0 + 1.5 = %f\n", xSat_Float2Float(sum1) );
+ printf( "2.0 * 1.5 = %f\n", xSat_Float2Float(mul1) );
+
+ printf( "1.5 + 2.5 = %f\n", xSat_Float2Float(sum2) );
+ printf( "1.5 * 2.5 = %f\n", xSat_Float2Float(mul2) );
+ printf( "12 / 2^2 = %f\n", xSat_Float2Float(xSat_FloatDiv(c12, 2)) );
+
+ assert( xSat_Equal(sum1, c2p5) );
+ assert( xSat_Equal(mul1, c3) );
+}
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index b8a34da7..e04ffbc9 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -1631,6 +1631,14 @@ static inline int Abc_TtFindFirstBit( word * pIn, int nVars )
return 64*w + Abc_Tt6FirstBit(pIn[w]);
return -1;
}
+static inline int Abc_TtFindFirstBit2( word * pIn, int nWords )
+{
+ int w;
+ for ( w = 0; w < nWords; w++ )
+ if ( pIn[w] )
+ return 64*w + Abc_Tt6FirstBit(pIn[w]);
+ return -1;
+}
static inline int Abc_TtFindFirstDiffBit( word * pIn1, word * pIn2, int nVars )
{
int w, nWords = Abc_TtWordNum(nVars);
@@ -1639,6 +1647,14 @@ static inline int Abc_TtFindFirstDiffBit( word * pIn1, word * pIn2, int nVars )
return 64*w + Abc_Tt6FirstBit(pIn1[w] ^ pIn2[w]);
return -1;
}
+static inline int Abc_TtFindFirstDiffBit2( word * pIn1, word * pIn2, int nWords )
+{
+ int w;
+ for ( w = 0; w < nWords; w++ )
+ if ( pIn1[w] ^ pIn2[w] )
+ return 64*w + Abc_Tt6FirstBit(pIn1[w] ^ pIn2[w]);
+ return -1;
+}
static inline int Abc_TtFindFirstZero( word * pIn, int nVars )
{
int w, nWords = Abc_TtWordNum(nVars);
@@ -2612,7 +2628,7 @@ static inline int Abc_TtProcessBiDec( word * pTruth, int nVars, int nSuppLim )
static inline void Abc_TtProcessBiDecTest( word * pTruth, int nVars, int nSuppLim )
{
word This, That, pTemp[64];
- int Res, resThis, resThat, nThis, nThat;
+ int Res, resThis, resThat;//, nThis, nThat;
int nWords = Abc_TtWordNum(nVars);
Abc_TtCopy( pTemp, pTruth, nWords, 0 );
Res = Abc_TtProcessBiDec( pTemp, nVars, nSuppLim );
@@ -2634,8 +2650,8 @@ static inline void Abc_TtProcessBiDecTest( word * pTruth, int nVars, int nSuppLi
// Dau_DsdPrintFromTruth( pTemp, nVars );
- nThis = Abc_TtBitCount16(resThis);
- nThat = Abc_TtBitCount16(resThat);
+ //nThis = Abc_TtBitCount16(resThis);
+ //nThat = Abc_TtBitCount16(resThat);
printf( "Variable sets: " );
Abc_TtPrintVarSet( resThis, nVars );
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index f09b8783..d952518f 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -1692,6 +1692,24 @@ static inline int Vec_IntTwoFindCommon( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Ve
}
return Vec_IntSize(vArr);
}
+static inline int Vec_IntTwoFindCommonReverse( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vArr )
+{
+ int * pBeg1 = vArr1->pArray;
+ int * pBeg2 = vArr2->pArray;
+ int * pEnd1 = vArr1->pArray + vArr1->nSize;
+ int * pEnd2 = vArr2->pArray + vArr2->nSize;
+ Vec_IntClear( vArr );
+ while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 )
+ {
+ if ( *pBeg1 == *pBeg2 )
+ Vec_IntPush( vArr, *pBeg1 ), pBeg1++, pBeg2++;
+ else if ( *pBeg1 > *pBeg2 )
+ pBeg1++;
+ else
+ pBeg2++;
+ }
+ return Vec_IntSize(vArr);
+}
/**Function*************************************************************
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 5b40665f..015aa1be 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -65,7 +65,7 @@ struct Vec_Ptr_t_
#define Vec_PtrForEachEntryTwo( Type1, vVec1, Type2, vVec2, pEntry1, pEntry2, i ) \
for ( i = 0; (i < Vec_PtrSize(vVec1)) && (((pEntry1) = (Type1)Vec_PtrEntry(vVec1, i)), 1) && (((pEntry2) = (Type2)Vec_PtrEntry(vVec2, i)), 1); i++ )
#define Vec_PtrForEachEntryDouble( Type1, Type2, vVec, Entry1, Entry2, i ) \
- for ( i = 0; (i+1 < Vec_IntSize(vVec)) && (((Entry1) = (Type1)Vec_PtrEntry(vVec, i)), 1) && (((Entry2) = (Type2)Vec_PtrEntry(vVec, i+1)), 1); i += 2 )
+ for ( i = 0; (i+1 < Vec_PtrSize(vVec)) && (((Entry1) = (Type1)Vec_PtrEntry(vVec, i)), 1) && (((Entry2) = (Type2)Vec_PtrEntry(vVec, i+1)), 1); i += 2 )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h
index e4e92503..c8c89701 100644
--- a/src/misc/vec/vecWec.h
+++ b/src/misc/vec/vecWec.h
@@ -303,6 +303,23 @@ static inline Vec_Int_t * Vec_WecPushLevel( Vec_Wec_t * p )
++p->nSize;
return Vec_WecEntryLast( p );
}
+static inline Vec_Int_t * Vec_WecInsertLevel( Vec_Wec_t * p, int i )
+{
+ Vec_Int_t * pTemp;
+ if ( p->nSize == p->nCap )
+ {
+ if ( p->nCap < 16 )
+ Vec_WecGrow( p, 16 );
+ else
+ Vec_WecGrow( p, 2 * p->nCap );
+ }
+ ++p->nSize;
+ assert( i >= 0 && i < p->nSize );
+ for ( pTemp = p->pArray + p->nSize - 2; pTemp >= p->pArray + i; pTemp-- )
+ pTemp[1] = pTemp[0];
+ Vec_IntZero( p->pArray + i );
+ return p->pArray + i;
+}
/**Function*************************************************************
@@ -544,6 +561,18 @@ static inline void Vec_WecPrint( Vec_Wec_t * p, int fSkipSingles )
printf( " }\n" );
}
}
+static inline void Vec_WecPrintLits( Vec_Wec_t * p )
+{
+ Vec_Int_t * vVec;
+ int i, k, iLit;
+ Vec_WecForEachLevel( p, vVec, i )
+ {
+ printf( " %4d : %2d {", i, Vec_IntSize(vVec) );
+ Vec_IntForEachEntry( vVec, iLit, k )
+ printf( " %c%d", Abc_LitIsCompl(iLit) ? '-' : '+', Abc_Lit2Var(iLit) );
+ printf( " }\n" );
+ }
+}
/**Function*************************************************************
diff --git a/src/misc/zlib/inflate.c b/src/misc/zlib/inflate.c
index 449779a9..9fae7045 100644
--- a/src/misc/zlib/inflate.c
+++ b/src/misc/zlib/inflate.c
@@ -1445,7 +1445,7 @@ long ZEXPORT inflateMark(z_streamp strm)
{
struct inflate_state FAR *state;
- if (strm == Z_NULL || strm->state == Z_NULL) return -1L << 16;
+ if (strm == Z_NULL || strm->state == Z_NULL) return -(1L << 16);
state = (struct inflate_state FAR *)strm->state;
return ((long)(state->back) << 16) +
(state->mode == COPY ? state->length :
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-09 03:14:12 +0000