diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-26 00:40:52 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-26 00:40:52 -0600 |
| commit | b28ff31b6713791f27b4860f439aaa3f63aab9d7 (patch) | |
| tree | 3b525d947ecae5e3d52e0cc9160962c09684310b /src/parser/smt2/Smt2.g | |
| parent | 808bb1bd855799535a1b690865dc873793a37f7f (diff) | |
Minor cleaning of smt2 parser (#3823)
Towards parser migration, will make the diff of the eventual conversion a bit smaller.
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 27 |
1 files changed, 0 insertions, 27 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e1f8031da..66831c0c4 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1536,16 +1536,6 @@ datatypesDef[bool isCo, } ; -pattern[CVC4::Expr& expr] -@declarations { - std::vector<Expr> patexpr; -} - : LPAREN_TOK termList[patexpr,expr] RPAREN_TOK - { - expr = MK_EXPR(kind::INST_PATTERN, patexpr); - } - ; - simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] @declarations { CVC4::Kind k; @@ -1568,13 +1558,6 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] } | str[s,false] { sexpr = SExpr(s); } -// | LPAREN_TOK STRCST_TOK -// ( INTEGER_LITERAL { -// s_vec.push_back( atoi( AntlrInput::tokenText($INTEGER_LITERAL) ) + 65 ); -// } )* RPAREN_TOK -// { -// sexpr = SExpr( MK_CONST( ::CVC4::String(s_vec) ) ); -// } | symbol[s,CHECK_NONE,SYM_SORT] { sexpr = SExpr(SExpr::Keyword(s)); } | tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK @@ -2512,15 +2495,6 @@ datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes, * "defined" as an unresolved type; don't worry, we check * below. */ : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); } - /* ( '[' symbol[id2,CHECK_UNDECLARED,SYM_SORT] { - t = PARSER_STATE->mkSort(id2); - params.push_back( t ); - } - ( symbol[id2,CHECK_UNDECLARED,SYM_SORT] { - t = PARSER_STATE->mkSort(id2); - params.push_back( t ); } - )* ']' - )?*/ //AJR: this isn't necessary if we use z3's style { datatypes.push_back(Datatype(EXPR_MANAGER, id, params, isCo)); if(!PARSER_STATE->isUnresolvedType(id)) { // if not unresolved, must be undeclared @@ -2649,7 +2623,6 @@ ATTRIBUTE_PATTERN_TOK : ':pattern'; ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern'; ATTRIBUTE_NAMED_TOK : ':named'; ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level'; -ATTRIBUTE_RR_PRIORITY : ':rr-priority'; // operators (NOTE: theory symbols go here) EXISTS_TOK : 'exists'; |