From 2267c5050fafde26b34dc1e84de015617efa7cc7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 13 Aug 2019 10:08:27 -0500 Subject: Introduce smt2 parsing utility ParseOp and refactor (#3165) --- src/parser/CMakeLists.txt | 1 + src/parser/smt2/Smt2.g | 392 +++------------------------------------------ src/parser/smt2/parse_op.h | 74 +++++++++ src/parser/smt2/smt2.cpp | 349 ++++++++++++++++++++++++++++++++++++++++ src/parser/smt2/smt2.h | 65 +++++++- 5 files changed, 512 insertions(+), 369 deletions(-) create mode 100644 src/parser/smt2/parse_op.h (limited to 'src/parser') diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index 03e194b90..8ac8baf1b 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -41,6 +41,7 @@ set(libcvc4parser_src_files smt1/smt1.h smt1/smt1_input.cpp smt1/smt1_input.h + smt2/parse_op.h smt2/smt2.cpp smt2/smt2.h smt2/smt2_input.cpp diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a5109361b..9e7bc74ee 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -79,8 +79,9 @@ using namespace CVC4::parser; #include -#include "parser/parser.h" #include "parser/antlr_tracing.h" +#include "parser/parser.h" +#include "parser/smt2/parse_op.h" #include "smt/command.h" namespace CVC4 { @@ -1833,42 +1834,15 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] Expr f; std::string name; Type type; + ParseOp p; } : termNonVariable[expr, expr2] // a qualified identifier (section 3.6 of SMT-LIB version 2.6) - | qualIdentifier[kind,name,f,type] + | qualIdentifier[p] { - if (kind != kind::NULL_EXPR || !type.isNull()) - { - PARSER_STATE->parseError( - "Bad syntax for qualified identifier operator in term position."); - } - else if (!f.isNull()) - { - expr = f; - } - else if (!PARSER_STATE->isDeclared(name,SYM_VARIABLE)) - { - if (PARSER_STATE->sygus_v1() && name[0] == '-' - && name.find_first_not_of("0123456789", 1) == std::string::npos) - { - // allow unary minus in sygus version 1 - expr = MK_CONST(Rational(name)); - } - else - { - std::stringstream ss; - ss << "Symbol " << name << " is not declared."; - PARSER_STATE->parseError(ss.str()); - } - } - else - { - expr = PARSER_STATE->getExpressionForName(name); - } - assert(!expr.isNull()); + expr = PARSER_STATE->parseOpToExpr(p); } ; @@ -1881,26 +1855,22 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] @init { Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; Kind kind = kind::NULL_EXPR; - Kind qkind = kind::NULL_EXPR; std::string name; std::vector args; std::vector< std::pair > sortedVarNames; Expr f, f2, f3; - Expr qexpr; - Type qtype; std::string attr; Expr attexpr; std::vector patexprs; std::vector patconds; std::unordered_set names; std::vector< std::pair > binders; - bool isBuiltinOperator = false; - bool isOverloadedFunction = false; int match_vindex = -1; std::vector match_ptypes; Type type; Type type2; api::Term atomTerm; + ParseOp p; } : LPAREN_TOK quantOp[kind] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK @@ -1939,241 +1909,10 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] expr = MK_EXPR(kind, args); } } - | LPAREN_TOK qualIdentifier[qkind,name,qexpr,qtype] - { - // process the operator - Debug("parser") << "Parsed qual id: " << qkind << "/" << name << "/" - << qexpr << "/" << qtype << std::endl; - if (qkind != kind::NULL_EXPR) - { - // It is a special case, e.g. tupSel or array constant specification. - // We have to wait until the arguments are parsed to resolve it. - } - else if (!qexpr.isNull()) - { - // An explicit operator, e.g. an indexed symbol. - args.push_back(qexpr); - if (qexpr.getType().isTester()) - { - kind = kind::APPLY_TESTER; - } - } - else - { - isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name); - if (isBuiltinOperator) - { - // a builtin operator, convert to kind - kind = PARSER_STATE->getOperatorKind(name); - } - else - { - // A non-built-in function application, get the expression - PARSER_STATE->checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE); - expr = PARSER_STATE->getVariable(name); - if (!expr.isNull()) - { - PARSER_STATE->checkFunctionLike(expr); - kind = PARSER_STATE->getKindForFunction(expr); - args.push_back(expr); - } - else - { - // Could not find the expression. It may be an overloaded symbol, - // in which case we may find it after knowing the types of its - // arguments. - isOverloadedFunction = true; - } - } - } - } + | LPAREN_TOK qualIdentifier[p] termList[args,expr] RPAREN_TOK - { Debug("parser") << "args has size " << args.size() << std::endl - << "expr is " << expr << std::endl; - for(std::vector::iterator i = args.begin(); i != args.end(); ++i) { - Debug("parser") << "++ " << *i << std::endl; - } - // We now can figure out what the operator is, if we guessed it was - // overloaded. - if(isOverloadedFunction) { - std::vector< Type > argTypes; - for(std::vector::iterator i = args.begin(); i != args.end(); ++i) { - argTypes.push_back( (*i).getType() ); - } - expr = PARSER_STATE->getOverloadedFunctionForTypes(name, argTypes); - if(!expr.isNull()) { - PARSER_STATE->checkFunctionLike(expr); - kind = PARSER_STATE->getKindForFunction(expr); - args.insert(args.begin(),expr); - }else{ - PARSER_STATE->parseError("Cannot find unambiguous overloaded function for argument types."); - } - } - // handle special cases - if (qkind == kind::STORE_ALL) - { - if (args.size() != 1) - { - PARSER_STATE->parseError("Too many arguments to array constant."); - } - if (!args[0].isConst()) - { - std::stringstream ss; - ss << "expected constant term inside array constant, but found " - << "nonconstant term:" << std::endl - << "the term: " << args[0]; - PARSER_STATE->parseError(ss.str()); - } - ArrayType aqtype = static_cast(qtype); - if (!aqtype.getConstituentType().isComparableTo(args[0].getType())) - { - std::stringstream ss; - ss << "type mismatch inside array constant term:" << std::endl - << "array type: " << qtype << std::endl - << "expected const type: " << aqtype.getConstituentType() - << std::endl - << "computed const type: " << args[0].getType(); - PARSER_STATE->parseError(ss.str()); - } - expr = MK_CONST(CVC4::ArrayStoreAll(qtype, args[0])); - } - else if (qkind == kind::APPLY_SELECTOR) - { - if (qexpr.isNull()) - { - PARSER_STATE->parseError("Could not process parsed tuple selector."); - } - // tuple selector case - Integer x = qexpr.getConst().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(); - expr = dt[0][n].getSelector(); - expr = MK_EXPR(kind::APPLY_SELECTOR, expr, args); - } - else if (qkind != kind::NULL_EXPR) - { - std::stringstream ss; - ss << "Could not process parsed qualified identifier kind " << qkind; - PARSER_STATE->parseError(ss.str()); - } - else if (isBuiltinOperator) - { - bool done = false; - if (args.size() > 2) - { - if (kind == CVC4::kind::INTS_DIVISION || kind == CVC4::kind::XOR - || kind == CVC4::kind::MINUS || kind == CVC4::kind::DIVISION - || (kind == CVC4::kind::BITVECTOR_XNOR && PARSER_STATE->v2_6())) - { - // Builtin operators that are not tokenized, are left associative, - // but not internally variadic must set this. - expr = - EXPR_MANAGER->mkLeftAssociative(kind, args); - done = true; - } - else if (kind == CVC4::kind::IMPLIES) - { - /* right-associative, but CVC4 internally only supports 2 args */ - expr = EXPR_MANAGER->mkRightAssociative(kind, args); - done = true; - } - else if (kind == CVC4::kind::EQUAL || kind == CVC4::kind::LT - || kind == CVC4::kind::GT || kind == CVC4::kind::LEQ - || kind == CVC4::kind::GEQ) - { - /* "chainable", but CVC4 internally only supports 2 args */ - expr = MK_EXPR(MK_CONST(Chain(kind)), args); - done = true; - } - } - - if (!done) - { - if (CVC4::kind::isAssociative(kind) - && args.size() > EXPR_MANAGER->maxArity(kind)) - { - /* Special treatment for associative operators with lots of children - */ - expr = EXPR_MANAGER->mkAssociative(kind, args); - } - else if (!PARSER_STATE->strictModeEnabled() - && (kind == CVC4::kind::AND || kind == CVC4::kind::OR) - && args.size() == 1) - { - /* Unary AND/OR can be replaced with the argument. - * It just so happens expr should already be the only argument. */ - assert(expr == args[0]); - } - else if (kind == CVC4::kind::MINUS && args.size() == 1) - { - expr = MK_EXPR(CVC4::kind::UMINUS, args[0]); - } - else - { - PARSER_STATE->checkOperator(kind, args.size()); - expr = MK_EXPR(kind, args); - } - } - } - else - { - bool done = false; - if (args.size() >= 2) - { - // may be partially applied function, in this case we use HO_APPLY - Type argt = args[0].getType(); - if (argt.isFunction()) - { - unsigned arity = static_cast(argt).getArity(); - if (args.size() - 1 < arity) - { - Debug("parser") << "Partial application of " << args[0]; - Debug("parser") << " : #argTypes = " << arity; - Debug("parser") << ", #args = " << args.size() - 1 << std::endl; - // must curry the partial application - expr = - EXPR_MANAGER->mkLeftAssociative(CVC4::kind::HO_APPLY, args); - done = true; - } - } - } - - if (!done) - { - if (kind == kind::NULL_EXPR) - { - std::vector eargs(args.begin() + 1, args.end()); - expr = MK_EXPR(args[0], eargs); - } - else - { - expr = MK_EXPR(kind, args); - } - } - } + { + expr = PARSER_STATE->applyParseOp(p,args); } | /* a let or sygus let binding */ LPAREN_TOK ( @@ -2422,7 +2161,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] /** * Matches a qualified identifier, which can be a combination of one or more of - * the following: + * the following, stored in the ParseOp utility class: * (1) A kind. * (2) A string name. * (3) An expression expr. @@ -2470,107 +2209,24 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] * expression (3), which may involve disambiguating f based on type T if it is * overloaded. */ -qualIdentifier[CVC4::Kind& kind, std::string& name, CVC4::Expr& expr, CVC4::Type& t] +qualIdentifier[CVC4::ParseOp& p] @init { Kind k; std::string baseName; Expr f; Type type; } -: identifier[kind,name,expr] +: identifier[p] | LPAREN_TOK AS_TOK - ( CONST_TOK sortSymbol[t, CHECK_DECLARED] + ( CONST_TOK sortSymbol[type, CHECK_DECLARED] { - if (!t.isArray()) - { - std::stringstream ss; - ss << "expected array constant term, but cast is not of array type" - << std::endl - << "cast type: " << t; - PARSER_STATE->parseError(ss.str()); - } - kind = kind::STORE_ALL; + p.d_kind = kind::STORE_ALL; + PARSER_STATE->applyTypeAscription(p, type); } - | identifier[k,baseName,f] + | identifier[p] sortSymbol[type, CHECK_DECLARED] { - if (f.isNull()) - { - Trace("parser-overloading") - << "Getting variable expression with name " << baseName - << " and type " << type << std::endl; - // get the variable expression for the type - if (PARSER_STATE->isDeclared(baseName, SYM_VARIABLE)) - { - f = PARSER_STATE->getExpressionForNameAndType(baseName, type); - } - if(f.isNull()) - { - std::stringstream ss; - ss << "Could not resolve expression with name " << baseName - << " and type " << type << std::endl; - PARSER_STATE->parseError(ss.str()); - } - } - Trace("parser-qid") << "Resolve ascription " << type << " on " << f; - Trace("parser-qid") << " " << f.getKind() << " " << f.getType(); - Trace("parser-qid") << std::endl; - // by default, we take f itself - expr = f; - if (f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype()) - { - // nullary constructors with a type ascription - // could be a parametric constructor or just an overloaded constructor - DatatypeType dtype = static_cast(type); - if (dtype.isParametric()) - { - std::vector v; - Expr e = f.getOperator(); - const DatatypeConstructor& dtc = - Datatype::datatypeOf(e)[Datatype::indexOf(e)]; - v.push_back(MK_EXPR(CVC4::kind::APPLY_TYPE_ASCRIPTION, - MK_CONST(AscriptionType( - dtc.getSpecializedConstructorType(type))), - f.getOperator())); - v.insert(v.end(), f.begin(), f.end()); - expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v); - } - } - else if (f.getType().isConstructor()) - { - // a non-nullary constructor with a type ascription - DatatypeType dtype = static_cast(type); - if (dtype.isParametric()) - { - const DatatypeConstructor& dtc = - Datatype::datatypeOf(f)[Datatype::indexOf(f)]; - expr = MK_EXPR(CVC4::kind::APPLY_TYPE_ASCRIPTION, - MK_CONST(AscriptionType( - dtc.getSpecializedConstructorType(type))), - f); - } - } - else if (f.getKind() == CVC4::kind::EMPTYSET) - { - Debug("parser") << "Empty set encountered: " << f << " " << type - << std::endl; - expr = MK_CONST(::CVC4::EmptySet(type)); - } - else if (f.getKind() == CVC4::kind::UNIVERSE_SET) - { - expr = EXPR_MANAGER->mkNullaryOperator(type, kind::UNIVERSE_SET); - } - else if (f.getKind() == CVC4::kind::SEP_NIL) - { - // We don't want the nil reference to be a constant: for instance, it - // could be of type Int but is not a const rational. However, the - // expression has 0 children. So we convert to a SEP_NIL variable. - expr = EXPR_MANAGER->mkNullaryOperator(type, kind::SEP_NIL); - } - else if (f.getType() != type) - { - PARSER_STATE->parseError("Type ascription not satisfied."); - } + PARSER_STATE->applyTypeAscription(p, type); } ) RPAREN_TOK @@ -2578,19 +2234,19 @@ qualIdentifier[CVC4::Kind& kind, std::string& name, CVC4::Expr& expr, CVC4::Type /** * Matches an identifier, which can be a combination of one or more of the - * following: + * following, stored in the ParseOp utility class: * (1) A kind. * (2) A string name. * (3) An expression expr. * For examples, see documentation of qualIdentifier. */ -identifier[CVC4::Kind& kind, std::string& name, CVC4::Expr& expr] +identifier[CVC4::ParseOp& p] @init { Expr f; Expr f2; std::vector numerals; } -: functionName[name, CHECK_NONE] +: functionName[p.d_name, CHECK_NONE] // indexed functions @@ -2607,18 +2263,18 @@ identifier[CVC4::Kind& kind, std::string& name, CVC4::Expr& expr] PARSER_STATE->parseError( "Bad syntax for test (_ is X), X must be a constructor."); } - expr = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getTester(); + p.d_expr = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getTester(); } | TUPLE_SEL_TOK m=INTEGER_LITERAL { // we adopt a special syntax (_ tupSel n) - kind = CVC4::kind::APPLY_SELECTOR; + p.d_kind = CVC4::kind::APPLY_SELECTOR; // put m in expr so that the caller can deal with this case - expr = MK_CONST(Rational(AntlrInput::tokenToUnsigned($m))); + p.d_expr = MK_CONST(Rational(AntlrInput::tokenToUnsigned($m))); } | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals] { - expr = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals) + p.d_expr = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals) .getExpr(); } ) diff --git a/src/parser/smt2/parse_op.h b/src/parser/smt2/parse_op.h new file mode 100644 index 000000000..40b42d0bb --- /dev/null +++ b/src/parser/smt2/parse_op.h @@ -0,0 +1,74 @@ +/********************* */ +/*! \file parse_op.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Definitions of parsed operators in smt2. + **/ + +#include "cvc4parser_private.h" + +#ifndef CVC4__PARSER__SMT2__PARSE_OP_H +#define CVC4__PARSER__SMT2__PARSE_OP_H + +#include + +#include "expr/expr.h" +#include "expr/kind.h" + +namespace CVC4 { + +/** A parsed operator + * + * The purpose of this struct is to store information regarding a parsed term + * in the smt2 language that might not be ready to associate with an + * expression. + * + * While parsing terms in smt2, we may store a combination of one or more of + * the following to track how to process this term: + * (1) A kind. + * (2) A string name. + * (3) An expression expr. + * (4) A type t. + * + * Examples: + * + * - For declared functions f that we have not yet looked up in a symbol table, + * we store (2). We may store a name in a state if f is overloaded and we have + * not yet parsed its arguments to know how to disambiguate f. + * - For tuple selectors (_ tupSel n), we store (1) and (3). Kind is set to + * APPLY_SELECTOR, and expr is set to n, which is to be interpreted by the + * caller as the n^th generic tuple selector. We do this since there is no + * AST expression representing generic tuple select, and we do not have enough + * type information at this point to know the type of the tuple we will be + * selecting from. + * - For array constant specifications prior to type ascription e.g. when we + * have parsed "const", we store (1), setting the kind to STORE_ALL. + * - For array constant specifications (as const (Array T1 T2)), we store (1) + * and (4), where kind is set to STORE_ALL and type is set to (Array T1 T2). + * When parsing this as an operator e.g. ((as const (Array T1 T2)) t), we + * interpret this operator by converting the next parsed constant of type T2 to + * an Array of type (Array T1 T2) over that constant. + */ +struct ParseOp +{ + ParseOp() : d_kind(kind::NULL_EXPR) {} + /** The kind associated with the parsed operator, if it exists */ + Kind d_kind; + /** The name associated with the parsed operator, if it exists */ + std::string d_name; + /** The expression associated with the parsed operator, if it exists */ + Expr d_expr; + /** The type associated with the parsed operator, if it exists */ + Type d_type; +}; + +} // namespace CVC4 + +#endif /* CVC4__PARSER__SMT2__PARSE_OP_H */ diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index d1fb3fe32..346675b6b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1566,6 +1566,355 @@ InputLanguage Smt2::getLanguage() const return em->getOptions().getInputLanguage(); } +void Smt2::applyTypeAscription(ParseOp& p, Type type) +{ + // (as const (Array T1 T2)) + if (p.d_kind == kind::STORE_ALL) + { + if (!type.isArray()) + { + std::stringstream ss; + ss << "expected array constant term, but cast is not of array type" + << std::endl + << "cast type: " << type; + parseError(ss.str()); + } + p.d_type = type; + return; + } + if (p.d_expr.isNull()) + { + Trace("parser-overloading") + << "Getting variable expression with name " << p.d_name << " and type " + << type << std::endl; + // get the variable expression for the type + if (isDeclared(p.d_name, SYM_VARIABLE)) + { + p.d_expr = getExpressionForNameAndType(p.d_name, type); + } + if (p.d_expr.isNull()) + { + std::stringstream ss; + ss << "Could not resolve expression with name " << p.d_name + << " and type " << type << std::endl; + parseError(ss.str()); + } + } + ExprManager* em = getExprManager(); + Type etype = p.d_expr.getType(); + Kind ekind = p.d_expr.getKind(); + Trace("parser-qid") << "Resolve ascription " << type << " on " << p.d_expr; + Trace("parser-qid") << " " << ekind << " " << etype; + Trace("parser-qid") << std::endl; + if (ekind == kind::APPLY_CONSTRUCTOR && type.isDatatype()) + { + // nullary constructors with a type ascription + // could be a parametric constructor or just an overloaded constructor + DatatypeType dtype = static_cast(type); + if (dtype.isParametric()) + { + std::vector v; + Expr e = p.d_expr.getOperator(); + const DatatypeConstructor& dtc = + Datatype::datatypeOf(e)[Datatype::indexOf(e)]; + v.push_back(em->mkExpr( + kind::APPLY_TYPE_ASCRIPTION, + em->mkConst(AscriptionType(dtc.getSpecializedConstructorType(type))), + p.d_expr.getOperator())); + v.insert(v.end(), p.d_expr.begin(), p.d_expr.end()); + p.d_expr = em->mkExpr(kind::APPLY_CONSTRUCTOR, v); + } + } + else if (etype.isConstructor()) + { + // a non-nullary constructor with a type ascription + DatatypeType dtype = static_cast(type); + if (dtype.isParametric()) + { + const DatatypeConstructor& dtc = + Datatype::datatypeOf(p.d_expr)[Datatype::indexOf(p.d_expr)]; + p.d_expr = em->mkExpr( + kind::APPLY_TYPE_ASCRIPTION, + em->mkConst(AscriptionType(dtc.getSpecializedConstructorType(type))), + p.d_expr); + } + } + else if (ekind == kind::EMPTYSET) + { + Debug("parser") << "Empty set encountered: " << p.d_expr << " " << type + << std::endl; + p.d_expr = em->mkConst(EmptySet(type)); + } + else if (ekind == kind::UNIVERSE_SET) + { + p.d_expr = em->mkNullaryOperator(type, kind::UNIVERSE_SET); + } + else if (ekind == kind::SEP_NIL) + { + // We don't want the nil reference to be a constant: for instance, it + // could be of type Int but is not a const rational. However, the + // expression has 0 children. So we convert to a SEP_NIL variable. + p.d_expr = em->mkNullaryOperator(type, kind::SEP_NIL); + } + else if (etype != type) + { + parseError("Type ascription not satisfied."); + } +} + +Expr Smt2::parseOpToExpr(ParseOp& p) +{ + Expr expr; + if (p.d_kind != kind::NULL_EXPR || !p.d_type.isNull()) + { + parseError( + "Bad syntax for qualified identifier operator in term position."); + } + else if (!p.d_expr.isNull()) + { + expr = p.d_expr; + } + else if (!isDeclared(p.d_name, SYM_VARIABLE)) + { + if (sygus_v1() && p.d_name[0] == '-' + && p.d_name.find_first_not_of("0123456789", 1) == std::string::npos) + { + // allow unary minus in sygus version 1 + expr = getExprManager()->mkConst(Rational(p.d_name)); + } + else + { + std::stringstream ss; + ss << "Symbol " << p.d_name << " is not declared."; + parseError(ss.str()); + } + } + else + { + expr = getExpressionForName(p.d_name); + } + assert(!expr.isNull()); + return expr; +} + +Expr Smt2::applyParseOp(ParseOp& p, std::vector& args) +{ + bool isBuiltinOperator = false; + // the builtin kind of the overall return expression + Kind kind = kind::NULL_EXPR; + // First phase: process the operator + if (Debug.isOn("parser")) + { + Debug("parser") << "Apply parse op to:" << std::endl; + Debug("parser") << "args has size " << args.size() << std::endl; + for (std::vector::iterator i = args.begin(); i != args.end(); ++i) + { + Debug("parser") << "++ " << *i << std::endl; + } + } + if (p.d_kind != kind::NULL_EXPR) + { + // It is a special case, e.g. tupSel or array constant specification. + // We have to wait until the arguments are parsed to resolve it. + } + else if (!p.d_expr.isNull()) + { + // An explicit operator, e.g. an indexed symbol. + args.insert(args.begin(), p.d_expr); + if (p.d_expr.getType().isTester()) + { + // Testers are handled differently than other indexed operators, + // since they require a kind. + kind = kind::APPLY_TESTER; + } + } + else + { + isBuiltinOperator = isOperatorEnabled(p.d_name); + if (isBuiltinOperator) + { + // a builtin operator, convert to kind + kind = getOperatorKind(p.d_name); + } + else + { + // A non-built-in function application, get the expression + checkDeclaration(p.d_name, CHECK_DECLARED, SYM_VARIABLE); + Expr v = getVariable(p.d_name); + if (!v.isNull()) + { + checkFunctionLike(v); + kind = getKindForFunction(v); + args.insert(args.begin(), v); + } + else + { + // Overloaded symbol? + // Could not find the expression. It may be an overloaded symbol, + // in which case we may find it after knowing the types of its + // arguments. + std::vector argTypes; + for (std::vector::iterator i = args.begin(); i != args.end(); ++i) + { + argTypes.push_back((*i).getType()); + } + Expr op = getOverloadedFunctionForTypes(p.d_name, argTypes); + if (!op.isNull()) + { + checkFunctionLike(op); + kind = getKindForFunction(op); + args.insert(args.begin(), op); + } + else + { + parseError( + "Cannot find unambiguous overloaded function for argument " + "types."); + } + } + } + } + + // Second phase: apply the arguments to the parse op + ExprManager* em = getExprManager(); + // handle special cases + if (p.d_kind == kind::STORE_ALL) + { + if (args.size() != 1) + { + parseError("Too many arguments to array constant."); + } + if (!args[0].isConst()) + { + std::stringstream ss; + ss << "expected constant term inside array constant, but found " + << "nonconstant term:" << std::endl + << "the term: " << args[0]; + parseError(ss.str()); + } + ArrayType aqtype = static_cast(p.d_type); + if (!aqtype.getConstituentType().isComparableTo(args[0].getType())) + { + std::stringstream ss; + ss << "type mismatch inside array constant term:" << std::endl + << "array type: " << p.d_type << std::endl + << "expected const type: " << aqtype.getConstituentType() << std::endl + << "computed const type: " << args[0].getType(); + parseError(ss.str()); + } + return em->mkConst(ArrayStoreAll(p.d_type, args[0])); + } + else if (p.d_kind == kind::APPLY_SELECTOR) + { + if (p.d_expr.isNull()) + { + parseError("Could not process parsed tuple selector."); + } + // tuple selector case + Integer x = p.d_expr.getConst().getNumerator(); + if (!x.fitsUnsignedInt()) + { + parseError("index of tupSel is larger than size of unsigned int"); + } + unsigned int n = x.toUnsignedInt(); + if (args.size() > 1) + { + parseError("tupSel applied to more than one tuple argument"); + } + Type t = args[0].getType(); + if (!t.isTuple()) + { + 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; + parseError(ss.str()); + } + const Datatype& dt = ((DatatypeType)t).getDatatype(); + return em->mkExpr(kind::APPLY_SELECTOR, dt[0][n].getSelector(), args); + } + else if (p.d_kind != kind::NULL_EXPR) + { + std::stringstream ss; + ss << "Could not process parsed qualified identifier kind " << p.d_kind; + parseError(ss.str()); + } + else if (isBuiltinOperator) + { + if (args.size() > 2) + { + if (kind == kind::INTS_DIVISION || kind == kind::XOR + || kind == kind::MINUS || kind == kind::DIVISION + || (kind == kind::BITVECTOR_XNOR && v2_6())) + { + // Builtin operators that are not tokenized, are left associative, + // but not internally variadic must set this. + return em->mkLeftAssociative(kind, args); + } + else if (kind == kind::IMPLIES) + { + /* right-associative, but CVC4 internally only supports 2 args */ + return em->mkRightAssociative(kind, args); + } + else if (kind == kind::EQUAL || kind == kind::LT || kind == kind::GT + || kind == kind::LEQ || kind == kind::GEQ) + { + /* "chainable", but CVC4 internally only supports 2 args */ + return em->mkExpr(em->mkConst(Chain(kind)), args); + } + } + + if (kind::isAssociative(kind) && args.size() > em->maxArity(kind)) + { + /* Special treatment for associative operators with lots of children + */ + return em->mkAssociative(kind, args); + } + else if (!strictModeEnabled() && (kind == kind::AND || kind == kind::OR) + && args.size() == 1) + { + // Unary AND/OR can be replaced with the argument. + return args[0]; + } + else if (kind == kind::MINUS && args.size() == 1) + { + return em->mkExpr(kind::UMINUS, args[0]); + } + else + { + checkOperator(kind, args.size()); + return em->mkExpr(kind, args); + } + } + + if (args.size() >= 2) + { + // may be partially applied function, in this case we use HO_APPLY + Type argt = args[0].getType(); + if (argt.isFunction()) + { + unsigned arity = static_cast(argt).getArity(); + if (args.size() - 1 < arity) + { + Debug("parser") << "Partial application of " << args[0]; + Debug("parser") << " : #argTypes = " << arity; + Debug("parser") << ", #args = " << args.size() - 1 << std::endl; + // must curry the partial application + return em->mkLeftAssociative(kind::HO_APPLY, args); + } + } + } + if (kind == kind::NULL_EXPR) + { + std::vector eargs(args.begin() + 1, args.end()); + return em->mkExpr(args[0], eargs); + } + return em->mkExpr(kind, args); +} + Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr) { if (!sexpr.isKeyword()) diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 669104954..7c7f290a5 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -28,6 +28,7 @@ #include "api/cvc4cpp.h" #include "parser/parser.h" #include "parser/smt1/smt1.h" +#include "parser/smt2/parse_op.h" #include "smt/command.h" #include "theory/logic_info.h" #include "util/abstract_value.h" @@ -444,7 +445,69 @@ class Smt2 : public Parser parseError(withLogic); } -private: + //------------------------- processing parse operators + /** + * Given a parse operator p, apply a type ascription to it. This method is run + * when we encounter "(as t type)" and information regarding t has been stored + * in p. + * + * This updates p to take into account the ascription. This may include: + * - Converting an (pre-ascribed) array constant specification "const" to + * an ascribed array constant specification (as const type) where type is + * (Array T1 T2) for some T1, T2. + * - Converting a (nullary or non-nullary) parametric datatype constructor to + * the specialized constructor for the given type. + * - Converting an empty set, universe set, or separation nil reference to + * the respective term of the given type. + * - If p's expression field is set, then we leave p unchanged, check if + * that expression has the given type and throw a parse error otherwise. + */ + void applyTypeAscription(ParseOp& p, Type type); + /** + * This converts a ParseOp to expression, assuming it is a standalone term. + * + * In particular: + * - If p's expression field is set, then that expression is returned. + * - If p's name field is set, then we look up that name in the symbol table + * of this class. + * In other cases, a parse error is thrown. + */ + Expr parseOpToExpr(ParseOp& p); + /** + * Apply parse operator to list of arguments, and return the resulting + * expression. + * + * This method involves two phases. + * (1) Processing the operator represented by p, + * (2) Applying that operator to the set of arguments. + * + * For (1), this involves determining the kind of the overall expression. We + * may be in one the following cases: + * - If p's expression field is set, we may choose to prepend it to args, or + * otherwise determine the appropriate kind of the overall expression based on + * this expression. + * - If p's name field is set, then we get the appropriate symbol for that + * name, which may involve disambiguating that name if it is overloaded based + * on the types of args. We then determine the overall kind of the return + * expression based on that symbol. + * - p's kind field may be already set. + * + * For (2), we construct the overall expression, which may involve the + * following: + * - If p is an array constant specification (as const (Array T1 T2)), then + * we return the appropriate array constant based on args[0]. + * - If p represents a tuple selector, then we infer the appropriate tuple + * selector expression based on the type of args[0]. + * - If the overall kind of the expression is chainable, we may convert it + * to a left- or right-associative chain. + * - If the overall kind is MINUS and args has size 1, then we return an + * application of UMINUS. + * - If the overall expression is a partial application, then we process this + * as a chain of HO_APPLY terms. + */ + Expr applyParseOp(ParseOp& p, std::vector& args); + //------------------------- end processing parse operators + private: std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type; std::map< CVC4::Expr, std::vector< CVC4::Expr > > d_sygus_let_func_to_vars; std::map< CVC4::Expr, CVC4::Expr > d_sygus_let_func_to_body; -- cgit v1.2.3