diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-23 20:07:19 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-23 20:07:19 -0600 |
commit | 612509379a1417f8d4a5e001ff143ba819f5516f (patch) | |
tree | 764c379a42fa29ec36d9c83d448901c975e2fa29 /src/parser/smt2/smt2.h | |
parent | c9ae6b9812e737ae7932df91fa5f334d6d2588d4 (diff) |
Ho parsing and regressions (#1350)
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r-- | src/parser/smt2/smt2.h | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 84c049ce9..835ff2b58 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -91,6 +91,52 @@ public: */ virtual Expr getExpressionForNameAndType(const std::string& name, Type t); + /** Make function defined by a define-fun(s)-rec command. + * + * fname : the name of the function. + * sortedVarNames : the list of variable arguments for the function. + * t : the range type of the function we are defining. + * + * This function will create a bind a new function term to name fname. + * The type of this function is + * Parser::mkFlatFunctionType(sorts,t,flattenVars), + * where sorts are the types in the second components of sortedVarNames. + * As descibed in Parser::mkFlatFunctionType, new bound variables may be + * added to flattenVars in this function if the function is given a function + * range type. + */ + Expr mkDefineFunRec( + const std::string& fname, + const std::vector<std::pair<std::string, Type> >& sortedVarNames, + Type t, + std::vector<Expr>& flattenVars); + + /** Push scope for define-fun-rec + * + * This calls Parser::pushScope(bindingLevel) and sets up + * initial information for reading a body of a function definition + * in the define-fun-rec and define-funs-rec command. + * The input parameters func/flattenVars are the result + * of a call to mkDefineRec above. + * + * func : the function whose body we are defining. + * sortedVarNames : the list of variable arguments for the function. + * flattenVars : the implicit variables introduced when defining func. + * + * This function: + * (1) Calls Parser::pushScope(bindingLevel). + * (2) Computes the bound variable list for the quantified formula + * that defined this definition and stores it in bvs. + * (3) Sets func_app to the APPLY_UF with func applied to bvs. + */ + void pushDefineFunRecScope( + const std::vector<std::pair<std::string, Type> >& sortedVarNames, + Expr func, + const std::vector<Expr>& flattenVars, + Expr& func_app, + std::vector<Expr>& bvs, + bool bindingLevel = false); + void reset(); void resetAssertions(); |