commit ff245d93f47f913ee76dbdd9ddfa28f5780fc32e Author: Elan Ruusamäe <g...@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 <bi...@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 <bi...@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 _______________________________________________ pld-cvs-commit mailing list pld-cvs-commit@lists.pld-linux.org http://lists.pld-linux.org/mailman/listinfo/pld-cvs-commit