diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-20 11:19:50 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-20 11:19:50 +0000 |
commit | 2499bd64a5ac688573ebbcd6114983f64a8094eb (patch) | |
tree | 0d49608cf7c21298fbeb8606fa1943c96beb8652 /src/parser/parser.h | |
parent | 5a98094e8eee680d4f489e901107dfc484a1679f (diff) |
numerous bugfixes
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r-- | src/parser/parser.h | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index 25fb30be6..033abb42a 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -125,8 +125,8 @@ class CVC4_PUBLIC Parser { */ DeclarationScope* d_declScope; - /** The name of the input file. */ -// std::string d_filename; + /** How many anonymous functions we've created. */ + size_t d_anonymousFunctionCount; /** Are we done */ bool d_done; @@ -322,6 +322,13 @@ public: /** Create a new CVC4 function expression of the given type. */ Expr mkFunction(const std::string& name, const Type& type); + /** + * 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()). + */ + Expr mkAnonymousFunction(const std::string& prefix, const Type& type); + /** Create a new variable definition (e.g., from a let binding). */ void defineVar(const std::string& name, const Expr& val); @@ -394,6 +401,9 @@ public: /** 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); |