commit 4d9d514952450eb08a3f48a5927359b75182cebb
Author: Jerry James <jamesjer(a)betterlinux.com>
Date: Wed Jul 31 16:49:06 2013 -0600
New upstream release.
Remove comment that was being pulled into postun.
.gitignore | 2 +-
picosat-alias.patch | 24 +++++++++--------
picosat-proof-access.patch | 59 ++++++++++++++++++++++---------------------
picosat-trace.patch | 24 +++++++++---------
picosat.spec | 11 ++++---
sources | 2 +-
6 files changed, 63 insertions(+), 59 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index a08d939..3757868 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1 @@
-/picosat-951.tar.gz
+/picosat-957.tar.gz
diff --git a/picosat-alias.patch b/picosat-alias.patch
index 271b754..bea34a9 100644
--- a/picosat-alias.patch
+++ b/picosat-alias.patch
@@ -1,37 +1,39 @@
---- ./picosat.c.orig 2012-08-20 14:56:30.236102928 -0600
-+++ ./picosat.c 2012-08-20 15:02:03.774695361 -0600
-@@ -1283,8 +1283,10 @@ new_clause (unsigned size, unsigned lear
+--- ./picosat.c.orig 2013-07-31 14:41:10.000000000 -0600
++++ ./picosat.c 2013-07-31 14:48:29.000000000 -0600
+@@ -1321,8 +1321,10 @@ new_clause (PS * ps, unsigned size, unsi
res->collected = 0;
#endif
- if (learned && size > 2)
-- *CLS2ACT (res) = cinc;
+- *CLS2ACT (res) = ps->cinc;
+ if (learned && size > 2) {
+ Act *act = CLS2ACT (res);
-+ *act = cinc;
++ *act = ps->cinc;
+ }
return res;
}
-@@ -5504,14 +5506,17 @@ iteration (void)
+@@ -5611,8 +5613,8 @@ iteration (PS * ps)
static int
- cmp_activity (Cls * c, Cls * d)
+ cmp_glue_activity_size (PS * ps, Cls * c, Cls * d)
{
- Act a;
- Act b;
+ Act a, *aptr;
+ Act b, *bptr;
- assert (c->learned);
- assert (d->learned);
+ (void) ps;
+
+@@ -5625,8 +5627,10 @@ cmp_glue_activity_size (PS * ps, Cls * c
+ if (c->glue > d->glue)
+ return -1;
- a = *CLS2ACT (c);
- b = *CLS2ACT (d);
+ aptr = CLS2ACT (c);
+ bptr = CLS2ACT (d);
-+
+ a = *aptr;
+ b = *bptr;
- if (a < b)
+ if (a < b) // then higher activity
return -1;
diff --git a/picosat-proof-access.patch b/picosat-proof-access.patch
index 0bdc039..ec04dc0 100644
--- a/picosat-proof-access.patch
+++ b/picosat-proof-access.patch
@@ -1,7 +1,7 @@
---- ./picosat.c.orig 2012-08-20 14:53:10.101697229 -0600
-+++ ./picosat.c 2012-08-20 14:55:28.099997470 -0600
-@@ -6362,6 +6362,168 @@ write_trace (FILE * file, int fmt)
- #endif
+--- ./picosat.c.orig 2013-07-31 14:26:09.000000000 -0600
++++ ./picosat.c 2013-07-31 14:41:10.000000000 -0600
+@@ -6383,6 +6383,168 @@ trace_zhain (PS * ps, unsigned idx, Zhn
+ fputs (" 0\n", file);
}
+/**
@@ -25,13 +25,13 @@
+}
+
+static int
-+my_write_idx (unsigned idx)
++my_write_idx (PS * ps, unsigned idx)
+{
+ return EXPORTIDX (idx);
+}
+
+static void
-+my_trace_lits (Cls * cls)
++my_trace_lits (PS * ps, Cls * cls)
+{
+ Lit **p, **eol = end_of_lits (cls);
+
@@ -48,7 +48,7 @@
+}
+
+static void
-+my_trace_zhain (unsigned idx, Zhn * zhain)
++my_trace_zhain (PS * ps, unsigned idx, Zhn * zhain)
+{
+ unsigned prev, this, delta, i;
+ Znt *p, byte;
@@ -57,12 +57,12 @@
+ assert (zhain);
+ assert (zhain->core);
+
-+ int id = my_write_idx (idx);
++ int id = my_write_idx (ps, idx);
+ add_int_to_proof(id);
+
+ cls = IDX2CLS (idx);
+ assert (cls);
-+ my_trace_lits (cls);
++ my_trace_lits (ps, cls);
+
+ i = 0;
+ delta = 0;
@@ -78,7 +78,7 @@
+
+ this = prev + delta;
+
-+ id = my_write_idx (this);
++ id = my_write_idx (ps, this);
+ add_int_to_proof(id);
+
+ prev = this;
@@ -90,23 +90,23 @@
+}
+
+static void
-+my_trace_clause (unsigned idx, Cls * cls)
++my_trace_clause (PS * ps, unsigned idx, Cls * cls)
+{
+ assert (cls);
+ assert (cls->core);
+ assert (!cls->learned);
+ assert (CLS2IDX (cls) == idx);
+
-+ add_int_to_proof (my_write_idx (idx));
++ add_int_to_proof (my_write_idx (ps, idx));
+
-+ my_trace_lits (cls);
++ my_trace_lits (ps, cls);
+
+ add_int_to_proof(0);
+
+}
+
+static int*
-+get_proof ()
++get_proof (PS * ps)
+{
+ Cls *cls, ** p;
+ Zhn *zhain;
@@ -119,21 +119,21 @@
+ current_size = PROOF_BLOCK;
+ cursor = 0;
+
-+ core ();
++ core (ps);
+
+ for (p = SOC; p != EOC; p = NXC (p))
+ {
+ cls = *p;
+
-+ if (oclauses <= p && p < eoo)
++ if (ps->oclauses <= p && p < ps->eoo)
+ {
-+ i = OIDX2IDX (p - oclauses);
++ i = OIDX2IDX (p - ps->oclauses);
+ assert (!cls || CLS2IDX (cls) == i);
+ }
+ else
+ {
-+ assert (lclauses <= p && p < eol);
-+ i = LIDX2IDX (p - lclauses);
++ assert (ps->lclauses <= p && p < eol);
++ i = LIDX2IDX (p - ps->lclauses);
+ }
+
+ zhain = IDX2ZHN (i);
@@ -142,12 +142,12 @@
+ {
+ if (zhain->core)
+ {
-+ my_trace_zhain (i, zhain);
++ my_trace_zhain (ps, i, zhain);
+ }
+ }
+ else if (cls && cls->core)
+ {
-+ my_trace_clause (i, cls);
++ my_trace_clause (ps, i, cls);
+ }
+ }
+ add_int_to_proof(EOP);
@@ -157,30 +157,31 @@
+#endif
+
+int *
-+picosat_get_proof ()
++picosat_get_proof (PS * ps)
+{
+#ifdef TRACE
-+ return get_proof();
++ return get_proof(ps);
+#else
+ return NULL;
+#endif
+}
+
static void
- write_core_wrapper (FILE * file, int fmt)
+ write_core (PS * ps, FILE * file)
{
---- ./picosat.h.orig 2012-08-12 08:06:23.000000000 -0600
-+++ ./picosat.h 2012-08-20 14:55:28.116997497 -0600
-@@ -251,6 +251,12 @@ void picosat_simplify (void);
+--- ./picosat.h.orig 2013-06-01 07:35:00.000000000 -0600
++++ ./picosat.h 2013-07-31 14:44:24.000000000 -0600
+@@ -275,6 +275,13 @@ void picosat_simplify (PicoSAT *);
*/
- void picosat_adjust (int max_idx);
+ void picosat_adjust (PicoSAT *, int max_idx);
+/* Return an array of int where every cell is the next value of the proof in
+ * EXTENDED_TRACECHECK_TRACE_FMT format.
+ * The proof finishes by EOP.
+ */
+#define EOP ((int)(1 << 31)) /* 2^31 -1, max caml int32*/
-+int* picosat_get_proof();
++int* picosat_get_proof(PicoSAT *);
++
/*------------------------------------------------------------------------*/
/* Statistics.
*/
diff --git a/picosat-trace.patch b/picosat-trace.patch
index bdfaddb..80de5d7 100644
--- a/picosat-trace.patch
+++ b/picosat-trace.patch
@@ -1,5 +1,5 @@
---- ./makefile.in.orig 2012-08-12 08:06:23.000000000 -0600
-+++ ./makefile.in 2012-08-20 14:52:17.942652233 -0600
+--- ./makefile.in.orig 2013-06-01 07:35:00.000000000 -0600
++++ ./makefile.in 2013-07-31 14:26:09.000000000 -0600
@@ -12,16 +12,16 @@ clean:
analyze:
clang --analyze $(CFLAGS) *.c *.h
@@ -21,7 +21,7 @@
$(CC) $(CFLAGS) -o $@ picogcnf.o -L. -lpicosat
app.o: app.c picosat.h makefile
-@@ -37,10 +37,10 @@ main.o: main.c picosat.h makefile
+@@ -40,10 +40,10 @@ main.o: main.c picosat.h makefile
$(CC) $(CFLAGS) -c $<
picosat.o: picosat.c picosat.h makefile
@@ -34,7 +34,7 @@
config.h: makefile VERSION mkconfig # and actually picosat.c
rm -f $@; ./mkconfig > $@
-@@ -51,6 +51,6 @@ libpicosat.a: picosat.o version.o
+@@ -54,6 +54,6 @@ libpicosat.a: picosat.o version.o
SONAME=-Xlinker -soname -Xlinker libpicosat.so
libpicosat.so: picosat.o version.o
@@ -42,9 +42,9 @@
+ $(CC) $(CFLAGS) -fPIC -shared -o $@ picosat.o version.o $(SONAME)
.PHONY: all clean
---- ./picosat.c.orig 2012-08-12 08:06:23.000000000 -0600
-+++ ./picosat.c 2012-08-20 14:53:10.101697229 -0600
-@@ -6564,7 +6564,7 @@ check_trace_support_and_execute (FILE *
+--- ./picosat.c.orig 2013-06-01 07:35:00.000000000 -0600
++++ ./picosat.c 2013-07-31 14:26:09.000000000 -0600
+@@ -6673,7 +6673,7 @@ check_trace_support_and_execute (PS * ps
(void) file;
(void) fmt;
(void) f;
@@ -53,7 +53,7 @@
#endif
}
-@@ -7214,7 +7214,7 @@ picosat_corelit (int int_lit)
+@@ -7360,7 +7360,7 @@ picosat_corelit (PS * ps, int int_lit)
return res;
}
#else
@@ -62,7 +62,7 @@
return 0;
#endif
}
-@@ -7250,7 +7250,7 @@ picosat_coreclause (int ocls)
+@@ -7396,7 +7396,7 @@ picosat_coreclause (PS * ps, int ocls)
return res;
}
#else
@@ -71,9 +71,9 @@
return 0;
#endif
}
---- ./picomus.c.orig 2012-08-12 08:06:23.000000000 -0600
-+++ ./picomus.c 2012-08-20 14:54:41.645922533 -0600
-@@ -193,9 +193,8 @@ int main (int argc, char ** argv) {
+--- ./picomus.c.orig 2013-06-01 07:35:00.000000000 -0600
++++ ./picomus.c 2013-07-31 14:26:09.000000000 -0600
+@@ -195,9 +195,8 @@ int main (int argc, char ** argv) {
"\n"
"This typically slows down this MUS extractor, since\n"
"it only relies on clause selector variables and\n"
diff --git a/picosat.spec b/picosat.spec
index 3658461..efa8b72 100644
--- a/picosat.spec
+++ b/picosat.spec
@@ -1,6 +1,6 @@
Name: picosat
-Version: 951
-Release: 2%{?dist}
+Version: 957
+Release: 1%{?dist}
Summary: A SAT solver
Group: Applications/Engineering
@@ -107,9 +107,6 @@ cp -p %{SOURCE1} %{SOURCE2} %{SOURCE3} $RPM_BUILD_ROOT%{_mandir}/man1
%postun libs -p /sbin/ldconfig
-# The LICENSE file is placed in the -libs package rather than the base package,
-# because the -libs package is always installed when the base package is
-# installed, but not vice versa.
%files
%{_bindir}/pico*
%{_mandir}/man1/picosat*
@@ -126,6 +123,10 @@ cp -p %{SOURCE1} %{SOURCE2} %{SOURCE3}
$RPM_BUILD_ROOT%{_mandir}/man1
%{_libdir}/libpicosat.so
%changelog
+* Wed Jul 31 2013 Jerry James <loganjerry(a)gmail.com> - 957-1
+- New upstream release
+- Remove comment that was being pulled into postun
+
* Thu Feb 14 2013 Fedora Release Engineering <rel-eng(a)lists.fedoraproject.org> -
951-2
- Rebuilt for
https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild
diff --git a/sources b/sources
index a1e0ad7..f06e750 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-eab092f83bcb083bce42e1a8873531b4 picosat-951.tar.gz
+6cb7d32a61b19e450961c689841aaccb picosat-957.tar.gz