mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
This commit is contained in:
commit
a0a505e1b8
|
@ -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) {
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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!
|
||||
|
|
|
@ -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!
|
||||
|
|
|
@ -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.
|
||||
|
|
|
@ -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.
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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"
|
||||
|
||||
|
|
|
@ -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}
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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
|
||||
|
@ -6922,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
|
||||
|
@ -7109,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.
|
||||
|
||||
|
@ -7140,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.
|
||||
|
||||
|
|
Loading…
Reference in a new issue