mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2015-10-27 18:11:35 -07:00
commit 47cb1058b2
68 changed files with 1281 additions and 882 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/asserted_formulas.cpp
View file

@ -593,7 +593,7 @@ void asserted_formulas::propagate_values() {
bool found = false;
// Separate the formulas in two sets: C and R
// C is a set which contains formulas of the form
// { x = n }, where x is a variable and n a numberal.
// { x = n }, where x is a variable and n a numeral.
// R contains the rest.
//
// - new_exprs1 is the set C
@ -613,15 +613,18 @@ void asserted_formulas::propagate_values() {
expr * lhs = to_app(n)->get_arg(0);
expr * rhs = to_app(n)->get_arg(1);
if (m_manager.is_value(lhs) || m_manager.is_value(rhs)) {
if (m_manager.is_value(lhs))
if (m_manager.is_value(lhs)) {
std::swap(lhs, rhs);
n = m_manager.mk_eq(lhs, rhs);
pr = m_manager.mk_symmetry(pr);
}
if (!m_manager.is_value(lhs) && !m_simplifier.is_cached(lhs)) {
if (i >= m_asserted_qhead) {
new_exprs1.push_back(n);
if (m_manager.proofs_enabled())
new_prs1.push_back(pr);
}
TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\n";);
TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\nproof: " << mk_pp(pr, m_manager) << "\n";);
m_simplifier.cache_result(lhs, rhs, pr);
found = true;
continue;

2
src/smt/params/dyn_ack_params.cpp
View file

@ -27,4 +27,4 @@ void dyn_ack_params::updt_params(params_ref const & _p) {
m_dack_threshold = p.dack_threshold();
m_dack_gc = p.dack_gc();
m_dack_gc_inv_decay = p.dack_gc_inv_decay();
}
}

2
src/smt/params/smt_params.h
View file

@ -66,7 +66,7 @@ enum case_split_strategy {
CS_ACTIVITY_WITH_CACHE, // case split based on activity and cache the activity
CS_RELEVANCY, // case split based on relevancy
CS_RELEVANCY_ACTIVITY, // case split based on relevancy and activity
CS_RELEVANCY_GOAL, // based on relevancy and the current goal
CS_RELEVANCY_GOAL // based on relevancy and the current goal
};
struct smt_params : public preprocessor_params,

2
src/smt/smt_almost_cg_table.cpp
View file

@ -67,7 +67,7 @@ namespace smt {
switch (num_args) {
case 2:
b += arg_hash(n, 1);
__fallthrough;
Z3_fallthrough;
case 1:
c += arg_hash(n, 0);
}

2
src/smt/smt_cg_table.cpp
View file

@ -127,7 +127,7 @@ namespace smt {
switch (i) {
case 2:
b += n->get_arg(1)->get_root()->hash();
__fallthrough;
Z3_fallthrough;
case 1:
c += n->get_arg(0)->get_root()->hash();
}

2
src/smt/smt_setup.h
View file

@ -28,7 +28,7 @@ namespace smt {
enum config_mode {
CFG_BASIC, // install theories based on user options
CFG_LOGIC, // install theories and configure Z3 based on the value of the parameter set-logic.
CFG_AUTO, // install theories based on static features of the input formula
CFG_AUTO // install theories based on static features of the input formula
};
class context;

15
src/smt/theory_arith_aux.h
View file

@ -1535,6 +1535,7 @@ namespace smt {
while (best_efforts < max_efforts && !ctx.get_cancel_flag()) {
theory_var x_j = null_theory_var;
theory_var x_i = null_theory_var;
bool has_bound = false;
max_gain.reset();
min_gain.reset();
++round;
@ -1543,12 +1544,15 @@ namespace smt {
typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) {
if (it->is_dead()) continue;
if (it->is_dead()) continue;
theory_var curr_x_j = it->m_var;
theory_var curr_x_i = null_theory_var;
SASSERT(is_non_base(curr_x_j));
curr_coeff = it->m_coeff;
bool curr_inc = curr_coeff.is_pos() ? max : !max;
bool curr_inc = curr_coeff.is_pos() ? max : !max;
if ((curr_inc && upper(curr_x_j)) || (!curr_inc && lower(curr_x_j))) {
has_bound = true;
}
if ((curr_inc && at_upper(curr_x_j)) || (!curr_inc && at_lower(curr_x_j))) {
// variable cannot be used for max/min.
continue;
@ -1560,8 +1564,9 @@ namespace smt {
SASSERT(!picked_var || safe_gain(curr_min_gain, curr_max_gain));
if (!picked_var) { // && (r.size() > 1 || !safe_gain(curr_min_gain, curr_max_gain))
if (!safe_gain(curr_min_gain, curr_max_gain)) {
TRACE("opt", tout << "no variable picked\n";);
has_bound = true;
best_efforts++;
}
else if (curr_x_i == null_theory_var) {
@ -1598,10 +1603,10 @@ namespace smt {
TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << max_gain << "\n";
tout << "best efforts: " << best_efforts << " has shared: " << has_shared << "\n";);
if (x_j == null_theory_var && x_i == null_theory_var) {
if (!has_bound && x_i == null_theory_var && x_j == null_theory_var) {
has_shared = false;
best_efforts = 0;
result = UNBOUNDED;
result = UNBOUNDED;
break;
}

13
src/smt/theory_diff_logic.h
View file

@ -399,7 +399,6 @@ namespace smt {
};
struct sidl_ext {
// TODO: It doesn't need to be a rational, but a bignum integer.
static const bool m_int_theory = true;
typedef s_integer numeral;
typedef s_integer fin_numeral;
@ -415,13 +414,11 @@ namespace smt {
rdl_ext() : m_epsilon(rational(), true) {}
};
struct srdl_ext {
static const bool m_int_theory = false;
typedef inf_s_integer numeral;
typedef s_integer fin_numeral;
numeral m_epsilon;
srdl_ext() : m_epsilon(s_integer(0),true) {}
};
//
// there is no s_rational class, so
// instead we use multi-precision rationals.
//
struct srdl_ext : public rdl_ext {};
typedef theory_diff_logic<idl_ext> theory_idl;
typedef theory_diff_logic<sidl_ext> theory_fidl;

63
src/smt/theory_fpa.cpp
View file

@ -74,7 +74,9 @@ namespace smt {
}
else {
SASSERT(is_rm(f->get_range()));
result = m_th.wrap(m.mk_const(f));
expr_ref bv(m);
bv = m_th.wrap(m.mk_const(f));
mk_rm(bv, result);
m_rm_const2bv.insert(f, result);
m.inc_ref(f);
m.inc_ref(result);
@ -83,7 +85,7 @@ namespace smt {
void theory_fpa::fpa2bv_converter_wrapped::mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
// TODO: This introduces temporary variables/func_decls that should be filtered in the end.
return fpa2bv_converter::mk_uninterpreted_function(f, num, args, result);
fpa2bv_converter::mk_uninterpreted_function(f, num, args, result);
}
expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_unspecified(func_decl * f, expr * x, expr * y) {
@ -106,7 +108,6 @@ namespace smt {
expr_ref sc(m);
m_th.m_converter.mk_is_zero(res, sc);
m_extra_assertions.push_back(sc);
//m_extra_assertions.push_back(m.mk_eq(m_th.unwrap(wrapped, f->get_range()), a));
return res;
}
@ -130,7 +131,6 @@ namespace smt {
expr_ref sc(m);
m_th.m_converter.mk_is_zero(res, sc);
m_extra_assertions.push_back(sc);
//m_extra_assertions.push_back(m.mk_eq(m_th.unwrap(wrapped, f->get_range()), a));
return res;
}
@ -314,6 +314,7 @@ namespace smt {
expr_ref theory_fpa::convert_atom(expr * e) {
ast_manager & m = get_manager();
TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, get_manager()) << "\n";);
expr_ref res(m);
proof_ref pr(m);
m_rw(e, res);
@ -331,15 +332,31 @@ namespace smt {
proof_ref pr(m);
m_rw(e, e_conv);
if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) {
m_th_rw(e_conv, res);
if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) {
if (!m_fpa_util.is_float(e_conv))
m_th_rw(e_conv, res);
else {
expr_ref bv(m);
bv = wrap(e_conv);
unsigned bv_sz = m_bv_util.get_bv_size(bv);
unsigned ebits = m_fpa_util.get_ebits(m.get_sort(e_conv));
unsigned sbits = m_fpa_util.get_sbits(m.get_sort(e_conv));
SASSERT(bv_sz == ebits + sbits);
m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
m_bv_util.mk_extract(sbits - 2, 0, bv),
res);
}
}
else if (m_fpa_util.is_rm(e)) {
SASSERT(is_sort_of(m.get_sort(e_conv), m_bv_util.get_family_id(), BV_SORT));
SASSERT(m_bv_util.get_bv_size(e_conv) == 3);
m_th_rw(e_conv, res);
SASSERT(is_app_of(e_conv, get_family_id(), OP_FPA_INTERNAL_RM));
expr_ref bv_rm(m);
bv_rm = to_app(e_conv)->get_arg(0);
m_th_rw(bv_rm);
m_converter.mk_rm(bv_rm, res);
}
else if (m_fpa_util.is_float(e)) {
else if (m_fpa_util.is_float(e)) {
SASSERT(is_app_of(e_conv, get_family_id(), OP_FPA_FP));
expr_ref sgn(m), sig(m), exp(m);
m_converter.split_fp(e_conv, sgn, exp, sig);
m_th_rw(sgn);
@ -426,7 +443,7 @@ namespace smt {
sort * srt = m.get_sort(e);
expr_ref res(m);
if (m_fpa_util.is_rm(srt)) {
res = to_app(e)->get_arg(0);
m_converter.mk_rm(to_app(e)->get_arg(0), res);
}
else {
SASSERT(m_fpa_util.is_float(srt));
@ -454,7 +471,6 @@ namespace smt {
TRACE("t_fpa_detail", tout << "cached:" << std::endl;
tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl <<
mk_ismt2_pp(res, m) << std::endl;);
return res;
}
else {
if (m_fpa_util.is_unwrap(e))
@ -464,7 +480,7 @@ namespace smt {
else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e))
res = convert_term(e);
else if (m_arith_util.is_real(e) || m_bv_util.is_bv(e))
res = convert_conversion_term(e);
res = convert_conversion_term(e);
else
UNREACHABLE();
@ -476,7 +492,7 @@ namespace smt {
m.inc_ref(res);
m_trail_stack.push(fpa2bv_conversion_trail_elem(m, m_conversions, e));
}
return res;
}
@ -643,19 +659,17 @@ namespace smt {
expr_ref xc(m), yc(m);
xc = convert(xe);
yc = convert(ye);
TRACE("t_fpa_detail", tout << "xc = " << mk_ismt2_pp(xc, m) << std::endl <<
"yc = " << mk_ismt2_pp(yc, m) << std::endl;);
expr_ref c(m);
if (fu.is_float(xe) && fu.is_float(ye))
if ((fu.is_float(xe) && fu.is_float(ye)) ||
(fu.is_rm(xe) && fu.is_rm(ye)))
m_converter.mk_eq(xc, yc, c);
else if (fu.is_rm(xe) && fu.is_rm(ye))
else
c = m.mk_eq(xc, yc);
else
UNREACHABLE();
m_th_rw(c);
assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c));
@ -671,7 +685,7 @@ namespace smt {
TRACE("t_fpa", tout << "new diseq: " << x << " != " << y << std::endl;);
TRACE("t_fpa_detail", tout << mk_ismt2_pp(get_enode(x)->get_owner(), m) << " != " <<
mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl;);
mk_ismt2_pp(get_enode(y)->get_owner(), m) << std::endl;);
fpa_util & fu = m_fpa_util;
@ -688,14 +702,13 @@ namespace smt {
expr_ref c(m);
if (fu.is_float(xe) && fu.is_float(ye)) {
if ((fu.is_float(xe) && fu.is_float(ye))||
(fu.is_rm(xe) && fu.is_rm(ye))) {
m_converter.mk_eq(xc, yc, c);
c = m.mk_not(c);
}
else if (fu.is_rm(xe) && fu.is_rm(ye))
c = m.mk_not(m.mk_eq(xc, yc));
else
UNREACHABLE();
c = m.mk_not(m.mk_eq(xc, yc));
m_th_rw(c);
assert_cnstr(m.mk_iff(m.mk_not(m.mk_eq(xe, ye)), c));