Renamed MintermizationDomain to BDDDomain

examples/example06-mintermization.cc

@@ -31,7 +31,7 @@ int main(int argc, char *argv[]) {
 
         std::vector<mata::IntermediateAut> inter_auts = mata::IntermediateAut::parse_from_mf(parsed);
         for (const auto& ia : inter_auts) {
-            mata::Mintermization<mata::MintermizationDomain> mintermization;
+            mata::Mintermization<mata::BDDDomain> mintermization;
             std::cout << ia << '\n';
             if ((ia.is_nfa() || ia.is_afa()) && ia.alphabet_type == mata::IntermediateAut::AlphabetType::BITVECTOR) {
                 const auto& aut = mintermization.mintermize(ia);

include/mata/parser/mintermization-domain.hh → include/mata/parser/bdd-domain.hh

@@ -1,5 +1,5 @@
 /*
- * mintermization-domain.hh -- Mintermization domain for BDD.
+ * bdd-domain.hh -- Mintermization domain for BDD.
  *
  * This file is a part of libmata.
  *
@@ -21,40 +21,49 @@
 #include "mata/cudd/cuddObj.hh"
 
 namespace mata {
-    struct MintermizationDomain {
+    struct BDDDomain {
         Cudd bdd_mng; // Manager of BDDs from lib cubdd, it allocates and manages BDDs.
         BDD val;
 
-        MintermizationDomain() : bdd_mng(0), val(BDD()) {}
+        BDDDomain() : bdd_mng(0), val(BDD()) {}
 
-        MintermizationDomain(Cudd mng) : bdd_mng(mng), val(BDD()) {}
+        BDDDomain(Cudd mng) : bdd_mng(mng), val(BDD()) {}
 
-        MintermizationDomain(Cudd mng, BDD val) : bdd_mng(mng), val(val) {};
+        BDDDomain(Cudd mng, BDD val) : bdd_mng(mng), val(val) {};
 
-        friend MintermizationDomain operator&&(const MintermizationDomain& lhs, const MintermizationDomain &rhs) {
+        friend BDDDomain operator&&(const BDDDomain& lhs, const BDDDomain &rhs) {
             return {lhs.bdd_mng, lhs.val * rhs.val};
         }
 
-        friend MintermizationDomain operator||(const MintermizationDomain& lhs, const MintermizationDomain &rhs) {
+        friend BDDDomain operator||(const BDDDomain& lhs, const BDDDomain &rhs) {
             return {lhs.bdd_mng, lhs.val + rhs.val};
         }
 
-        friend MintermizationDomain operator!(const MintermizationDomain &lhs) {
+        friend BDDDomain operator!(const BDDDomain &lhs) {
             return {lhs.bdd_mng, !lhs.val};
         }
 
-        bool operator==(const MintermizationDomain &rhs) const {
+        bool operator==(const BDDDomain &rhs) const {
             return this->val == rhs.val;
         }
 
         bool isFalse() const {
             return val.IsZero();
         }
 
-        MintermizationDomain getTrue() const;
-        MintermizationDomain getFalse() const;
-        MintermizationDomain getVar() const;
+        BDDDomain getTrue() const;
+        BDDDomain getFalse() const;
+        BDDDomain getVar() const;
     };
 }
 
-#endif //LIBMATA_MINTERMIZATION_DOMAIN_HH
+namespace std {
+    template<>
+    struct hash<struct mata::BDDDomain> {
+        size_t operator()(const struct mata::BDDDomain &algebra) const noexcept {
+            return hash<BDD>{}(algebra.val);
+        }
+    };
+}
+
+#endif //LIBMATA_BDD_DOMAIN_HH

include/mata/parser/mintermization.hh

@@ -18,17 +18,7 @@
 #define MATA_MINTERM_HH
 
 #include "inter-aut.hh"
-#include "mintermization-domain.hh"
-
-// custom specialization of std::hash can be injected in namespace std
-namespace std {
-    template<>
-    struct hash<struct mata::MintermizationDomain> {
-        size_t operator()(const struct mata::MintermizationDomain &algebra) const noexcept {
-            return hash<BDD>{}(algebra.val);
-        }
-    };
-}
+#include "bdd-domain.hh"
 
 namespace mata {
 

src/CMakeLists.txt

@@ -7,7 +7,7 @@ add_library(libmata STATIC
 	"${CMAKE_CURRENT_BINARY_DIR}/config.cc"
 	inter-aut.cc
 	mintermization.cc
-	mintermization-domain.cc
+	bdd-domain.cc
 	parser.cc
 	re2parser.cc
 	nfa/nfa.cc
@@ -24,6 +24,8 @@ add_library(libmata STATIC
 	nfa/builder.cc
 )
 
+SET(CMAKE_BUILD_TYPE Debug)
+
 # libmata needs at least c++20
 target_compile_features(libmata PUBLIC cxx_std_20)
 

src/mintermization-domain.cc → src/bdd-domain.cc

@@ -1,5 +1,5 @@
 /*
- * mintermization-domain.cc -- Mintermization domain for BDD.
+ * bdd-domain.cc -- Mintermization domain for BDD.
  *
  * This file is a part of libmata.
  *
@@ -14,16 +14,16 @@
  * GNU General Public License for more details.
  */
 
-#include "mata/parser/mintermization-domain.hh"
+#include "mata/parser/bdd-domain.hh"
 
-struct mata::MintermizationDomain mata::MintermizationDomain::getTrue() const {
-    return MintermizationDomain(bdd_mng, bdd_mng.bddOne());
+struct mata::BDDDomain mata::BDDDomain::getTrue() const {
+    return BDDDomain(bdd_mng, bdd_mng.bddOne());
 }
 
-struct mata::MintermizationDomain mata::MintermizationDomain::getFalse() const {
-    return MintermizationDomain(bdd_mng, bdd_mng.bddZero());
+struct mata::BDDDomain mata::BDDDomain::getFalse() const {
+    return BDDDomain(bdd_mng, bdd_mng.bddZero());
 }
 
-struct mata::MintermizationDomain mata::MintermizationDomain::getVar() const {
-    return MintermizationDomain(bdd_mng, bdd_mng.bddVar());
+struct mata::BDDDomain mata::BDDDomain::getVar() const {
+    return BDDDomain(bdd_mng, bdd_mng.bddVar());
 }

src/mintermization.cc

@@ -19,8 +19,6 @@
 
 #include <vector>
 
-using MintermizationDomain = struct mata::MintermizationDomain;
-
 namespace {
     const mata::FormulaGraph* detect_state_part(const mata::FormulaGraph* node)
     {

tests-integration/src/utils/utils.cc

@@ -20,7 +20,7 @@ int load_automaton(
         if (!mintermize_automata or inter_auts[0].alphabet_type != mata::IntermediateAut::AlphabetType::BITVECTOR) {
             aut = mata::nfa::builder::construct(inter_auts[0], &alphabet);
         } else {
-            mata::Mintermization<mata::MintermizationDomain> mintermization;
+            mata::Mintermization<mata::BDDDomain> mintermization;
             TIME_BEGIN(mintermization);
             mata::IntermediateAut mintermized = mintermization.mintermize(inter_auts[0]);
             TIME_END(mintermization);
@@ -57,7 +57,7 @@ int load_automata(
                 auts.push_back(mata::nfa::builder::construct(inter_aut, &alphabet));
             }
         } else {
-            mata::Mintermization<mata::MintermizationDomain> mintermization;
+            mata::Mintermization<mata::BDDDomain> mintermization;
             TIME_BEGIN(mintermization);
             std::vector<mata::IntermediateAut> mintermized = mintermization.mintermize(inter_auts);
             TIME_END(mintermization);

tests/CMakeLists.txt

@@ -19,6 +19,8 @@ add_executable(tests
 		strings/nfa-string-solving.cc
 )
 
+SET(CMAKE_BUILD_TYPE Debug)
+
 target_link_libraries(tests PRIVATE libmata Catch2::Catch2)
 
 # Add common compile warnings.

tests/mintermization.cc

@@ -19,14 +19,14 @@
 
 #include "mata/parser/inter-aut.hh"
 #include "mata/parser/mintermization.hh"
-#include "mata/parser/mintermization-domain.hh"
+#include "mata/parser/bdd-domain.hh"
 
 using namespace mata::parser;
 
 TEST_CASE("Mata::Mintermization::trans_to_vars_nfa")
 {
     Parsed parsed;
-    mata::Mintermization<mata::MintermizationDomain> mintermization{};
+    mata::Mintermization<mata::BDDDomain> mintermization{};
 
     SECTION("Empty trans")
     {
@@ -43,7 +43,7 @@ TEST_CASE("Mata::Mintermization::trans_to_vars_nfa")
         const auto& aut= auts[0];
         REQUIRE(aut.transitions[0].first.is_operand());
         REQUIRE(aut.transitions[0].second.children[0].node.is_operand());
-        const mata::MintermizationDomain alg = mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]);
+        const mata::BDDDomain alg = mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]);
         REQUIRE(alg.val.nodeCount() == 2);
     }
 
@@ -62,7 +62,7 @@ TEST_CASE("Mata::Mintermization::trans_to_vars_nfa")
         const auto& aut= auts[0];
         REQUIRE(aut.transitions[0].second.children[0].node.is_operator());
         REQUIRE(aut.transitions[0].second.children[1].node.is_operand());
-        const mata::MintermizationDomain alg  = mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]);
+        const mata::BDDDomain alg  = mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]);
         REQUIRE(alg.val.nodeCount() == 3);
     }
 
@@ -81,7 +81,7 @@ TEST_CASE("Mata::Mintermization::trans_to_vars_nfa")
         const auto& aut= auts[0];
         REQUIRE(aut.transitions[0].second.children[0].node.is_operator());
         REQUIRE(aut.transitions[0].second.children[1].node.is_operand());
-        const mata::MintermizationDomain alg = mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]);
+        const mata::BDDDomain alg = mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]);
         REQUIRE(alg.val.nodeCount() == 4);
         int inputs[] = {0,0,0,0};
         REQUIRE(alg.val.Eval(inputs).IsOne());
