mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

prevent infinite loop of axiom generation. working StartsWith

Browse source
This commit is contained in:
Murphy Berzish 2016-06-14 16:42:46 -04:00
parent c5ffb012dd
commit 4f131ebba7
2 changed files with 17 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/theory_str.cpp
View file

@ -601,6 +601,7 @@ void theory_str::propagate() {
for (unsigned i = 0; i < m_axiom_StartsWith_todo.size(); ++i) {
instantiate_axiom_StartsWith(m_axiom_StartsWith_todo[i]);
}
m_axiom_StartsWith_todo.reset();
}
}
@ -754,6 +755,11 @@ void theory_str::instantiate_axiom_CharAt(enode * e) {
ast_manager & m = get_manager();
app * expr = e->get_owner();
if (axiomatized_terms.contains(expr)) {
TRACE("t_str_detail", tout << "already set up CharAt axiom for " << mk_pp(expr, m) << std::endl;);
return;
}
axiomatized_terms.insert(expr);
TRACE("t_str_detail", tout << "instantiate CharAt axiom for " << mk_pp(expr, m) << std::endl;);
@ -790,7 +796,13 @@ void theory_str::instantiate_axiom_CharAt(enode * e) {
void theory_str::instantiate_axiom_StartsWith(enode * e) {
context & ctx = get_context();
ast_manager & m = get_manager();
app * expr = e->get_owner();
if (axiomatized_terms.contains(expr)) {
TRACE("t_str_detail", tout << "already set up StartsWith axiom for " << mk_pp(expr, m) << std::endl;);
return;
}
axiomatized_terms.insert(expr);
TRACE("t_str_detail", tout << "instantiate StartsWith axiom for " << mk_pp(expr, m) << std::endl;);

5
src/smt/theory_str.h
View file

@ -110,6 +110,11 @@ namespace smt {
ptr_vector<enode> m_axiom_CharAt_todo;
ptr_vector<enode> m_axiom_StartsWith_todo;
// hashtable of all exprs for which we've already set up term-specific axioms --
// this prevents infinite recursive descent with respect to axioms that
// include an occurrence of the term for which axioms are being generated
obj_hashtable<expr> axiomatized_terms;
int tmpStringVarCount;
int tmpXorVarCount;
int tmpLenTestVarCount;