mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 20:03:38 +00:00
Code Activity

defer equalities uncovered during init_search

Browse source
This commit is contained in:
Murphy Berzish 2015-09-27 23:24:41 -04:00
parent 86e6087718
commit 02cb329ca5
2 changed files with 16 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/smt/theory_str.cpp
View file

@ -118,7 +118,7 @@ app * theory_str::mk_strlen(app * e) {
} }
bool theory_str::can_propagate() { bool theory_str::can_propagate() {
return !m_basicstr_axiom_todo.empty() || !m_str_eq_length_axiom_todo.empty(); return !m_basicstr_axiom_todo.empty() || !m_str_eq_todo.empty();
} }
void theory_str::propagate() { void theory_str::propagate() {
@ -129,13 +129,13 @@ void theory_str::propagate() {
} }
m_basicstr_axiom_todo.reset(); m_basicstr_axiom_todo.reset();
for (unsigned i = 0; i < m_str_eq_length_axiom_todo.size(); ++i) { for (unsigned i = 0; i < m_str_eq_todo.size(); ++i) {
std::pair<enode*,enode*> pair = m_str_eq_length_axiom_todo[i]; std::pair<enode*,enode*> pair = m_str_eq_todo[i];
enode * lhs = pair.first; enode * lhs = pair.first;
enode * rhs = pair.second; enode * rhs = pair.second;
instantiate_str_eq_length_axiom(lhs, rhs); handle_equality(lhs->get_owner(), rhs->get_owner());
} }
m_str_eq_length_axiom_todo.reset(); m_str_eq_todo.reset();
} }
TRACE("t_str_detail", tout << "done propagating" << std::endl;); TRACE("t_str_detail", tout << "done propagating" << std::endl;);
} }
@ -299,7 +299,7 @@ void theory_str::attach_new_th_var(enode * n) {
void theory_str::reset_eh() { void theory_str::reset_eh() {
TRACE("t_str", tout << "resetting" << std::endl;); TRACE("t_str", tout << "resetting" << std::endl;);
m_basicstr_axiom_todo.reset(); m_basicstr_axiom_todo.reset();
m_str_eq_length_axiom_todo.reset(); m_str_eq_todo.reset();
pop_scope_eh(0); pop_scope_eh(0);
} }
@ -382,10 +382,10 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) {
TRACE("t_str", tout << "quick path: concat == \"\"" << std::endl;); TRACE("t_str", tout << "quick path: concat == \"\"" << std::endl;);
// assert the following axiom: // assert the following axiom:
// ( (Concat a1 a2) == str ) -> ( (a1 == "") AND (a2 == "") ) // ( (Concat a1 a2) == str ) -> ( (a1 == "") AND (a2 == "") )
expr_ref premise(ctx.mk_eq_atom(concat, str), m); expr_ref premise(m.mk_eq(concat, str), m);
expr_ref empty_str(m_strutil.mk_string(""), m); expr_ref empty_str(m_strutil.mk_string(""), m);
expr_ref c1(ctx.mk_eq_atom(a1, empty_str), m); expr_ref c1(m.mk_eq(a1, empty_str), m);
expr_ref c2(ctx.mk_eq_atom(a2, empty_str), m); expr_ref c2(m.mk_eq(a2, empty_str), m);
expr_ref conclusion(m.mk_and(c1, c2), m); expr_ref conclusion(m.mk_and(c1, c2), m);
expr_ref axiom(m.mk_implies(premise, conclusion), m); expr_ref axiom(m.mk_implies(premise, conclusion), m);
TRACE("t_str_detail", tout << "learn " << mk_ismt2_pp(axiom, m) << std::endl;); TRACE("t_str_detail", tout << "learn " << mk_ismt2_pp(axiom, m) << std::endl;);
@ -423,12 +423,7 @@ void theory_str::handle_equality(expr * lhs, expr * rhs) {
// TODO there's some setup with getLenValue() that I don't think is necessary // TODO there's some setup with getLenValue() that I don't think is necessary
// because we should already be generating the string length axioms for all string terms // because we should already be generating the string length axioms for all string terms
// set up string length axiom: instantiate_str_eq_length_axiom(ctx.get_enode(lhs), ctx.get_enode(rhs));
// (lhs == rhs) -> (Length(lhs) == Length(rhs))
enode * e_lhs = ctx.get_enode(lhs);
enode * e_rhs = ctx.get_enode(rhs);
std::pair<enode*,enode*> eq_pair(e_lhs, e_rhs);
m_str_eq_length_axiom_todo.push_back(eq_pair);
// group terms by equivalence class (groupNodeInEqc()) // group terms by equivalence class (groupNodeInEqc())
std::set<expr*> eqc_lhs_concat; std::set<expr*> eqc_lhs_concat;
@ -553,9 +548,6 @@ void theory_str::init_search_eh() {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
context & ctx = get_context(); context & ctx = get_context();
// TODO it would be better to refactor this function so that instead of deferring the axioms
// instead we defer the evaluation of the expression
TRACE("t_str_detail", TRACE("t_str_detail",
tout << "dumping all asserted formulas:" << std::endl; tout << "dumping all asserted formulas:" << std::endl;
unsigned nFormulas = ctx.get_num_asserted_formulas(); unsigned nFormulas = ctx.get_num_asserted_formulas();
@ -592,7 +584,11 @@ void theory_str::init_search_eh() {
SASSERT(eq->get_num_args() == 2); SASSERT(eq->get_num_args() == 2);
expr * lhs = eq->get_arg(0); expr * lhs = eq->get_arg(0);
expr * rhs = eq->get_arg(1); expr * rhs = eq->get_arg(1);
handle_equality(lhs, rhs);
enode * e_lhs = ctx.get_enode(lhs);
enode * e_rhs = ctx.get_enode(rhs);
std::pair<enode*,enode*> eq_pair(e_lhs, e_rhs);
m_str_eq_todo.push_back(eq_pair);
} else { } else {
TRACE("t_str_detail", tout << "expr ignored" << std::endl;); TRACE("t_str_detail", tout << "expr ignored" << std::endl;);
} }

2
src/smt/theory_str.h
View file

@ -39,7 +39,7 @@ namespace smt {
str_util m_strutil; str_util m_strutil;
ptr_vector<enode> m_basicstr_axiom_todo; ptr_vector<enode> m_basicstr_axiom_todo;
svector<std::pair<enode*,enode*> > m_str_eq_length_axiom_todo; svector<std::pair<enode*,enode*> > m_str_eq_todo;
protected: protected:
void assert_axiom(ast * e); void assert_axiom(ast * e);