mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

regenerated ml api

Browse source
This commit is contained in:
Josh Berdine 2012-10-07 00:08:11 +01:00
parent c0c98f7d09
commit cc940eb18e
3 changed files with 10030 additions and 10030 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
ml/z3.ml
View file

@ -1038,6 +1038,9 @@ external get_quantifier_num_no_patterns : context -> ast -> int
external get_quantifier_no_pattern_ast : context -> ast -> int -> ast
= "camlidl_z3_Z3_get_quantifier_no_pattern_ast"
external get_quantifier_num_bound : context -> ast -> int
= "camlidl_z3_Z3_get_quantifier_num_bound"
external get_quantifier_bound_name : context -> ast -> int -> symbol
= "camlidl_z3_Z3_get_quantifier_bound_name"
@ -1047,9 +1050,6 @@ external get_quantifier_bound_sort : context -> ast -> int -> sort
external get_quantifier_body : context -> ast -> ast
= "camlidl_z3_Z3_get_quantifier_body"
external get_quantifier_num_bound : context -> ast -> int
= "camlidl_z3_Z3_get_quantifier_num_bound"
external simplify : context -> ast -> ast
= "camlidl_z3_Z3_simplify"
@ -2830,6 +2830,9 @@ external get_quantifier_num_no_patterns : context -> ast -> int
external get_quantifier_no_pattern_ast : context -> ast -> int -> ast
= "camlidl_z3V3_Z3_get_quantifier_no_pattern_ast"
external get_quantifier_num_bound : context -> ast -> int
= "camlidl_z3V3_Z3_get_quantifier_num_bound"
external get_quantifier_bound_name : context -> ast -> int -> symbol
= "camlidl_z3V3_Z3_get_quantifier_bound_name"
@ -2839,9 +2842,6 @@ external get_quantifier_bound_sort : context -> ast -> int -> sort
external get_quantifier_body : context -> ast -> ast
= "camlidl_z3V3_Z3_get_quantifier_body"
external get_quantifier_num_bound : context -> ast -> int
= "camlidl_z3V3_Z3_get_quantifier_num_bound"
external simplify : context -> ast -> ast
= "camlidl_z3V3_Z3_simplify"

40
ml/z3.mli
View file

