mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix leaks reported in #1309
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
44be1501ff
commit
4d1acadabb
|
@ -1311,7 +1311,6 @@ namespace sat {
|
|||
clause_use_list & neg_occs = m_use_list.get(neg_l);
|
||||
unsigned num_pos = pos_occs.size() + num_bin_pos;
|
||||
unsigned num_neg = neg_occs.size() + num_bin_neg;
|
||||
m_elim_counter -= num_pos + num_neg;
|
||||
|
||||
TRACE("resolution", tout << v << " num_pos: " << num_pos << " neg_pos: " << num_neg << "\n";);
|
||||
|
||||
|
@ -1352,8 +1351,6 @@ namespace sat {
|
|||
collect_clauses(pos_l, m_pos_cls);
|
||||
collect_clauses(neg_l, m_neg_cls);
|
||||
|
||||
m_elim_counter -= num_pos * num_neg + before_lits;
|
||||
|
||||
TRACE("resolution_detail", tout << "collecting number of after_clauses\n";);
|
||||
unsigned before_clauses = num_pos + num_neg;
|
||||
unsigned after_clauses = 0;
|
||||
|
@ -1376,7 +1373,7 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";);
|
||||
|
||||
m_elim_counter -= num_pos * num_neg + before_lits;
|
||||
|
||||
// eliminate variable
|
||||
model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
|
||||
|
|
|
@ -315,6 +315,7 @@ namespace smt {
|
|||
m_trail.push_back(node);
|
||||
if (!cut_var_map.contains(baseNode)) {
|
||||
T_cut * varInfo = alloc(T_cut);
|
||||
m_cut_allocs.push_back(varInfo);
|
||||
varInfo->level = slevel;
|
||||
varInfo->vars[node] = 1;
|
||||
cut_var_map.insert(baseNode, std::stack<T_cut*>());
|
||||
|
@ -323,6 +324,7 @@ namespace smt {
|
|||
} else {
|
||||
if (cut_var_map[baseNode].empty()) {
|
||||
T_cut * varInfo = alloc(T_cut);
|
||||
m_cut_allocs.push_back(varInfo);
|
||||
varInfo->level = slevel;
|
||||
varInfo->vars[node] = 1;
|
||||
cut_var_map[baseNode].push(varInfo);
|
||||
|
@ -330,6 +332,7 @@ namespace smt {
|
|||
} else {
|
||||
if (cut_var_map[baseNode].top()->level < slevel) {
|
||||
T_cut * varInfo = alloc(T_cut);
|
||||
m_cut_allocs.push_back(varInfo);
|
||||
varInfo->level = slevel;
|
||||
cut_vars_map_copy(varInfo->vars, cut_var_map[baseNode].top()->vars);
|
||||
varInfo->vars[node] = 1;
|
||||
|
@ -359,6 +362,7 @@ namespace smt {
|
|||
|
||||
if (!cut_var_map.contains(destNode)) {
|
||||
T_cut * varInfo = alloc(T_cut);
|
||||
m_cut_allocs.push_back(varInfo);
|
||||
varInfo->level = slevel;
|
||||
cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars);
|
||||
cut_var_map.insert(destNode, std::stack<T_cut*>());
|
||||
|
@ -367,6 +371,7 @@ namespace smt {
|
|||
} else {
|
||||
if (cut_var_map[destNode].empty() || cut_var_map[destNode].top()->level < slevel) {
|
||||
T_cut * varInfo = alloc(T_cut);
|
||||
m_cut_allocs.push_back(varInfo);
|
||||
varInfo->level = slevel;
|
||||
cut_vars_map_copy(varInfo->vars, cut_var_map[destNode].top()->vars);
|
||||
cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars);
|
||||
|
|
|
@ -18,9 +18,12 @@
|
|||
#define _THEORY_STR_H_
|
||||
|
||||
#include "util/trail.h"
|
||||
#include "util/union_find.h"
|
||||
#include "util/scoped_ptr_vector.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/arith_decl_plugin.h"
|
||||
#include "ast/rewriter/th_rewriter.h"
|
||||
#include "ast/seq_decl_plugin.h"
|
||||
#include "smt/smt_theory.h"
|
||||
#include "smt/params/theory_str_params.h"
|
||||
#include "smt/proto_model/value_factory.h"
|
||||
|
@ -29,8 +32,6 @@
|
|||
#include<stack>
|
||||
#include<vector>
|
||||
#include<map>
|
||||
#include "ast/seq_decl_plugin.h"
|
||||
#include "util/union_find.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
@ -292,6 +293,7 @@ protected:
|
|||
bool avoidLoopCut;
|
||||
bool loopDetected;
|
||||
obj_map<expr, std::stack<T_cut*> > cut_var_map;
|
||||
scoped_ptr_vector<T_cut> m_cut_allocs;
|
||||
expr_ref m_theoryStrOverlapAssumption_term;
|
||||
|
||||
obj_hashtable<expr> variable_set;
|
||||
|
|
Loading…
Reference in a new issue