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

mark the position of the bug I found so I can recall it later

Browse source 
in process_concat_eq_type1() line 1048
This commit is contained in:
Murphy Berzish 2015-09-30 09:45:00 -04:00
parent 5189c24d42
commit f8c13792a3
2 changed files with 25 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/smt/theory_str.cpp
View file

@ -1045,6 +1045,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
expr_ref m_plus_t2(m_autil.mk_add(mk_strlen(m), mk_strlen(t2)), mgr); expr_ref m_plus_t2(m_autil.mk_add(mk_strlen(m), mk_strlen(t2)), mgr);
// TODO here is the bug: these EQs should be GTs
and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(mk_strlen(x), m_plus_t2)); and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(mk_strlen(x), m_plus_t2));
and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(mk_strlen(x), mk_strlen(m))); and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(mk_strlen(x), mk_strlen(m)));
and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(mk_strlen(n), mk_strlen(y))); and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(mk_strlen(n), mk_strlen(y)));
@ -1724,6 +1725,7 @@ void theory_str::init_search_eh() {
* This is done to find equalities between terms, etc. that we otherwise * This is done to find equalities between terms, etc. that we otherwise
* might not get a chance to see. * might not get a chance to see.
*/ */
/*
expr_ref_vector assignments(m); expr_ref_vector assignments(m);
ctx.get_assignments(assignments); ctx.get_assignments(assignments);
for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) { for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) {
@ -1745,6 +1747,7 @@ void theory_str::init_search_eh() {
<< ": expr ignored" << std::endl;); << ": expr ignored" << std::endl;);
} }
} }
*/
TRACE("t_str", tout << "search started" << std::endl;); TRACE("t_str", tout << "search started" << std::endl;);
search_started = true; search_started = true;
@ -1755,12 +1758,16 @@ void theory_str::new_eq_eh(theory_var x, theory_var y) {
TRACE("t_str", tout << "new eq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " = " << TRACE("t_str", tout << "new eq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " = " <<
mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;); mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;);
handle_equality(get_enode(x)->get_owner(), get_enode(y)->get_owner()); handle_equality(get_enode(x)->get_owner(), get_enode(y)->get_owner());
TRACE("t_str_detail", dump_assignments(););
} }
void theory_str::new_diseq_eh(theory_var x, theory_var y) { void theory_str::new_diseq_eh(theory_var x, theory_var y) {
//TRACE("t_str_detail", tout << "new diseq: v#" << x << " != v#" << y << std::endl;); //TRACE("t_str_detail", tout << "new diseq: v#" << x << " != v#" << y << std::endl;);
TRACE("t_str", tout << "new diseq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " != " << TRACE("t_str", tout << "new diseq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " != " <<
mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;); mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;);
TRACE("t_str_detail", dump_assignments(););
} }
void theory_str::relevant_eh(app * n) { void theory_str::relevant_eh(app * n) {
@ -1779,7 +1786,7 @@ void theory_str::push_scope_eh() {
void theory_str::pop_scope_eh(unsigned num_scopes) { void theory_str::pop_scope_eh(unsigned num_scopes) {
TRACE("t_str", tout << "pop " << num_scopes << std::endl;); TRACE("t_str", tout << "pop " << num_scopes << std::endl;);
context & ctx = get_context(); context & ctx = get_context();
unsigned sLevel = ctx.get_scope_level(); int sLevel = ctx.get_scope_level();
std::map<expr*, std::stack<T_cut *> >::iterator varItor = cut_var_map.begin(); std::map<expr*, std::stack<T_cut *> >::iterator varItor = cut_var_map.begin();
while (varItor != cut_var_map.end()) { while (varItor != cut_var_map.end()) {
while ((varItor->second.size() > 0) && (varItor->second.top()->level != 0) && (varItor->second.top()->level >= sLevel)) { while ((varItor->second.size() > 0) && (varItor->second.top()->level != 0) && (varItor->second.top()->level >= sLevel)) {
@ -1794,21 +1801,25 @@ void theory_str::pop_scope_eh(unsigned num_scopes) {
} }
} }
void theory_str::dump_assignments() {
ast_manager & m = get_manager();
context & ctx = get_context();
TRACE("t_str_detail",
tout << "dumping all assignments:" << std::endl;
expr_ref_vector assignments(m);
ctx.get_assignments(assignments);
for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) {
expr * ex = *i;
tout << mk_ismt2_pp(ex, m) << std::endl;
}
);
}
final_check_status theory_str::final_check_eh() { final_check_status theory_str::final_check_eh() {
ast_manager & m = get_manager();
context & ctx = get_context();
// TODO // TODO
TRACE("t_str", tout << "final check" << std::endl;); TRACE("t_str", tout << "final check" << std::endl;);
TRACE("t_str_detail", TRACE("t_str_detail", dump_assignments(););
tout << "dumping all assignments:" << std::endl;
expr_ref_vector assignments(m);
ctx.get_assignments(assignments);
for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) {
expr * ex = *i;
tout << mk_ismt2_pp(ex, m) << std::endl;
}
);
return FC_DONE; return FC_DONE;
} }

2
src/smt/theory_str.h
View file

@ -136,6 +136,8 @@ namespace smt {
bool new_eq_check(expr * lhs, expr * rhs); bool new_eq_check(expr * lhs, expr * rhs);
void group_terms_by_eqc(expr * n, std::set<expr*> & concats, std::set<expr*> & vars, std::set<expr*> & consts); void group_terms_by_eqc(expr * n, std::set<expr*> & concats, std::set<expr*> & vars, std::set<expr*> & consts);
void dump_assignments();
public: public:
theory_str(ast_manager & m); theory_str(ast_manager & m);
virtual ~theory_str(); virtual ~theory_str();