mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
f859689835
|
@ -163,11 +163,11 @@ void free_cnstr_array(Z3_ast * cnstrs)
|
|||
/**
|
||||
\brief Assert hard constraints stored in the given array.
|
||||
*/
|
||||
void assert_hard_constraints(Z3_context ctx, unsigned num_cnstrs, Z3_ast * cnstrs)
|
||||
void assert_hard_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z3_ast * cnstrs)
|
||||
{
|
||||
unsigned i;
|
||||
for (i = 0; i < num_cnstrs; i++) {
|
||||
Z3_assert_cnstr(ctx, cnstrs[i]);
|
||||
Z3_solver_assert(ctx, s, cnstrs[i]);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -176,14 +176,14 @@ void assert_hard_constraints(Z3_context ctx, unsigned num_cnstrs, Z3_ast * cnstr
|
|||
This funtion will assert each soft-constraint C_i as (C_i or k_i) where k_i is a fresh boolean variable.
|
||||
It will also return an array containing these fresh variables.
|
||||
*/
|
||||
Z3_ast * assert_soft_constraints(Z3_context ctx, unsigned num_cnstrs, Z3_ast * cnstrs)
|
||||
Z3_ast * assert_soft_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z3_ast * cnstrs)
|
||||
{
|
||||
unsigned i;
|
||||
Z3_ast * aux_vars;
|
||||
aux_vars = mk_fresh_bool_var_array(ctx, num_cnstrs);
|
||||
for (i = 0; i < num_cnstrs; i++) {
|
||||
Z3_ast assumption = cnstrs[i];
|
||||
Z3_assert_cnstr(ctx, mk_binary_or(ctx, assumption, aux_vars[i]));
|
||||
Z3_solver_assert(ctx, s, mk_binary_or(ctx, assumption, aux_vars[i]));
|
||||
}
|
||||
return aux_vars;
|
||||
}
|
||||
|
@ -299,7 +299,7 @@ int get_bit(unsigned val, unsigned idx)
|
|||
/**
|
||||
\brief Given an integer val encoded in n bits (boolean variables), assert the constraint that val <= k.
|
||||
*/
|
||||
void assert_le_k(Z3_context ctx, unsigned n, Z3_ast * val, unsigned k)
|
||||
void assert_le_k(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * val, unsigned k)
|
||||
{
|
||||
Z3_ast i1, i2, not_val, out;
|
||||
unsigned idx;
|
||||
|
@ -321,7 +321,7 @@ void assert_le_k(Z3_context ctx, unsigned n, Z3_ast * val, unsigned k)
|
|||
out = mk_ternary_or(ctx, i1, i2, mk_binary_and(ctx, not_val, out));
|
||||
}
|
||||
// printf("at-most-k:\n%s\n", Z3_ast_to_string(ctx, out));
|
||||
Z3_assert_cnstr(ctx, out);
|
||||
Z3_solver_assert(ctx, s, out);
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -331,14 +331,14 @@ void assert_le_k(Z3_context ctx, unsigned n, Z3_ast * val, unsigned k)
|
|||
We use a simple encoding using an adder (counter).
|
||||
An interesting exercise consists in implementing more sophisticated encodings.
|
||||
*/
|
||||
void assert_at_most_k(Z3_context ctx, unsigned n, Z3_ast * lits, unsigned k)
|
||||
void assert_at_most_k(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * lits, unsigned k)
|
||||
{
|
||||
Z3_ast * counter_bits;
|
||||
unsigned counter_bits_sz;
|
||||
if (k >= n || n <= 1)
|
||||
return; /* nothing to be done */
|
||||
counter_bits = mk_counter_circuit(ctx, n, lits, &counter_bits_sz);
|
||||
assert_le_k(ctx, counter_bits_sz, counter_bits, k);
|
||||
assert_le_k(ctx, s, counter_bits_sz, counter_bits, k);
|
||||
del_bool_var_array(counter_bits);
|
||||
}
|
||||
|
||||
|
@ -346,9 +346,9 @@ void assert_at_most_k(Z3_context ctx, unsigned n, Z3_ast * lits, unsigned k)
|
|||
\brief Assert that at most one literal in \c lits can be true,
|
||||
where \c n is the number of literals in lits.
|
||||
*/
|
||||
void assert_at_most_one(Z3_context ctx, unsigned n, Z3_ast * lits)
|
||||
void assert_at_most_one(Z3_context ctx, Z3_solver s, unsigned n, Z3_ast * lits)
|
||||
{
|
||||
assert_at_most_k(ctx, n, lits, 1);
|
||||
assert_at_most_k(ctx, s, n, lits, 1);
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -357,6 +357,7 @@ void assert_at_most_one(Z3_context ctx, unsigned n, Z3_ast * lits)
|
|||
void tst_at_most_one()
|
||||
{
|
||||
Z3_context ctx = mk_context();
|
||||
Z3_solver s = Z3_mk_solver(ctx);
|
||||
Z3_ast k1 = mk_bool_var(ctx, "k1");
|
||||
Z3_ast k2 = mk_bool_var(ctx, "k2");
|
||||
Z3_ast k3 = mk_bool_var(ctx, "k3");
|
||||
|
@ -368,29 +369,25 @@ void tst_at_most_one()
|
|||
Z3_model m = 0;
|
||||
Z3_lbool result;
|
||||
printf("testing at-most-one constraint\n");
|
||||
assert_at_most_one(ctx, 5, args1);
|
||||
assert_at_most_one(ctx, 3, args2);
|
||||
assert_at_most_one(ctx, s, 5, args1);
|
||||
assert_at_most_one(ctx, s, 3, args2);
|
||||
printf("it must be sat...\n");
|
||||
result = Z3_check_and_get_model(ctx, &m);
|
||||
result = Z3_solver_check(ctx, s);
|
||||
if (result != Z3_L_TRUE)
|
||||
error("BUG");
|
||||
m = Z3_solver_get_model(ctx, s);
|
||||
printf("model:\n%s\n", Z3_model_to_string(ctx, m));
|
||||
if (m) {
|
||||
Z3_del_model(ctx, m);
|
||||
}
|
||||
Z3_assert_cnstr(ctx, mk_binary_or(ctx, k2, k3));
|
||||
Z3_assert_cnstr(ctx, mk_binary_or(ctx, k1, k6));
|
||||
Z3_solver_assert(ctx, s, mk_binary_or(ctx, k2, k3));
|
||||
Z3_solver_assert(ctx, s, mk_binary_or(ctx, k1, k6));
|
||||
printf("it must be sat...\n");
|
||||
result = Z3_check_and_get_model(ctx, &m);
|
||||
result = Z3_solver_check(ctx, s);
|
||||
if (result != Z3_L_TRUE)
|
||||
error("BUG");
|
||||
m = Z3_solver_get_model(ctx, s);
|
||||
printf("model:\n%s\n", Z3_model_to_string(ctx, m));
|
||||
if (m) {
|
||||
Z3_del_model(ctx, m);
|
||||
}
|
||||
Z3_assert_cnstr(ctx, mk_binary_or(ctx, k4, k5));
|
||||
Z3_solver_assert(ctx, s, mk_binary_or(ctx, k4, k5));
|
||||
printf("it must be unsat...\n");
|
||||
result = Z3_check_and_get_model(ctx, &m);
|
||||
result = Z3_solver_check(ctx, s);
|
||||
if (result != Z3_L_FALSE)
|
||||
error("BUG");
|
||||
Z3_del_context(ctx);
|
||||
|
@ -407,7 +404,7 @@ unsigned get_num_disabled_soft_constraints(Z3_context ctx, Z3_model m, unsigned
|
|||
Z3_ast t = Z3_mk_true(ctx);
|
||||
for (i = 0; i < num_soft_cnstrs; i++) {
|
||||
Z3_ast val;
|
||||
if (Z3_eval(ctx, m, aux_vars[i], &val) == Z3_TRUE) {
|
||||
if (Z3_model_eval(ctx, m, aux_vars[i], 1, &val) == Z3_TRUE) {
|
||||
// printf("%s", Z3_ast_to_string(ctx, aux_vars[i]));
|
||||
// printf(" -> %s\n", Z3_ast_to_string(ctx, val));
|
||||
if (Z3_is_eq_ast(ctx, val, t)) {
|
||||
|
@ -428,21 +425,21 @@ unsigned get_num_disabled_soft_constraints(Z3_context ctx, Z3_model m, unsigned
|
|||
Exercise: use binary search to implement MaxSAT.
|
||||
Hint: you will need to use an answer literal to retract the at-most-k constraint.
|
||||
*/
|
||||
int naive_maxsat(Z3_context ctx, unsigned num_hard_cnstrs, Z3_ast * hard_cnstrs, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs)
|
||||
int naive_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_ast * hard_cnstrs, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs)
|
||||
{
|
||||
Z3_ast * aux_vars;
|
||||
Z3_lbool is_sat;
|
||||
unsigned r, k;
|
||||
assert_hard_constraints(ctx, num_hard_cnstrs, hard_cnstrs);
|
||||
assert_hard_constraints(ctx, s, num_hard_cnstrs, hard_cnstrs);
|
||||
printf("checking whether hard constraints are satisfiable...\n");
|
||||
is_sat = Z3_check(ctx);
|
||||
is_sat = Z3_solver_check(ctx, s);
|
||||
if (is_sat == Z3_L_FALSE) {
|
||||
// It is not possible to make the formula satisfiable even when ignoring all soft constraints.
|
||||
return -1;
|
||||
}
|
||||
if (num_soft_cnstrs == 0)
|
||||
return 0; // nothing to be done...
|
||||
aux_vars = assert_soft_constraints(ctx, num_soft_cnstrs, soft_cnstrs);
|
||||
aux_vars = assert_soft_constraints(ctx, s, num_soft_cnstrs, soft_cnstrs);
|
||||
// Perform linear search.
|
||||
r = 0;
|
||||
k = num_soft_cnstrs - 1;
|
||||
|
@ -451,19 +448,17 @@ int naive_maxsat(Z3_context ctx, unsigned num_hard_cnstrs, Z3_ast * hard_cnstrs,
|
|||
unsigned num_disabled;
|
||||
// at most k soft-constraints can be ignored.
|
||||
printf("checking whether at-most %d soft-constraints can be ignored.\n", k);
|
||||
assert_at_most_k(ctx, num_soft_cnstrs, aux_vars, k);
|
||||
is_sat = Z3_check_and_get_model(ctx, &m);
|
||||
assert_at_most_k(ctx, s, num_soft_cnstrs, aux_vars, k);
|
||||
is_sat = Z3_solver_check(ctx, s);
|
||||
if (is_sat == Z3_L_FALSE) {
|
||||
printf("unsat\n");
|
||||
return num_soft_cnstrs - k - 1;
|
||||
}
|
||||
m = Z3_solver_get_model(ctx, s);
|
||||
num_disabled = get_num_disabled_soft_constraints(ctx, m, num_soft_cnstrs, aux_vars);
|
||||
if (num_disabled > k) {
|
||||
error("BUG");
|
||||
}
|
||||
if (m) {
|
||||
Z3_del_model(ctx, m);
|
||||
}
|
||||
printf("sat\n");
|
||||
k = num_disabled;
|
||||
if (k == 0) {
|
||||
|
@ -489,28 +484,27 @@ int naive_maxsat(Z3_context ctx, unsigned num_hard_cnstrs, Z3_ast * hard_cnstrs,
|
|||
- replace aux-var with a new one
|
||||
* add at-most-one constraint with blocking
|
||||
*/
|
||||
int fu_malik_maxsat_step(Z3_context ctx, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs, Z3_ast * aux_vars)
|
||||
int fu_malik_maxsat_step(Z3_context ctx, Z3_solver s, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs, Z3_ast * aux_vars)
|
||||
{
|
||||
// create assumptions
|
||||
Z3_ast * assumptions = (Z3_ast*) malloc(sizeof(Z3_ast) * num_soft_cnstrs);
|
||||
Z3_ast * core = (Z3_ast*) malloc(sizeof(Z3_ast) * num_soft_cnstrs);
|
||||
unsigned core_size;
|
||||
Z3_ast dummy_proof; // we don't care about proofs in this example
|
||||
Z3_model m;
|
||||
Z3_lbool is_sat;
|
||||
Z3_ast_vector core;
|
||||
unsigned core_size;
|
||||
unsigned i = 0;
|
||||
for (i = 0; i < num_soft_cnstrs; i++) {
|
||||
// Recall that we asserted (soft_cnstrs[i] \/ aux_vars[i])
|
||||
// So using (NOT aux_vars[i]) as an assumption we are actually forcing the soft_cnstrs[i] to be considered.
|
||||
assumptions[i] = Z3_mk_not(ctx, aux_vars[i]);
|
||||
core[i] = 0;
|
||||
}
|
||||
|
||||
is_sat = Z3_check_assumptions(ctx, num_soft_cnstrs, assumptions, &m, &dummy_proof, &core_size, core);
|
||||
is_sat = Z3_solver_check_assumptions(ctx, s, num_soft_cnstrs, assumptions);
|
||||
if (is_sat != Z3_L_FALSE) {
|
||||
return 1; // done
|
||||
}
|
||||
else {
|
||||
core = Z3_solver_get_unsat_core(ctx, s);
|
||||
core_size = Z3_ast_vector_size(ctx, core);
|
||||
Z3_ast * block_vars = (Z3_ast*) malloc(sizeof(Z3_ast) * core_size);
|
||||
unsigned k = 0;
|
||||
// update soft-constraints and aux_vars
|
||||
|
@ -518,7 +512,7 @@ int fu_malik_maxsat_step(Z3_context ctx, unsigned num_soft_cnstrs, Z3_ast * soft
|
|||
unsigned j;
|
||||
// check whether assumption[i] is in the core or not
|
||||
for (j = 0; j < core_size; j++) {
|
||||
if (assumptions[i] == core[j])
|
||||
if (assumptions[i] == Z3_ast_vector_get(ctx, core, j))
|
||||
break;
|
||||
}
|
||||
if (j < core_size) {
|
||||
|
@ -531,10 +525,10 @@ int fu_malik_maxsat_step(Z3_context ctx, unsigned num_soft_cnstrs, Z3_ast * soft
|
|||
k++;
|
||||
// Add new constraint containing the block variable.
|
||||
// Note that we are using the new auxiliary variable to be able to use it as an assumption.
|
||||
Z3_assert_cnstr(ctx, mk_binary_or(ctx, soft_cnstrs[i], new_aux_var));
|
||||
Z3_solver_assert(ctx, s, mk_binary_or(ctx, soft_cnstrs[i], new_aux_var));
|
||||
}
|
||||
}
|
||||
assert_at_most_one(ctx, k, block_vars);
|
||||
assert_at_most_one(ctx, s, k, block_vars);
|
||||
return 0; // not done.
|
||||
}
|
||||
}
|
||||
|
@ -553,14 +547,14 @@ int fu_malik_maxsat_step(Z3_context ctx, unsigned num_soft_cnstrs, Z3_ast * soft
|
|||
Z. Fu and S. Malik, On solving the partial MAX-SAT problem, in International
|
||||
Conference on Theory and Applications of Satisfiability Testing, 2006.
|
||||
*/
|
||||
int fu_malik_maxsat(Z3_context ctx, unsigned num_hard_cnstrs, Z3_ast * hard_cnstrs, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs)
|
||||
int fu_malik_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_ast * hard_cnstrs, unsigned num_soft_cnstrs, Z3_ast * soft_cnstrs)
|
||||
{
|
||||
Z3_ast * aux_vars;
|
||||
Z3_lbool is_sat;
|
||||
unsigned k;
|
||||
assert_hard_constraints(ctx, num_hard_cnstrs, hard_cnstrs);
|
||||
assert_hard_constraints(ctx, s, num_hard_cnstrs, hard_cnstrs);
|
||||
printf("checking whether hard constraints are satisfiable...\n");
|
||||
is_sat = Z3_check(ctx);
|
||||
is_sat = Z3_solver_check(ctx, s);
|
||||
if (is_sat == Z3_L_FALSE) {
|
||||
// It is not possible to make the formula satisfiable even when ignoring all soft constraints.
|
||||
return -1;
|
||||
|
@ -571,11 +565,11 @@ int fu_malik_maxsat(Z3_context ctx, unsigned num_hard_cnstrs, Z3_ast * hard_cnst
|
|||
Fu&Malik algorithm is based on UNSAT-core extraction.
|
||||
We accomplish that using auxiliary variables (aka answer literals).
|
||||
*/
|
||||
aux_vars = assert_soft_constraints(ctx, num_soft_cnstrs, soft_cnstrs);
|
||||
aux_vars = assert_soft_constraints(ctx, s, num_soft_cnstrs, soft_cnstrs);
|
||||
k = 0;
|
||||
for (;;) {
|
||||
printf("iteration %d\n", k);
|
||||
if (fu_malik_maxsat_step(ctx, num_soft_cnstrs, soft_cnstrs, aux_vars)) {
|
||||
if (fu_malik_maxsat_step(ctx, s, num_soft_cnstrs, soft_cnstrs, aux_vars)) {
|
||||
return num_soft_cnstrs - k;
|
||||
}
|
||||
k++;
|
||||
|
@ -596,19 +590,21 @@ int fu_malik_maxsat(Z3_context ctx, unsigned num_hard_cnstrs, Z3_ast * hard_cnst
|
|||
int smtlib_maxsat(char * file_name, int approach)
|
||||
{
|
||||
Z3_context ctx;
|
||||
Z3_solver s;
|
||||
unsigned num_hard_cnstrs, num_soft_cnstrs;
|
||||
Z3_ast * hard_cnstrs, * soft_cnstrs;
|
||||
unsigned result = 0;
|
||||
ctx = mk_context();
|
||||
s = Z3_mk_solver(ctx);
|
||||
Z3_parse_smtlib_file(ctx, file_name, 0, 0, 0, 0, 0, 0);
|
||||
hard_cnstrs = get_hard_constraints(ctx, &num_hard_cnstrs);
|
||||
soft_cnstrs = get_soft_constraints(ctx, &num_soft_cnstrs);
|
||||
switch (approach) {
|
||||
case NAIVE_MAXSAT:
|
||||
result = naive_maxsat(ctx, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs);
|
||||
result = naive_maxsat(ctx, s, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs);
|
||||
break;
|
||||
case FU_MALIK_MAXSAT:
|
||||
result = fu_malik_maxsat(ctx, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs);
|
||||
result = fu_malik_maxsat(ctx, s, num_hard_cnstrs, hard_cnstrs, num_soft_cnstrs, soft_cnstrs);
|
||||
break;
|
||||
default:
|
||||
/* Exercise: implement your own MaxSAT algorithm.*/
|
||||
|
|
|
@ -57,7 +57,7 @@ log_h.write('inline void SetR(void * obj) { *g_z3_log << "= " << obj << "\\n"; }
|
|||
log_h.write('#define RETURN_Z3(Z3RES) if (_LOG_CTX.enabled()) { SetR(Z3RES); } return Z3RES\n')
|
||||
log_h.write('void _Z3_append_log(char const * msg);\n')
|
||||
##
|
||||
exe_c.write('void Z3_replacer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg_ex(ctx, c)); }\n')
|
||||
exe_c.write('void Z3_replacer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg(ctx, c)); }\n')
|
||||
##
|
||||
core_py.write('# Automatically generated file\n')
|
||||
core_py.write('import sys, os\n')
|
||||
|
@ -404,7 +404,7 @@ def mk_py_wrappers():
|
|||
if len(params) > 0 and param_type(params[0]) == CONTEXT:
|
||||
core_py.write(" err = lib().Z3_get_error_code(a0)\n")
|
||||
core_py.write(" if err != Z3_OK:\n")
|
||||
core_py.write(" raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))\n")
|
||||
core_py.write(" raise Z3Exception(lib().Z3_get_error_msg(a0, err))\n")
|
||||
if result == STRING:
|
||||
core_py.write(" return _to_pystr(r)\n")
|
||||
elif result != VOID:
|
||||
|
@ -477,7 +477,7 @@ def mk_dotnet_wrappers():
|
|||
dotnet.write(" LIB.Z3_set_error_handler(a0, a1);\n")
|
||||
dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n")
|
||||
dotnet.write(" if (err != Z3_error_code.Z3_OK)\n")
|
||||
dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n")
|
||||
dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg(a0, (uint)err)));\n")
|
||||
dotnet.write(" }\n\n")
|
||||
for name, result, params in _dotnet_decls:
|
||||
if result == STRING:
|
||||
|
@ -525,7 +525,7 @@ def mk_dotnet_wrappers():
|
|||
if len(params) > 0 and param_type(params[0]) == CONTEXT:
|
||||
dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n")
|
||||
dotnet.write(" if (err != Z3_error_code.Z3_OK)\n")
|
||||
dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));\n")
|
||||
dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg(a0, (uint)err)));\n")
|
||||
if result == STRING:
|
||||
dotnet.write(" return Marshal.PtrToStringAnsi(r);\n")
|
||||
elif result != VOID:
|
||||
|
@ -1276,7 +1276,7 @@ def mk_ml():
|
|||
if name not in Unwrapped and len(params) > 0 and param_type(params[0]) == CONTEXT:
|
||||
ml_native.write(' let err = (error_code_of_int (ML2C.n_get_error_code a0)) in \n')
|
||||
ml_native.write(' if err <> OK then\n')
|
||||
ml_native.write(' raise (Exception (ML2C.n_get_error_msg_ex a0 (int_of_error_code err)))\n')
|
||||
ml_native.write(' raise (Exception (ML2C.n_get_error_msg a0 (int_of_error_code err)))\n')
|
||||
ml_native.write(' else\n')
|
||||
if result == VOID and len(op) == 0:
|
||||
ml_native.write(' ()\n')
|
||||
|
|
|
@ -136,20 +136,6 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_label(Z3_context c, Z3_symbol s, Z3_bool is_pos, Z3_ast f) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_label(c, s, is_pos, f);
|
||||
RESET_ERROR_CODE();
|
||||
expr* _f = to_expr(f);
|
||||
if (!mk_c(c)->m().is_bool(_f)) {
|
||||
SET_ERROR_CODE(Z3_SORT_ERROR);
|
||||
return f;
|
||||
}
|
||||
expr* a = mk_c(c)->m().mk_label(is_pos != 0, to_symbol(s), _f);
|
||||
mk_c(c)->save_ast_trail(a);
|
||||
RETURN_Z3(of_ast(a));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_func_decl Z3_API Z3_mk_fresh_func_decl(Z3_context c, const char * prefix, unsigned domain_size,
|
||||
Z3_sort const domain[], Z3_sort range) {
|
||||
|
|
|
@ -32,8 +32,8 @@ void install_tactics(tactic_manager & ctx);
|
|||
|
||||
namespace api {
|
||||
|
||||
static void default_error_handler(Z3_context, Z3_error_code c) {
|
||||
printf("Error: %s\n", Z3_get_error_msg(c));
|
||||
static void default_error_handler(Z3_context ctx, Z3_error_code c) {
|
||||
printf("Error: %s\n", Z3_get_error_msg(ctx, c));
|
||||
exit(1);
|
||||
}
|
||||
|
||||
|
@ -207,20 +207,6 @@ namespace api {
|
|||
} }
|
||||
}
|
||||
|
||||
void context::persist_ast(ast * n, unsigned num_scopes) {
|
||||
// persist_ast is irrelevant when m_user_ref_count == true
|
||||
if (m_user_ref_count)
|
||||
return;
|
||||
if (num_scopes > m_ast_lim.size()) {
|
||||
num_scopes = m_ast_lim.size();
|
||||
}
|
||||
SASSERT(m_replay_stack.size() > num_scopes);
|
||||
unsigned j = m_replay_stack.size() - num_scopes - 1;
|
||||
if (!m_replay_stack[j]) {
|
||||
m_replay_stack[j] = alloc(ast_ref_vector, m());
|
||||
}
|
||||
m_replay_stack[j]->push_back(n);
|
||||
}
|
||||
|
||||
void context::save_ast_trail(ast * n) {
|
||||
SASSERT(m().contains(n));
|
||||
|
@ -476,13 +462,6 @@ extern "C" {
|
|||
Z3_CATCH;
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_set_logic(Z3_context c, Z3_string logic) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_set_logic(c, logic);
|
||||
RESET_ERROR_CODE();
|
||||
return mk_c(c)->get_smt_kernel().set_logic(symbol(logic));
|
||||
Z3_CATCH_RETURN(Z3_FALSE);
|
||||
}
|
||||
|
||||
void Z3_API Z3_get_version(unsigned * major,
|
||||
unsigned * minor,
|
||||
|
@ -534,7 +513,7 @@ extern "C" {
|
|||
SET_ERROR_CODE(e);
|
||||
}
|
||||
|
||||
static char const * _get_error_msg_ex(Z3_context c, Z3_error_code err) {
|
||||
static char const * _get_error_msg(Z3_context c, Z3_error_code err) {
|
||||
switch(err) {
|
||||
case Z3_OK: return "ok";
|
||||
case Z3_SORT_ERROR: return "type error";
|
||||
|
@ -553,24 +532,12 @@ extern "C" {
|
|||
}
|
||||
}
|
||||
|
||||
Z3_API char const * Z3_get_error_msg(Z3_error_code err) {
|
||||
LOG_Z3_get_error_msg(err);
|
||||
return _get_error_msg_ex(0, err);
|
||||
|
||||
Z3_API char const * Z3_get_error_msg(Z3_context c, Z3_error_code err) {
|
||||
LOG_Z3_get_error_msg(c, err);
|
||||
return _get_error_msg(c, err);
|
||||
}
|
||||
|
||||
Z3_API char const * Z3_get_error_msg_ex(Z3_context c, Z3_error_code err) {
|
||||
LOG_Z3_get_error_msg_ex(c, err);
|
||||
return _get_error_msg_ex(c, err);
|
||||
}
|
||||
|
||||
void Z3_API Z3_persist_ast(Z3_context c, Z3_ast n, unsigned num_scopes) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_persist_ast(c, n, num_scopes);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_VALID_AST(to_ast(n), );
|
||||
mk_c(c)->persist_ast(to_ast(n), num_scopes);
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
void Z3_API Z3_set_ast_print_mode(Z3_context c, Z3_ast_print_mode mode) {
|
||||
Z3_TRY;
|
||||
|
|
|
@ -155,7 +155,7 @@ namespace api {
|
|||
expr * mk_and(unsigned num_exprs, expr * const * exprs);
|
||||
|
||||
// Hack for preventing an AST for being GC when ref-count is not used
|
||||
void persist_ast(ast * n, unsigned num_scopes);
|
||||
// void persist_ast(ast * n, unsigned num_scopes);
|
||||
|
||||
// "Save" an AST that will exposed to the "external" world.
|
||||
void save_ast_trail(ast * n);
|
||||
|
|
|
@ -140,7 +140,7 @@ extern "C" {
|
|||
|
||||
Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_model_func_decl(c, m, i);
|
||||
LOG_Z3_model_get_func_decl(c, m, i);
|
||||
RESET_ERROR_CODE();
|
||||
Z3_func_decl r = get_model_func_decl_core(c, m, i);
|
||||
RETURN_Z3(r);
|
||||
|
@ -368,26 +368,6 @@ extern "C" {
|
|||
return Z3_model_get_func_decl(c, m, i);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_get_model_func_else(Z3_context c, Z3_model m, unsigned i) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_model_func_else(c, m, i);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_NON_NULL(m, 0);
|
||||
Z3_func_decl d = get_model_func_decl_core(c, m, i);
|
||||
if (d) {
|
||||
model * _m = to_model_ref(m);
|
||||
func_interp * g = _m->get_func_interp(to_func_decl(d));
|
||||
if (g) {
|
||||
expr * e = g->get_else();
|
||||
mk_c(c)->save_ast_trail(e);
|
||||
RETURN_Z3(of_ast(e));
|
||||
}
|
||||
SET_ERROR_CODE(Z3_IOB);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
RETURN_Z3(0);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
unsigned get_model_func_num_entries_core(Z3_context c, Z3_model m, unsigned i) {
|
||||
RESET_ERROR_CODE();
|
||||
|
@ -405,12 +385,6 @@ extern "C" {
|
|||
return 0;
|
||||
}
|
||||
|
||||
unsigned Z3_API Z3_get_model_func_num_entries(Z3_context c, Z3_model m, unsigned i) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_model_func_num_entries(c, m, i);
|
||||
return get_model_func_num_entries_core(c, m, i);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
unsigned get_model_func_entry_num_args_core(Z3_context c,
|
||||
Z3_model m,
|
||||
|
@ -431,238 +405,6 @@ extern "C" {
|
|||
return 0;
|
||||
}
|
||||
|
||||
unsigned Z3_API Z3_get_model_func_entry_num_args(Z3_context c,
|
||||
Z3_model m,
|
||||
unsigned i,
|
||||
unsigned j) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_model_func_entry_num_args(c, m, i, j);
|
||||
return get_model_func_entry_num_args_core(c, m, i, j);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_get_model_func_entry_arg(Z3_context c,
|
||||
Z3_model m,
|
||||
unsigned i,
|
||||
unsigned j,
|
||||
unsigned k) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_model_func_entry_arg(c, m, i, j, k);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_NON_NULL(m, 0);
|
||||
if (j >= get_model_func_num_entries_core(c, m, i) || k >= get_model_func_entry_num_args_core(c, m, i, j)) {
|
||||
SET_ERROR_CODE(Z3_IOB);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
Z3_func_decl d = get_model_func_decl_core(c, m, i);
|
||||
if (d) {
|
||||
model * _m = to_model_ref(m);
|
||||
func_interp * g = _m->get_func_interp(to_func_decl(d));
|
||||
if (g && j < g->num_entries()) {
|
||||
func_entry const * e = g->get_entry(j);
|
||||
if (k < g->get_arity()) {
|
||||
expr * a = e->get_arg(k);
|
||||
mk_c(c)->save_ast_trail(a);
|
||||
RETURN_Z3(of_ast(a));
|
||||
}
|
||||
}
|
||||
SET_ERROR_CODE(Z3_IOB);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
RETURN_Z3(0);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_get_model_func_entry_value(Z3_context c,
|
||||
Z3_model m,
|
||||
unsigned i,
|
||||
unsigned j) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_model_func_entry_value(c, m, i, j);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_NON_NULL(m, 0);
|
||||
if (j >= get_model_func_num_entries_core(c, m, i)) {
|
||||
SET_ERROR_CODE(Z3_IOB);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
Z3_func_decl d = get_model_func_decl_core(c, m, i);
|
||||
if (d) {
|
||||
model * _m = to_model_ref(m);
|
||||
func_interp * g = _m->get_func_interp(to_func_decl(d));
|
||||
if (g && j < g->num_entries()) {
|
||||
func_entry const* e = g->get_entry(j);
|
||||
expr* a = e->get_result();
|
||||
mk_c(c)->save_ast_trail(a);
|
||||
RETURN_Z3(of_ast(a));
|
||||
}
|
||||
SET_ERROR_CODE(Z3_IOB);
|
||||
RETURN_Z3(0);
|
||||
}
|
||||
RETURN_Z3(0);
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_eval(Z3_context c,
|
||||
Z3_model m,
|
||||
Z3_ast t,
|
||||
Z3_ast * v) {
|
||||
model_evaluator_params p;
|
||||
return Z3_model_eval(c, m, t, p.completion(), v);
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_eval_func_decl(Z3_context c,
|
||||
Z3_model m,
|
||||
Z3_func_decl decl,
|
||||
Z3_ast* v) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_eval_func_decl(c, m, decl, v);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_NON_NULL(m, Z3_FALSE);
|
||||
ast_manager & mgr = mk_c(c)->m();
|
||||
model * _m = to_model_ref(m);
|
||||
expr_ref result(mgr);
|
||||
if( _m->eval(to_func_decl(decl), result)) {
|
||||
mk_c(c)->save_ast_trail(result.get());
|
||||
*v = of_ast(result.get());
|
||||
RETURN_Z3_eval_func_decl Z3_TRUE;
|
||||
}
|
||||
else {
|
||||
return Z3_FALSE;
|
||||
}
|
||||
Z3_CATCH_RETURN(Z3_FALSE);
|
||||
}
|
||||
|
||||
|
||||
Z3_bool Z3_API Z3_is_array_value(Z3_context c, Z3_model _m, Z3_ast _v, unsigned* size) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_is_array_value(c, _m, _v, size);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_NON_NULL(_v, Z3_FALSE);
|
||||
CHECK_NON_NULL(_m, Z3_FALSE);
|
||||
model * m = to_model_ref(_m);
|
||||
expr * v = to_expr(_v);
|
||||
ast_manager& mgr = mk_c(c)->m();
|
||||
family_id afid = mk_c(c)->get_array_fid();
|
||||
unsigned sz = 0;
|
||||
array_util pl(mgr);
|
||||
if (pl.is_as_array(v)) {
|
||||
func_decl* f = pl.get_as_array_func_decl(to_app(v));
|
||||
func_interp* g = m->get_func_interp(f);
|
||||
sz = g->num_entries();
|
||||
if (sz > 0 && g->get_arity() != 1) {
|
||||
return Z3_FALSE;
|
||||
}
|
||||
}
|
||||
else {
|
||||
while (pl.is_store(v)) {
|
||||
if (to_app(v)->get_num_args() != 3) {
|
||||
return Z3_FALSE;
|
||||
}
|
||||
v = to_app(v)->get_arg(0);
|
||||
++sz;
|
||||
}
|
||||
if (!is_app_of(v, afid, OP_CONST_ARRAY)) {
|
||||
return Z3_FALSE;
|
||||
}
|
||||
}
|
||||
if (size) {
|
||||
*size = sz;
|
||||
}
|
||||
return Z3_TRUE;
|
||||
Z3_CATCH_RETURN(Z3_FALSE);
|
||||
}
|
||||
|
||||
|
||||
void Z3_API Z3_get_array_value(Z3_context c,
|
||||
Z3_model _m,
|
||||
Z3_ast _v,
|
||||
unsigned num_entries,
|
||||
Z3_ast indices[],
|
||||
Z3_ast values[],
|
||||
Z3_ast* else_value) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_array_value(c, _m, _v, num_entries, indices, values, else_value);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_NON_NULL(_m, );
|
||||
model * m = to_model_ref(_m);
|
||||
|
||||
expr* v = to_expr(_v);
|
||||
family_id afid = mk_c(c)->get_array_fid();
|
||||
ast_manager& mgr = mk_c(c)->m();
|
||||
array_util pl(mgr);
|
||||
|
||||
//
|
||||
// note: _v is already reference counted.
|
||||
// saving the trail for the returned values
|
||||
// is redundant.
|
||||
//
|
||||
unsigned sz = 0;
|
||||
if (pl.is_as_array(v)) {
|
||||
func_decl* f = pl.get_as_array_func_decl(to_app(v));
|
||||
func_interp* g = m->get_func_interp(f);
|
||||
sz = g->num_entries();
|
||||
if (g->get_arity() != 1) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return;
|
||||
}
|
||||
for (unsigned i = 0; i < sz && i < num_entries; ++i) {
|
||||
indices[i] = of_ast(g->get_entry(i)->get_arg(0));
|
||||
values[i] = of_ast(g->get_entry(i)->get_result());
|
||||
}
|
||||
if (else_value) {
|
||||
*else_value = of_ast(g->get_else());
|
||||
}
|
||||
}
|
||||
else {
|
||||
while (sz <= num_entries && is_app_of(v, afid, OP_STORE)) {
|
||||
app* a = to_app(v);
|
||||
if (a->get_num_args() != 3) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return;
|
||||
}
|
||||
expr* idx = a->get_arg(1);
|
||||
expr* val = a->get_arg(2);
|
||||
indices[sz] = of_ast(idx);
|
||||
values[sz] = of_ast(val);
|
||||
v = to_app(v)->get_arg(0);
|
||||
++sz;
|
||||
}
|
||||
|
||||
if (is_app_of(v, afid, OP_CONST_ARRAY)) {
|
||||
if (else_value) {
|
||||
*else_value = of_ast(to_app(v)->get_arg(0));
|
||||
}
|
||||
}
|
||||
else {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return;
|
||||
}
|
||||
}
|
||||
RETURN_Z3_get_array_value;
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_eval_decl(Z3_context c,
|
||||
Z3_model m,
|
||||
Z3_func_decl d,
|
||||
unsigned num_args,
|
||||
Z3_ast const args[],
|
||||
Z3_ast* v) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_eval_decl(c, m, d, num_args, args, v);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_NON_NULL(m, Z3_FALSE);
|
||||
ast_manager & mgr = mk_c(c)->m();
|
||||
model * _m = to_model_ref(m);
|
||||
app_ref app(mgr);
|
||||
app = mgr.mk_app(to_func_decl(d), num_args, to_exprs(args));
|
||||
expr_ref result(mgr);
|
||||
_m->eval(app.get(), result);
|
||||
mk_c(c)->save_ast_trail(result.get());
|
||||
*v = of_ast(result.get());
|
||||
RETURN_Z3_eval_decl Z3_TRUE;
|
||||
Z3_CATCH_RETURN(Z3_FALSE);
|
||||
}
|
||||
|
||||
Z3_API char const * Z3_model_to_string(Z3_context c, Z3_model m) {
|
||||
Z3_TRY;
|
||||
|
|
|
@ -466,42 +466,6 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_func_decl Z3_API Z3_mk_injective_function(Z3_context c,
|
||||
Z3_symbol s,
|
||||
unsigned domain_size,
|
||||
Z3_sort const domain[],
|
||||
Z3_sort range) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_injective_function(c, s, domain_size, domain, range);
|
||||
RESET_ERROR_CODE();
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mk_c(c)->reset_last_result();
|
||||
sort* range_ = to_sort(range);
|
||||
func_decl* d = m.mk_func_decl(to_symbol(s), domain_size, to_sorts(domain), range_);
|
||||
expr_ref_vector args(m);
|
||||
expr_ref fn(m), body(m);
|
||||
vector<symbol> names;
|
||||
for (unsigned i = 0; i < domain_size; ++i) {
|
||||
unsigned idx = domain_size-i-1;
|
||||
args.push_back(m.mk_var(idx, to_sort(domain[i])));
|
||||
names.push_back(symbol(idx));
|
||||
}
|
||||
fn = m.mk_app(d, args.size(), args.c_ptr());
|
||||
|
||||
for (unsigned i = 0; i < domain_size; ++i) {
|
||||
expr* arg = args[i].get();
|
||||
sort* dom = m.get_sort(arg);
|
||||
func_decl* inv = m.mk_fresh_func_decl(symbol("inv"), to_symbol(s), 1, &range_, dom);
|
||||
body = m.mk_eq(m.mk_app(inv, fn.get()), arg);
|
||||
body = m.mk_forall(args.size(), to_sorts(domain), names.c_ptr(), body.get());
|
||||
mk_c(c)->save_multiple_ast_trail(body.get());
|
||||
mk_c(c)->assert_cnstr(body.get());
|
||||
}
|
||||
mk_c(c)->save_multiple_ast_trail(d);
|
||||
RETURN_Z3(of_func_decl(d));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_pattern_to_ast(Z3_context c, Z3_pattern p) {
|
||||
RESET_ERROR_CODE();
|
||||
return (Z3_ast)(p);
|
||||
|
|
|
@ -6,7 +6,8 @@ Module Name:
|
|||
api_solver.cpp
|
||||
|
||||
Abstract:
|
||||
New solver API
|
||||
|
||||
Solver API
|
||||
|
||||
Author:
|
||||
|
||||
|
|
|
@ -1,358 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2012 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
api_solver_old.cpp
|
||||
|
||||
Abstract:
|
||||
OLD API for using solvers.
|
||||
|
||||
This has been deprecated
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2012-02-29.
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include<iostream>
|
||||
#include"z3.h"
|
||||
#include"api_log_macros.h"
|
||||
#include"api_context.h"
|
||||
#include"api_model.h"
|
||||
#include"cancel_eh.h"
|
||||
#include"scoped_timer.h"
|
||||
#include"rlimit.h"
|
||||
|
||||
extern "C" {
|
||||
|
||||
void Z3_API Z3_push(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_push(c);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_SEARCHING(c);
|
||||
mk_c(c)->push();
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
void Z3_API Z3_pop(Z3_context c, unsigned num_scopes) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_pop(c, num_scopes);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_SEARCHING(c);
|
||||
if (num_scopes > mk_c(c)->get_num_scopes()) {
|
||||
SET_ERROR_CODE(Z3_IOB);
|
||||
return;
|
||||
}
|
||||
if (num_scopes > 0) {
|
||||
mk_c(c)->pop(num_scopes);
|
||||
}
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
unsigned Z3_API Z3_get_num_scopes(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_num_scopes(c);
|
||||
RESET_ERROR_CODE();
|
||||
return mk_c(c)->get_num_scopes();
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
void Z3_API Z3_assert_cnstr(Z3_context c, Z3_ast a) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_assert_cnstr(c, a);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_FORMULA(a,);
|
||||
mk_c(c)->assert_cnstr(to_expr(a));
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
Z3_lbool Z3_API Z3_check_and_get_model(Z3_context c, Z3_model * m) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_check_and_get_model(c, m);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_SEARCHING(c);
|
||||
cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel());
|
||||
api::context::set_interruptable si(*(mk_c(c)), eh);
|
||||
flet<bool> _model(mk_c(c)->fparams().m_model, true);
|
||||
unsigned timeout = mk_c(c)->params().m_timeout;
|
||||
unsigned rlimit = mk_c(c)->params().m_rlimit;
|
||||
lbool result;
|
||||
try {
|
||||
scoped_timer timer(timeout, &eh);
|
||||
scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
|
||||
|
||||
model_ref _m;
|
||||
result = mk_c(c)->check(_m);
|
||||
if (m) {
|
||||
if (_m) {
|
||||
Z3_model_ref * m_ref = alloc(Z3_model_ref);
|
||||
m_ref->m_model = _m;
|
||||
// Must bump reference counter for backward compatibility reasons.
|
||||
// Don't need to invoke save_object, since the counter was bumped
|
||||
m_ref->inc_ref();
|
||||
*m = of_model(m_ref);
|
||||
}
|
||||
else {
|
||||
*m = 0;
|
||||
}
|
||||
}
|
||||
}
|
||||
catch (z3_exception & ex) {
|
||||
mk_c(c)->handle_exception(ex);
|
||||
RETURN_Z3_check_and_get_model static_cast<Z3_lbool>(l_undef);
|
||||
}
|
||||
RETURN_Z3_check_and_get_model static_cast<Z3_lbool>(result);
|
||||
Z3_CATCH_RETURN(Z3_L_UNDEF);
|
||||
}
|
||||
|
||||
Z3_lbool Z3_API Z3_check(Z3_context c) {
|
||||
Z3_TRY;
|
||||
// This is just syntax sugar...
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_SEARCHING(c);
|
||||
Z3_lbool r = Z3_check_and_get_model(c, 0);
|
||||
return r;
|
||||
Z3_CATCH_RETURN(Z3_L_UNDEF);
|
||||
}
|
||||
|
||||
|
||||
Z3_lbool Z3_API Z3_check_assumptions(Z3_context c,
|
||||
unsigned num_assumptions, Z3_ast const assumptions[],
|
||||
Z3_model * m, Z3_ast* proof,
|
||||
unsigned* core_size, Z3_ast core[]) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_check_assumptions(c, num_assumptions, assumptions, m, proof, core_size, core);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_SEARCHING(c);
|
||||
expr * const* _assumptions = to_exprs(assumptions);
|
||||
flet<bool> _model(mk_c(c)->fparams().m_model, true);
|
||||
cancel_eh<smt::kernel> eh(mk_c(c)->get_smt_kernel());
|
||||
api::context::set_interruptable si(*(mk_c(c)), eh);
|
||||
lbool result;
|
||||
result = mk_c(c)->get_smt_kernel().check(num_assumptions, _assumptions);
|
||||
if (result != l_false && m) {
|
||||
model_ref _m;
|
||||
mk_c(c)->get_smt_kernel().get_model(_m);
|
||||
if (_m) {
|
||||
Z3_model_ref * m_ref = alloc(Z3_model_ref);
|
||||
m_ref->m_model = _m;
|
||||
// Must bump reference counter for backward compatibility reasons.
|
||||
// Don't need to invoke save_object, since the counter was bumped
|
||||
m_ref->inc_ref();
|
||||
*m = of_model(m_ref);
|
||||
}
|
||||
else {
|
||||
*m = 0;
|
||||
}
|
||||
}
|
||||
if (result == l_false && core_size) {
|
||||
*core_size = mk_c(c)->get_smt_kernel().get_unsat_core_size();
|
||||
if (*core_size > num_assumptions) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
}
|
||||
for (unsigned i = 0; i < *core_size; ++i) {
|
||||
core[i] = of_ast(mk_c(c)->get_smt_kernel().get_unsat_core_expr(i));
|
||||
}
|
||||
}
|
||||
else if (core_size) {
|
||||
*core_size = 0;
|
||||
}
|
||||
if (result == l_false && proof) {
|
||||
*proof = of_ast(mk_c(c)->get_smt_kernel().get_proof());
|
||||
}
|
||||
else if (proof) {
|
||||
*proof = 0; // breaks abstraction.
|
||||
}
|
||||
RETURN_Z3_check_assumptions static_cast<Z3_lbool>(result);
|
||||
Z3_CATCH_RETURN(Z3_L_UNDEF);
|
||||
}
|
||||
|
||||
Z3_search_failure Z3_API Z3_get_search_failure(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_search_failure(c);
|
||||
RESET_ERROR_CODE();
|
||||
CHECK_SEARCHING(c);
|
||||
smt::failure f = mk_c(c)->get_smt_kernel().last_failure();
|
||||
return api::mk_Z3_search_failure(f);
|
||||
Z3_CATCH_RETURN(Z3_UNKNOWN);
|
||||
}
|
||||
|
||||
class labeled_literal {
|
||||
expr_ref m_literal;
|
||||
symbol m_label;
|
||||
bool m_enabled;
|
||||
public:
|
||||
labeled_literal(ast_manager& m, expr* l, symbol const& n) : m_literal(l,m), m_label(n), m_enabled(true) {}
|
||||
labeled_literal(ast_manager& m, expr* l) : m_literal(l,m), m_label(), m_enabled(true) {}
|
||||
bool is_enabled() const { return m_enabled; }
|
||||
void disable() { m_enabled = false; }
|
||||
symbol const& get_label() const { return m_label; }
|
||||
expr* get_literal() { return m_literal.get(); }
|
||||
};
|
||||
|
||||
typedef vector<labeled_literal> labels;
|
||||
|
||||
Z3_literals Z3_API Z3_get_relevant_labels(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_relevant_labels(c);
|
||||
RESET_ERROR_CODE();
|
||||
buffer<symbol> labl_syms;
|
||||
ast_manager& m = mk_c(c)->m();
|
||||
expr_ref_vector lits(m);
|
||||
mk_c(c)->get_smt_kernel().get_relevant_labels(0, labl_syms);
|
||||
mk_c(c)->get_smt_kernel().get_relevant_labeled_literals(mk_c(c)->fparams().m_at_labels_cex, lits);
|
||||
labels* lbls = alloc(labels);
|
||||
SASSERT(labl_syms.size() == lits.size());
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
lbls->push_back(labeled_literal(m,lits[i].get(), labl_syms[i]));
|
||||
}
|
||||
RETURN_Z3(reinterpret_cast<Z3_literals>(lbls));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_literals Z3_API Z3_get_relevant_literals(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_relevant_literals(c);
|
||||
RESET_ERROR_CODE();
|
||||
ast_manager& m = mk_c(c)->m();
|
||||
expr_ref_vector lits(m);
|
||||
mk_c(c)->get_smt_kernel().get_relevant_literals(lits);
|
||||
labels* lbls = alloc(labels);
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
lbls->push_back(labeled_literal(m,lits[i].get()));
|
||||
}
|
||||
RETURN_Z3(reinterpret_cast<Z3_literals>(lbls));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_literals Z3_API Z3_get_guessed_literals(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_guessed_literals(c);
|
||||
RESET_ERROR_CODE();
|
||||
ast_manager& m = mk_c(c)->m();
|
||||
expr_ref_vector lits(m);
|
||||
mk_c(c)->get_smt_kernel().get_guessed_literals(lits);
|
||||
labels* lbls = alloc(labels);
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
lbls->push_back(labeled_literal(m,lits[i].get()));
|
||||
}
|
||||
RETURN_Z3(reinterpret_cast<Z3_literals>(lbls));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
void Z3_API Z3_del_literals(Z3_context c, Z3_literals lbls) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_del_literals(c, lbls);
|
||||
RESET_ERROR_CODE();
|
||||
dealloc(reinterpret_cast<labels*>(lbls));
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
unsigned Z3_API Z3_get_num_literals(Z3_context c,Z3_literals lbls) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_num_literals(c, lbls);
|
||||
RESET_ERROR_CODE();
|
||||
return reinterpret_cast<labels*>(lbls)->size();
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_symbol Z3_API Z3_get_label_symbol(Z3_context c,Z3_literals lbls, unsigned idx) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_label_symbol(c, lbls, idx);
|
||||
RESET_ERROR_CODE();
|
||||
return of_symbol((*reinterpret_cast<labels*>(lbls))[idx].get_label());
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_get_literal(Z3_context c,Z3_literals lbls, unsigned idx) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_literal(c, lbls, idx);
|
||||
RESET_ERROR_CODE();
|
||||
expr* e = (*reinterpret_cast<labels*>(lbls))[idx].get_literal();
|
||||
mk_c(c)->save_ast_trail(e);
|
||||
RETURN_Z3(of_ast(e));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
void Z3_API Z3_disable_literal(Z3_context c, Z3_literals lbls, unsigned idx) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_disable_literal(c, lbls, idx);
|
||||
RESET_ERROR_CODE();
|
||||
(*reinterpret_cast<labels*>(lbls))[idx].disable();
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
void Z3_API Z3_block_literals(Z3_context c, Z3_literals lbls) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_block_literals(c, lbls);
|
||||
RESET_ERROR_CODE();
|
||||
labels* _lbls = reinterpret_cast<labels*>(lbls);
|
||||
ast_manager& m = mk_c(c)->m();
|
||||
expr_ref_vector lits(m);
|
||||
for (unsigned i = 0; i < _lbls->size(); ++i) {
|
||||
if ((*_lbls)[i].is_enabled()) {
|
||||
lits.push_back(m.mk_not((*_lbls)[i].get_literal()));
|
||||
}
|
||||
}
|
||||
expr_ref clause(m);
|
||||
clause = m.mk_or(lits.size(), lits.c_ptr());
|
||||
mk_c(c)->save_ast_trail(clause.get());
|
||||
mk_c(c)->assert_cnstr(clause.get());
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
Z3_API char const * Z3_context_to_string(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_context_to_string(c);
|
||||
RESET_ERROR_CODE();
|
||||
std::ostringstream buffer;
|
||||
mk_c(c)->get_smt_kernel().display(buffer);
|
||||
return mk_c(c)->mk_external_string(buffer.str());
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_get_context_assignment(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_context_assignment(c);
|
||||
RESET_ERROR_CODE();
|
||||
ast_manager& m = mk_c(c)->m();
|
||||
expr_ref result(m);
|
||||
expr_ref_vector assignment(m);
|
||||
mk_c(c)->get_smt_kernel().get_assignments(assignment);
|
||||
result = mk_c(c)->mk_and(assignment.size(), assignment.c_ptr());
|
||||
RETURN_Z3(of_ast(result.get()));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_string Z3_API Z3_statistics_to_string(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_statistics_to_string(c);
|
||||
RESET_ERROR_CODE();
|
||||
std::ostringstream buffer;
|
||||
mk_c(c)->get_smt_kernel().display_statistics(buffer);
|
||||
memory::display_max_usage(buffer);
|
||||
return mk_c(c)->mk_external_string(buffer.str());
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
void Z3_API Z3_soft_check_cancel(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_soft_check_cancel(c);
|
||||
RESET_ERROR_CODE();
|
||||
mk_c(c)->interrupt();
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
void Z3_display_statistics(Z3_context c, std::ostream& s) {
|
||||
mk_c(c)->get_smt_kernel().display_statistics(s);
|
||||
}
|
||||
|
||||
void Z3_display_istatistics(Z3_context c, std::ostream& s) {
|
||||
mk_c(c)->get_smt_kernel().display_istatistics(s);
|
||||
}
|
||||
|
|
@ -128,11 +128,20 @@ namespace z3 {
|
|||
Z3_set_error_handler(m_ctx, error_handler);
|
||||
Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
|
||||
}
|
||||
|
||||
void init_interp(config & c) {
|
||||
m_ctx = Z3_mk_interpolation_context(c);
|
||||
Z3_set_error_handler(m_ctx, error_handler);
|
||||
Z3_set_ast_print_mode(m_ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
|
||||
}
|
||||
|
||||
context(context const & s);
|
||||
context & operator=(context const & s);
|
||||
public:
|
||||
struct interpolation {};
|
||||
context() { config c; init(c); }
|
||||
context(config & c) { init(c); }
|
||||
context(config & c, interpolation) { init_interp(c); }
|
||||
~context() { Z3_del_context(m_ctx); }
|
||||
operator Z3_context() const { return m_ctx; }
|
||||
|
||||
|
|
|
@ -31,81 +31,6 @@ namespace Microsoft.Z3
|
|||
public class Deprecated
|
||||
{
|
||||
|
||||
/// <summary>
|
||||
/// Creates a backtracking point.
|
||||
/// </summary>
|
||||
/// <seealso cref="Pop"/>
|
||||
public static void Push(Context ctx) {
|
||||
Native.Z3_push(ctx.nCtx);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Backtracks <paramref name="n"/> backtracking points.
|
||||
/// </summary>
|
||||
/// <remarks>Note that an exception is thrown if <paramref name="n"/> is not smaller than <c>NumScopes</c></remarks>
|
||||
/// <seealso cref="Push"/>
|
||||
public static void Pop(Context ctx, uint n = 1) {
|
||||
Native.Z3_pop(ctx.nCtx, n);
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Assert a constraint (or multiple) into the solver.
|
||||
/// </summary>
|
||||
public static void Assert(Context ctx, params BoolExpr[] constraints)
|
||||
{
|
||||
Contract.Requires(constraints != null);
|
||||
Contract.Requires(Contract.ForAll(constraints, c => c != null));
|
||||
|
||||
ctx.CheckContextMatch(constraints);
|
||||
foreach (BoolExpr a in constraints)
|
||||
{
|
||||
Native.Z3_assert_cnstr(ctx.nCtx, a.NativeObject);
|
||||
}
|
||||
}
|
||||
/// <summary>
|
||||
/// Checks whether the assertions in the context are consistent or not.
|
||||
/// </summary>
|
||||
public static Status Check(Context ctx, List<BoolExpr> core, ref Model model, ref Expr proof, params Expr[] assumptions)
|
||||
{
|
||||
Z3_lbool r;
|
||||
model = null;
|
||||
proof = null;
|
||||
if (assumptions == null || assumptions.Length == 0)
|
||||
r = (Z3_lbool)Native.Z3_check(ctx.nCtx);
|
||||
else {
|
||||
IntPtr mdl = IntPtr.Zero, prf = IntPtr.Zero;
|
||||
uint core_size = 0;
|
||||
IntPtr[] native_core = new IntPtr[assumptions.Length];
|
||||
r = (Z3_lbool)Native.Z3_check_assumptions(ctx.nCtx,
|
||||
(uint)assumptions.Length, AST.ArrayToNative(assumptions),
|
||||
ref mdl, ref prf, ref core_size, native_core);
|
||||
|
||||
for (uint i = 0; i < core_size; i++)
|
||||
core.Add((BoolExpr)Expr.Create(ctx, native_core[i]));
|
||||
if (mdl != IntPtr.Zero) {
|
||||
model = new Model(ctx, mdl);
|
||||
}
|
||||
if (prf != IntPtr.Zero) {
|
||||
proof = Expr.Create(ctx, prf);
|
||||
}
|
||||
|
||||
}
|
||||
switch (r)
|
||||
{
|
||||
case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
|
||||
case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
|
||||
default: return Status.UNKNOWN;
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Retrieves an assignment to atomic propositions for a satisfiable context.
|
||||
/// </summary>
|
||||
public static BoolExpr GetAssignment(Context ctx)
|
||||
{
|
||||
IntPtr x = Native.Z3_get_context_assignment(ctx.nCtx);
|
||||
return (BoolExpr)Expr.Create(ctx, x);
|
||||
}
|
||||
|
||||
}
|
||||
}
|
807
src/api/z3_api.h
807
src/api/z3_api.h
|
@ -1552,8 +1552,6 @@ extern "C" {
|
|||
|
||||
\conly \sa Z3_del_context
|
||||
|
||||
\conly \deprecated Use #Z3_mk_context_rc
|
||||
|
||||
def_API('Z3_mk_context', CONTEXT, (_in(CONFIG),))
|
||||
*/
|
||||
#ifdef CorML3
|
||||
|
@ -5318,24 +5316,14 @@ END_MLAPI_EXCLUDE
|
|||
*/
|
||||
void Z3_API Z3_set_error(Z3_context c, Z3_error_code e);
|
||||
|
||||
#ifdef Conly
|
||||
/**
|
||||
\brief Return a string describing the given error code.
|
||||
|
||||
\deprecated Use #Z3_get_error_msg_ex instead.
|
||||
|
||||
def_API('Z3_get_error_msg', STRING, (_in(ERROR_CODE),))
|
||||
*/
|
||||
Z3_string Z3_API Z3_get_error_msg(Z3_error_code err);
|
||||
#endif
|
||||
|
||||
BEGIN_MLAPI_EXCLUDE
|
||||
/**
|
||||
\brief Return a string describing the given error code.
|
||||
|
||||
def_API('Z3_get_error_msg_ex', STRING, (_in(CONTEXT), _in(ERROR_CODE)))
|
||||
def_API('Z3_get_error_msg', STRING, (_in(CONTEXT), _in(ERROR_CODE)))
|
||||
*/
|
||||
Z3_string Z3_API Z3_get_error_msg_ex(Z3_context c, Z3_error_code err);
|
||||
Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err);
|
||||
END_MLAPI_EXCLUDE
|
||||
#ifdef ML4only
|
||||
#include <mlx_get_error_msg.idl>
|
||||
|
@ -7226,6 +7214,37 @@ END_MLAPI_EXCLUDE
|
|||
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s,
|
||||
unsigned num_assumptions, Z3_ast const assumptions[]);
|
||||
|
||||
|
||||
|
||||
#ifdef CorML4
|
||||
/**
|
||||
\brief 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 Z3_L_FALSE if the current assertions are not satisfiable.
|
||||
|
||||
|
||||
|
||||
def_API('Z3_get_implied_equalities', INT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT)))
|
||||
*/
|
||||
Z3_lbool Z3_API Z3_get_implied_equalities(
|
||||
Z3_context c,
|
||||
Z3_solver s,
|
||||
unsigned num_terms,
|
||||
Z3_ast const terms[],
|
||||
unsigned class_ids[]
|
||||
);
|
||||
#endif
|
||||
/**
|
||||
\brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions
|
||||
|
||||
|
@ -7372,769 +7391,9 @@ END_MLAPI_EXCLUDE
|
|||
#endif
|
||||
|
||||
|
||||
#ifdef CorML3
|
||||
|
||||
/**
|
||||
@name Deprecated Injective functions API
|
||||
*/
|
||||
/*@{*/
|
||||
|
||||
/**
|
||||
\brief Create injective function declaration
|
||||
|
||||
\deprecated This method just asserts a (universally quantified) formula that asserts that
|
||||
the new function is injective. It is compatible with the old interface for solving:
|
||||
#Z3_assert_cnstr, #Z3_check_assumptions, etc.
|
||||
|
||||
def_API('Z3_mk_injective_function', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT)))
|
||||
*/
|
||||
Z3_func_decl Z3_API Z3_mk_injective_function(
|
||||
Z3_context c,
|
||||
Z3_symbol s,
|
||||
unsigned domain_size, Z3_sort const domain[],
|
||||
Z3_sort range
|
||||
);
|
||||
|
||||
/*@}*/
|
||||
#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
|
||||
#Z3_check, #Z3_check_and_get_model, #Z3_check_assumptions and #Z3_push.
|
||||
Return \c Z3_TRUE if the logic was changed successfully, and \c Z3_FALSE otherwise.
|
||||
|
||||
\deprecated Subsumed by #Z3_mk_solver_for_logic
|
||||
|
||||
def_API('Z3_set_logic', VOID, (_in(CONTEXT), _in(STRING)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_set_logic(Z3_context c, Z3_string logic);
|
||||
|
||||
/**
|
||||
\brief Create a backtracking point.
|
||||
|
||||
The logical context can be viewed as a stack of contexts. The
|
||||
scope level is the number of elements on this stack. The stack
|
||||
of contexts is simulated using trail (undo) stacks.
|
||||
|
||||
\sa Z3_pop
|
||||
|
||||
\deprecated Subsumed by #Z3_solver_push
|
||||
|
||||
def_API('Z3_push', VOID, (_in(CONTEXT),))
|
||||
*/
|
||||
void Z3_API Z3_push(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Backtrack.
|
||||
|
||||
Restores the context from the top of the stack, and pops it off the
|
||||
stack. Any changes to the logical context (by #Z3_assert_cnstr or
|
||||
other functions) between the matching #Z3_push and \c Z3_pop
|
||||
operators are flushed, and the context is completely restored to
|
||||
what it was right before the #Z3_push.
|
||||
|
||||
\sa Z3_push
|
||||
|
||||
\deprecated Subsumed by #Z3_solver_pop
|
||||
|
||||
def_API('Z3_pop', VOID, (_in(CONTEXT), _in(UINT)))
|
||||
*/
|
||||
void Z3_API Z3_pop(Z3_context c, unsigned num_scopes);
|
||||
|
||||
/**
|
||||
\brief Retrieve the current scope level.
|
||||
|
||||
It retrieves the number of scopes that have been pushed, but not yet popped.
|
||||
|
||||
\sa Z3_push
|
||||
\sa Z3_pop
|
||||
|
||||
\deprecated Subsumed by #Z3_solver_get_num_scopes.
|
||||
|
||||
def_API('Z3_get_num_scopes', UINT, (_in(CONTEXT),))
|
||||
*/
|
||||
unsigned Z3_API Z3_get_num_scopes(Z3_context c);
|
||||
|
||||
/**
|
||||
\conly \brief Persist AST through num_scopes pops.
|
||||
\conly This function is only relevant if \c c was created using #Z3_mk_context.
|
||||
\conly If \c c was created using #Z3_mk_context_rc, this function is a NOOP.
|
||||
|
||||
\conly Normally, for contexts created using #Z3_mk_context,
|
||||
\conly references to terms are no longer valid when
|
||||
\conly popping scopes beyond the level where the terms are created.
|
||||
\conly If you want to reference a term below the scope where it
|
||||
\conly was created, use this method to specify how many pops
|
||||
\conly the term should survive.
|
||||
\conly The num_scopes should be at most equal to the number of
|
||||
\conly calls to Z3_push subtracted with the calls to Z3_pop.
|
||||
|
||||
\conly \deprecated Z3 users should move to #Z3_mk_context_rc and use the
|
||||
\conly reference counting APIs for managing AST nodes.
|
||||
|
||||
\mlonly \deprecated This function has no effect. \endmlonly
|
||||
|
||||
def_API('Z3_persist_ast', VOID, (_in(CONTEXT), _in(AST), _in(UINT)))
|
||||
*/
|
||||
void Z3_API Z3_persist_ast(Z3_context c, Z3_ast a, unsigned num_scopes);
|
||||
|
||||
/**
|
||||
\brief Assert a constraint into the logical context.
|
||||
|
||||
After one assertion, the logical context may become
|
||||
inconsistent.
|
||||
|
||||
The functions #Z3_check or #Z3_check_and_get_model should be
|
||||
used to check whether the logical context is consistent or not.
|
||||
|
||||
\sa Z3_check
|
||||
\sa Z3_check_and_get_model
|
||||
|
||||
\deprecated Subsumed by #Z3_solver_assert
|
||||
|
||||
def_API('Z3_assert_cnstr', VOID, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
void Z3_API Z3_assert_cnstr(Z3_context c, Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief Check whether the given logical context is consistent or not.
|
||||
|
||||
If the logical context is not unsatisfiable (i.e., the return value is different from \c Z3_L_FALSE)
|
||||
and model construction is enabled (see #Z3_mk_config),
|
||||
\conly then a model is stored in \c m. Otherwise, the value \c NULL is stored in \c m.
|
||||
\mlonly then a valid model is returned. Otherwise, it is unsafe to use the returned model.\endmlonly
|
||||
\conly The caller is responsible for deleting the model using the function #Z3_del_model.
|
||||
|
||||
\conly \remark In contrast with the rest of the Z3 API, the reference counter of the
|
||||
\conly model is incremented. This is to guarantee backward compatibility. In previous
|
||||
\conly versions, models did not support reference counting.
|
||||
|
||||
\remark Model construction must be enabled using configuration
|
||||
parameters (See, #Z3_mk_config).
|
||||
|
||||
\sa Z3_check
|
||||
\conly \sa Z3_del_model
|
||||
|
||||
\deprecated Subsumed by #Z3_solver_check
|
||||
|
||||
def_API('Z3_check_and_get_model', INT, (_in(CONTEXT), _out(MODEL)))
|
||||
*/
|
||||
Z3_lbool Z3_API Z3_check_and_get_model(Z3_context c, Z3_model * m);
|
||||
|
||||
/**
|
||||
\brief Check whether the given logical context is consistent or not.
|
||||
|
||||
The function #Z3_check_and_get_model should be used when models are needed.
|
||||
|
||||
\sa Z3_check_and_get_model
|
||||
|
||||
\deprecated Subsumed by #Z3_solver_check
|
||||
|
||||
def_API('Z3_check', INT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_lbool Z3_API Z3_check(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Check whether the given logical context and optional assumptions is consistent or not.
|
||||
|
||||
If the logical context is not unsatisfiable (i.e., the return value is different from \c Z3_L_FALSE),
|
||||
\conly a non-NULL model argument is passed in,
|
||||
and model construction is enabled (see #Z3_mk_config),
|
||||
\conly then a model is stored in \c m. Otherwise, \c m is left unchanged.
|
||||
\mlonly then a valid model is returned. Otherwise, it is unsafe to use the returned model.\endmlonly
|
||||
\conly The caller is responsible for deleting the model using the function #Z3_del_model.
|
||||
|
||||
\conly \remark If the model argument is non-NULL, then model construction must be enabled using configuration
|
||||
\conly parameters (See, #Z3_mk_config).
|
||||
|
||||
\param c logical context.
|
||||
\param num_assumptions number of auxiliary assumptions.
|
||||
\param assumptions array of auxiliary assumptions
|
||||
\param m optional pointer to a model.
|
||||
\param proof optional pointer to a proof term.
|
||||
\param core_size size of unsatisfiable core.
|
||||
\param core pointer to an array receiving unsatisfiable core.
|
||||
The unsatisfiable core is a subset of the assumptions, so the array has the same size as the assumptions.
|
||||
The \c core array is not populated if \c core_size is set to 0.
|
||||
|
||||
\pre assumptions comprises of propositional literals.
|
||||
In other words, you cannot use compound formulas for assumptions,
|
||||
but should use propositional variables or negations of propositional variables.
|
||||
|
||||
\conly \remark In constrast with the rest of the Z3 API, the reference counter of the
|
||||
\conly model is incremented. This is to guarantee backward compatibility. In previous
|
||||
\conly versions, models did not support reference counting.
|
||||
|
||||
\sa Z3_check
|
||||
\conly \sa Z3_del_model
|
||||
|
||||
\deprecated Subsumed by #Z3_solver_check_assumptions
|
||||
|
||||
def_API('Z3_check_assumptions', INT, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _out(MODEL), _out(AST), _out(UINT), _out_array2(1, 5, AST)))
|
||||
*/
|
||||
Z3_lbool Z3_API Z3_check_assumptions(
|
||||
Z3_context c,
|
||||
unsigned num_assumptions, Z3_ast const assumptions[],
|
||||
Z3_model * m, Z3_ast* proof,
|
||||
unsigned* core_size, Z3_ast core[]
|
||||
);
|
||||
#endif
|
||||
|
||||
#ifdef CorML4
|
||||
/**
|
||||
\brief 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 Z3_L_FALSE if the current assertions are not satisfiable.
|
||||
|
||||
\sa Z3_check_and_get_model
|
||||
\sa Z3_check
|
||||
|
||||
\deprecated To be moved outside of API.
|
||||
|
||||
def_API('Z3_get_implied_equalities', INT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT)))
|
||||
*/
|
||||
Z3_lbool Z3_API Z3_get_implied_equalities(
|
||||
Z3_context c,
|
||||
Z3_solver s,
|
||||
unsigned num_terms,
|
||||
Z3_ast const terms[],
|
||||
unsigned class_ids[]
|
||||
);
|
||||
#endif
|
||||
|
||||
#ifdef CorML3
|
||||
/**
|
||||
\brief Delete a model object.
|
||||
|
||||
\sa Z3_check_and_get_model
|
||||
|
||||
\conly \remark The Z3_check_and_get_model automatically increments a reference count on the model.
|
||||
\conly The expected usage is that models created by that method are deleted using Z3_del_model.
|
||||
\conly This is for backwards compatibility and in contrast to the rest of the API where
|
||||
\conly callers are responsible for managing reference counts.
|
||||
|
||||
\deprecated Subsumed by Z3_solver API
|
||||
|
||||
def_API('Z3_del_model', VOID, (_in(CONTEXT), _in(MODEL)))
|
||||
*/
|
||||
void Z3_API Z3_del_model(Z3_context c, Z3_model m);
|
||||
|
||||
/*@}*/
|
||||
|
||||
/**
|
||||
@name Deprecated Search control API
|
||||
*/
|
||||
/*@{*/
|
||||
|
||||
/**
|
||||
\brief Cancel an ongoing check.
|
||||
|
||||
Notifies the current check to abort and return.
|
||||
This method should be called from a different thread
|
||||
than the one performing the check.
|
||||
|
||||
\deprecated Use #Z3_interrupt instead.
|
||||
|
||||
def_API('Z3_soft_check_cancel', VOID, (_in(CONTEXT), ))
|
||||
*/
|
||||
void Z3_API Z3_soft_check_cancel(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Retrieve reason for search failure.
|
||||
|
||||
If a call to #Z3_check or #Z3_check_and_get_model returns Z3_L_UNDEF,
|
||||
use this facility to determine the more detailed cause of search failure.
|
||||
|
||||
\deprecated Subsumed by #Z3_solver_get_reason_unknown
|
||||
|
||||
def_API('Z3_get_search_failure', UINT, (_in(CONTEXT), ))
|
||||
*/
|
||||
Z3_search_failure Z3_API Z3_get_search_failure(Z3_context c);
|
||||
|
||||
/*@}*/
|
||||
|
||||
/**
|
||||
@name Deprecated Labels API
|
||||
*/
|
||||
/*@{*/
|
||||
|
||||
/**
|
||||
\brief Create a labeled formula.
|
||||
|
||||
\param c logical context.
|
||||
\param s name of the label.
|
||||
\param is_pos label polarity.
|
||||
\param f formula being labeled.
|
||||
|
||||
A label behaves as an identity function, so the truth value of the
|
||||
labeled formula is unchanged. Labels are used for identifying
|
||||
useful sub-formulas when generating counter-examples.
|
||||
|
||||
\deprecated Labels are only supported by the old Solver API.
|
||||
This feature is not essential (it can be simulated using auxiliary Boolean variables).
|
||||
It is only available for backward compatibility.
|
||||
|
||||
def_API('Z3_mk_label', AST, (_in(CONTEXT), _in(SYMBOL), _in(BOOL), _in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_label(Z3_context c, Z3_symbol s, Z3_bool is_pos, Z3_ast f);
|
||||
|
||||
/**
|
||||
\brief Retrieve the set of labels that were relevant in
|
||||
the context of the current satisfied context.
|
||||
|
||||
\sa Z3_del_literals
|
||||
\sa Z3_get_num_literals
|
||||
\sa Z3_get_label_symbol
|
||||
\sa Z3_get_literal
|
||||
|
||||
\deprecated This procedure is based on the old Solver API.
|
||||
|
||||
def_API('Z3_get_relevant_labels', LITERALS, (_in(CONTEXT), ))
|
||||
*/
|
||||
Z3_literals Z3_API Z3_get_relevant_labels(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Retrieve the set of literals that satisfy the current context.
|
||||
|
||||
\sa Z3_del_literals
|
||||
\sa Z3_get_num_literals
|
||||
\sa Z3_get_label_symbol
|
||||
\sa Z3_get_literal
|
||||
|
||||
\deprecated This procedure is based on the old Solver API.
|
||||
|
||||
def_API('Z3_get_relevant_literals', LITERALS, (_in(CONTEXT), ))
|
||||
*/
|
||||
Z3_literals Z3_API Z3_get_relevant_literals(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Retrieve the set of literals that whose assignment were
|
||||
guess, but not propagated during the search.
|
||||
|
||||
\sa Z3_del_literals
|
||||
\sa Z3_get_num_literals
|
||||
\sa Z3_get_label_symbol
|
||||
\sa Z3_get_literal
|
||||
|
||||
\deprecated This procedure is based on the old Solver API.
|
||||
|
||||
def_API('Z3_get_guessed_literals', LITERALS, (_in(CONTEXT), ))
|
||||
*/
|
||||
Z3_literals Z3_API Z3_get_guessed_literals(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Delete a labels context.
|
||||
|
||||
\sa Z3_get_relevant_labels
|
||||
|
||||
\deprecated This procedure is based on the old Solver API.
|
||||
|
||||
def_API('Z3_del_literals', VOID, (_in(CONTEXT), _in(LITERALS)))
|
||||
*/
|
||||
void Z3_API Z3_del_literals(Z3_context c, Z3_literals lbls);
|
||||
|
||||
/**
|
||||
\brief Retrieve the number of label symbols that were returned.
|
||||
|
||||
\sa Z3_get_relevant_labels
|
||||
|
||||
\deprecated This procedure is based on the old Solver API.
|
||||
|
||||
def_API('Z3_get_num_literals', UINT, (_in(CONTEXT), _in(LITERALS)))
|
||||
*/
|
||||
unsigned Z3_API Z3_get_num_literals(Z3_context c, Z3_literals lbls);
|
||||
|
||||
/**
|
||||
\brief Retrieve label symbol at idx.
|
||||
|
||||
\deprecated This procedure is based on the old Solver API.
|
||||
|
||||
def_API('Z3_get_label_symbol', SYMBOL, (_in(CONTEXT), _in(LITERALS), _in(UINT)))
|
||||
*/
|
||||
Z3_symbol Z3_API Z3_get_label_symbol(Z3_context c, Z3_literals lbls, unsigned idx);
|
||||
|
||||
/**
|
||||
\brief Retrieve literal expression at idx.
|
||||
|
||||
\deprecated This procedure is based on the old Solver API.
|
||||
|
||||
def_API('Z3_get_literal', AST, (_in(CONTEXT), _in(LITERALS), _in(UINT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_get_literal(Z3_context c, Z3_literals lbls, unsigned idx);
|
||||
|
||||
/**
|
||||
\brief Disable label.
|
||||
|
||||
The disabled label is not going to be used when blocking the subsequent search.
|
||||
|
||||
\sa Z3_block_literals
|
||||
|
||||
\deprecated This procedure is based on the old Solver API.
|
||||
|
||||
def_API('Z3_disable_literal', VOID, (_in(CONTEXT), _in(LITERALS), _in(UINT)))
|
||||
*/
|
||||
void Z3_API Z3_disable_literal(Z3_context c, Z3_literals lbls, unsigned idx);
|
||||
|
||||
/**
|
||||
\brief Block subsequent checks using the remaining enabled labels.
|
||||
|
||||
\deprecated This procedure is based on the old Solver API.
|
||||
|
||||
def_API('Z3_block_literals', VOID, (_in(CONTEXT), _in(LITERALS)))
|
||||
*/
|
||||
void Z3_API Z3_block_literals(Z3_context c, Z3_literals lbls);
|
||||
|
||||
/*@}*/
|
||||
|
||||
/**
|
||||
@name Deprecated Model API
|
||||
*/
|
||||
/*@{*/
|
||||
|
||||
/**
|
||||
\brief Return the number of constants assigned by the given model.
|
||||
|
||||
\mlonly \remark Consider using {!get_model_constants}. \endmlonly
|
||||
|
||||
\sa Z3_get_model_constant
|
||||
|
||||
\deprecated use #Z3_model_get_num_consts
|
||||
|
||||
def_API('Z3_get_model_num_constants', UINT, (_in(CONTEXT), _in(MODEL)))
|
||||
*/
|
||||
unsigned Z3_API Z3_get_model_num_constants(Z3_context c, Z3_model m);
|
||||
|
||||
/**
|
||||
\brief \mlh get_model_constant c m i \endmlh
|
||||
Return the i-th constant in the given model.
|
||||
|
||||
\mlonly \remark Consider using {!get_model_constants}. \endmlonly
|
||||
|
||||
\pre i < Z3_get_model_num_constants(c, m)
|
||||
|
||||
\deprecated use #Z3_model_get_const_decl
|
||||
|
||||
def_API('Z3_get_model_constant', FUNC_DECL, (_in(CONTEXT), _in(MODEL), _in(UINT)))
|
||||
*/
|
||||
Z3_func_decl Z3_API Z3_get_model_constant(Z3_context c, Z3_model m, unsigned i);
|
||||
|
||||
/**
|
||||
\brief Return the number of function interpretations in the given model.
|
||||
|
||||
A function interpretation is represented as a finite map and an 'else' value.
|
||||
Each entry in the finite map represents the value of a function given a set of arguments.
|
||||
|
||||
\deprecated use #Z3_model_get_num_funcs
|
||||
|
||||
def_API('Z3_get_model_num_funcs', UINT, (_in(CONTEXT), _in(MODEL)))
|
||||
*/
|
||||
unsigned Z3_API Z3_get_model_num_funcs(Z3_context c, Z3_model m);
|
||||
|
||||
/**
|
||||
\brief \mlh get_model_func_decl c m i \endmlh
|
||||
Return the declaration of the i-th function in the given model.
|
||||
|
||||
\pre i < Z3_get_model_num_funcs(c, m)
|
||||
|
||||
\sa Z3_get_model_num_funcs
|
||||
|
||||
\deprecated use #Z3_model_get_func_decl
|
||||
|
||||
def_API('Z3_get_model_func_decl', FUNC_DECL, (_in(CONTEXT), _in(MODEL), _in(UINT)))
|
||||
*/
|
||||
Z3_func_decl Z3_API Z3_get_model_func_decl(Z3_context c, Z3_model m, unsigned i);
|
||||
|
||||
/**
|
||||
\brief Return the value of the given constant or function
|
||||
in the given model.
|
||||
|
||||
\deprecated Consider using #Z3_model_eval or #Z3_model_get_func_interp
|
||||
|
||||
def_API('Z3_eval_func_decl', BOOL, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL), _out(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_eval_func_decl(Z3_context c, Z3_model m, Z3_func_decl decl, Z3_ast* v);
|
||||
|
||||
/**
|
||||
\brief \mlh is_array_value c v \endmlh
|
||||
Determine whether the term encodes an array value.
|
||||
A term encodes an array value if it is a nested sequence of
|
||||
applications of store on top of a constant array.
|
||||
The indices to the stores have to be values (for example, integer constants)
|
||||
so that equality between the indices can be evaluated.
|
||||
Array values are useful for representing interpretations for arrays.
|
||||
|
||||
Return the number of entries mapping to non-default values of the array.
|
||||
|
||||
\deprecated Use #Z3_is_as_array
|
||||
|
||||
def_API('Z3_is_array_value', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _out(UINT)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_is_array_value(Z3_context c, Z3_model m, Z3_ast v, unsigned* num_entries);
|
||||
|
||||
/**
|
||||
\brief \mlh get_array_value c v \endmlh
|
||||
An array values is represented as a dictionary plus a
|
||||
default (else) value. This function returns the array graph.
|
||||
|
||||
\pre Z3_TRUE == Z3_is_array_value(c, v, &num_entries)
|
||||
|
||||
\deprecated Use Z3_func_interp objects and #Z3_get_as_array_func_decl
|
||||
|
||||
def_API('Z3_get_array_value', VOID, (_in(CONTEXT), _in(MODEL), _in(AST), _in(UINT), _out_array(3, AST), _out_array(3, AST), _out (AST)))
|
||||
*/
|
||||
void Z3_API Z3_get_array_value(Z3_context c,
|
||||
Z3_model m,
|
||||
Z3_ast v,
|
||||
unsigned num_entries,
|
||||
Z3_ast indices[],
|
||||
Z3_ast values[],
|
||||
Z3_ast* else_value
|
||||
);
|
||||
|
||||
/**
|
||||
\brief \mlh get_model_func_else c m i \endmlh
|
||||
Return the 'else' value of the i-th function interpretation in the given model.
|
||||
|
||||
A function interpretation is represented as a finite map and an 'else' value.
|
||||
|
||||
\mlonly \remark Consider using {!get_model_funcs}. \endmlonly
|
||||
|
||||
\pre i < Z3_get_model_num_funcs(c, m)
|
||||
|
||||
\sa Z3_get_model_num_funcs
|
||||
\sa Z3_get_model_func_num_entries
|
||||
\sa Z3_get_model_func_entry_num_args
|
||||
\sa Z3_get_model_func_entry_arg
|
||||
|
||||
\deprecated Use Z3_func_interp objects
|
||||
|
||||
def_API('Z3_get_model_func_else', AST, (_in(CONTEXT), _in(MODEL), _in(UINT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_get_model_func_else(Z3_context c, Z3_model m, unsigned i);
|
||||
|
||||
/**
|
||||
\brief \mlh get_model_func_num_entries c m i \endmlh
|
||||
Return the number of entries of the i-th function interpretation in the given model.
|
||||
|
||||
A function interpretation is represented as a finite map and an 'else' value.
|
||||
|
||||
\mlonly \remark Consider using {!get_model_funcs}. \endmlonly
|
||||
|
||||
\pre i < Z3_get_model_num_funcs(c, m)
|
||||
|
||||
\sa Z3_get_model_num_funcs
|
||||
\sa Z3_get_model_func_else
|
||||
\sa Z3_get_model_func_entry_num_args
|
||||
\sa Z3_get_model_func_entry_arg
|
||||
|
||||
\deprecated Use Z3_func_interp objects
|
||||
|
||||
def_API('Z3_get_model_func_num_entries', UINT, (_in(CONTEXT), _in(MODEL), _in(UINT)))
|
||||
*/
|
||||
unsigned Z3_API Z3_get_model_func_num_entries(Z3_context c, Z3_model m, unsigned i);
|
||||
|
||||
/**
|
||||
\brief \mlh get_model_func_entry_num_args c m i j \endmlh
|
||||
Return the number of arguments of the j-th entry of the i-th function interpretation in the given
|
||||
model.
|
||||
|
||||
A function interpretation is represented as a finite map and an 'else' value.
|
||||
This function returns the j-th entry of this map.
|
||||
|
||||
An entry represents the value of a function given a set of arguments.
|
||||
\conly That is: it has the following format <tt>f(args[0],...,args[num_args - 1]) = val</tt>.
|
||||
|
||||
\mlonly \remark Consider using {!get_model_funcs}. \endmlonly
|
||||
|
||||
\pre i < Z3_get_model_num_funcs(c, m)
|
||||
\pre j < Z3_get_model_func_num_entries(c, m, i)
|
||||
|
||||
\sa Z3_get_model_num_funcs
|
||||
\sa Z3_get_model_func_num_entries
|
||||
\sa Z3_get_model_func_entry_arg
|
||||
|
||||
\deprecated Use Z3_func_interp objects
|
||||
|
||||
def_API('Z3_get_model_func_entry_num_args', UINT, (_in(CONTEXT), _in(MODEL), _in(UINT), _in(UINT)))
|
||||
*/
|
||||
unsigned Z3_API Z3_get_model_func_entry_num_args(Z3_context c,
|
||||
Z3_model m,
|
||||
unsigned i,
|
||||
unsigned j);
|
||||
|
||||
/**
|
||||
\brief \mlh get_model_func_entry_arg c m i j k \endmlh
|
||||
Return the k-th argument of the j-th entry of the i-th function interpretation in the given
|
||||
model.
|
||||
|
||||
A function interpretation is represented as a finite map and an 'else' value.
|
||||
This function returns the j-th entry of this map.
|
||||
|
||||
An entry represents the value of a function given a set of arguments.
|
||||
\conly That is: it has the following format <tt>f(args[0],...,args[num_args - 1]) = val</tt>.
|
||||
|
||||
\mlonly \remark Consider using {!get_model_funcs}. \endmlonly
|
||||
|
||||
\pre i < Z3_get_model_num_funcs(c, m)
|
||||
\pre j < Z3_get_model_func_num_entries(c, m, i)
|
||||
\pre k < Z3_get_model_func_entry_num_args(c, m, i, j)
|
||||
|
||||
\sa Z3_get_model_num_funcs
|
||||
\sa Z3_get_model_func_num_entries
|
||||
\sa Z3_get_model_func_entry_num_args
|
||||
|
||||
\deprecated Use Z3_func_interp objects
|
||||
|
||||
def_API('Z3_get_model_func_entry_arg', AST, (_in(CONTEXT), _in(MODEL), _in(UINT), _in(UINT), _in(UINT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_get_model_func_entry_arg(Z3_context c,
|
||||
Z3_model m,
|
||||
unsigned i,
|
||||
unsigned j,
|
||||
unsigned k);
|
||||
|
||||
/**
|
||||
\brief \mlh get_model_func_entry_value c m i j \endmlh
|
||||
Return the return value of the j-th entry of the i-th function interpretation in the given
|
||||
model.
|
||||
|
||||
A function interpretation is represented as a finite map and an 'else' value.
|
||||
This function returns the j-th entry of this map.
|
||||
|
||||
An entry represents the value of a function given a set of arguments.
|
||||
\conly That is: it has the following format <tt>f(args[0],...,args[num_args - 1]) = val</tt>.
|
||||
|
||||
\mlonly \remark Consider using {!get_model_funcs}. \endmlonly
|
||||
|
||||
\pre i < Z3_get_model_num_funcs(c, m)
|
||||
\pre j < Z3_get_model_func_num_entries(c, m, i)
|
||||
|
||||
\sa Z3_get_model_num_funcs
|
||||
\sa Z3_get_model_func_num_entries
|
||||
|
||||
\deprecated Use Z3_func_interp objects
|
||||
|
||||
def_API('Z3_get_model_func_entry_value', AST, (_in(CONTEXT), _in(MODEL), _in(UINT), _in(UINT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_get_model_func_entry_value(Z3_context c,
|
||||
Z3_model m,
|
||||
unsigned i,
|
||||
unsigned j);
|
||||
|
||||
/**
|
||||
\brief \mlh eval c m t \endmlh
|
||||
Evaluate the AST node \c t in the given model.
|
||||
\conly Return \c Z3_TRUE if succeeded, and store the result in \c v.
|
||||
\mlonly Return a pair: Boolean and value. The Boolean is true if the term was successfully evaluated. \endmlonly
|
||||
|
||||
The evaluation may fail for the following reasons:
|
||||
|
||||
- \c t contains a quantifier.
|
||||
|
||||
- the model \c m is partial, that is, it doesn't have a complete interpretation for uninterpreted functions.
|
||||
That is, the option <tt>MODEL_PARTIAL=true</tt> was used.
|
||||
|
||||
- \c t is type incorrect.
|
||||
|
||||
\deprecated Use #Z3_model_eval
|
||||
|
||||
def_API('Z3_eval', BOOL, (_in(CONTEXT), _in(MODEL), _in(AST), _out(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_ast * v);
|
||||
|
||||
/**
|
||||
\brief Evaluate declaration given values.
|
||||
|
||||
Provides direct way to evaluate declarations
|
||||
without going over terms.
|
||||
|
||||
\deprecated Consider using #Z3_model_eval and #Z3_substitute_vars
|
||||
|
||||
def_API('Z3_eval_decl', BOOL, (_in(CONTEXT), _in(MODEL), _in(FUNC_DECL), _in(UINT), _in_array(3, AST), _out(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_eval_decl(Z3_context c, Z3_model m,
|
||||
Z3_func_decl d,
|
||||
unsigned num_args,
|
||||
Z3_ast const args[],
|
||||
Z3_ast* v);
|
||||
|
||||
/*@}*/
|
||||
|
||||
/**
|
||||
@name Deprecated String conversion API
|
||||
*/
|
||||
/*@{*/
|
||||
|
||||
/**
|
||||
\brief Convert the given logical context into a string.
|
||||
|
||||
This function is mainly used for debugging purposes. It displays
|
||||
the internal structure of a logical context.
|
||||
|
||||
\conly \warning The result buffer is statically allocated by Z3. It will
|
||||
\conly be automatically deallocated when #Z3_del_context is invoked.
|
||||
\conly So, the buffer is invalidated in the next call to \c Z3_context_to_string.
|
||||
|
||||
\deprecated This method is obsolete. It just displays the internal representation of
|
||||
the global solver available for backward compatibility reasons.
|
||||
|
||||
def_API('Z3_context_to_string', STRING, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_string Z3_API Z3_context_to_string(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Return runtime statistics as a string.
|
||||
|
||||
This function is mainly used for debugging purposes. It displays
|
||||
statistics of the search activity.
|
||||
|
||||
\conly \warning The result buffer is statically allocated by Z3. It will
|
||||
\conly be automatically deallocated when #Z3_del_context is invoked.
|
||||
\conly So, the buffer is invalidated in the next call to \c Z3_context_to_string.
|
||||
|
||||
\deprecated This method is based on the old solver API.
|
||||
Use #Z3_stats_to_string when using the new solver API.
|
||||
|
||||
def_API('Z3_statistics_to_string', STRING, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_string Z3_API Z3_statistics_to_string(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Extract satisfying assignment from context as a conjunction.
|
||||
|
||||
This function can be used for debugging purposes. It returns a conjunction
|
||||
of formulas that are assigned to true in the current context.
|
||||
This conjunction will contain not only the assertions that are set to true
|
||||
under the current assignment, but will also include additional literals
|
||||
if there has been a call to #Z3_check or #Z3_check_and_get_model.
|
||||
|
||||
\deprecated This method is based on the old solver API.
|
||||
|
||||
def_API('Z3_get_context_assignment', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_get_context_assignment(Z3_context c);
|
||||
|
||||
/*@}*/
|
||||
#endif
|
||||
|
||||
|
||||
#ifndef CAMLIDL
|
||||
|
|
Loading…
Reference in a new issue