Merged alanmi/abc into default

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 );