Move LFSC checker out of the CVC repository. (#222)
authorAina Niemetz <aina.niemetz@gmail.com>
Fri, 25 Aug 2017 22:39:16 +0000 (15:39 -0700)
committerGitHub <noreply@github.com>
Fri, 25 Aug 2017 22:39:16 +0000 (15:39 -0700)
commitdfa69ff98a14fcc0f2387e59a0c9994ef440e7d0
tree23031231926757cb9b8aab425d8354683a3a66d7
parent378a0c45070ec033493c52e4fa92e6d03b89b6c0
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).
40 files changed:
.travis.yml
Makefile.am
config/lfsc.m4 [new file with mode: 0644]
configure.ac
contrib/get-lfsc-checker [new file with mode: 0755]
proofs/lfsc_checker/.gitignore [deleted file]
proofs/lfsc_checker/AUTHORS [deleted file]
proofs/lfsc_checker/COPYING [deleted file]
proofs/lfsc_checker/INSTALL [deleted file]
proofs/lfsc_checker/Makefile.am [deleted file]
proofs/lfsc_checker/NEWS [deleted file]
proofs/lfsc_checker/README [deleted file]
proofs/lfsc_checker/check.cpp [deleted file]
proofs/lfsc_checker/check.h [deleted file]
proofs/lfsc_checker/chunking_memory_management.h [deleted file]
proofs/lfsc_checker/code.cpp [deleted file]
proofs/lfsc_checker/code.h [deleted file]
proofs/lfsc_checker/config/ax_cxx_compile_stdcxx.m4 [deleted symlink]
proofs/lfsc_checker/config/ax_cxx_compile_stdcxx_11.m4 [deleted symlink]
proofs/lfsc_checker/configure.ac [deleted file]
proofs/lfsc_checker/expr.cpp [deleted file]
proofs/lfsc_checker/expr.h [deleted file]
proofs/lfsc_checker/libwriter.cpp [deleted file]
proofs/lfsc_checker/libwriter.h [deleted file]
proofs/lfsc_checker/main.cpp [deleted file]
proofs/lfsc_checker/position.h [deleted file]
proofs/lfsc_checker/print_smt2.cpp [deleted file]
proofs/lfsc_checker/print_smt2.h [deleted file]
proofs/lfsc_checker/scccode.cpp [deleted file]
proofs/lfsc_checker/scccode.h [deleted file]
proofs/lfsc_checker/sccwriter.cpp [deleted file]
proofs/lfsc_checker/sccwriter.h [deleted file]
proofs/lfsc_checker/trie.cpp [deleted file]
proofs/lfsc_checker/trie.h [deleted file]
src/Makefile.am
src/base/configuration_private.h
src/options/options_handler.cpp
src/options/options_handler.h
src/options/smt_options
src/smt/smt_engine_check_proof.cpp