diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 4d391c06f..705f9a3e7 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -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" diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 4dd3d5b14..2eb9eecb7 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -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} diff --git a/src/api/ml/z3_stubs.c b/src/api/ml/z3_stubs.c index 0cf20fb2e..bad4338de 100644 --- a/src/api/ml/z3_stubs.c +++ b/src/api/ml/z3_stubs.c @@ -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)