mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api
This commit is contained in:
commit
c3263e4731
|
@ -323,6 +323,9 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
|
|||
|
||||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
|
||||
result_pr = 0;
|
||||
TRACE("bit_blaster", tout << f->get_name() << " ";
|
||||
for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m()) << " ";
|
||||
tout << "\n";);
|
||||
if (num == 0 && f->get_family_id() == null_family_id && butil().is_bv_sort(f->get_range())) {
|
||||
mk_const(f, result);
|
||||
return BR_DONE;
|
||||
|
|
|
@ -828,6 +828,12 @@ void bit_blaster_tpl<Cfg>::mk_eq(unsigned sz, expr * const * a_bits, expr * cons
|
|||
|
||||
template<typename Cfg>
|
||||
void bit_blaster_tpl<Cfg>::mk_rotate_left(unsigned sz, expr * const * a_bits, unsigned n, expr_ref_vector & out_bits) {
|
||||
TRACE("bit_blaster", tout << n << ": " << sz << " ";
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
tout << mk_pp(a_bits[i], m()) << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
);
|
||||
n = n % sz;
|
||||
for (unsigned i = sz - n; i < sz; i++)
|
||||
out_bits.push_back(a_bits[i]);
|
||||
|
@ -974,7 +980,7 @@ void bit_blaster_tpl<Cfg>::mk_ashr(unsigned sz, expr * const * a_bits, expr * co
|
|||
mk_ite(eqs.get(i - j), a_bits[sz - j - 1], out, new_out);
|
||||
out = new_out;
|
||||
}
|
||||
TRACE("bit_blaster_tpl<Cfg>", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";);
|
||||
TRACE("bit_blaster", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";);
|
||||
out_bits.set(sz - i - 1, out);
|
||||
}
|
||||
}
|
||||
|
@ -1004,7 +1010,7 @@ void bit_blaster_tpl<Cfg>::mk_ext_rotate_left_right(unsigned sz, expr * const *
|
|||
out = a_bits[i];
|
||||
for (unsigned j = 1; j < sz; j++) {
|
||||
expr_ref new_out(m());
|
||||
unsigned src = (Left ? (i - j) : (i + j)) % sz;
|
||||
unsigned src = (Left ? (sz + i - j) : (i + j)) % sz;
|
||||
mk_ite(eqs.get(j), a_bits[src], out, new_out);
|
||||
out = new_out;
|
||||
}
|
||||
|
|
|
@ -21,6 +21,7 @@ Notes:
|
|||
#include"poly_rewriter_def.h"
|
||||
#include"ast_smt2_pp.h"
|
||||
|
||||
|
||||
mk_extract_proc::mk_extract_proc(bv_util & u):
|
||||
m_util(u),
|
||||
m_high(0),
|
||||
|
|
|
@ -191,8 +191,10 @@ expr * datatype_factory::get_fresh_value(sort * s) {
|
|||
// Approach 2)
|
||||
// For recursive datatypes.
|
||||
// search for constructor...
|
||||
unsigned num_iterations = 0;
|
||||
if (m_util.is_recursive(s)) {
|
||||
while(true) {
|
||||
++num_iterations;
|
||||
TRACE("datatype_factory", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
|
||||
ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(s);
|
||||
ptr_vector<func_decl>::const_iterator it = constructors->begin();
|
||||
|
@ -212,7 +214,13 @@ expr * datatype_factory::get_fresh_value(sort * s) {
|
|||
<< found_sibling << "\n";);
|
||||
if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) {
|
||||
found_sibling = true;
|
||||
expr * maybe_new_arg = get_almost_fresh_value(s_arg);
|
||||
expr * maybe_new_arg = 0;
|
||||
if (num_iterations <= 1) {
|
||||
maybe_new_arg = get_almost_fresh_value(s_arg);
|
||||
}
|
||||
else {
|
||||
maybe_new_arg = get_fresh_value(s_arg);
|
||||
}
|
||||
if (!maybe_new_arg) {
|
||||
TRACE("datatype_factory",
|
||||
tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";);
|
||||
|
@ -231,6 +239,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
|
|||
if (found_sibling) {
|
||||
expr_ref new_value(m_manager);
|
||||
new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
|
||||
TRACE("datatype_factory", tout << "potential new value: " << mk_pp(new_value, m_manager) << "\n";);
|
||||
m_last_fresh_value.insert(s, new_value);
|
||||
if (!set->contains(new_value)) {
|
||||
register_value(new_value);
|
||||
|
|
Loading…
Reference in a new issue