Merge pull request #207 from VeriFIT/fix-npm-test

Fixing JS binding tests
VeriFIT · Jan 4, 2025 · 44820d7 · 44820d7
2 parents b6435e5 + e4535f1
commit 44820d7
Show file tree

Hide file tree

Showing 5 changed files with 25 additions and 8 deletions.
diff --git a/src/api/js/src/high-level/high-level.test.ts b/src/api/js/src/high-level/high-level.test.ts
@@ -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 () => {

diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp
@@ -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);
             }

diff --git a/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp b/src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp
@@ -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() ) {
+            return FC_DONE;
+        }
+
         // 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.

diff --git a/src/smt/theory_str_noodler/util.cc b/src/smt/theory_str_noodler/util.cc
@@ -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;
+        }
+
         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);
         }
     }
 

diff --git a/src/smt/theory_str_noodler/util.h b/src/smt/theory_str_noodler/util.h
@@ -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.