From 8ce5282a6a8f77a4c0c78f28cc2859573f603993 Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Sat, 30 Sep 2023 21:52:37 +0200 Subject: [PATCH] Renamed MintermizationDomain to BDDDomain --- examples/example06-mintermization.cc | 2 +- ...mintermization-domain.hh => bdd-domain.hh} | 35 ++++++++++++------- include/mata/parser/mintermization.hh | 12 +------ src/CMakeLists.txt | 4 ++- ...mintermization-domain.cc => bdd-domain.cc} | 16 ++++----- src/mintermization.cc | 2 -- tests-integration/src/utils/utils.cc | 4 +-- tests/CMakeLists.txt | 2 ++ tests/mintermization.cc | 20 +++++------ 9 files changed, 49 insertions(+), 48 deletions(-) rename include/mata/parser/{mintermization-domain.hh => bdd-domain.hh} (55%) rename src/{mintermization-domain.cc => bdd-domain.cc} (51%) diff --git a/examples/example06-mintermization.cc b/examples/example06-mintermization.cc index b90c7c895..98509c0ad 100644 --- a/examples/example06-mintermization.cc +++ b/examples/example06-mintermization.cc @@ -31,7 +31,7 @@ int main(int argc, char *argv[]) { std::vector inter_auts = mata::IntermediateAut::parse_from_mf(parsed); for (const auto& ia : inter_auts) { - mata::Mintermization mintermization; + mata::Mintermization 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); diff --git a/include/mata/parser/mintermization-domain.hh b/include/mata/parser/bdd-domain.hh similarity index 55% rename from include/mata/parser/mintermization-domain.hh rename to include/mata/parser/bdd-domain.hh index 47c10b9cd..fde942fe3 100644 --- a/include/mata/parser/mintermization-domain.hh +++ b/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,29 +21,29 @@ #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; } @@ -51,10 +51,19 @@ namespace mata { 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 { + size_t operator()(const struct mata::BDDDomain &algebra) const noexcept { + return hash{}(algebra.val); + } + }; +} + +#endif //LIBMATA_BDD_DOMAIN_HH diff --git a/include/mata/parser/mintermization.hh b/include/mata/parser/mintermization.hh index 49a09e656..903c1671a 100644 --- a/include/mata/parser/mintermization.hh +++ b/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 { - size_t operator()(const struct mata::MintermizationDomain &algebra) const noexcept { - return hash{}(algebra.val); - } - }; -} +#include "bdd-domain.hh" namespace mata { diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 27a1cd85a..fd913e517 100644 --- a/src/CMakeLists.txt +++ b/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) diff --git a/src/mintermization-domain.cc b/src/bdd-domain.cc similarity index 51% rename from src/mintermization-domain.cc rename to src/bdd-domain.cc index ee7ef5ef1..910020d66 100644 --- a/src/mintermization-domain.cc +++ b/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()); } diff --git a/src/mintermization.cc b/src/mintermization.cc index f4ecf00a3..f11a7960f 100644 --- a/src/mintermization.cc +++ b/src/mintermization.cc @@ -19,8 +19,6 @@ #include -using MintermizationDomain = struct mata::MintermizationDomain; - namespace { const mata::FormulaGraph* detect_state_part(const mata::FormulaGraph* node) { diff --git a/tests-integration/src/utils/utils.cc b/tests-integration/src/utils/utils.cc index 86a5a58a4..868916564 100644 --- a/tests-integration/src/utils/utils.cc +++ b/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 mintermization; + mata::Mintermization 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 mintermization; + mata::Mintermization mintermization; TIME_BEGIN(mintermization); std::vector mintermized = mintermization.mintermize(inter_auts); TIME_END(mintermization); diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index c7a0a17e6..73c532c15 100644 --- a/tests/CMakeLists.txt +++ b/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. diff --git a/tests/mintermization.cc b/tests/mintermization.cc index aacea3aaa..121da2903 100644 --- a/tests/mintermization.cc +++ b/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 mintermization{}; + mata::Mintermization 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 mintermization{}; + mata::Mintermization 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 vars; + std::unordered_set 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 vars; + std::unordered_set 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 mintermization{}; + mata::Mintermization mintermization{}; SECTION("Mintermization small") { std::string file = @@ -202,7 +202,7 @@ TEST_CASE("mata::Mintermization::mintermization") { SECTION("Mintermization NFA multiple") { Parsed parsed; - mata::Mintermization mintermization{}; + mata::Mintermization mintermization{}; std::string file = "@NFA-bits\n"