rpms/picosat/F-12 picosat-proof-access.patch, NONE, 1.1 picosat-sharedlib.patch, NONE, 1.1 picosat.1, NONE, 1.1 picosat.spec, NONE, 1.1 .cvsignore, 1.1, 1.2 sources, 1.1, 1.2

Tue Jan 19 20:54:10 UTC 2010

Author: jjames

Update of /cvs/pkgs/rpms/picosat/F-12
In directory cvs1.fedora.phx.redhat.com:/tmp/cvs-serv30453/F-12

Modified Files:
	.cvsignore sources 
Added Files:
	picosat-proof-access.patch picosat-sharedlib.patch picosat.1 
	picosat.spec 
Log Message:
Initial import into F-11 and F-12 branches.


picosat-proof-access.patch:
 picosat.c |  154 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 picosat.h |    6 ++
 2 files changed, 160 insertions(+)

--- NEW FILE picosat-proof-access.patch ---
diff -dur picosat-913.ORIG/picosat.c picosat-913/picosat.c
--- picosat-913.ORIG/picosat.c	2009-07-13 07:04:44.000000000 -0600
+++ picosat-913/picosat.c	2009-09-02 12:24:48.428654095 -0600
@@ -6112,6 +6112,160 @@
 #endif
 }
 
+/**
+ * method to access the zhains without printing to a file
+ */
+
+static int* proof = NULL;
+static int cursor = 0;
+#define PROOF_BLOCK 10000
+static int current_size;
+static void add_int_to_proof(int i)
+{
+  if(cursor >= current_size){
+    current_size += PROOF_BLOCK;
+    proof = realloc(proof, current_size);
+  }
+  proof[cursor] = i;
+  cursor++;
+}
+
+static int
+my_write_idx (unsigned idx)
+{
+  return EXPORTIDX (idx);
+}
+static void
+my_trace_lits (Cls * cls)
+{
+  Lit **p, **eol = end_of_lits (cls);
+
+  assert (cls);
+  assert (cls->core);
+
+  for (p = cls->lits; p < eol; p++)
+    {
+      int lit = LIT2INT (*p);
+      add_int_to_proof(lit);
+    }
+
+  add_int_to_proof(0);
+}
+static void
+my_trace_zhain (unsigned idx, Zhn * zhain)
+{
+  unsigned prev, this, delta, i;
+  Znt *p, byte;
+  Cls * cls;
+
+  assert (zhain);
+  assert (zhain->core);
+
+  int id = my_write_idx (idx);
+  add_int_to_proof(id);
+
+  cls = IDX2CLS (idx);
+  assert (cls);
+  my_trace_lits (cls);
+
+  i = 0;
+  delta = 0;
+  prev = 0;
+
+  for (p = zhain->znt; (byte = *p); p++, i += 7)
+    {
+      delta |= (byte & 0x7f) << i;
+      if (byte & 0x80)
+	continue;
+
+      this = prev + delta;
+
+      int id = my_write_idx (this);
+      add_int_to_proof(id);
+
+      prev = this;
+      delta = 0;
+      i = -7;
+    }
+
+  add_int_to_proof(0);
+  
+}
+static void
+my_trace_clause (unsigned idx, Cls * cls)
+{
+  assert (cls);
+  assert (cls->core);
+  assert (!cls->learned);
+  assert (CLS2IDX (cls) == idx);
+
+  int id = my_write_idx (idx);
+  add_int_to_proof(id);
+
+  my_trace_lits (cls);
+
+  add_int_to_proof(0);
+
+}
+static int*
+get_proof()
+{
+#ifdef TRACE
+  if (proof != NULL){
+    free(proof);
+  }
+  proof = malloc(PROOF_BLOCK * (sizeof(int)));
+  current_size = PROOF_BLOCK;
+  cursor = 0;
+
+
+  Cls *cls, ** p;
+  Zhn *zhain;
+  unsigned i;
+
+  core ();
+
+  for (p = SOC; p != EOC; p = NXC (p))
+    {
+      cls = *p;
+
+      if (oclauses <= p && p < eoo)
+	{
+	  i = OIDX2IDX (p - oclauses);
+	  assert (!cls || CLS2IDX (cls) == i);
+	}
+      else
+	{
+          assert (lclauses <= p && p < eol);
+	  i = LIDX2IDX (p - lclauses);
+	}
+
+      zhain = IDX2ZHN (i);
+
+      if (zhain)
+	{
+	  if (zhain->core)
+	    {
+		my_trace_zhain (i, zhain);
+	    }
+	}
+      else if (cls)
+	{
+	  if (cls->core)
+	    my_trace_clause (i, cls);
+	}
+    }
+  add_int_to_proof(EOP);
+  return proof;
+#endif
+}
+int *
+picosat_get_proof(){
+  return get_proof();
+}
+////
+
+
 static void
 write_core_wrapper (FILE * file, int fmt)
 {
diff -dur picosat-913.ORIG/picosat.h picosat-913/picosat.h
--- picosat-913.ORIG/picosat.h	2009-07-13 07:04:44.000000000 -0600
+++ picosat-913/picosat.h	2009-09-02 12:24:27.959725988 -0600
@@ -178,6 +178,12 @@
  */
 void picosat_adjust (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();
 /*------------------------------------------------------------------------*/
 /* Statistics.
  */

picosat-sharedlib.patch:
 makefile.in |   14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

--- NEW FILE picosat-sharedlib.patch ---
diff -dur picosat-913.ORIG/makefile.in picosat-913/makefile.in
--- picosat-913.ORIG/makefile.in	2009-07-13 07:04:44.000000000 -0600
+++ picosat-913/makefile.in	2009-09-02 12:29:45.851603078 -0600
@@ -1,14 +1,15 @@
 CC=@CC@
 CFLAGS=@CFLAGS@
+SONAME=-Xlinker -soname -Xlinker libpicosat.so.0
 
-all: picosat libpicosat.a
+all: picosat libpicosat.so
 
 clean:
 	rm -f picosat *.exe *.s *.o *.a *.so
 	rm -f makefile config.h
 	rm -f gmon.out *~ 
 
-picosat: libpicosat.a app.o main.o
+picosat: libpicosat.so app.o main.o
 	$(CC) $(CFLAGS) -o $@ main.o app.o -L. -lpicosat
 
 app.o: app.c picosat.h makefile
@@ -18,16 +19,15 @@
 	$(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 # and actually picosat.c
 	rm -f $@; ./mkconfig > $@
 
-libpicosat.a: picosat.o version.o
-	ar rc $@ picosat.o version.o
-	ranlib $@
+libpicosat.so: picosat.o version.o
+	$(CC) $(CFLAGS) -shared -o $@ picosat.o version.o $(SONAME)
 
 .PHONY: all clean


--- NEW FILE picosat.1 ---
.TH "PICOSAT" "1" "Version 913" "PicoSAT" "User Commands"
.SH "NAME"
picosat \- Satisfiability (SAT) solver for boolean variables
.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.

.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

.TP 
.BI \-T " <trace>"
generate extended proof trace file

.TP 
.BI \-r " <trace>"
generate reverse unit propagation proof file

.TP 
.BI \-c " <core>"
generate clausal core file in DIMACS format

.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"
.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 
minisat2(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.



--- NEW FILE picosat.spec ---
Name:           picosat
Version:        913
Release:        2%{?dist}
Summary:        A SAT solver

Group:          Applications/Engineering
License:        MIT
URL:            http://fmv.jku.at/picosat/
Source0:        http://fmv.jku.at/picosat/%{name}-%{version}.tar.gz
# Thanks to David Wheeler for the man page.
Source1:        picosat.1
# This patch was sent upstream on 2 June 2009 and (mostly) incorporated into
# the unreleased upstream version 917.  It does the following:
# - Links the binary against a shared library instead of a static library.
# - Does not build the static library.
# - Gives the resulting library an soname.
Patch0:         picosat-sharedlib.patch
# This patch is needed by csisat.  I asked upstream about it on 2 June 2009,
# and they tell me that the next release of picosat will include this
# functionality, although implemented differently.  Until that release, and
# the corresponding adapation of the csisat code, though, we need this patch.
Patch1:         picosat-proof-access.patch
BuildRoot:      %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)

# gzip required (see app.c); find-requires can't see into C code to find it
Requires:       gzip, %{name}-libs = %{version}-%{release}

%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 libs
Group:          Development/Libraries
Summary:        A SAT solver library

%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
Group:          Development/Libraries
Summary:        Development files for PicoSAT
Requires:       %{name}-libs = %{version}-%{release}

%description devel
Headers and other develpment files for PicoSAT.

%prep
%setup -q
%patch0 -p1
%patch1 -p1

%build
# The configure script is NOT autoconf-generated and chooses its own CFLAGS,
# so we mimic its effects instead of using it.
sed -e "s/@CC@/gcc/" \
    -e "s/@CFLAGS@/${RPM_OPT_FLAGS} -DSTATS -DTRACE -DNDEBUG/" \
    -e "s/@TARGETS@/picosat libpicosat.so/" \
  makefile.in > makefile
make %{?_smp_mflags}

%install
rm -rf $RPM_BUILD_ROOT

# Install the header file
mkdir -p $RPM_BUILD_ROOT%{_includedir}
cp -p picosat.h $RPM_BUILD_ROOT%{_includedir}

# Install the library
mkdir -p $RPM_BUILD_ROOT%{_libdir}
cp -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 binary
mkdir -p $RPM_BUILD_ROOT%{_bindir}
cp -p picosat $RPM_BUILD_ROOT%{_bindir}

# Install the man page
mkdir -p $RPM_BUILD_ROOT%{_mandir}/man1
cp -p %{SOURCE1} $RPM_BUILD_ROOT%{_mandir}/man1

%post libs -p /sbin/ldconfig

%postun libs -p /sbin/ldconfig

%clean
rm -rf $RPM_BUILD_ROOT

# 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
%defattr(-,root,root,-)
%{_bindir}/picosat
%{_mandir}/man1/picosat.1*

%files libs
%defattr(-,root,root,-)
%doc LICENSE NEWS
%{_libdir}/libpicosat.so.*

%files devel
%defattr(-,root,root,-)
%{_includedir}/picosat.h
%{_libdir}/libpicosat.so

%changelog
* Tue Jan 19 2010 Jerry James <loganjerry at gmail.com> - 913-2
- Spec file cleanups from review
- Man page courtesy of David Wheeler

* Wed Sep  2 2009 Jerry James <loganjerry at gmail.com> - 913-1
- Initial RPM


Index: .cvsignore
===================================================================
RCS file: /cvs/pkgs/rpms/picosat/F-12/.cvsignore,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- .cvsignore	19 Jan 2010 19:27:47 -0000	1.1
+++ .cvsignore	19 Jan 2010 20:54:09 -0000	1.2
@@ -0,0 +1 @@
+picosat-913.tar.gz


Index: sources
===================================================================
RCS file: /cvs/pkgs/rpms/picosat/F-12/sources,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -p -r1.1 -r1.2
--- sources	19 Jan 2010 19:27:47 -0000	1.1
+++ sources	19 Jan 2010 20:54:10 -0000	1.2
@@ -0,0 +1 @@
+e658fa16cd71ff2cafae190a905a93c6  picosat-913.tar.gz

