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

fix cache bug in PDR reported by Phillip Ruemmer

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-17 21:20:56 -07:00
parent 5a45711f22
commit 60054ce469
2 changed files with 34 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -736,6 +736,11 @@ namespace pdr {
m_closed = true; m_closed = true;
} }
void model_node::reopen() {
SASSERT(m_closed);
m_closed = false;
}
static bool is_ini(datalog::rule const& r) { static bool is_ini(datalog::rule const& r) {
return r.get_uninterpreted_tail_size() == 0; return r.get_uninterpreted_tail_size() == 0;
} }
@ -745,6 +750,7 @@ namespace pdr {
return const_cast<datalog::rule*>(m_rule); return const_cast<datalog::rule*>(m_rule);
} }
// only initial states are not set by the PDR search. // only initial states are not set by the PDR search.
SASSERT(m_model.get());
datalog::rule const& rl1 = pt().find_rule(*m_model); datalog::rule const& rl1 = pt().find_rule(*m_model);
if (is_ini(rl1)) { if (is_ini(rl1)) {
set_rule(&rl1); set_rule(&rl1);
@ -864,9 +870,10 @@ namespace pdr {
} }
void model_search::add_leaf(model_node& n) { void model_search::add_leaf(model_node& n) {
unsigned& count = cache(n).insert_if_not_there2(n.state(), 0)->get_data().m_value; model_nodes ns;
++count; model_nodes& nodes = cache(n).insert_if_not_there2(n.state(), ns)->get_data().m_value;
if (count == 1 || is_repeated(n)) { nodes.push_back(&n);
if (nodes.size() == 1 || is_repeated(n)) {
set_leaf(n); set_leaf(n);
} }
else { else {
@ -875,7 +882,7 @@ namespace pdr {
} }
void model_search::set_leaf(model_node& n) { void model_search::set_leaf(model_node& n) {
erase_children(n); erase_children(n, true);
SASSERT(n.is_open()); SASSERT(n.is_open());
enqueue_leaf(n); enqueue_leaf(n);
} }
@ -897,7 +904,7 @@ namespace pdr {
set_leaf(*root); set_leaf(*root);
} }
obj_map<expr, unsigned>& model_search::cache(model_node const& n) { obj_map<expr, ptr_vector<model_node> >& model_search::cache(model_node const& n) {
unsigned l = n.orig_level(); unsigned l = n.orig_level();
if (l >= m_cache.size()) { if (l >= m_cache.size()) {
m_cache.resize(l + 1); m_cache.resize(l + 1);
@ -905,7 +912,7 @@ namespace pdr {
return m_cache[l]; return m_cache[l];
} }
void model_search::erase_children(model_node& n) { void model_search::erase_children(model_node& n, bool backtrack) {
ptr_vector<model_node> todo, nodes; ptr_vector<model_node> todo, nodes;
todo.append(n.children()); todo.append(n.children());
erase_leaf(n); erase_leaf(n);
@ -916,13 +923,20 @@ namespace pdr {
nodes.push_back(m); nodes.push_back(m);
todo.append(m->children()); todo.append(m->children());
erase_leaf(*m); erase_leaf(*m);
remove_node(*m); remove_node(*m, backtrack);
} }
std::for_each(nodes.begin(), nodes.end(), delete_proc<model_node>()); std::for_each(nodes.begin(), nodes.end(), delete_proc<model_node>());
} }
void model_search::remove_node(model_node& n) { void model_search::remove_node(model_node& n, bool backtrack) {
if (0 == --cache(n).find(n.state())) { model_nodes& nodes = cache(n).find(n.state());
nodes.erase(&n);
if (nodes.size() > 0 && n.is_open() && backtrack) {
for (unsigned i = 0; i < nodes.size(); ++i) {
nodes[i]->reopen();
}
}
if (nodes.empty()) {
cache(n).remove(n.state()); cache(n).remove(n.state());
} }
} }
@ -1203,8 +1217,8 @@ namespace pdr {
void model_search::reset() { void model_search::reset() {
if (m_root) { if (m_root) {
erase_children(*m_root); erase_children(*m_root, false);
remove_node(*m_root); remove_node(*m_root, false);
dealloc(m_root); dealloc(m_root);
m_root = 0; m_root = 0;
} }
@ -1240,7 +1254,7 @@ namespace pdr {
m_pm(m_fparams, params.max_num_contexts(), m), m_pm(m_fparams, params.max_num_contexts(), m),
m_query_pred(m), m_query_pred(m),
m_query(0), m_query(0),
m_search(m_params.bfs_model_search()), m_search(m_params.bfs_model_search(), m),
m_last_result(l_undef), m_last_result(l_undef),
m_inductive_lvl(0), m_inductive_lvl(0),
m_expanded_lvl(0), m_expanded_lvl(0),

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

@ -231,6 +231,7 @@ namespace pdr {
} }
void set_closed(); void set_closed();
void reopen();
void set_pre_closed() { m_closed = true; } void set_pre_closed() { m_closed = true; }
void reset() { m_children.reset(); } void reset() { m_children.reset(); }
@ -243,19 +244,21 @@ namespace pdr {
}; };
class model_search { class model_search {
typedef ptr_vector<model_node> model_nodes;
ast_manager& m;
bool m_bfs; bool m_bfs;
model_node* m_root; model_node* m_root;
std::deque<model_node*> m_leaves; std::deque<model_node*> m_leaves;
vector<obj_map<expr, unsigned> > m_cache; vector<obj_map<expr, model_nodes > > m_cache;
obj_map<expr, unsigned>& cache(model_node const& n); obj_map<expr, model_nodes>& cache(model_node const& n);
void erase_children(model_node& n); void erase_children(model_node& n, bool backtrack);
void erase_leaf(model_node& n); void erase_leaf(model_node& n);
void remove_node(model_node& n); void remove_node(model_node& n, bool backtrack);
void enqueue_leaf(model_node& n); // add leaf to priority queue. void enqueue_leaf(model_node& n); // add leaf to priority queue.
void update_models(); void update_models();
public: public:
model_search(bool bfs): m_bfs(bfs), m_root(0) {} model_search(bool bfs, ast_manager& m): m(m), m_bfs(bfs), m_root(0) {}
~model_search(); ~model_search();
void reset(); void reset();