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:
Christoph M. Wintersteiger 2013-06-21 21:16:12 +01:00
parent 0b6250253a 42898f3276
commit 9489c9b08b
5 changed files with 56 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/api/z3_replayer.cpp
View file

@ -26,6 +26,7 @@ Notes:
void register_z3_replayer_cmds(z3_replayer & in);
void throw_invalid_reference() {
TRACE("z3_replayer", tout << "invalid argument reference\n";);
throw z3_replayer_exception("invalid argument reference");
}

6
src/ast/rewriter/float_rewriter.cpp
View file

@ -88,7 +88,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
result = m_util.mk_value(v);
m_util.fm().del(v);
TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
// TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
return BR_DONE;
}
else if (m_util.is_value(args[1], q_mpf)) {
@ -97,7 +97,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
m_util.fm().set(v, ebits, sbits, rm, q_mpf);
result = m_util.mk_value(v);
m_util.fm().del(v);
TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
// TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
return BR_DONE;
}
else
@ -125,7 +125,7 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator());
result = m_util.mk_value(v);
m_util.fm().del(v);
TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
// TRACE("fp_rewriter", tout << "result: " << result << std::endl; );
return BR_DONE;
}
else {

18
src/nlsat/nlsat_explain.cpp
View file

@ -993,8 +993,22 @@ namespace nlsat {
}
return;
}
else if (s == -1 && !is_even) {
atom_sign = -atom_sign;
else {
// We have shown the current factor is a constant MODULO the sign of the leading coefficient (of the equation used to rewrite the factor).
if (!info.m_lc_const) {
// If the leading coefficient is not a constant, we must store this information as an extra assumption.
if (d % 2 == 0 || // d is even
is_even || // rewriting a factor of even degree, sign flip doesn't matter
_a->get_kind() == atom::EQ) { // rewriting an equation, sign flip doesn't matter
info.add_lc_diseq();
}
else {
info.add_lc_ineq();
}
}
if (s == -1 && !is_even) {
atom_sign = -atom_sign;
}
}
}
else {

36
src/smt/smt_model_finder.cpp
View file

@ -94,7 +94,7 @@ namespace smt {
}
obj_map<expr, unsigned> const & get_elems() const { return m_elems; }
void insert(expr * n, unsigned generation) {
if (m_elems.contains(n))
return;
@ -102,6 +102,14 @@ namespace smt {
m_elems.insert(n, generation);
SASSERT(!m_manager.is_model_value(n));
}
void remove(expr * n) {
// We can only remove n if it is in m_elems, AND m_inv was not initialized yet.
SASSERT(m_elems.contains(n));
SASSERT(m_inv.empty());
m_elems.erase(n);
m_manager.dec_ref(n);
}
void display(std::ostream & out) const {
obj_map<expr, unsigned>::iterator it = m_elems.begin();
@ -525,6 +533,30 @@ namespace smt {
}
}
// For each instantiation_set, reemove entries that do not evaluate to values.
void cleanup_instantiation_sets() {
ptr_vector<expr> to_delete;
ptr_vector<node>::const_iterator it = m_nodes.begin();
ptr_vector<node>::const_iterator end = m_nodes.end();
for (; it != end; ++it) {
node * curr = *it;
if (curr->is_root()) {
instantiation_set * s = curr->get_instantiation_set();
to_delete.reset();
obj_map<expr, unsigned> const & elems = s->get_elems();
for (obj_map<expr, unsigned>::iterator it = elems.begin(); it != elems.end(); it++) {
expr * n = it->m_key;
expr * n_val = eval(n, true);
if (!m_manager.is_value(n_val))
to_delete.push_back(n);
}
for (ptr_vector<expr>::iterator it = to_delete.begin(); it != to_delete.end(); it++) {
s->remove(*it);
}
}
}
}
void display_nodes(std::ostream & out) const {
display_key2node(out, m_uvars);
display_A_f_is(out);
@ -545,6 +577,7 @@ namespace smt {
r = 0;
else
r = tmp;
TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n----->\n" << mk_pp(r, m_manager) << "\n";);
m_eval_cache.insert(n, r);
m_eval_cache_range.push_back(r);
return r;
@ -1047,6 +1080,7 @@ namespace smt {
public:
void fix_model(expr_ref_vector & new_constraints) {
cleanup_instantiation_sets();
m_new_constraints = &new_constraints;
func_decl_set partial_funcs;
collect_partial_funcs(partial_funcs);

2
src/tactic/fpa/fpa2bv_rewriter.h
View file

@ -226,7 +226,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
if (t->get_idx() >= m_bindings.size())
return false;
unsigned inx = m_bindings.size() - t->get_idx() - 1;
// unsigned inx = m_bindings.size() - t->get_idx() - 1;
expr_ref new_exp(m());
sort * s = t->get_sort();