summaryrefslogtreecommitdiff
path: root/src/parser/smt2
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2')
-rw-r--r--src/parser/smt2/Smt2.g228
-rw-r--r--src/parser/smt2/smt2.cpp4
-rw-r--r--src/parser/smt2/smt2.h4
-rw-r--r--src/parser/smt2/smt2_input.cpp6
-rw-r--r--src/parser/smt2/smt2_input.h9
-rw-r--r--src/parser/smt2/sygus_input.cpp6
-rw-r--r--src/parser/smt2/sygus_input.h9
7 files changed, 134 insertions, 132 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index e1e1f1cb1..e55cbf510 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 CVC4;
-using namespace CVC4::parser;
+using namespace CVC5;
+using namespace CVC5::parser;
#undef PARSER_STATE
#define PARSER_STATE ((Smt2*)LEXER->super)
@@ -83,7 +83,7 @@ using namespace CVC4::parser;
#include "parser/parser.h"
#include "smt/command.h"
-namespace CVC4 {
+namespace CVC5 {
namespace api {
class Term;
@@ -113,8 +113,8 @@ namespace CVC4 {
#include "util/integer.h"
#include "util/rational.h"
-using namespace CVC4;
-using namespace CVC4::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 CVC4::parser;
* @return the parsed expression, or the Null Expr if we've reached the
* end of the input
*/
-parseExpr returns [CVC4::api::Term expr = CVC4::api::Term()]
+parseExpr returns [CVC5::api::Term expr = CVC5::api::Term()]
@declarations {
- CVC4::api::Term expr2;
+ CVC5::api::Term expr2;
}
: term[expr, expr2]
| EOF
@@ -148,9 +148,9 @@ parseExpr returns [CVC4::api::Term expr = CVC4::api::Term()]
* Parses a command
* @return the parsed command, or NULL if we've reached the end of the input
*/
-parseCommand returns [CVC4::Command* cmd_return = NULL]
+parseCommand returns [CVC5::Command* cmd_return = NULL]
@declarations {
- std::unique_ptr<CVC4::Command> cmd;
+ std::unique_ptr<CVC5::Command> cmd;
std::string name;
}
@after {
@@ -184,7 +184,7 @@ parseCommand returns [CVC4::Command* cmd_return = NULL]
* @return the parsed SyGuS command, or NULL if we've reached the end of the
* input
*/
-parseSygus returns [CVC4::Command* cmd_return = NULL]
+parseSygus returns [CVC5::Command* cmd_return = NULL]
@declarations {
std::string name;
}
@@ -199,16 +199,16 @@ parseSygus returns [CVC4::Command* cmd_return = NULL]
* Parse the internal portion of the command, ignoring the surrounding
* parentheses.
*/
-command [std::unique_ptr<CVC4::Command>* cmd]
+command [std::unique_ptr<CVC5::Command>* cmd]
@declarations {
std::string name;
std::vector<std::string> names;
- CVC4::api::Term expr, expr2;
- CVC4::api::Sort t;
- std::vector<CVC4::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, CVC4::api::Sort> > sortedVarNames;
- std::vector<CVC4::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<CVC4::Command>* cmd]
}
;
-sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
+sygusCommand returns [std::unique_ptr<CVC5::Command> cmd]
@declarations {
- CVC4::api::Term expr, expr2, fun;
- CVC4::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, CVC4::api::Sort> > sortedVarNames;
- std::vector<CVC4::api::Term> sygusVars;
+ std::vector<std::pair<std::string, CVC5::api::Sort> > sortedVarNames;
+ std::vector<CVC5::api::Term> sygusVars;
std::string name;
bool isInv;
- CVC4::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<CVC4::Command> cmd]
* The argument fun is a unique identifier to avoid naming clashes for the
* datatypes constructed by this call.
*/
-sygusGrammar[CVC4::api::Grammar*& ret,
- const std::vector<CVC4::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, CVC4::api::Sort>> sortedVarNames;
+ std::vector<std::pair<std::string, CVC5::api::Sort>> sortedVarNames;
// non-terminal symbols of the grammar
- std::vector<CVC4::api::Term> ntSyms;
- CVC4::api::Sort t;
+ std::vector<CVC5::api::Term> ntSyms;
+ CVC5::api::Sort t;
std::string name;
- CVC4::api::Term e, e2;
+ CVC5::api::Term e, e2;
unsigned dtProcessed = 0;
}
:
@@ -710,7 +710,7 @@ sygusGrammar[CVC4::api::Grammar*& ret,
}
;
-setInfoInternal[std::unique_ptr<CVC4::Command>* cmd]
+setInfoInternal[std::unique_ptr<CVC5::Command>* cmd]
@declarations {
std::string name;
api::Term sexpr;
@@ -721,7 +721,7 @@ setInfoInternal[std::unique_ptr<CVC4::Command>* cmd]
}
;
-setOptionInternal[std::unique_ptr<CVC4::Command>* cmd]
+setOptionInternal[std::unique_ptr<CVC5::Command>* cmd]
@init {
std::string name;
api::Term sexpr;
@@ -738,26 +738,26 @@ setOptionInternal[std::unique_ptr<CVC4::Command>* cmd]
}
;
-smt25Command[std::unique_ptr<CVC4::Command>* cmd]
+smt25Command[std::unique_ptr<CVC5::Command>* cmd]
@declarations {
std::string name;
std::string fname;
- CVC4::api::Term expr, expr2;
- std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
+ CVC5::api::Term expr, expr2;
+ std::vector<std::pair<std::string, CVC5::api::Sort> > sortedVarNames;
std::string s;
- CVC4::api::Sort t;
- CVC4::api::Term func;
- std::vector<CVC4::api::Term> bvs;
- std::vector<std::vector<std::pair<std::string, CVC4::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<CVC4::api::Term>> flattenVarsList;
- std::vector<std::vector<CVC4::api::Term>> formals;
- std::vector<CVC4::api::Term> funcs;
- std::vector<CVC4::api::Term> func_defs;
- CVC4::api::Term aexpr;
- std::unique_ptr<CVC4::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<CVC4::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<CVC4::Command>* cmd]
}
;
-extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
+extendedCommand[std::unique_ptr<CVC5::Command>* cmd]
@declarations {
std::vector<api::DatatypeDecl> dts;
- CVC4::api::Term e, e2;
- CVC4::api::Sort t, s;
+ CVC5::api::Term e, e2;
+ CVC5::api::Sort t, s;
std::string name;
std::vector<std::string> names;
- std::vector<CVC4::api::Term> terms;
+ std::vector<CVC5::api::Term> terms;
std::vector<api::Sort> sorts;
- std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
- std::unique_ptr<CVC4::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<CVC4::Command>* cmd]
{
PARSER_STATE->checkThatLogicIsSet();
PARSER_STATE->checkLogicAllowsFreeSorts();
- seq.reset(new CVC4::CommandSequence());
+ seq.reset(new CVC5::CommandSequence());
}
LPAREN_TOK
( symbol[name,CHECK_UNDECLARED,SYM_SORT]
@@ -917,7 +917,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
{ cmd->reset(seq.release()); }
| DECLARE_FUNS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
- { seq.reset(new CVC4::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<CVC4::Command>* cmd]
RPAREN_TOK
{ cmd->reset(seq.release()); }
| DECLARE_PREDS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
- { seq.reset(new CVC4::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<CVC4::Command>* cmd]
)
;
-datatypeDefCommand[bool isCo, std::unique_ptr<CVC4::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<CVC4::Command>* cmd]
datatypesDef[isCo, dnames, arities, cmd]
;
-datatypesDefCommand[bool isCo, std::unique_ptr<CVC4::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<CVC4::Command>* cmd]
datatypesDef[bool isCo,
const std::vector<std::string>& dnames,
const std::vector<int>& arities,
- std::unique_ptr<CVC4::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[CVC4::api::Term& sexpr]
+symbolicExpr[CVC5::api::Term& sexpr]
@declarations {
std::string s;
std::vector<api::Term> children;
@@ -1248,19 +1248,19 @@ symbolicExpr[CVC4::api::Term& sexpr]
{ sexpr = SOLVER->mkString(PARSER_STATE->processAdHocStringEsc(s)); }
| LPAREN_TOK
( symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK
- { sexpr = SOLVER->mkTerm(CVC4::api::SEXPR, children); }
+ { sexpr = SOLVER->mkTerm(CVC5::api::SEXPR, children); }
;
/**
* Matches a term.
* @return the expression representing the term.
*/
-term[CVC4::api::Term& expr, CVC4::api::Term& expr2]
+term[CVC5::api::Term& expr, CVC5::api::Term& expr2]
@init {
api::Kind kind = api::NULL_EXPR;
- CVC4::api::Term f;
+ CVC5::api::Term f;
std::string name;
- CVC4::api::Sort type;
+ CVC5::api::Sort type;
ParseOp p;
}
: termNonVariable[expr, expr2]
@@ -1278,23 +1278,23 @@ term[CVC4::api::Term& expr, CVC4::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[CVC4::api::Term& expr, CVC4::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<CVC4::api::Term> args;
- std::vector< std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
- CVC4::api::Term bvl;
- CVC4::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;
- CVC4::api::Term attexpr;
- std::vector<CVC4::api::Term> patexprs;
- std::vector<CVC4::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, CVC4::api::Term> > binders;
- CVC4::api::Sort type;
- CVC4::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[CVC4::api::Term& expr, CVC4::api::Term& expr2]
)*
RPAREN_TOK term[f3, f2] {
// make the match case
- std::vector<CVC4::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[CVC4::api::Term& expr, CVC4::api::Term& expr2]
* expression (3), which may involve disambiguating f based on type T if it is
* overloaded.
*/
-qualIdentifier[CVC4::ParseOp& p]
+qualIdentifier[CVC5::ParseOp& p]
@init {
api::Kind k;
std::string baseName;
- CVC4::api::Term f;
- CVC4::api::Sort type;
+ CVC5::api::Term f;
+ CVC5::api::Sort type;
}
: identifier[p]
| LPAREN_TOK AS_TOK
@@ -1608,10 +1608,10 @@ qualIdentifier[CVC4::ParseOp& p]
* (3) An expression expr.
* For examples, see documentation of qualIdentifier.
*/
-identifier[CVC4::ParseOp& p]
+identifier[CVC5::ParseOp& p]
@init {
- CVC4::api::Term f;
- CVC4::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[CVC4::ParseOp& p]
* Matches an atomic term (a term with no subterms).
* @return the expression expr representing the term or formula.
*/
-termAtomic[CVC4::api::Term& atomTerm]
+termAtomic[CVC5::api::Term& atomTerm]
@init {
- CVC4::api::Sort type;
- CVC4::api::Sort type2;
+ CVC5::api::Sort type;
+ CVC5::api::Sort type2;
std::string s;
std::vector<uint64_t> numerals;
}
@@ -1746,13 +1746,13 @@ termAtomic[CVC4::api::Term& atomTerm]
/**
* Read attribute
*/
-attribute[CVC4::api::Term& expr, CVC4::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;
- CVC4::api::Term patexpr;
- std::vector<CVC4::api::Term> patexprs;
- CVC4::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[CVC4::api::Term& expr, CVC4::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 CVC4::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 CVC4::api::Term in here just to avoid allocating a fresh CVC4::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<CVC4::api::Term>& formulas, CVC4::api::Term& expr]
+termList[std::vector<CVC5::api::Term>& formulas, CVC5::api::Term& expr]
@declarations {
- CVC4::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[CVC4::api::Kind& kind]
+quantOp[CVC5::api::Kind& kind]
@init {
Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
@@ -1884,7 +1884,7 @@ quantOp[CVC4::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, CVC4::parser::DeclarationCheck check]
+functionName[std::string& name, CVC5::parser::DeclarationCheck check]
: symbol[name,check,SYM_VARIABLE]
;
@@ -1892,16 +1892,16 @@ functionName[std::string& name, CVC4::parser::DeclarationCheck check]
* Matches a sequence of sort symbols and fills them into the given
* vector.
*/
-sortList[std::vector<CVC4::api::Sort>& sorts]
+sortList[std::vector<CVC5::api::Sort>& sorts]
@declarations {
- CVC4::api::Sort t;
+ CVC5::api::Sort t;
}
: ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )*
;
-nonemptySortList[std::vector<CVC4::api::Sort>& sorts]
+nonemptySortList[std::vector<CVC5::api::Sort>& sorts]
@declarations {
- CVC4::api::Sort t;
+ CVC5::api::Sort t;
}
: ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )+
;
@@ -1910,10 +1910,10 @@ nonemptySortList[std::vector<CVC4::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, CVC4::api::Sort> >& sortedVars]
+sortedVarList[std::vector<std::pair<std::string, CVC5::api::Sort> >& sortedVars]
@declarations {
std::string name;
- CVC4::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, CVC4::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[CVC4::api::Term& expr]
+boundVarList[CVC5::api::Term& expr]
@declarations {
- std::vector<std::pair<std::string, CVC4::api::Sort>> sortedVarNames;
+ std::vector<std::pair<std::string, CVC5::api::Sort>> sortedVarNames;
}
: LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
{
- std::vector<CVC4::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[CVC4::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, CVC4::parser::DeclarationCheck check]
+sortName[std::string& name, CVC5::parser::DeclarationCheck check]
: symbol[name,check,SYM_SORT]
;
-sortSymbol[CVC4::api::Sort& t, CVC4::parser::DeclarationCheck check]
+sortSymbol[CVC5::api::Sort& t, CVC5::parser::DeclarationCheck check]
@declarations {
std::string name;
- std::vector<CVC4::api::Sort> args;
+ std::vector<CVC5::api::Sort> args;
std::vector<uint64_t> numerals;
bool indexed = false;
}
@@ -2070,8 +2070,8 @@ sortSymbol[CVC4::api::Sort& t, CVC4::parser::DeclarationCheck check]
* symbol[] rule below.
*/
symbolList[std::vector<std::string>& names,
- CVC4::parser::DeclarationCheck check,
- CVC4::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,
- CVC4::parser::DeclarationCheck check,
- CVC4::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<CVC4::api::DatatypeDecl>& datatypes,
- std::vector< CVC4::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<CVC4::api::DatatypeDecl>& datatypes,
/**
* Parses a constructor defintion for type
*/
-constructorDef[CVC4::api::DatatypeDecl& type]
+constructorDef[CVC5::api::DatatypeDecl& type]
@init {
std::string id;
- CVC4::api::DatatypeConstructorDecl* ctor = NULL;
+ CVC5::api::DatatypeConstructorDecl* ctor = NULL;
}
: symbol[id,CHECK_NONE,SYM_VARIABLE]
{
@@ -2163,10 +2163,10 @@ constructorDef[CVC4::api::DatatypeDecl& type]
}
;
-selector[CVC4::api::DatatypeConstructorDecl& ctor]
+selector[CVC5::api::DatatypeConstructorDecl& ctor]
@init {
std::string id;
- CVC4::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 a014e1349..e05401da0 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -28,7 +28,7 @@
#undef true
#undef false
-namespace CVC4 {
+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
-}/* CVC4 namespace */
+} // namespace CVC5
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index a7fe65f67..ccb6456e7 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 CVC4 {
+namespace CVC5 {
class Command;
@@ -430,6 +430,6 @@ class Smt2 : public Parser
}; /* class Smt2 */
} // namespace parser
-} // namespace CVC4
+} // namespace CVC5
#endif /* CVC4__PARSER__SMT2_H */
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index c9019811b..3d6670469 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 CVC4 {
+namespace CVC5 {
namespace parser {
/* Use lookahead=2 */
@@ -67,5 +67,5 @@ api::Term Smt2Input::parseExpr()
return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
}
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
+} // namespace parser
+} // namespace CVC5
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index be8f37f52..0c5be3f97 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -23,9 +23,10 @@
#include "parser/smt2/Smt2Lexer.h"
#include "parser/smt2/Smt2Parser.h"
-// extern void Smt2ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser);
+// extern void Smt2ParserSetAntlrParser(CVC5::parser::AntlrParser*
+// newAntlrParser);
-namespace CVC4 {
+namespace CVC5 {
class Command;
class Expr;
@@ -80,7 +81,7 @@ class Smt2Input : public AntlrInput {
};/* class Smt2Input */
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
+} // namespace parser
+} // 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 6487e5dd6..bdddd47e8 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 CVC4 {
+namespace CVC5 {
namespace parser {
/* Use lookahead=2 */
@@ -68,5 +68,5 @@ api::Term SygusInput::parseExpr()
return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
}
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
+} // namespace parser
+} // namespace CVC5
diff --git a/src/parser/smt2/sygus_input.h b/src/parser/smt2/sygus_input.h
index ac7f56856..38497dfd2 100644
--- a/src/parser/smt2/sygus_input.h
+++ b/src/parser/smt2/sygus_input.h
@@ -23,9 +23,10 @@
#include "parser/smt2/Smt2Lexer.h"
#include "parser/smt2/Smt2Parser.h"
-// extern void Smt2ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser);
+// extern void Smt2ParserSetAntlrParser(CVC5::parser::AntlrParser*
+// newAntlrParser);
-namespace CVC4 {
+namespace CVC5 {
class Command;
class Expr;
@@ -80,7 +81,7 @@ class SygusInput : public AntlrInput {
};/* class SygusInput */
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
+} // namespace parser
+} // namespace CVC5
#endif /* CVC4__PARSER__SYGUS_INPUT_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback