/**
* Matches a term.
- * @return the expression representing the formula
+ * @return the expression representing the term.
*/
term[CVC4::Expr& expr, CVC4::Expr& expr2]
@init {
+ Kind kind = kind::NULL_EXPR;
+ Expr f;
std::string name;
+ Type type;
}
: termNonVariable[expr, expr2]
- /* a variable */
- | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
- { expr = PARSER_STATE->getExpressionForName(name);
- assert( !expr.isNull() );
+
+ // a qualified identifier (section 3.6 of SMT-LIB version 2.6)
+
+ | qualIdentifier[kind,name,f,type]
+ {
+ 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());
}
;
@init {
Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
Kind kind = kind::NULL_EXPR;
- Expr op;
+ Kind qkind = kind::NULL_EXPR;
std::string name;
std::vector<Expr> args;
std::vector< std::pair<std::string, Type> > sortedVarNames;
Expr f, f2, f3;
+ Expr qexpr;
+ Type qtype;
std::string attr;
Expr attexpr;
std::vector<Expr> patexprs;
std::vector< std::pair<std::string, Expr> > binders;
bool isBuiltinOperator = false;
bool isOverloadedFunction = false;
- bool readVariable = false;
int match_vindex = -1;
std::vector<Type> match_ptypes;
Type type;
Type type2;
api::Term atomTerm;
}
- : LPAREN_TOK AS_TOK ( termNonVariable[f, f2] | symbol[name,CHECK_DECLARED,SYM_VARIABLE] { readVariable = true; } )
- sortSymbol[type, CHECK_DECLARED] RPAREN_TOK
- {
- if(readVariable) {
- Trace("parser-overloading") << "Getting variable expression of type " << name << " with type " << type << std::endl;
- // get the variable expression for the type
- f = PARSER_STATE->getExpressionForNameAndType(name, type);
- assert( !f.isNull() );
- }
- if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype()) {
- // could be a parametric type constructor or just an overloaded constructor
- if(((DatatypeType)type).isParametric()) {
- std::vector<CVC4::Expr> 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{
- expr = f;
- }
- } else if(f.getKind() == CVC4::kind::EMPTYSET) {
- Debug("parser") << "Empty set encountered: " << f << " "
- << f2 << " " << 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.");
- }else{
- expr = f;
- }
- }
- }
- | LPAREN_TOK quantOp[kind]
+ : LPAREN_TOK quantOp[kind]
LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
{
PARSER_STATE->pushScope(true);
expr = MK_EXPR(kind, args);
}
}
- | LPAREN_TOK functionName[name, CHECK_NONE]
- { isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
- if(isBuiltinOperator) {
- /* A built-in operator */
- kind = PARSER_STATE->getOperatorKind(name);
- } else {
- /* A non-built-in function application */
- 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{
- isOverloadedFunction = true;
+ | 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;
+ }
}
}
}
- //(termList[args,expr])? RPAREN_TOK
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) {
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<Expr>::iterator i = args.begin(); i != args.end(); ++i) {
PARSER_STATE->parseError("Cannot find unambiguous overloaded function for argument types.");
}
}
-
- bool done = false;
- if (isBuiltinOperator)
+ // 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<ArrayType>(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<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();
+ 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
}
else
{
+ bool done = false;
if (args.size() >= 2)
{
// may be partially applied function, in this case we use HO_APPLY
if (!done)
{
- expr = MK_EXPR(kind, args);
- }
- }
- }
- | LPAREN_TOK
- ( /* An indexed function application */
- 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");
+ if (kind == kind::NULL_EXPR)
+ {
+ std::vector<Expr> eargs(args.begin() + 1, args.end());
+ expr = MK_EXPR(args[0], eargs);
}
- 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());
+ else
+ {
+ expr = MK_EXPR(kind, args);
}
- const Datatype & dt = ((DatatypeType)t).getDatatype();
- op = dt[0][n].getSelector();
}
- if (kind!=kind::NULL_EXPR) {
- expr = MK_EXPR( kind, op, args );
- } else {
- expr = MK_EXPR(op, args);
- }
- PARSER_STATE->checkOperator(expr.getKind(), args.size());
}
- | /* Array constant (in Z3 syntax) */
- LPAREN_TOK AS_TOK CONST_TOK sortSymbol[type, CHECK_DECLARED]
- RPAREN_TOK term[f, f2] RPAREN_TOK
- {
- if(!type.isArray()) {
- std::stringstream ss;
- ss << "expected array constant term, but cast is not of array type"
- << std::endl
- << "cast type: " << type;
- PARSER_STATE->parseError(ss.str());
- }
- if(!f.isConst()) {
- std::stringstream ss;
- ss << "expected constant term inside array constant, but found "
- << "nonconstant term:" << std::endl
- << "the term: " << f;
- PARSER_STATE->parseError(ss.str());
- }
- if(!ArrayType(type).getConstituentType().isComparableTo(f.getType())) {
- std::stringstream ss;
- ss << "type mismatch inside array constant term:" << std::endl
- << "array type: " << type << std::endl
- << "expected const type: " << ArrayType(type).getConstituentType()
- << std::endl
- << "computed const type: " << f.getType();
- PARSER_STATE->parseError(ss.str());
- }
- expr = MK_CONST( ::CVC4::ArrayStoreAll(type, f) );
- }
- )
+ }
| /* a let or sygus let binding */
LPAREN_TOK (
LET_TOK LPAREN_TOK
PARSER_STATE->popScope();
expr = MK_EXPR( CVC4::kind::LAMBDA, args );
}
-
| LPAREN_TOK TUPLE_CONST_TOK termList[args,expr] RPAREN_TOK
{
std::vector<api::Sort> sorts;
;
+/**
+ * Matches a qualified identifier, which can be a combination of one or more of
+ * the following:
+ * (1) A kind.
+ * (2) A string name.
+ * (3) An expression expr.
+ * (4) A type t.
+ *
+ * A qualified identifier is the generic case of function heads.
+ * With respect to the standard definition (Section 3.6 of SMT-LIB version 2.6)
+ * of qualified identifiers, we additionally parse:
+ * - "Array constant specifications" of the form (as const (Array T1 T2)),
+ * which notice are used as function heads e.g. ((as const (Array Int Int)) 0)
+ * specifies the constant array over integers consisting of constant 0. This
+ * is handled as if it were a special case of an operator here.
+ *
+ * Examples:
+ *
+ * (Identifiers)
+ *
+ * - For declared functions f, we return (2).
+ * - For indexed functions like testers (_ is C) and bitvector extract
+ * (_ extract n m), we return (3) for the appropriate operator.
+ * - For tuple selectors (_ tupSel n), we return (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.
+ *
+ * (Ascripted Identifiers)
+ *
+ * - For ascripted nullary parametric datatype constructors like
+ * (as nil (List Int)), we return (APPLY_CONSTRUCTOR C) for the appropriate
+ * specialized constructor C as (3).
+ * - For ascripted non-nullary parametric datatype constructors like
+ * (as cons (List Int)), we return the appropriate specialized constructor C
+ * as (3).
+ * - Overloaded non-parametric constructors (as C T) return the appropriate
+ * expression, analogous to the parametric cases above.
+ * - For other ascripted nullary constants like (as emptyset (Set T)),
+ * (as sep.nil T), we return the appropriate expression (3).
+ * - For array constant specifications (as const (Array T1 T2)), we return (1)
+ * and (4), where kind is set to STORE_ALL and type is set to (Array T1 T2),
+ * where this is to be interpreted by the caller as converting the next parsed
+ * constant of type T2 to an Array of type (Array T1 T2) over that constant.
+ * - For ascriptions on normal symbols (as f T), we return the appropriate
+ * 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]
+@init {
+ Kind k;
+ std::string baseName;
+ Expr f;
+ Type type;
+}
+: identifier[kind,name,expr]
+ | LPAREN_TOK AS_TOK
+ ( CONST_TOK sortSymbol[t, 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;
+ }
+ | identifier[k,baseName,f]
+ 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<DatatypeType>(type);
+ if (dtype.isParametric())
+ {
+ std::vector<CVC4::Expr> 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<DatatypeType>(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.");
+ }
+ }
+ )
+ RPAREN_TOK
+ ;
+
+/**
+ * Matches an identifier, which can be a combination of one or more of the
+ * following:
+ * (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]
+@init {
+ Expr f;
+ Expr f2;
+ std::vector<uint64_t> numerals;
+}
+: functionName[name, CHECK_NONE]
+
+ // indexed functions
+
+ | LPAREN_TOK INDEX_TOK
+ ( TESTER_TOK term[f, f2]
+ {
+ if (f.getKind() == kind::APPLY_CONSTRUCTOR && f.getNumChildren() == 0)
+ {
+ // for nullary constructors, must get the operator
+ f = f.getOperator();
+ }
+ if (!f.getType().isConstructor())
+ {
+ PARSER_STATE->parseError(
+ "Bad syntax for test (_ is X), X must be a constructor.");
+ }
+ 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;
+ // put m in expr so that the caller can deal with this case
+ expr = MK_CONST(Rational(AntlrInput::tokenToUnsigned($m)));
+ }
+ | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
+ {
+ expr = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals)
+ .getExpr();
+ }
+ )
+ RPAREN_TOK
+ ;
+
/**
* Matches an atomic term (a term with no subterms).
* @return the expression expr representing the term or formula.
}
;
-/**
- * Matches a bit-vector operator (the ones parametrized by numbers)
- */
-indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind]
-@init {
- Expr expr;
- Expr expr2;
- std::vector<uint64_t> numerals;
-}
- : LPAREN_TOK INDEX_TOK
- ( TESTER_TOK term[expr, expr2] {
- if( expr.getKind()==kind::APPLY_CONSTRUCTOR && expr.getNumChildren()==0 ){
- //for nullary constructors, must get the operator
- expr = expr.getOperator();
- }
- if( !expr.getType().isConstructor() ){
- PARSER_STATE->parseError("Bad syntax for test (_ is X), X must be a constructor.");
- }
- 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)));
- }
- | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
- {
- op = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals)
- .getExpr();
- }
- )
- RPAREN_TOK
- ;
-
/**
* Matches a sequence of terms and puts them into the formulas
* vector.
projects / cvc5.git / commitdiff