mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 13:47:01 +00:00
Code Activity

break stack abuse in relevancy propagation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-07-12 14:52:43 -07:00
parent 21201371ed
commit 6fbc8fa06c
1 changed files with 9 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/smt_relevancy.cpp
View file

@ -148,8 +148,11 @@ namespace smt {
unsigned m_trail_lim; unsigned m_trail_lim;
}; };
svector<scope> m_scopes; svector<scope> m_scopes;
bool m_propagating;
relevancy_propagator_imp(context & ctx):relevancy_propagator(ctx), m_qhead(0), m_relevant_exprs(ctx.get_manager()) {} relevancy_propagator_imp(context & ctx):
relevancy_propagator(ctx), m_qhead(0), m_relevant_exprs(ctx.get_manager()),
m_propagating(false) {}
virtual ~relevancy_propagator_imp() { virtual ~relevancy_propagator_imp() {
undo_trail(0); undo_trail(0);
@ -448,6 +451,11 @@ namespace smt {
relevant expressions. relevant expressions.
*/ */
virtual void propagate() { virtual void propagate() {
if (m_propagating) {
return;
}
flet<bool> l_prop(m_propagating, true);
ast_manager & m = get_manager(); ast_manager & m = get_manager();
while (m_qhead < m_relevant_exprs.size()) { while (m_qhead < m_relevant_exprs.size()) {
expr * n = m_relevant_exprs.get(m_qhead); expr * n = m_relevant_exprs.get(m_qhead);