diff options
Diffstat (limited to 'sci-mathematics')
3 files changed, 0 insertions, 147 deletions
diff --git a/sci-mathematics/nusmv/files/MiniSat_v1.14-optimizedlib.patch b/sci-mathematics/nusmv/files/MiniSat_v1.14-optimizedlib.patch deleted file mode 100644 index a291339491bf..000000000000 --- a/sci-mathematics/nusmv/files/MiniSat_v1.14-optimizedlib.patch +++ /dev/null @@ -1,44 +0,0 @@ -diff -Nuar MiniSat_v1.14/Makefile MiniSat_v1.14.new/Makefile ---- MiniSat_v1.14/Makefile 2006-04-02 01:33:46.000000000 -0800 -+++ MiniSat_v1.14.new/Makefile 2006-04-02 01:31:39.000000000 -0800 -@@ -26,10 +26,11 @@ - RANLIB = ranlib - AR = ar - --.PHONY : ls s p d r build clean depend -+.PHONY : lr ls s p d r build clean depend - - s: WAY=standard - ls: WAY=standard -+lr: WAY=release - p: WAY=profile - d: WAY=debug - r: WAY=release -@@ -38,8 +39,7 @@ - s: CFLAGS+=$(COPTIMIZE) -ggdb -D DEBUG - p: CFLAGS+=$(COPTIMIZE) -pg -ggdb -D DEBUG - d: CFLAGS+=-O0 -ggdb -D DEBUG --r: CFLAGS+=$(COPTIMIZE) -D NDEBUG --rs: CFLAGS+=$(COPTIMIZE) -D NDEBUG -+r rs ls lr: CFLAGS+=$(COPTIMIZE) -D NDEBUG - - s: build $(EXEC) - p: build $(EXEC)_profile -@@ -48,7 +48,7 @@ - rs: build $(EXEC)_static - - s: CFLAGS+=$(COPTIMIZE) -ggdb -D DEBUG --ls: lbuild $(LIB)_s -+ls lr: lbuild $(LIB)_s - - build: - @echo Building $(EXEC) "("$(WAY)")" -@@ -63,7 +63,7 @@ - ## Build rule - %.o %.op %.od %.or: %.C - @echo Compiling: $< -- @$(CXX) $(CFLAGS) -c -o $@ $< -+ $(CXX) $(CFLAGS) -c -o $@ $< - - ## Linking rules (standard/profile/debug/release) - $(EXEC): $(COBJS) diff --git a/sci-mathematics/nusmv/files/MiniSat_v1.14_gcc41.patch b/sci-mathematics/nusmv/files/MiniSat_v1.14_gcc41.patch deleted file mode 100644 index dd5856ae57e5..000000000000 --- a/sci-mathematics/nusmv/files/MiniSat_v1.14_gcc41.patch +++ /dev/null @@ -1,92 +0,0 @@ -Index: MiniSat/MiniSat_v1.14/SolverTypes.h -=================================================================== ---- MiniSat/MiniSat_v1.14/SolverTypes.h (revision 1040) -+++ MiniSat/MiniSat_v1.14/SolverTypes.h (working copy) -@@ -42,19 +42,32 @@ - public: - Lit() : x(2*var_Undef) {} // (lit_Undef) - explicit Lit(Var var, bool sign = false) : x((var+var) + (int)sign) { } -- friend Lit operator ~ (Lit p) { Lit q; q.x = p.x ^ 1; return q; } -+ friend Lit operator ~ (Lit p); - -- friend bool sign (Lit p) { return p.x & 1; } -- friend int var (Lit p) { return p.x >> 1; } -- friend int index (Lit p) { return p.x; } // A "toInt" method that guarantees small, positive integers suitable for array indexing. -- friend Lit toLit (int i) { Lit p; p.x = i; return p; } // Inverse of 'index()'. -- friend Lit unsign(Lit p) { Lit q; q.x = p.x & ~1; return q; } -- friend Lit id (Lit p, bool sgn) { Lit q; q.x = p.x ^ (int)sgn; return q; } -+ friend bool sign (Lit p); -+ friend int var (Lit p); -+ friend int index (Lit p); // A "toInt" method that guarantees small, positive integers suitable for array indexing. -+ friend Lit toLit (int i); // Inverse of 'index()'. -+ friend Lit unsign(Lit p); -+ friend Lit id (Lit p, bool sgn); - -- friend bool operator == (Lit p, Lit q) { return index(p) == index(q); } -- friend bool operator < (Lit p, Lit q) { return index(p) < index(q); } // '<' guarantees that p, ~p are adjacent in the ordering. -+ friend bool operator == (Lit p, Lit q); -+ friend bool operator < (Lit p, Lit q); // '<' guarantees that p, ~p are adjacent in the ordering. - }; - -+inline Lit operator ~ (Lit p) { Lit q; q.x = p.x ^ 1; return q; } -+ -+inline bool sign (Lit p) { return p.x & 1; } -+inline int var (Lit p) { return p.x >> 1; } -+inline int index (Lit p) { return p.x; } // A "toInt" method that guarantees small, positive integers suitable for array indexing. -+inline Lit toLit (int i) { Lit p; p.x = i; return p; } // Inverse of 'index()'. -+inline Lit unsign(Lit p) { Lit q; q.x = p.x & ~1; return q; } -+inline Lit id (Lit p, bool sgn) { Lit q; q.x = p.x ^ (int)sgn; return q; } -+ -+inline bool operator == (Lit p, Lit q) { return index(p) == index(q); } -+inline bool operator < (Lit p, Lit q) { return index(p) < index(q); } // '<' guarantees that p, ~p are adjacent in the ordering. -+ -+ - const Lit lit_Undef(var_Undef, false); // }- Useful special constants. - const Lit lit_Error(var_Undef, true ); // } - -@@ -79,11 +92,7 @@ - if (learnt) activity() = 0; } - - // -- use this function instead: -- friend Clause* Clause_new(bool learnt, const vec<Lit>& ps) { -- assert(sizeof(Lit) == sizeof(uint)); -- assert(sizeof(float) == sizeof(uint)); -- void* mem = xmalloc<char>(sizeof(Clause) + sizeof(uint)*(ps.size() + (int)learnt)); -- return new (mem) Clause(learnt, ps); } -+ friend Clause* Clause_new(bool learnt, const vec<Lit>& ps); - - int size () const { return size_learnt >> 1; } - bool learnt () const { return size_learnt & 1; } -@@ -92,6 +101,12 @@ - float& activity () const { return *((float*)&data[size()]); } - }; - -+inline Clause* Clause_new(bool learnt, const vec<Lit>& ps) { -+ assert(sizeof(Lit) == sizeof(uint)); -+ assert(sizeof(float) == sizeof(uint)); -+ void* mem = xmalloc<char>(sizeof(Clause) + sizeof(uint)*(ps.size() + (int)learnt)); -+ return new (mem) Clause(learnt, ps); -+} - - //================================================================================================= - // GClause -- Generalize clause: -@@ -102,8 +117,8 @@ - void* data; - GClause(void* d) : data(d) {} - public: -- friend GClause GClause_new(Lit p) { return GClause((void*)((index(p) << 1) + 1)); } -- friend GClause GClause_new(Clause* c) { assert(((uintp)c & 1) == 0); return GClause((void*)c); } -+ friend GClause GClause_new(Lit p); -+ friend GClause GClause_new(Clause* c); - - bool isLit () const { return ((uintp)data & 1) == 1; } - bool isNull () const { return data == NULL; } -@@ -114,6 +129,8 @@ - }; - #define GClause_NULL GClause_new((Clause*)NULL) - -+inline GClause GClause_new(Lit p) { return GClause((void*)((index(p) << 1) + 1)); } -+inline GClause GClause_new(Clause* c) { assert(((uintp)c & 1) == 0); return GClause((void*)c); } - - //================================================================================================= - #endif diff --git a/sci-mathematics/nusmv/files/cudd-no-pentium4.patch b/sci-mathematics/nusmv/files/cudd-no-pentium4.patch deleted file mode 100644 index 844f7c00d638..000000000000 --- a/sci-mathematics/nusmv/files/cudd-no-pentium4.patch +++ /dev/null @@ -1,11 +0,0 @@ ---- Makefile.orig 2010-07-12 02:54:26.000000000 +0200 -+++ Makefile 2010-07-12 02:54:49.000000000 +0200 -@@ -69,7 +69,7 @@ - # Gcc 2.8.1 or higher on i686. - #XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD - # Gcc 3.2.2 or higher on i686. --XCFLAGS = -mcpu=pentium4 -malign-double -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4 -DSIZEOF_INT=4 -+XCFLAGS = -malign-double -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4 -DSIZEOF_INT=4 - # Icc on i686. - #XCFLAGS = -ansi -align -ip -DHAVE_IEEE_754 -DBSD - # Gcc on ia64. |