summaryrefslogtreecommitdiff
path: root/src/parser/smt2/Smt2.g
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r--src/parser/smt2/Smt2.g106
1 files changed, 40 insertions, 66 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 6e9f04ce9..f1acac6ba 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -770,6 +770,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
std::vector< std::pair<std::string, Expr> > binders;
Type type;
std::string s;
+ bool isBuiltinOperator = false;
}
: /* a built-in operator application */
LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
@@ -835,7 +836,6 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
} else if(f.getKind() == CVC4::kind::EMPTYSET) {
Debug("parser") << "Empty set encountered: " << f << " "
<< f2 << " " << type << std::endl;
- // TODO: what is f2 about, should we add some assertions?
expr = MK_CONST( ::CVC4::EmptySet(type) );
} else {
if(f.getType() != type) {
@@ -879,34 +879,44 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
expr = MK_EXPR(kind, args);
}
}
- | /* A non-built-in function application */
- LPAREN_TOK
- functionName[name, CHECK_DECLARED]
- { PARSER_STATE->checkFunctionLike(name);
- const bool isDefinedFunction =
- PARSER_STATE->isDefinedFunction(name);
- if(isDefinedFunction) {
- expr = PARSER_STATE->getFunction(name);
- kind = CVC4::kind::APPLY;
+ | LPAREN_TOK functionName[name, CHECK_NONE]
+ { isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
+ if(isBuiltinOperator) {
+ /* A built-in operator not already handled by the lexer */
+ kind = PARSER_STATE->getOperatorKind(name);
} else {
- expr = PARSER_STATE->getVariable(name);
- Type t = expr.getType();
- if(t.isConstructor()) {
- kind = CVC4::kind::APPLY_CONSTRUCTOR;
- } else if(t.isSelector()) {
- kind = CVC4::kind::APPLY_SELECTOR;
- } else if(t.isTester()) {
- kind = CVC4::kind::APPLY_TESTER;
+ /* A non-built-in function application */
+ PARSER_STATE->checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE);
+ PARSER_STATE->checkFunctionLike(name);
+ const bool isDefinedFunction =
+ PARSER_STATE->isDefinedFunction(name);
+ if(isDefinedFunction) {
+ expr = PARSER_STATE->getFunction(name);
+ kind = CVC4::kind::APPLY;
} else {
- kind = CVC4::kind::APPLY_UF;
+ expr = PARSER_STATE->getVariable(name);
+ Type t = expr.getType();
+ if(t.isConstructor()) {
+ kind = CVC4::kind::APPLY_CONSTRUCTOR;
+ } else if(t.isSelector()) {
+ kind = CVC4::kind::APPLY_SELECTOR;
+ } else if(t.isTester()) {
+ kind = CVC4::kind::APPLY_TESTER;
+ } else {
+ kind = CVC4::kind::APPLY_UF;
+ }
}
+ args.push_back(expr);
}
- args.push_back(expr);
- }
+ }
termList[args,expr] RPAREN_TOK
{ Debug("parser") << "args has size " << args.size() << std::endl << "expr is " << expr << std::endl;
- for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
+ for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) {
Debug("parser") << "++ " << *i << std::endl;
+ }
+ if(isBuiltinOperator) {
+ PARSER_STATE->checkOperator(kind, args.size());
+ }
expr = MK_EXPR(kind, args); }
| /* An indexed function application */
@@ -1283,14 +1293,6 @@ builtinOp[CVC4::Kind& kind]
if(PARSER_STATE->strictModeEnabled()) {
PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode");
} }
- //NEW string
- //STRCONS_TOK { $kind = CVC4::kind::STRING_CONCAT; }
- //STRREVCONS_TOK { $kind = CVC4::kind::STRING_CONCAT; }
- //STRHEAD_TOK { $kind = CVC4::kind::STRING_CONCAT; }
- //STRTAIL_TOK { $kind = CVC4::kind::STRING_CONCAT; }
- //STRLAST_TOK { $kind = CVC4::kind::STRING_CONCAT; }
- //STRFIRST_TOK { $kind = CVC4::kind::STRING_CONCAT; }
- //OLD string
| STRCON_TOK { $kind = CVC4::kind::STRING_CONCAT; }
| STRLEN_TOK { $kind = CVC4::kind::STRING_LENGTH; }
| STRSUB_TOK { $kind = CVC4::kind::STRING_SUBSTR; }
@@ -1311,12 +1313,6 @@ builtinOp[CVC4::Kind& kind]
| REPLUS_TOK { $kind = CVC4::kind::REGEXP_PLUS; }
| REOPT_TOK { $kind = CVC4::kind::REGEXP_OPT; }
| RERANGE_TOK { $kind = CVC4::kind::REGEXP_RANGE; }
- | SETUNION_TOK { $kind = CVC4::kind::UNION; }
- | SETINT_TOK { $kind = CVC4::kind::INTERSECTION; }
- | SETMINUS_TOK { $kind = CVC4::kind::SETMINUS; }
- | SETSUB_TOK { $kind = CVC4::kind::SUBSET; }
- | SETIN_TOK { $kind = CVC4::kind::MEMBER; }
- | SETSINGLETON_TOK { $kind = CVC4::kind::SET_SINGLETON; }
// NOTE: Theory operators go here
;
@@ -1338,18 +1334,6 @@ functionName[std::string& name, CVC4::parser::DeclarationCheck check]
;
/**
- * Matches an previously declared function symbol (returning an Expr)
- */
-functionSymbol[CVC4::Expr& fun]
-@declarations {
- std::string name;
-}
- : functionName[name,CHECK_DECLARED]
- { PARSER_STATE->checkFunctionLike(name);
- fun = PARSER_STATE->getVariable(name); }
- ;
-
-/**
* Matches a sequence of sort symbols and fills them into the given
* vector.
*/
@@ -1421,12 +1405,14 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
}
| LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK
{
- if(name == "Array") {
+ if(name == "Array" &&
+ PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) ) {
if(args.size() != 2) {
PARSER_STATE->parseError("Illegal array type.");
}
t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
- } else if(name == "Set") {
+ } else if(name == "Set" &&
+ PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) ) {
if(args.size() != 1) {
PARSER_STATE->parseError("Illegal set type.");
}
@@ -1682,15 +1668,6 @@ BVSGE_TOK : 'bvsge';
BV2NAT_TOK : 'bv2nat';
INT2BV_TOK : 'int2bv';
-//STRING
-//NEW
-//STRCONS_TOK : 'str.cons';
-//STRREVCONS_TOK : 'str.revcons';
-//STRHEAD_TOK : 'str.head';
-//STRTAIL_TOK : 'str.tail';
-//STRLAST_TOK : 'str.last';
-//STRFIRST_TOK : 'str.first';
-//OLD
STRCON_TOK : 'str.++';
STRLEN_TOK : 'str.len';
STRSUB_TOK : 'str.substr' ;
@@ -1714,13 +1691,10 @@ RERANGE_TOK : 're.range';
RENOSTR_TOK : 're.nostr';
REALLCHAR_TOK : 're.allchar';
-SETUNION_TOK: 'union';
-SETINT_TOK: 'intersection';
-SETMINUS_TOK: 'setminus';
-SETSUB_TOK: 'subseteq';
-SETIN_TOK: 'in';
-SETSINGLETON_TOK: 'setenum';
-EMPTYSET_TOK: 'emptyset';
+EMPTYSET_TOK: 'emptyset'; // Other set theory operators are not
+ // tokenized and handled directly when
+ // processing a term
+
/**
* A sequence of printable ASCII characters (except backslash) that starts
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback