From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from pigeon.gentoo.org ([208.92.234.80] helo=lists.gentoo.org) by finch.gentoo.org with esmtp (Exim 4.60) (envelope-from ) id 1OR9gm-0003Rp-IR for garchives@archives.gentoo.org; Tue, 22 Jun 2010 20:03:21 +0000 Received: from pigeon.gentoo.org (localhost [127.0.0.1]) by pigeon.gentoo.org (Postfix) with SMTP id 02DA6E0B5B; Tue, 22 Jun 2010 20:03:20 +0000 (UTC) Received: from smtp.gentoo.org (smtp.gentoo.org [140.211.166.183]) by pigeon.gentoo.org (Postfix) with ESMTP id AAE4CE0B5C for ; Tue, 22 Jun 2010 20:03:19 +0000 (UTC) Received: from corvid.gentoo.org (corvid.gentoo.org [208.92.234.79]) (using TLSv1 with cipher DHE-RSA-CAMELLIA256-SHA (256/256 bits)) (No client certificate requested) by smtp.gentoo.org (Postfix) with ESMTP id 32FA01B40E9 for ; Tue, 22 Jun 2010 20:03:19 +0000 (UTC) Received: by corvid.gentoo.org (Postfix, from userid 2261) id 279C22C3ED; Tue, 22 Jun 2010 20:03:17 +0000 (UTC) From: "PaweA Hajdan (phajdan.jr)" To: gentoo-commits@lists.gentoo.org Reply-To: gentoo-dev@lists.gentoo.org, phajdan.jr@gentoo.org Subject: [gentoo-commits] gentoo-x86 commit in sci-mathematics/nusmv/files: MiniSat_v1.14_gcc41.patch X-VCS-Repository: gentoo-x86 X-VCS-Files: MiniSat_v1.14_gcc41.patch X-VCS-Directories: sci-mathematics/nusmv/files X-VCS-Committer: phajdan.jr X-VCS-Committer-Name: PaweA Hajdan Content-Type: text/plain; charset=utf8 Message-Id: <20100622200318.279C22C3ED@corvid.gentoo.org> Date: Tue, 22 Jun 2010 20:03:17 +0000 (UTC) Precedence: bulk List-Post: List-Help: List-Unsubscribe: List-Subscribe: List-Id: Gentoo Linux mail X-BeenThere: gentoo-commits@lists.gentoo.org Content-Transfer-Encoding: quoted-printable X-Archives-Salt: 7a4b3faf-a08b-445c-84f8-8f003ed00cee X-Archives-Hash: 8f6dffb88ff62f633aa0c13e04609180 phajdan.jr 10/06/22 20:03:17 Added: MiniSat_v1.14_gcc41.patch Log: Version bump, bug #311903. (Portage version: 2.1.8.3/cvs/Linux i686) Revision Changes Path 1.1 sci-mathematics/nusmv/files/MiniSat_v1.14_gcc41.patc= h file : http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/nu= smv/files/MiniSat_v1.14_gcc41.patch?rev=3D1.1&view=3Dmarkup plain: http://sources.gentoo.org/viewvc.cgi/gentoo-x86/sci-mathematics/nu= smv/files/MiniSat_v1.14_gcc41.patch?rev=3D1.1&content-type=3Dtext/plain Index: MiniSat_v1.14_gcc41.patch =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D Index: MiniSat/MiniSat_v1.14/SolverTypes.h =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D --- 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 =3D false) : x((var+var) + (int)sign= ) { } - friend Lit operator ~ (Lit p) { Lit q; q.x =3D p.x ^ 1; return q; } + friend Lit operator ~ (Lit p); =20 - 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 inde= xing. - friend Lit toLit (int i) { Lit p; p.x =3D i; return p; } // Invers= e of 'index()'. - friend Lit unsign(Lit p) { Lit q; q.x =3D p.x & ~1; return q; } - friend Lit id (Lit p, bool sgn) { Lit q; q.x =3D 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); =20 - friend bool operator =3D=3D (Lit p, Lit q) { return index(p) =3D=3D = 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 =3D=3D (Lit p, Lit q); + friend bool operator < (Lit p, Lit q); // '<' guarantees that p, ~p= are adjacent in the ordering. }; =20 +inline Lit operator ~ (Lit p) { Lit q; q.x =3D 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" me= thod that guarantees small, positive integers suitable for array indexing= . +inline Lit toLit (int i) { Lit p; p.x =3D i; return p; } // Inverse of= 'index()'. +inline Lit unsign(Lit p) { Lit q; q.x =3D p.x & ~1; return q; } +inline Lit id (Lit p, bool sgn) { Lit q; q.x =3D p.x ^ (int)sgn; ret= urn q; } + +inline bool operator =3D=3D (Lit p, Lit q) { return index(p) =3D=3D inde= x(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 ); // } =20 @@ -79,11 +92,7 @@ if (learnt) activity() =3D 0; } =20 // -- use this function instead: - friend Clause* Clause_new(bool learnt, const vec& ps) { - assert(sizeof(Lit) =3D=3D sizeof(uint)); - assert(sizeof(float) =3D=3D sizeof(uint)); - void* mem =3D xmalloc(sizeof(Clause) + sizeof(uint)*(ps.= size() + (int)learnt)); - return new (mem) Clause(learnt, ps); } + friend Clause* Clause_new(bool learnt, const vec& ps); =20 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()]= ); } }; =20 +inline Clause* Clause_new(bool learnt, const vec& ps) { + assert(sizeof(Lit) =3D=3D sizeof(uint)); + assert(sizeof(float) =3D=3D sizeof(uint)); + void* mem =3D xmalloc(sizeof(Clause) + sizeof(uint)*(ps.= size() + (int)learnt)); + return new (mem) Clause(learnt, ps);=20 +} =20 //=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D // GClause -- Generalize clause: @@ -102,8 +117,8 @@ void* data; GClause(void* d) : data(d) {} public: - friend GClause GClause_new(Lit p) { return GClause((void*)((inde= x(p) << 1) + 1)); } - friend GClause GClause_new(Clause* c) { assert(((uintp)c & 1) =3D=3D= 0); return GClause((void*)c); } + friend GClause GClause_new(Lit p); + friend GClause GClause_new(Clause* c);=20 =20 bool isLit () const { return ((uintp)data & 1) =3D=3D 1; } bool isNull () const { return data =3D=3D NULL; } @@ -114,6 +129,8 @@ }; #define GClause_NULL GClause_new((Clause*)NULL) =20 +inline GClause GClause_new(Lit p) { return GClause((void*)((index(p) << = 1) + 1)); } +inline GClause GClause_new(Clause* c) { assert(((uintp)c & 1) =3D=3D 0);= return GClause((void*)c); } =20 //=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D #endif