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

Regenerate ml api

Browse source
This commit is contained in:
Josh Berdine 2012-12-20 12:58:21 +00:00
parent a7f89dcdd2
commit d7b8110cc8
3 changed files with 84 additions and 134 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/api/ml/z3.ml
View file

@ -229,16 +229,6 @@ and param_kind =
| PK_OTHER
| PK_INVALID
and search_failure =
| NO_FAILURE
| UNKNOWN
| TIMEOUT
| MEMOUT_WATERMARK
| CANCELED
| NUM_CONFLICTS
| THEORY
| QUANTIFIERS
and ast_print_mode =
| PRINT_SMTLIB_FULL
| PRINT_LOW_LEVEL
@ -1598,6 +1588,9 @@ external stats_get_uint_value : context -> stats -> int -> int
external stats_get_double_value : context -> stats -> int -> float
= "camlidl_z3_Z3_stats_get_double_value"
external get_implied_equalities : context -> solver -> ast array -> lbool * int array
= "camlidl_z3_Z3_get_implied_equalities"
(* Internal auxiliary functions: *)
(*
@ -2988,9 +2981,6 @@ external check : context -> lbool
external check_assumptions : context -> ast array -> int -> ast array -> lbool * model * ast * int * ast array
= "camlidl_z3V3_Z3_check_assumptions"
external get_implied_equalities : context -> ast array -> lbool * int array
= "camlidl_z3V3_Z3_get_implied_equalities"
external del_model : context -> model -> unit
= "camlidl_z3V3_Z3_del_model"

71
src/api/ml/z3.mli
View file

@ -229,16 +229,6 @@ and param_kind =
| PK_OTHER
| PK_INVALID
and search_failure =
| NO_FAILURE
| UNKNOWN
| TIMEOUT
| MEMOUT_WATERMARK
| CANCELED
| NUM_CONFLICTS
| THEORY
| QUANTIFIERS
and ast_print_mode =
| PRINT_SMTLIB_FULL
| PRINT_LOW_LEVEL
@ -866,23 +856,9 @@ and goal_prec =
- PK_OTHER all internal parameter kinds which are not exposed in the API.
- PK_INVALID invalid parameter.
*)
(**
{!search_failure}
The different kinds of search failure types.
- NO_FAILURE: The last search was successful
- UNKNOWN: Undocumented failure reason
- TIMEOUT: Timeout
- MEMOUT_WATERMAK: Search hit a memory high-watermak limit
- CANCELED: External cancel flag was set
- NUM_CONFLICTS: Maximum number of conflicts was reached
- THEORY: Theory is incomplete
- QUANTIFIERS: Logical context contains universal quantifiers
*)
(**
{!ast_print_mode}
Z3 pretty printing modes (See {!set_ast_print_mode}).
- PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose format.
- PRINT_LOW_LEVEL: Print AST nodes using a low-level format.
- PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x compliant format.
@ -891,7 +867,6 @@ and goal_prec =
(**
{!error_code}
Z3 error codes
- OK: No error.
- SORT_ERROR: User tried to build an invalid (type incorrect) AST.
- IOB: Index out of bounds.
@ -908,7 +883,6 @@ and goal_prec =
*)
(**
Definitions for update_api.py
def_Type('CONFIG', 'config', 'Config')
def_Type('CONTEXT', 'context', 'ContextObj')
def_Type('AST', 'ast', 'Ast')
@ -5043,6 +5017,30 @@ external stats_get_uint_value : context -> stats -> int -> int
external stats_get_double_value : context -> stats -> int -> float
= "camlidl_z3_Z3_stats_get_double_value"
(**
{2 {L Deprecated Constraints API}}
*)
(**
Summary: Retrieve congruence class representatives for terms.
The function can be used for relying on Z3 to identify equal terms under the current
set of assumptions. The array of terms and array of class identifiers should have
the same length. The class identifiers are numerals that are assigned to the same
value for their corresponding terms if the current context forces the terms to be
equal. You cannot deduce that terms corresponding to different numerals must be all different,
(especially when using non-convex theories).
All implied equalities are returned by this call.
This means that two terms map to the same class identifier if and only if
the current context implies that they are equal.
A side-effect of the function is a satisfiability check on the assertions on the solver that is passed in.
The function return L_FALSE if the current assertions are not satisfiable.
- {b See also}: {!check_and_get_model}
- {b See also}: {!check}
@deprecated To be moved outside of API.
def_API('get_implied_equalities', UINT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT)))
*)
external get_implied_equalities : context -> solver -> ast array -> lbool * int array
= "camlidl_z3_Z3_get_implied_equalities"
(**
{2 {L Legacy V3 API}}
@ -8941,27 +8939,6 @@ external check : context -> lbool
external check_assumptions : context -> ast array -> int -> ast array -> lbool * model * ast * int * ast array
= "camlidl_z3V3_Z3_check_assumptions"
(**
Summary: Retrieve congruence class representatives for terms.
The function can be used for relying on Z3 to identify equal terms under the current
set of assumptions. The array of terms and array of class identifiers should have
the same length. The class identifiers are numerals that are assigned to the same
value for their corresponding terms if the current context forces the terms to be
equal. You cannot deduce that terms corresponding to different numerals must be all different,
(especially when using non-convex theories).
All implied equalities are returned by this call.
This means that two terms map to the same class identifier if and only if
the current context implies that they are equal.
A side-effect of the function is a satisfiability check.
The function return L_FALSE if the current assertions are not satisfiable.
- {b See also}: {!check_and_get_model}
- {b See also}: {!check}
@deprecated Subsumed by solver API
def_API('get_implied_equalities', UINT, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _out_array(1, UINT)))
*)
external get_implied_equalities : context -> ast array -> lbool * int array
= "camlidl_z3V3_Z3_get_implied_equalities"
(**
Summary: Delete a model object.
- {b See also}: {!check_and_get_model}

131
src/api/ml/z3_stubs.c
View file

@ -594,30 +594,7 @@ value _v1;
return _v1;
}
int camlidl_transl_table_z3_enum_8[8] = {
Z3_NO_FAILURE,
Z3_UNKNOWN,
Z3_TIMEOUT,
Z3_MEMOUT_WATERMARK,
Z3_CANCELED,
Z3_NUM_CONFLICTS,
Z3_THEORY,
Z3_QUANTIFIERS,
};
void camlidl_ml2c_z3_Z3_search_failure(value _v1, Z3_search_failure * _c2, camlidl_ctx _ctx)
{
(*_c2) = camlidl_transl_table_z3_enum_8[Int_val(_v1)];
}
value camlidl_c2ml_z3_Z3_search_failure(Z3_search_failure * _c2, camlidl_ctx _ctx)
{
value _v1;
_v1 = camlidl_find_enum((*_c2), camlidl_transl_table_z3_enum_8, 8, "typedef Z3_search_failure: bad enum value");
return _v1;
}
int camlidl_transl_table_z3_enum_9[4] = {
int camlidl_transl_table_z3_enum_8[4] = {
Z3_PRINT_SMTLIB_FULL,
Z3_PRINT_LOW_LEVEL,
Z3_PRINT_SMTLIB_COMPLIANT,
@ -626,7 +603,7 @@ int camlidl_transl_table_z3_enum_9[4] = {
void camlidl_ml2c_z3_Z3_ast_print_mode(value _v1, Z3_ast_print_mode * _c2, camlidl_ctx _ctx)
{
(*_c2) = camlidl_transl_table_z3_enum_9[Int_val(_v1)];
(*_c2) = camlidl_transl_table_z3_enum_8[Int_val(_v1)];
}
value camlidl_c2ml_z3_Z3_ast_print_mode(Z3_ast_print_mode * _c2, camlidl_ctx _ctx)
@ -642,7 +619,7 @@ value _v1;
return _v1;
}
int camlidl_transl_table_z3_enum_10[13] = {
int camlidl_transl_table_z3_enum_9[13] = {
Z3_OK,
Z3_SORT_ERROR,
Z3_IOB,
@ -660,13 +637,13 @@ int camlidl_transl_table_z3_enum_10[13] = {
void camlidl_ml2c_z3_Z3_error_code(value _v1, Z3_error_code * _c2, camlidl_ctx _ctx)
{
(*_c2) = camlidl_transl_table_z3_enum_10[Int_val(_v1)];
(*_c2) = camlidl_transl_table_z3_enum_9[Int_val(_v1)];
}
value camlidl_c2ml_z3_Z3_error_code(Z3_error_code * _c2, camlidl_ctx _ctx)
{
value _v1;
_v1 = camlidl_find_enum((*_c2), camlidl_transl_table_z3_enum_10, 13, "typedef Z3_error_code: bad enum value");
_v1 = camlidl_find_enum((*_c2), camlidl_transl_table_z3_enum_9, 13, "typedef Z3_error_code: bad enum value");
return _v1;
}
@ -698,7 +675,7 @@ void check_error_code (Z3_context c)
/* Disable default error handler, all error checking is done by check_error_code */
void* error_handler_static = NULL;
int camlidl_transl_table_z3_enum_11[4] = {
int camlidl_transl_table_z3_enum_10[4] = {
Z3_GOAL_PRECISE,
Z3_GOAL_UNDER,
Z3_GOAL_OVER,
@ -707,7 +684,7 @@ int camlidl_transl_table_z3_enum_11[4] = {
void camlidl_ml2c_z3_Z3_goal_prec(value _v1, Z3_goal_prec * _c2, camlidl_ctx _ctx)
{
(*_c2) = camlidl_transl_table_z3_enum_11[Int_val(_v1)];
(*_c2) = camlidl_transl_table_z3_enum_10[Int_val(_v1)];
}
value camlidl_c2ml_z3_Z3_goal_prec(Z3_goal_prec * _c2, camlidl_ctx _ctx)
@ -11110,6 +11087,56 @@ check_error_code(c);
return _vres;
}
value camlidl_z3_Z3_get_implied_equalities(
value _v_c,
value _v_s,
value _v_terms)
{
Z3_context c; /*in*/
Z3_solver s; /*in*/
unsigned int num_terms; /*in*/
Z3_ast const *terms; /*in*/
unsigned int *class_ids; /*out*/
Z3_lbool _res;
struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };
camlidl_ctx _ctx = &_ctxs;
mlsize_t _c1;
mlsize_t _c2;
value _v3;
mlsize_t _c4;
value _v5;
value _vresult;
value _vres[2] = { 0, 0, };
camlidl_ml2c_z3_Z3_context(_v_c, &c, _ctx);
camlidl_ml2c_z3_Z3_solver(_v_s, &s, _ctx);
_c1 = Wosize_val(_v_terms);
terms = camlidl_malloc(_c1 * sizeof(Z3_ast const ), _ctx);
for (_c2 = 0; _c2 < _c1; _c2++) {
_v3 = Field(_v_terms, _c2);
camlidl_ml2c_z3_Z3_ast(_v3, &terms[_c2], _ctx);
}
num_terms = _c1;
class_ids = camlidl_malloc(num_terms * sizeof(unsigned int ), _ctx);
_res = Z3_get_implied_equalities(c, s, num_terms, terms, class_ids);
Begin_roots_block(_vres, 2)
_vres[0] = camlidl_c2ml_z3_Z3_lbool(&_res, _ctx);
_vres[1] = camlidl_alloc(num_terms, 0);
for (_c4 = 0; _c4 < num_terms; _c4++) {
_v5 = Val_int(class_ids[_c4]);
modify(&Field(_vres[1], _c4), _v5);
}
_vresult = camlidl_alloc_small(2, 0);
Field(_vresult, 0) = _vres[0];
Field(_vresult, 1) = _vres[1];
End_roots()
camlidl_free(_ctx);
/* begin user-supplied deallocation sequence */
check_error_code(c);
/* end user-supplied deallocation sequence */
return _vresult;
}
void camlidl_ml2c_z3V3_Z3_symbol(value _v1, Z3_symbol * _c2, camlidl_ctx _ctx)
{
*_c2 = *((Z3_symbol *) Bp_val(_v1));
@ -18321,50 +18348,6 @@ value camlidl_z3V3_Z3_check_assumptions(
return _vresult;
}
value camlidl_z3V3_Z3_get_implied_equalities(
value _v_c,
value _v_terms)
{
Z3_context c; /*in*/
unsigned int num_terms; /*in*/
Z3_ast const *terms; /*in*/
unsigned int *class_ids; /*out*/
Z3_lbool _res;
struct camlidl_ctx_struct _ctxs = { CAMLIDL_TRANSIENT, NULL };
camlidl_ctx _ctx = &_ctxs;
mlsize_t _c1;
mlsize_t _c2;
value _v3;
mlsize_t _c4;
value _v5;
value _vresult;
value _vres[2] = { 0, 0, };
camlidl_ml2c_z3V3_Z3_context(_v_c, &c, _ctx);
_c1 = Wosize_val(_v_terms);
terms = camlidl_malloc(_c1 * sizeof(Z3_ast const ), _ctx);
for (_c2 = 0; _c2 < _c1; _c2++) {
_v3 = Field(_v_terms, _c2);
camlidl_ml2c_z3V3_Z3_ast(_v3, &terms[_c2], _ctx);
}
num_terms = _c1;
class_ids = camlidl_malloc(num_terms * sizeof(unsigned int ), _ctx);
_res = Z3_get_implied_equalities(c, num_terms, terms, class_ids);
Begin_roots_block(_vres, 2)
_vres[0] = camlidl_c2ml_z3V3_Z3_lbool(&_res, _ctx);
_vres[1] = camlidl_alloc(num_terms, 0);
for (_c4 = 0; _c4 < num_terms; _c4++) {
_v5 = Val_int(class_ids[_c4]);
modify(&Field(_vres[1], _c4), _v5);
}
_vresult = camlidl_alloc_small(2, 0);
Field(_vresult, 0) = _vres[0];
Field(_vresult, 1) = _vres[1];
End_roots()
camlidl_free(_ctx);
return _vresult;
}
value camlidl_z3V3_Z3_del_model(
value _v_c,
value _v_m)