mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-03-05 17:55:27 +00:00
parent 03a8ef2795
commit 8abedbf389
1 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/api/z3_api.h
View file

@ -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)))
*/