diff options
Diffstat (limited to 'src/parser/antlr_parser.h')
| -rw-r--r-- | src/parser/antlr_parser.h | 132 |
1 files changed, 99 insertions, 33 deletions
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index 5a7291be6..3cfe4fc5d 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -31,6 +31,8 @@ namespace CVC4 { class Command; +class Type; +class FunctionType; namespace parser { @@ -110,23 +112,13 @@ protected: * @return the variable expression */ Expr getVariable(std::string var_name); + Expr getFunction(std::string var_name); + /* Expr getPredicate(std::string var_name); */ /** - * Return true if the the declaration policy we want to enforce is true. - * @param varName the symbol to check - * @oaram check the kind of check to perform - * @return true if the check holds + * Returns a sort, given a name */ - bool checkDeclaration(std::string varName, DeclarationCheck check); - - /** - * Return true if the the declaration policy we want to enforce is true - * on the given sort name. - * @param name the sort symbol to check - * @oaram check the kind of check to perform - * @return true if the check holds - */ - bool checkSort(std::string name, DeclarationCheck check); + const Type* getSort(std::string sort_name); /** * Types of symbols. @@ -135,9 +127,11 @@ protected: /** Variables */ SYM_VARIABLE, /** Predicates */ - SYM_PREDICATE, + /* SYM_PREDICATE, */ /** Functions */ - SYM_FUNCTION + SYM_FUNCTION, + /** Sorts */ + SYM_SORT }; /** @@ -147,10 +141,19 @@ protected: bool isDeclared(std::string var_name, SymbolType type = SYM_VARIABLE); /** - * Checks if the sort has been declared. - * @param the sort name + * Return true if the the declaration policy we want to enforce is true. + * @param varName the symbol to check + * @oaram check the kind of check to perform + * @return true if the check holds */ - bool isSort(std::string name); + bool checkDeclaration(std::string varName, + DeclarationCheck check, + SymbolType type = SYM_VARIABLE); + + + /** Returns the type for the variable with the given name. */ + const Type* getType(std::string var_name, + SymbolType type = SYM_VARIABLE); /** * Returns the true expression. @@ -199,14 +202,32 @@ protected: */ Expr mkExpr(Kind kind, const std::vector<Expr>& children); + /* Create a new CVC4 variable expression . */ + Expr mkVar(const std::string name, const Type* type); + + const std::vector<Expr> + mkVars(const std::vector<std::string> names, + const Type* type); + + + /** Returns a function type over the given domain and range types. */ + const FunctionType* functionType(const Type* domain, const Type* range); + /** Returns a function type over the given types. argTypes must have + at least 1 element. */ + const FunctionType* functionType(const std::vector<const Type*>& argTypes, + const Type* rangeType); + /** Returns a function type over the given types. types must have + at least 2 elements (i.e., a domain and range). */ + const FunctionType* functionType(const std::vector<const Type*>& types); + /** * Creates a new function over the given sorts. The function * has arity sorts.size() - 1 and range type sorts[sorts.size() - 1]. * @param name the name of the function * @param sorts the sorts */ - void newFunction(std::string name, - const std::vector<std::string>& sorts); + Expr newFunction(std::string name, + const std::vector<const Type*>& sorts); /** * Creates new functions over the given sorts. Each function has @@ -214,40 +235,75 @@ protected: * @param name the name of the function * @param sorts the sorts */ - void newFunctions(const std::vector<std::string>& names, - const std::vector<std::string>& sorts); + const std::vector<Expr> + newFunctions(const std::vector<std::string>& names, + const std::vector<const Type*>& sorts); + + /** Returns a predicate type over the given sorts. sorts must be + non-empty. If sorts has size 1, then the type is just BOOLEAN. */ + const Type* predicateType(const std::vector<const Type*>& sorts); /** - * Creates a new predicate over the given sorts. The predicate has - * arity sorts.size(). + * Creates a new predicate (a function with range boolean) over the + * given sorts. The predicate has sorts.size(). * @param name the name of the predicate * @param sorts the sorts */ - void newPredicate(std::string name, const std::vector<std::string>& sorts); + Expr newPredicate(std::string name, const std::vector<const Type*>& sorts); /** - * Creates new predicates over the given sorts. Each predicate - * will have arity sorts.size(). + * Creates new predicates (a function with range boolean) over the + * given sorts. Each predicate will have arity sorts.size(). * @param p_names the names of the predicates */ - void newPredicates(const std::vector<std::string>& names, const std::vector< - std::string>& sorts); + const std::vector<Expr> + newPredicates(const std::vector<std::string>& names, + const std::vector<const Type*>& sorts); /** * Creates a new sort with the given name. */ - void newSort(std::string name); + const Type* newSort(std::string name); /** * Creates a new sorts with the given names. */ - void newSorts(const std::vector<std::string>& names); + const std::vector<const Type*> + newSorts(const std::vector<std::string>& names); + + bool isBoolean(std::string name); + bool isFunction(std::string name); + bool isPredicate(std::string name); + + const BooleanType* booleanType(); + const KindType* kindType(); + + unsigned int minArity(Kind kind); + unsigned int maxArity(Kind kind); /** * Returns the precedence rank of the kind. */ static unsigned getPrecedence(Kind kind); + inline std::string toString(DeclarationCheck check) { + switch(check) { + case CHECK_NONE: return "CHECK_NONE"; + case CHECK_DECLARED: return "CHECK_DECLARED"; + case CHECK_UNDECLARED: return "CHECK_UNDECLARED"; + default: Unreachable(); + } + } + + inline std::string toString(SymbolType type) { + switch(type) { + case SYM_VARIABLE: return "SYM_VARIABLE"; + case SYM_FUNCTION: return "SYM_FUNCTION"; + case SYM_SORT: return "SYM_SORT"; + default: Unreachable(); + } + } + private: /** The expression manager */ @@ -256,10 +312,20 @@ private: /** The symbol table lookup */ SymbolTable<Expr> d_varSymbolTable; + /** A temporary hack: keep all the variable types in their own special + table. These should actually be Expr attributes. */ + SymbolTable<const Type*> d_varTypeTable; + /** The sort table */ - SymbolTable<std::string> d_sortTable; + SymbolTable<const Type*> d_sortTable; + + Expr getSymbol(std::string var_name, SymbolType type); + }; + + + }/* CVC4::parser namespace */ }/* CVC4 namespace */ |