[minisat2] Add a man page, courtesy of the Debian maintainers. Build a shared library, and add -devel and -libs
Jerry James
jjames at fedoraproject.org
Fri Mar 1 22:10:12 UTC 2013
commit ed37227bdf2aa3f11711144c8f96196912e87b6f
Author: Jerry James <jamesjer at betterlinux.com>
Date: Fri Mar 1 15:09:51 2013 -0700
Add a man page, courtesy of the Debian maintainers.
Build a shared library, and add -devel and -libs packages (bz 912190).
minisat.1 | 90 ++++++++++++++++++++++++++++++++++++++++++++++
minisat2-sharedlib.patch | 58 +++++++++++++++++++++++++++++
minisat2.spec | 76 +++++++++++++++++++++++++++++++++-----
3 files changed, 214 insertions(+), 10 deletions(-)
---
diff --git a/minisat.1 b/minisat.1
new file mode 100644
index 0000000..57b1be4
--- /dev/null
+++ b/minisat.1
@@ -0,0 +1,90 @@
+.\" Hey, EMACS: -*- nroff -*-
+.\" First parameter, NAME, should be all caps
+.\" Second parameter, SECTION, should be 1-8, maybe w/ subsection
+.\" other parameters are allowed: see man(7), man(1)
+.TH MINISAT2 1 "June 7, 2008"
+.\" Please adjust this date whenever revising the manpage.
+.\"
+.\" Some roff macros, for reference:
+.\" .nh disable hyphenation
+.\" .hy enable hyphenation
+.\" .ad l left justify
+.\" .ad b justify to both left and right margins
+.\" .nf disable filling
+.\" .fi enable filling
+.\" .br insert line break
+.\" .sp <n> insert n+1 empty lines
+.\" for manpage-specific macros, see man(7)
+.SH NAME
+minisat2 \- fast and lightweight SAT solver
+.SH SYNOPSIS
+.B minisat2
+.RI [ options ] " input-file
+.I result-output-file
+.SH DESCRIPTION
+This manual page documents briefly the
+.B minisat2
+command. MiniSat is a minimalistic, open-source SAT solver, developed to help
+researchers and developers alike to get started on SAT. Winning all the
+industrial categories of the SAT 2005 competition, MiniSat is a good starting
+point both for future research in SAT, and for applications using SAT.
+
+Despite the NP completeness of the satisfiabilty problem of Boolean formulas
+(SAT), SAT solvers are often able to decide this problem in a reasonable time
+frame. As all other NP complete problems are reducible to SAT, the solvers
+have become a general purpose tool for this class of problems.
+.PP
+.SH OPTIONS
+.B \-h, \-help
+Show summary of options.
+.TP
+.B \-pre {none,once}
+Disable or enable preprocessing.
+.TP
+.B \-asymm
+Unknown.
+.TP
+.B \-rcheck
+Enable checking for redundant clauses.
+.TP
+.B \-grow <num> [ >0 ]
+Number of additional clauses that may be introduced when eliminating a variable.
+Defaults to 0.
+.TP
+.B \-polarity-mode {true,false,rnd}
+Set default polarity for decisions made (true, false, or random).
+.TP
+.B \-decay <num> [ 0 - 1 ]
+Inverse of the variable activity decay factor (defaults to 0.95).
+.TP
+.B \-rnd-freq <num> [ 0 - 1 ]
+The frequency with which the decision heuristic tries to choose a random
+variable (defaults to 0.02).
+.TP
+.B \-freeze <freeze-file>
+File containing a list of literals to be frozen at the given polarity.
+.TP
+.B \-dimacs <output-file>
+Print (possibly preprocessed) input problem in DIMACS format.
+.TP
+.B \-verbosity {0,1,2}
+Set the verbosity of informational output.
+.PP
+.SH EXIT CODES
+.B 0
+if parsing the command line options fails, usage information is requested, or
+output of the input problem in dimacs format succeeds.
+.B 1
+if interrupted by SIGINT or if an input file cannot be read,
+.B 3
+if parsing the input fails,
+.B 10
+if found satisfiable, and
+.B 20
+if found unsatisfiable.
+.PP
+.SH AUTHOR
+minisat2 was written by Niklas Een, Niklas Sorensson
+.PP
+This manual page was written by Michael Tautschnig <mt at debian.org>,
+for the Debian project (but may be used by others).
diff --git a/minisat2-sharedlib.patch b/minisat2-sharedlib.patch
new file mode 100644
index 0000000..206eef5
--- /dev/null
+++ b/minisat2-sharedlib.patch
@@ -0,0 +1,58 @@
+--- mtl/template.mk.orig 2010-07-10 10:07:36.000000000 -0600
++++ mtl/template.mk 2013-03-01 14:59:16.048911115 -0700
+@@ -5,6 +5,8 @@
+ ## "make d" for a debug version (no optimizations).
+ ## "make" for the standard version (optimized, but with debug information and assertions active)
+
++VERSION =
++MAJVER = $(shell sed -r s/^\([[:digit:]]+\).*/\\1/ <<<$(VERSION))
+ PWD = $(shell pwd)
+ EXEC ?= $(notdir $(PWD))
+
+@@ -41,7 +43,7 @@
+ libr: lib$(LIB)_release.a
+
+ ## Compile options
+-%.o: CFLAGS +=$(COPTIMIZE) -g -D DEBUG
++%.o: CFLAGS +=$(COPTIMIZE) -g -D NDEBUG -fPIC
+ %.op: CFLAGS +=$(COPTIMIZE) -pg -g -D NDEBUG
+ %.od: CFLAGS +=-O0 -g -D DEBUG
+ %.or: CFLAGS +=$(COPTIMIZE) -g -D NDEBUG
+@@ -54,12 +56,13 @@
+ $(EXEC)_static: LFLAGS += --static
+
+ ## Dependencies
+-$(EXEC): $(COBJS)
++$(EXEC): lib$(LIB).so
+ $(EXEC)_profile: $(PCOBJS)
+ $(EXEC)_debug: $(DCOBJS)
+ $(EXEC)_release: $(RCOBJS)
+ $(EXEC)_static: $(RCOBJS)
+
++lib$(LIB).so: $(filter-out */Main.o, $(COBJS))
+ lib$(LIB)_standard.a: $(filter-out */Main.o, $(COBJS))
+ lib$(LIB)_profile.a: $(filter-out */Main.op, $(PCOBJS))
+ lib$(LIB)_debug.a: $(filter-out */Main.od, $(DCOBJS))
+@@ -72,11 +75,21 @@
+ @$(CXX) $(CFLAGS) -c -o $@ $<
+
+ ## Linking rules (standard/profile/debug/release)
+-$(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static:
++$(EXEC): Main.o
++ @echo Linking: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
++ @$(CXX) $< -o $@ -L. -l$(LIB) $(LFLAGS)
++
++$(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static:
+ @echo Linking: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
+ @$(CXX) $^ $(LFLAGS) -o $@
+
+ ## Library rules (standard/profile/debug/release)
++lib$(LIB).so: $(COBJS)
++ @echo Making library: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
++ @$(CXX) -shared -Wl,-soname=$@.$(MAJVER) -o $@.$(VERSION) $^ $(LFLAGS)
++ @ln -s lib$(LIB).so.$(VERSION) lib$(LIB).so.$(MAJVER)
++ @ln -s lib$(LIB).so.$(MAJVER) lib$(LIB).so
++
+ lib$(LIB)_standard.a lib$(LIB)_profile.a lib$(LIB)_release.a lib$(LIB)_debug.a:
+ @echo Making library: "$@ ( $(foreach f,$^,$(subst $(MROOT)/,,$f)) )"
+ @$(AR) -rcsv $@ $^
diff --git a/minisat2.spec b/minisat2.spec
index 59dad44..9d287b2 100644
--- a/minisat2.spec
+++ b/minisat2.spec
@@ -2,7 +2,7 @@
Name: minisat2
Version: 2.2.0
-Release: 4%{?dist}
+Release: 5%{?dist}
Summary: Minimalistic SAT solver
License: MIT
@@ -12,11 +12,16 @@ Source0: http://minisat.se/downloads/%{myname}-%{version}.tar.gz
# Sent sources, test, patches (below) to upstream via email on 2008-07-08:
Source1: http://www.dwheeler.com/essays/minisat-user-guide-1.0.html
Source2: minisat2-test.in
+# Man page courtesy of Debian
+Source3: minisat.1
# Don't try to set the FPU to double precision unless the target CPU supports
# that operation
-Patch0: minisat2-FPU.patch
+Patch0: %{name}-FPU.patch
+# Build a shared library
+Patch1: %{name}-sharedlib.patch
BuildRequires: zlib-devel
+Requires: %{name}-libs%{?_isa} = %{version}-%{release}
%description
MiniSat is a minimalistic, open-source Boolean satisfiability problem
@@ -33,9 +38,26 @@ set of assignments that make the expression true. Although the problem
is NP-complete, SAT solvers (like this one) are often able to decide
this problem in a reasonable time frame.
+%package libs
+Summary: Minimalistic SAT solver library
+Group: System Environment/Libraries
+
+%description libs
+The MiniSat library.
+
+%package devel
+Summary: Development files for %{name}
+Group: Development/Libraries
+Requires: %{name}-libs%{?_isa} = %{version}-%{release}
+
+%description devel
+The %{name}-devel package contains libraries and header files for
+developing applications that use %{name}.
+
%prep
%setup -q -n minisat
%patch0
+%patch1
cp -p %{SOURCE1} minisat-user-guide.html
cp -p %{SOURCE2} .
@@ -45,21 +67,39 @@ sed -i 's/@$(CXX)/$(CXX)/' mtl/template.mk
%build
# Build "simp", which adds simplification capabilities, instead of just "core"
-make %{?_smp_mflags} -C simp r \
+make %{?_smp_mflags} -C simp s \
MROOT=`pwd` \
COPTIMIZE="$RPM_OPT_FLAGS" \
+ VERSION=%{version} \
+ LIB=%{myname} \
LFLAGS="$RPM_LD_FLAGS -lz"
-cp -p simp/%{myname}_release %{myname}
%install
mkdir -p $RPM_BUILD_ROOT%{_bindir}
-install -m 0755 %{myname} $RPM_BUILD_ROOT%{_bindir}
+install -m 0755 simp/%{myname} $RPM_BUILD_ROOT%{_bindir}
+
+mkdir -p $RPM_BUILD_ROOT%{_mandir}/man1
+install -m 0644 %{SOURCE3} $RPM_BUILD_ROOT%{_mandir}/man1
+
+mkdir -p $RPM_BUILD_ROOT%{_libdir}
+cp -dp simp/lib%{myname}.so* $RPM_BUILD_ROOT%{_libdir}
+chmod 0755 $RPM_BUILD_ROOT%{_libdir}/lib%{myname}.so.%{version}
+
+mkdir -p $RPM_BUILD_ROOT%{_includedir}/%{myname}/core
+cp -p core/*.h $RPM_BUILD_ROOT%{_includedir}/%{myname}/core
+mkdir -p $RPM_BUILD_ROOT%{_includedir}/%{myname}/mtl
+cp -p mtl/*.h $RPM_BUILD_ROOT%{_includedir}/%{myname}/mtl
+mkdir -p $RPM_BUILD_ROOT%{_includedir}/%{myname}/simp
+cp -p simp/*.h $RPM_BUILD_ROOT%{_includedir}/%{myname}/simp
+mkdir -p $RPM_BUILD_ROOT%{_includedir}/%{myname}/utils
+cp -p utils/*.h $RPM_BUILD_ROOT%{_includedir}/%{myname}/utils
%check
# Test "minisat2-test.in" is a brief quote from
# http://www.satcompetition.org/2004/format-solvers2004.html
# Exit value is 10 for satisfiable, 20 for unsatisfiable
-./minisat minisat2-test.in minisat2-test.out || true
+export LD_LIBRARY_PATH=$RPM_BUILD_ROOT%{_libdir}
+simp/minisat minisat2-test.in minisat2-test.out || true
echo
echo "RESULTS:"
cat minisat2-test.out
@@ -72,15 +112,31 @@ else
false
fi
+%post libs -p /sbin/ldconfig
+
+%postun libs -p /sbin/ldconfig
+
%files
-%doc LICENSE
%doc doc/ReleaseNotes-2.2.0.txt
%doc minisat-user-guide.html
%doc minisat2-test.in
%doc minisat2-test.out
-%attr(755,root,root) %{_bindir}/%{myname}
+%{_bindir}/%{myname}
+%{_mandir}/man1/minisat.1*
+
+%files libs
+%doc LICENSE
+%{_libdir}/lib%{myname}.so.*
+
+%files devel
+%{_includedir}/%{myname}/
+%{_libdir}/lib%{myname}.so
%changelog
+* Fri Mar 1 2013 Jerry James <loganjerry at gmail.com> - 2.2.0-5
+- Add a man page, courtesy of the Debian maintainers
+- Build a shared library, and add -devel and -libs packages (bz 912190)
+
* Thu Feb 14 2013 Fedora Release Engineering <rel-eng at lists.fedoraproject.org> - 2.2.0-4
- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild
@@ -106,10 +162,10 @@ fi
* Wed Feb 25 2009 Fedora Release Engineering <rel-eng at lists.fedoraproject.org> - 2.0-8.20070721
- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild
-* Tue Aug 7 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-7.20070721
+* Thu Aug 7 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-7.20070721
- Removed code for switching between -O2 and -O3, per reviewer request.
-* Tue Aug 7 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-6.20070721
+* Thu Aug 7 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-6.20070721
- Timing tests found -O3 was unhelpful; switched back to -O2, but left stub
in case a switch to another -O level would help in the future.
-O3 real 0m35.714s, 0m35.714s, 0m35.834s vs. -O2 real 0m35.296s, 0m35.301s
More information about the scm-commits
mailing list