diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-27 14:55:55 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-27 16:46:22 -0400 |
commit | a399bd138c387820e0d441372a7dbe7bee1dd0f4 (patch) | |
tree | 4d3e778a31fa1c1d679f1e49f33fc8a508e1105b /src/expr | |
parent | ba893aaccd2f60168db6a50eccd947d7cf7f3069 (diff) |
Better user documentation for mkVar() and mkBoundVar().
Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_manager_template.h | 62 |
1 files changed, 61 insertions, 1 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index fd81c9bf8..15278dfb6 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -468,10 +468,70 @@ public: Type getType(Expr e, bool check = false) throw(TypeCheckingException); - // variables are special, because duplicates are permitted + /** + * Create a new, fresh variable. This variable is guaranteed to be + * distinct from every variable thus far in the ExprManager, even + * if it shares a name with another; this is to support any kind of + * scoping policy on top of ExprManager. The SymbolTable class + * can be used to store and lookup symbols by name, if desired. + * + * @param name a name to associate to the fresh new variable + * @param type the type for the new variable + * @param isGlobal whether this variable is to be considered "global" + * or not. Note that this information isn't used by the ExprManager, + * but is passed on to the ExprManager's event subscribers like the + * model-building service; if isGlobal is true, this newly-created + * variable will still available in models generated after an + * intervening pop. + */ Expr mkVar(const std::string& name, Type type, bool isGlobal = false); + + /** + * Create a (nameless) new, fresh variable. This variable is guaranteed + * to be distinct from every variable thus far in the ExprManager. + * + * @param type the type for the new variable + * @param isGlobal whether this variable is to be considered "global" + * or not. Note that this information isn't used by the ExprManager, + * but is passed on to the ExprManager's event subscribers like the + * model-building service; if isGlobal is true, this newly-created + * variable will still available in models generated after an + * intervening pop. + */ Expr mkVar(Type type, bool isGlobal = false); + + /** + * Create a new, fresh variable for use in a binder expression + * (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA). It is + * an error for this bound variable to exist outside of a binder, + * and it should also only be used in a single binder expression. + * That is, two distinct FORALL expressions should use entirely + * disjoint sets of bound variables (however, a single FORALL + * expression can be used in multiple places in a formula without + * a problem). This newly-created bound variable is guaranteed to + * be distinct from every variable thus far in the ExprManager, even + * if it shares a name with another; this is to support any kind of + * scoping policy on top of ExprManager. The SymbolTable class + * can be used to store and lookup symbols by name, if desired. + * + * @param name a name to associate to the fresh new bound variable + * @param type the type for the new bound variable + */ Expr mkBoundVar(const std::string& name, Type type); + + /** + * Create a (nameless) new, fresh variable for use in a binder + * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, or LAMBDA). + * It is an error for this bound variable to exist outside of a + * binder, and it should also only be used in a single binder + * expression. That is, two distinct FORALL expressions should use + * entirely disjoint sets of bound variables (however, a single FORALL + * expression can be used in multiple places in a formula without + * a problem). This newly-created bound variable is guaranteed to + * be distinct from every variable thus far in the ExprManager. + * + * @param type the type for the new bound variable + */ Expr mkBoundVar(Type type); /** Get a reference to the statistics registry for this ExprManager */ |