mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

decongest critical section in lia2card-tactic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-05-17 22:59:11 +01:00
parent afea50e631
commit 552bba2c8c
1 changed files with 22 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/tactic/arith/lia2card_tactic.cpp
View file

@ -31,18 +31,22 @@ public:
arith_util a; arith_util a;
params_ref m_params; params_ref m_params;
pb_util m_pb; pb_util m_pb;
mutable ptr_vector<expr> m_todo; mutable ptr_vector<expr>* m_todo;
expr_set m_01s; expr_set* m_01s;
bool m_compile_equality; bool m_compile_equality;
lia2card_tactic(ast_manager & _m, params_ref const & p): lia2card_tactic(ast_manager & _m, params_ref const & p):
m(_m), m(_m),
a(m), a(m),
m_pb(m), m_pb(m),
m_todo(alloc(ptr_vector<expr>)),
m_01s(alloc(expr_set)),
m_compile_equality(false) { m_compile_equality(false) {
} }
virtual ~lia2card_tactic() { virtual ~lia2card_tactic() {
dealloc(m_todo);
dealloc(m_01s);
} }
void set_cancel(bool f) { void set_cancel(bool f) {
@ -60,7 +64,7 @@ public:
expr_dependency_ref & core) { expr_dependency_ref & core) {
SASSERT(g->is_well_sorted()); SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0; mc = 0; pc = 0; core = 0;
m_01s.reset(); m_01s->reset();
tactic_report report("cardinality-intro", *g); tactic_report report("cardinality-intro", *g);
@ -76,7 +80,7 @@ public:
if (a.is_int(x) && if (a.is_int(x) &&
bounds.has_lower(x, lo, s1) && !s1 && lo.is_zero() && bounds.has_lower(x, lo, s1) && !s1 && lo.is_zero() &&
bounds.has_upper(x, hi, s2) && !s2 && hi.is_one()) { bounds.has_upper(x, hi, s2) && !s2 && hi.is_one()) {
m_01s.insert(x); m_01s->insert(x);
TRACE("pb", tout << "add bound " << mk_pp(x, m) << "\n";); TRACE("pb", tout << "add bound " << mk_pp(x, m) << "\n";);
} }
} }
@ -114,11 +118,11 @@ public:
void extract_pb_substitution(ast_mark& mark, expr* fml, expr_safe_replace& sub) { void extract_pb_substitution(ast_mark& mark, expr* fml, expr_safe_replace& sub) {
expr_ref tmp(m); expr_ref tmp(m);
m_todo.reset(); m_todo->reset();
m_todo.push_back(fml); m_todo->push_back(fml);
while (!m_todo.empty()) { while (!m_todo->empty()) {
expr* e = m_todo.back(); expr* e = m_todo->back();
m_todo.pop_back(); m_todo->pop_back();
if (mark.is_marked(e) || !is_app(e)) { if (mark.is_marked(e) || !is_app(e)) {
continue; continue;
} }
@ -128,13 +132,13 @@ public:
continue; continue;
} }
app* ap = to_app(e); app* ap = to_app(e);
m_todo.append(ap->get_num_args(), ap->get_args()); m_todo->append(ap->get_num_args(), ap->get_args());
} }
} }
bool is_01var(expr* x) const { bool is_01var(expr* x) const {
return m_01s.contains(x); return m_01s->contains(x);
} }
expr_ref mk_01(expr* x) { expr_ref mk_01(expr* x) {
@ -283,11 +287,15 @@ public:
} }
virtual void cleanup() { virtual void cleanup() {
expr_set* d = alloc(expr_set);
ptr_vector<expr>* todo = alloc(ptr_vector<expr>);
#pragma omp critical (tactic_cancel) #pragma omp critical (tactic_cancel)
{ {
m_01s.reset(); std::swap(m_01s, d);
m_todo.reset(); std::swap(m_todo, todo);
} }
dealloc(d);
dealloc(todo);
} }
}; };