[packages/picosat] new, version 6bc069c
glen
glen at pld-linux.org
Sat Dec 1 23:31:04 CET 2018
commit ff245d93f47f913ee76dbdd9ddfa28f5780fc32e
Author: Elan Ruusamäe <glen at pld-linux.org>
Date: Sun Dec 2 00:30:39 2018 +0200
new, version 6bc069c
based on fedora package
picomus.1 | 55 ++++++++++++++
picosat-trace.patch | 90 +++++++++++++++++++++++
picosat.1 | 202 ++++++++++++++++++++++++++++++++++++++++++++++++++++
picosat.spec | 164 ++++++++++++++++++++++++++++++++++++++++++
picosat.trace.1 | 1 +
5 files changed, 512 insertions(+)
---
diff --git a/picosat.spec b/picosat.spec
new file mode 100644
index 0000000..87f8edb
--- /dev/null
+++ b/picosat.spec
@@ -0,0 +1,164 @@
+Summary: A SAT solver
+Name: picosat
+Version: 965
+Release: 1
+License: MIT
+Group: Applications
+Source0: http://fmv.jku.at/picosat/%{name}-%{version}.tar.gz
+# Source0-md5: d37c236d5c60b03d888d137c2fa4285f
+Source1: %{name}.1
+Source2: %{name}.trace.1
+Source3: picomus.1
+Patch0: %{name}-trace.patch
+URL: http://fmv.jku.at/picosat/
+BuildRequires: R
+Requires: %{name}-libs = %{version}-%{release}
+Requires: bzip2
+Requires: gzip
+BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
+
+%description
+PicoSAT solves the SAT problem, which is the classical NP complete
+problem of searching for a satisfying assignment of a propositional
+formula in conjunctive normal form (CNF). PicoSAT can generate proofs
+and cores in memory by compressing the proof trace. It supports the
+proof format of TraceCheck.
+
+%package -n R-picosat
+Summary: A SAT solver library for R
+Group: Libraries
+
+%description -n R-picosat
+The PicoSAT library, which contains routines that solve the SAT
+problem. The library has a simple API which is similar to that of
+previous solvers by the same authors.
+
+This version of the library is built for use with R projects.
+
+%package libs
+Summary: A SAT solver library
+Group: Libraries
+
+%description libs
+The PicoSAT library, which contains routines that solve the SAT
+problem. The library has a simple API which is similar to that of
+previous solvers by the same authors.
+
+%package devel
+Summary: Development files for PicoSAT
+Group: Development/Libraries
+Requires: %{name}-libs = %{version}-%{release}
+Requires: R-%{name} = %{version}-%{release}
+
+%description devel
+Headers and other development files for PicoSAT.
+
+%prep
+%setup -q
+%patch0
+
+%build
+# The configure script is NOT autoconf-generated and chooses its own CFLAGS,
+# so we mimic its effects instead of using it.
+
+# Build the version with R support
+sed -e "s/@CC@/gcc/" \
+ -e "s|@CFLAGS@|$RPM_OPT_FLAGS -D_GNU_SOURCE=1 -DNDEBUG -DRCODE -I%{_includedir}/R|" \
+ -e "s|-Xlinker libpicosat.so|-Xlinker libpicosat.so.0 $RPM_LD_FLAGS -L%{_libdir}/R/lib -lR|" \
+ -e "s/libpicosat/libpicosat-R/g" \
+ -e "s/-lpicosat/-lpicosat-R/g" \
+ -e "s/@TARGETS@/libpicosat-R.so/" \
+ makefile.in > makefile
+%{__make}
+
+# Build the version with trace support
+sed -e "s/@CC@/gcc/" \
+ -e "s|@CFLAGS@|$RPM_OPT_FLAGS -D_GNU_SOURCE=1 -DNDEBUG -DTRACE|" \
+ -e "s|-Xlinker libpicosat.so|-Xlinker libpicosat.so.0 $RPM_LD_FLAGS|" \
+ -e "s/libpicosat/libpicosat-trace/g" \
+ -e "s/-lpicosat/-lpicosat-trace/g" \
+ -e "s/@TARGETS@/libpicosat-trace.so picosat picomus/" \
+ makefile.in > makefile
+%{__make}
+mv picosat picosat.trace
+
+# Build the fast version.
+# Note that picomus needs trace support, so we don't rebuild it.
+rm -f *.o *.s config.h
+sed -e "s/@CC@/gcc/" \
+ -e "s|@CFLAGS@|$RPM_OPT_FLAGS -D_GNU_SOURCE=1 -DNDEBUG|" \
+ -e "s|-Xlinker libpicosat.so|-Xlinker libpicosat.so.0 $RPM_LD_FLAGS|" \
+ -e "s/@TARGETS@/libpicosat.so picosat picomcs picogcnf/" \
+ makefile.in > makefile
+%{__make}
+
+%install
+rm -rf $RPM_BUILD_ROOT
+# Install the header file
+install -d $RPM_BUILD_ROOT%{_includedir}
+cp -p picosat.h $RPM_BUILD_ROOT%{_includedir}
+
+# Install the libraries
+install -d $RPM_BUILD_ROOT%{_libdir}
+install -p libpicosat-R.so \
+ $RPM_BUILD_ROOT%{_libdir}/libpicosat-R.so.0.0.%{version}
+ln -s libpicosat-R.so.0.0.%{version} $RPM_BUILD_ROOT%{_libdir}/libpicosat-R.so.0
+ln -s libpicosat-R.so.0 $RPM_BUILD_ROOT%{_libdir}/libpicosat-R.so
+install -p libpicosat-trace.so \
+ $RPM_BUILD_ROOT%{_libdir}/libpicosat-trace.so.0.0.%{version}
+ln -s libpicosat-trace.so.0.0.%{version} $RPM_BUILD_ROOT%{_libdir}/libpicosat-trace.so.0
+ln -s libpicosat-trace.so.0 $RPM_BUILD_ROOT%{_libdir}/libpicosat-trace.so
+install -p libpicosat.so \
+ $RPM_BUILD_ROOT%{_libdir}/libpicosat.so.0.0.%{version}
+ln -s libpicosat.so.0.0.%{version} $RPM_BUILD_ROOT%{_libdir}/libpicosat.so.0
+ln -s libpicosat.so.0 $RPM_BUILD_ROOT%{_libdir}/libpicosat.so
+
+# Install the binaries
+install -d $RPM_BUILD_ROOT%{_bindir}
+install -p picosat picosat.trace picomus picomcs picogcnf \
+ $RPM_BUILD_ROOT%{_bindir}
+
+# Install the man pages
+install -d $RPM_BUILD_ROOT%{_mandir}/man1
+cp -p %{SOURCE1} %{SOURCE2} %{SOURCE3} $RPM_BUILD_ROOT%{_mandir}/man1
+
+%post libs -p /sbin/ldconfig
+%postun libs -p /sbin/ldconfig
+
+%post -n R-picosat -p /sbin/ldconfig
+%postun -n R-picosat -p /sbin/ldconfig
+
+%clean
+rm -rf $RPM_BUILD_ROOT
+
+%files
+%defattr(644,root,root,755)
+%attr(755,root,root) %{_bindir}/picogcnf
+%attr(755,root,root) %{_bindir}/picomcs
+%attr(755,root,root) %{_bindir}/picomus
+%attr(755,root,root) %{_bindir}/picosat
+%attr(755,root,root) %{_bindir}/picosat.trace
+%{_mandir}/man1/picomus.1*
+%{_mandir}/man1/picosat.1*
+%{_mandir}/man1/picosat.trace.1
+
+%files libs
+%defattr(644,root,root,755)
+%doc NEWS LICENSE
+%ghost %{_libdir}/libpicosat.so.0
+%attr(755,root,root) %{_libdir}/libpicosat.so.*.*.*
+%ghost %{_libdir}/libpicosat-trace.so.0
+%attr(755,root,root) %{_libdir}/libpicosat-trace.so.*.*.*
+
+%files devel
+%defattr(644,root,root,755)
+%{_includedir}/picosat.h
+%{_libdir}/libpicosat.so
+%{_libdir}/libpicosat-trace.so
+%{_libdir}/libpicosat-R.so
+
+%files -n R-picosat
+%defattr(644,root,root,755)
+%doc NEWS LICENSE
+%attr(755,root,root) %{_libdir}/libpicosat-R.so.*.*.*
+%ghost %{_libdir}/libpicosat-R.so.0
diff --git a/picomus.1 b/picomus.1
new file mode 100644
index 0000000..0e38fc8
--- /dev/null
+++ b/picomus.1
@@ -0,0 +1,55 @@
+.TH "PICOMUS" "1" "Version 936" "PicoSAT" "User Commands"
+.SH "NAME"
+picomus \- Minimal Unsatisfiable Core (MUS) generator
+.SH "SYNOPSIS"
+.B picomus
+[\fIOPTION\fR]... [\fIINPUT\fR [\fIOUTPUT\fR]]
+.SH "DESCRIPTION"
+.\" Add any additional description here
+.PP
+PicoMUS is a satisfiability (SAT) solver that generates a minimal unsatisfiable
+core, using the PicoSAT library.
+
+.SH "OPTIONS"
+.TP
+.BI \-h
+print this command line option summary and exit
+
+.TP
+.BI \-v
+enable verbose output
+
+.PP
+If no input filename is given, or the input filename is "-", then standard
+input is used. If the output filename is "-", then standard output is used.
+If no output filename is given, then the MUS is computed but not printed.
+
+.SH "CONFORMING TO"
+.PP
+This program uses DIMACS CNF format as input. The output conforms to the
+standard SAT solver format used at SAT competitions.
+
+.SH "EXIT STATUS"
+.PP
+The output is a number of lines.
+Most of these will begin with "c" (comment), and give detailed
+technical information.
+The output line beginning with "s" declares whether or not
+it is satisfiable.
+The line "s SATISFIABLE" is produced if it is satisfiable
+(exit status 10),
+and "s UNSATISFIABLE" is produced if it is not satisfiable
+(exit status 20).
+
+.SH "AUTHORS"
+picomus was written by Armin Biere <biere at jku.at>
+.PP
+This man page was written by Jerry James.
+It is released to the public domain; you may use it in any way you wish.
+
+.SH "SEE ALSO"
+.PP
+\fIpicosat\fP(1), \fIminisat2\fP(1).
+
+.\" This documentation was written by Jerry James in 2011, and
+.\" is released to the public domain. Anyone can use it, in any way.
diff --git a/picosat-trace.patch b/picosat-trace.patch
new file mode 100644
index 0000000..1d4638f
--- /dev/null
+++ b/picosat-trace.patch
@@ -0,0 +1,90 @@
+# This patch has not been sent upstream. It is specific to Fedora's build of
+# two distinct binaries, one with trace support and one without.
+
+--- ./makefile.in.orig 2016-01-13 00:19:13.000000000 -0700
++++ ./makefile.in 2016-01-13 19:45:19.860821928 -0700
+@@ -12,16 +12,16 @@ clean:
+ analyze:
+ clang --analyze $(CFLAGS) *.c *.h
+
+-picosat: libpicosat.a app.o main.o
++picosat: libpicosat.so app.o main.o
+ $(CC) $(CFLAGS) -o $@ main.o app.o -L. -lpicosat
+
+-picomcs: libpicosat.a picomcs.o
++picomcs: libpicosat.so picomcs.o
+ $(CC) $(CFLAGS) -o $@ picomcs.o -L. -lpicosat
+
+-picomus: libpicosat.a picomus.o
++picomus: libpicosat.so picomus.o
+ $(CC) $(CFLAGS) -o $@ picomus.o -L. -lpicosat
+
+-picogcnf: libpicosat.a picogcnf.o
++picogcnf: libpicosat.so picogcnf.o
+ $(CC) $(CFLAGS) -o $@ picogcnf.o -L. -lpicosat
+
+ app.o: app.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
+- $(CC) $(CFLAGS) -c $<
++ $(CC) $(CFLAGS) -fPIC -c $<
+
+ version.o: version.c config.h makefile
+- $(CC) $(CFLAGS) -c $<
++ $(CC) $(CFLAGS) -fPIC -c $<
+
+ config.h: makefile VERSION mkconfig.sh # and actually picosat.c
+ rm -f $@; ./mkconfig.sh > $@
+@@ -54,6 +54,6 @@ libpicosat.a: picosat.o version.o
+
+ SONAME=-Xlinker -soname -Xlinker libpicosat.so
+ libpicosat.so: picosat.o version.o
+- $(CC) $(CFLAGS) -shared -o $@ picosat.o version.o $(SONAME)
++ $(CC) $(CFLAGS) -fPIC -shared -o $@ picosat.o version.o $(SONAME)
+
+ .PHONY: all clean
+--- ./picomus.c.orig 2016-01-13 00:19:13.000000000 -0700
++++ ./picomus.c 2016-01-13 21:14:22.638231658 -0700
+@@ -193,9 +193,8 @@ static const char * USAGE =
+ "\n"
+ "This typically slows down this MUS extractor, since\n"
+ "it only relies on clause selector variables and\n"
+-"can not make use of core extraction. To enable\n"
+-"trace generation use './configure.sh --trace' or\n"
+-"'./configure.sh -O --trace' when building PicoSAT.\n"
++"can not make use of core extraction. To use trace\n"
++"support, run picomus.trace instead.\n"
+ #else
+ "Since trace generation code is included, this binary\n"
+ "uses also core extraction in addition to clause selector\n"
+--- ./picosat.c.orig 2016-01-13 00:19:13.000000000 -0700
++++ ./picosat.c 2016-01-13 19:45:19.879820386 -0700
+@@ -6547,7 +6547,7 @@ check_trace_support_and_execute (PS * ps
+ (void) file;
+ (void) fmt;
+ (void) f;
+- ABORT ("compiled without trace support");
++ ABORT ("compiled without trace support; please use picosat.trace instead");
+ #endif
+ }
+
+@@ -7262,7 +7262,7 @@ picosat_corelit (PS * ps, int int_lit)
+ return res;
+ }
+ #else
+- ABORT ("compiled without trace support");
++ ABORT ("compiled without trace support; please use picosat.trace instead");
+ return 0;
+ #endif
+ }
+@@ -7298,7 +7298,7 @@ picosat_coreclause (PS * ps, int ocls)
+ return res;
+ }
+ #else
+- ABORT ("compiled without trace support");
++ ABORT ("compiled without trace support; please use picosat.trace instead");
+ return 0;
+ #endif
+ }
diff --git a/picosat.1 b/picosat.1
new file mode 100644
index 0000000..028703b
--- /dev/null
+++ b/picosat.1
@@ -0,0 +1,202 @@
+.TH "PICOSAT" "1" "Version 936" "PicoSAT" "User Commands"
+.SH "NAME"
+picosat \- Satisfiability (SAT) solver with proof and core support
+.SH "SYNOPSIS"
+.B picosat
+[\fIOPTION\fR]... [\fIFILE\fR]
+.SH "DESCRIPTION"
+.\" Add any additional description here
+.PP
+PicoSAT is a satisfiability (SAT) solver for boolean variables in
+boolean expressions.
+A SAT solver can determine if it is possible to find assignments to boolean
+variables that would make a given set of expressions true.
+If it's satisfiable, it can also show
+a set of assignments that make the expression true.
+Many problems can be broken down into a large SAT problem
+(perhaps with thousands of variables), so SAT solvers have a variety
+of uses.
+.PP
+The \fBpicosat\fP binary is built with options that provide for the greatest
+speed. A second binary, \fBpicosat.trace\fP, is built with proof and core
+capabilities, which incur some overhead.
+
+.SH "OPTIONS"
+.TP
+.BI \-h
+print this command line option summary and exit
+
+.TP
+.BI \-\-version
+print version and exit
+
+.TP
+.BI \-\-config
+print build configuration and exit
+
+.TP
+.BI \-v
+enable verbose output
+
+.TP
+.BI \-f
+ignore invalid header
+
+.TP
+.BI \-n
+do not print satisfying assignment
+
+.TP
+.BI \-p
+print formula in DIMACS format and exit
+
+.TP
+.BI \-a " <lit>"
+start with an assumption
+
+.TP
+.BI \-l " <limit>"
+set decision limit (no limit per default)
+
+.TP
+.BI \-i " <0|1>"
+force FALSE respectively TRUE as default phase
+
+.TP
+.BI \-s " <seed>"
+set random number generator seed (default 0)
+
+.TP
+.BI \-o " <output>"
+set output file (<stdout> per default)
+
+.TP
+.BI \-t " <trace>"
+generate compact proof trace file (use picosat.trace; see above)
+
+.TP
+.BI \-T " <trace>"
+generate extended proof trace file (use picosat.trace; see above)
+
+.TP
+.BI \-r " <trace>"
+generate reverse unit propagation proof file (use picosat.trace; see above)
+
+.TP
+.BI \-c " <core>"
+generate clausal core file in DIMACS format (use picosat.trace; see above)
+
+.TP
+.BI \-V " <core>"
+generate file listing core variables
+
+.TP
+.BI \-U " <core>"
+generate file listing used variables
+
+.PP
+If no input filename is given, standard input is used.
+
+.SH "CONFORMING TO"
+.PP
+This program uses DIMACS CNF format as input.
+.PP
+Like many SAT solvers, this program requires that its input be in
+conjunctive normal form (CNF or cnf) in DIMACS CNF format.
+CNF is built from these building blocks:
+.TP 3
+*
+.I R term :
+A term is either a boolean variable (e.g., x4)
+or a negated boolean variable (NOT x4, written here as \-x4).
+.TP
+*
+.I R clause :
+A clause is a set of one or more terms, connected with OR
+(written here as |); boolean variables may not repeat inside a clause.
+.TP
+*
+.I R expression :
+An expression is a set of one or more clauses,
+each connected by AND (written here as &).
+
+.PP
+Any boolean expression can be converted into CNF.
+
+.PP
+DIMACS CNF format is a simple text format for CNF.
+Every line beginning "c" is a comment.
+The first non\-comment line must be of the form:
+.PP
+ p cnf NUMBER_OF_VARIABLES NUMBER_OF_CLAUSES
+.PP
+Each of the non\-comment lines afterwards defines a clause.
+Each of these lines is a space\-separated list of variables;
+a positive value means that corresponding variable
+(so 4 means x4), and a negative value means the negation of that variable
+(so \-5 means \-x5).
+Each line must end in a space and the number 0.
+
+.SH "EXIT STATUS"
+.PP
+The output is a number of lines.
+Most of these will begin with "c" (comment), and give detailed
+technical information.
+The output line beginning with "s" declares whether or not
+it is satisfiable.
+The line "s SATISFIABLE" is produced if it is satisfiable
+(exit status 10),
+and "s UNSATISFIABLE" is produced if it is not satisfiable
+(exit status 20).
+.PP
+If it is satisfiable,
+the output line beginning with "v" declares a set of variable settings
+that satisfy all formulas.
+For example:
+.PP
+ v 1 \-2 \-3 \-4 5 0
+.PP
+Shows that there is a solution with variable 1 true, variables 2, 3, and 4
+false, and variable 5 true.
+
+.SH "EXAMPLE"
+.PP
+An example of CNF is:
+.PP
+ (x1 | \-x5 | x4) &
+ (\-x1 | x5 | x3 | x4) &
+ (\-x3 | x4).
+.PP
+The DIMACS CNF format for the above set of expressions could be:
+.PP
+ c Here is a comment.
+ p cnf 5 3
+ 1 \-5 4 0
+ \-1 5 3 4 0
+ \-3 \-4 0
+.PP
+The "p cnf" line above means that this is SAT problem in CNF format with
+5 variables and 3 clauses. The first line after it is the first clause,
+meaning x1 | \-x5 | x4.
+.PP
+CNFs with conflicting requirements are not satisfiable.
+For example, the following DIMACS CNF formatted data is not satisfiable,
+because it requires that variable 1 always be true and also always be false:
+.PP
+ c This is not satisfiable.
+ p cnf 2 2
+ \-1 0
+ 1 0
+
+.SH "AUTHORS"
+picosat was written by Armin Biere <biere at jku.at>
+.PP
+This man page was written by David A. Wheeler.
+It is released to the public domain; you may use it in any way you wish.
+
+.SH "SEE ALSO"
+.PP
+\fIpicomus\fP(1), \fIminisat2\fP(1).
+
+.\" This documentation was written by David A. Wheeler in 2010, and
+.\" is released to the public domain. Anyone can use it, in any way.
diff --git a/picosat.trace.1 b/picosat.trace.1
new file mode 100644
index 0000000..4c8637d
--- /dev/null
+++ b/picosat.trace.1
@@ -0,0 +1 @@
+.so picosat.1
================================================================
---- gitweb:
http://git.pld-linux.org/gitweb.cgi/packages/picosat.git/commitdiff/ff245d93f47f913ee76dbdd9ddfa28f5780fc32e
More information about the pld-cvs-commit
mailing list