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/.

11 files changed, 39 insertions, 39 deletions

diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 77c4d5a09..424f5e0df 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -16,7 +16,7 @@
 # Check if the toml Python module is installed.
 check_python_module("toml")
 
-libcvc4_add_sources(
+libcvc5_add_sources(
   base_handlers.h
   decision_weight.h
   didyoumean.cpp
@@ -66,7 +66,7 @@ set(options_toml_files
 string(REPLACE "toml" "cpp;" options_gen_cpp_files ${options_toml_files})
 string(REPLACE "toml" "h;"   options_gen_h_files ${options_toml_files})
 
-libcvc4_add_sources(GENERATED options.cpp ${options_gen_cpp_files})
+libcvc5_add_sources(GENERATED options.cpp ${options_gen_cpp_files})
 
 list_prepend(options_toml_files "${CMAKE_CURRENT_LIST_DIR}/" abs_toml_files)
 
@@ -88,7 +88,7 @@ add_custom_command(
       module_template.cpp
       options_holder_template.h
       options_template.cpp
-      ${CMAKE_CURRENT_BINARY_DIR}/../../doc/cvc4.1_template
+      ${CMAKE_CURRENT_BINARY_DIR}/../../doc/cvc5.1_template
       ${CMAKE_CURRENT_BINARY_DIR}/../../doc/SmtEngine.3cvc_template
       ${CMAKE_CURRENT_BINARY_DIR}/../../doc/options.3cvc_template
 )
diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index a43641c73..164dd736b 100644
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -4,7 +4,7 @@ header = "options/datatypes_options.h"
 
 # How to handle selectors applied to incorrect constructors.  If this option is set,
 # then we do not rewrite such a selector term to an arbitrary ground term.  
-# For example, by default cvc4 considers cdr( nil ) = nil.  If this option is set, then
+# For example, by default cvc5 considers cdr( nil ) = nil.  If this option is set, then
 # cdr( nil ) has no set value.
 [[option]]
   name       = "dtRewriteErrorSel"
diff --git a/src/options/language.h b/src/options/language.h
index 54e0e9dfa..04182cdd9 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -21,14 +21,14 @@
 #include <ostream>
 #include <string>
 
-#include "cvc4_export.h"
+#include "cvc5_export.h"
 
 namespace cvc5 {
 namespace language {
 
 namespace input {
 
-enum CVC4_EXPORT Language
+enum CVC5_EXPORT Language
 {
   // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
 
@@ -60,7 +60,7 @@ enum CVC4_EXPORT Language
   LANG_MAX
 }; /* enum Language */
 
-inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_EXPORT;
+inline std::ostream& operator<<(std::ostream& out, Language lang) CVC5_EXPORT;
 inline std::ostream& operator<<(std::ostream& out, Language lang) {
   switch(lang) {
   case LANG_AUTO:
@@ -84,7 +84,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
 
 namespace output {
 
-enum CVC4_EXPORT Language
+enum CVC5_EXPORT Language
 {
   // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
 
@@ -119,7 +119,7 @@ enum CVC4_EXPORT Language
   LANG_MAX
 }; /* enum Language */
 
-inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_EXPORT;
+inline std::ostream& operator<<(std::ostream& out, Language lang) CVC5_EXPORT;
 inline std::ostream& operator<<(std::ostream& out, Language lang) {
   switch(lang) {
   case LANG_SMTLIB_V2_6: out << "LANG_SMTLIB_V2_6"; break;
@@ -147,24 +147,24 @@ typedef language::output::Language OutputLanguage;
 namespace language {
 
 /** Is the language a variant of the smtlib version 2 language? */
-bool isInputLang_smt2(InputLanguage lang) CVC4_EXPORT;
-bool isOutputLang_smt2(OutputLanguage lang) CVC4_EXPORT;
+bool isInputLang_smt2(InputLanguage lang) CVC5_EXPORT;
+bool isOutputLang_smt2(OutputLanguage lang) CVC5_EXPORT;
 
 /**
   * Is the language smtlib 2.6 or above? If exact=true, then this method returns
   * false if the input language is not exactly SMT-LIB 2.6.
   */
-bool isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC4_EXPORT;
-bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC4_EXPORT;
+bool isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC5_EXPORT;
+bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC5_EXPORT;
 
 /** Is the language a variant of the SyGuS input language? */
-bool isInputLangSygus(InputLanguage lang) CVC4_EXPORT;
-bool isOutputLangSygus(OutputLanguage lang) CVC4_EXPORT;
+bool isInputLangSygus(InputLanguage lang) CVC5_EXPORT;
+bool isOutputLangSygus(OutputLanguage lang) CVC5_EXPORT;
 
-InputLanguage toInputLanguage(OutputLanguage language) CVC4_EXPORT;
-OutputLanguage toOutputLanguage(InputLanguage language) CVC4_EXPORT;
-InputLanguage toInputLanguage(std::string language) CVC4_EXPORT;
-OutputLanguage toOutputLanguage(std::string language) CVC4_EXPORT;
+InputLanguage toInputLanguage(OutputLanguage language) CVC5_EXPORT;
+OutputLanguage toOutputLanguage(InputLanguage language) CVC5_EXPORT;
+InputLanguage toInputLanguage(std::string language) CVC5_EXPORT;
+OutputLanguage toOutputLanguage(std::string language) CVC5_EXPORT;
 
 }  // namespace language
 }  // namespace cvc5
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 4fe93c129..c28a6f0cf 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -33,7 +33,7 @@
         - module_template.h
 
     Directory <tpl-doc> must contain:
-        - cvc4.1_template
+        - cvc5.1_template
         - options.3cvc_template
         - SmtEngine.3cvc_template
     These files get generated during autogen.sh from the corresponding *.in
@@ -49,7 +49,7 @@
         - <dst>/MODULE_options.cpp
         - <dst>/options_holder.h
         - <dst>/options.cpp
-        - <tpl-doc>/cvc4.1
+        - <tpl-doc>/cvc5.1
         - <tpl-doc>/options.3
         - <tpl-doc>/SmtEngine.3
 """
@@ -1133,7 +1133,7 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder,
         getoption_handlers='\n'.join(getoption_handlers)
     ))
 
-    write_file(doc_dir, 'cvc4.1', tpl_man_cvc.format(
+    write_file(doc_dir, 'cvc5.1', tpl_man_cvc.format(
         man_common='\n'.join(man_common),
         man_others='\n'.join(man_others)
     ))
@@ -1330,7 +1330,7 @@ def mkoptions_main():
     tpl_options_holder = read_tpl(src_dir, 'options_holder_template.h')
 
     # Read documentation template files from documentation directory.
-    tpl_man_cvc = read_tpl(doc_dir, 'cvc4.1_template')
+    tpl_man_cvc = read_tpl(doc_dir, 'cvc5.1_template')
     tpl_man_smt = read_tpl(doc_dir, 'SmtEngine.3cvc_template')
     tpl_man_int = read_tpl(doc_dir, 'options.3cvc_template')
 
diff --git a/src/options/open_ostream.cpp b/src/options/open_ostream.cpp
index fa36738d9..3b13c42e2 100644
--- a/src/options/open_ostream.cpp
+++ b/src/options/open_ostream.cpp
@@ -60,15 +60,16 @@ std::pair< bool, std::ostream* > OstreamOpener::open(const std::string& optarg)
                                     std::ofstream::out | std::ofstream::trunc);
     if(outStream == NULL || !*outStream) {
       std::stringstream ss;
-      ss << "Cannot open " << d_channelName << " file: `"
-         << optarg << "': " << cvc4_errno_failreason();
+      ss << "Cannot open " << d_channelName << " file: `" << optarg
+         << "': " << cvc5_errno_failreason();
       throw OptionException(ss.str());
     }
     return make_pair(true, outStream);
   }
 }
 
-std::string cvc4_errno_failreason() {
+std::string cvc5_errno_failreason()
+{
 #if HAVE_STRERROR_R
 #if STRERROR_R_CHAR_P
   if(errno != 0) {
diff --git a/src/options/open_ostream.h b/src/options/open_ostream.h
index b135ef7ce..162bf3f11 100644
--- a/src/options/open_ostream.h
+++ b/src/options/open_ostream.h
@@ -54,7 +54,7 @@ class OstreamOpener {
 
 }; /* class OstreamOpener */
 
-std::string cvc4_errno_failreason();
+std::string cvc5_errno_failreason();
 
 }  // namespace cvc5
 
diff --git a/src/options/option_exception.h b/src/options/option_exception.h
index 4cfe55a31..f5590709e 100644
--- a/src/options/option_exception.h
+++ b/src/options/option_exception.h
@@ -19,7 +19,7 @@
 #define CVC5__OPTION_EXCEPTION_H
 
 #include "base/exception.h"
-#include "cvc4_export.h"
+#include "cvc5_export.h"
 
 namespace cvc5 {
 
@@ -29,7 +29,7 @@ namespace cvc5 {
  * name is itself unrecognized, a UnrecognizedOptionException (a derived
  * class, below) should be used instead.
  */
-class CVC4_EXPORT OptionException : public cvc5::Exception
+class CVC5_EXPORT OptionException : public cvc5::Exception
 {
  public:
   OptionException(const std::string& s) : cvc5::Exception(s_errPrefix + s) {}
diff --git a/src/options/options.h b/src/options/options.h
index 79b00de30..67707c990 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -25,7 +25,7 @@
 
 #include "base/listener.h"
 #include "base/modal_exception.h"
-#include "cvc4_export.h"
+#include "cvc5_export.h"
 #include "options/language.h"
 #include "options/option_exception.h"
 #include "options/printer_modes.h"
@@ -42,7 +42,7 @@ namespace options {
 
 class OptionsListener;
 
-class CVC4_EXPORT Options
+class CVC5_EXPORT Options
 {
   friend api::Solver;
   /** The struct that holds all option values. */
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 3c5616c73..0e2315aa0 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -15,15 +15,14 @@
 
 #include "options/options_handler.h"
 
+#include <cerrno>
 #include <ostream>
 #include <string>
-#include <cerrno>
-
-#include "cvc4autoconfig.h"
 
 #include "base/check.h"
 #include "base/configuration.h"
 #include "base/configuration_private.h"
+#include "base/cvc5config.h"
 #include "base/exception.h"
 #include "base/modal_exception.h"
 #include "base/output.h"
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 91d06dec2..f24f83b2b 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -15,7 +15,7 @@
 
 #if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__)
 // force use of optreset; mingw32 croaks on argv-switching otherwise
-#include "cvc4autoconfig.h"
+#include "base/cvc5config.h"
 #define _BSD_SOURCE
 #undef HAVE_DECL_OPTRESET
 #define HAVE_DECL_OPTRESET 1
@@ -58,7 +58,7 @@ extern int optreset;
 ${headers_module}$
 
 #include "options/options_holder.h"
-#include "cvc4autoconfig.h"
+#include "base/cvc5config.h"
 #include "options/base_handlers.h"
 
 ${headers_handler}$
diff --git a/src/options/set_language.h b/src/options/set_language.h
index 5ff7cdb7b..45add38ac 100644
--- a/src/options/set_language.h
+++ b/src/options/set_language.h
@@ -20,7 +20,7 @@
 
 #include <iostream>
 
-#include "cvc4_export.h"
+#include "cvc5_export.h"
 #include "options/language.h"
 
 namespace cvc5 {
@@ -29,7 +29,7 @@ namespace language {
 /**
  * IOStream manipulator to set the output language for Exprs.
  */
-class CVC4_EXPORT SetLanguage
+class CVC5_EXPORT SetLanguage
 {
  public:
   /**
@@ -87,7 +87,7 @@ private:
  *
  * The setting stays permanently (until set again) with the stream.
  */
-std::ostream& operator<<(std::ostream& out, SetLanguage l) CVC4_EXPORT;
+std::ostream& operator<<(std::ostream& out, SetLanguage l) CVC5_EXPORT;
 
 }  // namespace language
 }  // namespace cvc5