Skip to content

Commit

Permalink
remove symbol -> zstring -> symbol round-trips
Browse files Browse the repository at this point in the history 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed May 22, 2021
1 parent 5cb0bac commit 20a67e4
Show file tree
Hide file tree
Showing 13 changed files with 68 additions and 62 deletions.
7 changes: 7 additions & 0 deletions src/ast/ast.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,9 @@ parameter::~parameter() {
if (m_kind == PARAM_RATIONAL) {
dealloc(m_rational);
}
if (m_kind == PARAM_ZSTRING) {
dealloc(m_zstring);
}
}

parameter::parameter(parameter const& other) {
Expand All @@ -64,6 +67,7 @@ parameter& parameter::operator=(parameter const& other) {
case PARAM_RATIONAL: m_rational = alloc(rational, other.get_rational()); break;
case PARAM_DOUBLE: m_dval = other.m_dval; break;
case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break;
case PARAM_ZSTRING: m_zstring = alloc(zstring, other.get_zstring()); break;
default:
UNREACHABLE();
break;
Expand Down Expand Up @@ -99,6 +103,7 @@ bool parameter::operator==(parameter const & p) const {
case PARAM_RATIONAL: return get_rational() == p.get_rational();
case PARAM_DOUBLE: return m_dval == p.m_dval;
case PARAM_EXTERNAL: return m_ext_id == p.m_ext_id;
case PARAM_ZSTRING: return get_zstring() == p.get_zstring();
default: UNREACHABLE(); return false;
}
}
Expand All @@ -111,6 +116,7 @@ unsigned parameter::hash() const {
case PARAM_SYMBOL: b = get_symbol().hash(); break;
case PARAM_RATIONAL: b = get_rational().hash(); break;
case PARAM_DOUBLE: b = static_cast<unsigned>(m_dval); break;
case PARAM_ZSTRING: b = get_zstring().hash(); break;
case PARAM_EXTERNAL: b = m_ext_id; break;
}
return (b << 2) | m_kind;

This comment has been minimized.

Sign in to view

Copy link
@NikolajBjorner

NikolajBjorner May 24, 2021

Author Contributor

@nunoplopes could you see if b << 3 makes a difference?
m_kind uses now more than 2 bits to represent.
I don't see why adding ZSTRING should influence your code-path at all.

This comment has been minimized.

Sign in to view

Copy link
@nunoplopes

nunoplopes May 24, 2021

Collaborator

m_kind changed because the order in the enum changed. But I'll try << 3 😀

This comment has been minimized.

Sign in to view

Copy link
@NikolajBjorner

NikolajBjorner May 24, 2021

Author Contributor

Have you double checked variability over random seeds?
Do you have a way to profile memory (Windows memory profiler still works for me when debugging stand-alone memory usage) for what you are doing?

This comment has been minimized.

Sign in to view

Copy link
@NikolajBjorner

NikolajBjorner May 24, 2021

Author Contributor

I really don't see why << 2 vs << 3 should matter. It could also have been ^ m_kind or even ignoring m_kind if the hash functions for the parameter entries are any reasonable.

This comment has been minimized.

Sign in to view

Copy link
@nunoplopes

nunoplopes May 24, 2021

Collaborator

<<2 vs << 3 matters because for rationals it now misses the bit entirely, as m_kind changed from 3 to 4.
So the last 3 bits of such hashes will always be '100'. So it loses the last bit of 'b' as it's overwritten. I guess that was already happening for PARAM_DOUBLE & PARAM_EXTERNAL, but I don't use those.
Maybe something to try as well is to just ignore m_kind as you suggest. I'll try.

This comment has been minimized.

Sign in to view

Copy link
@nunoplopes

nunoplopes May 25, 2021

Collaborator

I benchmarked master vs return (b<<3) | m_kind vs return b.
The last 2 options are much better than master (faster & fewer OOMs), and return b even performs a bit better (and less 1 OOM).
Can I do the honors and change it to return b? Do you want try some other benchmarks? (I only see a difference with large benchmarks, like 100+ MBs of smtlib).

This comment has been minimized.

Sign in to view

Copy link
@NikolajBjorner

NikolajBjorner May 25, 2021

Author Contributor

Doesn't make sense: b has all the entropy of b, b << 2 looses 2 bits, b << 3 looses 3 bits and replace by m_kind.
Are you sure the fluctuation you see isn't at the level of noise?

This comment has been minimized.

Sign in to view

Copy link
@nunoplopes

nunoplopes May 25, 2021

Collaborator

(b << 2) | m_kind is the worst possible because it stacks one bit of m_kind on top of b. Moreover, that's the least significant bit of b, which is important, because the hash table will truncate the hash to the first 'n' least significant bits.

So, b << 2 or b << 3 or b doesn't really matter in terms of the bits they lose, because they lose bits that aren't used by the hash table anyway. Making sure we don't use a bit in the least significant area is the most important thing here.
In ASCII art:

b                 = bbbbbbbbbb
b << 2            = bbbbbbbb00
b << 2 | RATIONAL = bbbbbbb100  <-- lost 1 bit of b

usage in the hash table:
bucket number = hash & ((1 << n)-1)  = 0000bb100 (e.g.)

This shows why return b or return (b << 3) | m_kind are the best options. And why return b is even better if expressions are biased towards a single kind. My experimental results back this theory nicely.

The results I'm seeing are not in the noise. I'm seeing close to double OOMs due to increased number of hash collisions.

This comment has been minimized.

Sign in to view

Copy link
@NikolajBjorner

NikolajBjorner May 25, 2021

Author Contributor

you are still not considering "XOR", that is b ^ m_kind. It should be similar to just b.

This comment has been minimized.

Sign in to view

Copy link
@NikolajBjorner

NikolajBjorner May 25, 2021

Author Contributor

I see that since the hash table depends on the lower bits for bucket selection it is important that bits are evenly distributed. Using just the kind bits as low order is very bad.

This comment has been minimized.

Sign in to view

Copy link
@nunoplopes

nunoplopes May 26, 2021

Collaborator

I'm running my benchmarks with xor now. Will give the results tmr.

This comment has been minimized.

Sign in to view

Copy link
@nunoplopes

nunoplopes May 27, 2021

Collaborator

return b wins. the xor is the 3rd, return b << 3 the 2nd. All way better than the current version.
I've changed this now! 😀
Expand All @@ -124,6 +130,7 @@ std::ostream& parameter::display(std::ostream& out) const {
case PARAM_AST: return out << "#" << get_ast()->get_id();
case PARAM_DOUBLE: return out << m_dval;
case PARAM_EXTERNAL: return out << "@" << m_ext_id;
case PARAM_ZSTRING: return out << get_zstring();
default:
UNREACHABLE();
return out << "[invalid parameter]";
Expand Down
11 changes: 10 additions & 1 deletion src/ast/ast.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ Revision History:
#include "util/vector.h"
#include "util/hashtable.h"
#include "util/buffer.h"
#include "util/zstring.h"
#include "util/symbol.h"
#include "util/rational.h"
#include "util/hash.h"
Expand Down Expand Up @@ -100,6 +101,7 @@ class parameter {
PARAM_INT,
PARAM_AST,
PARAM_SYMBOL,
PARAM_ZSTRING,
PARAM_RATIONAL,
PARAM_DOUBLE,
// PARAM_EXTERNAL is used for handling decl_plugin specific parameters.
Expand All @@ -119,6 +121,7 @@ class parameter {
ast* m_ast; // for PARAM_AST
symbol m_symbol; // for PARAM_SYMBOL
rational* m_rational; // for PARAM_RATIONAL
zstring* m_zstring; // for PARAM_ZSTRING
double m_dval; // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin)
unsigned m_ext_id; // for PARAM_EXTERNAL
};
Expand All @@ -131,7 +134,9 @@ class parameter {
explicit parameter(ast * p): m_kind(PARAM_AST), m_ast(p) {}
explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL), m_symbol(s) {}
explicit parameter(rational const & r): m_kind(PARAM_RATIONAL), m_rational(alloc(rational, r)) {}
explicit parameter(rational && r) : m_kind(PARAM_RATIONAL), m_rational(alloc(rational, std::move(r))) {}
explicit parameter(rational && r) : m_kind(PARAM_RATIONAL), m_rational(alloc(rational, std::move(r))) {}
explicit parameter(zstring const& s): m_kind(PARAM_ZSTRING), m_zstring(alloc(zstring, s)) {}
explicit parameter(zstring && s): m_kind(PARAM_ZSTRING), m_zstring(alloc(zstring, std::move(s))) {}
explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {}
explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s)) {}
explicit parameter(const std::string &s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s)) {}
Expand All @@ -146,6 +151,7 @@ class parameter {
case PARAM_RATIONAL: m_rational = nullptr; std::swap(m_rational, other.m_rational); break;
case PARAM_DOUBLE: m_dval = other.m_dval; break;
case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break;
case PARAM_ZSTRING: m_zstring = other.m_zstring; break;
default:
UNREACHABLE();
break;
Expand All @@ -163,13 +169,15 @@ class parameter {
bool is_rational() const { return m_kind == PARAM_RATIONAL; }
bool is_double() const { return m_kind == PARAM_DOUBLE; }
bool is_external() const { return m_kind == PARAM_EXTERNAL; }
bool is_zstring() const { return m_kind == PARAM_ZSTRING; }

bool is_int(int & i) const { return is_int() && (i = get_int(), true); }
bool is_ast(ast * & a) const { return is_ast() && (a = get_ast(), true); }
bool is_symbol(symbol & s) const { return is_symbol() && (s = get_symbol(), true); }
bool is_rational(rational & r) const { return is_rational() && (r = get_rational(), true); }
bool is_double(double & d) const { return is_double() && (d = get_double(), true); }
bool is_external(unsigned & id) const { return is_external() && (id = get_ext_id(), true); }
bool is_zstring(zstring& s) const { return is_zstring() && (s = get_zstring(), true); }

/**
\brief This method is invoked when the parameter is
Expand All @@ -187,6 +195,7 @@ class parameter {
ast * get_ast() const { SASSERT(is_ast()); return m_ast; }
symbol get_symbol() const { SASSERT(is_symbol()); return m_symbol; }
rational const & get_rational() const { SASSERT(is_rational()); return *m_rational; }
zstring const& get_zstring() const { SASSERT(is_zstring()); return *m_zstring; }
double get_double() const { SASSERT(is_double()); return m_dval; }
unsigned get_ext_id() const { SASSERT(is_external()); return m_ext_id; }

Expand Down
2 changes: 1 addition & 1 deletion src/ast/rewriter/seq_axioms.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -682,7 +682,7 @@ namespace seq {
// itos(n) does not start with "0" when n > 0
// n = 0 or at(itos(n),0) != "0"
// alternative: n >= 0 => itos(stoi(itos(n))) = itos(n)
expr_ref zs(seq.str.mk_string(symbol("0")), m);
expr_ref zs(seq.str.mk_string("0"), m);
m_rewrite(zs);
expr_ref eq0 = mk_eq(n, zero);
expr_ref at0 = mk_eq(seq.str.mk_at(e, zero), zs);
Expand Down
8 changes: 4 additions & 4 deletions src/ast/rewriter/seq_rewriter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2159,7 +2159,7 @@ br_status seq_rewriter::mk_str_from_code(expr* a, expr_ref& result) {
rational r;
if (m_autil.is_numeral(a, r)) {
if (r.is_neg() || r > u().max_char()) {
result = str().mk_string(symbol(""));
result = str().mk_string(zstring());
}
else {
unsigned num = r.get_unsigned();
Expand Down Expand Up @@ -2207,10 +2207,10 @@ br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
rational r;
if (m_autil.is_numeral(a, r)) {
if (r.is_int() && !r.is_neg()) {
result = str().mk_string(symbol(r.to_string()));
result = str().mk_string(zstring(r));
}
else {
result = str().mk_string(symbol(""));
result = str().mk_string(zstring());
}
return BR_DONE;
}
Expand All @@ -2225,7 +2225,7 @@ br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
eqs.push_back(m().mk_eq(b, str().mk_string(s)));
}
result = m().mk_or(eqs);
result = m().mk_ite(result, b, str().mk_string(symbol("")));
result = m().mk_ite(result, b, str().mk_string(zstring()));
return BR_REWRITE2;
}
return BR_FAILED;
Expand Down
16 changes: 4 additions & 12 deletions src/ast/seq_decl_plugin.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -375,7 +375,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
case OP_SEQ_EMPTY:
match(*m_sigs[k], arity, domain, range, rng);
if (rng == m_string) {
parameter param(symbol(""));
parameter param(zstring(""));
return mk_func_decl(OP_STRING_CONST, 1, &param, 0, nullptr, m_string);
}
else {
Expand Down Expand Up @@ -474,7 +474,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
m.raise_exception("Incorrect arguments used for re.^. Expected one non-negative integer parameter");

case OP_STRING_CONST:
if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) {
if (!(num_parameters == 1 && arity == 0 && parameters[0].is_zstring())) {
m.raise_exception("invalid string declaration");
}
return m.mk_const_decl(m_stringc_sym, m_string,
Expand Down Expand Up @@ -630,16 +630,8 @@ void seq_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
sort_names.push_back(builtin_name("StringSequence", _STRING_SORT));
}

app* seq_decl_plugin::mk_string(symbol const& s) {
parameter param(s);
func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string,
func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
return m_manager->mk_const(f);
}

app* seq_decl_plugin::mk_string(zstring const& s) {
symbol sym(s.encode());
parameter param(sym);
parameter param(s);
func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string,
func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
return m_manager->mk_const(f);
Expand Down Expand Up @@ -792,7 +784,7 @@ app* seq_util::mk_lt(expr* ch1, expr* ch2) const {

bool seq_util::str::is_string(func_decl const* f, zstring& s) const {
if (is_string(f)) {
s = zstring(f->get_parameter(0).get_symbol().bare_str());
s = f->get_parameter(0).get_zstring();
return true;
}
else {
Expand Down
13 changes: 3 additions & 10 deletions src/ast/seq_decl_plugin.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,7 +191,6 @@ class seq_decl_plugin : public decl_plugin {
unsigned max_char() const { return get_char_plugin().max_char(); }
unsigned num_bits() const { return get_char_plugin().num_bits(); }

app* mk_string(symbol const& s);
app* mk_string(zstring const& s);
app* mk_char(unsigned ch);

Expand Down Expand Up @@ -262,9 +261,6 @@ class seq_util {
ast_manager& m;
family_id m_fid;

app* mk_string(char const* s) { return mk_string(symbol(s)); }
app* mk_string(std::string const& s) { return mk_string(symbol(s.c_str())); }


public:
str(seq_util& u): u(u), m(u.m), m_fid(u.m_fid) {}
Expand All @@ -273,7 +269,6 @@ class seq_util {
sort* mk_string_sort() const { return m.mk_sort(m_fid, _STRING_SORT, 0, nullptr); }
app* mk_empty(sort* s) const { return m.mk_const(m.mk_func_decl(m_fid, OP_SEQ_EMPTY, 0, nullptr, 0, (expr*const*)nullptr, s)); }
app* mk_string(zstring const& s) const;
app* mk_string(symbol const& s) const { return u.seq.mk_string(s); }
app* mk_char(unsigned ch) const;
app* mk_concat(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); }
app* mk_concat(expr* a, expr* b, expr* c) const { return mk_concat(a, mk_concat(b, c)); }
Expand Down Expand Up @@ -313,14 +308,12 @@ class seq_util {
bool is_skolem(func_decl const* f) const { return is_decl_of(f, m_fid, _OP_SEQ_SKOLEM); }

bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
bool is_string(expr const* n, symbol& s) const {
return is_string(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true);
}
bool is_string(func_decl const* f) const { return is_decl_of(f, m_fid, OP_STRING_CONST); }
bool is_string(expr const* n, zstring& s) const;
bool is_string(func_decl const* f, zstring& s) const;
bool is_empty(expr const* n) const { symbol s;
return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0);
bool is_empty(expr const* n) const {
zstring s;
return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && s.empty());
}
bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); }
bool is_length(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_LENGTH); }
Expand Down
14 changes: 8 additions & 6 deletions src/model/seq_factory.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,8 +67,8 @@ class seq_factory : public value_factory {
}
bool get_some_values(sort* s, expr_ref& v1, expr_ref& v2) override {
if (u.is_string(s)) {
v1 = u.str.mk_string(symbol("a"));
v2 = u.str.mk_string(symbol("b"));
v1 = u.str.mk_string("a");
v2 = u.str.mk_string("b");
return true;
}
sort* ch;
Expand All @@ -94,10 +94,11 @@ class seq_factory : public value_factory {
while (true) {
std::ostringstream strm;
strm << m_unique_delim << std::hex << m_next++ << std::dec << m_unique_delim;
symbol sym(strm.str());
std::string s(strm.str());
symbol sym(s);
if (m_strings.contains(sym)) continue;
m_strings.insert(sym);
return u.str.mk_string(sym);
return u.str.mk_string(s);
}
}
sort* seq = nullptr, *ch = nullptr;
Expand Down Expand Up @@ -131,8 +132,9 @@ class seq_factory : public value_factory {
return nullptr;
}
void register_value(expr* n) override {
symbol sym;
if (u.str.is_string(n, sym)) {
zstring s;
if (u.str.is_string(n, s)) {
symbol sym(s.encode());
m_strings.insert(sym);
if (sym.str().find(m_unique_delim) != std::string::npos)
add_new_delim();
Expand Down
2 changes: 1 addition & 1 deletion src/parsers/smt2/smt2parser.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1188,7 +1188,7 @@ namespace smt2 {

void parse_string_const() {
SASSERT(curr() == scanner::STRING_TOKEN);
zstring zs(m_scanner.get_string(), true);
zstring zs(m_scanner.get_string());
expr_stack().push_back(sutil().str.mk_string(zs));
TRACE("smt2parser", tout << "new string: " << mk_pp(expr_stack().back(), m()) << "\n";);
next();
Expand Down
3 changes: 1 addition & 2 deletions src/smt/theory_str.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -190,8 +190,7 @@ namespace smt {
}

expr * theory_str::mk_string(const char * str) {
symbol sym(str);
return u.str.mk_string(sym);
return u.str.mk_string(str);
}

void theory_str::collect_statistics(::statistics & st) const {
Expand Down
11 changes: 6 additions & 5 deletions src/smt/theory_str.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,22 +53,23 @@ class str_value_factory : public value_factory {
u(m), delim("!"), m_next(0) {}
~str_value_factory() override {}
expr * get_some_value(sort * s) override {
return u.str.mk_string(symbol("some value"));
return u.str.mk_string("some value");
}
bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override {
v1 = u.str.mk_string(symbol("value 1"));
v2 = u.str.mk_string(symbol("value 2"));
v1 = u.str.mk_string("value 1");
v2 = u.str.mk_string("value 2");
return true;
}
expr * get_fresh_value(sort * s) override {
if (u.is_string(s)) {
while (true) {
std::ostringstream strm;
strm << delim << std::hex << (m_next++) << std::dec << delim;
symbol sym(strm.str());
std::string s(strm.str());
symbol sym(s);
if (m_strings.contains(sym)) continue;
m_strings.insert(sym);
return u.str.mk_string(sym);
return u.str.mk_string(s);
}
}
sort* seq = nullptr;
Expand Down
20 changes: 8 additions & 12 deletions src/smt/theory_str_mc.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1337,9 +1337,8 @@ namespace smt {
rw(arg_subst);
TRACE("str_fl", tout << "ival = " << ival << ", string arg evaluates to " << mk_pp(arg_subst, m) << std::endl;);

symbol arg_str;
if (u.str.is_string(arg_subst, arg_str)) {
zstring arg_zstr(arg_str.bare_str());
zstring arg_zstr;
if (u.str.is_string(arg_subst, arg_zstr)) {
rational arg_value;
if (string_integer_conversion_valid(arg_zstr, arg_value)) {
if (ival != arg_value) {
Expand All @@ -1365,9 +1364,8 @@ namespace smt {
(*replacer)(arg, arg_subst);
rw(arg_subst);
TRACE("str_fl", tout << "ival = " << ival << ", string arg evaluates to " << mk_pp(arg_subst, m) << std::endl;);
symbol arg_str;
if (u.str.is_string(arg_subst, arg_str)) {
zstring arg_zstr(arg_str.bare_str());
zstring arg_zstr;
if (u.str.is_string(arg_subst, arg_zstr)) {
if (ival >= rational::zero() && ival <= rational(u.max_char())) {
// check that arg_subst has length 1 and that the codepoints are the same
if (arg_zstr.length() != 1 || rational(arg_zstr[0]) != ival) {
Expand Down Expand Up @@ -1396,9 +1394,8 @@ namespace smt {
rw(e_subst);
TRACE("str_fl", tout << "ival = " << ival << ", string arg evaluates to " << mk_pp(e_subst, m) << std::endl;);

symbol e_str;
if (u.str.is_string(e_subst, e_str)) {
zstring e_zstr(e_str.bare_str());
zstring e_zstr;
if (u.str.is_string(e_subst, e_zstr)) {
// if arg is negative, e must be empty
// if arg is non-negative, e must be valid AND cannot contain leading zeroes

Expand Down Expand Up @@ -1436,9 +1433,8 @@ namespace smt {
(*replacer)(e, e_subst);
rw(e_subst);
TRACE("str_fl", tout << "ival = " << ival << ", string arg evaluates to " << mk_pp(e_subst, m) << std::endl;);
symbol e_str;
if (u.str.is_string(e_subst, e_str)) {
zstring e_zstr(e_str.bare_str());
zstring e_zstr;
if (u.str.is_string(e_subst, e_zstr)) {
// if arg is out of range, e must be empty
// if arg is in range, e must be valid
if (ival <= rational::zero() || ival >= rational(u.max_char())) {
Expand Down
Loading

3 comments on commit 20a67e4

@nunoplopes
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm seeing a significant regression after this patch. The number of OOMs more than doubles.
The deal is.. I don't use the string theory. So why the heck is this happening? I thought it could be because of the implicit constructors, as they could be silently changing some parameters from symbols to zstrings, but I change zstring to have explicit constructors and still OOMs.. Rings any bell @NikolajBjorner?

git bisect says:

20a67e47caefc3caf1d4fef9612c5caf6a4fe611 is the first bad commit
commit 20a67e47caefc3caf1d4fef9612c5caf6a4fe611
Author: Nikolaj Bjorner <nbjorner@microsoft.com>
Date:   Sat May 22 13:12:49 2021 -0700

    remove symbol -> zstring -> symbol round-trips

    Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

 src/ast/ast.cpp                   |  7 +++++++
 src/ast/ast.h                     | 11 ++++++++++-
 src/ast/rewriter/seq_axioms.cpp   |  2 +-
 src/ast/rewriter/seq_rewriter.cpp |  8 ++++----
 src/ast/seq_decl_plugin.cpp       | 16 ++++------------
 src/ast/seq_decl_plugin.h         | 13 +++----------
 src/model/seq_factory.h           | 14 ++++++++------
 src/parsers/smt2/smt2parser.cpp   |  2 +-
 src/smt/theory_str.cpp            |  3 +--
 src/smt/theory_str.h              | 11 ++++++-----
 src/smt/theory_str_mc.cpp         | 20 ++++++++------------
 src/util/zstring.cpp              | 14 +++++++++-----
 src/util/zstring.h                |  9 ++++++---
 13 files changed, 68 insertions(+), 62 deletions(-)

@nunoplopes
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

oh, wait, it changed the hash for parameters, as ZSTRING was placed in the middle. Let me confirm that theory by moving it to end.

@nunoplopes
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

oh, wait, it changed the hash for parameters, as ZSTRING was placed in the middle. Let me confirm that theory by moving it to end.

That's it! The difference in the hash of parameters is the cause.
Should we just change the order of elements so we preserve the old hash function and call it a day?

Please sign in to comment.