mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

sort out terminology/add explanations, add shortcut to C++, fix #6491

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-13 16:17:38 -08:00
parent 2d7a38e95e
commit cd3d38caf7
3 changed files with 26 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/api/c++/z3++.h
View file

@ -366,8 +366,14 @@ namespace z3 {
void recdef(func_decl, expr_vector const& args, expr const& body); 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); 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(symbol const & name, sort const & s);
expr constant(char 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 bool_const(char const * name);
expr int_const(char const * name); expr int_const(char const * name);
expr real_const(char const * name); expr real_const(char const * name);
@ -378,6 +384,12 @@ namespace z3 {
template<size_t precision> template<size_t precision>
expr fpa_const(char const * name); expr fpa_const(char const * name);
/**
\brief create a de-Bruijn variable.
*/
expr variable(unsigned index, sort const& s);
expr fpa_rounding_mode(); expr fpa_rounding_mode();
expr bool_val(bool b); expr bool_val(bool b);
@ -3580,6 +3592,11 @@ namespace z3 {
return expr(*this, r); return expr(*this, r);
} }
inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); } 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::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::int_const(char const * name) { return constant(name, int_sort()); }
inline expr context::real_const(char const * name) { return constant(name, real_sort()); } inline expr context::real_const(char const * name) { return constant(name, real_sort()); }

4
src/api/python/z3/z3.py
View file

@ -1469,7 +1469,9 @@ def FreshConst(sort, prefix="c"):
def Var(idx, s): def Var(idx, s):
"""Create a Z3 free variable. Free variables are used to create quantified formulas. """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, IntSort())
Var(0) Var(0)
>>> eq(Var(0, IntSort()), Var(0, BoolSort())) >>> eq(Var(0, IntSort()), Var(0, BoolSort()))

8
src/api/z3_api.h
View file

@ -4051,7 +4051,10 @@ extern "C" {
Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[]); 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 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 the meaning of de-Bruijn indices by indicating the compilation process from
@ -5318,8 +5321,9 @@ extern "C" {
Z3_ast const to[]); 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]}. 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))) def_API('Z3_substitute_vars', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
*/ */