Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: azonenberg/yosys
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: 106e44f40640
Choose a base ref
...
head repository: azonenberg/yosys
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: 58ee8e3b8a81
Choose a head ref
  • 2 commits
  • 5 files changed
  • 1 contributor

Commits on Mar 27, 2017

  1. Copy the full SHA
    71cbe98 View commit details
  2. Copy the full SHA
    58ee8e3 View commit details
Showing with 65 additions and 18 deletions.
  1. +43 −0 libs/minisat/00_PATCH_no_fpu_control.patch
  2. +20 −0 libs/minisat/00_PATCH_typofixes.patch
  3. +2 −0 libs/minisat/00_UPDATE.sh
  4. +0 −11 libs/minisat/System.cc
  5. +0 −7 libs/minisat/System.h
43 changes: 43 additions & 0 deletions libs/minisat/00_PATCH_no_fpu_control.patch
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
--- System.cc
+++ System.cc
@@ -97,17 +97,6 @@ double Minisat::memUsedPeak(bool) { return 0; }
#endif


-void Minisat::setX86FPUPrecision()
-{
-#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW)
- // Only correct FPU precision on Linux architectures that needs and supports it:
- fpu_control_t oldcw, newcw;
- _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
- printf("WARNING: for repeatability, setting FPU to use double precision\n");
-#endif
-}
-
-
#if !defined(_MSC_VER) && !defined(__MINGW32__)
void Minisat::limitMemory(uint64_t max_mem_mb)
{
--- System.h
+++ System.h
@@ -21,10 +21,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#ifndef Minisat_System_h
#define Minisat_System_h

-#if defined(__linux__)
-#include <fpu_control.h>
-#endif
-
#include "IntTypes.h"

//-------------------------------------------------------------------------------------------------
@@ -36,9 +32,6 @@ static inline double cpuTime(void); // CPU-time in seconds.
extern double memUsed(); // Memory in mega bytes (returns 0 for unsupported architectures).
extern double memUsedPeak(bool strictlyPeak = false); // Peak-memory in mega bytes (returns 0 for unsupported architectures).

-extern void setX86FPUPrecision(); // Make sure double's are represented with the same precision
- // in memory and registers.
-
extern void limitMemory(uint64_t max_mem_mb); // Set a limit on total memory usage. The exact
// semantics varies depending on architecture.

20 changes: 20 additions & 0 deletions libs/minisat/00_PATCH_typofixes.patch
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
--- Solver.h
+++ Solver.h
@@ -103,7 +103,7 @@ public:
int nFreeVars () const;
void printStats () const; // Print some current statistics to standard output.

- // Resource contraints:
+ // Resource constraints:
//
void setConfBudget(int64_t x);
void setPropBudget(int64_t x);
@@ -230,7 +230,7 @@ protected:
double learntsize_adjust_confl;
int learntsize_adjust_cnt;

- // Resource contraints:
+ // Resource constraints:
//
int64_t conflict_budget; // -1 means no budget.
int64_t propagation_budget; // -1 means no budget.
2 changes: 2 additions & 0 deletions libs/minisat/00_UPDATE.sh
Original file line number Diff line number Diff line change
@@ -14,4 +14,6 @@ sed -i -e '1 i #define __STDC_FORMAT_MACROS' *.cc

patch -p0 < 00_PATCH_mkLit_default_arg.patch
patch -p0 < 00_PATCH_remove_zlib.patch
patch -p0 < 00_PATCH_no_fpu_control.patch
patch -p0 < 00_PATCH_typofixes.patch

11 changes: 0 additions & 11 deletions libs/minisat/System.cc
Original file line number Diff line number Diff line change
@@ -97,17 +97,6 @@ double Minisat::memUsedPeak(bool) { return 0; }
#endif


void Minisat::setX86FPUPrecision()
{
#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE) && defined(_FPU_GETCW)
// Only correct FPU precision on Linux architectures that needs and supports it:
fpu_control_t oldcw, newcw;
_FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
printf("WARNING: for repeatability, setting FPU to use double precision\n");
#endif
}


#if !defined(_MSC_VER) && !defined(__MINGW32__)
void Minisat::limitMemory(uint64_t max_mem_mb)
{
7 changes: 0 additions & 7 deletions libs/minisat/System.h
Original file line number Diff line number Diff line change
@@ -21,10 +21,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#ifndef Minisat_System_h
#define Minisat_System_h

#if defined(__linux__)
#include <fpu_control.h>
#endif

#include "IntTypes.h"

//-------------------------------------------------------------------------------------------------
@@ -36,9 +32,6 @@ static inline double cpuTime(void); // CPU-time in seconds.
extern double memUsed(); // Memory in mega bytes (returns 0 for unsupported architectures).
extern double memUsedPeak(bool strictlyPeak = false); // Peak-memory in mega bytes (returns 0 for unsupported architectures).

extern void setX86FPUPrecision(); // Make sure double's are represented with the same precision
// in memory and registers.

extern void limitMemory(uint64_t max_mem_mb); // Set a limit on total memory usage. The exact
// semantics varies depending on architecture.