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 | |
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')
-rw-r--r-- | src/parser/antlr_input.cpp | 9 | ||||
-rw-r--r-- | src/parser/antlr_input_imports.cpp | 14 | ||||
-rw-r--r-- | src/parser/antlr_line_buffered_input.h | 2 | ||||
-rw-r--r-- | src/parser/antlr_tracing.h | 4 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 26 | ||||
-rw-r--r-- | src/parser/cvc/README | 30 | ||||
-rw-r--r-- | src/parser/parser.h | 13 | ||||
-rw-r--r-- | src/parser/parser_builder.h | 2 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 8 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 2 | ||||
-rw-r--r-- | src/parser/tptp/Tptp.g | 2 |
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 */ |