diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-08-25 15:39:16 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-08-25 15:39:16 -0700 |
commit | dfa69ff98a14fcc0f2387e59a0c9994ef440e7d0 (patch) | |
tree | 23031231926757cb9b8aab425d8354683a3a66d7 /contrib | |
parent | 378a0c45070ec033493c52e4fa92e6d03b89b6c0 (diff) |
Move LFSC checker out of the CVC repository. (#222)
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).
Diffstat (limited to 'contrib')
-rwxr-xr-x | contrib/get-lfsc-checker | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/contrib/get-lfsc-checker b/contrib/get-lfsc-checker new file mode 100755 index 000000000..495082387 --- /dev/null +++ b/contrib/get-lfsc-checker @@ -0,0 +1,51 @@ +#!/bin/bash +# +set -e + +lfscrepo="https://github.com/CVC4/LFSC.git" +dirname="lfsc-checker" + + +cd "$(dirname "$0")/.." + +if ! [ -e src/parser/cvc/Cvc.g ]; then + echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2 + echo "but apparently:" >&2 + echo >&2 + echo " $(pwd)" >&2 + echo >&2 + echo "is not a CVC4 source tree ?!" >&2 + exit 1 +fi + +function gitclone { + if which git &> /dev/null + then + git clone "$1" "$2" + else + echo "Need git to clone LFSC checker. Please install git." >&2 + exit 1 + fi +} + +if [ -e lfsc-checker ]; then + echo 'error: file or directory "lfsc-checker" already exists!' >&2 + exit 1 +fi + +mkdir $dirname +cd $dirname + +LFSC_PATH=`pwd` + +gitclone $lfscrepo . +mkdir install +mkdir build +cd build +cmake -DCMAKE_INSTALL_PREFIX:PATH=$LFSC_PATH/install .. +make install +cd .. + +echo +echo ===================== Now configure CVC4 with ===================== +echo ./configure --with-lfsc |