Rename occurrences of CVC4 to CVC5. (#6351)

This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.

11 files changed, 57 insertions, 55 deletions

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 7690d8962..de90ee14b 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -239,10 +239,11 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
   AntlrInput* input;
 
   switch(lang) {
-  case LANG_CVC4: {
-    input = new CvcInput(inputStream);
-    break;
-  }
+    case LANG_CVC:
+    {
+      input = new CvcInput(inputStream);
+      break;
+    }
 
   case LANG_SYGUS_V2: input = new SygusInput(inputStream); break;
 
diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp
index 738f4c6e2..c04349491 100644
--- a/src/parser/antlr_input_imports.cpp
+++ b/src/parser/antlr_input_imports.cpp
@@ -18,7 +18,7 @@
 
 /*
  * The functions in this file are based on implementations in libantlr3c,
- * with only minor CVC4-specific changes.
+ * with only minor cvc5-specific changes.
  */
 
 // [The "BSD licence"]
@@ -79,7 +79,7 @@ namespace parser {
 ///
 /// If you override, make sure to update errorCount if you care about that.
 ///
-/* *** CVC4 NOTE ***
+/* *** cvc5 NOTE ***
  * This function is has been modified in not-completely-trivial ways from its
  * libantlr3c implementation to support more informative error messages and to
  * invoke the error reporting mechanism of the Input class instead of the
@@ -90,7 +90,7 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
   pANTLR3_UINT8 * tokenNames = recognizer->state->tokenNames;
   stringstream ss;
 
-  // Dig the CVC4 objects out of the ANTLR3 mess
+  // Dig the cvc5 objects out of the ANTLR3 mess
   pANTLR3_PARSER antlr3Parser = (pANTLR3_PARSER)(recognizer->super);
   Assert(antlr3Parser != NULL);
   Parser *parser = (Parser*)(antlr3Parser->super);
@@ -285,7 +285,7 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
 ///
 /// \see nextToken
 ///
-/* *** CVC4 NOTE ***
+/* *** cvc5 NOTE ***
  * This is copied, largely unmodified, from antlr3lexer.c
  *
  */
@@ -346,7 +346,7 @@ AntlrInput::nextTokenStr (pANTLR3_TOKEN_SOURCE toksource)
         // Recognition exception, report it and try to recover.
         //
         lexer->rec->state->failed = ANTLR3_TRUE;
-        // *** CVC4 EDIT: Just call the AntlrInput error routine
+        // *** cvc5 EDIT: Just call the AntlrInput error routine
         lexerError(lexer->rec);
         lexer->recover(lexer);
       }
@@ -356,7 +356,7 @@ AntlrInput::nextTokenStr (pANTLR3_TOKEN_SOURCE toksource)
         {
           // Emit the real token, which adds it in to the token stream basically
           //
-          // *** CVC4 Edit: call emit on the lexer object
+          // *** cvc5 Edit: call emit on the lexer object
           lexer->emit(lexer);
         }
         else if (lexer->rec->state->token == &(toksource->skipToken))
@@ -375,7 +375,7 @@ AntlrInput::nextTokenStr (pANTLR3_TOKEN_SOURCE toksource)
   }
 }
 
-/* *** CVC4 NOTE ***
+/* *** cvc5 NOTE ***
  * This is copied, totaly unmodified, from antlr3lexer.c
  * in order to use nextTokenStr previously defined.
  *
diff --git a/src/parser/antlr_line_buffered_input.h b/src/parser/antlr_line_buffered_input.h
index 3203e815b..c92f2d496 100644
--- a/src/parser/antlr_line_buffered_input.h
+++ b/src/parser/antlr_line_buffered_input.h
@@ -14,7 +14,7 @@
  *
  * By default, ANTLR expects the whole input to be in a single, consecutive
  * buffer. When doing incremental solving and the input is coming from the
- * standard input, this is problematic because CVC4 might receive new input
+ * standard input, this is problematic because cvc5 might receive new input
  * based on the result of solving the existing input.
  *
  * This file overwrites the _LA and the consume functions of the input streamto
diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h
index cd1066383..595a2d784 100644
--- a/src/parser/antlr_tracing.h
+++ b/src/parser/antlr_tracing.h
@@ -54,7 +54,7 @@ static struct __Cvc4System {
   struct JavaPrinter {
     template <class T>
     JavaPrinter operator+(const T& t) const {
-      CVC4Message() << t;
+      CVC5Message() << t;
       return JavaPrinter();
     }
   };/* struct JavaPrinter */
