diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2011-05-13 22:02:52 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2011-05-13 22:02:52 +0000 |
commit | 8d54316e7ff784a8d66da9ecc2d289ab463761c2 (patch) | |
tree | c7b5351b372cb360780ce62935fb2cfb5792299a /src/parser/parser.h | |
parent | 69c9ec0e1e42f3f2f2f79d3e98398c5cd1559c66 (diff) |
added support for parametric datatypes, updated cvc parser to handle parametric datatypes, type ascriptions are not implemented yet
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r-- | src/parser/parser.h | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index 6509b192b..6d55e195e 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -150,7 +150,7 @@ class CVC4_PUBLIC Parser { * depend on mkMutualDatatypeTypes() to check everything and clear * this out. */ - std::set<SortType> d_unresolved; + std::set<Type> d_unresolved; /** * "Preemption commands": extra commands implied by subterms that @@ -255,6 +255,11 @@ public: const std::vector<Type>& params); /** + * Returns arity of a (parameterized) sort, given a name and args. + */ + size_t getArity(const std::string& sort_name); + + /** * Checks if a symbol has been declared. * @param name the symbol name * @param type the symbol type @@ -368,6 +373,14 @@ public: SortType mkUnresolvedType(const std::string& name); /** + * Creates a new "unresolved type," used only during parsing. + */ + SortConstructorType mkUnresolvedTypeConstructor(const std::string& name, + size_t arity); + SortConstructorType mkUnresolvedTypeConstructor(const std::string& name, + const std::vector<Type>& params); + + /** * Returns true IFF name is an unresolved type. */ bool isUnresolvedType(const std::string& name); |