mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 06:43:40 +00:00
Code Activity

fix #3785

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-06 12:56:52 -07:00
parent 077a2cf6f7
commit 07413cc928
3 changed files with 21 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ast/rewriter/rewriter_def.h
View file

@ -38,17 +38,10 @@ void rewriter_tpl<Config>::process_var(var * v) {
unsigned idx = v->get_idx(); unsigned idx = v->get_idx();
if (ProofGen) { if (ProofGen) {
result_pr_stack().push_back(nullptr); // implicit reflexivity result_pr_stack().push_back(nullptr); // implicit reflexivity
SASSERT(
true || // disabled for now
idx >= m_bindings.size() ||
!m_bindings[m_bindings.size() - idx - 1] ||
v == m_bindings[m_bindings.size() - idx - 1]);
} }
unsigned index = 0; unsigned index = 0;
expr * r; expr * r;
if (!ProofGen && idx < m_bindings.size() && if (idx < m_bindings.size() && (index = m_bindings.size() - idx - 1, r = m_bindings[index])) {
(index = m_bindings.size() - idx - 1, r = m_bindings[index])) {
CTRACE("rewriter", v->get_sort() != m().get_sort(r), CTRACE("rewriter", v->get_sort() != m().get_sort(r),
tout << expr_ref(v, m()) << ":" << sort_ref(v->get_sort(), m()) << " != " << expr_ref(r, m()) << ":" << sort_ref(m().get_sort(r), m()); tout << expr_ref(v, m()) << ":" << sort_ref(v->get_sort(), m()) << " != " << expr_ref(r, m()) << ":" << sort_ref(m().get_sort(r), m());
tout << "index " << index << " bindings " << m_bindings.size() << "\n"; tout << "index " << index << " bindings " << m_bindings.size() << "\n";
@ -60,9 +53,8 @@ void rewriter_tpl<Config>::process_var(var * v) {
expr* c = get_cached(r, shift_amount); expr* c = get_cached(r, shift_amount);
if (c) { if (c) {
result_stack().push_back(c); result_stack().push_back(c);
set_new_child_flag(v);
return;
} }
else {
expr_ref tmp(m()); expr_ref tmp(m());
m_shifter(r, shift_amount, tmp); m_shifter(r, shift_amount, tmp);
result_stack().push_back(tmp); result_stack().push_back(tmp);
@ -70,15 +62,17 @@ void rewriter_tpl<Config>::process_var(var * v) {
display_bindings(tout);); display_bindings(tout););
cache_shifted_result(r, shift_amount, tmp); cache_shifted_result(r, shift_amount, tmp);
} }
}
else { else {
result_stack().push_back(r); result_stack().push_back(r);
TRACE("rewriter", tout << idx << " " << mk_ismt2_pp(r, m()) << "\n";); TRACE("rewriter", tout << idx << " " << mk_ismt2_pp(r, m()) << "\n";);
} }
set_new_child_flag(v); set_new_child_flag(v);
return;
} }
else {
result_stack().push_back(v); result_stack().push_back(v);
} }
}
template<typename Config> template<typename Config>
template<bool ProofGen> template<bool ProofGen>

1
src/muz/base/dl_rule.cpp
View file

@ -570,6 +570,7 @@ namespace datalog {
default: fml = m.mk_implies(m.mk_and(body.size(), body.c_ptr()), fml); break; default: fml = m.mk_implies(m.mk_and(body.size(), body.c_ptr()), fml); break;
} }
m_free_vars.reset();
m_free_vars(fml); m_free_vars(fml);
if (m_free_vars.empty()) { if (m_free_vars.empty()) {
return; return;

13
src/muz/transforms/dl_mk_bit_blast.cpp
View file

@ -240,7 +240,7 @@ namespace datalog {
m_context.get_rule_manager().to_formula(*r2.get(), fml1); m_context.get_rule_manager().to_formula(*r2.get(), fml1);
m_blaster(fml1, fml2, pr); m_blaster(fml1, fml2, pr);
m_rewriter(fml2, fml3); m_rewriter(fml2, fml3);
TRACE("dl", tout << mk_pp(fml, m) << " -> " << mk_pp(fml2, m) << " -> " << mk_pp(fml3, m) << "\n";); TRACE("dl", tout << fml << "\n-> " << fml1 << "\n-> " << fml2 << "\n-> " << fml3 << "\n";);
if (fml3 != fml) { if (fml3 != fml) {
fml = fml3; fml = fml3;
return true; return true;
@ -268,6 +268,8 @@ namespace datalog {
if (!m_context.xform_bit_blast()) { if (!m_context.xform_bit_blast()) {
return nullptr; return nullptr;
} }
if (m.proofs_enabled())
return nullptr;
rule_manager& rm = m_context.get_rule_manager(); rule_manager& rm = m_context.get_rule_manager();
unsigned sz = source.get_num_rules(); unsigned sz = source.get_num_rules();
expr_ref fml(m); expr_ref fml(m);
@ -277,7 +279,9 @@ namespace datalog {
for (unsigned i = 0; !m_context.canceled() && i < sz; ++i) { for (unsigned i = 0; !m_context.canceled() && i < sz; ++i) {
rule * r = source.get_rule(i); rule * r = source.get_rule(i);
rm.to_formula(*r, fml); rm.to_formula(*r, fml);
TRACE("dl", tout << fml << "\n";);
if (blast(r, fml)) { if (blast(r, fml)) {
TRACE("dl", tout << "blasted: " << fml << "\n";);
proof_ref pr(m); proof_ref pr(m);
if (r->get_proof()) { if (r->get_proof()) {
scoped_proof _sc(m); scoped_proof _sc(m);
@ -295,10 +299,9 @@ namespace datalog {
// copy output predicates without any rule (bit-blasting not really needed) // copy output predicates without any rule (bit-blasting not really needed)
const func_decl_set& decls = source.get_output_predicates(); const func_decl_set& decls = source.get_output_predicates();
for (func_decl_set::iterator I = decls.begin(), E = decls.end(); I != E; ++I) { for (func_decl* p : decls)
if (!source.contains(*I)) if (!source.contains(p))
result->set_output_predicate(*I); result->set_output_predicate(p);
}
if (m_context.get_model_converter()) { if (m_context.get_model_converter()) {
generic_model_converter* fmc = alloc(generic_model_converter, m, "dl_mk_bit_blast"); generic_model_converter* fmc = alloc(generic_model_converter, m, "dl_mk_bit_blast");