From 45f4d6c7e8678e140b363f3114b5393ed1f29681 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 11 Feb 2017 13:55:41 -0800 Subject: [PATCH] Movinng custom floating-point implementations, etc. --- abclib.dsp | 24 +++++++++---------- src/misc/util/abc_global.h | 2 ++ .../xsatDouble.h => misc/util/utilDouble.h} | 6 +---- .../xsatFloat.h => misc/util/utilFloat.h} | 5 ++-- src/sat/bsat/satSolver.h | 3 ++- 5 files changed, 19 insertions(+), 21 deletions(-) rename src/{sat/xsat/xsatDouble.h => misc/util/utilDouble.h} (96%) rename src/{sat/xsat/xsatFloat.h => misc/util/utilFloat.h} (98%) diff --git a/abclib.dsp b/abclib.dsp index 853076350..f9cc2f502 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 00d5d5148..9e9068169 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 similarity index 96% rename from src/sat/xsat/xsatDouble.h rename to src/misc/util/utilDouble.h index d90e8c05b..0d0237818 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 similarity index 98% rename from src/sat/xsat/xsatFloat.h rename to src/misc/util/utilFloat.h index fb451a945..f0739a922 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 226d8c7ad..21f24fcb1 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