[packages/NuSMV] - rel 8; build fixed
arekm
arekm at pld-linux.org
Sat Dec 12 22:20:28 CET 2015
commit 17427a1955c8d3e925fdd7d95f506f7fe74907ab
Author: Arkadiusz Miśkiewicz <arekm at maven.pl>
Date: Sat Dec 12 22:20:23 2015 +0100
- rel 8; build fixed
NuSMV-build.patch | 53 +++++++++++++++++++++++++++++++++++++++++++++++++++++
NuSMV.spec | 8 +++++---
2 files changed, 58 insertions(+), 3 deletions(-)
---
diff --git a/NuSMV.spec b/NuSMV.spec
index a8f12a4..b8e4e81 100644
--- a/NuSMV.spec
+++ b/NuSMV.spec
@@ -9,7 +9,7 @@ Summary: New Symbolic Model Verifier
Summary(pl.UTF-8): Nowy weryfikator modeli symbolicznych
Name: NuSMV
Version: 2.5.4
-Release: 7
+Release: 8
License: LGPL
Group: Applications
Source0: http://nusmv.irst.itc.it/distrib/%{name}-%{version}.tar.gz
@@ -98,11 +98,13 @@ Statyczna biblioteka NuSMV.
%prep
%setup -q
-%patch0 -p1
-
install %{SOURCE1} MiniSat/
+cd MiniSat
+unzip -q *.zip
+cd ..
install %{SOURCE2} zchaff/
+%patch0 -p1
%patch1 -p1
%patch2 -p1
diff --git a/NuSMV-build.patch b/NuSMV-build.patch
index 1520b01..c48244d 100644
--- a/NuSMV-build.patch
+++ b/NuSMV-build.patch
@@ -118,3 +118,56 @@ diff -ur NuSMV-2.4.0/nusmv/helpers/extract_doc.in NuSMV-2.4.0-ok/nusmv/helpers/e
cfile=$1
htmldir=$2
+--- NuSMV-2.5.4/MiniSat/minisat/simp/SimpSolver.C~ 2015-12-12 22:07:12.000000000 +0100
++++ NuSMV-2.5.4/MiniSat/minisat/simp/SimpSolver.C 2015-12-12 22:09:59.149163015 +0100
+@@ -37,7 +37,7 @@ SimpSolver::SimpSolver() :
+ , bwdsub_assigns (0)
+ {
+ vec<Lit> dummy(1,lit_Undef);
+- bwdsub_tmpunit = Clause_new(dummy);
++ bwdsub_tmpunit = Clause::Clause_new(dummy);
+ remove_satisfied = false;
+ }
+
+--- NuSMV-2.5.4/MiniSat/minisat/core/SolverTypes.h~ 2006-11-10 22:54:30.000000000 +0100
++++ NuSMV-2.5.4/MiniSat/minisat/core/SolverTypes.h 2015-12-12 22:14:08.982282692 +0100
+@@ -119,7 +119,7 @@ public:
+
+ // -- use this function instead:
+ template<class V>
+- friend Clause* Clause_new(const V& ps, bool learnt = false) {
++ static Clause* Clause_new(const V& ps, bool learnt = false) {
+ assert(sizeof(Lit) == sizeof(uint32_t));
+ assert(sizeof(float) == sizeof(uint32_t));
+ void* mem = malloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size()));
+--- NuSMV-2.5.4/MiniSat/minisat/simp/SimpSolver.C~ 2015-12-12 22:14:47.000000000 +0100
++++ NuSMV-2.5.4/MiniSat/minisat/simp/SimpSolver.C 2015-12-12 22:16:31.295964939 +0100
+@@ -489,7 +489,7 @@ bool SimpSolver::eliminateVar(Var v, boo
+ elimtable[v].order = elimorder++;
+ assert(elimtable[v].eliminated.size() == 0);
+ for (int i = 0; i < cls.size(); i++){
+- elimtable[v].eliminated.push(Clause_new(*cls[i]));
++ elimtable[v].eliminated.push(Clause::Clause_new(*cls[i]));
+ removeClause(*cls[i]); }
+
+ // Produce clauses in cross product:
+--- NuSMV-2.5.4/MiniSat/minisat/core/Solver.C~ 2015-12-12 22:16:49.000000000 +0100
++++ NuSMV-2.5.4/MiniSat/minisat/core/Solver.C 2015-12-12 22:17:47.084605634 +0100
+@@ -114,7 +114,7 @@ bool Solver::addClause(vec<Lit>& ps)
+ uncheckedEnqueue(ps[0]);
+ return ok = (propagate() == NULL);
+ }else{
+- Clause* c = Clause_new(ps, false);
++ Clause* c = Clause::Clause_new(ps, false);
+ clauses.push(c);
+ attachClause(*c);
+ }
+@@ -598,7 +598,7 @@ lbool Solver::search(int nof_conflicts,
+ if (learnt_clause.size() == 1){
+ uncheckedEnqueue(learnt_clause[0]);
+ }else{
+- Clause* c = Clause_new(learnt_clause, true);
++ Clause* c = Clause::Clause_new(learnt_clause, true);
+ learnts.push(c);
+ attachClause(*c);
+ claBumpActivity(*c);
================================================================
---- gitweb:
http://git.pld-linux.org/gitweb.cgi/packages/NuSMV.git/commitdiff/17427a1955c8d3e925fdd7d95f506f7fe74907ab
More information about the pld-cvs-commit
mailing list