From 7b1fac11e647c77eccd54cb591feb699b832d276 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 19 Dec 2012 12:33:14 -0800 Subject: [PATCH 1/6] Add new C++ examples Signed-off-by: Leonardo de Moura --- examples/c++/example.cpp | 65 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 65 insertions(+) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index ab6e67ab9..9e92d99ab 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -812,6 +812,68 @@ void tst_visit() { visit(f); } +void incremental_example1() { + std::cout << "incremental example1\n"; + context c; + expr x = c.int_const("x"); + solver s(c); + s.add(x > 0); + std::cout << s.check() << "\n"; + // We can add more formulas to the solver + s.add(x < 0); + // and, invoke s.check() again... + std::cout << s.check() << "\n"; +} + +void incremental_example2() { + // In this example, we show how push() and pop() can be used + // to remove formulas added to the solver. + std::cout << "incremental example2\n"; + context c; + expr x = c.int_const("x"); + solver s(c); + s.add(x > 0); + std::cout << s.check() << "\n"; + // push() creates a backtracking point (aka a snapshot). + s.push(); + // We can add more formulas to the solver + s.add(x < 0); + // and, invoke s.check() again... + std::cout << s.check() << "\n"; + // pop() will remove all formulas added between this pop() and the matching push() + s.pop(); + // The context is satisfiable again + std::cout << s.check() << "\n"; + // and contains only x > 0 + std::cout << s << "\n"; +} + +void incremental_example3() { + // In this example, we show how to use assumptions to "remove" + // formulas added to a solver. Actually, we disable them. + std::cout << "incremental example3\n"; + context c; + expr x = c.int_const("x"); + solver s(c); + s.add(x > 0); + std::cout << s.check() << "\n"; + // Now, suppose we want to add x < 0 to the solver, but we also want + // to be able to disable it later. + // To do that, we create an auxiliary Boolean variable + expr b = c.bool_const("b"); + // and, assert (b implies x < 0) + s.add(implies(b, x < 0)); + // Now, we check whether s is satisfiable under the assumption "b" is true. + expr_vector a1(c); + a1.push_back(b); + std::cout << s.check(a1) << "\n"; + // To "disable" (x > 0), we may just ask with the assumption "not b" or not provide any assumption. + std::cout << s.check() << "\n"; + expr_vector a2(c); + a2.push_back(!b); + std::cout << s.check(a2) << "\n"; +} + int main() { try { demorgan(); std::cout << "\n"; @@ -842,6 +904,9 @@ int main() { tactic_example9(); std::cout << "\n"; tactic_qe(); std::cout << "\n"; tst_visit(); std::cout << "\n"; + incremental_example1(); std::cout << "\n"; + incremental_example2(); std::cout << "\n"; + incremental_example3(); std::cout << "\n"; std::cout << "done\n"; } catch (exception & ex) { From 27438b0fc948a78591f774108180b87b09499790 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 13 Dec 2012 11:33:38 +0000 Subject: [PATCH 2/6] Fix newlines --- src/api/ml/README-linux | 44 ++++++++++++++++++------------------ src/api/ml/README-osx | 44 ++++++++++++++++++------------------ src/api/ml/README-test-linux | 34 ++++++++++++++-------------- src/api/ml/README-test-osx | 34 ++++++++++++++-------------- src/api/ml/exec.sh | 8 +++---- 5 files changed, 82 insertions(+), 82 deletions(-) diff --git a/src/api/ml/README-linux b/src/api/ml/README-linux index a726c0c94..5ee20bb27 100644 --- a/src/api/ml/README-linux +++ b/src/api/ml/README-linux @@ -1,22 +1,22 @@ -The OCaml API for Z3 was tested using OCaml 3.12.1. -You also need CamlIDL to be able to generate the OCaml API. - -- To download OCaml: - http://caml.inria.fr/ocaml/ - -- To download CamlIDL: - http://forge.ocamlcore.org/projects/camlidl/ - -- To build the OCaml API for Z3: - ./build-lib.sh - -Remark: The OCaml and C compiler tool chains must be configured in your environment. - -Remark: Building the OCaml API copies some pathnames into files, -so the OCaml API must be recompiled if the Z3 library files are moved. - -See ../examples/ocaml/build-test.sh for an example of how to compile and link with Z3. - -Acknowledgements: -The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg. -Many thanks to them! +The OCaml API for Z3 was tested using OCaml 3.12.1. +You also need CamlIDL to be able to generate the OCaml API. + +- To download OCaml: + http://caml.inria.fr/ocaml/ + +- To download CamlIDL: + http://forge.ocamlcore.org/projects/camlidl/ + +- To build the OCaml API for Z3: + ./build-lib.sh + +Remark: The OCaml and C compiler tool chains must be configured in your environment. + +Remark: Building the OCaml API copies some pathnames into files, +so the OCaml API must be recompiled if the Z3 library files are moved. + +See ../examples/ocaml/build-test.sh for an example of how to compile and link with Z3. + +Acknowledgements: +The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg. +Many thanks to them! diff --git a/src/api/ml/README-osx b/src/api/ml/README-osx index a726c0c94..5ee20bb27 100644 --- a/src/api/ml/README-osx +++ b/src/api/ml/README-osx @@ -1,22 +1,22 @@ -The OCaml API for Z3 was tested using OCaml 3.12.1. -You also need CamlIDL to be able to generate the OCaml API. - -- To download OCaml: - http://caml.inria.fr/ocaml/ - -- To download CamlIDL: - http://forge.ocamlcore.org/projects/camlidl/ - -- To build the OCaml API for Z3: - ./build-lib.sh - -Remark: The OCaml and C compiler tool chains must be configured in your environment. - -Remark: Building the OCaml API copies some pathnames into files, -so the OCaml API must be recompiled if the Z3 library files are moved. - -See ../examples/ocaml/build-test.sh for an example of how to compile and link with Z3. - -Acknowledgements: -The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg. -Many thanks to them! +The OCaml API for Z3 was tested using OCaml 3.12.1. +You also need CamlIDL to be able to generate the OCaml API. + +- To download OCaml: + http://caml.inria.fr/ocaml/ + +- To download CamlIDL: + http://forge.ocamlcore.org/projects/camlidl/ + +- To build the OCaml API for Z3: + ./build-lib.sh + +Remark: The OCaml and C compiler tool chains must be configured in your environment. + +Remark: Building the OCaml API copies some pathnames into files, +so the OCaml API must be recompiled if the Z3 library files are moved. + +See ../examples/ocaml/build-test.sh for an example of how to compile and link with Z3. + +Acknowledgements: +The OCaml interface for Z3 was written by Josh Berdine and Jakob Lichtenberg. +Many thanks to them! diff --git a/src/api/ml/README-test-linux b/src/api/ml/README-test-linux index 34900883d..fc15fb2a2 100644 --- a/src/api/ml/README-test-linux +++ b/src/api/ml/README-test-linux @@ -1,17 +1,17 @@ -This directory contains scripts to build the test application using -OCaml. You also need CamlIDL to be able to generate the OCaml API. - -- To download OCaml: - http://caml.inria.fr/ocaml/ - -- To download CamlIDL: - http://forge.ocamlcore.org/projects/camlidl/ - -- One must build the OCaml library before compiling the example. - Go to directory ../ocaml - -- Use 'build-test.sh' to build the test application using the OCaml compiler. - -Remark: The OCaml and C compiler tool chains must be configured in your environment. - -- Use 'exec.sh' to execute test_mlapi. The script sets LD_LIBRARY_PATH, and invokes test_mlapi. +This directory contains scripts to build the test application using +OCaml. You also need CamlIDL to be able to generate the OCaml API. + +- To download OCaml: + http://caml.inria.fr/ocaml/ + +- To download CamlIDL: + http://forge.ocamlcore.org/projects/camlidl/ + +- One must build the OCaml library before compiling the example. + Go to directory ../ocaml + +- Use 'build-test.sh' to build the test application using the OCaml compiler. + +Remark: The OCaml and C compiler tool chains must be configured in your environment. + +- Use 'exec.sh' to execute test_mlapi. The script sets LD_LIBRARY_PATH, and invokes test_mlapi. diff --git a/src/api/ml/README-test-osx b/src/api/ml/README-test-osx index bfc6b115e..3a20d1f1d 100644 --- a/src/api/ml/README-test-osx +++ b/src/api/ml/README-test-osx @@ -1,17 +1,17 @@ -This directory contains scripts to build the test application using -OCaml. You also need CamlIDL to be able to generate the OCaml API. - -- To download OCaml: - http://caml.inria.fr/ocaml/ - -- To download CamlIDL: - http://forge.ocamlcore.org/projects/camlidl/ - -- One must build the OCaml library before compiling the example. - Go to directory ../ocaml - -- Use 'build-test.sh' to build the test application using the OCaml compiler. - -Remark: The OCaml and C compiler tool chains must be configured in your environment. - -- Use 'exec.sh' to execute test_mlapi. The script sets DYLD_LIBRARY_PATH, and invokes test_mlapi. +This directory contains scripts to build the test application using +OCaml. You also need CamlIDL to be able to generate the OCaml API. + +- To download OCaml: + http://caml.inria.fr/ocaml/ + +- To download CamlIDL: + http://forge.ocamlcore.org/projects/camlidl/ + +- One must build the OCaml library before compiling the example. + Go to directory ../ocaml + +- Use 'build-test.sh' to build the test application using the OCaml compiler. + +Remark: The OCaml and C compiler tool chains must be configured in your environment. + +- Use 'exec.sh' to execute test_mlapi. The script sets DYLD_LIBRARY_PATH, and invokes test_mlapi. diff --git a/src/api/ml/exec.sh b/src/api/ml/exec.sh index a1d3c8e49..573ec6ddf 100644 --- a/src/api/ml/exec.sh +++ b/src/api/ml/exec.sh @@ -1,4 +1,4 @@ -#!/bin/sh -export LD_LIBRARY_PATH=../../lib:$LD_LIBRARY_PATH # for linux -export DYLD_LIBRARY_PATH=../../lib:$DYLD_LIBRARY_PATH # for osx -./test_mlapi +#!/bin/sh +export LD_LIBRARY_PATH=../../lib:$LD_LIBRARY_PATH # for linux +export DYLD_LIBRARY_PATH=../../lib:$DYLD_LIBRARY_PATH # for osx +./test_mlapi From 32896a15e6e82e660164ddb9845d0c43fdcf2b25 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 12 Dec 2012 02:02:08 +0000 Subject: [PATCH 3/6] Fix for compiling ml api --- src/api/ml/Makefile.build | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/ml/Makefile.build b/src/api/ml/Makefile.build index 27c798bbf..0a737e356 100644 --- a/src/api/ml/Makefile.build +++ b/src/api/ml/Makefile.build @@ -13,7 +13,7 @@ XCDBG=-g $(CFLAGS) XCOPT=-ccopt -Ox -ccopt -Oy- $(CFLAGS) # ole32 is needed by camlidl (COM support) XLIB=-cclib ole32.lib -AR=lib /nologo /LIBPATH:../../build ../../z3.lib /out: +AR=lib /nologo /LIBPATH:../../build ../../libz3.lib /out: O=obj A=lib else From fd5372d7a27792e884bd7d94da053599f8f98eb6 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sat, 8 Dec 2012 18:05:26 +0000 Subject: [PATCH 4/6] Z3_search_failure type not needed in v4 ml api --- src/api/z3_api.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index e12ce3591..e8306bfb6 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1080,6 +1080,7 @@ typedef enum { Z3_PK_INVALID } Z3_param_kind; +#ifdef CorML3 /** \mlonly {!search_failure} \endmlonly \conly \brief The different kinds of search failure types. @@ -1103,6 +1104,7 @@ typedef enum { Z3_THEORY, Z3_QUANTIFIERS } Z3_search_failure; +#endif /** \mlonly {!ast_print_mode} \endmlonly \conly \brief From a7f89dcdd2faabffd980d16326f15f9304fdca2e Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 20 Dec 2012 12:54:44 +0000 Subject: [PATCH 5/6] Move Z3_get_implied_equalities from v3 to v4 ml api as it now needs Z3_solver type --- src/api/z3_api.h | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index e8306bfb6..98bde7bcf 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6924,12 +6924,15 @@ END_MLAPI_EXCLUDE ); /*@}*/ - +#endif + + /** @name Deprecated Constraints API */ /*@{*/ +#ifdef CorML3 /** \brief Set the SMTLIB logic to be used in the given logical context. It is incorrect to invoke this function after invoking @@ -7111,7 +7114,9 @@ END_MLAPI_EXCLUDE __out Z3_model * m, __out Z3_ast* proof, __inout unsigned* core_size, __inout_ecount(num_assumptions) Z3_ast core[] ); +#endif +#ifdef CorML4 /** \brief Retrieve congruence class representatives for terms. @@ -7142,7 +7147,9 @@ END_MLAPI_EXCLUDE __in_ecount(num_terms) Z3_ast const terms[], __out_ecount(num_terms) unsigned class_ids[] ); +#endif +#ifdef CorML3 /** \brief Delete a model object. From d7b8110cc8cf5d20540be1b0955dfb0241c857dd Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 20 Dec 2012 12:58:21 +0000 Subject: [PATCH 6/6] Regenerate ml api --- src/api/ml/z3.ml | 16 +----- src/api/ml/z3.mli | 71 ++++++++--------------- src/api/ml/z3_stubs.c | 131 ++++++++++++++++++------------------------ 3 files changed, 84 insertions(+), 134 deletions(-) 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)