diff options
author | Robin H. Johnson <robbat2@gentoo.org> | 2015-08-08 13:49:04 -0700 |
---|---|---|
committer | Robin H. Johnson <robbat2@gentoo.org> | 2015-08-08 17:38:18 -0700 |
commit | 56bd759df1d0c750a065b8c845e93d5dfa6b549d (patch) | |
tree | 3f91093cdb475e565ae857f1c5a7fd339e2d781e /sci-mathematics/nusmv/files | |
download | gentoo-56bd759df1d0c750a065b8c845e93d5dfa6b549d.tar.gz gentoo-56bd759df1d0c750a065b8c845e93d5dfa6b549d.tar.xz |
proj/gentoo: Initial commit
This commit represents a new era for Gentoo:
Storing the gentoo-x86 tree in Git, as converted from CVS.
This commit is the start of the NEW history.
Any historical data is intended to be grafted onto this point.
Creation process:
1. Take final CVS checkout snapshot
2. Remove ALL ChangeLog* files
3. Transform all Manifests to thin
4. Remove empty Manifests
5. Convert all stale $Header$/$Id$ CVS keywords to non-expanded Git $Id$
5.1. Do not touch files with -kb/-ko keyword flags.
Signed-off-by: Robin H. Johnson <robbat2@gentoo.org>
X-Thanks: Alec Warner <antarus@gentoo.org> - did the GSoC 2006 migration tests
X-Thanks: Robin H. Johnson <robbat2@gentoo.org> - infra guy, herding this project
X-Thanks: Nguyen Thai Ngoc Duy <pclouds@gentoo.org> - Former Gentoo developer, wrote Git features for the migration
X-Thanks: Brian Harring <ferringb@gentoo.org> - wrote much python to improve cvs2svn
X-Thanks: Rich Freeman <rich0@gentoo.org> - validation scripts
X-Thanks: Patrick Lauer <patrick@gentoo.org> - Gentoo dev, running new 2014 work in migration
X-Thanks: Michał Górny <mgorny@gentoo.org> - scripts, QA, nagging
X-Thanks: All of other Gentoo developers - many ideas and lots of paint on the bikeshed
Diffstat (limited to 'sci-mathematics/nusmv/files')
3 files changed, 147 insertions, 0 deletions
diff --git a/sci-mathematics/nusmv/files/MiniSat_v1.14-optimizedlib.patch b/sci-mathematics/nusmv/files/MiniSat_v1.14-optimizedlib.patch new file mode 100644 index 00000000000..a291339491b --- /dev/null +++ b/sci-mathematics/nusmv/files/MiniSat_v1.14-optimizedlib.patch @@ -0,0 +1,44 @@ +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 new file mode 100644 index 00000000000..dd5856ae57e --- /dev/null +++ b/sci-mathematics/nusmv/files/MiniSat_v1.14_gcc41.patch @@ -0,0 +1,92 @@ +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 new file mode 100644 index 00000000000..844f7c00d63 --- /dev/null +++ b/sci-mathematics/nusmv/files/cudd-no-pentium4.patch @@ -0,0 +1,11 @@ +--- 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. |