@ -2741,8 +2741,8 @@ external mk_quantifier : context -> bool -> int -> pattern array -> sort array -
@param weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
@param num_patterns number of patterns.
@param patterns array containing the patterns created using {!mk_pattern}.
@param num_no_patterns number of patterns.
@param no_patterns array containing the patterns created using {!mk_pattern}.
@param num_no_patterns number of no_patterns.
@param no_patterns array containing subexpressions to be excluded from inferred patterns.
@param num_decls number of variables to be bound.
@param sorts array of sorts of the bound variables.
@param decl_names names of the bound variables.
@ -3585,6 +3585,14 @@ external get_quantifier_num_no_patterns : context -> ast -> int
external get_quantifier_no_pattern_ast : context -> ast -> int -> ast
= "camlidl_z3_Z3_get_quantifier_no_pattern_ast"
(**
Summary: Return number of bound variables of quantifier.
- {b Precondition}: get_ast_kind a == QUANTIFIER_AST
*)
external get_quantifier_num_bound : context -> ast -> int
= "camlidl_z3_Z3_get_quantifier_num_bound"
(**
Summary: Return symbol of the i'th bound variable.
@ -3609,14 +3617,6 @@ external get_quantifier_bound_sort : context -> ast -> int -> sort
external get_quantifier_body : context -> ast -> ast
= "camlidl_z3_Z3_get_quantifier_body"
(**
Summary: Return number of bound variables of quantifier.
- {b Precondition}: get_ast_kind a == QUANTIFIER_AST
*)
external get_quantifier_num_bound : context -> ast -> int
= "camlidl_z3_Z3_get_quantifier_num_bound"
(**
{3 {L Simplification}}
*)
@ -7737,8 +7737,8 @@ external mk_quantifier : context -> bool -> int -> pattern array -> sort array -
@param weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
@param num_patterns number of patterns.
@param patterns array containing the patterns created using {!mk_pattern}.
@param num_no_patterns number of patterns.
@param no_patterns array containing the patterns created using {!mk_pattern}.
@param num_no_patterns number of no_patterns.
@param no_patterns array containing subexpressions to be excluded from inferred patterns.
@param num_decls number of variables to be bound.
@param sorts array of sorts of the bound variables.
@param decl_names names of the bound variables.
@ -8500,6 +8500,14 @@ external get_quantifier_num_no_patterns : context -> ast -> int
external get_quantifier_no_pattern_ast : context -> ast -> int -> ast
= "camlidl_z3V3_Z3_get_quantifier_no_pattern_ast"
(**
Summary: Return number of bound variables of quantifier.
- {b Precondition}: get_ast_kind a == QUANTIFIER_AST
*)
external get_quantifier_num_bound : context -> ast -> int
= "camlidl_z3V3_Z3_get_quantifier_num_bound"
(**
Summary: Return symbol of the i'th bound variable.
@ -8524,14 +8532,6 @@ external get_quantifier_bound_sort : context -> ast -> int -> sort
external get_quantifier_body : context -> ast -> ast
= "camlidl_z3V3_Z3_get_quantifier_body"
(**
Summary: Return number of bound variables of quantifier.
- {b Precondition}: get_ast_kind a == QUANTIFIER_AST
*)
external get_quantifier_num_bound : context -> ast -> int
= "camlidl_z3V3_Z3_get_quantifier_num_bound"
(**
{3 {L Simplification}}
*)

82
ml/z3_stubs.c
View file

@ -6661,6 +6661,28 @@ check_error_code(c);
return _vres;
}
value camlidl_z3_Z3_get_quantifier_num_bound(
value _v_c,
value _v_a)
{
Z3_context c; /*in*/
Z3_ast a; /*in*/
unsigned int _res;
value _vres;
struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };
camlidl_ctx _ctx = &_ctxs;
camlidl_ml2c_z3_Z3_context(_v_c, &c, _ctx);
camlidl_ml2c_z3_Z3_ast(_v_a, &a, _ctx);
_res = Z3_get_quantifier_num_bound(c, a);
_vres = Val_int(_res);
camlidl_free(_ctx);
/* begin user-supplied deallocation sequence */
check_error_code(c);
/* end user-supplied deallocation sequence */
return _vres;
}
value camlidl_z3_Z3_get_quantifier_bound_name(
value _v_c,
value _v_a,
@ -6733,28 +6755,6 @@ check_error_code(c);
return _vres;
}
value camlidl_z3_Z3_get_quantifier_num_bound(
value _v_c,
value _v_a)
{
Z3_context c; /*in*/
Z3_ast a; /*in*/
unsigned int _res;
value _vres;
struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };
camlidl_ctx _ctx = &_ctxs;
camlidl_ml2c_z3_Z3_context(_v_c, &c, _ctx);
camlidl_ml2c_z3_Z3_ast(_v_a, &a, _ctx);
_res = Z3_get_quantifier_num_bound(c, a);
_vres = Val_int(_res);
camlidl_free(_ctx);
/* begin user-supplied deallocation sequence */
check_error_code(c);
/* end user-supplied deallocation sequence */
return _vres;
}
value camlidl_z3_Z3_simplify(
value _v_c,
value _v_a)
@ -16691,6 +16691,25 @@ value camlidl_z3V3_Z3_get_quantifier_no_pattern_ast(
return _vres;
}
value camlidl_z3V3_Z3_get_quantifier_num_bound(
value _v_c,
value _v_a)
{
Z3_context c; /*in*/
Z3_ast a; /*in*/
unsigned int _res;
value _vres;
struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };
camlidl_ctx _ctx = &_ctxs;
camlidl_ml2c_z3V3_Z3_context(_v_c, &c, _ctx);
camlidl_ml2c_z3V3_Z3_ast(_v_a, &a, _ctx);
_res = Z3_get_quantifier_num_bound(c, a);
_vres = Val_int(_res);
camlidl_free(_ctx);
return _vres;
}
value camlidl_z3V3_Z3_get_quantifier_bound_name(
value _v_c,
value _v_a,
@ -16754,25 +16773,6 @@ value camlidl_z3V3_Z3_get_quantifier_body(
return _vres;
}
value camlidl_z3V3_Z3_get_quantifier_num_bound(
value _v_c,
value _v_a)
{
Z3_context c; /*in*/
Z3_ast a; /*in*/
unsigned int _res;
value _vres;
struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };
camlidl_ctx _ctx = &_ctxs;
camlidl_ml2c_z3V3_Z3_context(_v_c, &c, _ctx);
camlidl_ml2c_z3V3_Z3_ast(_v_a, &a, _ctx);
_res = Z3_get_quantifier_num_bound(c, a);
_vres = Val_int(_res);
camlidl_free(_ctx);
return _vres;
}
value camlidl_z3V3_Z3_simplify(
value _v_c,
value _v_a)