diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 55a1b93d9..15bcedcb0 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -62,7 +62,7 @@ DEFINE_TYPE(Z3_rcf_num); - \c Z3_constructor: type constructor for a (recursive) datatype. - \c Z3_constructor_list: list of constructors for a (recursive) datatype. - \c Z3_params: parameter set used to configure many components such as: simplifiers, tactics, solvers, etc. - - \c Z3_param_descrs: provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters. + - \c Z3_param_descrs: provides a collection of parameter names, their types, default values and documentation strings. Solvers, tactics, and other objects accept different collection of parameters. - \c Z3_model: model for the constraints asserted into the logical context. - \c Z3_func_interp: interpretation of a function in a model. - \c Z3_func_entry: representation of the value of a \c Z3_func_interp at a particular point. @@ -1129,7 +1129,7 @@ typedef enum { Z3_OP_SEQ_EXTRACT, Z3_OP_SEQ_REPLACE, Z3_OP_SEQ_AT, - Z3_OP_SEQ_LENGTH, + Z3_OP_SEQ_LENGTH, Z3_OP_SEQ_INDEX, Z3_OP_SEQ_TO_RE, Z3_OP_SEQ_IN_RE, @@ -3185,11 +3185,11 @@ extern "C" { def_API('Z3_is_string', BOOL, (_in(CONTEXT), _in(AST))) */ - Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s); + Z3_bool Z3_API Z3_is_string(Z3_context c, Z3_ast s); /** \brief Retrieve the string constant stored in \c s. - + \pre Z3_is_string(c, s) def_API('Z3_get_string' ,STRING ,(_in(CONTEXT), _in(AST))) @@ -3285,7 +3285,7 @@ extern "C" { def_API('Z3_mk_seq_index' ,AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) */ Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset); - + /** \brief Create a regular expression that accepts the sequence \c seq. @@ -4429,8 +4429,8 @@ extern "C" { Provides an interface to the AST simplifier used by Z3. It returns an AST object which is equal to the argument. - The returned AST is simplified using algebraic simplificaiton rules, - such as constant propagation (propagating true/false over logical connectives). + The returned AST is simplified using algebraic simplificaiton rules, + such as constant propagation (propagating true/false over logical connectives). def_API('Z3_simplify', AST, (_in(CONTEXT), _in(AST))) */