Merge pull request #481 from VeriFIT/generalize_minimize

feat(python): Generalize minimization to allow setting an algorithm #patch
VeriFIT · Feb 4, 2025 · 03c5ee7 · 03c5ee7
2 parents 066b717 + 78c24da
commit 03c5ee7
Show file tree

Hide file tree

Showing 5 changed files with 23 additions and 6 deletions.
diff --git a/bindings/python/libmata/nfa/nfa.pxd b/bindings/python/libmata/nfa/nfa.pxd
@@ -204,7 +204,7 @@ cdef extern from "mata/nfa/plumbing.hh" namespace "mata::nfa::plumbing":
     cdef void c_complement "mata::nfa::plumbing::complement" (CNfa*, CNfa&, CAlphabet&, ParameterMap&) except +
     cdef void c_revert "mata::nfa::plumbing::revert" (CNfa*, CNfa&)
     cdef void c_remove_epsilon "mata::nfa::plumbing::remove_epsilon" (CNfa*, CNfa&, Symbol) except +
-    cdef void c_minimize "mata::nfa::plumbing::minimize" (CNfa*, CNfa&)
+    cdef void c_minimize "mata::nfa::plumbing::minimize" (CNfa*, CNfa&, ParameterMap&)
     cdef void c_reduce "mata::nfa::plumbing::reduce" (CNfa*, CNfa&, StateRenaming*, ParameterMap&)
 
 

diff --git a/bindings/python/libmata/nfa/nfa.pyx b/bindings/python/libmata/nfa/nfa.pyx
@@ -970,14 +970,23 @@ def remove_epsilon(Nfa lhs, Symbol epsilon = CEPSILON):
     mata_nfa.c_remove_epsilon(result.thisptr.get(), dereference(lhs.thisptr.get()), epsilon)
     return result
 
-def minimize(Nfa lhs):
+def minimize(Nfa lhs, params = None):
     """Minimizes the automaton lhs
 
     :param Nfa lhs: automaton to be minimized
+    :param Dict params: Additional parameters for the minimization operation:
+      - "algorithm":
+        - "brzozowski": The Brzozowski minimization algorithm.
+        - "hopcroft": The Hopcroft minimization algorithm, only works on trimmed (no useless states) DFAs as input.
     :return: minimized automaton
     """
+    params = params or {"algorithm": "brzozowski"}
     result = Nfa()
-    mata_nfa.c_minimize(result.thisptr.get(), dereference(lhs.thisptr.get()))
+    mata_nfa.c_minimize(result.thisptr.get(), dereference(lhs.thisptr.get()),
+        {
+            k.encode('utf-8'): v.encode('utf-8') for k, v in params.items()
+        }
+    )
     return result
 
 def reduce_with_state_map(Nfa aut, params = None):

diff --git a/bindings/python/tests/test_nfa.py b/bindings/python/tests/test_nfa.py
@@ -622,6 +622,10 @@ def test_minimize(
     minimized = mata_nfa.minimize(lhs)
     assert minimized.get_num_of_transitions() == 1
 
+    lhs.trim()
+    minimized_hopcroft = mata_nfa.minimize(lhs, {"algorithm": "hopcroft"})
+    assert minimized_hopcroft.get_num_of_transitions() == 1
+
 
 def test_to_dot():
     lhs = mata_nfa.Nfa()

diff --git a/include/mata/nfa/plumbing.hh b/include/mata/nfa/plumbing.hh
@@ -4,6 +4,8 @@
 #ifndef MATA_NFA_PLUMBING_HH_
 #define MATA_NFA_PLUMBING_HH_
 
+#include "mata/nfa/algorithms.hh"
+#include "mata/nfa/types.hh"
 #include "nfa.hh"
 #include "builder.hh"
 
@@ -35,8 +37,8 @@ inline void complement(
                                        { "minimize",  "false"}}) { *result = complement(aut, alphabet, params);
 }
 
-inline void minimize(Nfa* res, const Nfa &aut) { *res = minimize(aut); }
-
+inline void minimize(Nfa* res, const Nfa &aut, const ParameterMap& params = {{ "algorithm", "brzozowski"}}) { *res = minimize(aut, params); }
+ 
 inline void determinize(Nfa* result, const Nfa& aut, std::unordered_map<StateSet, State> *subset_map = nullptr) {
     *result = determinize(aut, subset_map);
 }

diff --git a/src/nfa/operations.cc b/src/nfa/operations.cc
@@ -942,7 +942,9 @@ Nfa mata::nfa::minimize(
 
     const std::string& str_algo = params.at("algorithm");
     if ("brzozowski" == str_algo) {  /* default */ }
-    else {
+    else if ("hopcroft" == str_algo) {
+        algo = algorithms::minimize_hopcroft;
+    } else {
         throw std::runtime_error(std::to_string(__func__) +
             " received an unknown value of the \"algorithm\" key: " + str_algo);
     }