rpms/cvc4
3
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

New upstream release.

Browse Source 
Also:
- Drop updated test files, now included upstream
- Drop obsolete workarounds for glpk compatibility
- Drop lfsc BR/R, as it has been incorporated into cvc4
This commit is contained in:
Jerry James 2015-01-02 16:57:48 -07:00
parent 9feb5dc450
commit f624faa170
8 changed files with 166 additions and 637 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.gitignore vendored
View File

@ -1 +1 @@
/cvc4-1.3.tar.gz
/cvc4-1.4.tar.gz

30
cvc4-abc.patch Normal file
View File

@ -0,0 +1,30 @@
--- ./configure.orig 2014-07-13 11:47:37.469270988 -0600
+++ ./configure 2015-01-01 21:00:00.000000000 -0700
@@ -19368,7 +19368,7 @@ See \`config.log' for more details" "$LI
fi
- if ! test -d "$ABC_HOME" || ! test -x "$ABC_HOME/arch_flags"; then
+ if ! test -d "$ABC_HOME" ; then
{ { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
$as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
as_fn_error $? "either $ABC_HOME is not an abc source tree or it's not yet built
@@ -19377,15 +19377,15 @@ See \`config.log' for more details" "$LI
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for arch_flags to use with libabc" >&5
$as_echo_n "checking for arch_flags to use with libabc... " >&6; }
- libabc_arch_flags="$("$ABC_HOME/arch_flags")"
+ libabc_arch_flags=""
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $libabc_arch_flags" >&5
$as_echo "$libabc_arch_flags" >&6; }
- CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$ABC_HOME/src $libabc_arch_flags"
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$ABC_HOME/include/abc"
ABC_LDFLAGS="-L$ABC_HOME"
cvc4_save_LDFLAGS="$LDFLAGS"
ABC_LIBS=
- CPPFLAGS="$CPPFLAGS -I$ABC_HOME/src $libabc_arch_flags"
+ CPPFLAGS="$CPPFLAGS -I$ABC_HOME/include/abc"
LDFLAGS="$LDFLAGS $ABC_LDFLAGS"
ac_fn_c_check_header_mongrel "$LINENO" "base/abc/abc.h" "ac_cv_header_base_abc_abc_h" "$ac_includes_default"
if test "x$ac_cv_header_base_abc_abc_h" = xyes; then :

124
cvc4-doxygen.patch
View File

@ -1,5 +1,5 @@
--- ./src/decision/options.h.orig 2013-12-06 16:07:43.586866550 -0700
+++ ./src/decision/options.h 2013-12-06 16:07:43.586866550 -0700
--- ./src/decision/options.h.orig 2014-07-13 11:48:44.263172259 -0600
+++ ./src/decision/options.h 2014-07-13 11:48:44.263172259 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -9,8 +9,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/expr/expr_manager_template.h.orig 2013-12-03 15:24:58.911994034 -0700
+++ ./src/expr/expr_manager_template.h 2013-12-03 15:24:58.911994034 -0700
--- ./src/expr/expr_manager_template.h.orig 2014-07-13 11:32:35.479585444 -0600
+++ ./src/expr/expr_manager_template.h 2014-07-13 11:32:35.479585444 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file expr_manager_template.h
@ -18,8 +18,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: Dejan Jovanovic
--- ./src/expr/expr_template.h.orig 2013-11-27 09:42:59.916302990 -0700
+++ ./src/expr/expr_template.h 2013-11-27 09:42:59.916302990 -0700
--- ./src/expr/expr_template.h.orig 2014-07-13 11:32:35.479585444 -0600
+++ ./src/expr/expr_template.h 2014-07-13 11:32:35.479585444 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file expr_template.h
@ -27,8 +27,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: Dejan Jovanovic
--- ./src/expr/kind_template.h.orig 2013-11-11 10:21:58.180347624 -0700
+++ ./src/expr/kind_template.h 2013-11-11 10:21:58.180347624 -0700
--- ./src/expr/kind_template.h.orig 2014-07-13 11:32:35.479585444 -0600
+++ ./src/expr/kind_template.h 2014-07-13 11:32:35.479585444 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file kind_template.h
@ -36,8 +36,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: Dejan Jovanovic
--- ./src/expr/options.h.orig 2013-12-06 16:07:22.010279788 -0700
+++ ./src/expr/options.h 2013-12-06 16:07:22.010279788 -0700
--- ./src/expr/options.h.orig 2014-07-13 11:48:13.930308852 -0600
+++ ./src/expr/options.h 2014-07-13 11:48:13.930308852 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -47,8 +47,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/main/options.h.orig 2013-12-06 16:07:45.234911367 -0700
+++ ./src/main/options.h 2013-12-06 16:07:45.234911367 -0700
--- ./src/main/options.h.orig 2014-07-13 11:48:47.275258010 -0600
+++ ./src/main/options.h 2014-07-13 11:48:47.275258010 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -58,8 +58,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/options/base_options.h.orig 2013-12-06 16:07:21.118255532 -0700
+++ ./src/options/base_options.h 2013-12-06 16:07:21.118255532 -0700
--- ./src/options/base_options.h.orig 2014-07-13 11:48:12.830277541 -0600
+++ ./src/options/base_options.h 2014-07-13 11:48:12.830277541 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -69,8 +69,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/options/base_options_template.h.orig 2013-11-11 10:21:58.276350312 -0700
+++ ./src/options/base_options_template.h 2013-11-11 10:21:58.276350312 -0700
--- ./src/options/base_options_template.h.orig 2014-07-13 11:32:35.579588292 -0600
+++ ./src/options/base_options_template.h 2014-07-13 11:32:35.579588292 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file base_options_template.h
@ -78,8 +78,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/options/options.h.orig 2013-11-11 10:21:58.284350536 -0700
+++ ./src/options/options.h 2013-11-11 10:21:58.284350536 -0700
--- ./src/options/options.h.orig 2014-07-01 12:37:15.061881767 -0600
+++ ./src/options/options.h 2014-07-01 12:37:15.061881767 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file options.h
@ -87,8 +87,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/parser/options.h.orig 2013-12-06 16:07:46.070934102 -0700
+++ ./src/parser/options.h 2013-12-06 16:07:46.070934102 -0700
--- ./src/parser/options.h.orig 2014-07-13 11:48:48.427290778 -0600
+++ ./src/parser/options.h 2014-07-13 11:48:48.427290778 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -98,8 +98,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/printer/options.h.orig 2013-12-06 16:07:39.042742975 -0700
+++ ./src/printer/options.h 2013-12-06 16:07:39.042742975 -0700
--- ./src/printer/options.h.orig 2014-07-13 11:48:37.070967532 -0600
+++ ./src/printer/options.h 2014-07-13 11:48:37.070967532 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -109,8 +109,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/proof/options.h.orig 2013-12-06 16:07:38.522728834 -0700
+++ ./src/proof/options.h 2013-12-06 16:07:38.522728834 -0700
--- ./src/proof/options.h.orig 2014-07-13 11:48:36.346946926 -0600
+++ ./src/proof/options.h 2014-07-13 11:48:36.346946926 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -120,8 +120,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/prop/options.h.orig 2013-12-06 16:07:38.086716977 -0700
+++ ./src/prop/options.h 2013-12-06 16:07:38.086716977 -0700
--- ./src/prop/options.h.orig 2014-07-13 11:48:35.870933374 -0600
+++ ./src/prop/options.h 2014-07-13 11:48:35.870933374 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -131,8 +131,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/smt/options.h.orig 2013-12-06 16:07:42.546838267 -0700
+++ ./src/smt/options.h 2013-12-06 16:07:42.546838267 -0700
--- ./src/smt/options.h.orig 2014-07-13 11:48:42.683127279 -0600
+++ ./src/smt/options.h 2014-07-13 11:48:42.683127279 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -142,8 +142,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/arith/options.h.orig 2013-12-06 16:07:28.406453727 -0700
+++ ./src/theory/arith/options.h 2013-12-06 16:07:28.406453727 -0700
--- ./src/theory/arith/options.h.orig 2014-07-13 11:48:23.866591680 -0600
+++ ./src/theory/arith/options.h 2014-07-13 11:48:23.866591680 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -153,8 +153,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/arrays/options.h.orig 2013-12-06 16:07:31.002524327 -0700
+++ ./src/theory/arrays/options.h 2013-12-06 16:07:31.002524327 -0700
--- ./src/theory/arrays/options.h.orig 2014-07-13 11:48:26.966679925 -0600
+++ ./src/theory/arrays/options.h 2014-07-13 11:48:26.966679925 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -164,8 +164,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/booleans/options.h.orig 2013-12-06 16:07:22.494292954 -0700
+++ ./src/theory/booleans/options.h 2013-12-06 16:07:22.494292954 -0700
--- ./src/theory/booleans/options.h.orig 2014-07-13 11:48:14.450323654 -0600
+++ ./src/theory/booleans/options.h 2014-07-13 11:48:14.450323654 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -175,8 +175,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/builtin/options.h.orig 2013-12-06 16:07:25.114364203 -0700
+++ ./src/theory/builtin/options.h 2013-12-06 16:07:25.114364203 -0700
--- ./src/theory/builtin/options.h.orig 2014-07-13 11:48:18.334434213 -0600
+++ ./src/theory/builtin/options.h 2014-07-13 11:48:18.334434213 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -186,8 +186,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/bv/options.h.orig 2013-12-06 16:07:24.114337006 -0700
+++ ./src/theory/bv/options.h 2013-12-06 16:07:24.114337006 -0700
--- ./src/theory/bv/options.h.orig 2014-07-13 11:48:17.270403926 -0600
+++ ./src/theory/bv/options.h 2014-07-13 11:48:17.270403926 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -197,8 +197,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/datatypes/options.h.orig 2013-12-06 16:07:24.714353323 -0700
+++ ./src/theory/datatypes/options.h 2013-12-06 16:07:24.714353323 -0700
--- ./src/theory/datatypes/options.h.orig 2014-07-13 11:48:17.930422713 -0600
+++ ./src/theory/datatypes/options.h 2014-07-13 11:48:17.930422713 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -208,8 +208,19 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/options.h.orig 2013-12-06 16:07:23.074308723 -0700
+++ ./src/theory/options.h 2013-12-06 16:07:23.074308723 -0700
--- ./src/theory/idl/options.h.orig 2014-07-13 11:48:49.099309909 -0600
+++ ./src/theory/idl/options.h 2014-07-13 11:48:49.099309909 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/idl/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/options.h.orig 2014-07-13 11:48:15.082341645 -0600
+++ ./src/theory/options.h 2014-07-13 11:48:15.082341645 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -219,8 +230,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/quantifiers/options.h.orig 2013-12-06 16:07:35.278640613 -0700
+++ ./src/theory/quantifiers/options.h 2013-12-06 16:07:35.278640613 -0700
--- ./src/theory/quantifiers/options.h.orig 2014-07-13 11:48:32.886848435 -0600
+++ ./src/theory/quantifiers/options.h 2014-07-13 11:48:32.886848435 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -230,19 +241,30 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/rewriterules/options.h.orig 2013-12-06 16:07:35.926658235 -0700
+++ ./src/theory/rewriterules/options.h 2013-12-06 16:07:35.926658235 -0700
--- ./src/theory/sets/options.h.orig 2014-07-13 11:48:49.839330972 -0600
+++ ./src/theory/sets/options.h 2014-07-13 11:48:49.839330972 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/rewriterules/options.h
+/*! \file theory/sets/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/uf/options.h.orig 2013-12-06 16:07:30.142500939 -0700
+++ ./src/theory/uf/options.h 2013-12-06 16:07:30.142500939 -0700
--- ./src/theory/strings/options.h.orig 2014-07-13 11:48:34.382891021 -0600
+++ ./src/theory/strings/options.h 2014-07-13 11:48:34.382891021 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
/********************* */
-/*! \file base_options_template.h
+/*! \file theory/strings/options.h
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/theory/uf/options.h.orig 2014-07-13 11:48:25.926650321 -0600
+++ ./src/theory/uf/options.h 2014-07-13 11:48:25.926650321 -0600
@@ -28,7 +28,7 @@
/* Edit the template file instead. */
@ -252,8 +274,8 @@
** \verbatim
** Original author: Morgan Deters
** Major contributors: none
--- ./src/util/tls.h.in.orig 2013-12-03 13:43:42.822811181 -0700
+++ ./src/util/tls.h.in 2013-12-03 13:43:42.822811181 -0700
--- ./src/util/tls.h.in.orig 2014-07-13 11:32:36.123603789 -0600
+++ ./src/util/tls.h.in 2014-07-13 11:32:36.123603789 -0600
@@ -1,5 +1,5 @@
/********************* */
-/*! \file tls.h.in

98
cvc4.spec
View File

@ -1,10 +1,13 @@
# CVC4 1.4 and later need a modified glpk, unavailable in Fedora. Therefore,
# we currently build without glpk support.
%ifarch %{ix86} x86_64 ppc ppc64
%global have_perftools 1
%endif
Name: cvc4
Version: 1.3
Release: 7%{?dist}
Version: 1.4
Release: 1%{?dist}
Summary: Automatic theorem prover for SMT problems
# License breakdown:
@ -12,19 +15,20 @@ Summary: Automatic theorem prover for SMT problems
# o src/util/channel.h
# o examples/hashsmt/sha1.hpp
# - Files containing code under the BSD license:
# o proofs/lfsc_checker/*
# o src/parser/antlr_input_imports.cpp
# o src/parser/bounded_token_buffer.cpp
# - All other files are distributed under the MIT license
License: MIT and BSD and Boost
# But we link with readline, so it all gets subsumed by GPLv3+ anyway.
License: GPLv3+
URL: http://cvc4.cs.nyu.edu/web/
Source0: http://cvc4.cs.nyu.edu/builds/src/%{name}-%{version}.tar.gz
# Updated *.plf files from upstream. These are needed only for the self-tests.
Source1: smt.plf
Source2: sat.plf
Source3: th_base.plf
# Fix some doxygen problems. Upstream plans to fix this differently.
Patch0: %{name}-doxygen.patch
# Adapt to the way the Fedora ABC package is constructed.
Patch1: %{name}-abc.patch
BuildRequires: abc-devel
BuildRequires: antlr3-C-devel
BuildRequires: antlr3-tool
BuildRequires: boost-devel
@ -32,21 +36,21 @@ BuildRequires: chrpath
BuildRequires: cxxtest
BuildRequires: doxygen-latex
BuildRequires: ghostscript
BuildRequires: glpk-devel
BuildRequires: gmp-devel
%if 0%{?have_perftools}
BuildRequires: gperftools-devel
%endif
BuildRequires: java-devel >= 1:1.6.0
BuildRequires: java-devel
BuildRequires: jpackage-utils
BuildRequires: lfsc
BuildRequires: perl
BuildRequires: python
BuildRequires: readline-devel
BuildRequires: swig
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
Requires: lfsc
Obsoletes: lfsc < 1.0-1%{?dist}
Provides: lfsc = %{version}-%{release}
%description
CVC4 is an efficient open-source automatic theorem prover for
@ -74,6 +78,7 @@ Header files and library links for developing applications that use %{name}.
%package doc
Summary: Interface documentation for %{name}
Provides: bundled(jquery)
%description doc
Interface documentation for %{name}.
@ -96,33 +101,51 @@ Java interface to %{name}.
%prep
%setup -q
# The rpm patch macro doesn't understand -T, and we need to it to avoid
# The rpm patch macro doesn't understand -T, and we need it to to avoid
# regenerating the very files we're trying to patch.
patch -p0 -T < %{PATCH0}
%patch1
# Don't change the build flags we want to use and avoid hardcoded rpaths
# Don't change the build flags we want to use, avoid hardcoded rpaths, adapt to
# antlr 3.5, and allow boost to use g++ 4.9.
sed -e '/^if test "$enable_debug_symbols"/,/fi/d' \
-e 's|^hardcode_libdir_flag_spec=.*|hardcode_libdir_flag_spec=""|g' \
-e 's|^runpath_var=LD_RUN_PATH|runpath_var=DIE_RPATH_DIE|g' \
-e 's,^hardcode_libdir_flag_spec=.*,hardcode_libdir_flag_spec="",g' \
-e 's,runpath_var=LD_RUN_PATH,runpath_var=DIE_RPATH_DIE,g' \
-e 's,\([^.]\)3\.4,\13.5,g' \
-e 's,\(__GNUC_MINOR__ == \)8\(.*\)gcc48,\19\2gcc49,' \
-i configure
# Change the Java installation paths for Fedora
sed -i "s|^\(javalibdir =.*\)jni|\1java/%{name}|" src/bindings/Makefile.in
# Make lfsc documentation available
cp -p proofs/lfsc_checker/AUTHORS AUTHORS.lfsc
cp -p proofs/lfsc_checker/COPYING COPYING.lfsc
cp -p proofs/lfsc_checker/NEWS NEWS.lfsc
cp -p proofs/lfsc_checker/README README.lfsc
# Preserve timestamps when installing
for fil in $(find . -name Makefile\*); do
sed -i 's/$(install_sh) -c/$(install_sh) -p/' $fil
done
%build
%configure --enable-proof --enable-language-bindings=all --with-portfolio \
export CPPFLAGS="-I%{_jvmdir}/java/include -I%{_jvmdir}/java/include/linux -I%{_includedir}/abc"
%if %{__isa_bits} == 64
CPPFLAGS+=" -DLIN64"
%else
CPPFLAGS+=" -DLIN"
%endif
%configure --enable-gpl --enable-proof --enable-language-bindings=all \
%if 0%{?have_perftools}
--with-google-perftools \
%endif
--with-glpk --without-compat \
CPPFLAGS="-I%{_jvmdir}/java/include -I%{_jvmdir}/java/include/linux -DFEDORA_GLPK_ITCNT -Dlpx_get_int_parm(x,y)=glp_get_it_cnt(x)" \
LFSCARGS="%{_datadir}/lfsc/sat.plf"
--with-portfolio --with-abc --with-abc-dir=%{_prefix} --with-readline \
--without-compat
# Workaround libtool reordering -Wl,--as-needed after all the libraries
sed -i 's/CC=.g../& -Wl,--as-needed/' builds/*-linux-gnu/default-proof/libtool
# Workaround insufficiently quoted CPPFLAGS
find builds -name Makefile | xargs sed -i 's/-Dlpx.*glp_get_it_cnt(x)/"&"/'
sed -i 's/CC=.g../& -Wl,--as-needed/' \
builds/*-linux-gnu*/production-abc-proof/libtool
make %{?_smp_mflags}
make doc
@ -150,14 +173,14 @@ chrpath -d %{buildroot}%{_bindir}/* \
%{buildroot}%{_jnidir}/%{name}/lib%{name}*.so.*.*.*
# Help the debuginfo generator
BUILDS=builds/*-*-linux-gnu
BUILDS=$(echo builds/*-*-linux-gnu*)
for dir in decision expr main parser printer prop smt theory theory/arith \
theory/arrays theory/booleans theory/bv theory/datatypes theory/idl \
theory/quantifiers theory/rewriterules theory/strings theory/uf; do
ln -s $PWD/src/$dir/options $BUILDS/default-proof/src/$dir
ln -s $PWD/src/$dir/options $BUILDS/production-abc-proof/src/$dir
done
ln -s default-proof/src $BUILDS
ln -s $PWD/src/options/base_options $BUILDS/default-proof/src/options
ln -s production-abc-proof/src $BUILDS
ln -s $PWD/src/options/base_options $BUILDS/production-abc-proof/src/options
ln -s $PWD/src/options/base_options_template.cpp $BUILDS/src/options
ln -s $PWD/src/options/options_holder_template.h $BUILDS/src/options
ln -s $PWD/src/options/options_template.cpp $BUILDS/src/options
@ -171,19 +194,14 @@ ln -s $PWD/src/smt/smt_options_template.cpp $BUILDS/src/smt
# The tests use a large amount of stack space
ulimit -s unlimited
# The tests require unreleased *.plf files from upstream
for mk in $(find builds/*-*-linux-gnu/default-proof/test -name Makefile)
do
sed -e 's,^\(LFSCARGS =\).*,\1 %{SOURCE1} %{SOURCE2} %{SOURCE3},' \
-e 's,^\(TESTS_ENVIRONMENT = LFSC=\)".*",\1"lfsc %{SOURCE1} %{SOURCE2} %{SOURCE3}",' \
-i $mk
done
export LD_LIBRARY_PATH=$PWD/builds%{_libdir}
make check
%files
%doc AUTHORS NEWS README RELEASE-NOTES THANKS
%doc AUTHORS AUTHORS.lfsc NEWS NEWS.lfsc README README.lfsc RELEASE-NOTES THANKS
%license COPYING.lfsc
%{_bindir}/*
%{_datadir}/%{name}/
%{_mandir}/man1/*
%{_mandir}/man5/*
@ -191,7 +209,7 @@ make check
%doc doc/doxygen/*
%files libs
%doc COPYING
%license COPYING
%{_libdir}/lib%{name}*.so.*
%files devel
@ -204,6 +222,12 @@ make check
%{_jnidir}/%{name}/
%changelog
* Thu Jan 1 2015 Jerry James <loganjerry@gmail.com> - 1.4-1
- New upstream release
- Drop updated test files, now included upstream
- Drop obsolete workarounds for glpk compatibility
- Drop lfsc BR/R, as it has been incorporated into cvc4
* Fri Aug 22 2014 Jerry James <loganjerry@gmail.com> - 1.3-7
- Remove arm platforms from have_perftools due to bz 1109309

127
sat.plf
View File

@ -1,127 +0,0 @@
(declare bool type)
(declare tt bool)
(declare ff bool)
(declare var type)
(declare lit type)
(declare pos (! x var lit))
(declare neg (! x var lit))
(declare clause type)
(declare cln clause)
(declare clc (! x lit (! c clause clause)))
; constructs for general clauses for R, Q, satlem
(declare concat (! c1 clause (! c2 clause clause)))
(declare clr (! l lit (! c clause clause)))
; code to check resolutions
(program append ((c1 clause) (c2 clause)) clause
(match c1 (cln c2) ((clc l c1') (clc l (append c1' c2)))))
; we use marks as follows:
; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable.
; -- mark 2 to record if we are supposed to remove a negative occurrence of the variable.
; -- mark 3 if we did indeed remove the variable positively
; -- mark 4 if we did indeed remove the variable negatively
(program simplify_clause ((c clause)) clause
(match c
(cln cln)
((clc l c1)
(match l
; Set mark 1 on v if it is not set, to indicate we should remove it.
; After processing the rest of the clause, set mark 3 if we were already
; supposed to remove v (so if mark 1 was set when we began). Clear mark3
; if we were not supposed to be removing v when we began this call.
((pos v)
(let m (ifmarked v tt (do (markvar v) ff))
(let c' (simplify_clause c1)
(match m
(tt (do (ifmarked3 v v (markvar3 v)) c'))
(ff (do (ifmarked3 v (markvar3 v) v) (markvar v) (clc l c')))))))
; the same as the code for tt, but using different marks.
((neg v)
(let m (ifmarked2 v tt (do (markvar2 v) ff))
(let c' (simplify_clause c1)
(match m
(tt (do (ifmarked4 v v (markvar4 v)) c'))
(ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c')))))))))
((concat c1 c2) (append (simplify_clause c1) (simplify_clause c2)))
((clr l c1)
(match l
; set mark 1 to indicate we should remove v, and fail if
; mark 3 is not set after processing the rest of the clause
; (we will set mark 3 if we remove a positive occurrence of v).
((pos v)
(let m (ifmarked v tt (do (markvar v) ff))
(let m3 (ifmarked3 v (do (markvar3 v) tt) ff)
(let c' (simplify_clause c1)
(ifmarked3 v (do (match m3 (tt v) (ff (markvar3 v)))
(match m (tt v) (ff (markvar v))) c')
(fail clause))))))
; same as the tt case, but with different marks.
((neg v)
(let m2 (ifmarked2 v tt (do (markvar2 v) ff))
(let m4 (ifmarked4 v (do (markvar4 v) tt) ff)
(let c' (simplify_clause c1)
(ifmarked4 v (do (match m4 (tt v) (ff (markvar4 v)))
(match m2 (tt v) (ff (markvar2 v))) c')
(fail clause))))))
))))
; resolution proofs
(declare holds (! c clause type))
(declare R (! c1 clause (! c2 clause
(! u1 (holds c1)
(! u2 (holds c2)
(! n var
(holds (concat (clr (pos n) c1)
(clr (neg n) c2)))))))))
(declare Q (! c1 clause (! c2 clause
(! u1 (holds c1)
(! u2 (holds c2)
(! n var
(holds (concat (clr (neg n) c1)
(clr (pos n) c2)))))))))
(declare satlem_simplify
(! c1 clause
(! c2 clause
(! c3 clause
(! u1 (holds c1)
(! r (^ (simplify_clause c1) c2)
(! u2 (! x (holds c2) (holds c3))
(holds c3))))))))
(declare satlem
(! c clause
(! c2 clause
(! u (holds c)
(! u2 (! v (holds c) (holds c2))
(holds c2))))))
; A little example to demonstrate simplify_clause.
; It can handle nested clr's of both polarities,
; and correctly cleans up marks when it leaves a
; clr or clc scope. Uncomment and run with
; --show-runs to see it in action.
;
; (check
; (% v1 var
; (% u1 (holds (concat (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln))))))
; (clc (pos v1) (clc (pos v1) cln))))
; (satlem _ _ _ u1 (\ x x))))))
;(check
; (% v1 var
; (% u1 (holds (clr (neg v1) (concat (clc (neg v1) cln)
; (clr (neg v1) (clc (neg v1) cln)))))
; (satlem _ _ _ u1 (\ x x))))))

313
smt.plf
View File

@ -1,313 +0,0 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; SMT syntax and semantics (not theory-specific)
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare formula type)
(declare th_holds (! f formula type))
; constants
(declare true formula)
(declare false formula)
; logical connectives
(declare not (! f formula formula))
(declare and (! f1 formula (! f2 formula formula)))
(declare or (! f1 formula (! f2 formula formula)))
(declare impl (! f1 formula (! f2 formula formula)))
(declare iff (! f1 formula (! f2 formula formula)))
(declare xor (! f1 formula (! f2 formula formula)))
(declare ifte (! b formula (! f1 formula (! f2 formula formula))))
; terms
(declare sort type) ; sort in the theory
(declare arrow (! s1 sort (! s2 sort sort))) ; function constructor
(declare term (! t sort type)) ; declared terms in formula
(declare apply (! s1 sort
(! s2 sort
(! t1 (term (arrow s1 s2))
(! t2 (term s1)
(term s2))))))
(declare ite (! s sort
(! f formula
(! t1 (term s)
(! t2 (term s)
(term s))))))
; let/flet
(declare let (! s sort
(! t (term s)
(! f (! v (term s) formula)
formula))))
(declare flet (! f1 formula
(! f2 (! v formula formula)
formula)))
; predicates
(declare = (! s sort
(! x (term s)
(! y (term s)
formula))))
; To avoid duplicating some of the rules (e.g., cong), we will view
; applications of predicates as terms of sort "Bool".
; Such terms can be injected as atomic formulas using "p_app".
(declare Bool sort) ; the special sort for predicates
(declare p_app (! x (term Bool) formula)) ; propositional application of term
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Examples
; an example of "(p1 or p2(0)) and t1=t2(1)"
;(! p1 (term Bool)
;(! p2 (term (arrow Int Bool))
;(! t1 (term Int)
;(! t2 (term (arrow Int Int))
;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0)))
; (= _ t1 (apply _ _ t2 1))))
; ...
; another example of "p3(a,b)"
;(! a (term Int)
;(! b (term Int)
;(! p3 (term (arrow Int (arrow Int Bool))) ; arrow is right assoc.
;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc.
; ...
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Natural deduction rules : used for CNF
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; contradiction
(declare contra
(! f formula
(! r1 (th_holds f)
(! r2 (th_holds (not f))
(th_holds false)))))
;; not not
(declare not_not_intro
(! f formula
(! u (th_holds f)
(th_holds (not (not f))))))
(declare not_not_elim
(! f formula
(! u (th_holds (not (not f)))
(th_holds f))))
;; or elimination
(declare or_elim_1
(! f1 formula
(! f2 formula
(! u1 (th_holds (not f1))
(! u2 (th_holds (or f1 f2))
(th_holds f2))))))
(declare or_elim_2
(! f1 formula
(! f2 formula
(! u1 (th_holds (not f2))
(! u2 (th_holds (or f1 f2))
(th_holds f1))))))
;; and elimination
(declare and_elim_1
(! f1 formula
(! f2 formula
(! u (th_holds (and f1 f2))
(th_holds f1)))))
(declare and_elim_2
(! f1 formula
(! f2 formula
(! u (th_holds (and f1 f2))
(th_holds f2)))))
;; not impl elimination
(declare not_impl_elim_1
(! f1 formula
(! f2 formula
(! u (th_holds (not (impl f1 f2)))
(th_holds f1)))))
(declare not_impl_elim_2
(! f1 formula
(! f2 formula
(! u (th_holds (not (impl f1 f2)))
(th_holds (not f2))))))
;; impl elimination
(declare impl_intro (! f1 formula
(! f2 formula
(! i1 (! u (th_holds f1)
(th_holds f2))
(th_holds (impl f1 f2))))))
(declare impl_elim
(! f1 formula
(! f2 formula
(! u1 (th_holds f1)
(! u2 (th_holds (impl f1 f2))
(th_holds f2))))))
;; iff elimination
(declare iff_elim_1
(! f1 formula
(! f2 formula
(! u1 (th_holds (iff f1 f2))
(th_holds (impl f1 f2))))))
(declare iff_elim_2
(! f1 formula
(! f2 formula
(! u1 (th_holds (iff f1 f2))
(th_holds (impl f2 f1))))))
(declare not_iff_elim_1
(! f1 formula
(! f2 formula
(! u1 (th_holds (not f1))
(! u2 (th_holds (not (iff f1 f2)))
(th_holds f2))))))
(declare not_iff_elim_2
(! f1 formula
(! f2 formula
(! u1 (th_holds f1)
(! u2 (th_holds (not (iff f1 f2)))
(th_holds (not f2)))))))
;; ite elimination
(declare ite_elim_1
(! a formula
(! b formula
(! c formula
(! u1 (th_holds a)
(! u2 (th_holds (ifte a b c))
(th_holds b)))))))
(declare ite_elim_2
(! a formula
(! b formula
(! c formula
(! u1 (th_holds (not a))
(! u2 (th_holds (ifte a b c))
(th_holds c)))))))
(declare ite_elim_3
(! a formula
(! b formula
(! c formula
(! u1 (th_holds (not b))
(! u2 (th_holds (ifte a b c))
(th_holds c)))))))
(declare ite_elim_2n
(! a formula
(! b formula
(! c formula
(! u1 (th_holds a)
(! u2 (th_holds (ifte (not a) b c))
(th_holds c)))))))
(declare not_ite_elim_1
(! a formula
(! b formula
(! c formula
(! u1 (th_holds a)
(! u2 (th_holds (not (ifte a b c)))
(th_holds (not b))))))))
(declare not_ite_elim_2
(! a formula
(! b formula
(! c formula
(! u1 (th_holds (not a))
(! u2 (th_holds (not (ifte a b c)))
(th_holds (not c))))))))
(declare not_ite_elim_3
(! a formula
(! b formula
(! c formula
(! u1 (th_holds b)
(! u2 (th_holds (not (ifte a b c)))
(th_holds (not c))))))))
(declare not_ite_elim_2n
(! a formula
(! b formula
(! c formula
(! u1 (th_holds a)
(! u2 (th_holds (not (ifte (not a) b c)))
(th_holds (not c))))))))
;; How to do CNF for disjunctions of theory literals.
;;
;; Given theory literals F1....Fn, and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))).
;;
;; We introduce atoms a1...an for literals F1...Fn, mapping them to boolean literals v1...vn.
;; Do this at the beginning of the proof:
;;
;; (decl_atom F1 (\ v1 (\ a1
;; (decl_atom F2 (\ v2 (\ a2
;; ....
;; (decl_atom Fn (\ vn (\ an
;;
;; Our input A is clausified by the following proof:
;;
;;(satlem _ _
;;(asf _ _ _ a1 (\ l1
;;(asf _ _ _ a2 (\ l2
;;...
;;(asf _ _ _ an (\ ln
;;(clausify_false
;;
;; (contra _
;; (or_elim_1 _ _ l{n-1}
;; ...
;; (or_elim_1 _ _ l2
;; (or_elim_1 _ _ l1 A))))) ln)
;;
;;))))))) (\ C
;;
;; We now have the free variable C, which should be the clause (v1 V ... V vn).
;;
;; We also need to consider the polarity of literals, say we have A of the form (th_holds (or (not F1) (or F2 (not F3)))).
;; Where necessary, we use "ast" instead of "asf", introduce negations by "not_not_intro" for pattern matching, and flip
;; the arguments of contra:
;;
;;(satlem _ _
;;(ast _ _ _ a1 (\ l1
;;(asf _ _ _ a2 (\ l2
;;(ast _ _ _ a3 (\ l3
;;(clausify_false
;;
;; (contra _ l3
;; (or_elim_1 _ _ l2
;; (or_elim_1 _ _ (not_not_intro l1) A))))
;;
;;))))))) (\ C
;;
;; C should be the clause (~v1 V v2 V ~v3 )

2
sources
View File

@ -1 +1 @@
a8c2bf10b7fa581a8de283072f4137b6 cvc4-1.3.tar.gz
581c559c02b94fcb18b2e5b11432e009 cvc4-1.4.tar.gz

107
th_base.plf
View File

@ -1,107 +0,0 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Atomization / Clausification
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; binding between an LF var and an (atomic) formula
(declare atom (! v var (! p formula type)))
(declare decl_atom
(! f formula
(! u (! v var
(! a (atom v f)
(holds cln)))
(holds cln))))
; direct clausify
(declare clausify_form
(! f formula
(! v var
(! a (atom v f)
(! u (th_holds f)
(holds (clc (pos v) cln)))))))
(declare clausify_form_not
(! f formula
(! v var
(! a (atom v f)
(! u (th_holds (not f))
(holds (clc (neg v) cln)))))))
(declare clausify_false
(! u (th_holds false)
(holds cln)))
(declare th_let_pf
(! f formula
(! u (th_holds f)
(! u2 (! v (th_holds f) (holds cln))
(holds cln)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Theory reasoning
; - make a series of assumptions and then derive a contradiction (or false)
; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"
; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare ast
(! v var
(! f formula
(! C clause
(! r (atom v f) ;this is specified
(! u (! o (th_holds f)
(holds C))
(holds (clc (neg v) C))))))))
(declare asf
(! v var
(! f formula
(! C clause
(! r (atom v f)
(! u (! o (th_holds (not f))
(holds C))
(holds (clc (pos v) C))))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Theory of Equality and Congruence Closure
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; temporary :
(declare trust (th_holds false))
(declare refl
(! s sort
(! t (term s)
(th_holds (= s t t)))))
(declare symm (! s sort
(! x (term s)
(! y (term s)
(! u (th_holds (= _ x y))
(th_holds (= _ y x)))))))
(declare trans (! s sort
(! x (term s)
(! y (term s)
(! z (term s)
(! u (th_holds (= _ x y))
(! u (th_holds (= _ y z))
(th_holds (= _ x z)))))))))
(declare cong (! s1 sort
(! s2 sort
(! a1 (term (arrow s1 s2))
(! b1 (term (arrow s1 s2))
(! a2 (term s1)
(! b2 (term s1)
(! u1 (th_holds (= _ a1 b1))
(! u2 (th_holds (= _ a2 b2))
(th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2))))))))))))