Merged alanmi/abc into default

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 :