diff options
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 69 |
1 files changed, 28 insertions, 41 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 88035dba4..6eb3d8061 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -722,29 +722,27 @@ sygusGrammar[CVC4::api::Grammar*& ret, setInfoInternal[std::unique_ptr<CVC4::Command>* cmd] @declarations { std::string name; - SExpr sexpr; + api::Term sexpr; } : KEYWORD symbolicExpr[sexpr] { name = AntlrInput::tokenText($KEYWORD); - PARSER_STATE->setInfo(name.c_str() + 1, sexpr); - cmd->reset(new SetInfoCommand(name.c_str() + 1, sexpr)); + cmd->reset(new SetInfoCommand(name.c_str() + 1, sexprToString(sexpr))); } ; setOptionInternal[std::unique_ptr<CVC4::Command>* cmd] @init { std::string name; - SExpr sexpr; + api::Term sexpr; } : keyword[name] symbolicExpr[sexpr] - { PARSER_STATE->setOption(name.c_str() + 1, sexpr); - cmd->reset(new SetOptionCommand(name.c_str() + 1, sexpr)); + { cmd->reset(new SetOptionCommand(name.c_str() + 1, sexprToString(sexpr))); // Ugly that this changes the state of the parser; but // global-declarations affects parsing, so we can't hold off // on this until some SmtEngine eventually (if ever) executes it. if(name == ":global-declarations") { - SYM_MAN->setGlobalDeclarations(sexpr.getValue() == "true"); + SYM_MAN->setGlobalDeclarations(sexprToString(sexpr) == "true"); } } ; @@ -755,7 +753,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] std::string fname; CVC4::api::Term expr, expr2; std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames; - SExpr sexpr; + std::string s; CVC4::api::Sort t; CVC4::api::Term func; std::vector<CVC4::api::Term> bvs; @@ -786,8 +784,8 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd] /* echo */ | ECHO_TOK - ( simpleSymbolicExpr[sexpr] - { cmd->reset(new EchoCommand(sexpr.toString())); } + ( simpleSymbolicExpr[s] + { cmd->reset(new EchoCommand(s)); } | { cmd->reset(new EchoCommand()); } ) @@ -1246,30 +1244,17 @@ datatypesDef[bool isCo, } ; -simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] -@declarations { - CVC4::Kind k; - std::string s; - std::vector<unsigned int> s_vec; -} +simpleSymbolicExprNoKeyword[std::string& s] : INTEGER_LITERAL - { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); } + { s = AntlrInput::tokenText($INTEGER_LITERAL); } | DECIMAL_LITERAL - { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); } + { s = AntlrInput::tokenText($DECIMAL_LITERAL); } | HEX_LITERAL - { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); - std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); - sexpr = SExpr(Integer(hexString, 16)); - } + { s = AntlrInput::tokenText($HEX_LITERAL); } | BINARY_LITERAL - { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); - std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); - sexpr = SExpr(Integer(binString, 2)); - } + { s = AntlrInput::tokenText($BINARY_LITERAL); } | str[s,false] - { sexpr = SExpr(s); } | symbol[s,CHECK_NONE,SYM_SORT] - { sexpr = SExpr(SExpr::Keyword(s)); } | tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK @@ -1279,7 +1264,7 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | SIMPLIFY_TOK) - { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); } + { s = AntlrInput::tokenText($tok); } ; keyword[std::string& s] @@ -1287,20 +1272,21 @@ keyword[std::string& s] { s = AntlrInput::tokenText($KEYWORD); } ; -simpleSymbolicExpr[CVC4::SExpr& sexpr] - : simpleSymbolicExprNoKeyword[sexpr] - | KEYWORD - { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); } +simpleSymbolicExpr[std::string& s] + : simpleSymbolicExprNoKeyword[s] + | KEYWORD { s = AntlrInput::tokenText($KEYWORD); } ; -symbolicExpr[CVC4::SExpr& sexpr] +symbolicExpr[CVC4::api::Term& sexpr] @declarations { - std::vector<SExpr> children; + std::string s; + std::vector<api::Term> children; } - : simpleSymbolicExpr[sexpr] + : simpleSymbolicExpr[s] + { sexpr = SOLVER->mkString(PARSER_STATE->processAdHocStringEsc(s)); } | LPAREN_TOK ( symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK - { sexpr = SExpr(children); } + { sexpr = SOLVER->mkTerm(CVC4::api::SEXPR, children); } ; /** @@ -1781,13 +1767,14 @@ termAtomic[CVC4::api::Term& atomTerm] */ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] @init { - SExpr sexpr; + api::Term sexpr; + std::string s; CVC4::api::Term patexpr; std::vector<CVC4::api::Term> patexprs; CVC4::api::Term e2; bool hasValue = false; } - : KEYWORD ( simpleSymbolicExprNoKeyword[sexpr] { hasValue = true; } )? + : KEYWORD ( simpleSymbolicExprNoKeyword[s] { hasValue = true; } )? { attr = AntlrInput::tokenText($KEYWORD); PARSER_STATE->attributeNotSupported(attr); @@ -1824,7 +1811,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbolicExpr[sexpr] { api::Sort boolType = SOLVER->getBooleanSort(); - api::Term avar = SOLVER->mkConst(boolType, sexpr.toString()); + api::Term avar = SOLVER->mkConst(boolType, sexprToString(sexpr)); attr = std::string(":qid"); retExpr = MK_TERM(api::INST_ATTRIBUTE, avar); Command* c = new SetUserAttributeCommand("qid", avar); @@ -1835,7 +1822,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr] { attr = std::string(":named"); // notify that expression was given a name - PARSER_STATE->notifyNamedExpression(expr, sexpr.getValue()); + PARSER_STATE->notifyNamedExpression(expr, sexprToString(sexpr)); } ; |