@@ -67,7 +67,7 @@ static struct __Cvc4System {
      * to the call-by-value semantics of C.  All that's left to
      * do is print the newline.
      */
-    void println(JavaPrinter) { CVC4Message() << std::endl; }
+    void println(JavaPrinter) { CVC5Message() << std::endl; }
   } out;
 } System;
 
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index f78426eda..2ad56d6e4 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -23,7 +23,7 @@ options {
   // defaultErrorHandler = false;
 
   // Only lookahead of <= k requested (disable for LL* parsing)
-  // Note that CVC4's BoundedTokenBuffer requires a fixed k !
+  // Note that cvc5's BoundedTokenBuffer requires a fixed k !
   // If you change this k, change it also in cvc_input.cpp !
   k = 3;
 }/* options */
@@ -555,7 +555,7 @@ api::Term addNots(api::Solver* s, size_t n, api::Term e) {
 
 namespace cvc5 {
   class Expr;
-}/* CVC4 namespace */
+}/* cvc5 namespace */
 
 }/* @parser::includes */
 
@@ -633,16 +633,16 @@ parseCommand returns [cvc5::Command* cmd_return = NULL]
     { std::string s = AntlrInput::tokenText($IDENTIFIER);
     if(s == "benchmark") {
         PARSER_STATE->parseError(
-            "In CVC4 presentation language mode, but SMT-LIBv1 format "
+            "In cvc5 presentation language mode, but SMT-LIBv1 format "
             "detected, which is not supported anymore.");
       } else if(s == "set" || s == "get" || s == "declare" ||
                 s == "define" || s == "assert") {
         PARSER_STATE->parseError(
-            "In CVC4 presentation language mode, but SMT-LIB format detected. "
+            "In cvc5 presentation language mode, but SMT-LIB format detected. "
             "Use --lang smt for SMT-LIB support.");
       } else {
         PARSER_STATE->parseError(
-            "A CVC4 presentation language command cannot begin with a "
+            "A cvc5 presentation language command cannot begin with a "
             "parenthesis; expected command name.");
       }
     }
@@ -798,24 +798,24 @@ mainCommand[std::unique_ptr<cvc5::Command>* cmd]
   | DBG_TOK
     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
       { Debug.on(s); Trace.on(s); }
-    | { CVC4Message() << "Please specify what to debug." << std::endl; }
+    | { CVC5Message() << "Please specify what to debug." << std::endl; }
     )
 
   | TRACE_TOK
     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
       { Trace.on(s); }
-    | { CVC4Message() << "Please specify something to trace." << std::endl; }
+    | { CVC5Message() << "Please specify something to trace." << std::endl; }
     )
   | UNTRACE_TOK
     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
       { Trace.off(s); }
-    | { CVC4Message() << "Please specify something to untrace." << std::endl; }
+    | { CVC5Message() << "Please specify something to untrace." << std::endl; }
     )
 
   | HELP_TOK
     ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
-      { CVC4Message() << "No help available for `" << s << "'." << std::endl; }
-  |   { CVC4Message() << "Please use --help at the command line for help."
+      { CVC5Message() << "No help available for `" << s << "'." << std::endl; }
+  |   { CVC5Message() << "Please use --help at the command line for help."
                 << std::endl; }
             )
 
