summaryrefslogtreecommitdiffstats
path: root/src/misc/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/misc/util')
-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
5 files changed, 487 insertions, 10 deletions
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 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-28 11:50:29 +0000