diff options
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r-- | src/parser/parser.h | 22 |
1 files changed, 1 insertions, 21 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index 8f9cc425a..9319181db 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -497,15 +497,10 @@ public: */ 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). @@ -522,15 +517,6 @@ public: 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); @@ -677,12 +663,6 @@ public: */ 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); |