Movinng custom floating-point implementations, etc.

5 files changed, 19 insertions, 21 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 85307635..f9cc2f50 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1971,10 +1971,6 @@ SOURCE=.\src\sat\xsat\xsatCnfReader.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\sat\xsat\xsatFloat.h
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\sat\xsat\xsatHeap.h
 # End Source File
 # Begin Source File
@@ -2031,10 +2027,6 @@ SOURCE=.\src\sat\satoko\cnf_reader.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\sat\satoko\utils\fixed.h
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\sat\satoko\utils\heap.h
 # End Source File
 # Begin Source File
@@ -2051,6 +2043,10 @@ SOURCE=.\src\sat\satoko\satoko.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\satoko\utils\sdbl.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\satoko\solver.c
 # End Source File
 # Begin Source File
@@ -2075,10 +2071,6 @@ SOURCE=.\src\sat\satoko\utils\vec\vec_char.h
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\sat\satoko\utils\vec\vec_dble.h
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\sat\satoko\utils\vec\vec_flt.h
 # End Source File
 # Begin Source File
@@ -3659,10 +3651,18 @@ SOURCE=.\src\misc\util\utilColor.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\misc\util\utilDouble.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\misc\util\utilFile.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\misc\util\utilFloat.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\misc\util\utilIsop.c
 # End Source File
 # Begin Source File
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/sat/xsat/xsatDouble.h b/src/misc/util/utilDouble.h
index d90e8c05..0d023781 100644
--- a/src/sat/xsat/xsatDouble.h
+++ b/src/misc/util/utilDouble.h
@@ -1,6 +1,6 @@
 /**CFile****************************************************************
 
-  FileName    [xdouble.h]
+  FileName    [utilDouble.h]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
@@ -46,10 +46,6 @@ ABC_NAMESPACE_HEADER_START
     Only addition, multiplication, and division by 2^n are currently implemented.
 */
 
-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;         }
-
-
 typedef word xdbl;
 
 static inline word   Xdbl_Exp( xdbl a )                 { return a >> 48;           }
diff --git a/src/sat/xsat/xsatFloat.h b/src/misc/util/utilFloat.h
index fb451a94..f0739a92 100644
--- a/src/sat/xsat/xsatFloat.h
+++ b/src/misc/util/utilFloat.h
@@ -1,11 +1,10 @@
 /**CFile****************************************************************
 
-  FileName    [xsatFloat.h]
+  FileName    [utilFloat.h]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [xSAT - A SAT solver written in C.
-               Read the license file for more info.]
+  PackageName []
 
   Synopsis    [Floating point number implementation.]
 
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 226d8c7a..21f24fcb 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -30,7 +30,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "satVec.h"
 #include "satClause.h"
-#include "sat/xsat/xsatFloat.h"
+#include "misc/util/utilFloat.h"
+#include "misc/util/utilDouble.h"
 
 ABC_NAMESPACE_HEADER_START