mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix #1005, disable expansion of regular expression range to union as it degrades performance significantly

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-05 10:59:47 -04:00
parent 9499fa62ac
commit 7e1fae418a
3 changed files with 9 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/seq_rewriter.cpp
View file

@ -1434,6 +1434,7 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
* (re.range c_1 c_n) = (re.union (str.to.re c1) (str.to.re c2) ... (str.to.re cn))
*/
br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) {
return BR_FAILED;
TRACE("seq", tout << "rewrite re.range [" << mk_pp(lo, m()) << " " << mk_pp(hi, m()) << "]\n";);
zstring str_lo, str_hi;
if (m_util.str.is_string(lo, str_lo) && m_util.str.is_string(hi, str_hi)) {

2
src/smt/theory_arith.h
View file

@ -505,7 +505,7 @@ namespace smt {
struct var_value_eq {
theory_arith & m_th;
var_value_eq(theory_arith & th):m_th(th) {}
bool operator()(theory_var v1, theory_var v2) const { return m_th.get_value(v1) == m_th.get_value(v2) && m_th.is_int(v1) == m_th.is_int(v2); }
bool operator()(theory_var v1, theory_var v2) const { return m_th.get_value(v1) == m_th.get_value(v2) && m_th.is_int_src(v1) == m_th.is_int_src(v2); }
};
typedef int_hashtable<var_value_hash, var_value_eq> var_value_table;

11
src/smt/theory_arith_aux.h
View file

@ -2201,16 +2201,19 @@ namespace smt {
int num = get_num_vars();
for (theory_var v = 0; v < num; v++) {
enode * n = get_enode(v);
TRACE("func_interp_bug", tout << "#" << n->get_owner_id() << " -> " << m_value[v] << "\n";);
if (!is_relevant_and_shared(n))
TRACE("func_interp_bug", tout << mk_pp(n->get_owner(), get_manager()) << " -> " << m_value[v] << " root #" << n->get_root()->get_owner_id() << " " << is_relevant_and_shared(n) << "\n";);
if (!is_relevant_and_shared(n)) {
continue;
}
theory_var other = null_theory_var;
other = m_var_value_table.insert_if_not_there(v);
if (other == v)
if (other == v) {
continue;
}
enode * n2 = get_enode(other);
if (n->get_root() == n2->get_root())
if (n->get_root() == n2->get_root()) {
continue;
}
TRACE("func_interp_bug", tout << "adding to assume_eq queue #" << n->get_owner_id() << " #" << n2->get_owner_id() << "\n";);
m_assume_eq_candidates.push_back(std::make_pair(other, v));
result = true;