Implementation()
: d_context(),
d_exprMap(new (true) CDHashMap<string, Expr>(&d_context)),
- d_typeMap(new (true) TypeMap(&d_context)),
- d_functions(new (true) CDHashSet<Expr, ExprHashFunction>(&d_context)) {
+ d_typeMap(new (true) TypeMap(&d_context))
+ {
d_overload_trie = new OverloadedTypeTrie(&d_context);
}
~Implementation() {
d_exprMap->deleteSelf();
d_typeMap->deleteSelf();
- d_functions->deleteSelf();
delete d_overload_trie;
}
bool bind(const string& name, Expr obj, bool levelZero, bool doOverload);
- bool bindDefinedFunction(const string& name, Expr obj, bool levelZero,
- bool doOverload);
void bindType(const string& name, Type t, bool levelZero = false);
void bindType(const string& name, const vector<Type>& params, Type t,
bool levelZero = false);
using TypeMap = CDHashMap<string, std::pair<vector<Type>, Type>>;
TypeMap* d_typeMap;
- /** A set of defined functions. */
- CDHashSet<Expr, ExprHashFunction>* d_functions;
-
//------------------------ operator overloading
// the null expression
Expr d_nullExpr;
return true;
}
-bool SymbolTable::Implementation::bindDefinedFunction(const string& name,
- Expr obj, bool levelZero,
- bool doOverload) {
- PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
- ExprManagerScope ems(obj);
- if (doOverload) {
- if (!bindWithOverloading(name, obj)) {
- return false;
- }
- }
- if (levelZero) {
- d_exprMap->insertAtContextLevelZero(name, obj);
- d_functions->insertAtContextLevelZero(obj);
- } else {
- d_exprMap->insert(name, obj);
- d_functions->insert(obj);
- }
- return true;
-}
-
bool SymbolTable::Implementation::isBound(const string& name) const {
return d_exprMap->find(name) != d_exprMap->end();
}
-bool SymbolTable::Implementation::isBoundDefinedFunction(
- const string& name) const {
- CDHashMap<string, Expr>::const_iterator found = d_exprMap->find(name);
- return found != d_exprMap->end() && d_functions->contains((*found).second);
-}
-
-bool SymbolTable::Implementation::isBoundDefinedFunction(Expr func) const {
- return d_functions->contains(func);
-}
-
Expr SymbolTable::Implementation::lookup(const string& name) const {
Assert(isBound(name));
Expr expr = (*d_exprMap->find(name)).second;
return d_implementation->bind(name, obj, levelZero, doOverload);
}
-bool SymbolTable::bindDefinedFunction(const string& name,
- Expr obj,
- bool levelZero,
- bool doOverload)
-{
- return d_implementation->bindDefinedFunction(name, obj, levelZero,
- doOverload);
-}
-
void SymbolTable::bindType(const string& name, Type t, bool levelZero)
{
d_implementation->bindType(name, t, levelZero);
{
return d_implementation->isBound(name);
}
-
-bool SymbolTable::isBoundDefinedFunction(const string& name) const
-{
- return d_implementation->isBoundDefinedFunction(name);
-}
-
-bool SymbolTable::isBoundDefinedFunction(Expr func) const
-{
- return d_implementation->isBoundDefinedFunction(func);
-}
bool SymbolTable::isBoundType(const string& name) const
{
return d_implementation->isBoundType(name);
bool levelZero = false,
bool doOverload = false);
- /**
- * Bind a function body to a name in the current scope.
- *
- * When doOverload is false:
- * if <code>name</code> is already bound to an expression in the current
- * level, then the binding is replaced. If <code>name</code> is bound
- * in a previous level, then the binding is "covered" by this one
- * until the current scope is popped.
- * If levelZero is true the name shouldn't be already bound.
- *
- * When doOverload is true:
- * if <code>name</code> is already bound to an expression in the current
- * level, then we mark the previous bound expression and obj as overloaded
- * functions.
- *
- * Same as bind() but registers this as a function (so that
- * isBoundDefinedFunction() returns true).
- *
- * @param name an identifier
- * @param obj the expression to bind to <code>name</code>
- * @param levelZero set if the binding must be done at level 0
- * @param doOverload set if the binding can overload the function name.
- *
- * Returns false if the binding was invalid.
- */
- bool bindDefinedFunction(const std::string& name,
- Expr obj,
- bool levelZero = false,
- bool doOverload = false);
-
/**
* Bind a type to a name in the current scope. If <code>name</code>
* is already bound to a type in the current level, then the binding
bool levelZero = false);
/**
- * Check whether a name is bound to an expression with either bind()
- * or bindDefinedFunction().
+ * Check whether a name is bound to an expression with bind().
*
* @param name the identifier to check.
* @returns true iff name is bound in the current scope.
*/
bool isBound(const std::string& name) const;
- /**
- * Check whether a name was bound to a function with bindDefinedFunction().
- */
- bool isBoundDefinedFunction(const std::string& name) const;
-
/**
* Check whether an Expr was bound to a function (i.e., was the
* second arg to bindDefinedFunction()).
Debug("parser") << "making " << *i << " : " << t << " = " << f << std::endl;
PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
Expr func = EXPR_MANAGER->mkVar(*i, t, ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
- PARSER_STATE->defineFunction(*i, f);
+ PARSER_STATE->defineVar(*i, f);
Command* decl = new DefineFunctionCommand(*i, func, f);
seq->addCommand(decl);
}
}
Kind Parser::getKindForFunction(Expr fun) {
- if(isDefinedFunction(fun)) {
+ Type t = fun.getType();
+ if (t.isFunction())
+ {
return APPLY_UF;
}
- Type t = fun.getType();
- if(t.isConstructor()) {
+ else if (t.isConstructor())
+ {
return APPLY_CONSTRUCTOR;
- } else if(t.isSelector()) {
+ }
+ else if (t.isSelector())
+ {
return APPLY_SELECTOR;
- } else if(t.isTester()) {
+ }
+ else if (t.isTester())
+ {
return APPLY_TESTER;
- } else if(t.isFunction()) {
- return APPLY_UF;
- }else{
+ }
+ else
+ {
parseError("internal error: unhandled function application kind");
return UNDEFINED_KIND;
}
type.isSelector();
}
-/* Returns true if name is bound to a defined function. */
-bool Parser::isDefinedFunction(const std::string& name) {
- // more permissive in type than isFunction(), because defined
- // functions can be zero-ary and declared functions cannot.
- return d_symtab->isBoundDefinedFunction(name);
-}
-
-/* Returns true if the Expr is a defined function. */
-bool Parser::isDefinedFunction(Expr func) {
- // more permissive in type than isFunction(), because defined
- // functions can be zero-ary and declared functions cannot.
- return d_symtab->isBoundDefinedFunction(func);
-}
-
/* Returns true if name is bound to a function returning boolean. */
bool Parser::isPredicate(const std::string& name) {
Expr expr = getVariable(name);
return expr;
}
-Expr Parser::mkFunction(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 = getExprManager()->mkVar(name, type, flags);
- defineFunction(name, expr, flags & ExprManager::VAR_FLAG_GLOBAL, doOverload);
- return expr;
-}
-
Expr Parser::mkAnonymousFunction(const std::string& prefix, const Type& type,
uint32_t flags) {
if (d_globalDeclarations) {
assert(isDeclared(name));
}
-void Parser::defineFunction(const std::string& name, const Expr& val,
- 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));
-}
-
void Parser::defineType(const std::string& name, const Type& type) {
d_symtab->bindType(name, type);
assert(isDeclared(name, SYM_SORT));
*/
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,
- 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()).
+ * difference between mkAnonymousFunction() and mkVar()).
*
* flags specify information about the variable, e.g. whether it is global or defined
* (see enum in expr_manager_template.h).
void defineVar(const std::string& name, const Expr& val,
bool levelZero = false, bool doOverload = false);
- /** 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 doOverload = false);
-
/** Create a new type definition. */
void defineType(const std::string& name, const Type& type);
*/
bool isFunctionLike(Expr fun);
- /** Is the symbol bound to a defined function? */
- bool isDefinedFunction(const std::string& name);
-
- /** Is the Expr a defined function? */
- bool isDefinedFunction(Expr func);
-
/** Is the symbol bound to a predicate? */
bool isPredicate(const std::string& name);
// 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, true);
+ Expr func = PARSER_STATE->mkVar(name, t,
+ ExprManager::VAR_FLAG_DEFINED, true);
cmd->reset(new DefineFunctionCommand(name, func, terms, expr));
}
| DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
}
( symbol[name,CHECK_NONE,SYM_VARIABLE] {
if( !terms.empty() ){
- if( !PARSER_STATE->isDefinedFunction(name) ){
+ if (!PARSER_STATE->isDeclared(name))
+ {
std::stringstream ss;
ss << "Function " << name << " in inv-constraint is not defined.";
PARSER_STATE->parseError(ss.str());
// fail, but we need an operator to continue here..
Debug("parser-sygus")
<< "Sygus grammar " << fun << " : op (declare="
- << PARSER_STATE->isDeclared(name) << ", define="
- << PARSER_STATE->isDefinedFunction(name) << ") : " << name
+ << PARSER_STATE->isDeclared(name) << ") : " << name
<< std::endl;
- if(!PARSER_STATE->isDeclared(name) &&
- !PARSER_STATE->isDefinedFunction(name) ){
+ if (!PARSER_STATE->isDeclared(name))
+ {
PARSER_STATE->parseError("Functions in sygus grammars must be "
"defined.");
}
( symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
{ PARSER_STATE->checkUserSymbol(name); }
term[e,e2]
- { Expr func = PARSER_STATE->mkFunction(name, e.getType(),
- ExprManager::VAR_FLAG_DEFINED);
+ { Expr func = PARSER_STATE->mkVar(name, e.getType(),
+ ExprManager::VAR_FLAG_DEFINED);
cmd->reset(new DefineFunctionCommand(name, func, e));
}
| LPAREN_TOK
}
t = EXPR_MANAGER->mkFunctionType(sorts, t);
}
- Expr func = PARSER_STATE->mkFunction(name, t,
- ExprManager::VAR_FLAG_DEFINED);
+ Expr func = PARSER_STATE->mkVar(name, t,
+ ExprManager::VAR_FLAG_DEFINED);
cmd->reset(new DefineFunctionCommand(name, func, terms, e));
}
)
// declare the name down here (while parsing term, signature
// must not be extended with the name itself; no recursion
// permitted)
- Expr func = PARSER_STATE->mkFunction(name, t,
- ExprManager::VAR_FLAG_DEFINED);
+ Expr func = PARSER_STATE->mkVar(name, t,
+ ExprManager::VAR_FLAG_DEFINED);
cmd->reset(new DefineFunctionCommand(name, func, terms, e));
}
// check that sexpr is a fresh function symbol, and reserve it
PARSER_STATE->reserveSymbolAtAssertionLevel(name);
// define it
- Expr func = PARSER_STATE->mkFunction(name, expr.getType());
+ Expr func = PARSER_STATE->mkVar(name, expr.getType());
// remember the last term to have been given a :named attribute
PARSER_STATE->setLastNamedTerm(expr, name);
// bind name to expr with define-fun
Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
std::stringstream ss;
ss << datatypes[index].getName() << "_let";
- Expr let_func = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
+ Expr let_func = mkVar(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
d_sygus_defined_funs.push_back( let_func );
preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) );
// the given name.
spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
}
- else if (isDefinedFunction(ops[i]))
+ else if (ops[i].getKind() == kind::VARIABLE)
{
Debug("parser-sygus") << "--> Defined function " << ops[i]
<< std::endl;
CVC4::Expr freshExpr;
if (type.isFunction())
{
- freshExpr = PARSER_STATE->mkFunction(name, type);
+ freshExpr = PARSER_STATE->mkVar(name, type);
}
else
{
}
} else {
// as yet, it's undeclared
- CVC4::Expr expr;
- if(type.isFunction()) {
- expr = PARSER_STATE->mkFunction(name, type);
- } else {
- expr = PARSER_STATE->mkVar(name, type);
- }
+ CVC4::Expr expr = PARSER_STATE->mkVar(name, type);
cmd = new DeclareFunctionCommand(name, expr, type);
}
}
projects / cvc5.git / commitdiff