From f624faa1705dc40eca4a531ea607bed904c85f35 Mon Sep 17 00:00:00 2001 From: Jerry James Date: Fri, 2 Jan 2015 16:57:48 -0700 Subject: [PATCH] New upstream release. 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 --- .gitignore | 2 +- cvc4-abc.patch | 30 +++++ cvc4-doxygen.patch | 124 ++++++++++-------- cvc4.spec | 98 ++++++++------ sat.plf | 127 ------------------ smt.plf | 313 --------------------------------------------- sources | 2 +- th_base.plf | 107 ---------------- 8 files changed, 166 insertions(+), 637 deletions(-) create mode 100644 cvc4-abc.patch delete mode 100644 sat.plf delete mode 100644 smt.plf delete mode 100644 th_base.plf diff --git a/.gitignore b/.gitignore index c0346c5..c4944a6 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1 @@ -/cvc4-1.3.tar.gz +/cvc4-1.4.tar.gz diff --git a/cvc4-abc.patch b/cvc4-abc.patch new file mode 100644 index 0000000..e2f0dfa --- /dev/null +++ b/cvc4-abc.patch @@ -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 : diff --git a/cvc4-doxygen.patch b/cvc4-doxygen.patch index a572bc9..3c05327 100644 --- a/cvc4-doxygen.patch +++ b/cvc4-doxygen.patch @@ -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 diff --git a/cvc4.spec b/cvc4.spec index 3cba481..0961c46 100644 --- a/cvc4.spec +++ b/cvc4.spec @@ -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 - 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 - 1.3-7 - Remove arm platforms from have_perftools due to bz 1109309 diff --git a/sat.plf b/sat.plf deleted file mode 100644 index 09255f6..0000000 --- a/sat.plf +++ /dev/null @@ -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)))))) \ No newline at end of file diff --git a/smt.plf b/smt.plf deleted file mode 100644 index 75bfc44..0000000 --- a/smt.plf +++ /dev/null @@ -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 ) \ No newline at end of file diff --git a/sources b/sources index 7bf6add..e52e87d 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -a8c2bf10b7fa581a8de283072f4137b6 cvc4-1.3.tar.gz +581c559c02b94fcb18b2e5b11432e009 cvc4-1.4.tar.gz diff --git a/th_base.plf b/th_base.plf deleted file mode 100644 index e66990d..0000000 --- a/th_base.plf +++ /dev/null @@ -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)))))))))))) -