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

crash avoidance in theory_str search start, fixes length-001.smt2 regression

Browse source
This commit is contained in:
Murphy Berzish 2016-08-09 20:11:25 -04:00
parent 3dff240bb3
commit f7ba3ff084
2 changed files with 19 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/smt/theory_str.cpp
View file

@ -42,6 +42,7 @@ theory_str::theory_str(ast_manager & m):
sLevel(0), sLevel(0),
finalCheckProgressIndicator(false), finalCheckProgressIndicator(false),
m_trail(m), m_trail(m),
m_delayed_axiom_setup_terms(m),
tmpStringVarCount(0), tmpStringVarCount(0),
tmpXorVarCount(0), tmpXorVarCount(0),
tmpLenTestVarCount(0), tmpLenTestVarCount(0),
@ -755,10 +756,12 @@ bool theory_str::can_propagate() {
|| !m_axiom_Contains_todo.empty() || !m_axiom_Indexof_todo.empty() || !m_axiom_Indexof2_todo.empty() || !m_axiom_LastIndexof_todo.empty() || !m_axiom_Contains_todo.empty() || !m_axiom_Indexof_todo.empty() || !m_axiom_Indexof2_todo.empty() || !m_axiom_LastIndexof_todo.empty()
|| !m_axiom_Substr_todo.empty() || !m_axiom_Replace_todo.empty() || !m_axiom_Substr_todo.empty() || !m_axiom_Replace_todo.empty()
|| !m_axiom_RegexIn_todo.empty() || !m_axiom_RegexIn_todo.empty()
|| !m_delayed_axiom_setup_terms.empty();
; ;
} }
void theory_str::propagate() { void theory_str::propagate() {
context & ctx = get_context();
while (can_propagate()) { while (can_propagate()) {
TRACE("t_str_detail", tout << "propagating..." << std::endl;); TRACE("t_str_detail", tout << "propagating..." << std::endl;);
for (unsigned i = 0; i < m_basicstr_axiom_todo.size(); ++i) { for (unsigned i = 0; i < m_basicstr_axiom_todo.size(); ++i) {
@ -829,6 +832,13 @@ void theory_str::propagate() {
instantiate_axiom_RegexIn(m_axiom_RegexIn_todo[i]); instantiate_axiom_RegexIn(m_axiom_RegexIn_todo[i]);
} }
m_axiom_RegexIn_todo.reset(); m_axiom_RegexIn_todo.reset();
for (unsigned i = 0; i < m_delayed_axiom_setup_terms.size(); ++i) {
// I think this is okay
ctx.internalize(m_delayed_axiom_setup_terms[i].get(), false);
set_up_axioms(m_delayed_axiom_setup_terms[i].get());
}
m_delayed_axiom_setup_terms.reset();
} }
} }
@ -5140,6 +5150,7 @@ void theory_str::set_up_axioms(expr * ex) {
": expr is of sort Bool" << std::endl;); ": expr is of sort Bool" << std::endl;);
// set up axioms for boolean terms // set up axioms for boolean terms
ensure_enode(ex);
if (ctx.e_internalized(ex)) { if (ctx.e_internalized(ex)) {
enode * n = ctx.get_enode(ex); enode * n = ctx.get_enode(ex);
SASSERT(n); SASSERT(n);
@ -5157,14 +5168,16 @@ void theory_str::set_up_axioms(expr * ex) {
} }
} }
} else { } else {
TRACE("t_str_detail", tout << "WARNING: Bool term " << mk_ismt2_pp(ex, get_manager()) << " not internalized. Skipping to prevent a crash." << std::endl;); TRACE("t_str_detail", tout << "WARNING: Bool term " << mk_ismt2_pp(ex, get_manager()) << " not internalized. Delaying axiom setup to prevent a crash." << std::endl;);
ENSURE(!search_started); // infinite loop prevention
m_delayed_axiom_setup_terms.push_back(ex);
return; return;
} }
} else if (ex_sort == int_sort) { } else if (ex_sort == int_sort) {
TRACE("t_str_detail", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) << TRACE("t_str_detail", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) <<
": expr is of sort Int" << std::endl;); ": expr is of sort Int" << std::endl;);
// set up axioms for boolean terms // set up axioms for integer terms
enode * n = ctx.get_enode(ex); enode * n = ensure_enode(ex);
SASSERT(n); SASSERT(n);
if (is_app(ex)) { if (is_app(ex)) {

3
src/smt/theory_str.h
View file

@ -129,6 +129,9 @@ namespace smt {
str_value_factory * m_factory; str_value_factory * m_factory;
// terms we couldn't go through set_up_axioms() with because they weren't internalized
expr_ref_vector m_delayed_axiom_setup_terms;
ptr_vector<enode> m_basicstr_axiom_todo; ptr_vector<enode> m_basicstr_axiom_todo;
svector<std::pair<enode*,enode*> > m_str_eq_todo; svector<std::pair<enode*,enode*> > m_str_eq_todo;
ptr_vector<enode> m_concat_axiom_todo; ptr_vector<enode> m_concat_axiom_todo;