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
#include <memory>
-#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 {
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);
}
;
@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<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<Expr> patconds;
std::unordered_set<std::string> names;
std::vector< std::pair<std::string, Expr> > binders;
- bool isBuiltinOperator = false;
- bool isOverloadedFunction = false;
int match_vindex = -1;
std::vector<Type> match_ptypes;
Type type;
Type type2;
api::Term atomTerm;
+ ParseOp p;
}
: LPAREN_TOK quantOp[kind]
LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
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<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) {
- 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<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
- || 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<FunctionType>(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<Expr> 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 (
/**
* 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.
* 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<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.");
- }
+ PARSER_STATE->applyTypeAscription(p, type);
}
)
RPAREN_TOK
/**
* 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<uint64_t> numerals;
}
-: functionName[name, CHECK_NONE]
+: functionName[p.d_name, CHECK_NONE]
// indexed functions
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();
}
)
--- /dev/null
+/********************* */
+/*! \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 <string>
+
+#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 */
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<DatatypeType>(type);
+ if (dtype.isParametric())
+ {
+ std::vector<Expr> 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<DatatypeType>(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<Expr>& 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<Expr>::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<Type> argTypes;
+ for (std::vector<Expr>::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<ArrayType>(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<Rational>().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<FunctionType>(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<Expr> 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())
#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"
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<Expr>& 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;
projects / cvc5.git / commitdiff