mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-11-19 23:27:24 +01:00
commit 9175cf195d
16 changed files with 137 additions and 1621 deletions
Download patch file Download diff file Expand all files Collapse all files

98
examples/maxsat/maxsat.c
View file

@ -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.*/

12
scripts/update_api.py
View file

@ -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:
@ -632,7 +632,7 @@ def mk_java():
if len(params) > 0 and param_type(params[0]) == CONTEXT:
java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n')
java_native.write(' if (err != Z3_error_code.Z3_OK)\n')
java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n')
java_native.write(' throw new Z3Exception(INTERNALgetErrorMsg(a0, err.toInt()));\n')
if result != VOID:
java_native.write(' return res;\n')
java_native.write(' }\n\n')
@ -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')

14
src/api/api_ast.cpp
View file

@ -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) {

47
src/api/api_context.cpp
View file

@ -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;

2
src/api/api_context.h
View file

@ -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);

260
src/api/api_model.cpp
View file

@ -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;

36
src/api/api_quant.cpp
View file

@ -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);

3
src/api/api_solver.cpp
View file

@ -6,7 +6,8 @@ Module Name:
api_solver.cpp
Abstract:
New solver API
Solver API
Author:

358
src/api/api_solver_old.cpp
View file

@ -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);
}

9
src/api/c++/z3++.h
View file

@ -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; }

75
src/api/dotnet/Deprecated.cs
View file

@ -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
View file

@ -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

20
src/opt/opt_context.cpp
View file

@ -241,27 +241,37 @@ namespace opt {
TRACE("opt", model_smt2_pp(tout, m, *m_model, 0););
m_optsmt.setup(*m_opt_solver.get());
update_lower();
switch (m_objectives.size()) {
case 0:
return is_sat;
break;
case 1:
return execute(m_objectives[0], true, false);
is_sat = execute(m_objectives[0], true, false);
break;
default: {
opt_params optp(m_params);
symbol pri = optp.priority();
if (pri == symbol("pareto")) {
return execute_pareto();
is_sat = execute_pareto();
}
else if (pri == symbol("box")) {
return execute_box();
is_sat = execute_box();
}
else {
return execute_lex();
is_sat = execute_lex();
}
break;
}
}
return adjust_unknown(is_sat);
}
lbool context::adjust_unknown(lbool r) {
if (r == l_true && m_opt_solver.get() && m_opt_solver->was_unknown()) {
r = l_undef;
}
return r;
}
bool context::print_model() const {
opt_params optp(m_params);

1
src/opt/opt_context.h
View file

@ -229,6 +229,7 @@ namespace opt {
lbool execute_lex();
lbool execute_box();
lbool execute_pareto();
lbool adjust_unknown(lbool r);
bool scoped_lex();
expr_ref to_expr(inf_eps const& n);

12
src/opt/opt_solver.cpp
View file

@ -44,7 +44,8 @@ namespace opt {
m_fm(fm),
m_objective_terms(m),
m_dump_benchmarks(false),
m_first(true) {
m_first(true),
m_was_unknown(false) {
m_params.updt_params(p);
if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {
m_params.m_relevancy_lvl = 0;
@ -173,6 +174,7 @@ namespace opt {
else {
r = m_context.check(num_assumptions, assumptions);
}
r = adjust_result(r);
m_first = false;
if (dump_benchmarks()) {
w.stop();
@ -242,6 +244,7 @@ namespace opt {
TRACE("opt", tout << ge << "\n";);
assert_expr(ge);
lbool is_sat = m_context.check(0, 0);
is_sat = adjust_result(is_sat);
if (is_sat == l_true) {
set_model(i);
}
@ -261,6 +264,13 @@ namespace opt {
}
lbool opt_solver::adjust_result(lbool r) {
if (r == l_undef && m_context.last_failure() == smt::QUANTIFIERS) {
r = l_true;
m_was_unknown = true;
}
return r;
}
void opt_solver::get_unsat_core(ptr_vector<expr> & r) {
unsigned sz = m_context.get_unsat_core_size();

4
src/opt/opt_solver.h
View file

@ -82,6 +82,7 @@ namespace opt {
static unsigned m_dump_count;
statistics m_stats;
bool m_first;
bool m_was_unknown;
public:
opt_solver(ast_manager & m, params_ref const & p, filter_model_converter& fm);
virtual ~opt_solver();
@ -117,6 +118,8 @@ namespace opt {
return m_valid_objectives[obj_index];
}
bool was_unknown() const { return m_was_unknown; }
vector<inf_eps> const& get_objective_values();
expr_ref mk_ge(unsigned obj_index, inf_eps const& val);
@ -136,6 +139,7 @@ namespace opt {
private:
lbool decrement_value(unsigned i, inf_eps& val);
void set_model(unsigned i);
lbool adjust_result(lbool r);
};
}