Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fixing JS binding tests #207

Merged
merged 4 commits into from
Jan 4, 2025
Merged

Fixing JS binding tests #207

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
fd03518
get_len_expr: fixing asserts during quantifier handling
vhavlena Jan 2, 2025
61d142a
js-test: set model to true
vhavlena Jan 2, 2025
b37672a
gather free length variables from quantified formulae
vhavlena Jan 2, 2025
e4535f1
final_check: remove language equations check
vhavlena Jan 4, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions src/api/js/src/high-level/high-level.test.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,6 +101,7 @@ describe('high-level', () => {
resetParams();
expect(getParam('pp.decimal')).toStrictEqual('false');
expect(getParam('timeout')).toStrictEqual('4294967295');
setParam('model', true);
});

it('proves x = y implies g(x) = g(y)', async () => {
Expand Down
2 changes: 1 addition & 1 deletion src/smt/theory_str_noodler/theory_str_noodler.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -140,7 +140,7 @@ namespace smt::noodler {
for (unsigned i = 0; i < nFormulas; ++i) {
STRACE("str-init-formula", tout << "Initial asserted formula " << i << ": " << expr_ref(ctx.get_asserted_formula(i), m) << std::endl;);
obj_hashtable<app> lens;
util::get_len_exprs(to_app(ctx.get_asserted_formula(i)), m_util_s, m, lens);
util::get_len_exprs(ctx.get_asserted_formula(i), m_util_s, m, lens);
for (app* const a : lens) {
util::get_str_variables(a, this->m_util_s, m, this->len_vars, &this->predicate_replace);
}
Expand Down
5 changes: 5 additions & 0 deletions src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,11 @@ namespace smt::noodler {
bool contains_conversions = !this->m_conversion_todo.empty();
bool contains_eqs_and_diseqs_only = this->m_not_contains_todo_rel.empty() && this->m_conversion_todo.empty();

// nothing is trivially SAT
if(contains_eqs_and_diseqs_only && this->m_word_eq_todo_rel.empty() && this->m_word_diseq_todo_rel.empty() && this->m_membership_todo_rel.empty() && this->m_lang_eq_or_diseq_todo_rel.empty() ) {
return FC_DONE;
}
jurajsic marked this conversation as resolved.
Show resolved Hide resolved

// As a heuristic, for the case we have exactly one constraint, which is of type 'x (not)in RE', we use universality/emptiness
// checking of the regex (using some heuristics) instead of constructing the automaton of RE. The construction (especially complement)
// can sometimes blow up, so the check should be faster.
Expand Down
23 changes: 17 additions & 6 deletions src/smt/theory_str_noodler/util.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -118,16 +118,27 @@ namespace smt::noodler::util {
return BasicTerm{ BasicTermType::Variable, variable_app->get_decl()->get_name().str() };
}

void get_len_exprs(app* const ex, const seq_util& m_util_s, const ast_manager& m, obj_hashtable<app>& res) {
void get_len_exprs(expr* const ex, const seq_util& m_util_s, ast_manager& m, obj_hashtable<app>& res) {

if(is_quantifier(ex)) {
quantifier* qf = to_quantifier(ex);
get_len_exprs(qf->get_expr(), m_util_s, m, res);
return;
}
// quantified variable
if(is_var(ex)) {
return;
}
Comment on lines +128 to +131
Copy link
Member

Choose a reason for hiding this comment

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

Should we put some test that if ex is string variable, we throw error? So we do not accidentally handle some formula with string quantifiers incorrectly.

Copy link
Member

Choose a reason for hiding this comment

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

Hmm, now that I think about it, it will probably fail somewhere further in the solver if we get quantifiers, so it might not be needed.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

If there is a quantification over non-string variables (ints or whatever), it could be correct. For a quantification over string variables it likely fails somewhere else (we need to look at it properly at some point).


if(m_util_s.str.is_length(ex)) {
res.insert(ex);
res.insert(to_app(ex));
return;
}

for(unsigned i = 0; i < ex->get_num_args(); i++) {
SASSERT(is_app(ex->get_arg(i)));
app *arg = to_app(ex->get_arg(i));
get_len_exprs(arg, m_util_s, m, res);
SASSERT(is_app(ex));
app *ex_app = to_app(ex);
for(unsigned i = 0; i < ex_app->get_num_args(); i++) {
get_len_exprs(ex_app->get_arg(i), m_util_s, m, res);
}
}

Expand Down
2 changes: 1 addition & 1 deletion src/smt/theory_str_noodler/util.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ namespace smt::noodler::util {
*/
BasicTerm get_variable_basic_term(expr* variable);

void get_len_exprs(app* ex, const seq_util& m_util_s, const ast_manager& m, obj_hashtable<app>& res);
void get_len_exprs(expr* ex, const seq_util& m_util_s, ast_manager& m, obj_hashtable<app>& res);

/**
* @brief Create a fresh noodler (BasicTerm) variable with a given @p name followed by a unique suffix.
Expand Down
Loading