@@ -1104,7 +1104,7 @@ declareVariables[std::unique_ptr<cvc5::Command>* cmd, cvc5::api::Sort& t,
                             << "with type " << oldType << std::endl;
             if(oldType != t) {
               std::stringstream ss;
-              ss << language::SetLanguage(language::output::LANG_CVC4)
+              ss << language::SetLanguage(language::output::LANG_CVC)
                  << "incompatible type for `" << *i << "':" << std::endl
                  << "  old type: " << oldType << std::endl
                  << "  new type: " << t << std::endl;
@@ -1394,7 +1394,7 @@ typeLetDecl[cvc5::parser::DeclarationCheck check]
   ;
 
 /**
- * Matches a CVC4 expression.  Formulas and terms are not really
+ * Matches a cvc5 expression.  Formulas and terms are not really
  * distinguished during parsing; please ignore the naming of the
  * grammar rules.
  *
@@ -1526,7 +1526,7 @@ letDecl
 }
   : identifier[name,CHECK_NONE,SYM_VARIABLE] EQUAL_TOK formula[e]
     {
-      Debug("parser") << language::SetLanguage(language::output::LANG_CVC4)
+      Debug("parser") << language::SetLanguage(language::output::LANG_CVC)
                       << e.getSort() << std::endl;
       PARSER_STATE->defineVar(name, e);
       Debug("parser") << "LET[" << PARSER_STATE->scopeLevel() << "]: "
diff --git a/src/parser/cvc/README b/src/parser/cvc/README
index 513a8e85a..df6c82de9 100644
--- a/src/parser/cvc/README
+++ b/src/parser/cvc/README
@@ -1,4 +1,4 @@
-Notes on CVC4's CVC language parser.
+Notes on cvc5's CVC language parser.
 
 This language parser attempts to maintain some backward compatibility
 with previous versions of the language.  However, as the language
@@ -9,21 +9,21 @@ need to be removed.
 In order to support our users, we have tried to parse what CVC3 could
 and (at least) offer an error when a feature is unavailable or
 unimplemented.  But this is not always possible.  Please report a
-bug if a particular discrepancy between CVC3 and CVC4 handling of
+bug if a particular discrepancy between CVC3 and cvc5 handling of
 the CVC language is a concern to you; we may be able to add a
 compatibility mode, or at least offer better warnings or errors.
 
-Below is a list of the known differences between CVC3's and CVC4's
+Below is a list of the known differences between CVC3's and cvc5's
 version of the CVC language.  This is the list of differences in
-language design and parsing ONLY.  The featureset of CVC4 is
+language design and parsing ONLY.  The featureset of cvc5 is
 rapidly expanding, but does not match CVC3's breadth yet.  However,
-CVC4 should tell you of an unimplemented feature if you try to use
+cvc5 should tell you of an unimplemented feature if you try to use
 it (rather than giving a cryptic parse or assertion error).
 
-* CVC4 does not add the current assumptions to the scope after
+* cvc5 does not add the current assumptions to the scope after
   SAT/INVALID responses like CVC3 did.
 
-* CVC4 no longer supports the "old" function syntax:
+* cvc5 no longer supports the "old" function syntax:
 
     f : [INT -> INT];
 
@@ -37,21 +37,21 @@ it (rather than giving a cryptic parse or assertion error).
 * QUERY and CHECKSAT do not add their argument to the current
   list of assertions like CVC3 did.
 
-* CVC4 allows datatypes to hold complex types that contain self-
+* cvc5 allows datatypes to hold complex types that contain self-
   or mutual references.  For example,
 
     DATATYPE tree = node(children:ARRAY INT OF tree) | leaf(data:INT) END;
 
-  is permissible in CVC4 but not in CVC3.
+  is permissible in cvc5 but not in CVC3.
 
-* CVC4 supports parameterized types in datatype definitions, e.g.
+* cvc5 supports parameterized types in datatype definitions, e.g.
 
     DATATYPE list[T] = cons(car:T) | nil END;
 
   You can then declare "x : list[INT];" or "x : list[list[INT]];",
   for example.
 
-* CVC4 supports type ascriptions, e.g.
+* cvc5 supports type ascriptions, e.g.
 
     U : TYPE;
     f : INT -> U;
@@ -70,16 +70,16 @@ it (rather than giving a cryptic parse or assertion error).
     DATATYPE Item = Carrots | Butter | Milk | Bread END;
     groceries : list[Item] = cons(Butter, cons(Bread, nil:list[INT]));
 
-* CVC4 supports stronger distinction between type and variable names.
-  This means that CVC4 may allow you to declare things that CVC3 does
+* cvc5 supports stronger distinction between type and variable names.
+  This means that cvc5 may allow you to declare things that CVC3 does
   not:
 
     a : TYPE;
     a : INT; % CVC3 complains
-    a : a; % CVC4 complains, `a' cannot both be INT and `a'
+    a : a; % cvc5 complains, `a' cannot both be INT and `a'
     b : a; % No problem, `a' is both the type of `b', and an INT
 
-* CVC4 supports a command-level LET syntax, e.g.:
+* cvc5 supports a command-level LET syntax, e.g.:
 
     LET double = LAMBDA(x:INT) : 2*x IN
       QUERY double(5) = 10;
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 3382d25eb..da35606c1 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -391,7 +391,7 @@ public:
    */
   void checkFunctionLike(api::Term fun);
 
-  /** Create a new CVC4 variable expression of the given type.
+  /** Create a new cvc5 variable expression of the given type.
    *
    * It is inserted at context level zero in the symbol table if levelZero is
    * true, or if we are using global declarations.
@@ -407,7 +407,7 @@ public:
                     bool doOverload = false);
 
   /**
-   * Create a set of new CVC4 variable expressions of the given type.
+   * Create a set of new cvc5 variable expressions of the given type.
    *
    * It is inserted at context level zero in the symbol table if levelZero is
    * true, or if we are using global declarations.
@@ -423,12 +423,12 @@ public:
                                   bool doOverload = false);
 
   /**
-   * Create a new CVC4 bound variable expression of the given type. This binds
+   * Create a new cvc5 bound variable expression of the given type. This binds
    * the symbol name to that variable in the current scope.
    */
   api::Term bindBoundVar(const std::string& name, const api::Sort& type);
   /**
-   * Create a new CVC4 bound variable expressions of the given names and types.
+   * Create a new cvc5 bound variable expressions of the given names and types.
    * Like the method above, this binds these names to those variables in the
    * current scope.
    */
@@ -436,11 +436,12 @@ public:
       std::vector<std::pair<std::string, api::Sort> >& sortedVarNames);
 
   /**
-   * Create a set of new CVC4 bound variable expressions of the given type.
+   * Create a set of new cvc5 bound variable expressions of the given type.
    *
    * For each name, if a symbol with name already exists,
    *  then if doOverload is true, we create overloaded operators.
-   *  else if doOverload is false, the existing expression is shadowed by the new expression.
+   *  else if doOverload is false, the existing expression is shadowed by the
+   * new expression.
    */
   std::vector<api::Term> bindBoundVars(const std::vector<std::string> names,
                                        const api::Sort& type);
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 87fef8e93..b0f9e35e6 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -152,7 +152,7 @@ class CVC4_EXPORT ParserBuilder
    * parse would otherwise be an incorrect parse tree and the error
    * would go undetected.  This is specifically for circumstances
    * where the parser is ahead of the functionality present elsewhere
-   * in CVC4 (such as quantifiers, subtypes, records, etc. in the CVC
+   * in cvc5 (such as quantifiers, subtypes, records, etc. in the CVC
    * language parser).
    */
   ParserBuilder& withParseOnly(bool flag = true);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 16eba8fb3..34fabed0d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -23,7 +23,7 @@ options {
   // defaultErrorHandler = false;
 
   // Only lookahead of <= k requested (disable for LL* parsing)
-  // Note that CVC4's BoundedTokenBuffer requires a fixed k !
+  // Note that cvc5's BoundedTokenBuffer requires a fixed k !
   // If you change this k, change it also in smt2_input.cpp !
   k = 2;
 }/* options */
@@ -91,7 +91,7 @@ namespace cvc5 {
     class Sort;
   }
   
-}/* CVC4 namespace */
+}/* cvc5 namespace */
 
 }/* @parser::includes */
 
