diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-15 13:04:55 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-15 20:04:55 +0000 |
| commit | 77bca094a140b35341257f125a55212ff0108250 (patch) | |
| tree | 1d3369b9be5fc4c3e8cb279ae5ea662e59cbcb3e /src/parser/smt2 | |
| parent | 63647b1d79df6f287ea6599958b16fce44b8271d (diff) | |
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.
Diffstat (limited to 'src/parser/smt2')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 8 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 2 |
2 files changed, 5 insertions, 5 deletions
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."); |