diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-04-21 10:21:34 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-21 10:21:34 -0700 |
commit | ae5ee4b07dc3d3c792e7fe7f382ff490dd28aca4 (patch) | |
tree | a7c2ab8013f46dbea75fcd6e7da3fb83e2012b2f /src/main | |
parent | 86aa9bc35ba9dc9a57913a2ffc71619c7657cc35 (diff) |
Goodbye CVC4, hello cvc5! (#6371)
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/CMakeLists.txt | 42 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 7 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 8 | ||||
-rw-r--r-- | src/main/main.cpp | 6 | ||||
-rw-r--r-- | src/main/main.h | 14 | ||||
-rw-r--r-- | src/main/signal_handlers.cpp | 26 | ||||
-rw-r--r-- | src/main/time_limit.cpp | 2 |
7 files changed, 49 insertions, 56 deletions
diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index 868b7f97d..029397832 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -26,11 +26,11 @@ set(libmain_src_files ) #-----------------------------------------------------------------------------# -# Build object library since we will use the object files for cvc4-bin and +# Build object library since we will use the object files for cvc5-bin and # main-test library. add_library(main OBJECT ${libmain_src_files}) -target_compile_definitions(main PRIVATE -D__BUILDING_CVC4DRIVER) +target_compile_definitions(main PRIVATE -D__BUILDING_CVC5DRIVER) if(ENABLE_SHARED) set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE ON) endif() @@ -39,8 +39,8 @@ endif() # supported for cmake version >= 3.12. Hence, we have to manually add the # library dependencies for main. As a consequence, include directories from # dependencies are not propagated and we need to manually add the include -# directories of libcvc4 to main. -add_dependencies(main cvc4 cvc4parser gen-tokens) +# directories of libcvc5 to main. +add_dependencies(main cvc5 cvc5parser gen-tokens) # Note: This should not be required anymore as soon as we get rid of the # smt_engine.h include in src/main. smt_engine.h has transitive includes @@ -56,35 +56,35 @@ target_include_directories(main PRIVATE ${GMP_INCLUDES}) # that we don't have to include all object files of main into each api/unit # test. Do not link against main-test in any other case. add_library(main-test driver_unified.cpp $<TARGET_OBJECTS:main>) -target_compile_definitions(main-test PRIVATE -D__BUILDING_CVC4DRIVER) -target_link_libraries(main-test PUBLIC cvc4 cvc4parser) +target_compile_definitions(main-test PRIVATE -D__BUILDING_CVC5DRIVER) +target_link_libraries(main-test PUBLIC cvc5 cvc5parser) if(USE_CLN) target_link_libraries(main-test PUBLIC CLN) endif() target_link_libraries(main-test PUBLIC GMP) #-----------------------------------------------------------------------------# -# cvc4 binary configuration +# cvc5 binary configuration -add_executable(cvc4-bin driver_unified.cpp main.cpp $<TARGET_OBJECTS:main>) -target_compile_definitions(cvc4-bin PRIVATE -D__BUILDING_CVC4DRIVER) -set_target_properties(cvc4-bin +add_executable(cvc5-bin driver_unified.cpp main.cpp $<TARGET_OBJECTS:main>) +target_compile_definitions(cvc5-bin PRIVATE -D__BUILDING_CVC5DRIVER) +set_target_properties(cvc5-bin PROPERTIES - OUTPUT_NAME cvc4 + OUTPUT_NAME cvc5 RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) -target_link_libraries(cvc4-bin PUBLIC cvc4 cvc4parser) +target_link_libraries(cvc5-bin PUBLIC cvc5 cvc5parser) if(USE_CLN) - target_link_libraries(cvc4-bin PUBLIC CLN) + target_link_libraries(cvc5-bin PUBLIC CLN) endif() -target_link_libraries(cvc4-bin PUBLIC GMP) +target_link_libraries(cvc5-bin PUBLIC GMP) if(PROGRAM_PREFIX) install(PROGRAMS - $<TARGET_FILE:cvc4-bin> + $<TARGET_FILE:cvc5-bin> DESTINATION ${CMAKE_INSTALL_BINDIR} - RENAME ${PROGRAM_PREFIX}cvc4) + RENAME ${PROGRAM_PREFIX}cvc5) else() - install(TARGETS cvc4-bin + install(TARGETS cvc5-bin DESTINATION ${CMAKE_INSTALL_BINDIR}) endif() @@ -93,13 +93,13 @@ endif() # https://cmake.org/cmake/help/v3.0/prop_tgt/LINK_SEARCH_START_STATIC.html # https://cmake.org/cmake/help/v3.0/prop_tgt/LINK_SEARCH_END_STATIC.html if(ENABLE_STATIC_BINARY) - set_target_properties(cvc4-bin PROPERTIES LINK_FLAGS -static) - set_target_properties(cvc4-bin PROPERTIES LINK_SEARCH_START_STATIC ON) - set_target_properties(cvc4-bin PROPERTIES LINK_SEARCH_END_STATIC ON) + set_target_properties(cvc5-bin PROPERTIES LINK_FLAGS -static) + set_target_properties(cvc5-bin PROPERTIES LINK_SEARCH_START_STATIC ON) + set_target_properties(cvc5-bin PROPERTIES LINK_SEARCH_END_STATIC ON) endif() if(USE_EDITLINE) - target_link_libraries(cvc4-bin PUBLIC ${Editline_LIBRARIES}) + target_link_libraries(cvc5-bin PUBLIC ${Editline_LIBRARIES}) target_link_libraries(main-test PUBLIC ${Editline_LIBRARIES}) target_include_directories(main PUBLIC ${Editline_INCLUDE_DIRS}) endif() diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 2481eda10..9b0ea4759 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * Driver for cvc5 executable (cvc4). + * Driver for cvc5 executable (cvc5). */ #include <stdio.h> @@ -26,8 +26,8 @@ #include "api/cpp/cvc5.h" #include "base/configuration.h" +#include "base/cvc5config.h" #include "base/output.h" -#include "cvc4autoconfig.h" #include "main/command_executor.h" #include "main/interactive_shell.h" #include "main/main.h" @@ -91,7 +91,8 @@ void printUsage(Options& opts, bool full) { } } -int runCvc4(int argc, char* argv[], Options& opts) { +int runCvc5(int argc, char* argv[], Options& opts) +{ main::totalTime = std::make_unique<TotalTimer>(); // For the signal handlers' benefit pOptions = &opts; diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 127b2c14d..516f9e621 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -27,7 +27,7 @@ #include <vector> // This must go before HAVE_LIBEDITLINE. -#include "cvc4autoconfig.h" +#include "base/cvc5config.h" #if HAVE_LIBEDITLINE #include <editline/readline.h> @@ -112,13 +112,13 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) OutputLanguage lang = toOutputLanguage(d_options.getInputLanguage()); switch(lang) { case output::LANG_CVC: - d_historyFilename = string(getenv("HOME")) + "/.cvc4_history"; + d_historyFilename = string(getenv("HOME")) + "/.cvc5_history"; commandsBegin = cvc_commands; commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands); break; case output::LANG_TPTP: - d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_tptp"; + d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_tptp"; commandsBegin = tptp_commands; commandsEnd = tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands); @@ -126,7 +126,7 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) default: if (language::isOutputLang_smt2(lang)) { - d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2"; + d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_smtlib2"; commandsBegin = smt2_commands; commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands); diff --git a/src/main/main.cpp b/src/main/main.cpp index a4e70be89..6a7baebb3 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -41,13 +41,13 @@ using namespace cvc5::language; * cvc5's main() routine is just an exception-safe wrapper around cvc5. * Please don't construct anything here. Even if the constructor is * inside the try { }, an exception during destruction can cause - * problems. That's why main() wraps runCvc4() in the first place. - * Put everything in runCvc4(). + * problems. That's why main() wraps runCvc5() in the first place. + * Put everything in runCvc5(). */ int main(int argc, char* argv[]) { Options opts; try { - return runCvc4(argc, argv, opts); + return runCvc5(argc, argv, opts); } catch(OptionException& e) { #ifdef CVC5_COMPETITION_MODE *opts.getOut() << "unknown" << endl; diff --git a/src/main/main.h b/src/main/main.h index 121f9d951..54abbdbe9 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -18,8 +18,8 @@ #include <memory> #include <string> +#include "base/cvc5config.h" #include "base/exception.h" -#include "cvc4autoconfig.h" #include "options/options.h" #ifndef CVC5__MAIN__MAIN_H @@ -62,19 +62,11 @@ extern bool segvSpin; /** A pointer to the options in play */ extern thread_local Options* pOptions; -/** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. - * This can throw a cvc5::Exception. - */ -void cvc4_init(); - -/** Shutdown the driver. Frees memory for the signal handlers. */ -void cvc4_shutdown() noexcept; - } // namespace main } // namespace cvc5 -/** Actual Cvc4 driver functions **/ -int runCvc4(int argc, char* argv[], cvc5::Options&); +/** Actual cvc5 driver functions **/ +int runCvc5(int argc, char* argv[], cvc5::Options&); void printUsage(cvc5::Options&, bool full = false); #endif /* CVC5__MAIN__MAIN_H */ diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp index 9a6e34075..503bbc198 100644 --- a/src/main/signal_handlers.cpp +++ b/src/main/signal_handlers.cpp @@ -32,8 +32,8 @@ #endif /* __WIN32__ */ +#include "base/cvc5config.h" #include "base/exception.h" -#include "cvc4autoconfig.h" #include "main/command_executor.h" #include "main/main.h" #include "options/options.h" @@ -73,8 +73,8 @@ void timeout_handler() #ifndef __WIN32__ #ifdef HAVE_SIGALTSTACK -size_t cvc4StackSize; -void* cvc4StackBase; +size_t stackSize; +void* stackBase; #endif /* HAVE_SIGALTSTACK */ /** Handler for SIGXCPU and SIGALRM, i.e., timeout. */ @@ -100,15 +100,15 @@ void sigint_handler(int sig, siginfo_t* info, void*) /** Handler for SIGSEGV (segfault). */ void segv_handler(int sig, siginfo_t* info, void* c) { - uintptr_t extent = reinterpret_cast<uintptr_t>(cvc4StackBase) - cvc4StackSize; + uintptr_t extent = reinterpret_cast<uintptr_t>(stackBase) - stackSize; uintptr_t addr = reinterpret_cast<uintptr_t>(info->si_addr); #ifdef CVC5_DEBUG safe_print(STDERR_FILENO, "cvc5 suffered a segfault in DEBUG mode.\n"); safe_print(STDERR_FILENO, "Offending address is "); safe_print(STDERR_FILENO, info->si_addr); safe_print(STDERR_FILENO, "\n"); - // cerr << "base is " << (void*)cvc4StackBase << endl; - // cerr << "size is " << cvc4StackSize << endl; + // cerr << "base is " << (void*)stackBase << endl; + // cerr << "size is " << stackSize << endl; // cerr << "extent is " << (void*)extent << endl; if (addr >= extent && addr <= extent + 10 * 1024) { @@ -211,7 +211,7 @@ void ill_handler(int sig, siginfo_t* info, void*) static terminate_handler default_terminator; -void cvc4terminate() +void cvc5terminate() { set_terminate(default_terminator); #ifdef CVC5_DEBUG @@ -301,8 +301,8 @@ void install() throw Exception(string("sigaltstack() failure: ") + strerror(errno)); } - cvc4StackSize = limit.rlim_cur; - cvc4StackBase = ss.ss_sp; + stackSize = limit.rlim_cur; + stackBase = ss.ss_sp; struct sigaction act4; act4.sa_sigaction = segv_handler; @@ -325,16 +325,16 @@ void install() #endif /* __WIN32__ */ - default_terminator = set_terminate(cvc4terminate); + default_terminator = set_terminate(cvc5terminate); } void cleanup() noexcept { #ifndef __WIN32__ #ifdef HAVE_SIGALTSTACK - free(cvc4StackBase); - cvc4StackBase = NULL; - cvc4StackSize = 0; + free(stackBase); + stackBase = nullptr; + stackSize = 0; #endif /* HAVE_SIGALTSTACK */ #endif /* __WIN32__ */ } diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp index bd41ed7ed..82cfda017 100644 --- a/src/main/time_limit.cpp +++ b/src/main/time_limit.cpp @@ -41,7 +41,7 @@ #include "time_limit.h" -#include "cvc4autoconfig.h" +#include "base/cvc5config.h" #if HAVE_SETITIMER #include <signal.h> |