mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-15 18:36:16 +00:00
Code Activity

fix memory leaks from cancellations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-01-15 20:09:27 -08:00
parent 24eae3f6e0
commit c4c9de0838
4 changed files with 39 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

47
src/muz/pdr/pdr_context.cpp
View file

@ -575,7 +575,7 @@ namespace pdr {
// Predicates that are variable representatives. Other predicates at // Predicates that are variable representatives. Other predicates at
// positions the variables occur are made equivalent with these. // positions the variables occur are made equivalent with these.
expr_ref_vector conj(m); expr_ref_vector conj(m);
app_ref_vector& var_reprs = *(alloc(app_ref_vector, m)); app_ref_vector var_reprs(m);
ptr_vector<app> aux_vars; ptr_vector<app> aux_vars;
unsigned ut_size = rule.get_uninterpreted_tail_size(); unsigned ut_size = rule.get_uninterpreted_tail_size();
@ -584,8 +584,9 @@ namespace pdr {
init_atom(pts, rule.get_head(), var_reprs, conj, UINT_MAX); init_atom(pts, rule.get_head(), var_reprs, conj, UINT_MAX);
for (unsigned i = 0; i < ut_size; ++i) { for (unsigned i = 0; i < ut_size; ++i) {
if (rule.is_neg_tail(i)) { if (rule.is_neg_tail(i)) {
dealloc(&var_reprs); char const* msg = "PDR does not supported negated predicates in rule tails";
throw default_exception("PDR does not support negated predicates in rule tails"); IF_VERBOSE(0, verbose_stream() << msg << "\n";);
throw default_exception(msg);
} }
init_atom(pts, rule.get_tail(i), var_reprs, conj, i); init_atom(pts, rule.get_tail(i), var_reprs, conj, i);
} }
@ -600,14 +601,14 @@ namespace pdr {
flatten_and(tail); flatten_and(tail);
for (unsigned i = 0; i < tail.size(); ++i) { for (unsigned i = 0; i < tail.size(); ++i) {
expr_ref tmp(m); expr_ref tmp(m);
var_subst(m, false)(tail[i].get(), var_reprs.size(), (expr*const*)var_reprs.c_ptr(), tmp); var_subst vs(m, false);
vs(tail[i].get(), var_reprs.size(), (expr*const*)var_reprs.c_ptr(), tmp);
conj.push_back(tmp); conj.push_back(tmp);
TRACE("pdr", tout << mk_pp(tail[i].get(), m) << "\n" << mk_pp(tmp, m) << "\n";); TRACE("pdr", tout << mk_pp(tail[i].get(), m) << "\n" << mk_pp(tmp, m) << "\n";);
if (!is_ground(tmp)) { if (!is_ground(tmp)) {
std::stringstream msg; std::stringstream msg;
msg << "PDR cannot solve non-ground tails: " << tmp; msg << "PDR cannot solve non-ground tails: " << tmp;
IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";); IF_VERBOSE(0, verbose_stream() << msg.str() << "\n";);
dealloc(&var_reprs);
throw default_exception(msg.str()); throw default_exception(msg.str());
} }
} }
@ -631,7 +632,7 @@ namespace pdr {
m_rule2transition.insert(&rule, fml.get()); m_rule2transition.insert(&rule, fml.get());
rules.push_back(&rule); rules.push_back(&rule);
} }
m_rule2inst.insert(&rule, &var_reprs); m_rule2inst.insert(&rule, alloc(app_ref_vector, var_reprs));
m_rule2vars.insert(&rule, aux_vars); m_rule2vars.insert(&rule, aux_vars);
TRACE("pdr", TRACE("pdr",
tout << rule.get_decl()->get_name() << "\n"; tout << rule.get_decl()->get_name() << "\n";
@ -1468,13 +1469,20 @@ namespace pdr {
reset(); reset();
} }
void context::reset() { void context::reset(decl2rel& rels) {
TRACE("pdr", tout << "\n";); decl2rel::iterator it = rels.begin(), end = rels.end();
decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
for (; it != end; ++it) { for (; it != end; ++it) {
dealloc(it->m_value); dealloc(it->m_value);
} }
m_rels.reset(); rels.reset();
}
void context::reset(bool full) {
TRACE("pdr", tout << "reset\n";);
reset(m_rels);
if (full) {
reset(m_rels_tmp);
}
m_search.reset(); m_search.reset();
m_query = 0; m_query = 0;
m_last_result = l_undef; m_last_result = l_undef;
@ -1496,6 +1504,7 @@ namespace pdr {
e->get_data().m_value->add_rule(pred_rules[i]); e->get_data().m_value->add_rule(pred_rules[i]);
} }
} }
TRACE("pdr", tout << "adding rules\n";);
datalog::rule_set::iterator rit = rules.begin(), rend = rules.end(); datalog::rule_set::iterator rit = rules.begin(), rend = rules.end();
for (; rit != rend; ++rit) { for (; rit != rend; ++rit) {
datalog::rule* r = *rit; datalog::rule* r = *rit;
@ -1510,6 +1519,7 @@ namespace pdr {
} }
} }
// Initialize use list dependencies // Initialize use list dependencies
TRACE("pdr", tout << "initialize use list dependencies\n";);
decl2rel::iterator it = rels.begin(), end = rels.end(); decl2rel::iterator it = rels.begin(), end = rels.end();
for (; it != end; ++it) { for (; it != end; ++it) {
func_decl* pred = it->m_key; func_decl* pred = it->m_key;
@ -1523,9 +1533,11 @@ namespace pdr {
} }
} }
TRACE("pdr", tout << "initialize predicate transformers\n";);
// Initialize the predicate transformers. // Initialize the predicate transformers.
it = rels.begin(), end = rels.end(); it = rels.begin(), end = rels.end();
for (; it != end; ++it) { for (; it != end; ++it) {
SASSERT(it->m_value);
pred_transformer& rel = *it->m_value; pred_transformer& rel = *it->m_value;
rel.initialize(rels); rel.initialize(rels);
TRACE("pdr", rel.display(tout); ); TRACE("pdr", rel.display(tout); );
@ -1533,21 +1545,24 @@ namespace pdr {
} }
void context::update_rules(datalog::rule_set& rules) { void context::update_rules(datalog::rule_set& rules) {
decl2rel rels; TRACE("pdr", tout << "update rules\n";);
reset(m_rels_tmp);
init_core_generalizers(rules); init_core_generalizers(rules);
init_rules(rules, rels); init_rules(rules, m_rels_tmp);
decl2rel::iterator it = rels.begin(), end = rels.end(); decl2rel::iterator it = m_rels_tmp.begin(), end = m_rels_tmp.end();
for (; it != end; ++it) { for (; it != end; ++it) {
pred_transformer* pt = 0; pred_transformer* pt = 0;
if (m_rels.find(it->m_key, pt)) { if (m_rels.find(it->m_key, pt)) {
it->m_value->inherit_properties(*pt); it->m_value->inherit_properties(*pt);
} }
} }
reset(); reset(false);
it = rels.begin(), end = rels.end(); it = m_rels_tmp.begin(), end = m_rels_tmp.end();
for (; it != end; ++it) { for (; it != end; ++it) {
m_rels.insert(it->m_key, it->m_value); m_rels.insert(it->m_key, it->m_value);
} }
m_rels_tmp.reset();
TRACE("pdr", tout << "done update rules\n";);
} }
unsigned context::get_num_levels(func_decl* p) { unsigned context::get_num_levels(func_decl* p) {
@ -1875,6 +1890,7 @@ namespace pdr {
} }
lbool context::solve() { lbool context::solve() {
TRACE("pdr", tout << "solve\n";);
m_last_result = l_undef; m_last_result = l_undef;
try { try {
solve_impl(); solve_impl();
@ -2090,6 +2106,7 @@ namespace pdr {
} }
case l_undef: { case l_undef: {
TRACE("pdr", tout << "unknown state: " << mk_pp(m_pm.mk_and(cube), m) << "\n";); TRACE("pdr", tout << "unknown state: " << mk_pp(m_pm.mk_and(cube), m) << "\n";);
IF_VERBOSE(1, verbose_stream() << "unknown state\n";);
throw unknown_exception(); throw unknown_exception();
} }
} }

6
src/muz/pdr/pdr_context.h
View file

@ -328,6 +328,7 @@ namespace pdr {
datalog::context* m_context; datalog::context* m_context;
manager m_pm; manager m_pm;
decl2rel m_rels; // Map from relation predicate to fp-operator. decl2rel m_rels; // Map from relation predicate to fp-operator.
decl2rel m_rels_tmp;
func_decl_ref m_query_pred; func_decl_ref m_query_pred;
pred_transformer* m_query; pred_transformer* m_query;
mutable model_search m_search; mutable model_search m_search;
@ -370,6 +371,8 @@ namespace pdr {
void reset_core_generalizers(); void reset_core_generalizers();
void reset(decl2rel& rels);
void validate(); void validate();
void validate_proof(); void validate_proof();
void validate_search(); void validate_search();
@ -410,8 +413,7 @@ namespace pdr {
lbool solve(); lbool solve();
void reset(bool full = true);
void reset();
void set_query(func_decl* q) { m_query_pred = q; } void set_query(func_decl* q) { m_query_pred = q; }

4
src/muz/pdr/pdr_dl_interface.cpp
View file

@ -19,12 +19,8 @@ Revision History:
#include "dl_context.h" #include "dl_context.h"
#include "dl_mk_coi_filter.h" #include "dl_mk_coi_filter.h"
#include "dl_mk_interp_tail_simplifier.h"
#include "dl_mk_subsumption_checker.h"
#include "dl_mk_rule_inliner.h"
#include "dl_rule.h" #include "dl_rule.h"
#include "dl_rule_transformer.h" #include "dl_rule_transformer.h"
#include "smt2parser.h"
#include "pdr_context.h" #include "pdr_context.h"
#include "pdr_dl_interface.h" #include "pdr_dl_interface.h"
#include "dl_rule_set.h" #include "dl_rule_set.h"

4
src/smt/asserted_formulas.cpp
View file

@ -184,13 +184,13 @@ void asserted_formulas::get_assertions(ptr_vector<expr> & result) {
} }
void asserted_formulas::push_scope() { void asserted_formulas::push_scope() {
SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size()); SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size() || m_manager.canceled());
TRACE("asserted_formulas_scopes", tout << "push:\n"; display(tout);); TRACE("asserted_formulas_scopes", tout << "push:\n"; display(tout););
m_scopes.push_back(scope()); m_scopes.push_back(scope());
m_macro_manager.push_scope(); m_macro_manager.push_scope();
scope & s = m_scopes.back(); scope & s = m_scopes.back();
s.m_asserted_formulas_lim = m_asserted_formulas.size(); s.m_asserted_formulas_lim = m_asserted_formulas.size();
SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead); SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead || m_manager.canceled());
s.m_inconsistent_old = m_inconsistent; s.m_inconsistent_old = m_inconsistent;
m_defined_names.push(); m_defined_names.push();
m_bv_sharing.push_scope(); m_bv_sharing.push_scope();