* Update parser for operator overloading.
* Improvements
* Updates
* Add assert
i != i_end;
++i) {
if(PARSER_STATE->isDeclared(*i, SYM_VARIABLE)) {
- Type oldType = PARSER_STATE->getType(*i);
+ Type oldType = PARSER_STATE->getVariable(*i).getType();
Debug("parser") << " " << *i << " was declared previously "
<< "with type " << oldType << std::endl;
if(oldType != t) {
formula[f] { args.push_back(f); }
( COMMA formula[f] { args.push_back(f); } )* RPAREN
// TODO: check arity
- { Type t = args.front().getType();
- Debug("parser") << "type is " << t << std::endl;
+ { Kind k = PARSER_STATE->getKindForFunction(args.front());
Debug("parser") << "expr is " << args.front() << std::endl;
- if(PARSER_STATE->isDefinedFunction(args.front())) {
- f = MK_EXPR(CVC4::kind::APPLY, args);
- } else if(t.isFunction()) {
- f = MK_EXPR(CVC4::kind::APPLY_UF, args);
- } else if(t.isConstructor()) {
- f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, args);
- } else if(t.isSelector()) {
- f = MK_EXPR(CVC4::kind::APPLY_SELECTOR, args);
- } else if(t.isTester()) {
- f = MK_EXPR(CVC4::kind::APPLY_TESTER, args);
- } else {
- PARSER_STATE->parseError("internal error: unhandled function application kind");
- }
+ Debug("parser") << "kind is " << k << std::endl;
+ f = MK_EXPR(k, args);
}
/* record / tuple select */
/* variable / zero-ary constructor application */
| identifier[name,CHECK_DECLARED,SYM_VARIABLE]
/* ascriptions will be required for parameterized zero-ary constructors */
- { f = PARSER_STATE->getVariable(name); }
- { // datatypes: zero-ary constructors
- Type t2 = PARSER_STATE->getType(name);
+ { f = PARSER_STATE->getVariable(name);
+ // datatypes: zero-ary constructors
+ Type t2 = f.getType();
if(t2.isConstructor() && ConstructorType(t2).getArity() == 0) {
// don't require parentheses, immediately turn it into an apply
f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, f);
#include <iostream>
#include <iterator>
#include <sstream>
+#include <unordered_set>
#include "base/output.h"
#include "expr/expr.h"
return getSymbol(name, SYM_VARIABLE);
}
-Type Parser::getType(const std::string& var_name, SymbolType type) {
- checkDeclaration(var_name, CHECK_DECLARED, type);
- assert(isDeclared(var_name, type));
- Type t = getSymbol(var_name, type).getType();
- return t;
+Expr Parser::getExpressionForName(const std::string& name) {
+ Type t;
+ return getExpressionForNameAndType(name, t);
+}
+
+Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) {
+ assert( isDeclared(name) );
+ // first check if the variable is declared and not overloaded
+ Expr expr = getVariable(name);
+ if(expr.isNull()) {
+ // the variable is overloaded, try with type if the type exists
+ if(!t.isNull()) {
+ // if we decide later to support annotations for function types, this will update to
+ // separate t into ( argument types, return type )
+ expr = getOverloadedConstantForType(name, t);
+ if(expr.isNull()) {
+ parseError("Cannot get overloaded constant for type ascription.");
+ }
+ }else{
+ parseError("Overloaded constants must be type cast.");
+ }
+ }
+ // now, post-process the expression
+ assert( !expr.isNull() );
+ if(isDefinedFunction(expr)) {
+ // defined functions/constants are wrapped in an APPLY so that they are
+ // expanded into their definition, e.g. during SmtEnginePrivate::expandDefinitions
+ expr = d_exprManager->mkExpr(CVC4::kind::APPLY, expr);
+ }else{
+ Type te = expr.getType();
+ if(te.isConstructor() && ConstructorType(te).getArity() == 0) {
+ // nullary constructors have APPLY_CONSTRUCTOR kind with no children
+ expr = d_exprManager->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, expr);
+ }
+ }
+ return expr;
+}
+
+Kind Parser::getKindForFunction(Expr fun) {
+ if(isDefinedFunction(fun)) {
+ return APPLY;
+ }
+ Type t = fun.getType();
+ if(t.isConstructor()) {
+ return APPLY_CONSTRUCTOR;
+ } else if(t.isSelector()) {
+ return APPLY_SELECTOR;
+ } else if(t.isTester()) {
+ return APPLY_TESTER;
+ } else if(t.isFunction()) {
+ return APPLY_UF;
+ }else{
+ parseError("internal error: unhandled function application kind");
+ return UNDEFINED_KIND;
+ }
}
Type Parser::getSort(const std::string& name) {
/* Returns true if name is bound to a boolean variable. */
bool Parser::isBoolean(const std::string& name) {
- return isDeclared(name, SYM_VARIABLE) && getType(name).isBoolean();
+ Expr expr = getVariable(name);
+ return !expr.isNull() && expr.getType().isBoolean();
}
-/* Returns true if name is bound to a function-like thing (function,
- * constructor, tester, or selector). */
-bool Parser::isFunctionLike(const std::string& name) {
- if (!isDeclared(name, SYM_VARIABLE)) {
+bool Parser::isFunctionLike(Expr fun) {
+ if(fun.isNull()) {
return false;
}
- Type type = getType(name);
+ Type type = fun.getType();
return type.isFunction() || type.isConstructor() || type.isTester() ||
type.isSelector();
}
/* Returns true if name is bound to a function returning boolean. */
bool Parser::isPredicate(const std::string& name) {
- return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
+ Expr expr = getVariable(name);
+ return !expr.isNull() && expr.getType().isPredicate();
}
-Expr Parser::mkVar(const std::string& name, const Type& type, uint32_t flags) {
+Expr Parser::mkVar(const std::string& name, const Type& type, uint32_t flags, bool doOverload) {
if (d_globalDeclarations) {
flags |= ExprManager::VAR_FLAG_GLOBAL;
}
Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
Expr expr = d_exprManager->mkVar(name, type, flags);
- defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL);
+ defineVar(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload);
return expr;
}
}
Expr Parser::mkFunction(const std::string& name, const Type& type,
- uint32_t flags) {
+ uint32_t flags, bool doOverload) {
if (d_globalDeclarations) {
flags |= ExprManager::VAR_FLAG_GLOBAL;
}
Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
Expr expr = d_exprManager->mkVar(name, type, flags);
- defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL);
+ defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload);
return expr;
}
}
std::vector<Expr> Parser::mkVars(const std::vector<std::string> names,
- const Type& type, uint32_t flags) {
+ const Type& type, uint32_t flags, bool doOverload) {
if (d_globalDeclarations) {
flags |= ExprManager::VAR_FLAG_GLOBAL;
}
std::vector<Expr> vars;
for (unsigned i = 0; i < names.size(); ++i) {
- vars.push_back(mkVar(names[i], type, flags));
+ vars.push_back(mkVar(names[i], type, flags, doOverload));
}
return vars;
}
}
void Parser::defineVar(const std::string& name, const Expr& val,
- bool levelZero) {
+ bool levelZero, bool doOverload) {
Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl;
- d_symtab->bind(name, val, levelZero);
+ if (!d_symtab->bind(name, val, levelZero, doOverload)) {
+ std::stringstream ss;
+ ss << "Failed to bind " << name << " to symbol of type " << val.getType();
+ parseError(ss.str());
+ }
assert(isDeclared(name));
}
void Parser::defineFunction(const std::string& name, const Expr& val,
- bool levelZero) {
- d_symtab->bindDefinedFunction(name, val, levelZero);
+ bool levelZero, bool doOverload) {
+ if (!d_symtab->bindDefinedFunction(name, val, levelZero, doOverload)) {
+ std::stringstream ss;
+ ss << "Failed to bind defined function " << name << " to symbol of type " << val.getType();
+ parseError(ss.str());
+ }
assert(isDeclared(name));
}
}
std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(
- std::vector<Datatype>& datatypes) {
+ std::vector<Datatype>& datatypes, bool doOverload) {
try {
std::vector<DatatypeType> types =
d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
} else {
defineType(name, t);
}
+ std::unordered_set< std::string > consNames;
+ std::unordered_set< std::string > selNames;
for (Datatype::const_iterator j = dt.begin(), j_end = dt.end();
j != j_end; ++j) {
const DatatypeConstructor& ctor = *j;
Expr constructor = ctor.getConstructor();
Debug("parser-idt") << "+ define " << constructor << std::endl;
string constructorName = ctor.getName();
- if (isDeclared(constructorName, SYM_VARIABLE)) {
- throw ParserException(constructorName + " already declared");
+ if(consNames.find(constructorName)==consNames.end()) {
+ if(!doOverload) {
+ checkDeclaration(constructorName, CHECK_UNDECLARED);
+ }
+ defineVar(constructorName, constructor, false, doOverload);
+ consNames.insert(constructorName);
+ }else{
+ throw ParserException(constructorName + " already declared in this datatype");
}
- defineVar(constructorName, constructor);
Expr tester = ctor.getTester();
Debug("parser-idt") << "+ define " << tester << std::endl;
string testerName = ctor.getTesterName();
- if (isDeclared(testerName, SYM_VARIABLE)) {
- throw ParserException(testerName + " already declared");
+ if(!doOverload) {
+ checkDeclaration(testerName, CHECK_UNDECLARED);
}
- defineVar(testerName, tester);
+ defineVar(testerName, tester, false, doOverload);
for (DatatypeConstructor::const_iterator k = ctor.begin(),
k_end = ctor.end();
k != k_end; ++k) {
Expr selector = (*k).getSelector();
Debug("parser-idt") << "+++ define " << selector << std::endl;
string selectorName = (*k).getName();
- if (isDeclared(selectorName, SYM_VARIABLE)) {
- throw ParserException(selectorName + " already declared");
+ if(selNames.find(selectorName)==selNames.end()) {
+ if(!doOverload) {
+ checkDeclaration(selectorName, CHECK_UNDECLARED);
+ }
+ defineVar(selectorName, selector, false, doOverload);
+ selNames.insert(selectorName);
+ }else{
+ throw ParserException(selectorName + " already declared in this datatype");
}
- defineVar(selectorName, selector);
}
}
}
}
}
-void Parser::checkFunctionLike(const std::string& name) throw(ParserException) {
- if (d_checksEnabled && !isFunctionLike(name)) {
- parseError("Expecting function-like symbol, found '" + name + "'");
+void Parser::checkFunctionLike(Expr fun) throw(ParserException) {
+ if (d_checksEnabled && !isFunctionLike(fun)) {
+ stringstream ss;
+ ss << "Expecting function-like symbol, found '";
+ ss << fun;
+ ss << "'";
+ parseError(ss.str());
}
}
*/
class CVC4_PUBLIC Parser {
friend class ParserBuilder;
-
+private:
/** The expression manager */
ExprManager *d_exprManager;
/** The resource manager associated with this expr manager */
*/
std::list<Command*> d_commandQueue;
- /** Lookup a symbol in the given namespace. */
+ /** Lookup a symbol in the given namespace (as specified by the type).
+ * Only returns a symbol if it is not overloaded, returns null otherwise.
+ */
Expr getSymbol(const std::string& var_name, SymbolType type);
protected:
bool logicIsForced() const { return d_logicIsForced; }
/**
- * Returns a variable, given a name.
+ * Gets the variable currently bound to name.
*
* @param name the name of the variable
* @return the variable expression
+ * Only returns a variable if its name is not overloaded, returns null otherwise.
*/
Expr getVariable(const std::string& name);
/**
- * Returns a function, given a name.
+ * Gets the function currently bound to name.
*
* @param name the name of the variable
* @return the variable expression
+ * Only returns a function if its name is not overloaded, returns null otherwise.
*/
Expr getFunction(const std::string& name);
+ /**
+ * Returns the expression that name should be interpreted as, based on the current binding.
+ *
+ * The symbol name should be declared.
+ * This creates the expression that the string "name" should be interpreted as.
+ * Typically this corresponds to a variable, but it may also correspond to
+ * a nullary constructor or a defined function.
+ * Only returns an expression if its name is not overloaded, returns null otherwise.
+ */
+ virtual Expr getExpressionForName(const std::string& name);
+
+ /**
+ * Returns the expression that name should be interpreted as, based on the current binding.
+ *
+ * This is the same as above but where the name has been type cast to t.
+ */
+ virtual Expr getExpressionForNameAndType(const std::string& name, Type t);
+
+ /**
+ * Returns the kind that should be used for applications of expression fun, where
+ * fun has "function-like" type, i.e. where checkFunctionLike(fun) returns true.
+ * Returns a parse error if fun does not have function-like type.
+ *
+ * For example, this function returns
+ * APPLY_UF if fun has function type,
+ * APPLY_CONSTRUCTOR if fun has constructor type.
+ */
+ Kind getKindForFunction(Expr fun);
+
/**
* Returns a sort, given a name.
* @param sort_name the name to look up
void reserveSymbolAtAssertionLevel(const std::string& name);
/**
- * Checks whether the given name is bound to a function.
- * @param name the name to check
- * @throws ParserException if checks are enabled and name is not
- * bound to a function
+ * Checks whether the given expression is function-like, i.e.
+ * it expects arguments. This is checked by looking at the type
+ * of fun. Examples of function types are function, constructor,
+ * selector, tester.
+ * @param fun the expression to check
+ * @throws ParserException if checks are enabled and fun is not
+ * a function
*/
- void checkFunctionLike(const std::string& name) throw(ParserException);
+ void checkFunctionLike(Expr fun) throw(ParserException);
/**
* Check that <code>kind</code> can accept <code>numArgs</code> arguments.
*/
void checkOperator(Kind kind, unsigned numArgs) throw(ParserException);
- /**
- * Returns the type for the variable with the given name.
+ /** Create a new CVC4 variable expression of the given type.
*
- * @param var_name the symbol to lookup
- * @param type the (namespace) type of the symbol
+ * flags specify information about the variable, e.g. whether it is global or defined
+ * (see enum in expr_manager_template.h).
+ *
+ * If a symbol with name already exists,
+ * then if doOverload is true, we create overloaded operators.
+ * else if doOverload is false, the existing expression is shadowed by the new expression.
*/
- Type getType(const std::string& var_name, SymbolType type = SYM_VARIABLE);
-
- /** Create a new CVC4 variable expression of the given type. */
Expr mkVar(const std::string& name, const Type& type,
- uint32_t flags = ExprManager::VAR_FLAG_NONE);
+ uint32_t flags = ExprManager::VAR_FLAG_NONE,
+ bool doOverload = false);
/**
* Create a set of new CVC4 variable expressions of the given type.
+ *
+ * flags specify information about the variable, e.g. whether it is global or defined
+ * (see enum in expr_manager_template.h).
+ *
+ * For each name, if a symbol with name already exists,
+ * then if doOverload is true, we create overloaded operators.
+ * else if doOverload is false, the existing expression is shadowed by the new expression.
*/
std::vector<Expr>
mkVars(const std::vector<std::string> names, const Type& type,
- uint32_t flags = ExprManager::VAR_FLAG_NONE);
+ uint32_t flags = ExprManager::VAR_FLAG_NONE,
+ bool doOverload = false);
/** Create a new CVC4 bound variable expression of the given type. */
Expr mkBoundVar(const std::string& name, const Type& type);
/**
* Create a set of new CVC4 bound variable expressions of the given type.
+ *
+ * flags specify information about the variable, e.g. whether it is global or defined
+ * (see enum in expr_manager_template.h).
+ *
+ * For each name, if a symbol with name already exists,
+ * then if doOverload is true, we create overloaded operators.
+ * else if doOverload is false, the existing expression is shadowed by the new expression.
*/
std::vector<Expr> mkBoundVars(const std::vector<std::string> names, const Type& type);
/** Create a new CVC4 function expression of the given type. */
Expr mkFunction(const std::string& name, const Type& type,
- uint32_t flags = ExprManager::VAR_FLAG_NONE);
+ uint32_t flags = ExprManager::VAR_FLAG_NONE,
+ bool doOverload=false);
/**
* Create a new CVC4 function expression of the given type,
* appending a unique index to its name. (That's the ONLY
* difference between mkAnonymousFunction() and mkFunction()).
+ *
+ * flags specify information about the variable, e.g. whether it is global or defined
+ * (see enum in expr_manager_template.h).
*/
Expr mkAnonymousFunction(const std::string& prefix, const Type& type,
uint32_t flags = ExprManager::VAR_FLAG_NONE);
- /** Create a new variable definition (e.g., from a let binding). */
+ /** Create a new variable definition (e.g., from a let binding).
+ * levelZero is set if the binding must be done at level 0.
+ * If a symbol with name already exists,
+ * then if doOverload is true, we create overloaded operators.
+ * else if doOverload is false, the existing expression is shadowed by the new expression.
+ */
void defineVar(const std::string& name, const Expr& val,
- bool levelZero = false);
+ bool levelZero = false, bool doOverload = false);
- /** Create a new function definition (e.g., from a define-fun). */
+ /** Create a new function definition (e.g., from a define-fun).
+ * levelZero is set if the binding must be done at level 0.
+ * If a symbol with name already exists,
+ * then if doOverload is true, we create overloaded operators.
+ * else if doOverload is false, the existing expression is shadowed by the new expression.
+ */
void defineFunction(const std::string& name, const Expr& val,
- bool levelZero = false);
+ bool levelZero = false, bool doOverload = false);
/** Create a new type definition. */
void defineType(const std::string& name, const Type& type);
/**
* Create sorts of mutually-recursive datatypes.
+ * For each symbol defined by the datatype, if a symbol with name already exists,
+ * then if doOverload is true, we create overloaded operators.
+ * else if doOverload is false, the existing expression is shadowed by the new expression.
*/
std::vector<DatatypeType>
- mkMutualDatatypeTypes(std::vector<Datatype>& datatypes);
+ mkMutualDatatypeTypes(std::vector<Datatype>& datatypes, bool doOverload=false);
/**
* Add an operator to the current legal set.
/** Is the symbol bound to a boolean variable? */
bool isBoolean(const std::string& name);
- /** Is the symbol bound to a function (or function-like thing)? */
- bool isFunctionLike(const std::string& name);
+ /** Is fun a function (or function-like thing)?
+ * Currently this means its type is either a function, constructor, tester, or selector.
+ */
+ bool isFunctionLike(Expr fun);
/** Is the symbol bound to a defined function? */
bool isDefinedFunction(const std::string& name);
~ExprStream() { delete d_parser; }
Expr nextExpr() { return d_parser->nextExpression(); }
};/* class Parser::ExprStream */
+
+ //------------------------ operator overloading
+ /** is this function overloaded? */
+ bool isOverloadedFunction(Expr fun) {
+ return d_symtab->isOverloadedFunction(fun);
+ }
+
+ /** Get overloaded constant for type.
+ * If possible, it returns a defined symbol with name
+ * that has type t. Otherwise returns null expression.
+ */
+ Expr getOverloadedConstantForType(const std::string& name, Type t) {
+ return d_symtab->getOverloadedConstantForType(name, t);
+ }
+
+ /**
+ * If possible, returns a defined function for a name
+ * and a vector of expected argument types. Otherwise returns
+ * null expression.
+ */
+ Expr getOverloadedFunctionForTypes(const std::string& name, std::vector< Type >& argTypes) {
+ return d_symtab->getOverloadedFunctionForTypes(name, argTypes);
+ }
+ //------------------------ end operator overloading
};/* class Parser */
}/* CVC4::parser namespace */
std::string name;
}
: functionName[name,CHECK_DECLARED]
- { PARSER_STATE->checkFunctionLike(name);
- fun = PARSER_STATE->getVariable(name); }
+ { fun = PARSER_STATE->getVariable(name);
+ PARSER_STATE->checkFunctionLike(fun); }
;
/**
}
| /* function declaration */
DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
- symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+ symbol[name,CHECK_NONE,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(name); }
LPAREN_TOK sortList[sorts] RPAREN_TOK
sortSymbol[t,CHECK_DECLARED]
}
t = EXPR_MANAGER->mkFunctionType(sorts, t);
}
- Expr func = PARSER_STATE->mkVar(name, t);
+ // we allow overloading for function declarations
+ Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
cmd->reset(new DeclareFunctionCommand(name, func, t));
}
| /* function definition */
// declare the name down here (while parsing term, signature
// must not be extended with the name itself; no recursion
// permitted)
+ // we allow overloading for function definitions
Expr func = PARSER_STATE->mkFunction(name, t,
- ExprManager::VAR_FLAG_DEFINED);
+ ExprManager::VAR_FLAG_DEFINED, true);
cmd->reset(new DefineFunctionCommand(name, func, terms, expr));
}
| /* value query */
}else{
synth_fun_type = range;
}
- synth_fun = PARSER_STATE->mkVar(fun, synth_fun_type);
+ // allow overloading for synth fun
+ synth_fun = PARSER_STATE->mkVar(fun, synth_fun_type, ExprManager::VAR_FLAG_NONE, true);
PARSER_STATE->pushScope(true);
for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend;
/* declare-const */
| DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
- symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+ symbol[name,CHECK_NONE,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(name); }
sortSymbol[t,CHECK_DECLARED]
- { Expr c = PARSER_STATE->mkVar(name, t);
+ { // allow overloading here
+ Expr c = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
cmd->reset(new DeclareFunctionCommand(name, c, t)); }
/* get model */
{ PARSER_STATE->checkThatLogicIsSet();
seq.reset(new CVC4::CommandSequence());
}
- symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE]
+ symbol[fname,CHECK_NONE,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(fname); }
LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
sortSymbol[t,CHECK_DECLARED]
}
t = EXPR_MANAGER->mkFunctionType(sorts, t);
}
- Expr func = PARSER_STATE->mkVar(fname, t);
+ // allow overloading
+ Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_NONE, true);
seq->addCommand(new DeclareFunctionCommand(fname, func, t));
if( sortedVarNames.empty() ){
func_app = func;
}
}
sortedVarNames.clear();
- Expr func = PARSER_STATE->mkVar(fname, t);
+ // allow overloading
+ Expr func = PARSER_STATE->mkVar(fname, t, ExprManager::VAR_FLAG_NONE, true);
seq->addCommand(new DeclareFunctionCommand(fname, func, t));
funcs.push_back( func );
}
} else {
t = sorts[0];
}
- Expr func = PARSER_STATE->mkVar(name, t);
+ // allow overloading
+ Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
seq->addCommand(new DeclareFunctionCommand(name, func, t));
sorts.clear();
}
}
t = EXPR_MANAGER->mkFunctionType(sorts, t);
}
- Expr func = PARSER_STATE->mkVar(name, t);
+ // allow overloading
+ Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
seq->addCommand(new DeclareFunctionCommand(name, func, t));
sorts.clear();
}
RPAREN_TOK
LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
{ PARSER_STATE->popScope();
- cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)));
+ cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts, true)));
}
;
}
( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
RPAREN_TOK
- { cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts))); }
+ { cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts, true))); }
;
datatypesDefCommand[bool isCo, std::unique_ptr<CVC4::Command>* cmd]
)+
RPAREN_TOK
{ PARSER_STATE->popScope();
- cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)));
+ cmd->reset(new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts, true)));
}
;
* @return the expression representing the formula
*/
term[CVC4::Expr& expr, CVC4::Expr& expr2]
+@init {
+ std::string name;
+}
+: termNonVariable[expr, expr2]
+ /* a variable */
+ | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
+ { expr = PARSER_STATE->getExpressionForName(name);
+ assert( !expr.isNull() );
+ }
+ ;
+
+/**
+ * Matches a term.
+ * @return the expression representing the formula
+ */
+termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
@init {
Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
Kind kind = kind::NULL_EXPR;
Type type;
std::string s;
bool isBuiltinOperator = false;
+ bool isOverloadedFunction = false;
+ bool readVariable = false;
int match_vindex = -1;
std::vector<Type> match_ptypes;
}
expr = MK_EXPR(kind, args);
}
}
- | LPAREN_TOK AS_TOK term[f, f2] sortSymbol[type, CHECK_DECLARED] RPAREN_TOK
+ | 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()) {
- 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);
+ // 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;
} else {
if(f.getType() != type) {
PARSER_STATE->parseError("Type ascription not satisfied.");
+ }else{
+ expr = f;
}
}
}
} else {
/* A non-built-in function application */
PARSER_STATE->checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE);
- //hack to allow constants with parentheses (disabled for now)
- //if( PARSER_STATE->sygus() && !PARSER_STATE->isFunctionLike(name) ){
- // op = PARSER_STATE->getVariable(name);
- //}else{
- PARSER_STATE->checkFunctionLike(name);
- const bool isDefinedFunction =
- PARSER_STATE->isDefinedFunction(name);
- if(isDefinedFunction) {
- expr = PARSER_STATE->getFunction(name);
- kind = CVC4::kind::APPLY;
- } else {
- expr = PARSER_STATE->getVariable(name);
- Type t = expr.getType();
- if(t.isConstructor()) {
- kind = CVC4::kind::APPLY_CONSTRUCTOR;
- } else if(t.isSelector()) {
- kind = CVC4::kind::APPLY_SELECTOR;
- } else if(t.isTester()) {
- kind = CVC4::kind::APPLY_TESTER;
- } else {
- kind = CVC4::kind::APPLY_UF;
- }
+ expr = PARSER_STATE->getVariable(name);
+ if(!expr.isNull()) {
+ //hack to allow constants with parentheses (disabled for now)
+ //if( PARSER_STATE->sygus() && !PARSER_STATE->isFunctionLike(expr) ){
+ // op = PARSER_STATE->getVariable(name);
+ //}else{
+ PARSER_STATE->checkFunctionLike(expr);
+ kind = PARSER_STATE->getKindForFunction(expr);
+ args.push_back(expr);
+ }else{
+ isOverloadedFunction = true;
}
- args.push_back(expr);
}
- }
+ }
//(termList[args,expr])? RPAREN_TOK
termList[args,expr] RPAREN_TOK
{ 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(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.");
+ }
+ }
if(isBuiltinOperator) {
PARSER_STATE->checkOperator(kind, args.size());
}
// ConstructorType(expr.getType()).getArity()==0;
expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr);
}
- /* a variable */
- | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
- { if( PARSER_STATE->sygus() && name[0]=='-' &&
- name.find_first_not_of("0123456789", 1) == std::string::npos ){
- //allow unary minus in sygus
- expr = MK_CONST(Rational(name));
- }else{
- const bool isDefinedFunction =
- PARSER_STATE->isDefinedFunction(name);
- if(PARSER_STATE->isAbstractValue(name)) {
- expr = PARSER_STATE->mkAbstractValue(name);
- } else if(isDefinedFunction) {
- expr = MK_EXPR(CVC4::kind::APPLY,
- PARSER_STATE->getFunction(name));
- } else {
- expr = PARSER_STATE->getVariable(name);
- Type t = PARSER_STATE->getType(name);
- if(t.isConstructor() && ConstructorType(t).getArity() == 0) {
- // don't require parentheses, immediately turn it into an apply
- expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr);
- }
- }
- }
- }
/* attributed expressions */
| LPAREN_TOK ATTRIBUTE_TOK term[expr, f2]
std::string id;
CVC4::DatatypeConstructor* ctor = NULL;
}
- : symbol[id,CHECK_UNDECLARED,SYM_VARIABLE]
+ : symbol[id,CHECK_NONE,SYM_VARIABLE]
{ // make the tester
std::string testerId("is-");
testerId.append(id);
- PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
ctor = new CVC4::DatatypeConstructor(id, testerId);
}
( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
std::string id;
Type t, t2;
}
- : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t,CHECK_NONE]
+ : symbol[id,CHECK_NONE,SYM_SORT] sortSymbol[t,CHECK_NONE]
{ ctor.addArg(id, t);
Debug("parser-idt") << "selector: " << id.c_str()
<< " of type " << t << std::endl;
return d_logicSet;
}
+Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) {
+ if(sygus() && name[0]=='-' &&
+ name.find_first_not_of("0123456789", 1) == std::string::npos) {
+ //allow unary minus in sygus
+ return getExprManager()->mkConst(Rational(name));
+ }else if(isAbstractValue(name)) {
+ return mkAbstractValue(name);
+ }else{
+ return Parser::getExpressionForNameAndType(name, t);
+ }
+}
+
void Smt2::reset() {
d_logicSet = false;
d_logic = LogicInfo();
bool isTheoryEnabled(Theory theory) const;
bool logicIsSet();
+
+ /**
+ * Returns the expression that name should be interpreted as.
+ */
+ virtual Expr getExpressionForNameAndType(const std::string& name, Type t);
void reset();
hung13sdk_output2.smt2 \
declare-funs.smt2 \
declare-fun-is-match.smt2 \
+ issue1063-overloading-dt-cons.smt2 \
+ issue1063-overloading-dt-sel.smt2 \
+ issue1063-overloading-dt-fun.smt2 \
non-fatal-errors.smt2 \
sqrt2-sort-inf-unk.smt2
+
# Regression tests for PL inputs
CVC_TESTS = \
boolean.cvc \
% EXPECT-ERROR: CVC4 Error:
-% EXPECT-ERROR: Parse Error: foo already declared
+% EXPECT-ERROR: Parse Error: foo already declared in this datatype
% EXIT: 1
-DATATYPE single_ctor = foo(bar:REAL) END;
+DATATYPE single_ctor = foo(bar:REAL) | foo(bar2:REAL) END;
DATATYPE double_ctor = foo(bar:REAL) END;
--- /dev/null
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes () ((Enum0 (In_Air) (On_Ground) (None))))
+(declare-datatypes () ((Enum1 (True) (False) (None))))
+(declare-fun var_0 (Int) Enum0)
+(declare-fun var_1 (Int) Enum1)
+(assert (= (var_0 0) (as None Enum0)))
+(assert (= (var_1 1) (as None Enum1)))
+(assert (not (is-In_Air (var_0 0))))
+(declare-fun var_2 () Enum1)
+(assert (is-None var_2))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes () ((Enum (cons (val Int)) (On_Ground) (None))))
+(declare-fun cons (Int Int) Int)
+(declare-fun cons (Enum) Bool)
+(declare-fun cons (Bool) Int)
+(assert (cons (cons 0)))
+(assert (= (cons (cons true) (cons false)) 4))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --lang=smt2.5
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes () ((Enum0 (cons (data Int)) (None))))
+(declare-datatypes () ((Enum1 (cons (data Bool)) (None))))
+(declare-fun var_0 () Enum0)
+(declare-fun var_1 () Enum1)
+(assert (= (data var_0) 5))
+(assert (data var_1))
+(check-sat)
projects / cvc5.git / commitdiff