mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-06-03 11:48:21 -07:00
parent bd064bf5d0 56bfc06c4f
commit aa0d921240
4 changed files with 139 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_ast.cpp
View file

@ -1070,6 +1070,10 @@ extern "C" {
case OP_BV2INT: return Z3_OP_BV2INT;
case OP_CARRY: return Z3_OP_CARRY;
case OP_XOR3: return Z3_OP_XOR3;
case OP_BSMUL_NO_OVFL:
case OP_BUMUL_NO_OVFL:
case OP_BSMUL_NO_UDFL:
return Z3_OP_UNINTERPRETED;
default:
UNREACHABLE();
return Z3_OP_UNINTERPRETED;

133
src/api/api_bv.cpp
View file

@ -121,10 +121,20 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
unsigned sz = Z3_get_bv_sort_size(c, s);
rational max_bound = power(rational(2), sz);
Z3_ast bound = Z3_mk_numeral(c, max_bound.to_string().c_str(), int_s);
Z3_ast pred = Z3_mk_bvslt(c, n, Z3_mk_int(c, 0, s));
Z3_inc_ref(c, bound);
Z3_ast zero = Z3_mk_int(c, 0, s);
Z3_inc_ref(c, zero);
Z3_ast pred = Z3_mk_bvslt(c, n, zero);
Z3_inc_ref(c, pred);
// if n <_sigend 0 then r - s^sz else r
Z3_ast args[2] = { r, bound };
Z3_ast res = Z3_mk_ite(c, pred, Z3_mk_sub(c, 2, args), r);
Z3_ast sub = Z3_mk_sub(c, 2, args);
Z3_inc_ref(c, sub);
Z3_ast res = Z3_mk_ite(c, pred, sub, r);
Z3_dec_ref(c, bound);
Z3_dec_ref(c, pred);
Z3_dec_ref(c, sub);
Z3_dec_ref(c, zero);
RETURN_Z3(res);
}
else {
@ -156,7 +166,14 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return Z3_mk_bvshl(c, Z3_mk_int64(c, 1, s), Z3_mk_int64(c, sz - 1, s));
Z3_ast x = Z3_mk_int64(c, 1, s);
Z3_inc_ref(c, x);
Z3_ast y = Z3_mk_int64(c, sz - 1, s);
Z3_inc_ref(c, y);
Z3_ast result = Z3_mk_bvshl(c, x, y);
Z3_dec_ref(c, x);
Z3_dec_ref(c, y);
return result;
Z3_CATCH_RETURN(0);
}
@ -177,17 +194,40 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
RESET_ERROR_CODE();
if (is_signed) {
Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1));
Z3_inc_ref(c, zero);
Z3_ast r = Z3_mk_bvadd(c, t1, t2);
Z3_ast args[2] = { Z3_mk_bvslt(c, zero, t1), Z3_mk_bvslt(c, zero, t2) };
Z3_inc_ref(c, r);
Z3_ast l1 = Z3_mk_bvslt(c, zero, t1);
Z3_inc_ref(c, l1);
Z3_ast l2 = Z3_mk_bvslt(c, zero, t2);
Z3_inc_ref(c, l2);
Z3_ast args[2] = { l1, l2 };
Z3_ast args_pos = Z3_mk_and(c, 2, args);
return Z3_mk_implies(c, args_pos, Z3_mk_bvslt(c, zero, r));
Z3_inc_ref(c, args_pos);
Z3_ast result = Z3_mk_implies(c, args_pos, Z3_mk_bvslt(c, zero, r));
Z3_dec_ref(c, r);
Z3_dec_ref(c, l1);
Z3_dec_ref(c, l2);
Z3_dec_ref(c, args_pos);
Z3_dec_ref(c, zero);
return result;
}
else {
unsigned sz = Z3_get_bv_sort_size(c, Z3_get_sort(c, t1));
t1 = Z3_mk_zero_ext(c, 1, t1);
Z3_inc_ref(c, t1);
t2 = Z3_mk_zero_ext(c, 1, t2);
Z3_inc_ref(c, t2);
Z3_ast r = Z3_mk_bvadd(c, t1, t2);
return Z3_mk_eq(c, Z3_mk_extract(c, sz, sz, r), Z3_mk_int(c, 0, Z3_mk_bv_sort(c, 1)));
Z3_inc_ref(c, r);
Z3_ast ex = Z3_mk_extract(c, sz, sz, r);
Z3_inc_ref(c, ex);
Z3_ast result = Z3_mk_eq(c, ex, Z3_mk_int(c, 0, Z3_mk_bv_sort(c, 1)));
Z3_dec_ref(c, t1);
Z3_dec_ref(c, t2);
Z3_dec_ref(c, ex);
Z3_dec_ref(c, r);
return result;
}
Z3_CATCH_RETURN(0);
}
@ -197,10 +237,26 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_TRY;
RESET_ERROR_CODE();
Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1));
Z3_inc_ref(c, zero);
Z3_ast r = Z3_mk_bvadd(c, t1, t2);
Z3_ast args[2] = { Z3_mk_bvslt(c, t1, zero), Z3_mk_bvslt(c, t2, zero) };
Z3_inc_ref(c, r);
Z3_ast l1 = Z3_mk_bvslt(c, t1, zero);
Z3_inc_ref(c, l1);
Z3_ast l2 = Z3_mk_bvslt(c, t2, zero);
Z3_inc_ref(c, l2);
Z3_ast args[2] = { l1, l2 };
Z3_ast args_neg = Z3_mk_and(c, 2, args);
return Z3_mk_implies(c, args_neg, Z3_mk_bvslt(c, r, zero));
Z3_inc_ref(c, args_neg);
Z3_ast lt = Z3_mk_bvslt(c, r, zero);
Z3_inc_ref(c, lt);
Z3_ast result = Z3_mk_implies(c, args_neg, lt);
Z3_dec_ref(c, lt);
Z3_dec_ref(c, l1);
Z3_dec_ref(c, l2);
Z3_dec_ref(c, r);
Z3_dec_ref(c, args_neg);
Z3_dec_ref(c, zero);
return result;
Z3_CATCH_RETURN(0);
}
@ -208,12 +264,28 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) {
Z3_TRY;
RESET_ERROR_CODE();
Z3_sort s = Z3_get_sort(c, t2);
Z3_ast minus_t2 = Z3_mk_bvneg(c, t2);
Z3_inc_ref(c, minus_t2);
Z3_sort s = Z3_get_sort(c, t2);
Z3_ast min = Z3_mk_bvsmin(c, s);
return Z3_mk_ite(c, Z3_mk_eq(c, t2, min),
Z3_mk_bvslt(c, t1, Z3_mk_int(c, 0, s)),
Z3_mk_bvadd_no_overflow(c, t1, minus_t2, true));
Z3_inc_ref(c, min);
Z3_ast x = Z3_mk_eq(c, t2, min);
Z3_inc_ref(c, x);
Z3_ast zero = Z3_mk_int(c, 0, s);
Z3_inc_ref(c, zero);
Z3_ast y = Z3_mk_bvslt(c, t1, zero);
Z3_inc_ref(c, y);
Z3_ast z = Z3_mk_bvadd_no_overflow(c, t1, minus_t2, true);
Z3_inc_ref(c, z);
Z3_ast result = Z3_mk_ite(c, x, y, z);
mk_c(c)->save_ast_trail(to_app(result));
Z3_dec_ref(c, minus_t2);
Z3_dec_ref(c, min);
Z3_dec_ref(c, x);
Z3_dec_ref(c, y);
Z3_dec_ref(c, z);
Z3_dec_ref(c, zero);
return result;
Z3_CATCH_RETURN(0);
}
@ -222,10 +294,19 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
RESET_ERROR_CODE();
if (is_signed) {
Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1));
if (Z3_get_error_code(c) != Z3_OK) return 0;
Z3_inc_ref(c, zero);
Z3_ast minus_t2 = Z3_mk_bvneg(c, t2);
if (Z3_get_error_code(c) != Z3_OK) return 0;
return Z3_mk_implies(c, Z3_mk_bvslt(c, zero, t2), Z3_mk_bvadd_no_underflow(c, t1, minus_t2));
Z3_inc_ref(c, minus_t2);
Z3_ast x = Z3_mk_bvslt(c, zero, t2);
Z3_inc_ref(c, x);
Z3_ast y = Z3_mk_bvadd_no_underflow(c, t1, minus_t2);
Z3_inc_ref(c, y);
Z3_ast result = Z3_mk_implies(c, x, y);
Z3_dec_ref(c, zero);
Z3_dec_ref(c, minus_t2);
Z3_dec_ref(c, x);
Z3_dec_ref(c, y);
return result;
}
else {
return Z3_mk_bvule(c, t2, t1);
@ -267,12 +348,24 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
Z3_TRY;
RESET_ERROR_CODE();
Z3_sort s = Z3_get_sort(c, t1);
if (Z3_get_error_code(c) != Z3_OK) return 0;
Z3_ast min = Z3_mk_bvmsb(c, s);
if (Z3_get_error_code(c) != Z3_OK) return 0;
Z3_ast args[2] = { Z3_mk_eq(c, t1, min),
Z3_mk_eq(c, t2, Z3_mk_int(c, -1, s)) };
return Z3_mk_not(c, Z3_mk_and(c, 2, args));
Z3_inc_ref(c, min);
Z3_ast x = Z3_mk_eq(c, t1, min);
Z3_inc_ref(c, x);
Z3_ast y = Z3_mk_int(c, -1, s);
Z3_inc_ref(c, y);
Z3_ast z = Z3_mk_eq(c, t2, y);
Z3_inc_ref(c, z);
Z3_ast args[2] = { x, z };
Z3_ast u = Z3_mk_and(c, 2, args);
Z3_inc_ref(c, u);
Z3_ast result = Z3_mk_not(c, u);
Z3_dec_ref(c, min);
Z3_dec_ref(c, x);
Z3_dec_ref(c, y);
Z3_dec_ref(c, z);
Z3_dec_ref(c, u);
return result;
Z3_CATCH_RETURN(0);
}

