| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Removes some hacks due to Swig 2's incomplete C++11 support and adds
checks for version 3 at configuration time as well as in swig.h
|
|
C++11 supports explicitly deleting functions that should not be used
(explictly or implictly), e.g. copy or assignment constructors. We were
previously using the CVC4_UNDEFINED macro that used a compiler-specific
attribute. The C++11 feature should be more portable.
|
|
|
|
If the boost program_options library is missing, CryptoMiniSat5 only
builds a cryptominisat5_simple binary and omits the cryptominisat5,
which has more command-line options. We do not use the binary anyway, so
this commit changes the cryptominisat.m4 script to look for the
cryptominisat5_simple binary, which is always generated.
|
|
|
|
The autogen.sh script that we use causes the tap-driver.sh script to be
copied from automake installed on the system, so we do not have to
include it in our git repository. This also avoids ping-ponging between
different versions of the tap-driver script if different people have
different versions and commit them as part of their PRs.
|
|
Until now, we have been using a bash script for the running the
regressions. That script had several issues, e.g. it was creating many
temprorary files and it was calling itself recursively, making it
difficult to maintain. This commit replaces the script with a Python
script. The Python script uses the TAP protocol, which allows us to
display the results of multiple tests per file (e.g. with --check-models
and without) separately and with more details. It also outputs whenever it starts running
a test, which allows finding "stuck" regression tests on Travis. As recommended in the
automake documentation [0], the commit copies the TAP driver to enable
TAP support for the test driver.
Note: the commit also changes some of the regressions slightly because
we were using "%" for the test directives in SMT files which does not
correspond to the comment character ";". Using the comment character
simplifies the handling and makes it easier for users to reproduce a
failure (they can simply run CVC4 on the regression file).
[0]
https://www.gnu.org/software/automake/manual/html_node/Use-TAP-with-the-Automake-test-harness.html
|
|
Our current build scripts did not work with Automake 1.16. At configure
time, the .swig_deps target in src/bindings/Makefile.am was executed due
to the `@mk_include@ .swig_deps` (which is not the case with older
versions of Automake). This ultimately caused configure to fail because
SWIG was complaining about missing files (generated source files, such
as src/expr/expr.h). This commit fixes the issue by adding
`-ignoremissing` to the call to SWIG. With that option, SWIG is not
complaining about the missing files and the dependency generation
completes successfully.
Currently, the src/bindings/compat/java/create_impl.py script is not
compatible with Python 3, which leads to errors when building on systems
where `python` links to Python 3 (e.g. on Arch Linux). This commit makes
the script compatible with both Python 2 and 3.
Our build scripts were using old -source/-target versions when calling
`javac`. Those are not supported by newer Java versions (e.g. Java 9).
This commit updates the version to 1.6, which is still fairly old, so
should be broadly supported.
Finally, some systems (e.g. Arch Linux' AUR package for SWIG 2) refer to
SWIG 2 as `swig-2`. This commit adds support for detecting this at
configure time.
|
|
|
|
|
|
|
|
Also removed obsolete CUDD related code.
|
|
C++11 introduced the thread_local keyword, so we don't need to use
non-standard extensions or our custom pthread extension anymore.
The behavior was previously introduced as a workaround in commit
753a072c542c1c254d7c6adbf10e091ba585ede5. This commit
introduces the macro CVC4_THREAD_LOCAL that can be used to
declare variables as thread local. For Swig, this macro is defined to
be empty.
|
|
LFSC now lives outside of the CVC4 repository and is not part of the CVC4 distribution
anymore. As a consequence, we
+ Add --with-lfsc and --with-lfsc-directory as configure options.
In the case where CVC4 has not been built with integrated LFSC, all code that interacts with
LFSC is disabled.
+ Disable proof checking if CVC4_USE_LFSC is not defined.
Configuring the build with --check-proofs but without --with-lfsc results in an error.
+ Do not call LFSC's cleanup function (but we should in the future).
LFSC checker segfaults during cleanup on regression testcase regress0/bv/core/bitvec7.smt.
Disabled call to lfscc_cleanup until the problem in lfscc is fixed.
+ Disable building with LFSC for the distcheck travis build since it is not part of the distribution
anymore. Further, make distcheck with LFSC would require to call contrib/get-lfsc-checker
before calling make check on the temp build (the build of the unpacked distribution tar ball).
|
|
* Find antlr-3.4 directory if installed via contrib/get-antlr-3.4.
|
|
Previously, we were checking whether we should use is_sorted
from std or __gnu_cxx. With C++11, std::is_sorted is
guaranteed to exist. This commit changes
arith/normal_form.{h,cpp} to always use std::is_sorted and
also removes the custom implementations for merge and copy by
using the std implementations instead.
|
|
|
|
This commit fixes two issues that caused the competition configuration to fail on the cluster machines:
We used an ancient version of ABC that declared a function (factorial()
luckySimple.c) in a source file as inline but not static. This issue was fixed
in the following commit:
https://bitbucket.org/alanmi/abc/commits/e0aa7af0d73538fb786c4dcc72745578f0068a38
The issue with non-static inline functions in source files is described in the
following Stackoverflow post:
https://stackoverflow.com/questions/16740515/simple-c-inline-linker-error
This commit updates ABC to a much newer version (commit tagged as abc20160717),
which fixes the issue. One of the modifications previously performed by
contrib/get-abc does not need to be necessary anymore.
CryptoMiniSat was always linked against m4ri, even though it was not getting
compiled with it (-DNOM4RI="ON" in contrib/get-cryptominisat4). This commit
removes the part of config/cryptominisat.m4 that explicitly sets the libraries
linked to and instead uses the result of CVC4_TRY_CRYPTOMINISAT_WITH (which
seems to work even though there is comment indicating otherwise). Further, it
adds -pthread to the libraries required by CryptoMiniSat because it is required
by the version of CryptoMiniSat that we use (a newer version supports disabling
that behavior, so it might be a good idea to update). Previously, this would
lead to linker errors.
Tested with the following configuration:
./configure competition --with-antlr-dir=`pwd`/antlr-3.4 ANTLR=`pwd`/antlr-3.4/bin/antlr3 --enable-static-binary --enable-gpl --with-cln --with-glpk --with-glpk-dir=`pwd`/glpk-cut-log --with-abc --with-abc-dir=`pwd`/abc/alanmi-abc-53f39c11b58d --disable-thread-support --without-readline --disable-shared --with-cryptominisat --with-cryptominisat-dir=`pwd`/cryptominisat4
|
|
|
|
|
|
(mostly whitespace differences).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Add abc to build id and fix static building.
Add abc to --show-config output and Configuration class API.
Add ability to select abc source path.
Fix arch_flags for abc.
|
|
|
|
|
|
master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.
|
|
|
|
|
|
|
|
discussion at Monday meeting)
|
|
Conflicts:
COPYING
NEWS
config/cvc4.m4
|
|
|
|
|
|
|
|
generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
|
|
is now production.
|
|
|
|
|
|
RPM/Debian builds.
|