@@ -93,7 +93,7 @@ TEST_CASE("Mata::Mintermization::trans_to_vars_nfa")
 TEST_CASE("mata::Mintermization::compute_minterms")
 {
     Parsed parsed;
-    mata::Mintermization<mata::MintermizationDomain> mintermization{};
+    mata::Mintermization<mata::BDDDomain> mintermization{};
 
     SECTION("Minterm from trans no elimination")
     {
@@ -111,7 +111,7 @@ TEST_CASE("mata::Mintermization::compute_minterms")
         const auto& aut= auts[0];
         REQUIRE(aut.transitions[0].second.children[0].node.is_operator());
         REQUIRE(aut.transitions[0].second.children[1].node.is_operand());
-        std::unordered_set<mata::MintermizationDomain> vars;
+        std::unordered_set<mata::BDDDomain> vars;
         vars.insert(mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]));
         vars.insert(mintermization.graph_to_vars_nfa(aut.transitions[1].second.children[0]));
         auto res = mintermization.compute_minterms(vars);
@@ -134,7 +134,7 @@ TEST_CASE("mata::Mintermization::compute_minterms")
         const auto& aut= auts[0];
         REQUIRE(aut.transitions[0].second.children[0].node.is_operator());
         REQUIRE(aut.transitions[0].second.children[1].node.is_operand());
-        std::unordered_set<struct mata::MintermizationDomain> vars;
+        std::unordered_set<struct mata::BDDDomain> vars;
         vars.insert(mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]));
         vars.insert(mintermization.graph_to_vars_nfa(aut.transitions[1].second.children[0]));
         auto res = mintermization.compute_minterms(vars);
@@ -144,7 +144,7 @@ TEST_CASE("mata::Mintermization::compute_minterms")
 
 TEST_CASE("mata::Mintermization::mintermization") {
     Parsed parsed;
-    mata::Mintermization<mata::MintermizationDomain> mintermization{};
+    mata::Mintermization<mata::BDDDomain> mintermization{};
 
     SECTION("Mintermization small") {
         std::string file =
@@ -202,7 +202,7 @@ TEST_CASE("mata::Mintermization::mintermization") {
 
     SECTION("Mintermization NFA multiple") {
         Parsed parsed;
-        mata::Mintermization<mata::MintermizationDomain> mintermization{};
+        mata::Mintermization<mata::BDDDomain> mintermization{};
 
         std::string file =
                 "@NFA-bits\n"