From b37672a749fe0b4522158abf155566647cc69227 Mon Sep 17 00:00:00 2001
From: vhavlena <vohavlena@gmail.com>
Date: Thu, 2 Jan 2025 23:13:26 +0100
Subject: [PATCH] gather free length variables from quantified formulae

---
 .../theory_str_noodler/theory_str_noodler.cpp |  6 +---
 .../theory_str_noodler_final_check.cpp        |  5 ++++
 src/smt/theory_str_noodler/util.cc            | 28 +++++++++++--------
 src/smt/theory_str_noodler/util.h             |  2 +-
 4 files changed, 24 insertions(+), 17 deletions(-)

diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp
index 5711096dcc..25daa48520 100644
--- a/src/smt/theory_str_noodler/theory_str_noodler.cpp
+++ b/src/smt/theory_str_noodler/theory_str_noodler.cpp
@@ -140,11 +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;
-            // it seems Z3 is asserting formulae under quantification separately; 
-            // we can skip quantified formulae as the lenght variables were computed before.
-            if(!is_quantifier(ctx.get_asserted_formula(i))) {
-                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
index c9ebd50f17..e7a26c3493 100644
--- 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() && this->m_lang_eq_or_diseq_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
index d5a77947be..fe3a6d9024 100644
--- a/src/smt/theory_str_noodler/util.cc
+++ b/src/smt/theory_str_noodler/util.cc
@@ -118,21 +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++) {
-            // it seems Z3 is asserting formulae under quantification separately; 
-            // we can skip quantified formulae as the lenght variables were computed before.
-            if(is_quantifier(ex->get_arg(i))) {
-                return;
-            }
-            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
index 46bf36e46e..8b495a5d57 100644
--- 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.