sort out terminology/add explanations, add shortcut to C++, fix Z3Pro…

…ver#6491

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/c++/z3++.h

@@ -366,8 +366,14 @@ namespace z3 {
         void      recdef(func_decl, expr_vector const& args, expr const& body);
         func_decl user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range);
 
+        /**
+           \brief create an uninterpreted constant.
+         */
         expr constant(symbol const & name, sort const & s);
         expr constant(char const * name, sort const & s);
+        /**
+           \brief create uninterpreted constants of a given sort.
+         */
         expr bool_const(char const * name);
         expr int_const(char const * name);
         expr real_const(char const * name);
@@ -378,6 +384,12 @@ namespace z3 {
         template<size_t precision>
         expr fpa_const(char const * name);
 
+        /**
+           \brief create a de-Bruijn variable.
+         */
+        expr variable(unsigned index, sort const& s);
+
+
         expr fpa_rounding_mode();
 
         expr bool_val(bool b);
@@ -3580,6 +3592,11 @@ namespace z3 {
         return expr(*this, r);
     }
     inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
+    inline expr context::variable(unsigned idx, sort const& s) { 
+        Z3_ast r = Z3_mk_bound(m_ctx, idx, s);
+        check_error();
+        return expr(*this, r);
+    }
     inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
     inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
     inline expr context::real_const(char const * name) { return constant(name, real_sort()); }

src/api/python/z3/z3.py

@@ -1469,7 +1469,9 @@ def FreshConst(sort, prefix="c"):
 
 def Var(idx, s):
     """Create a Z3 free variable. Free variables are used to create quantified formulas.
-
+    A free variable with index n is bound when it occurs within the scope of n+1 quantified
+    declarations.
+    
     >>> Var(0, IntSort())
     Var(0)
     >>> eq(Var(0, IntSort()), Var(0, BoolSort()))

src/api/z3_api.h

@@ -4051,7 +4051,10 @@ extern "C" {
     Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[]);
 
     /**
-       \brief Create a bound variable.
+       \brief Create a variable. 
+
+       Variables are intended to be bound by a scope created by a quantifier. So we call them bound variables
+       even if they appear as free variables in the expression produced by \c Z3_mk_bound.
 
        Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain
        the meaning of de-Bruijn indices by indicating the compilation process from
@@ -5318,8 +5321,9 @@ extern "C" {
                                 Z3_ast const to[]);
 
     /**
-       \brief Substitute the free variables in \c a with the expressions in \c to.
+       \brief Substitute the variables in \c a with the expressions in \c to.
        For every \c i smaller than \c num_exprs, the variable with de-Bruijn index \c i is replaced with term \ccode{to[i]}.
+       Note that a variable is created using the function \ref Z3_mk_bound. 
 
        def_API('Z3_substitute_vars', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
     */