@@ -483,7 +483,7 @@ command [std::unique_ptr<cvc5::Command>* cmd]
     /* New SMT-LIB 2.5 command set */
   | smt25Command[cmd]
 
-    /* CVC4-extended SMT-LIB commands */
+    /* cvc5-extended SMT-LIB commands */
   | extendedCommand[cmd]
     { if(PARSER_STATE->strictModeEnabled()) {
         PARSER_STATE->parseError(
@@ -632,7 +632,7 @@ sygusGrammar[cvc5::api::Grammar*& ret,
               << "2.0 format requires a predeclaration of the non-terminal "
               << "symbols of the grammar to be given prior to the definition "
               << "of the grammar. See https://sygus.org/language/ for details "
-              << "and examples. CVC4 versions past 1.8 do not support SyGuS "
+              << "and examples. cvc5 versions past 1.8 do not support SyGuS "
               << "version 1.0.";
         }
         else
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 19b343a66..10396d1dc 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -732,7 +732,7 @@ void Smt2::checkThatLogicIsSet()
       else
       {
         warning("No set-logic command was given before this point.");
-        warning("CVC4 will make all theories available.");
+        warning("cvc5 will make all theories available.");
         warning(
             "Consider setting a stricter logic for (likely) better "
             "performance.");
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 3932b8f7d..6877306a2 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -25,7 +25,7 @@ options {
   // defaultErrorHandler = false;
 
   // Only lookahead of <= k requested (disable for LL* parsing)
-  // Note that CVC4's BoundedTokenBuffer requires a fixed k !
+  // Note that cvc5's BoundedTokenBuffer requires a fixed k !
   // If you change this k, change it also in tptp_input.cpp !
   k = 2;
 }/* options */