diff options
Diffstat (limited to 'src/parser/parser.h')
| -rw-r--r-- | src/parser/parser.h | 168 |
1 files changed, 81 insertions, 87 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index d40236208..373da6c47 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -42,9 +42,6 @@ class Command; class FunctionType; class Type; class ResourceManager; -namespace api { -class Solver; -} //for sygus gterm two-pass parsing class CVC4_PUBLIC SygusGTerm { @@ -59,10 +56,10 @@ public: gterm_unresolved, gterm_ignore, }; - Type d_type; + api::Sort d_type; /** The parsed operator */ ParseOp d_op; - std::vector< Expr > d_let_vars; + std::vector<api::Term> d_let_vars; unsigned d_gterm_type; std::string d_name; std::vector< SygusGTerm > d_children; @@ -214,7 +211,7 @@ private: std::string d_forcedLogic; /** The set of operators available in the current logic. */ - std::set<Kind> d_logicOperators; + std::set<api::Kind> d_logicOperators; /** The set of attributes already warned about. */ std::set<std::string> d_attributesWarnedAbout; @@ -226,7 +223,7 @@ private: * depend on mkMutualDatatypeTypes() to check everything and clear * this out. */ - std::set<Type> d_unresolved; + std::set<api::Sort> d_unresolved; /** * "Preemption commands": extra commands implied by subterms that @@ -240,7 +237,7 @@ private: /** Lookup a symbol in the given namespace (as specified by the type). * Only returns a symbol if it is not overloaded, returns null otherwise. */ - Expr getSymbol(const std::string& var_name, SymbolType type); + api::Term getSymbol(const std::string& var_name, SymbolType type); protected: /** The API Solver object. */ @@ -340,7 +337,7 @@ public: * @return the variable expression * Only returns a variable if its name is not overloaded, returns null otherwise. */ - Expr getVariable(const std::string& name); + api::Term getVariable(const std::string& name); /** * Gets the function currently bound to name. @@ -349,7 +346,7 @@ public: * @return the variable expression * Only returns a function if its name is not overloaded, returns null otherwise. */ - Expr getFunction(const std::string& name); + api::Term getFunction(const std::string& name); /** * Returns the expression that name should be interpreted as, based on the current binding. @@ -360,15 +357,16 @@ public: * a nullary constructor or a defined function. * Only returns an expression if its name is not overloaded, returns null otherwise. */ - virtual Expr getExpressionForName(const std::string& name); - + virtual api::Term getExpressionForName(const std::string& name); + /** * Returns the expression that name should be interpreted as, based on the current binding. * * This is the same as above but where the name has been type cast to t. */ - virtual Expr getExpressionForNameAndType(const std::string& name, Type t); - + virtual api::Term getExpressionForNameAndType(const std::string& name, + api::Sort t); + /** * Returns the kind that should be used for applications of expression fun. * This is a generalization of ExprManager::operatorToKind that also @@ -379,19 +377,19 @@ public: * APPLY_UF if fun has function type, * APPLY_CONSTRUCTOR if fun has constructor type. */ - Kind getKindForFunction(Expr fun); - + api::Kind getKindForFunction(api::Term fun); + /** * Returns a sort, given a name. * @param sort_name the name to look up */ - Type getSort(const std::string& sort_name); + api::Sort getSort(const std::string& sort_name); /** * Returns a (parameterized) sort, given a name and args. */ - Type getSort(const std::string& sort_name, - const std::vector<Type>& params); + api::Sort getSort(const std::string& sort_name, + const std::vector<api::Sort>& params); /** * Returns arity of a (parameterized) sort, given a name and args. @@ -434,28 +432,7 @@ public: * @throws ParserException if checks are enabled and fun is not * a function */ - void checkFunctionLike(Expr fun); - - /** - * Check that <code>kind</code> can accept <code>numArgs</code> arguments. - * @param kind the built-in operator to check - * @param numArgs the number of actual arguments - * @throws ParserException if checks are enabled and the operator - * <code>kind</code> cannot be applied to <code>numArgs</code> - * arguments. - */ - void checkArity(Kind kind, unsigned numArgs); - - /** - * Check that <code>kind</code> is a legal operator in the current - * logic and that it can accept <code>numArgs</code> arguments. - * - * @param kind the built-in operator to check - * @param numArgs the number of actual arguments - * @throws ParserException if the parser mode is strict and the - * operator <code>kind</code> has not been enabled - */ - void checkOperator(Kind kind, unsigned numArgs); + void checkFunctionLike(api::Term fun); /** Create a new CVC4 variable expression of the given type. * @@ -466,9 +443,10 @@ public: * then if doOverload is true, we create overloaded operators. * else if doOverload is false, the existing expression is shadowed by the new expression. */ - Expr mkVar(const std::string& name, const Type& type, - uint32_t flags = ExprManager::VAR_FLAG_NONE, - bool doOverload = false); + api::Term bindVar(const std::string& name, + const api::Sort& type, + uint32_t flags = ExprManager::VAR_FLAG_NONE, + bool doOverload = false); /** * Create a set of new CVC4 variable expressions of the given type. @@ -480,23 +458,23 @@ public: * then if doOverload is true, we create overloaded operators. * else if doOverload is false, the existing expression is shadowed by the new expression. */ - std::vector<Expr> - mkVars(const std::vector<std::string> names, const Type& type, - uint32_t flags = ExprManager::VAR_FLAG_NONE, - bool doOverload = false); + std::vector<api::Term> bindVars(const std::vector<std::string> names, + const api::Sort& type, + uint32_t flags = ExprManager::VAR_FLAG_NONE, + bool doOverload = false); /** * Create a new CVC4 bound variable expression of the given type. This binds * the symbol name to that variable in the current scope. */ - Expr mkBoundVar(const std::string& name, const Type& type); + api::Term bindBoundVar(const std::string& name, const api::Sort& type); /** * Create a new CVC4 bound variable expressions of the given names and types. * Like the method above, this binds these names to those variables in the * current scope. */ - std::vector<Expr> mkBoundVars( - std::vector<std::pair<std::string, Type> >& sortedVarNames); + std::vector<api::Term> bindBoundVars( + std::vector<std::pair<std::string, api::Sort> >& sortedVarNames); /** * Create a set of new CVC4 bound variable expressions of the given type. @@ -508,7 +486,8 @@ public: * then if doOverload is true, we create overloaded operators. * else if doOverload is false, the existing expression is shadowed by the new expression. */ - std::vector<Expr> mkBoundVars(const std::vector<std::string> names, const Type& type); + std::vector<api::Term> bindBoundVars(const std::vector<std::string> names, + const api::Sort& type); /** * Create a new CVC4 function expression of the given type, @@ -518,8 +497,9 @@ public: * flags specify information about the variable, e.g. whether it is global or defined * (see enum in expr_manager_template.h). */ - Expr mkAnonymousFunction(const std::string& prefix, const Type& type, - uint32_t flags = ExprManager::VAR_FLAG_NONE); + api::Term mkAnonymousFunction(const std::string& prefix, + const api::Sort& type, + uint32_t flags = ExprManager::VAR_FLAG_NONE); /** Create a new variable definition (e.g., from a let binding). * levelZero is set if the binding must be done at level 0. @@ -527,8 +507,10 @@ public: * then if doOverload is true, we create overloaded operators. * else if doOverload is false, the existing expression is shadowed by the new expression. */ - void defineVar(const std::string& name, const Expr& val, - bool levelZero = false, bool doOverload = false); + void defineVar(const std::string& name, + const api::Term& val, + bool levelZero = false, + bool doOverload = false); /** * Create a new type definition. @@ -539,7 +521,7 @@ public: * cannot be removed by poppoing the user context */ void defineType(const std::string& name, - const Type& type, + const api::Sort& type, bool levelZero = false); /** @@ -552,46 +534,44 @@ public: * cannot be removed by poppoing the user context */ void defineType(const std::string& name, - const std::vector<Type>& params, - const Type& type, + const std::vector<api::Sort>& params, + const api::Sort& type, bool levelZero = false); /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */ void defineParameterizedType(const std::string& name, - const std::vector<Type>& params, - const Type& type); + const std::vector<api::Sort>& params, + const api::Sort& type); /** * Creates a new sort with the given name. */ - SortType mkSort(const std::string& name, - uint32_t flags = ExprManager::SORT_FLAG_NONE); + api::Sort mkSort(const std::string& name, + uint32_t flags = ExprManager::SORT_FLAG_NONE); /** * Creates a new sort constructor with the given name and arity. */ - SortConstructorType mkSortConstructor( - const std::string& name, - size_t arity, - uint32_t flags = ExprManager::SORT_FLAG_NONE); + api::Sort mkSortConstructor(const std::string& name, + size_t arity, + uint32_t flags = ExprManager::SORT_FLAG_NONE); /** * Creates a new "unresolved type," used only during parsing. */ - SortType mkUnresolvedType(const std::string& name); + api::Sort mkUnresolvedType(const std::string& name); /** * Creates a new unresolved (parameterized) type constructor of the given * arity. */ - SortConstructorType mkUnresolvedTypeConstructor(const std::string& name, - size_t arity); + api::Sort mkUnresolvedTypeConstructor(const std::string& name, size_t arity); /** * Creates a new unresolved (parameterized) type constructor given the type * parameters. */ - SortConstructorType mkUnresolvedTypeConstructor(const std::string& name, - const std::vector<Type>& params); + api::Sort mkUnresolvedTypeConstructor(const std::string& name, + const std::vector<api::Sort>& params); /** * Returns true IFF name is an unresolved type. @@ -651,9 +631,9 @@ public: * where @ is (higher-order) application. In this example, z is added to * flattenVars. */ - Type mkFlatFunctionType(std::vector<Type>& sorts, - Type range, - std::vector<Expr>& flattenVars); + api::Sort mkFlatFunctionType(std::vector<api::Sort>& sorts, + api::Sort range, + std::vector<api::Term>& flattenVars); /** make flat function type * @@ -661,7 +641,7 @@ public: * This is used when the arguments of the function are not important (for * instance, if we are only using this type in a declare-fun). */ - Type mkFlatFunctionType(std::vector<Type>& sorts, Type range); + api::Sort mkFlatFunctionType(std::vector<api::Sort>& sorts, api::Sort range); /** make higher-order apply * @@ -676,7 +656,7 @@ public: * for each i where 0 <= i < args.size(). If expr is not of this * type, the expression returned by this method will not be well typed. */ - Expr mkHoApply(Expr expr, std::vector<Expr>& args); + api::Term mkHoApply(api::Term expr, const std::vector<api::Term>& args); /** Apply type ascription * @@ -702,12 +682,21 @@ public: */ api::Term applyTypeAscription(api::Term t, api::Sort s); + //!!!!!!!!!!! temporary + /** + * Make var, with flags required by the ExprManager, see ExprManager::mkVar. + */ + api::Term mkVar(const std::string& name, + const api::Sort& type, + uint32_t flags); + //!!!!!!!!!!! temporary + /** * Add an operator to the current legal set. * * @param kind the built-in operator to add */ - void addOperator(Kind kind); + void addOperator(api::Kind kind); /** * Preempt the next returned command with other ones; used to @@ -723,7 +712,7 @@ public: /** Is fun a function (or function-like thing)? * Currently this means its type is either a function, constructor, tester, or selector. */ - bool isFunctionLike(Expr fun); + bool isFunctionLike(api::Term fun); /** Is the symbol bound to a predicate? */ bool isPredicate(const std::string& name); @@ -864,25 +853,30 @@ public: //------------------------ operator overloading /** is this function overloaded? */ - bool isOverloadedFunction(Expr fun) { - return d_symtab->isOverloadedFunction(fun); + bool isOverloadedFunction(api::Term fun) + { + return d_symtab->isOverloadedFunction(fun.getExpr()); } - + /** Get overloaded constant for type. * If possible, it returns a defined symbol with name * that has type t. Otherwise returns null expression. */ - Expr getOverloadedConstantForType(const std::string& name, Type t) { - return d_symtab->getOverloadedConstantForType(name, t); + api::Term getOverloadedConstantForType(const std::string& name, api::Sort t) + { + return d_symtab->getOverloadedConstantForType(name, t.getType()); } - + /** * If possible, returns a defined function for a name * and a vector of expected argument types. Otherwise returns * null expression. */ - Expr getOverloadedFunctionForTypes(const std::string& name, std::vector< Type >& argTypes) { - return d_symtab->getOverloadedFunctionForTypes(name, argTypes); + api::Term getOverloadedFunctionForTypes(const std::string& name, + std::vector<api::Sort>& argTypes) + { + return d_symtab->getOverloadedFunctionForTypes( + name, api::sortVectorToTypes(argTypes)); } //------------------------ end operator overloading };/* class Parser */ |