diff options
author | Arjun Viswanathan <arjun-viswanathan@uiowa.edu> | 2017-12-27 21:43:35 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-27 21:43:35 -0600 |
commit | 2731897b5f9ed46c66e3bdf20cde47ef43923a9c (patch) | |
tree | a95d36fdeb9c6a0d5dbc41ef4dc7bafdcb6e81b3 /src/parser/smt2 | |
parent | 3b7f04092f55b263b1f89fa2c2517821013ff5fe (diff) |
Rel smt parser (#1446)
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 58 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 8 |
2 files changed, 62 insertions, 4 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 81f62ccf4..d424fefad 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1980,11 +1980,33 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] | LPAREN_TOK ( /* An indexed function application */ - indexedFunctionName[op, kind] termList[args,expr] RPAREN_TOK - { - if( kind!=kind::NULL_EXPR ){ + indexedFunctionName[op, kind] termList[args,expr] RPAREN_TOK { + if(kind==CVC4::kind::APPLY_SELECTOR) { + //tuple selector case + Integer x = op.getConst<CVC4::Rational>().getNumerator(); + if (!x.fitsUnsignedInt()) { + PARSER_STATE->parseError("index of tupSel is larger than size of unsigned int"); + } + unsigned int n = x.toUnsignedInt(); + if (args.size()>1) { + PARSER_STATE->parseError("tupSel applied to more than one tuple argument"); + } + Type t = args[0].getType(); + if (!t.isTuple()) { + PARSER_STATE->parseError("tupSel applied to non-tuple"); + } + size_t length = ((DatatypeType)t).getTupleLength(); + if (n >= length) { + std::stringstream ss; + ss << "tuple is of length " << length << "; cannot access index " << n; + PARSER_STATE->parseError(ss.str()); + } + const Datatype & dt = ((DatatypeType)t).getDatatype(); + op = dt[0][n].getSelector(); + } + if (kind!=kind::NULL_EXPR) { expr = MK_EXPR( kind, op, args ); - }else{ + } else { expr = MK_EXPR(op, args); } PARSER_STATE->checkOperator(expr.getKind(), args.size()); @@ -2347,6 +2369,25 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] { //booleanType is placeholder here since we don't have type info without type annotation expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::SEP_NIL); } // NOTE: Theory constants go here + + | LPAREN_TOK TUPLE_CONST_TOK termList[args,expr] RPAREN_TOK + { std::vector<Type> types; + for(std::vector<Expr>::const_iterator i = args.begin(); i != args.end(); ++i) { + types.push_back((*i).getType()); + } + DatatypeType t = EXPR_MANAGER->mkTupleType(types); + const Datatype& dt = t.getDatatype(); + args.insert(args.begin(), dt[0].getConstructor()); + expr = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); + } + + | TUPLE_CONST_TOK + { std::vector<Type> types; + DatatypeType t = EXPR_MANAGER->mkTupleType(types); + const Datatype& dt = t.getDatatype(); + args.insert(args.begin(), dt[0].getConstructor()); + expr = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); + } ; /** @@ -2565,6 +2606,11 @@ indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind] op = Datatype::datatypeOf(expr)[Datatype::indexOf(expr)].getTester(); kind = CVC4::kind::APPLY_TESTER; } + | TUPLE_SEL_TOK m=INTEGER_LITERAL { + kind = CVC4::kind::APPLY_SELECTOR; + //put m in op so that the caller (termNonVariable) can deal with this case + op = MK_CONST(Rational(AntlrInput::tokenToUnsigned($m))); + } | badIndexedFunctionName ) RPAREN_TOK @@ -2843,6 +2889,8 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] PARSER_STATE->parseError("Illegal set type."); } t = EXPR_MANAGER->mkSetType( args[0] ); + } else if(name == "Tuple") { + t = EXPR_MANAGER->mkTupleType(args); } else if(check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT)) { t = PARSER_STATE->getSort(name, args); @@ -3137,6 +3185,8 @@ INST_CLOSURE_TOK : 'inst-closure'; EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset'; UNIVSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'univset'; NILREF_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'sep.nil'; +TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }? 'mkTuple'; +TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }? 'tupSel'; // Other set theory operators are not // tokenized and handled directly when // processing a term diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 381a60fa8..e4f6569b8 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -240,14 +240,22 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::INSERT, "insert"); addOperator(kind::CARD, "card"); addOperator(kind::COMPLEMENT, "complement"); + addOperator(kind::JOIN, "join"); + addOperator(kind::PRODUCT, "product"); + addOperator(kind::TRANSPOSE, "transpose"); + addOperator(kind::TCLOSURE, "tclosure"); break; case THEORY_DATATYPES: + { + const std::vector<Type> types; + defineType("Tuple", getExprManager()->mkTupleType(types)); Parser::addOperator(kind::APPLY_CONSTRUCTOR); Parser::addOperator(kind::APPLY_TESTER); Parser::addOperator(kind::APPLY_SELECTOR); Parser::addOperator(kind::APPLY_SELECTOR_TOTAL); break; + } case THEORY_STRINGS: defineType("String", getExprManager()->stringType()); |