[cvc4] 02/03: Add debian/*
Fabian Wolff
fw-guest at moszumanska.debian.org
Mon Mar 27 16:28:41 UTC 2017
This is an automated email from the git hooks/post-receive script.
fw-guest pushed a commit to branch master
in repository cvc4.
commit e38afe6cb10bdb79f0bae398b9605e4deae7578f
Author: Fabian Wolff <fabi.wolff at arcor.de>
Date: Fri Mar 17 16:39:15 2017 +0100
Add debian/*
---
debian/changelog | 5 +
debian/compat | 1 +
debian/control | 96 +++++++++++++++
debian/copyright | 208 ++++++++++++++++++++++++++++++++
debian/cvc4.install | 4 +
debian/libcvc4-3.install | 1 +
debian/libcvc4-dev.install | 3 +
debian/libcvc4parser3.install | 1 +
debian/patches/01-ref-compare.patch | 17 +++
debian/patches/02-timestamps.patch | 17 +++
debian/patches/03-include-paths.patch | 16 +++
debian/patches/04-spelling-errors.patch | 208 ++++++++++++++++++++++++++++++++
debian/patches/series | 4 +
debian/rules | 22 ++++
debian/source/format | 1 +
15 files changed, 604 insertions(+)
diff --git a/debian/changelog b/debian/changelog
new file mode 100644
index 0000000..24bbb27
--- /dev/null
+++ b/debian/changelog
@@ -0,0 +1,5 @@
+cvc4 (1.5~pre-20170316) UNRELEASED; urgency=medium
+
+ * Initial release. (Closes: #757048)
+
+ -- Fabian Wolff <fabi.wolff at arcor.de> Thu, 16 Mar 2017 17:18:54 +0100
diff --git a/debian/compat b/debian/compat
new file mode 100644
index 0000000..ec63514
--- /dev/null
+++ b/debian/compat
@@ -0,0 +1 @@
+9
diff --git a/debian/control b/debian/control
new file mode 100644
index 0000000..eb45117
--- /dev/null
+++ b/debian/control
@@ -0,0 +1,96 @@
+Source: cvc4
+Maintainer: Fabian Wolff <fabi.wolff at arcor.de>
+Section: math
+Priority: optional
+Build-Depends: debhelper (>= 9),
+ dh-autoreconf,
+ libgmp-dev,
+ libantlr3c-dev,
+ libboost-thread-dev,
+ libreadline-dev,
+ pkg-config,
+ cxxtest,
+ chrpath
+Standards-Version: 3.9.8
+Homepage: http://cvc4.cs.stanford.edu/web/
+
+Package: cvc4
+Architecture: any
+Depends: libcvc4-3 (= ${binary:Version}),
+ libcvc4parser3 (= ${binary:Version}),
+ ${shlibs:Depends},
+ ${misc:Depends}
+Description: automated theorem prover for SMT problems
+ CVC4 is an efficient automatic theorem prover for satisfiability
+ modulo theories (SMT) problems. It can be used to prove the validity
+ (or, dually, the satisfiability) of first-order formulas in a large
+ number of built-in logical theories and their combination.
+ .
+ CVC4 is intended to be an open and extensible SMT engine, and it can
+ be used as a stand-alone tool or as a library. It is the fourth in
+ the Cooperating Validity Checker family of tools (also including CVC,
+ CVC Lite and CVC3). CVC4 has been designed to increase the
+ performance and reduce the memory overhead of its predecessors.
+ .
+ This package contains binaries needed to use CVC4 as a stand-alone
+ tool.
+
+Package: libcvc4-dev
+Architecture: any
+Section: libdevel
+Depends: libcvc4-3 (= ${binary:Version}),
+ libcvc4parser3 (= ${binary:Version}),
+ ${shlibs:Depends},
+ ${misc:Depends}
+Description: automated theorem prover for SMT problems (development files)
+ CVC4 is an efficient automatic theorem prover for satisfiability
+ modulo theories (SMT) problems. It can be used to prove the validity
+ (or, dually, the satisfiability) of first-order formulas in a large
+ number of built-in logical theories and their combination.
+ .
+ CVC4 is intended to be an open and extensible SMT engine, and it can
+ be used as a stand-alone tool or as a library. It is the fourth in
+ the Cooperating Validity Checker family of tools (also including CVC,
+ CVC Lite and CVC3). CVC4 has been designed to increase the
+ performance and reduce the memory overhead of its predecessors.
+ .
+ This package contains development files for CVC4. Install it if you
+ want to develop applications that use CVC4's API.
+
+Package: libcvc4-3
+Architecture: any
+Section: libs
+Depends: ${shlibs:Depends},
+ ${misc:Depends}
+Description: automated theorem prover for SMT problems (runtime)
+ CVC4 is an efficient automatic theorem prover for satisfiability
+ modulo theories (SMT) problems. It can be used to prove the validity
+ (or, dually, the satisfiability) of first-order formulas in a large
+ number of built-in logical theories and their combination.
+ .
+ CVC4 is intended to be an open and extensible SMT engine, and it can
+ be used as a stand-alone tool or as a library. It is the fourth in
+ the Cooperating Validity Checker family of tools (also including CVC,
+ CVC Lite and CVC3). CVC4 has been designed to increase the
+ performance and reduce the memory overhead of its predecessors.
+ .
+ This package contains CVC4's runtime shared libraries.
+
+Package: libcvc4parser3
+Architecture: any
+Section: libs
+Depends: ${shlibs:Depends},
+ ${misc:Depends}
+Description: automated theorem prover for SMT problems (parser runtime)
+ CVC4 is an efficient automatic theorem prover for satisfiability
+ modulo theories (SMT) problems. It can be used to prove the validity
+ (or, dually, the satisfiability) of first-order formulas in a large
+ number of built-in logical theories and their combination.
+ .
+ CVC4 is intended to be an open and extensible SMT engine, and it can
+ be used as a stand-alone tool or as a library. It is the fourth in
+ the Cooperating Validity Checker family of tools (also including CVC,
+ CVC Lite and CVC3). CVC4 has been designed to increase the
+ performance and reduce the memory overhead of its predecessors.
+ .
+ This package contains runtime shared libraries for CVC4's parser.
diff --git a/debian/copyright b/debian/copyright
new file mode 100644
index 0000000..1c321c2
--- /dev/null
+++ b/debian/copyright
@@ -0,0 +1,208 @@
+Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
+Upstream-Name: CVC4
+Source: http://cvc4.cs.stanford.edu/downloads/builds/src/
+
+Files: *
+Copyright: 2009-2017 New York University and The University of Iowa
+License: GPL-3+
+Comment: CVC4 is available under both the BSD-3-clause and the
+ GPL-3+ licenses. For optimal performance, linking against
+ GPL libraries is recommended, which is why this package is
+ built and linked against those libraries, resulting in CVC4
+ being covered by the GPL-3+ license.
+
+Files: debian/*
+Copyright: 2017 Fabian Wolff <fabi.wolff at arcor.de>
+License: GPL-3+
+
+License: GPL-3+
+ This program is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or (at
+ your option) any later version.
+ .
+ This program is distributed in the hope that it will be useful, but
+ WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ General Public License for more details.
+ .
+ You should have received a copy of the GNU General Public License
+ along with this program. If not, see <http://www.gnu.org/licenses/>.
+ .
+ On Debian systems, the complete text of the GNU General Public License
+ version 3 can be found in the file `/usr/share/common-licenses/GPL-3'.
+
+Files: config/boost.m4
+Copyright: 2007-2011 Benoit Sigoure <tsuna at lrde.epita.fr>
+License: GPL-3+ with Autoconf exception #1
+ This program is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or (at
+ your option) any later version.
+ .
+ Additional permission under section 7 of the GNU General Public
+ License, version 3 ("GPLv3"):
+ .
+ If you convey this file as part of a work that contains a
+ configuration script generated by Autoconf, you may do so under terms
+ of your choice.
+ .
+ This program is distributed in the hope that it will be useful, but
+ WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ General Public License for more details.
+ .
+ You should have received a copy of the GNU General Public License
+ along with this program. If not, see <http://www.gnu.org/licenses/>.
+ .
+ On Debian systems, the complete text of the GNU General Public License
+ version 3 can be found in the file `/usr/share/common-licenses/GPL-3'.
+
+Files: config/doxygen.am
+Copyright: 2004 Oren Ben-Kiki
+License: GPL-3+ with Autoconf exception #2
+
+Files: config/ax_tls.m4
+Copyright: 2008 Alan Woodland <ajw05 at aber.ac.uk>
+ 2010 Diego Elio Pettenò <flameeyes at gmail.com>
+License: GPL-3+ with Autoconf exception #2
+
+License: GPL-3+ with Autoconf exception #2
+ This program is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or (at
+ your option) any later version.
+ .
+ This program is distributed in the hope that it will be useful, but
+ WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ General Public License for more details.
+ .
+ You should have received a copy of the GNU General Public License
+ along with this program. If not, see <http://www.gnu.org/licenses/>.
+ .
+ As a special exception, the respective Autoconf Macro's copyright
+ owner gives unlimited permission to copy, distribute and modify the
+ configure scripts that are the output of Autoconf when processing the
+ Macro. You need not follow the terms of the GNU General Public
+ License when using or distributing such scripts, even though portions
+ of the text of the Macro appear in them. The GNU General Public
+ License (GPL) does govern all other use of the material that
+ constitutes the Autoconf Macro.
+ .
+ This special exception to the GPL applies to versions of the Autoconf
+ Macro released by the Autoconf Archive. When you make and distribute
+ a modified version of the Autoconf Macro, you may extend this special
+ exception to the GPL you apply to your modified version as well.
+ .
+ On Debian systems, the complete text of the GNU General Public License
+ version 3 can be found in the file `/usr/share/common-licenses/GPL-3'.
+
+Files: config/pkg.m4
+Copyright: 2004 Scott James Remnant <scott at netsplit.com>
+License: GPL-3+ with Autoconf exception #3
+ This program is free software: you can redistribute it and/or modify
+ it under the terms of the GNU General Public License as published by
+ the Free Software Foundation, either version 3 of the License, or (at
+ your option) any later version.
+ .
+ This program is distributed in the hope that it will be useful, but
+ WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+ General Public License for more details.
+ .
+ You should have received a copy of the GNU General Public License
+ along with this program. If not, see <http://www.gnu.org/licenses/>.
+ .
+ As a special exception to the GNU General Public License, if you
+ distribute this file as part of a program that contains a
+ configuration script generated by Autoconf, you may include it under
+ the same distribution terms that you use for the rest of that
+ program.
+ .
+ On Debian systems, the complete text of the GNU General Public License
+ version 3 can be found in the file `/usr/share/common-licenses/GPL-3'.
+
+Files: src/parser/bounded_token_buffer.*
+ src/parser/antlr_input_imports.cpp
+Copyright: 2005-2009 Jim Idle, Temporal Wave LLC
+License: BSD-3-clause
+
+Files: proofs/lfsc_checker/*
+Copyright: 2012-2013 The University of Iowa
+License: BSD-3-clause
+
+License: BSD-3-clause
+ All rights reserved.
+ .
+ Redistribution and use in source and binary forms, with or without
+ modification, are permitted provided that the following conditions
+ are met:
+ 1. Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+ 2. Redistributions in binary form must reproduce the above copyright
+ notice, this list of conditions and the following disclaimer in the
+ documentation and/or other materials provided with the distribution.
+ 3. The name of the author may not be used to endorse or promote products
+ derived from this software without specific prior written permission.
+ .
+ THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR
+ IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
+ OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
+ IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT,
+ INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
+ NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
+ THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+Files: src/util/channel.h
+Copyright: 2009-2014 New York University and The University of Iowa
+ 2003-2008 Jan Gaspar
+License: BSL-1.0
+ Permission is hereby granted, free of charge, to any person or organization
+ obtaining a copy of the software and accompanying documentation covered by
+ this license (the "Software") to use, reproduce, display, distribute,
+ execute, and transmit the Software, and to prepare derivative works of the
+ Software, and to permit third-parties to whom the Software is furnished to
+ do so, all subject to the following:
+ .
+ The copyright notices in the Software and this entire statement, including
+ the above license grant, this restriction and the following disclaimer,
+ must be included in all copies of the Software, in whole or in part, and
+ all derivative works of the Software, unless such copies or derivative
+ works are solely in the form of machine-executable object code generated by
+ a source language processor.
+ .
+ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ FITNESS FOR A PARTICULAR PURPOSE, TITLE AND NON-INFRINGEMENT. IN NO EVENT
+ SHALL THE COPYRIGHT HOLDERS OR ANYONE DISTRIBUTING THE SOFTWARE BE LIABLE
+ FOR ANY DAMAGES OR OTHER LIABILITY, WHETHER IN CONTRACT, TORT OR OTHERWISE,
+ ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
+ DEALINGS IN THE SOFTWARE.
+
+Files: src/prop/minisat/*
+ src/prop/bvminisat/*
+Copyright: 2003-2010 Niklas Sorensson
+ 2003-2006 Niklas Een
+License: Expat
+ Permission is hereby granted, free of charge, to any person obtaining a
+ copy of this software and associated documentation files (the
+ "Software"), to deal in the Software without restriction, including
+ without limitation the rights to use, copy, modify, merge, publish,
+ distribute, sublicense, and/or sell copies of the Software, and to
+ permit persons to whom the Software is furnished to do so, subject to
+ the following conditions:
+ .
+ The above copyright notice and this permission notice shall be included
+ in all copies or substantial portions of the Software.
+ .
+ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
+ OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+ MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+ NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+ LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+ OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+ WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/debian/cvc4.install b/debian/cvc4.install
new file mode 100644
index 0000000..4c8cef1
--- /dev/null
+++ b/debian/cvc4.install
@@ -0,0 +1,4 @@
+usr/bin/cvc4
+usr/bin/pcvc4
+usr/share/man/man1/cvc4.1
+usr/share/man/man1/pcvc4.1
diff --git a/debian/libcvc4-3.install b/debian/libcvc4-3.install
new file mode 100644
index 0000000..4eec866
--- /dev/null
+++ b/debian/libcvc4-3.install
@@ -0,0 +1 @@
+usr/lib/*/libcvc4.so.*
diff --git a/debian/libcvc4-dev.install b/debian/libcvc4-dev.install
new file mode 100644
index 0000000..7089394
--- /dev/null
+++ b/debian/libcvc4-dev.install
@@ -0,0 +1,3 @@
+usr/include/cvc4
+usr/lib/*/*.a
+usr/lib/*/*.so
diff --git a/debian/libcvc4parser3.install b/debian/libcvc4parser3.install
new file mode 100644
index 0000000..06f111a
--- /dev/null
+++ b/debian/libcvc4parser3.install
@@ -0,0 +1 @@
+usr/lib/*/libcvc4parser.so.*
diff --git a/debian/patches/01-ref-compare.patch b/debian/patches/01-ref-compare.patch
new file mode 100644
index 0000000..00cb3f5
--- /dev/null
+++ b/debian/patches/01-ref-compare.patch
@@ -0,0 +1,17 @@
+Description: Fix a compilation error
+Author: Fabian Wolff <fabi.wolff at arcor.de>
+Forwarded: no
+Last-Update: 2017-03-17
+---
+This patch header follows DEP-3: http://dep.debian.net/deps/dep3/
+--- a/src/main/interactive_shell.cpp
++++ b/src/main/interactive_shell.cpp
+@@ -104,7 +104,7 @@
+ }
+
+ #if HAVE_LIBREADLINE
+- if(d_in == cin) {
++ if(&d_in == &cin) {
+ ::rl_readline_name = const_cast<char*>("CVC4");
+ #if READLINE_COMPENTRY_FUNC_RETURNS_CHARP
+ ::rl_completion_entry_function = commandGenerator;
diff --git a/debian/patches/02-timestamps.patch b/debian/patches/02-timestamps.patch
new file mode 100644
index 0000000..926b0d9
--- /dev/null
+++ b/debian/patches/02-timestamps.patch
@@ -0,0 +1,17 @@
+Description: Make timestamps reproducible
+Author: Fabian Wolff <fabi.wolff at arcor.de>
+Forwarded: no
+Last-Update: 2017-03-17
+---
+This patch header follows DEP-3: http://dep.debian.net/deps/dep3/
+--- a/src/base/configuration.cpp
++++ b/src/base/configuration.cpp
+@@ -291,7 +291,7 @@
+ }
+
+ std::string Configuration::getCompiledDateTime() {
+- return __DATE__ " " __TIME__;
++ return DEB_BUILD_DATE " " DEB_BUILD_TIME;
+ }
+
+ }/* CVC4 namespace */
diff --git a/debian/patches/03-include-paths.patch b/debian/patches/03-include-paths.patch
new file mode 100644
index 0000000..d08a21e
--- /dev/null
+++ b/debian/patches/03-include-paths.patch
@@ -0,0 +1,16 @@
+Description: Remove erroneous include path
+Author: Fabian Wolff <fabi.wolff at arcor.de>
+Forwarded: no
+Last-Update: 2017-03-17
+---
+This patch header follows DEP-3: http://dep.debian.net/deps/dep3/
+--- a/test/unit/Makefile.am
++++ b/test/unit/Makefile.am
+@@ -69,7 +69,6 @@
+
+ AM_CPPFLAGS = \
+ -I. \
+- "-I at CXXTEST@" \
+ "-I at top_builddir@/src" \
+ "-I at top_srcdir@/src/include" \
+ "-I at top_srcdir@/lib" \
diff --git a/debian/patches/04-spelling-errors.patch b/debian/patches/04-spelling-errors.patch
new file mode 100644
index 0000000..a38b8b6
--- /dev/null
+++ b/debian/patches/04-spelling-errors.patch
@@ -0,0 +1,208 @@
+Description: Fix spelling errors found by Lintian
+Author: Fabian Wolff <fabi.wolff at arcor.de>
+Forwarded: no
+Last-Update: 2017-03-17
+---
+This patch header follows DEP-3: http://dep.debian.net/deps/dep3/
+--- a/doc/cvc4.1
++++ b/doc/cvc4.1
+@@ -176,7 +176,7 @@
+ .IP "\-\-replay\-reject\-cut"
+ maximum complexity of any coefficient while replaying cuts
+ .IP "\-\-replay\-lemma\-reject\-cut"
+-maximum complexity of any coefficient while outputing replaying cut lemmas
++maximum complexity of any coefficient while outputting replaying cut lemmas
+ .IP "\-\-replay\-soi\-major\-threshold"
+ threshold for a major tolerance failure by the approximate solver
+ .IP "\-\-replay\-soi\-major\-threshold\-pen"
+@@ -784,38 +784,38 @@
+ .IP "\-\-model\-u\-dt\-enum"
+ in models, output uninterpreted sorts as datatype enumerations [*]
+ .IP "\-\-rewrite\-step"
+-ammount of resources spent for each rewrite step (EXPERTS only)
++amount of resources spent for each rewrite step (EXPERTS only)
+ .IP "\-\-theory\-check\-step"
+-ammount of resources spent for each theory check call (EXPERTS only)
++amount of resources spent for each theory check call (EXPERTS only)
+ .IP "\-\-decision\-step"
+-ammount of getNext decision calls in the decision engine (EXPERTS only)
++amount of getNext decision calls in the decision engine (EXPERTS only)
+
+ .IP "\-\-bitblast\-step"
+-ammount of resources spent for each bitblast step (EXPERTS only)
++amount of resources spent for each bitblast step (EXPERTS only)
+
+ .IP "\-\-parse\-step"
+-ammount of resources spent for each command/expression parsing (EXPERTS only)
++amount of resources spent for each command/expression parsing (EXPERTS only)
+
+ .IP "\-\-lemma\-step"
+-ammount of resources spent when adding lemmas (EXPERTS only)
++amount of resources spent when adding lemmas (EXPERTS only)
+
+ .IP "\-\-restart\-step"
+-ammount of resources spent for each theory restart (EXPERTS only)
++amount of resources spent for each theory restart (EXPERTS only)
+
+ .IP "\-\-cnf\-step"
+-ammount of resources spent for each call to cnf conversion (EXPERTS only)
++amount of resources spent for each call to cnf conversion (EXPERTS only)
+
+ .IP "\-\-preprocess\-step"
+-ammount of resources spent for each preprocessing step in SmtEngine (EXPERTS only)
++amount of resources spent for each preprocessing step in SmtEngine (EXPERTS only)
+
+ .IP "\-\-quantifier\-step"
+-ammount of resources spent for quantifier instantiations (EXPERTS only)
++amount of resources spent for quantifier instantiations (EXPERTS only)
+
+ .IP "\-\-sat\-conflict\-step"
+-ammount of resources spent for each sat conflict (main sat solver) (EXPERTS only)
++amount of resources spent for each sat conflict (main sat solver) (EXPERTS only)
+
+ .IP "\-\-bv\-sat\-conflict\-step"
+-ammount of resources spent for each sat conflict (bitvectors) (EXPERTS only)
++amount of resources spent for each sat conflict (bitvectors) (EXPERTS only)
+
+
+ .IP "\-\-rewrite\-apply\-to\-const"
+--- a/proofs/signatures/signatures.cpp
++++ b/proofs/signatures/signatures.cpp
+@@ -1359,7 +1359,7 @@
+ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\n\
+ \n\
+ ; bit blast x = y\n\
+-; for x,y of size n, it will return a conjuction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1})))\n\
++; for x,y of size n, it will return a conjunction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1})))\n\
+ ; f is the accumulator formula that builds the equality in the right order\n\
+ (program bblast_eq_rec ((x bblt) (y bblt) (f formula)) formula\n\
+ (match x\n\
+--- a/proofs/signatures/th_bv_bitblast.plf
++++ b/proofs/signatures/th_bv_bitblast.plf
+@@ -425,7 +425,7 @@
+ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+ ; bit blast x = y
+-; for x,y of size n, it will return a conjuction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1})))
++; for x,y of size n, it will return a conjunction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1})))
+ ; f is the accumulator formula that builds the equality in the right order
+ (program bblast_eq_rec ((x bblt) (y bblt) (f formula)) formula
+ (match x
+--- a/src/options/arith_options
++++ b/src/options/arith_options
+@@ -135,7 +135,7 @@
+ maximum complexity of any coefficient while replaying cuts
+
+ option lemmaRejectCutSize --replay-lemma-reject-cut unsigned :default 25500
+- maximum complexity of any coefficient while outputing replaying cut lemmas
++ maximum complexity of any coefficient while outputting replaying cut lemmas
+
+ option soiApproxMajorFailure --replay-soi-major-threshold double :default .01
+ threshold for a major tolerance failure by the approximate solver
+--- a/src/options/options_handler.cpp
++++ b/src/options/options_handler.cpp
+@@ -958,7 +958,7 @@
+ Bit-blasting modes currently supported by the --bitblast option:\n\
+ \n\
+ lazy (default)\n\
+-+ Separate boolean structure and term reasoning betwen the core\n\
+++ Separate boolean structure and term reasoning between the core\n\
+ SAT solver and the bv SAT solver\n\
+ \n\
+ eager\n\
+--- a/src/options/smt_options
++++ b/src/options/smt_options
+@@ -108,40 +108,40 @@
+
+ # Resource spending options for SPARK
+ expert-option rewriteStep rewrite-step --rewrite-step unsigned :default 1
+- ammount of resources spent for each rewrite step
++ amount of resources spent for each rewrite step
+
+ expert-option theoryCheckStep theory-check-step --theory-check-step unsigned :default 1
+- ammount of resources spent for each theory check call
++ amount of resources spent for each theory check call
+
+ expert-option decisionStep decision-step --decision-step unsigned :default 1
+- ammount of getNext decision calls in the decision engine
++ amount of getNext decision calls in the decision engine
+
+ expert-option bitblastStep bitblast-step --bitblast-step unsigned :default 1
+- ammount of resources spent for each bitblast step
++ amount of resources spent for each bitblast step
+
+ expert-option parseStep parse-step --parse-step unsigned :default 1
+- ammount of resources spent for each command/expression parsing
++ amount of resources spent for each command/expression parsing
+
+ expert-option lemmaStep lemma-step --lemma-step unsigned :default 1
+- ammount of resources spent when adding lemmas
++ amount of resources spent when adding lemmas
+
+ expert-option restartStep restart-step --restart-step unsigned :default 1
+- ammount of resources spent for each theory restart
++ amount of resources spent for each theory restart
+
+ expert-option cnfStep cnf-step --cnf-step unsigned :default 1
+- ammount of resources spent for each call to cnf conversion
++ amount of resources spent for each call to cnf conversion
+
+ expert-option preprocessStep preprocess-step --preprocess-step unsigned :default 1
+- ammount of resources spent for each preprocessing step in SmtEngine
++ amount of resources spent for each preprocessing step in SmtEngine
+
+ expert-option quantifierStep quantifier-step --quantifier-step unsigned :default 1
+- ammount of resources spent for quantifier instantiations
++ amount of resources spent for quantifier instantiations
+
+ expert-option satConflictStep sat-conflict-step --sat-conflict-step unsigned :default 1
+- ammount of resources spent for each sat conflict (main sat solver)
++ amount of resources spent for each sat conflict (main sat solver)
+
+ expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step unsigned :default 1
+- ammount of resources spent for each sat conflict (bitvectors)
++ amount of resources spent for each sat conflict (bitvectors)
+
+
+ expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false
+--- a/src/theory/arith/arith_rewriter.cpp
++++ b/src/theory/arith/arith_rewriter.cpp
+@@ -210,7 +210,7 @@
+ // Todo improve the exception thrown
+ std::stringstream ss;
+ ss << "The POW(^) operator can only be used with a natural number ";
+- ss << "in the exponent. Exception occured in:" << std::endl;
++ ss << "in the exponent. Exception occurred in:" << std::endl;
+ ss << " " << t;
+ throw LogicException(ss.str());
+ }
+--- a/src/theory/builtin/kinds
++++ b/src/theory/builtin/kinds
+@@ -302,7 +302,7 @@
+
+ operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body"
+
+-parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjuction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator"
++parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjunction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator"
+ constant CHAIN_OP \
+ ::CVC4::Chain \
+ ::CVC4::ChainHashFunction \
+--- a/src/theory/strings/theory_strings_type_rules.h
++++ b/src/theory/strings/theory_strings_type_rules.h
+@@ -98,7 +98,7 @@
+ if( check ) {
+ TypeNode t = n[0].getType(check);
+ if (!t.isString()) {
+- throw TypeCheckingExceptionPrivate(n, "expecting an orginal string term in string contain");
++ throw TypeCheckingExceptionPrivate(n, "expecting an original string term in string contain");
+ }
+ t = n[1].getType(check);
+ if (!t.isString()) {
+--- a/test/regress/regress0/arith/bug716.1.cvc
++++ b/test/regress/regress0/arith/bug716.1.cvc
+@@ -1,4 +1,4 @@
+-% EXPECT: The POW(^) operator can only be used with a natural number in the exponent. Exception occured in:
++% EXPECT: The POW(^) operator can only be used with a natural number in the exponent. Exception occurred in:
+ % EXPECT: 2 ^ x
+ % EXIT: 1
+ x: INT;
diff --git a/debian/patches/series b/debian/patches/series
new file mode 100644
index 0000000..39f5b6c
--- /dev/null
+++ b/debian/patches/series
@@ -0,0 +1,4 @@
+01-ref-compare.patch
+02-timestamps.patch
+03-include-paths.patch
+04-spelling-errors.patch
diff --git a/debian/rules b/debian/rules
new file mode 100755
index 0000000..d965a0b
--- /dev/null
+++ b/debian/rules
@@ -0,0 +1,22 @@
+#!/usr/bin/make -f
+
+# Uncomment this to turn on verbose mode.
+# export DH_VERBOSE=1
+
+export DEB_BUILD_MAINT_OPTIONS = hardening=+all
+
+export DEB_CPPFLAGS_MAINT_APPEND = \
+ -DDEB_BUILD_DATE="\"$(shell dpkg-parsechangelog -SDate | date -f- +%F)\"" \
+ -DDEB_BUILD_TIME="\"$(shell dpkg-parsechangelog -SDate | date -f- +%T)\""
+
+%:
+ dh $@ --parallel --with autoreconf
+
+override_dh_auto_configure:
+ dh_auto_configure -- --enable-static --enable-shared \
+ --with-build=production --enable-gpl --with-portfolio \
+ --enable-unit-testing --with-readline --without-compat
+
+override_dh_install:
+ chrpath -d debian/tmp/usr/bin/pcvc4
+ dh_install
diff --git a/debian/source/format b/debian/source/format
new file mode 100644
index 0000000..163aaf8
--- /dev/null
+++ b/debian/source/format
@@ -0,0 +1 @@
+3.0 (quilt)
--
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/debian-science/packages/cvc4.git
More information about the debian-science-commits
mailing list