From cd485f03dd7118a9990013779febb8432f39bf66 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 20 Jun 2013 17:02:15 -0700
Subject: [PATCH 1/4] Add trace msg
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
src/api/z3_replayer.cpp | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp
index 079516145..acdb10bf6 100644
--- a/src/api/z3_replayer.cpp
+++ b/src/api/z3_replayer.cpp
@@ -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");
}
From 185f125f7a3d356192df272bfb2339ad36d3cdf9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 20 Jun 2013 17:48:43 -0700
Subject: [PATCH 2/4] Fix problem reported at
http://stackoverflow.com/questions/17215640/getting-concrete-values-from-a-model-containing-array-ext
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
src/smt/smt_model_finder.cpp | 36 +++++++++++++++++++++++++++++++++++-
1 file changed, 35 insertions(+), 1 deletion(-)
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index f3d0ca3bb..c4a48d9f8 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -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);
From a60b53bfd8dff26011e8bfd7bbca7801bf645dbf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 20 Jun 2013 17:52:20 -0700
Subject: [PATCH 3/4] Fix compilation errors/warnings when using GCC
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
src/ast/rewriter/float_rewriter.cpp | 6 +++---
src/tactic/fpa/fpa2bv_rewriter.h | 2 +-
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp
index 367fa3a4c..0a4c3fc4e 100644
--- a/src/ast/rewriter/float_rewriter.cpp
+++ b/src/ast/rewriter/float_rewriter.cpp
@@ -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 {
diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h
index 24e275c0d..d737683a8 100644
--- a/src/tactic/fpa/fpa2bv_rewriter.h
+++ b/src/tactic/fpa/fpa2bv_rewriter.h
@@ -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();
From 42898f327671aa71e259a2966d78c45432a7b18a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 21 Jun 2013 10:31:11 -0700
Subject: [PATCH 4/4] Fix bug reported by Florian <corzilius@cs.rwth-aachen.de>
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
src/nlsat/nlsat_explain.cpp | 18 ++++++++++++++++--
1 file changed, 16 insertions(+), 2 deletions(-)
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index be60fb052..50466c276 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -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 {