mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

regenerated ml api

Browse source
This commit is contained in:
Josh Berdine 2012-10-22 03:37:57 +01:00
parent 8231d1cbcf
commit d71595fc1c
3 changed files with 1545 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ml/z3.ml
View file

@ -198,6 +198,7 @@ and decl_kind =
| OP_PR_SKOLEMIZE
| OP_PR_MODUS_PONENS_OEQ
| OP_PR_TH_LEMMA
| OP_PR_HYPER_RESOLVE
| OP_RA_STORE
| OP_RA_EMPTY
| OP_RA_IS_EMPTY
@ -342,6 +343,9 @@ external param_descrs_size : context -> param_descrs -> int
external param_descrs_get_name : context -> param_descrs -> int -> symbol
= "camlidl_z3_Z3_param_descrs_get_name"
external param_descrs_to_string : context -> param_descrs -> string
= "camlidl_z3_Z3_param_descrs_to_string"
(**
Refined view of a {!symbol}.
@ -2153,6 +2157,7 @@ and decl_kind =
| OP_PR_SKOLEMIZE
| OP_PR_MODUS_PONENS_OEQ
| OP_PR_TH_LEMMA
| OP_PR_HYPER_RESOLVE
| OP_RA_STORE
| OP_RA_EMPTY
| OP_RA_IS_EMPTY

1522
ml/z3.mli
View file

File diff suppressed because it is too large Load diff

32
ml/z3_stubs.c
View file

@ -416,7 +416,7 @@ value _v1;
return _v1;
}
int camlidl_transl_table_z3_enum_6[151] = {
int camlidl_transl_table_z3_enum_6[152] = {
Z3_OP_TRUE,
Z3_OP_FALSE,
Z3_OP_EQ,
@ -548,6 +548,7 @@ int camlidl_transl_table_z3_enum_6[151] = {
Z3_OP_PR_SKOLEMIZE,
Z3_OP_PR_MODUS_PONENS_OEQ,
Z3_OP_PR_TH_LEMMA,
Z3_OP_PR_HYPER_RESOLVE,
Z3_OP_RA_STORE,
Z3_OP_RA_EMPTY,
Z3_OP_RA_IS_EMPTY,
@ -578,7 +579,7 @@ void camlidl_ml2c_z3_Z3_decl_kind(value _v1, Z3_decl_kind * _c2, camlidl_ctx _ct
value camlidl_c2ml_z3_Z3_decl_kind(Z3_decl_kind * _c2, camlidl_ctx _ctx)
{
value _v1;
_v1 = camlidl_find_enum((*_c2), camlidl_transl_table_z3_enum_6, 151, "typedef Z3_decl_kind: bad enum value");
_v1 = camlidl_find_enum((*_c2), camlidl_transl_table_z3_enum_6, 152, "typedef Z3_decl_kind: bad enum value");
return _v1;
}
@ -1063,6 +1064,28 @@ check_error_code(c);
return _vres;
}
value camlidl_z3_Z3_param_descrs_to_string(
value _v_c,
value _v_p)
{
Z3_context c; /*in*/
Z3_param_descrs p; /*in*/
Z3_string _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_param_descrs(_v_p, &p, _ctx);
_res = Z3_param_descrs_to_string(c, p);
_vres = camlidl_c2ml_z3_Z3_string(&_res, _ctx);
camlidl_free(_ctx);
/* begin user-supplied deallocation sequence */
check_error_code(c);
/* end user-supplied deallocation sequence */
return _vres;
}
value camlidl_z3_Z3_mk_int_symbol(
value _v_c,
value _v_i)
@ -11344,7 +11367,7 @@ value _v1;
return _v1;
}
int camlidl_transl_table_z3V3_enum_6[151] = {
int camlidl_transl_table_z3V3_enum_6[152] = {
Z3_OP_TRUE,
Z3_OP_FALSE,
Z3_OP_EQ,
@ -11476,6 +11499,7 @@ int camlidl_transl_table_z3V3_enum_6[151] = {
Z3_OP_PR_SKOLEMIZE,
Z3_OP_PR_MODUS_PONENS_OEQ,
Z3_OP_PR_TH_LEMMA,
Z3_OP_PR_HYPER_RESOLVE,
Z3_OP_RA_STORE,
Z3_OP_RA_EMPTY,
Z3_OP_RA_IS_EMPTY,
@ -11506,7 +11530,7 @@ void camlidl_ml2c_z3V3_Z3_decl_kind(value _v1, Z3_decl_kind * _c2, camlidl_ctx _
value camlidl_c2ml_z3V3_Z3_decl_kind(Z3_decl_kind * _c2, camlidl_ctx _ctx)
{
value _v1;
_v1 = camlidl_find_enum((*_c2), camlidl_transl_table_z3V3_enum_6, 151, "typedef Z3_decl_kind: bad enum value");
_v1 = camlidl_find_enum((*_c2), camlidl_transl_table_z3V3_enum_6, 152, "typedef Z3_decl_kind: bad enum value");
return _v1;
}