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

Revert "experimental z3str2 search order"

Browse source 
This reverts commit 0dfaa30ae8.
This commit is contained in:
Murphy Berzish 2017-01-16 15:46:17 -05:00
parent 0dfaa30ae8
commit 4b6582b8f3
2 changed files with 3 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/smt/theory_str.cpp
View file

@ -41,7 +41,6 @@ theory_str::theory_str(ast_manager & m, theory_str_params const & params):
opt_DeferEQCConsistencyCheck(false), opt_DeferEQCConsistencyCheck(false),
opt_CheckVariableScope(true), opt_CheckVariableScope(true),
opt_ConcatOverlapAvoid(true), opt_ConcatOverlapAvoid(true),
opt_DeferredSearchOrder(true),
/* Internal setup */ /* Internal setup */
search_started(false), search_started(false),
m_autil(m), m_autil(m),
@ -900,8 +899,7 @@ 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_library_aware_axiom_todo.empty() || !m_axiom_RegexIn_todo.empty() || !m_library_aware_axiom_todo.empty()
|| !m_delayed_axiom_setup_terms.empty() || !m_delayed_axiom_setup_terms.empty();
|| (opt_DeferredSearchOrder && !m_new_eqs.empty())
; ;
} }
@ -1002,14 +1000,6 @@ void theory_str::propagate() {
set_up_axioms(m_delayed_axiom_setup_terms[i].get()); set_up_axioms(m_delayed_axiom_setup_terms[i].get());
} }
m_delayed_axiom_setup_terms.reset(); m_delayed_axiom_setup_terms.reset();
if (opt_DeferredSearchOrder) {
for (unsigned i = 0; i < m_new_eqs.size(); ++i) {
var_pair & p = m_new_eqs[i];
cb_new_eq(p.first, p.second);
}
m_new_eqs.reset();
}
} }
} }
@ -7072,15 +7062,7 @@ void theory_str::init_search_eh() {
search_started = true; search_started = true;
} }
void theory_str::new_eq_eh(theory_var v1, theory_var v2) { void theory_str::new_eq_eh(theory_var x, theory_var y) {
if (opt_DeferredSearchOrder) {
m_new_eqs.push_back(var_pair(v1,v2));
} else {
cb_new_eq(v1, v2);
}
}
void theory_str::cb_new_eq(theory_var x, theory_var y) {
//TRACE("t_str_detail", tout << "new eq: v#" << x << " = v#" << y << std::endl;); //TRACE("t_str_detail", tout << "new eq: v#" << x << " = v#" << y << std::endl;);
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;);

16
src/smt/theory_str.h
View file

@ -97,8 +97,6 @@ namespace smt {
} }
}; };
typedef std::pair<theory_var, theory_var> var_pair;
class theory_str : public theory { class theory_str : public theory {
struct T_cut struct T_cut
{ {
@ -190,16 +188,6 @@ namespace smt {
*/ */
bool opt_ConcatOverlapAvoid; bool opt_ConcatOverlapAvoid;
/*
* If DeferredSearchOrder is set to true,
* certain behaviours from user_smt_theory will be emulated in order to
* reproduce more faithfully the search order used by Z3str2.
* In particular, new equalities will be saved and processed during propagate(),
* and asserted axioms will be deferred until the end of each propagate() step.
*/
bool opt_DeferredSearchOrder;
svector<var_pair> m_new_eqs;
bool search_started; bool search_started;
arith_util m_autil; arith_util m_autil;
str_util m_strutil; str_util m_strutil;
@ -597,11 +585,9 @@ namespace smt {
void get_unique_non_concat_nodes(expr * node, std::set<expr*> & argSet); void get_unique_non_concat_nodes(expr * node, std::set<expr*> & argSet);
bool propagate_length_within_eqc(expr * var); bool propagate_length_within_eqc(expr * var);
// TESTING
void refresh_theory_var(expr * e); void refresh_theory_var(expr * e);
// user_smt_theory search order emulation
void cb_new_eq(theory_var v1, theory_var v2);
public: public:
theory_str(ast_manager & m, theory_str_params const & params); theory_str(ast_manager & m, theory_str_params const & params);
virtual ~theory_str(); virtual ~theory_str();