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

very very basic Contains support in theory_str

Browse source 
not included: the 1200 lines of code that make it very fast
This commit is contained in:
Murphy Berzish 2016-06-14 18:43:51 -04:00
parent a3986d6d0e
commit 7aeeb599ef
2 changed files with 33 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/smt/theory_str.cpp
View file

@ -569,6 +569,7 @@ expr * theory_str::mk_concat(expr * n1, expr * n2) {
bool theory_str::can_propagate() { bool theory_str::can_propagate() {
return !m_basicstr_axiom_todo.empty() || !m_str_eq_todo.empty() || !m_concat_axiom_todo.empty() return !m_basicstr_axiom_todo.empty() || !m_str_eq_todo.empty() || !m_concat_axiom_todo.empty()
|| !m_axiom_CharAt_todo.empty() || !m_axiom_StartsWith_todo.empty() || !m_axiom_EndsWith_todo.empty() || !m_axiom_CharAt_todo.empty() || !m_axiom_StartsWith_todo.empty() || !m_axiom_EndsWith_todo.empty()
|| !m_axiom_Contains_todo.empty()
; ;
} }
@ -607,6 +608,11 @@ void theory_str::propagate() {
instantiate_axiom_EndsWith(m_axiom_EndsWith_todo[i]); instantiate_axiom_EndsWith(m_axiom_EndsWith_todo[i]);
} }
m_axiom_EndsWith_todo.reset(); m_axiom_EndsWith_todo.reset();
for (unsigned i = 0; i < m_axiom_Contains_todo.size(); ++i) {
instantiate_axiom_Contains(m_axiom_Contains_todo[i]);
}
m_axiom_Contains_todo.reset();
} }
} }
@ -873,6 +879,27 @@ void theory_str::instantiate_axiom_EndsWith(enode * e) {
assert_axiom(finalAxiom); assert_axiom(finalAxiom);
} }
void theory_str::instantiate_axiom_Contains(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 Contains axiom for " << mk_pp(expr, m) << std::endl;);
return;
}
axiomatized_terms.insert(expr);
TRACE("t_str_detail", tout << "instantiate Contains axiom for " << mk_pp(expr, m) << std::endl;);
expr_ref ts0(mk_str_var("ts0"), m);
expr_ref ts1(mk_str_var("ts1"), m);
// TODO NEXT registerContain(expr);
expr_ref breakdownAssert(ctx.mk_eq_atom(expr, ctx.mk_eq_atom(expr->get_arg(0), mk_concat(ts0, mk_concat(expr->get_arg(1), ts1)))), m);
SASSERT(breakdownAssert);
assert_axiom(breakdownAssert);
}
void theory_str::attach_new_th_var(enode * n) { void theory_str::attach_new_th_var(enode * n) {
context & ctx = get_context(); context & ctx = get_context();
theory_var v = mk_var(n); theory_var v = mk_var(n);
@ -3630,6 +3657,8 @@ void theory_str::set_up_axioms(expr * ex) {
m_axiom_StartsWith_todo.push_back(n); m_axiom_StartsWith_todo.push_back(n);
} else if (is_EndsWith(ap)) { } else if (is_EndsWith(ap)) {
m_axiom_EndsWith_todo.push_back(n); m_axiom_EndsWith_todo.push_back(n);
} else if (is_Contains(ap)) {
m_axiom_Contains_todo.push_back(n);
} }
} }
} else { } else {

4
src/smt/theory_str.h
View file

@ -110,6 +110,7 @@ namespace smt {
ptr_vector<enode> m_axiom_CharAt_todo; ptr_vector<enode> m_axiom_CharAt_todo;
ptr_vector<enode> m_axiom_StartsWith_todo; ptr_vector<enode> m_axiom_StartsWith_todo;
ptr_vector<enode> m_axiom_EndsWith_todo; ptr_vector<enode> m_axiom_EndsWith_todo;
ptr_vector<enode> m_axiom_Contains_todo;
// hashtable of all exprs for which we've already set up term-specific axioms -- // hashtable of all exprs for which we've already set up term-specific axioms --
// this prevents infinite recursive descent with respect to axioms that // this prevents infinite recursive descent with respect to axioms that
@ -183,6 +184,8 @@ namespace smt {
bool is_StartsWith(enode const * n) const { return is_StartsWith(n->get_owner()); } bool is_StartsWith(enode const * n) const { return is_StartsWith(n->get_owner()); }
bool is_EndsWith(app const * a) const { return a->is_app_of(get_id(), OP_STR_ENDSWITH); } bool is_EndsWith(app const * a) const { return a->is_app_of(get_id(), OP_STR_ENDSWITH); }
bool is_EndsWith(enode const * n) const { return is_EndsWith(n->get_owner()); } bool is_EndsWith(enode const * n) const { return is_EndsWith(n->get_owner()); }
bool is_Contains(app const * a) const { return a->is_app_of(get_id(), OP_STR_CONTAINS); }
bool is_Contains(enode const * n) const { return is_Contains(n->get_owner()); }
void instantiate_concat_axiom(enode * cat); void instantiate_concat_axiom(enode * cat);
void instantiate_basic_string_axioms(enode * str); void instantiate_basic_string_axioms(enode * str);
@ -191,6 +194,7 @@ namespace smt {
void instantiate_axiom_CharAt(enode * e); void instantiate_axiom_CharAt(enode * e);
void instantiate_axiom_StartsWith(enode * e); void instantiate_axiom_StartsWith(enode * e);
void instantiate_axiom_EndsWith(enode * e); void instantiate_axiom_EndsWith(enode * e);
void instantiate_axiom_Contains(enode * e);
void set_up_axioms(expr * ex); void set_up_axioms(expr * ex);
void handle_equality(expr * lhs, expr * rhs); void handle_equality(expr * lhs, expr * rhs);