29
src/shell/smtlib_frontend.cpp
View file

@ -54,13 +54,19 @@ static void display_statistics() {
}
static void on_timeout() {
display_statistics();
exit(0);
#pragma omp critical (g_display_stats)
{
display_statistics();
exit(0);
}
}
static void on_ctrl_c(int) {
signal (SIGINT, SIG_DFL);
display_statistics();
#pragma omp critical (g_display_stats)
{
display_statistics();
}
raise(SIGINT);
}
@ -83,9 +89,12 @@ unsigned read_smtlib_file(char const * benchmark_file) {
}
}
display_statistics();
register_on_timeout_proc(0);
g_solver = 0;
#pragma omp critical (g_display_stats)
{
display_statistics();
register_on_timeout_proc(0);
g_solver = 0;
}
return solver.get_error_code();
}
@ -118,8 +127,12 @@ unsigned read_smtlib2_commands(char const * file_name) {
result = parse_smt2_commands(ctx, std::cin, true);
}
display_statistics();
g_cmd_context = 0;
#pragma omp critical (g_display_stats)
{
display_statistics();
g_cmd_context = 0;
}
return result ? 0 : 1;
}

2
src/smt/theory_arith_core.h
View file

@ -408,7 +408,7 @@ namespace smt {
mk_axiom(eqz, upper);
rational k;
if (m_params.m_arith_enum_const_mod && m_util.is_numeral(divisor, k) &&
k.is_pos() && k < rational(512)) {
k.is_pos() && k < rational(8)) {
rational j(0);
#if 1
literal_buffer lits;