Merge pull request #99 from VeriFIT/nielsen_first

Run nielsen before underapproximation
VeriFIT · Sep 23, 2023 · a0e3745 · a0e3745
2 parents 8eb505f + ca447c6
commit a0e3745
Showing 1 changed file with 9 additions and 6 deletions.
diff --git a/src/smt/theory_str_noodler/theory_str_noodler.cpp b/src/smt/theory_str_noodler/theory_str_noodler.cpp
@@ -885,12 +885,6 @@ namespace smt::noodler {
         // Get the initial length vars that are needed here (i.e they are in aut_assignment)
         std::unordered_set<BasicTerm> init_length_sensitive_vars{ get_init_length_vars(aut_assignment) };
 
-        // try underapproximation (if enabled) to solve
-        if(m_params.m_underapproximation && is_underapprox_suitable(instance, aut_assignment) && solve_underapprox(instance, aut_assignment, init_length_sensitive_vars, conversions) == l_true) {
-            STRACE("str", tout << "Sat from underapproximation" << std::endl;);
-            return FC_DONE;
-        }
-
         // try Nielsen transformation (if enabled) to solve
         if(m_params.m_try_nielsen && is_nielsen_suitable(instance)) {
             STRACE("str", tout << "Trying nielsen" << std::endl);
@@ -920,6 +914,15 @@ namespace smt::noodler {
             }
         }
 
+        // try underapproximation (if enabled) to solve
+        if(m_params.m_underapproximation && is_underapprox_suitable(instance, aut_assignment)) {
+            STRACE("str", tout << "Try underapproximation" << std::endl);
+            if (solve_underapprox(instance, aut_assignment, init_length_sensitive_vars, conversions) == l_true) {
+                STRACE("str", tout << "Sat from underapproximation" << std::endl;);
+                return FC_DONE;
+            }
+        }
+
         DecisionProcedure dec_proc = DecisionProcedure{ instance, aut_assignment, init_length_sensitive_vars, m_params, conversions };
 
         STRACE("str", tout << "Starting preprocessing" << std::endl);