# ChangeLog for sci-mathematics/nusmv
# Copyright 1999-2010 Gentoo Foundation; Distributed under the GPL v2
-# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/nusmv/ChangeLog,v 1.8 2010/01/13 16:48:53 bicatali Exp $
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/nusmv/ChangeLog,v 1.9 2010/06/22 20:03:17 phajdan.jr Exp $
+
+*nusmv-2.5.0 (22 Jun 2010)
+
+ 22 Jun 2010; Pawel Hajdan jr <phajdan.jr@gentoo.org>
+ +files/MiniSat_v1.14_gcc41.patch, +nusmv-2.5.0.ebuild:
+ Version bump, bug #311903.
13 Jan 2010; Sébastien Fabbro <bicatali@gentoo.org> nusmv-2.3.1.ebuild:
Added VARTEXFONTS, bug #223077
------BEGIN PGP SIGNED MESSAGE-----
-Hash: SHA1
-
AUX MiniSat_v1.14-optimizedlib.patch 1112 RMD160 9ae63aef1b74fac1bad9ee62049460856b5c5982 SHA1 7a2ee88eef0591690a2a728c07b68fdd882addda SHA256 21016b1ce69553c058385afa93f13248dbdc398c7968609d86dd9b707e227bfb
+AUX MiniSat_v1.14_gcc41.patch 4568 RMD160 59cccf1bfd15a4913c6026875639212859ce1ffa SHA1 532288df7231053ec41bbc11a02a1ec12ec396a4 SHA256 05179a822cca176f76340b2a5a9ffab1128d7018a1dfee743fb937abdc8233d9
DIST MiniSat_v1.14_src.zip 29428 RMD160 d5f0dc611a6116128d9a404f9045e02b185958b4 SHA1 266536cf5e5e77aa0478b98869bcd67ac1a523b6 SHA256 8e5e0ee84a770dcb3abd6fc65ed4aef938f9ffabca5ddc8a739029f7fb58a8f5
DIST NuSMV-2.3.1.tar.gz 2590944 RMD160 74f00e1c29dabe98e04cf0d652b92d63a73b07dc SHA1 588d3b43f136273176f4a6056b474f9d872b977b SHA256 b8ba0f29afafdfdef8c30f722eead3ef6cbb17e4bfe5563240a01d8a99dbbf68
+DIST NuSMV-2.5.0.tar.gz 3792968 RMD160 aaa3b9dc1329ad3feca6c9511b144437caf83472 SHA1 4b2837b0511e9eaf0eee53395308e8eaba6be727 SHA256 59310f5f23f72cb1ad16419e40f245db7c5aa41c0f59ba5c75732bb6c4b56ff1
EBUILD nusmv-2.3.1.ebuild 3331 RMD160 09aa89279858b6a6ac1be71adaf54545d4dffc54 SHA1 36c394fa4bbc8053059bd19be61ae8679983eb53 SHA256 43f713b4e5f21318516348f732f4129670235317724ce595d1e635aa0fbd91cd
-MISC ChangeLog 1356 RMD160 82fb9a1381f05b2c643dd2e11c6f907336800d37 SHA1 af2ee0e584af336b1864e598e2c613f36c7c8300 SHA256 f5b7a780e1e0f4f58eaf3e9025a31929ca37d215631409ddd4af49c6e43c5086
+EBUILD nusmv-2.5.0.ebuild 3504 RMD160 5c4594ec3c14bd77fefb7346e8736c52385fd145 SHA1 feb109b871e3f50028e7511151d3392b9ba546d3 SHA256 bd2396e81e30647d88334f9cb6f71b0b75414de49eadf7d2e8b1ffe20634518e
+MISC ChangeLog 1528 RMD160 e7b6b30f32950d1c18bb9095b6e9b9758a0bf556 SHA1 10d7264837b2a1fcb4af40cdd55daf2353d98aa2 SHA256 341299d9a7043a303f8d11b39dca07557a71e348dd1504b6871d1938496262d4
MISC metadata.xml 301 RMD160 95f4a72bad52574229901ce16d7d503b68cb22f9 SHA1 a62c653d31a41d1e11cea40d2d9366676d67d333 SHA256 b7f1f13dae0ffaaf9894bf5f5a95b351d63c630e9ccaab304b1edb8fa8f1c18c
------BEGIN PGP SIGNATURE-----
-Version: GnuPG v2.0.14 (GNU/Linux)
-
-iEYEARECAAYFAktOAgoACgkQ1ycZbhPLE2ApZACfQzxCrKqtPob3XwjbHxLGiai5
-vzMAn2IaaIqDNuoqEsj+hUeoms2x2w5q
-=gXuV
------END PGP SIGNATURE-----
--- /dev/null
+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
--- /dev/null
+# Copyright 1999-2010 Gentoo Foundation
+# Distributed under the terms of the GNU General Public License v2
+# $Header: /var/cvsroot/gentoo-x86/sci-mathematics/nusmv/nusmv-2.5.0.ebuild,v 1.1 2010/06/22 20:03:17 phajdan.jr Exp $
+
+inherit eutils toolchain-funcs
+
+NUSMV_PN="NuSMV"
+NUSMV_PV="${PV}"
+NUSMV_P="${NUSMV_PN}-${NUSMV_PV}"
+NUSMV_A="${NUSMV_P}.tar.gz"
+NUSMV_S="${WORKDIR}/${NUSMV_P}/nusmv"
+
+MINISAT_PN="MiniSat"
+MINISAT_PV="1.14"
+MINISAT_P="${MINISAT_PN}_v${MINISAT_PV}"
+MINISAT_A="${MINISAT_P}_src.zip"
+MINISAT_S="${WORKDIR}/${NUSMV_P}/MiniSat/${MINISAT_P}"
+
+CUDD_PN="cudd"
+CUDD_PV="2.4.1.1"
+CUDD_P="${CUDD_PN}-${CUDD_PV}"
+#CUDD_A is none
+CUDD_S="${WORKDIR}/${NUSMV_P}/${CUDD_P}"
+
+DESCRIPTION="NuSMV: new symbolic model checker"
+HOMEPAGE="http://nusmv.irst.itc.it/"
+# The Homepage is _very_ slow, 2Kb/sec or worse.
+# So we use our own mirror.
+# Additionally, MiniSat is distributed with a slightly different filename
+# So we mirror it ourselves
+SRC_URI="mirror://gentoo/${NUSMV_A}
+ http://nusmv.irst.itc.it/distrib/${NUSMV_A}
+ minisat? ( mirror://gentoo/${MINISAT_A} )"
+LICENSE="LGPL-2.1"
+SLOT="0"
+KEYWORDS="~x86 ~amd64"
+IUSE="minisat examples"
+RDEPEND="dev-libs/expat"
+DEPEND="${RDEPEND}
+ virtual/latex-base
+ || ( ( dev-texlive/texlive-latexextra )
+ app-text/ptex )
+ app-text/ghostscript-gpl
+ www-client/lynx
+ dev-lang/perl"
+# the above 4 are for docs, which aren't optional yet patches welcome to
+# avoid building the docs but I suspect anybody using this package will
+# actually need them
+S="${NUSMV_S}"
+
+src_unpack() {
+ unpack ${NUSMV_A}
+ if use minisat; then
+ cd "${WORKDIR}"/${NUSMV_P}/MiniSat
+ unpack ${MINISAT_A}
+ epatch ${MINISAT_P}_nusmv.patch
+ epatch "${FILESDIR}"/${MINISAT_P}-optimizedlib.patch
+ epatch "${FILESDIR}"/${MINISAT_P}_gcc41.patch
+ fi
+ for i in ${NUSMV_S}/doc/{user-man,tutorial}/Makefile.in ; do
+ sed -i.orig \
+ '/install_sh_DATA/s!$(datadir)!$(DESTDIR)$(datadir)!g' \
+ ${i} || die "sed $i failed"
+ done
+}
+
+src_compile() {
+ rm -f ${NUSMV_S}/${MINISAT_P}
+ if use minisat; then
+ cd ${MINISAT_S}
+ # do NOT merge these targets
+ emake COPTIMIZE="${CFLAGS}" r || die "Failed to build minisat bin"
+ emake COPTIMIZE="${CFLAGS}" lr || die "Failed to build minisat lib"
+ ln -sf ${MINISAT_S} "${WORKDIR}"/${NUSMV_P}/${MINISAT_P}
+ fi
+
+ cd ${CUDD_S}
+ emake clean || die "Failed to clean cudd out."
+ emake \
+ CPP="$(tc-getCPP)" CC="$(tc-getCC)" \
+ RANLIB="$(tc-getRANLIB)" ICFLAGS="${CFLAGS}" \
+ || die "Failed to build cudd."
+
+ local myconf="$(use_enable minisat) --enable-pslparser"
+ if use minisat; then
+ myconf="${myconf}
+ --with-minisat-incdir=../${MINISAT_P}
+ --with-minisat-libdir=../${MINISAT_P}"
+ fi
+
+ cd ${NUSMV_S}
+ econf ${myconf} || die "econf failed"
+ emake || die "emake failed"
+
+ VARTEXFONTS="${T}"/fonts emake docs
+}
+
+src_install() {
+ into /usr
+ if use minisat; then
+ newbin ${MINISAT_S}/minisat_release minisat
+ fi
+
+ dodir /usr/share/nusmv/doc
+ cd ${NUSMV_S}
+ emake DESTDIR="${D}" install || die "emake install failed"
+ # duplicate items
+ rm -f "${D}"/usr/share/nusmv/{LGPL-2.1,README*,NEWS}
+ # real docs
+ dodoc README* NEWS AUTHORS
+ dodoc doc/tutorial/tutorial.pdf
+ dodoc doc/user-man/nusmv.pdf
+
+ # move package-installed docs
+ mv "${D}"/usr/share/nusmv/doc/* "${D}"/usr/share/doc/${PF}/
+ rmdir "${D}"/usr/share/nusmv/doc
+
+ # clean out examples if not needed
+ if use !examples ; then
+ rm -rf "${D}"/usr/share/nusmv/examples || die "Failed to remove examples"
+ fi
+}
+
+src_test() {
+ cd ${NUSMV_S}
+ emake check || die "emake check failed"
+}
projects / gentoo.git / commitdiff