diff options
Diffstat (limited to 'src/parser')
39 files changed, 447 insertions, 447 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index ac9417197..a818f4148 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -34,11 +34,11 @@ #include "parser/tptp/tptp_input.h" using namespace std; -using namespace CVC5; -using namespace CVC5::parser; -using namespace CVC5::kind; +using namespace cvc5; +using namespace cvc5::parser; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace parser { // These functions exactly wrap the antlr3 source inconsistencies. @@ -582,4 +582,4 @@ void AntlrInput::setAntlr3Parser(pANTLR3_PARSER pParser) { } } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index de0d563ef..c7cb60af7 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -36,7 +36,7 @@ #include "util/integer.h" #include "util/rational.h" -namespace CVC5 { +namespace cvc5 { namespace parser { /** Wrapper around an ANTLR3 input stream. */ @@ -292,6 +292,6 @@ inline BitVector AntlrInput::tokenToBitvector(pANTLR3_COMMON_TOKEN number, pANTL } } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__ANTLR_INPUT_H */ diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp index 98c071ed3..bceaa5586 100644 --- a/src/parser/antlr_input_imports.cpp +++ b/src/parser/antlr_input_imports.cpp @@ -60,7 +60,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { namespace parser { /// Report a recognition problem. @@ -436,4 +436,4 @@ AntlrInput::nextToken (pANTLR3_TOKEN_SOURCE toksource) } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp index 66ebff7b3..1dd7c953c 100644 --- a/src/parser/antlr_line_buffered_input.cpp +++ b/src/parser/antlr_line_buffered_input.cpp @@ -38,7 +38,7 @@ #include "base/check.h" #include "base/output.h" -namespace CVC5 { +namespace cvc5 { namespace parser { static pANTLR3_INPUT_STREAM antlr3CreateLineBufferedStream( @@ -218,8 +218,8 @@ setupInputStream(pANTLR3_INPUT_STREAM input) static ANTLR3_UCHAR bufferedInputLA(pANTLR3_INT_STREAM is, ANTLR3_INT32 la) { pANTLR3_INPUT_STREAM input = ((pANTLR3_INPUT_STREAM)(is->super)); - CVC5::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM line_buffered_input = - (CVC5::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM)input; + cvc5::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM line_buffered_input = + (cvc5::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM)input; uint8_t* result = line_buffered_input->line_buffer->getPtrWithOffset( input->line, input->charPositionInLine, la - 1); return (result != NULL) ? *result : ANTLR3_CHARSTREAM_EOF; @@ -255,8 +255,8 @@ static void bufferedInputRewind(pANTLR3_INT_STREAM is, ANTLR3_MARKER mark) { static void bufferedInputConsume(pANTLR3_INT_STREAM is) { pANTLR3_INPUT_STREAM input = ((pANTLR3_INPUT_STREAM)(is->super)); - CVC5::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM line_buffered_input = - (CVC5::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM)input; + cvc5::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM line_buffered_input = + (cvc5::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM)input; uint8_t* current = line_buffered_input->line_buffer->getPtr( input->line, input->charPositionInLine); @@ -285,7 +285,7 @@ static void bufferedInputSeek(pANTLR3_INT_STREAM is, ANTLR3_MARKER seekPoint) { pANTLR3_INPUT_STREAM input = ((pANTLR3_INPUT_STREAM)(is->super)); // Check that we are not seeking backwards. - Assert(!((CVC5::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM)input) + Assert(!((cvc5::parser::pANTLR3_LINE_BUFFERED_INPUT_STREAM)input) ->line_buffer->isPtrBefore( (uint8_t*)seekPoint, input->line, input->charPositionInLine)); @@ -412,4 +412,4 @@ static pANTLR3_INPUT_STREAM antlr3CreateLineBufferedStream( } } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/antlr_line_buffered_input.h b/src/parser/antlr_line_buffered_input.h index 0699c16d0..d687550a4 100644 --- a/src/parser/antlr_line_buffered_input.h +++ b/src/parser/antlr_line_buffered_input.h @@ -30,7 +30,7 @@ #include "parser/line_buffer.h" -namespace CVC5 { +namespace cvc5 { namespace parser { typedef struct ANTLR3_LINE_BUFFERED_INPUT_STREAM { @@ -45,6 +45,6 @@ pANTLR3_INPUT_STREAM antlr3LineBufferedStreamNew(std::istream& in, LineBuffer* line_buffer); } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__ANTLR_LINE_BUFFERED_INPUT_H */ diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index d1b0ea20b..af4ee4d41 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -57,7 +57,7 @@ #include "base/check.h" -namespace CVC5 { +namespace cvc5 { namespace parser { #ifdef ANTLR3_WINDOWS @@ -526,4 +526,4 @@ getSourceName (pANTLR3_INT_STREAM is) } } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/bounded_token_buffer.h b/src/parser/bounded_token_buffer.h index c6599b5af..79bfe0d40 100644 --- a/src/parser/bounded_token_buffer.h +++ b/src/parser/bounded_token_buffer.h @@ -30,7 +30,7 @@ #include <antlr3defs.h> -namespace CVC5 { +namespace cvc5 { namespace parser { #ifdef __cplusplus @@ -59,6 +59,6 @@ BoundedTokenBufferFree(pBOUNDED_TOKEN_BUFFER buffer); #endif } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__BOUNDED_TOKEN_BUFFER_H */ diff --git a/src/parser/bounded_token_factory.cpp b/src/parser/bounded_token_factory.cpp index f7f8a245f..aceff0de4 100644 --- a/src/parser/bounded_token_factory.cpp +++ b/src/parser/bounded_token_factory.cpp @@ -19,7 +19,7 @@ #include <antlr3interfaces.h> #include "parser/bounded_token_factory.h" -namespace CVC5 { +namespace cvc5 { namespace parser { static pANTLR3_COMMON_TOKEN @@ -141,4 +141,4 @@ setInputStream (pANTLR3_TOKEN_FACTORY factory, pANTLR3_INPUT_STREAM input) } } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/bounded_token_factory.h b/src/parser/bounded_token_factory.h index 0f29bbb99..3aa347d52 100644 --- a/src/parser/bounded_token_factory.h +++ b/src/parser/bounded_token_factory.h @@ -22,7 +22,7 @@ #ifndef CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H #define CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H -namespace CVC5 { +namespace cvc5 { namespace parser { #ifdef __cplusplus @@ -46,6 +46,6 @@ BoundedTokenFactoryNew(pANTLR3_INPUT_STREAM input,ANTLR3_UINT32 size); #endif } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__BOUNDED_TOKEN_FACTORY_H */ diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 2ed1a924c..0b27b45fa 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -430,8 +430,8 @@ unsigned findPivot(const std::vector<unsigned>& operators, return pivot; }/* findPivot() */ -CVC5::api::Term createPrecedenceTree(Parser* parser, api::Solver* solver, - const std::vector<CVC5::api::Term>& expressions, +cvc5::api::Term createPrecedenceTree(Parser* parser, api::Solver* solver, + const std::vector<cvc5::api::Term>& expressions, const std::vector<unsigned>& operators, unsigned startIndex, unsigned stopIndex) { Assert(expressions.size() == operators.size() + 1); @@ -447,9 +447,9 @@ CVC5::api::Term createPrecedenceTree(Parser* parser, api::Solver* solver, //Debug("prec") << "pivot[" << startIndex << "," << stopIndex - 1 << "] at " << pivot << std::endl; bool negate; api::Kind k = getOperatorKind(operators[pivot], negate); - CVC5::api::Term lhs = createPrecedenceTree( + cvc5::api::Term lhs = createPrecedenceTree( parser, solver, expressions, operators, startIndex, pivot); - CVC5::api::Term rhs = createPrecedenceTree( + cvc5::api::Term rhs = createPrecedenceTree( parser, solver, expressions, operators, pivot + 1, stopIndex); if (lhs.getSort().isSet()) @@ -477,7 +477,7 @@ CVC5::api::Term createPrecedenceTree(Parser* parser, api::Solver* solver, }/* createPrecedenceTree() recursive variant */ api::Term createPrecedenceTree(Parser* parser, api::Solver* s, - const std::vector<CVC5::api::Term>& expressions, + const std::vector<cvc5::api::Term>& expressions, const std::vector<unsigned>& operators) { if(Debug.isOn("prec") && operators.size() > 1) { for(unsigned i = 0; i < expressions.size(); ++i) { @@ -552,7 +552,7 @@ api::Term addNots(api::Solver* s, size_t n, api::Term e) { #include "smt/command.h" #include "util/rational.h" -namespace CVC5 { +namespace cvc5 { class Expr; }/* CVC4 namespace */ @@ -582,8 +582,8 @@ namespace CVC5 { }); \ }) -using namespace CVC5; -using namespace CVC5::parser; +using namespace cvc5; +using namespace cvc5::parser; /* These need to be macros so they can refer to the PARSER macro, which will be defined * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ @@ -611,7 +611,7 @@ using namespace CVC5::parser; * Parses an expression. * @return the parsed expression */ -parseExpr returns [CVC5::api::Term expr = CVC5::api::Term()] +parseExpr returns [cvc5::api::Term expr = cvc5::api::Term()] : formula[expr] | EOF ; @@ -620,9 +620,9 @@ parseExpr returns [CVC5::api::Term expr = CVC5::api::Term()] * Parses a command (the whole benchmark) * @return the command of the benchmark */ -parseCommand returns [CVC5::Command* cmd_return = NULL] +parseCommand returns [cvc5::Command* cmd_return = NULL] @declarations { - std::unique_ptr<CVC5::Command> cmd; + std::unique_ptr<cvc5::Command> cmd; } @after { cmd_return = cmd.release(); @@ -652,7 +652,7 @@ parseCommand returns [CVC5::Command* cmd_return = NULL] * Matches a command of the input. If a declaration, it will return an empty * command. */ -command [std::unique_ptr<CVC5::Command>* cmd] +command [std::unique_ptr<cvc5::Command>* cmd] : ( mainCommand[cmd] SEMICOLON | SEMICOLON | LET_TOK { PARSER_STATE->pushScope(); } @@ -674,18 +674,18 @@ command [std::unique_ptr<CVC5::Command>* cmd] } ; -typeOrVarLetDecl[CVC5::parser::DeclarationCheck check] +typeOrVarLetDecl[cvc5::parser::DeclarationCheck check] options { backtrack = true; } : letDecl | typeLetDecl[check] ; -mainCommand[std::unique_ptr<CVC5::Command>* cmd] +mainCommand[std::unique_ptr<cvc5::Command>* cmd] @init { api::Term f; api::Term sexpr; std::string id; api::Sort t; - std::vector<CVC5::api::DatatypeDecl> dts; + std::vector<cvc5::api::DatatypeDecl> dts; Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl; std::string s; api::Term func; @@ -694,7 +694,7 @@ mainCommand[std::unique_ptr<CVC5::Command>* cmd] std::vector<api::Term> formulas; std::vector<std::vector<api::Term>> formals; std::vector<std::string> ids; - std::vector<CVC5::api::Sort> types; + std::vector<cvc5::api::Sort> types; bool idCommaFlag = true; bool formCommaFlag = true; } @@ -953,7 +953,7 @@ simpleSymbolicExpr[std::string& s] { s = AntlrInput::tokenText($IDENTIFIER); } ; -symbolicExpr[CVC5::api::Term& sexpr] +symbolicExpr[cvc5::api::Term& sexpr] @declarations { std::string s; std::vector<api::Term> children; @@ -961,13 +961,13 @@ symbolicExpr[CVC5::api::Term& sexpr] : simpleSymbolicExpr[s] { sexpr = SOLVER->mkString(PARSER_STATE->processAdHocStringEsc(s)); } | LPAREN (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN - { sexpr = SOLVER->mkTerm(CVC5::api::SEXPR, children); } + { sexpr = SOLVER->mkTerm(cvc5::api::SEXPR, children); } ; /** * Match a top-level declaration. */ -toplevelDeclaration[std::unique_ptr<CVC5::Command>* cmd] +toplevelDeclaration[std::unique_ptr<cvc5::Command>* cmd] @init { std::vector<std::string> ids; api::Sort t; @@ -982,7 +982,7 @@ toplevelDeclaration[std::unique_ptr<CVC5::Command>* cmd] /** * A bound variable declaration. */ -boundVarDecl[std::vector<std::string>& ids, CVC5::api::Sort& t] +boundVarDecl[std::vector<std::string>& ids, cvc5::api::Sort& t] @init { std::unique_ptr<Command> local_cmd; } @@ -1001,8 +1001,8 @@ boundVarDecls : boundVarDecl[ids,t] ( COMMA boundVarDecl[ids,t] )* ; -boundVarDeclsReturn[std::vector<CVC5::api::Term>& terms, - std::vector<CVC5::api::Sort>& types] +boundVarDeclsReturn[std::vector<cvc5::api::Term>& terms, + std::vector<cvc5::api::Sort>& types] @init { std::vector<std::string> ids; api::Sort t; @@ -1012,8 +1012,8 @@ boundVarDeclsReturn[std::vector<CVC5::api::Term>& terms, : boundVarDeclReturn[terms,types] ( COMMA boundVarDeclReturn[terms,types] )* ; -boundVarDeclReturn[std::vector<CVC5::api::Term>& terms, - std::vector<CVC5::api::Sort>& types] +boundVarDeclReturn[std::vector<cvc5::api::Term>& terms, + std::vector<cvc5::api::Sort>& types] @init { std::vector<std::string> ids; api::Sort t; @@ -1035,7 +1035,7 @@ boundVarDeclReturn[std::vector<CVC5::api::Term>& terms, * because type declarations are always top-level, except for * type-lets, which don't use this rule. */ -declareTypes[std::unique_ptr<CVC5::Command>* cmd, +declareTypes[std::unique_ptr<cvc5::Command>* cmd, const std::vector<std::string>& idList] @init { api::Sort t; @@ -1077,7 +1077,7 @@ declareTypes[std::unique_ptr<CVC5::Command>* cmd, * permitted and "cmd" is output. If topLevel is false, bound vars * are created */ -declareVariables[std::unique_ptr<CVC5::Command>* cmd, CVC5::api::Sort& t, +declareVariables[std::unique_ptr<cvc5::Command>* cmd, cvc5::api::Sort& t, const std::vector<std::string>& idList, bool topLevel] @init { api::Term f; @@ -1167,8 +1167,8 @@ declareVariables[std::unique_ptr<CVC5::Command>* cmd, CVC5::api::Sort& t, * @param check what kinds of check to perform on the symbols */ identifierList[std::vector<std::string>& idList, - CVC5::parser::DeclarationCheck check, - CVC5::parser::SymbolType type] + cvc5::parser::DeclarationCheck check, + cvc5::parser::SymbolType type] @init { std::string id; idList.clear(); @@ -1181,8 +1181,8 @@ identifierList[std::vector<std::string>& idList, * Matches an identifier and returns a string. */ identifier[std::string& id, - CVC5::parser::DeclarationCheck check, - CVC5::parser::SymbolType type] + cvc5::parser::DeclarationCheck check, + cvc5::parser::SymbolType type] : IDENTIFIER { id = AntlrInput::tokenText($IDENTIFIER); PARSER_STATE->checkDeclaration(id, check, type); } @@ -1200,8 +1200,8 @@ identifier[std::string& id, * way; then you should trace through Parser::bindMutualDatatypeType() * to figure out just what you're in for. */ -type[CVC5::api::Sort& t, - CVC5::parser::DeclarationCheck check] +type[cvc5::api::Sort& t, + cvc5::parser::DeclarationCheck check] @init { api::Sort t2; bool lhs; @@ -1244,8 +1244,8 @@ type[CVC5::api::Sort& t, // there). The "type" rule above uses restictedTypePossiblyFunctionLHS // directly in order to implement that; this rule allows a type list to // parse but then issues an error. -restrictedType[CVC5::api::Sort& t, - CVC5::parser::DeclarationCheck check] +restrictedType[cvc5::api::Sort& t, + cvc5::parser::DeclarationCheck check] @init { bool lhs; } @@ -1257,8 +1257,8 @@ restrictedType[CVC5::api::Sort& t, * lhs is set to "true" on output if we have a list of types, so an * ARROW must follow. An ARROW can always follow; lhs means it MUST. */ -restrictedTypePossiblyFunctionLHS[CVC5::api::Sort& t, - CVC5::parser::DeclarationCheck check, +restrictedTypePossiblyFunctionLHS[cvc5::api::Sort& t, + cvc5::parser::DeclarationCheck check, bool& lhs] @init { api::Sort t2; @@ -1369,8 +1369,8 @@ restrictedTypePossiblyFunctionLHS[CVC5::api::Sort& t, } ; -parameterization[CVC5::parser::DeclarationCheck check, - std::vector<CVC5::api::Sort>& params] +parameterization[cvc5::parser::DeclarationCheck check, + std::vector<cvc5::api::Sort>& params] @init { api::Sort t; } @@ -1383,7 +1383,7 @@ bound | integer ; -typeLetDecl[CVC5::parser::DeclarationCheck check] +typeLetDecl[cvc5::parser::DeclarationCheck check] @init { api::Sort t; std::string id; @@ -1399,11 +1399,11 @@ typeLetDecl[CVC5::parser::DeclarationCheck check] * * @return the expression representing the formula/term */ -formula[CVC5::api::Term& f] +formula[cvc5::api::Term& f] @init { Debug("parser-extra") << "formula: " << AntlrInput::tokenText(LT(1)) << std::endl; api::Term f2; - std::vector<CVC5::api::Term> expressions; + std::vector<cvc5::api::Term> expressions; std::vector<unsigned> operators; unsigned op; } @@ -1421,7 +1421,7 @@ formula[CVC5::api::Term& f] ) ; -morecomparisons[std::vector<CVC5::api::Term>& expressions, +morecomparisons[std::vector<cvc5::api::Term>& expressions, std::vector<unsigned>& operators] returns [size_t i = 0] @init { unsigned op; @@ -1445,7 +1445,7 @@ nots returns [size_t n = 0] : ( NOT_TOK { ++$n; } )* ; -prefixFormula[CVC5::api::Term& f] +prefixFormula[cvc5::api::Term& f] @init { std::vector<std::string> ids; std::vector<api::Term> terms; @@ -1499,7 +1499,7 @@ prefixFormula[CVC5::api::Term& f] } ; -instantiationPatterns[ CVC5::api::Term& expr ] +instantiationPatterns[ cvc5::api::Term& expr ] @init { std::vector<api::Term> args; api::Term f; @@ -1545,9 +1545,9 @@ booleanBinop[unsigned& op] | AND_TOK ; -comparison[CVC5::api::Term& f] +comparison[cvc5::api::Term& f] @init { - std::vector<CVC5::api::Term> expressions; + std::vector<cvc5::api::Term> expressions; std::vector<unsigned> operators; unsigned op; } @@ -1585,9 +1585,9 @@ arithmeticBinop[unsigned& op] ; /** Parses an array/tuple/record assignment term. */ -term[CVC5::api::Term& f] +term[cvc5::api::Term& f] @init { - std::vector<CVC5::api::Term> expressions; + std::vector<cvc5::api::Term> expressions; std::vector<unsigned> operators; unsigned op; api::Sort t; @@ -1607,24 +1607,24 @@ term[CVC5::api::Term& f] * Parses just part of the array assignment (and constructs * the store terms). */ -arrayStore[CVC5::api::Term& f] +arrayStore[cvc5::api::Term& f] @init { api::Term f2, k; } : LBRACKET formula[k] RBRACKET - { f2 = MK_TERM(CVC5::api::SELECT, f, k); } + { f2 = MK_TERM(cvc5::api::SELECT, f, k); } ( ( arrayStore[f2] | DOT ( tupleStore[f2] | recordStore[f2] ) ) | ASSIGN_TOK term[f2] ) - { f = MK_TERM(CVC5::api::STORE, f, k, f2); } + { f = MK_TERM(cvc5::api::STORE, f, k, f2); } ; /** * Parses just part of the tuple assignment (and constructs * the store terms). */ -tupleStore[CVC5::api::Term& f] +tupleStore[cvc5::api::Term& f] @init { api::Term f2; } @@ -1654,7 +1654,7 @@ tupleStore[CVC5::api::Term& f] * Parses just part of the record assignment (and constructs * the store terms). */ -recordStore[CVC5::api::Term& f] +recordStore[cvc5::api::Term& f] @init { std::string id; api::Term f2; @@ -1680,7 +1680,7 @@ recordStore[CVC5::api::Term& f] ; /** Parses a unary minus term. */ -uminusTerm[CVC5::api::Term& f] +uminusTerm[cvc5::api::Term& f] @init { unsigned minusCount = 0; } @@ -1690,14 +1690,14 @@ uminusTerm[CVC5::api::Term& f] while (minusCount > 0) { --minusCount; - f = MK_TERM(CVC5::api::UMINUS, f); + f = MK_TERM(cvc5::api::UMINUS, f); } }; /** Parses bitvectors. Starts with binary operators @, &, and |. */ -bvBinaryOpTerm[CVC5::api::Term& f] +bvBinaryOpTerm[cvc5::api::Term& f] @init { - std::vector<CVC5::api::Term> expressions; + std::vector<cvc5::api::Term> expressions; std::vector<unsigned> operators; unsigned op; } @@ -1714,12 +1714,12 @@ bvBinop[unsigned& op] | BVAND_TOK ; -bvNegTerm[CVC5::api::Term& f] +bvNegTerm[cvc5::api::Term& f] /* BV neg */ : BVNEG_TOK bvNegTerm[f] { - f = f.getSort().isSet() ? MK_TERM(CVC5::api::COMPLEMENT, f) - : MK_TERM(CVC5::api::BITVECTOR_NOT, f); + f = f.getSort().isSet() ? MK_TERM(cvc5::api::COMPLEMENT, f) + : MK_TERM(cvc5::api::BITVECTOR_NOT, f); } | relationBinopTerm[f] ; @@ -1733,9 +1733,9 @@ relationBinop[unsigned& op] | JOIN_IMAGE_TOK ; -relationBinopTerm[CVC5::api::Term& f] +relationBinopTerm[cvc5::api::Term& f] @init { - std::vector<CVC5::api::Term> expressions; + std::vector<cvc5::api::Term> expressions; std::vector<unsigned> operators; unsigned op; } @@ -1753,7 +1753,7 @@ relationBinopTerm[CVC5::api::Term& f] * brackets ], so we left-factor as much out as possible to make ANTLR * happy. */ -postfixTerm[CVC5::api::Term& f] +postfixTerm[cvc5::api::Term& f] @init { api::Term f2; bool extract = false, left = false; @@ -1772,7 +1772,7 @@ postfixTerm[CVC5::api::Term& f] f = SOLVER->mkTerm(SOLVER->mkOp(api::BITVECTOR_EXTRACT,k1,k2), f); } else { /* array select */ - f = MK_TERM(CVC5::api::SELECT, f, f2); + f = MK_TERM(cvc5::api::SELECT, f, f2); } } /* left- or right-shift */ @@ -1834,19 +1834,19 @@ postfixTerm[CVC5::api::Term& f] ) )* | FLOOR_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::TO_INTEGER, f); } + { f = MK_TERM(cvc5::api::TO_INTEGER, f); } | IS_INTEGER_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::IS_INTEGER, f); } + { f = MK_TERM(cvc5::api::IS_INTEGER, f); } | ABS_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::ABS, f); } + { f = MK_TERM(cvc5::api::ABS, f); } | DIVISIBLE_TOK LPAREN formula[f] COMMA n=numeral RPAREN - { f = MK_TERM(SOLVER->mkOp(CVC5::api::DIVISIBLE, n), f); } + { f = MK_TERM(SOLVER->mkOp(cvc5::api::DIVISIBLE, n), f); } | DISTINCT_TOK LPAREN formula[f] { args.push_back(f); } ( COMMA formula[f] { args.push_back(f); } )* RPAREN { f = (args.size() == 1) ? SOLVER->mkTrue() - : MK_TERM(CVC5::api::DISTINCT, args); + : MK_TERM(cvc5::api::DISTINCT, args); } ) ( typeAscription[f, t] @@ -1856,12 +1856,12 @@ postfixTerm[CVC5::api::Term& f] )? ; -relationTerm[CVC5::api::Term& f] +relationTerm[cvc5::api::Term& f] /* relation terms */ : TRANSPOSE_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::TRANSPOSE, f); } + { f = MK_TERM(cvc5::api::TRANSPOSE, f); } | TRANSCLOSURE_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::TCLOSURE, f); } + { f = MK_TERM(cvc5::api::TCLOSURE, f); } | TUPLE_TOK LPAREN formula[f] RPAREN { std::vector<api::Sort> types; std::vector<api::Term> args; @@ -1873,30 +1873,30 @@ relationTerm[CVC5::api::Term& f] f = MK_TERM(api::APPLY_CONSTRUCTOR, args); } | IDEN_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::IDEN, f); } + { f = MK_TERM(cvc5::api::IDEN, f); } | bvTerm[f] ; -bvTerm[CVC5::api::Term& f] +bvTerm[cvc5::api::Term& f] @init { api::Term f2; std::vector<api::Term> args; } /* BV xor */ : BVXOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_XOR, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_XOR, f, f2); } | BVNAND_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_NAND, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_NAND, f, f2); } | BVNOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_NOR, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_NOR, f, f2); } | BVCOMP_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_COMP, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_COMP, f, f2); } | BVXNOR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_XNOR, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_XNOR, f, f2); } /* BV unary minus */ | BVUMINUS_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_NEG, f); } + { f = MK_TERM(cvc5::api::BITVECTOR_NEG, f); } /* BV addition */ | BVPLUS_TOK LPAREN k=numeral COMMA formula[f] { args.push_back(f); } ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN @@ -1907,7 +1907,7 @@ bvTerm[CVC5::api::Term& f] for (unsigned i = 0; i < args.size(); ++ i) { ENSURE_BV_SIZE(k, args[i]); } - f = MK_TERM(CVC5::api::BITVECTOR_PLUS, args); + f = MK_TERM(cvc5::api::BITVECTOR_PLUS, args); } /* BV subtraction */ | BVSUB_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN @@ -1917,7 +1917,7 @@ bvTerm[CVC5::api::Term& f] } ENSURE_BV_SIZE(k, f); ENSURE_BV_SIZE(k, f2); - f = MK_TERM(CVC5::api::BITVECTOR_SUB, f, f2); + f = MK_TERM(cvc5::api::BITVECTOR_SUB, f, f2); } /* BV multiplication */ | BVMULT_TOK LPAREN k=numeral COMMA formula[f] COMMA formula[f2] RPAREN @@ -1927,32 +1927,32 @@ bvTerm[CVC5::api::Term& f] } ENSURE_BV_SIZE(k, f); ENSURE_BV_SIZE(k, f2); - f = MK_TERM(CVC5::api::BITVECTOR_MULT, f, f2); + f = MK_TERM(cvc5::api::BITVECTOR_MULT, f, f2); } /* BV unsigned division */ | BVUDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_UDIV, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_UDIV, f, f2); } /* BV signed division */ | BVSDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_SDIV, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_SDIV, f, f2); } /* BV unsigned remainder */ | BVUREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_UREM, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_UREM, f, f2); } /* BV signed remainder */ | BVSREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_SREM, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_SREM, f, f2); } /* BV signed modulo */ | BVSMOD_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_SMOD, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_SMOD, f, f2); } /* BV left shift */ | BVSHL_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_SHL, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_SHL, f, f2); } /* BV arithmetic right shift */ | BVASHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_ASHR, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_ASHR, f, f2); } /* BV logical left shift */ | BVLSHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_LSHR, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_LSHR, f, f2); } /* BV sign extension */ | SX_TOK LPAREN formula[f] COMMA k=numeral RPAREN { unsigned n = f.getSort().getBVSize(); @@ -1983,25 +1983,25 @@ bvTerm[CVC5::api::Term& f] /* BV comparisons */ | BVLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_ULT, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_ULT, f, f2); } | BVLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_ULE, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_ULE, f, f2); } | BVGT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_UGT, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_UGT, f, f2); } | BVGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_UGE, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_UGE, f, f2); } | BVSLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_SLT, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_SLT, f, f2); } | BVSLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_SLE, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_SLE, f, f2); } | BVSGT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_SGT, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_SGT, f, f2); } | BVSGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::BITVECTOR_SGE, f, f2); } + { f = MK_TERM(cvc5::api::BITVECTOR_SGE, f, f2); } | stringTerm[f] ; -stringTerm[CVC5::api::Term& f] +stringTerm[cvc5::api::Term& f] @init { api::Term f2; api::Term f3; @@ -2011,67 +2011,67 @@ stringTerm[CVC5::api::Term& f] /* String prefix operators */ : STRING_CONCAT_TOK LPAREN formula[f] { args.push_back(f); } ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN - { f = MK_TERM(CVC5::api::STRING_CONCAT, args); } + { f = MK_TERM(cvc5::api::STRING_CONCAT, args); } | STRING_LENGTH_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::STRING_LENGTH, f); } + { f = MK_TERM(cvc5::api::STRING_LENGTH, f); } | STRING_CONTAINS_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::STRING_CONTAINS, f, f2); } + { f = MK_TERM(cvc5::api::STRING_CONTAINS, f, f2); } | STRING_SUBSTR_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN - { f = MK_TERM(CVC5::api::STRING_SUBSTR, f, f2, f3); } + { f = MK_TERM(cvc5::api::STRING_SUBSTR, f, f2, f3); } | STRING_CHARAT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::STRING_CHARAT, f, f2); } + { f = MK_TERM(cvc5::api::STRING_CHARAT, f, f2); } | STRING_INDEXOF_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN - { f = MK_TERM(CVC5::api::STRING_INDEXOF, f, f2, f3); } + { f = MK_TERM(cvc5::api::STRING_INDEXOF, f, f2, f3); } | STRING_REPLACE_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN - { f = MK_TERM(CVC5::api::STRING_REPLACE, f, f2, f3); } + { f = MK_TERM(cvc5::api::STRING_REPLACE, f, f2, f3); } | STRING_REPLACE_ALL_TOK LPAREN formula[f] COMMA formula[f2] COMMA formula[f3] RPAREN - { f = MK_TERM(CVC5::api::STRING_REPLACE_ALL, f, f2, f3); } + { f = MK_TERM(cvc5::api::STRING_REPLACE_ALL, f, f2, f3); } | STRING_PREFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::STRING_PREFIX, f, f2); } + { f = MK_TERM(cvc5::api::STRING_PREFIX, f, f2); } | STRING_SUFFIXOF_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::STRING_SUFFIX, f, f2); } + { f = MK_TERM(cvc5::api::STRING_SUFFIX, f, f2); } | STRING_STOI_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::STRING_TO_INT, f); } + { f = MK_TERM(cvc5::api::STRING_TO_INT, f); } | STRING_ITOS_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::STRING_FROM_INT, f); } + { f = MK_TERM(cvc5::api::STRING_FROM_INT, f); } | STRING_TO_REGEXP_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::STRING_TO_REGEXP, f); } + { f = MK_TERM(cvc5::api::STRING_TO_REGEXP, f); } | STRING_TOLOWER_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::STRING_TOLOWER, f); } + { f = MK_TERM(cvc5::api::STRING_TOLOWER, f); } | STRING_TOUPPER_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::STRING_TOUPPER, f); } + { f = MK_TERM(cvc5::api::STRING_TOUPPER, f); } | STRING_REV_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::STRING_REV, f); } + { f = MK_TERM(cvc5::api::STRING_REV, f); } | REGEXP_CONCAT_TOK LPAREN formula[f] { args.push_back(f); } ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN - { f = MK_TERM(CVC5::api::REGEXP_CONCAT, args); } + { f = MK_TERM(cvc5::api::REGEXP_CONCAT, args); } | REGEXP_UNION_TOK LPAREN formula[f] { args.push_back(f); } ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN - { f = MK_TERM(CVC5::api::REGEXP_UNION, args); } + { f = MK_TERM(cvc5::api::REGEXP_UNION, args); } | REGEXP_INTER_TOK LPAREN formula[f] { args.push_back(f); } ( COMMA formula[f2] { args.push_back(f2); } )+ RPAREN - { f = MK_TERM(CVC5::api::REGEXP_INTER, args); } + { f = MK_TERM(cvc5::api::REGEXP_INTER, args); } | REGEXP_STAR_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::REGEXP_STAR, f); } + { f = MK_TERM(cvc5::api::REGEXP_STAR, f); } | REGEXP_PLUS_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::REGEXP_PLUS, f); } + { f = MK_TERM(cvc5::api::REGEXP_PLUS, f); } | REGEXP_OPT_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::REGEXP_OPT, f); } + { f = MK_TERM(cvc5::api::REGEXP_OPT, f); } | REGEXP_RANGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN - { f = MK_TERM(CVC5::api::REGEXP_RANGE, f, f2); } + { f = MK_TERM(cvc5::api::REGEXP_RANGE, f, f2); } | REGEXP_LOOP_TOK LPAREN formula[f] COMMA lo=numeral COMMA hi=numeral RPAREN { - api::Op lop = SOLVER->mkOp(CVC5::api::REGEXP_LOOP, lo, hi); + api::Op lop = SOLVER->mkOp(cvc5::api::REGEXP_LOOP, lo, hi); f = MK_TERM(lop, f); } | REGEXP_COMPLEMENT_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::REGEXP_COMPLEMENT, f); } + { f = MK_TERM(cvc5::api::REGEXP_COMPLEMENT, f); } | SEQ_UNIT_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::SEQ_UNIT, f); } + { f = MK_TERM(cvc5::api::SEQ_UNIT, f); } | REGEXP_EMPTY_TOK - { f = MK_TERM(CVC5::api::REGEXP_EMPTY, std::vector<api::Term>()); } + { f = MK_TERM(cvc5::api::REGEXP_EMPTY, std::vector<api::Term>()); } | REGEXP_SIGMA_TOK - { f = MK_TERM(CVC5::api::REGEXP_SIGMA, std::vector<api::Term>()); } + { f = MK_TERM(cvc5::api::REGEXP_SIGMA, std::vector<api::Term>()); } /* string literal */ | str[s] @@ -2080,20 +2080,20 @@ stringTerm[CVC5::api::Term& f] | setsTerm[f] ; -setsTerm[CVC5::api::Term& f] +setsTerm[cvc5::api::Term& f] @init { } /* Sets prefix operators */ : SETS_CARD_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::CARD, f); } + { f = MK_TERM(cvc5::api::CARD, f); } | SETS_CHOOSE_TOK LPAREN formula[f] RPAREN - { f = MK_TERM(CVC5::api::CHOOSE, f); } + { f = MK_TERM(cvc5::api::CHOOSE, f); } | simpleTerm[f] ; /** Parses a simple term. */ -simpleTerm[CVC5::api::Term& f] +simpleTerm[cvc5::api::Term& f] @init { std::string name; std::vector<api::Term> args; @@ -2234,7 +2234,7 @@ simpleTerm[CVC5::api::Term& f] api::Sort dtype = f.getSort(); if(dtype.isConstructor() && dtype.getConstructorArity() == 0) { // don't require parentheses, immediately turn it into an apply - f = MK_TERM(CVC5::api::APPLY_CONSTRUCTOR, f); + f = MK_TERM(cvc5::api::APPLY_CONSTRUCTOR, f); } } ; @@ -2243,7 +2243,7 @@ simpleTerm[CVC5::api::Term& f] * Matches a type ascription. * The f arg is the term to check (it is an input-only argument). */ -typeAscription[const CVC5::api::Term& f, CVC5::api::Sort& t] +typeAscription[const cvc5::api::Term& f, cvc5::api::Sort& t] @init { } : COLON COLON type[t,CHECK_DECLARED] @@ -2252,14 +2252,14 @@ typeAscription[const CVC5::api::Term& f, CVC5::api::Sort& t] /** * Matches an entry in a record literal. */ -recordEntry[std::string& name, CVC5::api::Term& ex] +recordEntry[std::string& name, cvc5::api::Term& ex] : identifier[name,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK formula[ex] ; /** * Parses an ITE term. */ -iteTerm[CVC5::api::Term& f] +iteTerm[cvc5::api::Term& f] @init { std::vector<api::Term> args; Debug("parser-extra") << "ite: " << AntlrInput::tokenText(LT(1)) << std::endl; @@ -2268,13 +2268,13 @@ iteTerm[CVC5::api::Term& f] THEN_TOK formula[f] { args.push_back(f); } iteElseTerm[f] { args.push_back(f); } ENDIF_TOK - { f = MK_TERM(CVC5::api::ITE, args); } + { f = MK_TERM(cvc5::api::ITE, args); } ; /** * Parses the else part of the ITE, i.e. ELSE f, or ELSIF b THEN f1 ... */ -iteElseTerm[CVC5::api::Term& f] +iteElseTerm[cvc5::api::Term& f] @init { std::vector<api::Term> args; Debug("parser-extra") << "else: " << AntlrInput::tokenText(LT(1)) << std::endl; @@ -2283,13 +2283,13 @@ iteElseTerm[CVC5::api::Term& f] | ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); } THEN_TOK iteThen = formula[f] { args.push_back(f); } iteElse = iteElseTerm[f] { args.push_back(f); } - { f = MK_TERM(CVC5::api::ITE, args); } + { f = MK_TERM(cvc5::api::ITE, args); } ; /** * Parses a datatype definition */ -datatypeDef[std::vector<CVC5::api::DatatypeDecl>& datatypes] +datatypeDef[std::vector<cvc5::api::DatatypeDecl>& datatypes] @init { std::string id, id2; api::Sort t; @@ -2324,14 +2324,14 @@ datatypeDef[std::vector<CVC5::api::DatatypeDecl>& datatypes] /** * Parses a constructor defintion for type */ -constructorDef[CVC5::api::DatatypeDecl& type] +constructorDef[cvc5::api::DatatypeDecl& type] @init { std::string id; - std::unique_ptr<CVC5::api::DatatypeConstructorDecl> ctor; + std::unique_ptr<cvc5::api::DatatypeConstructorDecl> ctor; } : identifier[id,CHECK_UNDECLARED,SYM_SORT] { - ctor.reset(new CVC5::api::DatatypeConstructorDecl( + ctor.reset(new cvc5::api::DatatypeConstructorDecl( SOLVER->mkDatatypeConstructorDecl(id))); } ( LPAREN @@ -2345,7 +2345,7 @@ constructorDef[CVC5::api::DatatypeDecl& type] } ; -selector[std::unique_ptr<CVC5::api::DatatypeConstructorDecl>* ctor] +selector[std::unique_ptr<cvc5::api::DatatypeConstructorDecl>* ctor] @init { std::string id; api::Sort t, t2; @@ -2377,7 +2377,7 @@ numeral returns [unsigned k = 0] /** * Similar to numeral but for arbitrary-precision, signed integer. */ -integer returns [CVC5::Rational k = 0] +integer returns [cvc5::Rational k = 0] : INTEGER_LITERAL { $k = AntlrInput::tokenToInteger($INTEGER_LITERAL); } | MINUS_TOK INTEGER_LITERAL diff --git a/src/parser/cvc/cvc.cpp b/src/parser/cvc/cvc.cpp index 3cd486981..a115fa276 100644 --- a/src/parser/cvc/cvc.cpp +++ b/src/parser/cvc/cvc.cpp @@ -17,7 +17,7 @@ #include "parser/cvc/cvc.h" #include "smt/command.h" -namespace CVC5 { +namespace cvc5 { namespace parser { void Cvc::forceLogic(const std::string& logic) @@ -35,4 +35,4 @@ bool Cvc::getTesterName(api::Term cons, std::string& name) } } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/cvc/cvc.h b/src/parser/cvc/cvc.h index c36e36979..acfcc1d17 100644 --- a/src/parser/cvc/cvc.h +++ b/src/parser/cvc/cvc.h @@ -22,7 +22,7 @@ #include "api/cvc4cpp.h" #include "parser/parser.h" -namespace CVC5 { +namespace cvc5 { namespace parser { @@ -48,6 +48,6 @@ class Cvc : public Parser }; } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__CVC_H */ diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index a4a9c27f2..f746c5f05 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -24,7 +24,7 @@ #include "parser/cvc/CvcParser.h" #include "parser/parser_exception.h" -namespace CVC5 { +namespace cvc5 { namespace parser { /* Use lookahead=3 */ @@ -73,4 +73,4 @@ pANTLR3_LEXER CvcInput::getLexer() { */ } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index c9862916a..82b2d652c 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -23,10 +23,10 @@ #include "parser/cvc/CvcLexer.h" #include "parser/cvc/CvcParser.h" -// extern void CvcParserSetAntlrParser(CVC5::parser::AntlrParser* +// extern void CvcParserSetAntlrParser(cvc5::parser::AntlrParser* // newAntlrParser); -namespace CVC5 { +namespace cvc5 { class Command; class Expr; @@ -73,6 +73,6 @@ class CvcInput : public AntlrInput { }; // class CvcInput } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__CVC_INPUT_H */ diff --git a/src/parser/input.cpp b/src/parser/input.cpp index d0c71bd13..8c9519022 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -25,11 +25,11 @@ using namespace std; -using namespace CVC5; -using namespace CVC5::parser; -using namespace CVC5::kind; +using namespace cvc5; +using namespace cvc5::parser; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace parser { InputStreamException::InputStreamException(const std::string& msg) : @@ -80,4 +80,4 @@ Input* Input::newStringInput(InputLanguage lang, } } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/input.h b/src/parser/input.h index 2a401521c..fcaa36932 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -30,7 +30,7 @@ #include "options/language.h" #include "parser/parser_exception.h" -namespace CVC5 { +namespace cvc5 { class Command; @@ -177,6 +177,6 @@ class CVC4_EXPORT Input }; /* class Input */ } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__ANTLR_INPUT_H */ diff --git a/src/parser/line_buffer.cpp b/src/parser/line_buffer.cpp index 1675d8f99..694478d38 100644 --- a/src/parser/line_buffer.cpp +++ b/src/parser/line_buffer.cpp @@ -22,7 +22,7 @@ #include "base/check.h" -namespace CVC5 { +namespace cvc5 { namespace parser { LineBuffer::LineBuffer(std::istream* stream) : d_stream(stream) {} @@ -90,4 +90,4 @@ bool LineBuffer::readToLine(size_t line_size) } } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/line_buffer.h b/src/parser/line_buffer.h index 3625ade87..a8a4e993c 100644 --- a/src/parser/line_buffer.h +++ b/src/parser/line_buffer.h @@ -25,7 +25,7 @@ #include <istream> #include <vector> -namespace CVC5 { +namespace cvc5 { namespace parser { class LineBuffer { @@ -71,6 +71,6 @@ class LineBuffer { }; } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__LINE_BUFFER_H */ diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp index 04a2ef2eb..4259e328f 100644 --- a/src/parser/memory_mapped_input_buffer.cpp +++ b/src/parser/memory_mapped_input_buffer.cpp @@ -30,7 +30,7 @@ #include "base/exception.h" #include "parser/memory_mapped_input_buffer.h" -namespace CVC5 { +namespace cvc5 { namespace parser { extern "C" { @@ -130,4 +130,4 @@ void UnmapFile(pANTLR3_INPUT_STREAM input) { }/* extern "C" */ } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/memory_mapped_input_buffer.h b/src/parser/memory_mapped_input_buffer.h index 31f15d459..96009674e 100644 --- a/src/parser/memory_mapped_input_buffer.h +++ b/src/parser/memory_mapped_input_buffer.h @@ -22,7 +22,7 @@ #include <antlr3input.h> #include <string> -namespace CVC5 { +namespace cvc5 { namespace parser { #ifdef __cplusplus @@ -37,6 +37,6 @@ MemoryMappedInputBufferNew(const std::string& filename); #endif } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H */ diff --git a/src/parser/parse_op.cpp b/src/parser/parse_op.cpp index 377958ecd..0d024da61 100644 --- a/src/parser/parse_op.cpp +++ b/src/parser/parse_op.cpp @@ -14,7 +14,7 @@ #include "parser/parse_op.h" -namespace CVC5 { +namespace cvc5 { std::ostream& operator<<(std::ostream& os, const ParseOp& p) { @@ -44,4 +44,4 @@ std::ostream& operator<<(std::ostream& os, const ParseOp& p) return os << out.str(); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/parse_op.h b/src/parser/parse_op.h index 1c508a92e..1163ab6be 100644 --- a/src/parser/parse_op.h +++ b/src/parser/parse_op.h @@ -21,7 +21,7 @@ #include "api/cvc4cpp.h" -namespace CVC5 { +namespace cvc5 { /** A parsed operator * @@ -79,6 +79,6 @@ struct ParseOp std::ostream& operator<<(std::ostream& os, const ParseOp& p); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__PARSE_OP_H */ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index a4268e74e..6725b5ec7 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -33,9 +33,9 @@ #include "smt/command.h" using namespace std; -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace parser { Parser::Parser(api::Solver* solver, @@ -909,4 +909,4 @@ api::Term Parser::mkStringConstant(const std::string& s) } } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/parser.h b/src/parser/parser.h index 0ae63cdd1..173b98a9c 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -33,7 +33,7 @@ #include "parser/parser_exception.h" #include "util/unsafe_interrupt_exception.h" -namespace CVC5 { +namespace cvc5 { // Forward declarations class Command; @@ -774,6 +774,6 @@ public: }; /* class Parser */ } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__PARSER_STATE_H */ diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index ffd993383..b0b6a03e7 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -29,7 +29,7 @@ #include "smt2/smt2.h" #include "tptp/tptp.h" -namespace CVC5 { +namespace cvc5 { namespace parser { ParserBuilder::ParserBuilder(api::Solver* solver, @@ -218,4 +218,4 @@ ParserBuilder& ParserBuilder::withStringInput(const std::string& input) { } } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 8ec59d4b2..0575dd21d 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -25,7 +25,7 @@ #include "options/language.h" #include "parser/input.h" -namespace CVC5 { +namespace cvc5 { namespace api { class Solver; @@ -189,6 +189,6 @@ class CVC4_EXPORT ParserBuilder }; /* class ParserBuilder */ } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__PARSER_BUILDER_H */ diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index 1863b39cd..7fcbce213 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -26,7 +26,7 @@ #include "base/exception.h" #include "cvc4_export.h" -namespace CVC5 { +namespace cvc5 { namespace parser { class CVC4_EXPORT ParserException : public Exception @@ -100,6 +100,6 @@ class ParserEndOfFileException : public ParserException }; /* class ParserEndOfFileException */ } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__PARSER_EXCEPTION_H */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e55cbf510..6adc6275a 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -66,8 +66,8 @@ options { #include "parser/smt2/smt2.h" #include "parser/antlr_input.h" -using namespace CVC5; -using namespace CVC5::parser; +using namespace cvc5; +using namespace cvc5::parser; #undef PARSER_STATE #define PARSER_STATE ((Smt2*)LEXER->super) @@ -83,7 +83,7 @@ using namespace CVC5::parser; #include "parser/parser.h" #include "smt/command.h" -namespace CVC5 { +namespace cvc5 { namespace api { class Term; @@ -113,8 +113,8 @@ namespace CVC5 { #include "util/integer.h" #include "util/rational.h" -using namespace CVC5; -using namespace CVC5::parser; +using namespace cvc5; +using namespace cvc5::parser; /* These need to be macros so they can refer to the PARSER macro, which * will be defined by ANTLR *after* this section. (If they were functions, @@ -136,9 +136,9 @@ using namespace CVC5::parser; * @return the parsed expression, or the Null Expr if we've reached the * end of the input */ -parseExpr returns [CVC5::api::Term expr = CVC5::api::Term()] +parseExpr returns [cvc5::api::Term expr = cvc5::api::Term()] @declarations { - CVC5::api::Term expr2; + cvc5::api::Term expr2; } : term[expr, expr2] | EOF @@ -148,9 +148,9 @@ parseExpr returns [CVC5::api::Term expr = CVC5::api::Term()] * Parses a command * @return the parsed command, or NULL if we've reached the end of the input */ -parseCommand returns [CVC5::Command* cmd_return = NULL] +parseCommand returns [cvc5::Command* cmd_return = NULL] @declarations { - std::unique_ptr<CVC5::Command> cmd; + std::unique_ptr<cvc5::Command> cmd; std::string name; } @after { @@ -184,7 +184,7 @@ parseCommand returns [CVC5::Command* cmd_return = NULL] * @return the parsed SyGuS command, or NULL if we've reached the end of the * input */ -parseSygus returns [CVC5::Command* cmd_return = NULL] +parseSygus returns [cvc5::Command* cmd_return = NULL] @declarations { std::string name; } @@ -199,16 +199,16 @@ parseSygus returns [CVC5::Command* cmd_return = NULL] * Parse the internal portion of the command, ignoring the surrounding * parentheses. */ -command [std::unique_ptr<CVC5::Command>* cmd] +command [std::unique_ptr<cvc5::Command>* cmd] @declarations { std::string name; std::vector<std::string> names; - CVC5::api::Term expr, expr2; - CVC5::api::Sort t; - std::vector<CVC5::api::Term> terms; + cvc5::api::Term expr, expr2; + cvc5::api::Sort t; + std::vector<cvc5::api::Term> terms; std::vector<api::Sort> sorts; - std::vector<std::pair<std::string, CVC5::api::Sort> > sortedVarNames; - std::vector<CVC5::api::Term> flattenVars; + std::vector<std::pair<std::string, cvc5::api::Sort> > sortedVarNames; + std::vector<cvc5::api::Term> flattenVars; } : /* set the logic */ SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT] @@ -505,16 +505,16 @@ command [std::unique_ptr<CVC5::Command>* cmd] } ; -sygusCommand returns [std::unique_ptr<CVC5::Command> cmd] +sygusCommand returns [std::unique_ptr<cvc5::Command> cmd] @declarations { - CVC5::api::Term expr, expr2, fun; - CVC5::api::Sort t, range; + cvc5::api::Term expr, expr2, fun; + cvc5::api::Sort t, range; std::vector<std::string> names; - std::vector<std::pair<std::string, CVC5::api::Sort> > sortedVarNames; - std::vector<CVC5::api::Term> sygusVars; + std::vector<std::pair<std::string, cvc5::api::Sort> > sortedVarNames; + std::vector<cvc5::api::Term> sygusVars; std::string name; bool isInv; - CVC5::api::Grammar* grammar = nullptr; + cvc5::api::Grammar* grammar = nullptr; } : /* declare-var */ DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -597,18 +597,18 @@ sygusCommand returns [std::unique_ptr<CVC5::Command> cmd] * The argument fun is a unique identifier to avoid naming clashes for the * datatypes constructed by this call. */ -sygusGrammar[CVC5::api::Grammar*& ret, - const std::vector<CVC5::api::Term>& sygusVars, +sygusGrammar[cvc5::api::Grammar*& ret, + const std::vector<cvc5::api::Term>& sygusVars, const std::string& fun] @declarations { // the pre-declaration - std::vector<std::pair<std::string, CVC5::api::Sort>> sortedVarNames; + std::vector<std::pair<std::string, cvc5::api::Sort>> sortedVarNames; // non-terminal symbols of the grammar - std::vector<CVC5::api::Term> ntSyms; - CVC5::api::Sort t; + std::vector<cvc5::api::Term> ntSyms; + cvc5::api::Sort t; std::string name; - CVC5::api::Term e, e2; + cvc5::api::Term e, e2; unsigned dtProcessed = 0; } : @@ -710,7 +710,7 @@ sygusGrammar[CVC5::api::Grammar*& ret, } ; -setInfoInternal[std::unique_ptr<CVC5::Command>* cmd] +setInfoInternal[std::unique_ptr<cvc5::Command>* cmd] @declarations { std::string name; api::Term sexpr; @@ -721,7 +721,7 @@ setInfoInternal[std::unique_ptr<CVC5::Command>* cmd] } ; -setOptionInternal[std::unique_ptr<CVC5::Command>* cmd] +setOptionInternal[std::unique_ptr<cvc5::Command>* cmd] @init { std::string name; api::Term sexpr; @@ -738,26 +738,26 @@ setOptionInternal[std::unique_ptr<CVC5::Command>* cmd] } ; -smt25Command[std::unique_ptr<CVC5::Command>* cmd] +smt25Command[std::unique_ptr<cvc5::Command>* cmd] @declarations { std::string name; std::string fname; - CVC5::api::Term expr, expr2; - std::vector<std::pair<std::string, CVC5::api::Sort> > sortedVarNames; + cvc5::api::Term expr, expr2; + std::vector<std::pair<std::string, cvc5::api::Sort> > sortedVarNames; std::string s; - CVC5::api::Sort t; - CVC5::api::Term func; - std::vector<CVC5::api::Term> bvs; - std::vector<std::vector<std::pair<std::string, CVC5::api::Sort>>> + cvc5::api::Sort t; + cvc5::api::Term func; + std::vector<cvc5::api::Term> bvs; + std::vector<std::vector<std::pair<std::string, cvc5::api::Sort>>> sortedVarNamesList; - std::vector<std::vector<CVC5::api::Term>> flattenVarsList; - std::vector<std::vector<CVC5::api::Term>> formals; - std::vector<CVC5::api::Term> funcs; - std::vector<CVC5::api::Term> func_defs; - CVC5::api::Term aexpr; - std::unique_ptr<CVC5::CommandSequence> seq; + std::vector<std::vector<cvc5::api::Term>> flattenVarsList; + std::vector<std::vector<cvc5::api::Term>> formals; + std::vector<cvc5::api::Term> funcs; + std::vector<cvc5::api::Term> func_defs; + cvc5::api::Term aexpr; + std::unique_ptr<cvc5::CommandSequence> seq; std::vector<api::Sort> sorts; - std::vector<CVC5::api::Term> flattenVars; + std::vector<cvc5::api::Term> flattenVars; } /* declare-const */ : DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -880,17 +880,17 @@ smt25Command[std::unique_ptr<CVC5::Command>* cmd] } ; -extendedCommand[std::unique_ptr<CVC5::Command>* cmd] +extendedCommand[std::unique_ptr<cvc5::Command>* cmd] @declarations { std::vector<api::DatatypeDecl> dts; - CVC5::api::Term e, e2; - CVC5::api::Sort t, s; + cvc5::api::Term e, e2; + cvc5::api::Sort t, s; std::string name; std::vector<std::string> names; - std::vector<CVC5::api::Term> terms; + std::vector<cvc5::api::Term> terms; std::vector<api::Sort> sorts; - std::vector<std::pair<std::string, CVC5::api::Sort> > sortedVarNames; - std::unique_ptr<CVC5::CommandSequence> seq; + std::vector<std::pair<std::string, cvc5::api::Sort> > sortedVarNames; + std::unique_ptr<cvc5::CommandSequence> seq; api::Grammar* g = nullptr; } /* Extended SMT-LIB set of commands syntax, not permitted in @@ -904,7 +904,7 @@ extendedCommand[std::unique_ptr<CVC5::Command>* cmd] { PARSER_STATE->checkThatLogicIsSet(); PARSER_STATE->checkLogicAllowsFreeSorts(); - seq.reset(new CVC5::CommandSequence()); + seq.reset(new cvc5::CommandSequence()); } LPAREN_TOK ( symbol[name,CHECK_UNDECLARED,SYM_SORT] @@ -917,7 +917,7 @@ extendedCommand[std::unique_ptr<CVC5::Command>* cmd] { cmd->reset(seq.release()); } | DECLARE_FUNS_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { seq.reset(new CVC5::CommandSequence()); } + { seq.reset(new cvc5::CommandSequence()); } LPAREN_TOK ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } @@ -942,7 +942,7 @@ extendedCommand[std::unique_ptr<CVC5::Command>* cmd] RPAREN_TOK { cmd->reset(seq.release()); } | DECLARE_PREDS_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { seq.reset(new CVC5::CommandSequence()); } + { seq.reset(new cvc5::CommandSequence()); } LPAREN_TOK ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } @@ -1074,7 +1074,7 @@ extendedCommand[std::unique_ptr<CVC5::Command>* cmd] ) ; -datatypeDefCommand[bool isCo, std::unique_ptr<CVC5::Command>* cmd] +datatypeDefCommand[bool isCo, std::unique_ptr<cvc5::Command>* cmd] @declarations { std::vector<api::DatatypeDecl> dts; std::string name; @@ -1090,7 +1090,7 @@ datatypeDefCommand[bool isCo, std::unique_ptr<CVC5::Command>* cmd] datatypesDef[isCo, dnames, arities, cmd] ; -datatypesDefCommand[bool isCo, std::unique_ptr<CVC5::Command>* cmd] +datatypesDefCommand[bool isCo, std::unique_ptr<cvc5::Command>* cmd] @declarations { std::vector<api::DatatypeDecl> dts; std::string name; @@ -1123,7 +1123,7 @@ datatypesDefCommand[bool isCo, std::unique_ptr<CVC5::Command>* cmd] datatypesDef[bool isCo, const std::vector<std::string>& dnames, const std::vector<int>& arities, - std::unique_ptr<CVC5::Command>* cmd] + std::unique_ptr<cvc5::Command>* cmd] @declarations { std::vector<api::DatatypeDecl> dts; std::string name; @@ -1239,7 +1239,7 @@ simpleSymbolicExpr[std::string& s] | KEYWORD { s = AntlrInput::tokenText($KEYWORD); } ; -symbolicExpr[CVC5::api::Term& sexpr] +symbolicExpr[cvc5::api::Term& sexpr] @declarations { std::string s; std::vector<api::Term> children; @@ -1248,19 +1248,19 @@ symbolicExpr[CVC5::api::Term& sexpr] { sexpr = SOLVER->mkString(PARSER_STATE->processAdHocStringEsc(s)); } | LPAREN_TOK ( symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK - { sexpr = SOLVER->mkTerm(CVC5::api::SEXPR, children); } + { sexpr = SOLVER->mkTerm(cvc5::api::SEXPR, children); } ; /** * Matches a term. * @return the expression representing the term. */ -term[CVC5::api::Term& expr, CVC5::api::Term& expr2] +term[cvc5::api::Term& expr, cvc5::api::Term& expr2] @init { api::Kind kind = api::NULL_EXPR; - CVC5::api::Term f; + cvc5::api::Term f; std::string name; - CVC5::api::Sort type; + cvc5::api::Sort type; ParseOp p; } : termNonVariable[expr, expr2] @@ -1278,23 +1278,23 @@ term[CVC5::api::Term& expr, CVC5::api::Term& expr2] * @return the expression expr representing the term or formula, and expr2, an * optional annotation for expr (for instance, for attributed expressions). */ -termNonVariable[CVC5::api::Term& expr, CVC5::api::Term& expr2] +termNonVariable[cvc5::api::Term& expr, cvc5::api::Term& expr2] @init { Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; api::Kind kind = api::NULL_EXPR; std::string name; - std::vector<CVC5::api::Term> args; - std::vector< std::pair<std::string, CVC5::api::Sort> > sortedVarNames; - CVC5::api::Term bvl; - CVC5::api::Term f, f2, f3; + std::vector<cvc5::api::Term> args; + std::vector< std::pair<std::string, cvc5::api::Sort> > sortedVarNames; + cvc5::api::Term bvl; + cvc5::api::Term f, f2, f3; std::string attr; - CVC5::api::Term attexpr; - std::vector<CVC5::api::Term> patexprs; - std::vector<CVC5::api::Term> matchcases; + cvc5::api::Term attexpr; + std::vector<cvc5::api::Term> patexprs; + std::vector<cvc5::api::Term> matchcases; std::unordered_set<std::string> names; - std::vector< std::pair<std::string, CVC5::api::Term> > binders; - CVC5::api::Sort type; - CVC5::api::Sort type2; + std::vector< std::pair<std::string, cvc5::api::Term> > binders; + cvc5::api::Sort type; + cvc5::api::Sort type2; api::Term atomTerm; ParseOp p; std::vector<api::Sort> argTypes; @@ -1409,7 +1409,7 @@ termNonVariable[CVC5::api::Term& expr, CVC5::api::Term& expr2] )* RPAREN_TOK term[f3, f2] { // make the match case - std::vector<CVC5::api::Term> cargs; + std::vector<cvc5::api::Term> cargs; cargs.push_back(f); cargs.insert(cargs.end(),args.begin(),args.end()); api::Term c = MK_TERM(api::APPLY_CONSTRUCTOR,cargs); @@ -1577,12 +1577,12 @@ termNonVariable[CVC5::api::Term& expr, CVC5::api::Term& expr2] * expression (3), which may involve disambiguating f based on type T if it is * overloaded. */ -qualIdentifier[CVC5::ParseOp& p] +qualIdentifier[cvc5::ParseOp& p] @init { api::Kind k; std::string baseName; - CVC5::api::Term f; - CVC5::api::Sort type; + cvc5::api::Term f; + cvc5::api::Sort type; } : identifier[p] | LPAREN_TOK AS_TOK @@ -1608,10 +1608,10 @@ qualIdentifier[CVC5::ParseOp& p] * (3) An expression expr. * For examples, see documentation of qualIdentifier. */ -identifier[CVC5::ParseOp& p] +identifier[cvc5::ParseOp& p] @init { - CVC5::api::Term f; - CVC5::api::Term f2; + cvc5::api::Term f; + cvc5::api::Term f2; std::vector<uint64_t> numerals; } : functionName[p.d_name, CHECK_NONE] @@ -1670,10 +1670,10 @@ identifier[CVC5::ParseOp& p] * Matches an atomic term (a term with no subterms). * @return the expression expr representing the term or formula. */ -termAtomic[CVC5::api::Term& atomTerm] +termAtomic[cvc5::api::Term& atomTerm] @init { - CVC5::api::Sort type; - CVC5::api::Sort type2; + cvc5::api::Sort type; + cvc5::api::Sort type2; std::string s; std::vector<uint64_t> numerals; } @@ -1746,13 +1746,13 @@ termAtomic[CVC5::api::Term& atomTerm] /** * Read attribute */ -attribute[CVC5::api::Term& expr, CVC5::api::Term& retExpr, std::string& attr] +attribute[cvc5::api::Term& expr, cvc5::api::Term& retExpr, std::string& attr] @init { api::Term sexpr; std::string s; - CVC5::api::Term patexpr; - std::vector<CVC5::api::Term> patexprs; - CVC5::api::Term e2; + cvc5::api::Term patexpr; + std::vector<cvc5::api::Term> patexprs; + cvc5::api::Term e2; bool hasValue = false; } : KEYWORD ( simpleSymbolicExprNoKeyword[s] { hasValue = true; } )? @@ -1811,13 +1811,13 @@ attribute[CVC5::api::Term& expr, CVC5::api::Term& retExpr, std::string& attr] * Matches a sequence of terms and puts them into the formulas * vector. * @param formulas the vector to fill with terms - * @param expr an CVC5::api::Term reference for the elements of the sequence + * @param expr an cvc5::api::Term reference for the elements of the sequence */ -/* NOTE: We pass an CVC5::api::Term in here just to avoid allocating a fresh CVC5::api::Term every +/* NOTE: We pass an cvc5::api::Term in here just to avoid allocating a fresh cvc5::api::Term every * time through this rule. */ -termList[std::vector<CVC5::api::Term>& formulas, CVC5::api::Term& expr] +termList[std::vector<cvc5::api::Term>& formulas, cvc5::api::Term& expr] @declarations { - CVC5::api::Term expr2; + cvc5::api::Term expr2; } : ( term[expr, expr2] { formulas.push_back(expr); } )+ ; @@ -1872,7 +1872,7 @@ str[std::string& s, bool fsmtlib] } ; -quantOp[CVC5::api::Kind& kind] +quantOp[cvc5::api::Kind& kind] @init { Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl; } @@ -1884,7 +1884,7 @@ quantOp[CVC5::api::Kind& kind] * Matches a (possibly undeclared) function symbol (returning the string) * @param check what kind of check to do with the symbol */ -functionName[std::string& name, CVC5::parser::DeclarationCheck check] +functionName[std::string& name, cvc5::parser::DeclarationCheck check] : symbol[name,check,SYM_VARIABLE] ; @@ -1892,16 +1892,16 @@ functionName[std::string& name, CVC5::parser::DeclarationCheck check] * Matches a sequence of sort symbols and fills them into the given * vector. */ -sortList[std::vector<CVC5::api::Sort>& sorts] +sortList[std::vector<cvc5::api::Sort>& sorts] @declarations { - CVC5::api::Sort t; + cvc5::api::Sort t; } : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )* ; -nonemptySortList[std::vector<CVC5::api::Sort>& sorts] +nonemptySortList[std::vector<cvc5::api::Sort>& sorts] @declarations { - CVC5::api::Sort t; + cvc5::api::Sort t; } : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+ ; @@ -1910,10 +1910,10 @@ nonemptySortList[std::vector<CVC5::api::Sort>& sorts] * Matches a sequence of (variable,sort) symbol pairs and fills them * into the given vector. */ -sortedVarList[std::vector<std::pair<std::string, CVC5::api::Sort> >& sortedVars] +sortedVarList[std::vector<std::pair<std::string, cvc5::api::Sort> >& sortedVars] @declarations { std::string name; - CVC5::api::Sort t; + cvc5::api::Sort t; } : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED] RPAREN_TOK @@ -1925,13 +1925,13 @@ sortedVarList[std::vector<std::pair<std::string, CVC5::api::Sort> >& sortedVars] * Matches a sequence of (variable, sort) symbol pairs, registers them as bound * variables, and returns a term corresponding to the list of pairs. */ -boundVarList[CVC5::api::Term& expr] +boundVarList[cvc5::api::Term& expr] @declarations { - std::vector<std::pair<std::string, CVC5::api::Sort>> sortedVarNames; + std::vector<std::pair<std::string, cvc5::api::Sort>> sortedVarNames; } : LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK { - std::vector<CVC5::api::Term> args = + std::vector<cvc5::api::Term> args = PARSER_STATE->bindBoundVars(sortedVarNames); expr = MK_TERM(api::BOUND_VAR_LIST, args); } @@ -1941,14 +1941,14 @@ boundVarList[CVC5::api::Term& expr] * Matches the sort symbol, which can be an arbitrary symbol. * @param check the check to perform on the name */ -sortName[std::string& name, CVC5::parser::DeclarationCheck check] +sortName[std::string& name, cvc5::parser::DeclarationCheck check] : symbol[name,check,SYM_SORT] ; -sortSymbol[CVC5::api::Sort& t, CVC5::parser::DeclarationCheck check] +sortSymbol[cvc5::api::Sort& t, cvc5::parser::DeclarationCheck check] @declarations { std::string name; - std::vector<CVC5::api::Sort> args; + std::vector<cvc5::api::Sort> args; std::vector<uint64_t> numerals; bool indexed = false; } @@ -2070,8 +2070,8 @@ sortSymbol[CVC5::api::Sort& t, CVC5::parser::DeclarationCheck check] * symbol[] rule below. */ symbolList[std::vector<std::string>& names, - CVC5::parser::DeclarationCheck check, - CVC5::parser::SymbolType type] + cvc5::parser::DeclarationCheck check, + cvc5::parser::SymbolType type] @declarations { std::string id; } @@ -2085,8 +2085,8 @@ symbolList[std::vector<std::string>& names, * @param type the intended namespace for the symbol */ symbol[std::string& id, - CVC5::parser::DeclarationCheck check, - CVC5::parser::SymbolType type] + cvc5::parser::DeclarationCheck check, + cvc5::parser::SymbolType type] : SIMPLE_SYMBOL { id = AntlrInput::tokenText($SIMPLE_SYMBOL); if(!PARSER_STATE->isAbstractValue(id)) { @@ -2125,8 +2125,8 @@ nonemptyNumeralList[std::vector<uint64_t>& numerals] /** * Parses a datatype definition */ -datatypeDef[bool isCo, std::vector<CVC5::api::DatatypeDecl>& datatypes, - std::vector< CVC5::api::Sort >& params] +datatypeDef[bool isCo, std::vector<cvc5::api::DatatypeDecl>& datatypes, + std::vector< cvc5::api::Sort >& params] @init { std::string id; } @@ -2145,10 +2145,10 @@ datatypeDef[bool isCo, std::vector<CVC5::api::DatatypeDecl>& datatypes, /** * Parses a constructor defintion for type */ -constructorDef[CVC5::api::DatatypeDecl& type] +constructorDef[cvc5::api::DatatypeDecl& type] @init { std::string id; - CVC5::api::DatatypeConstructorDecl* ctor = NULL; + cvc5::api::DatatypeConstructorDecl* ctor = NULL; } : symbol[id,CHECK_NONE,SYM_VARIABLE] { @@ -2163,10 +2163,10 @@ constructorDef[CVC5::api::DatatypeDecl& type] } ; -selector[CVC5::api::DatatypeConstructorDecl& ctor] +selector[cvc5::api::DatatypeConstructorDecl& ctor] @init { std::string id; - CVC5::api::Sort t, t2; + cvc5::api::Sort t, t2; } : symbol[id,CHECK_NONE,SYM_SORT] sortSymbol[t,CHECK_NONE] { diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e05401da0..a1659dcc2 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -28,7 +28,7 @@ #undef true #undef false -namespace CVC5 { +namespace cvc5 { namespace parser { Smt2::Smt2(api::Solver* solver, @@ -1209,4 +1209,4 @@ api::Term Smt2::mkAnd(const std::vector<api::Term>& es) } } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index ccb6456e7..5ad508868 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -31,7 +31,7 @@ #include "theory/logic_info.h" #include "util/abstract_value.h" -namespace CVC5 { +namespace cvc5 { class Command; @@ -430,6 +430,6 @@ class Smt2 : public Parser }; /* class Smt2 */ } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__SMT2_H */ diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 3d6670469..650d97299 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -26,7 +26,7 @@ #include "parser/smt2/Smt2Parser.h" #include "parser/smt2/smt2.h" -namespace CVC5 { +namespace cvc5 { namespace parser { /* Use lookahead=2 */ @@ -68,4 +68,4 @@ api::Term Smt2Input::parseExpr() } } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 0c5be3f97..1c892909e 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -23,10 +23,10 @@ #include "parser/smt2/Smt2Lexer.h" #include "parser/smt2/Smt2Parser.h" -// extern void Smt2ParserSetAntlrParser(CVC5::parser::AntlrParser* +// extern void Smt2ParserSetAntlrParser(cvc5::parser::AntlrParser* // newAntlrParser); -namespace CVC5 { +namespace cvc5 { class Command; class Expr; @@ -82,6 +82,6 @@ class Smt2Input : public AntlrInput { };/* class Smt2Input */ } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__SMT2_INPUT_H */ diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp index bdddd47e8..cc605b842 100644 --- a/src/parser/smt2/sygus_input.cpp +++ b/src/parser/smt2/sygus_input.cpp @@ -26,7 +26,7 @@ #include "parser/smt2/Smt2Parser.h" #include "parser/smt2/sygus_input.h" -namespace CVC5 { +namespace cvc5 { namespace parser { /* Use lookahead=2 */ @@ -69,4 +69,4 @@ api::Term SygusInput::parseExpr() } } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/smt2/sygus_input.h b/src/parser/smt2/sygus_input.h index 38497dfd2..8ad398cf9 100644 --- a/src/parser/smt2/sygus_input.h +++ b/src/parser/smt2/sygus_input.h @@ -23,10 +23,10 @@ #include "parser/smt2/Smt2Lexer.h" #include "parser/smt2/Smt2Parser.h" -// extern void Smt2ParserSetAntlrParser(CVC5::parser::AntlrParser* +// extern void Smt2ParserSetAntlrParser(cvc5::parser::AntlrParser* // newAntlrParser); -namespace CVC5 { +namespace cvc5 { class Command; class Expr; @@ -82,6 +82,6 @@ class SygusInput : public AntlrInput { };/* class SygusInput */ } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__SYGUS_INPUT_H */ diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 265784d48..030330748 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -65,8 +65,8 @@ options { #include "parser/tptp/tptp.h" #include "parser/antlr_input.h" -using namespace CVC5; -using namespace CVC5::parser; +using namespace cvc5; +using namespace cvc5::parser; /* These need to be macros so they can refer to the PARSER macro, which will be defined * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ @@ -108,8 +108,8 @@ using namespace CVC5::parser; #include "util/integer.h" #include "util/rational.h" -using namespace CVC5; -using namespace CVC5::parser; +using namespace cvc5; +using namespace cvc5::parser; /* These need to be macros so they can refer to the PARSER macro, which will be defined * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ @@ -127,10 +127,10 @@ using namespace CVC5::parser; /** * Parses an expression. - * @return the parsed expression, or the Null CVC5::api::Term if we've reached + * @return the parsed expression, or the Null cvc5::api::Term if we've reached * the end of the input */ -parseExpr returns [CVC5::parser::tptp::myExpr expr] +parseExpr returns [cvc5::parser::tptp::myExpr expr] : cnfFormula[expr] | EOF ; @@ -139,9 +139,9 @@ parseExpr returns [CVC5::parser::tptp::myExpr expr] * Parses a command * @return the parsed command, or NULL if we've reached the end of the input */ -parseCommand returns [CVC5::Command* cmd = NULL] +parseCommand returns [cvc5::Command* cmd = NULL] @declarations { - CVC5::api::Term expr; + cvc5::api::Term expr; Tptp::FormulaRole fr; std::string name, inclSymbol; ParseOp p; @@ -159,7 +159,7 @@ parseCommand returns [CVC5::Command* cmd = NULL] } (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK { - CVC5::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr, expr); + cvc5::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr, expr); if( !aexpr.isNull() ){ // set the expression name (e.g. used with unsat core printing) SYM_MAN->setExpressionName(aexpr, name, true); @@ -171,7 +171,7 @@ parseCommand returns [CVC5::Command* cmd = NULL] { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(true); } fofFormula[expr] (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK { - CVC5::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr); + cvc5::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr); if( !aexpr.isNull() ){ // set the expression name (e.g. used with unsat core printing) SYM_MAN->setExpressionName(aexpr, name, true); @@ -185,7 +185,7 @@ parseCommand returns [CVC5::Command* cmd = NULL] { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(false); } tffFormula[expr] (COMMA_TOK anything*)? { - CVC5::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr); + cvc5::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr); if( !aexpr.isNull() ){ // set the expression name (e.g. used with unsat core printing) SYM_MAN->setExpressionName(aexpr, name, true); @@ -207,7 +207,7 @@ parseCommand returns [CVC5::Command* cmd = NULL] PARSER_STATE->parseError("Top level expression must be a formula"); } expr = p.d_expr; - CVC5::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr, expr); + cvc5::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr, expr); if (!aexpr.isNull()) { // set the expression name (e.g. used with unsat core printing) @@ -242,7 +242,7 @@ parseCommand returns [CVC5::Command* cmd = NULL] { CommandSequence* seq = new CommandSequence(); // assert that all distinct constants are distinct - CVC5::api::Term aexpr = PARSER_STATE->getAssertionDistinctConstants(); + cvc5::api::Term aexpr = PARSER_STATE->getAssertionDistinctConstants(); if( !aexpr.isNull() ) { seq->addCommand(new AssertCommand(aexpr, false)); @@ -268,7 +268,7 @@ parseCommand returns [CVC5::Command* cmd = NULL] ; /* Parse a formula Role */ -formulaRole[CVC5::parser::Tptp::FormulaRole& role] +formulaRole[cvc5::parser::Tptp::FormulaRole& role] : LOWER_WORD { std::string r = AntlrInput::tokenText($LOWER_WORD); @@ -296,12 +296,12 @@ formulaRole[CVC5::parser::Tptp::FormulaRole& role] /* It can parse a little more than the cnf grammar: false and true can appear. * Normally only false can appear and only at top level. */ -cnfFormula[CVC5::api::Term& expr] +cnfFormula[cvc5::api::Term& expr] : LPAREN_TOK cnfDisjunction[expr] RPAREN_TOK | cnfDisjunction[expr] ; -cnfDisjunction[CVC5::api::Term& expr] +cnfDisjunction[cvc5::api::Term& expr] @declarations { std::vector<api::Term> args; } @@ -313,16 +313,16 @@ cnfDisjunction[CVC5::api::Term& expr] } ; -cnfLiteral[CVC5::api::Term& expr] +cnfLiteral[cvc5::api::Term& expr] : atomicFormula[expr] | NOT_TOK atomicFormula[expr] { expr = MK_TERM(api::NOT, expr); } ; -atomicFormula[CVC5::api::Term& expr] +atomicFormula[cvc5::api::Term& expr] @declarations { - CVC5::api::Term expr2; + cvc5::api::Term expr2; std::string name; - std::vector<CVC5::api::Term> args; + std::vector<cvc5::api::Term> args; bool equal; ParseOp p; } @@ -386,11 +386,11 @@ atomicFormula[CVC5::api::Term& expr] | definedProp[expr] ; -thfAtomicFormula[CVC5::ParseOp& p] +thfAtomicFormula[cvc5::ParseOp& p] @declarations { - CVC5::api::Term expr2; + cvc5::api::Term expr2; std::string name; - std::vector<CVC5::api::Term> args; + std::vector<cvc5::api::Term> args; bool equal; } : atomicWord[p.d_name] (LPAREN_TOK arguments[args] RPAREN_TOK)? @@ -432,12 +432,12 @@ thfAtomicFormula[CVC5::ParseOp& p] //%----Using <plain_term> removes a reduce/reduce ambiguity in lex/yacc. //%----Note: "defined" means a word starting with one $ and "system" means $$. -definedProp[CVC5::api::Term& expr] +definedProp[cvc5::api::Term& expr] : TRUE_TOK { expr = SOLVER->mkTrue(); } | FALSE_TOK { expr = SOLVER->mkFalse(); } ; -definedPred[CVC5::ParseOp& p] +definedPred[cvc5::ParseOp& p] : '$less' { p.d_kind = api::LT; @@ -497,7 +497,7 @@ definedPred[CVC5::ParseOp& p] } ; -thfDefinedPred[CVC5::ParseOp& p] +thfDefinedPred[cvc5::ParseOp& p] : '$less' { p.d_kind = api::LT; @@ -561,7 +561,7 @@ thfDefinedPred[CVC5::ParseOp& p] RPAREN_TOK ; -definedFun[CVC5::ParseOp& p] +definedFun[cvc5::ParseOp& p] @declarations { bool remainder = false; } @@ -724,16 +724,16 @@ equalOp[bool& equal] | DISEQUAL_TOK { equal = false; } ; -term[CVC5::api::Term& expr] +term[cvc5::api::Term& expr] : functionTerm[expr] | conditionalTerm[expr] | simpleTerm[expr] | letTerm[expr] ; -letTerm[CVC5::api::Term& expr] +letTerm[cvc5::api::Term& expr] @declarations { - CVC5::api::Term lhs, rhs; + cvc5::api::Term lhs, rhs; } : '$let_ft' LPAREN_TOK { PARSER_STATE->pushScope(); } tffLetFormulaDefn[lhs, rhs] COMMA_TOK @@ -752,14 +752,14 @@ letTerm[CVC5::api::Term& expr] ; /* Not an application */ -simpleTerm[CVC5::api::Term& expr] +simpleTerm[cvc5::api::Term& expr] : variable[expr] | NUMBER { expr = PARSER_STATE->d_tmp_expr; } | DISTINCT_OBJECT { expr = PARSER_STATE->convertStrToUnsorted(AntlrInput::tokenText($DISTINCT_OBJECT)); } ; /* Not an application */ -thfSimpleTerm[CVC5::api::Term& expr] +thfSimpleTerm[cvc5::api::Term& expr] : NUMBER { expr = PARSER_STATE->d_tmp_expr; } | DISTINCT_OBJECT { @@ -768,9 +768,9 @@ thfSimpleTerm[CVC5::api::Term& expr] } ; -functionTerm[CVC5::api::Term& expr] +functionTerm[cvc5::api::Term& expr] @declarations { - std::vector<CVC5::api::Term> args; + std::vector<cvc5::api::Term> args; ParseOp p; } : plainTerm[expr] @@ -780,15 +780,15 @@ functionTerm[CVC5::api::Term& expr] } ; -conditionalTerm[CVC5::api::Term& expr] +conditionalTerm[cvc5::api::Term& expr] @declarations { - CVC5::api::Term expr2, expr3; + cvc5::api::Term expr2, expr3; } : '$ite_t' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK term[expr2] COMMA_TOK term[expr3] RPAREN_TOK { expr = MK_TERM(api::ITE, expr, expr2, expr3); } ; -plainTerm[CVC5::api::Term& expr] +plainTerm[cvc5::api::Term& expr] @declarations { std::string name; std::vector<api::Term> args; @@ -801,15 +801,15 @@ plainTerm[CVC5::api::Term& expr] } ; -arguments[std::vector<CVC5::api::Term>& args] +arguments[std::vector<cvc5::api::Term>& args] @declarations { - CVC5::api::Term expr; + cvc5::api::Term expr; } : term[expr] { args.push_back(expr); } ( COMMA_TOK term[expr] { args.push_back(expr); } )* ; -variable[CVC5::api::Term& expr] +variable[cvc5::api::Term& expr] : UPPER_WORD { std::string name = AntlrInput::tokenText($UPPER_WORD); @@ -824,13 +824,13 @@ variable[CVC5::api::Term& expr] /*******/ /* FOF */ -fofFormula[CVC5::api::Term& expr] : fofLogicFormula[expr] ; +fofFormula[cvc5::api::Term& expr] : fofLogicFormula[expr] ; -fofLogicFormula[CVC5::api::Term& expr] +fofLogicFormula[cvc5::api::Term& expr] @declarations { tptp::NonAssoc na; - std::vector< CVC5::api::Term > args; - CVC5::api::Term expr2; + std::vector< cvc5::api::Term > args; + cvc5::api::Term expr2; } : fofUnitaryFormula[expr] ( // Non-associative: <=> <~> ~& ~| @@ -870,10 +870,10 @@ fofLogicFormula[CVC5::api::Term& expr] )? ; -fofUnitaryFormula[CVC5::api::Term& expr] +fofUnitaryFormula[cvc5::api::Term& expr] @declarations { api::Kind kind; - std::vector< CVC5::api::Term > bv; + std::vector< cvc5::api::Term > bv; } : atomicFormula[expr] | LPAREN_TOK fofLogicFormula[expr] RPAREN_TOK @@ -888,14 +888,14 @@ fofUnitaryFormula[CVC5::api::Term& expr] } ; -bindvariable[CVC5::api::Term& expr] +bindvariable[cvc5::api::Term& expr] : UPPER_WORD { std::string name = AntlrInput::tokenText($UPPER_WORD); expr = PARSER_STATE->bindBoundVar(name, PARSER_STATE->d_unsorted); } ; -fofBinaryNonAssoc[CVC5::parser::tptp::NonAssoc& na] +fofBinaryNonAssoc[cvc5::parser::tptp::NonAssoc& na] : IFF_TOK { na = tptp::NA_IFF; } | REVIFF_TOK { na = tptp::NA_REVIFF; } | REVOR_TOK { na = tptp::NA_REVOR; } @@ -904,7 +904,7 @@ fofBinaryNonAssoc[CVC5::parser::tptp::NonAssoc& na] | REVIMPLIES_TOK { na = tptp::NA_REVIMPLIES; } ; -folQuantifier[CVC5::api::Kind& kind] +folQuantifier[cvc5::api::Kind& kind] : FORALL_TOK { kind = api::FORALL; } | EXISTS_TOK { kind = api::EXISTS; } ; @@ -912,7 +912,7 @@ folQuantifier[CVC5::api::Kind& kind] /*******/ /* THF */ -thfQuantifier[CVC5::api::Kind& kind] +thfQuantifier[cvc5::api::Kind& kind] : FORALL_TOK { kind = api::FORALL; } | EXISTS_TOK { kind = api::EXISTS; } | LAMBDA_TOK { kind = api::LAMBDA; } @@ -930,11 +930,11 @@ thfQuantifier[CVC5::api::Kind& kind] } ; -thfAtomTyping[CVC5::Command*& cmd] +thfAtomTyping[cvc5::Command*& cmd] // for now only supports mapping types (i.e. no applied types) @declarations { - CVC5::api::Term expr; - CVC5::api::Sort type; + cvc5::api::Term expr; + cvc5::api::Sort type; std::string name; } : LPAREN_TOK thfAtomTyping[cmd] RPAREN_TOK @@ -988,7 +988,7 @@ thfAtomTyping[CVC5::Command*& cmd] else { // as of yet, it's undeclared - CVC5::api::Term freshExpr; + cvc5::api::Term freshExpr; if (type.isFunction()) { freshExpr = PARSER_STATE->bindVar(name, type); @@ -1003,12 +1003,12 @@ thfAtomTyping[CVC5::Command*& cmd] ) ; -thfLogicFormula[CVC5::ParseOp& p] +thfLogicFormula[cvc5::ParseOp& p] @declarations { tptp::NonAssoc na; - std::vector<CVC5::api::Term> args; + std::vector<cvc5::api::Term> args; std::vector<ParseOp> p_args; - CVC5::api::Term expr2; + cvc5::api::Term expr2; bool equal; ParseOp p1; } @@ -1194,7 +1194,7 @@ thfLogicFormula[CVC5::ParseOp& p] )? ; -thfTupleForm[std::vector<CVC5::api::Term>& args] +thfTupleForm[std::vector<cvc5::api::Term>& args] @declarations { ParseOp p; } @@ -1217,11 +1217,11 @@ thfTupleForm[std::vector<CVC5::api::Term>& args] )+ ; -thfUnitaryFormula[CVC5::ParseOp& p] +thfUnitaryFormula[cvc5::ParseOp& p] @declarations { api::Kind kind; - std::vector< CVC5::api::Term > bv; - CVC5::api::Term expr; + std::vector< cvc5::api::Term > bv; + cvc5::api::Term expr; bool equal; ParseOp p1; } @@ -1289,12 +1289,12 @@ thfUnitaryFormula[CVC5::ParseOp& p] /*******/ /* TFF */ -tffFormula[CVC5::api::Term& expr] : tffLogicFormula[expr]; +tffFormula[cvc5::api::Term& expr] : tffLogicFormula[expr]; -tffTypedAtom[CVC5::Command*& cmd] +tffTypedAtom[cvc5::Command*& cmd] @declarations { - CVC5::api::Term expr; - CVC5::api::Sort type; + cvc5::api::Term expr; + cvc5::api::Sort type; std::string name; } : LPAREN_TOK tffTypedAtom[cmd] RPAREN_TOK @@ -1327,18 +1327,18 @@ tffTypedAtom[CVC5::Command*& cmd] } } else { // as yet, it's undeclared - CVC5::api::Term aexpr = PARSER_STATE->bindVar(name, type); + cvc5::api::Term aexpr = PARSER_STATE->bindVar(name, type); cmd = new DeclareFunctionCommand(name, aexpr, type); } } ) ; -tffLogicFormula[CVC5::api::Term& expr] +tffLogicFormula[cvc5::api::Term& expr] @declarations { tptp::NonAssoc na; - std::vector< CVC5::api::Term > args; - CVC5::api::Term expr2; + std::vector< cvc5::api::Term > args; + cvc5::api::Term expr2; } : tffUnitaryFormula[expr] ( // Non Assoc <=> <~> ~& ~| @@ -1378,11 +1378,11 @@ tffLogicFormula[CVC5::api::Term& expr] )? ; -tffUnitaryFormula[CVC5::api::Term& expr] +tffUnitaryFormula[cvc5::api::Term& expr] @declarations { api::Kind kind; - std::vector< CVC5::api::Term > bv; - CVC5::api::Term lhs, rhs; + std::vector< cvc5::api::Term > bv; + cvc5::api::Term lhs, rhs; } : atomicFormula[expr] | LPAREN_TOK tffLogicFormula[expr] RPAREN_TOK @@ -1413,17 +1413,17 @@ tffUnitaryFormula[CVC5::api::Term& expr] RPAREN_TOK ; -tffLetTermDefn[CVC5::api::Term& lhs, CVC5::api::Term& rhs] +tffLetTermDefn[cvc5::api::Term& lhs, cvc5::api::Term& rhs] @declarations { - std::vector<CVC5::api::Term> bvlist; + std::vector<cvc5::api::Term> bvlist; } : (FORALL_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)* tffLetTermBinding[bvlist, lhs, rhs] ; -tffLetTermBinding[std::vector<CVC5::api::Term> & bvlist, - CVC5::api::Term& lhs, - CVC5::api::Term& rhs] +tffLetTermBinding[std::vector<cvc5::api::Term> & bvlist, + cvc5::api::Term& lhs, + cvc5::api::Term& rhs] : term[lhs] EQUAL_TOK term[rhs] { PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false); @@ -1438,17 +1438,17 @@ tffLetTermBinding[std::vector<CVC5::api::Term> & bvlist, | LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK ; -tffLetFormulaDefn[CVC5::api::Term& lhs, CVC5::api::Term& rhs] +tffLetFormulaDefn[cvc5::api::Term& lhs, cvc5::api::Term& rhs] @declarations { - std::vector<CVC5::api::Term> bvlist; + std::vector<cvc5::api::Term> bvlist; } : (FORALL_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)* tffLetFormulaBinding[bvlist, lhs, rhs] ; -tffLetFormulaBinding[std::vector<CVC5::api::Term> & bvlist, - CVC5::api::Term& lhs, - CVC5::api::Term& rhs] +tffLetFormulaBinding[std::vector<cvc5::api::Term> & bvlist, + cvc5::api::Term& lhs, + cvc5::api::Term& rhs] : atomicFormula[lhs] IFF_TOK tffUnitaryFormula[rhs] { @@ -1464,10 +1464,10 @@ tffLetFormulaBinding[std::vector<CVC5::api::Term> & bvlist, | LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK ; -thfBindVariable[CVC5::api::Term& expr] +thfBindVariable[cvc5::api::Term& expr] @declarations { std::string name; - CVC5::api::Sort type = PARSER_STATE->d_unsorted; + cvc5::api::Sort type = PARSER_STATE->d_unsorted; } : UPPER_WORD { name = AntlrInput::tokenText($UPPER_WORD); } @@ -1478,9 +1478,9 @@ thfBindVariable[CVC5::api::Term& expr] ; -tffbindvariable[CVC5::api::Term& expr] +tffbindvariable[cvc5::api::Term& expr] @declarations { - CVC5::api::Sort type = PARSER_STATE->d_unsorted; + cvc5::api::Sort type = PARSER_STATE->d_unsorted; } : UPPER_WORD ( COLON_TOK parseType[type] )? @@ -1491,18 +1491,18 @@ tffbindvariable[CVC5::api::Term& expr] // bvlist is accumulative; it can already contain elements // on the way in, which are left undisturbed -tffVariableList[std::vector<CVC5::api::Term>& bvlist] +tffVariableList[std::vector<cvc5::api::Term>& bvlist] @declarations { - CVC5::api::Term e; + cvc5::api::Term e; } : tffbindvariable[e] { bvlist.push_back(e); } ( COMMA_TOK tffbindvariable[e] { bvlist.push_back(e); } )* ; -parseThfType[CVC5::api::Sort& type] +parseThfType[cvc5::api::Sort& type] // assumes only mapping types (arrows), no tuple type @declarations { - std::vector<CVC5::api::Sort> sorts; + std::vector<cvc5::api::Sort> sorts; } : thfType[type] { sorts.push_back(type); } ( @@ -1522,17 +1522,17 @@ parseThfType[CVC5::api::Sort& type] } ; -thfType[CVC5::api::Sort& type] +thfType[cvc5::api::Sort& type] // assumes only mapping types (arrows), no tuple type : simpleType[type] | LPAREN_TOK parseThfType[type] RPAREN_TOK | LBRACK_TOK { UNSUPPORTED("Tuple types"); } parseThfType[type] RBRACK_TOK ; -parseType[CVC5::api::Sort & type] +parseType[cvc5::api::Sort & type] @declarations { - std::vector<CVC5::api::Sort> v; + std::vector<cvc5::api::Sort> v; } : simpleType[type] | ( simpleType[type] { v.push_back(type); } @@ -1546,7 +1546,7 @@ parseType[CVC5::api::Sort & type] ; // non-function types -simpleType[CVC5::api::Sort& type] +simpleType[cvc5::api::Sort& type] @declarations { std::string name; } diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index e6b4969c3..136319225 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -28,7 +28,7 @@ #undef true #undef false -namespace CVC5 { +namespace cvc5 { namespace parser { Tptp::Tptp(api::Solver* solver, @@ -202,7 +202,7 @@ void Tptp::checkLetBinding(const std::vector<api::Term>& bvlist, { parseError("malformed let: LHS must be formula"); } - for (const CVC5::api::Term& var : vars) + for (const cvc5::api::Term& var : vars) { if (var.hasOp()) { @@ -569,4 +569,4 @@ Command* Tptp::makeAssertCommand(FormulaRole fr, } } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 318ef7f4a..b91418bd0 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -27,7 +27,7 @@ #include "parser/parser.h" #include "util/hash.h" -namespace CVC5 { +namespace cvc5 { class Command; @@ -218,12 +218,12 @@ namespace tptp { * Just exists to provide the uintptr_t constructor that ANTLR * requires. */ -struct myExpr : public CVC5::api::Term +struct myExpr : public cvc5::api::Term { - myExpr() : CVC5::api::Term() {} - myExpr(void*) : CVC5::api::Term() {} - myExpr(const CVC5::api::Term& e) : CVC5::api::Term(e) {} - myExpr(const myExpr& e) : CVC5::api::Term(e) {} + myExpr() : cvc5::api::Term() {} + myExpr(void*) : cvc5::api::Term() {} + myExpr(const cvc5::api::Term& e) : cvc5::api::Term(e) {} + myExpr(const myExpr& e) : cvc5::api::Term(e) {} }; /* struct myExpr*/ enum NonAssoc { @@ -238,6 +238,6 @@ enum NonAssoc { } // namespace tptp } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__TPTP_INPUT_H */ diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp index f3489f3fe..9e2943c47 100644 --- a/src/parser/tptp/tptp_input.cpp +++ b/src/parser/tptp/tptp_input.cpp @@ -26,7 +26,7 @@ #include "parser/tptp/TptpParser.h" #include "parser/tptp/tptp.h" -namespace CVC5 { +namespace cvc5 { namespace parser { /* Use lookahead=2 */ @@ -69,4 +69,4 @@ api::Term TptpInput::parseExpr() } } // namespace parser -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h index bfe8562fc..ff4ac590f 100644 --- a/src/parser/tptp/tptp_input.h +++ b/src/parser/tptp/tptp_input.h @@ -23,10 +23,10 @@ #include "parser/tptp/TptpLexer.h" #include "parser/tptp/TptpParser.h" -// extern void TptpParserSetAntlrParser(CVC5::parser::AntlrParser* +// extern void TptpParserSetAntlrParser(cvc5::parser::AntlrParser* // newAntlrParser); -namespace CVC5 { +namespace cvc5 { class Command; class Expr; @@ -82,6 +82,6 @@ class TptpInput : public AntlrInput { };/* class TptpInput */ } // namespace parser -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__PARSER__TPTP_INPUT_H */ |