diff --git a/examples/example06-mintermization.cc b/examples/example06-mintermization.cc index 519d4d7f..98509c0a 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/bdd-domain.hh b/include/mata/parser/bdd-domain.hh new file mode 100644 index 00000000..fba4ff18 --- /dev/null +++ b/include/mata/parser/bdd-domain.hh @@ -0,0 +1,69 @@ +/* + * bdd-domain.hh -- Mintermization domain for BDD. + * + * This file is a part of libmata. + * + * This program is free software; you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation; either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + */ + + +#ifndef MATA_BDD_DOMAIN_HH +#define MATA_BDD_DOMAIN_HH + +#include "mata/cudd/cuddObj.hh" + +namespace mata { + struct BDDDomain { + Cudd bdd_mng; // Manager of BDDs from lib cubdd, it allocates and manages BDDs. + BDD val; + + BDDDomain() : bdd_mng(0), val(BDD()) {} + + BDDDomain(Cudd mng) : bdd_mng(mng), val(BDD()) {} + + BDDDomain(Cudd mng, BDD val) : bdd_mng(mng), val(val) {}; + + friend BDDDomain operator&&(const BDDDomain& lhs, const BDDDomain &rhs) { + return {lhs.bdd_mng, lhs.val * rhs.val}; + } + + friend BDDDomain operator||(const BDDDomain& lhs, const BDDDomain &rhs) { + return {lhs.bdd_mng, lhs.val + rhs.val}; + } + + friend BDDDomain operator!(const BDDDomain &lhs) { + return {lhs.bdd_mng, !lhs.val}; + } + + bool operator==(const BDDDomain &rhs) const { + return this->val == rhs.val; + } + + bool isFalse() const { + return val.IsZero(); + } + + BDDDomain get_true() const; + BDDDomain get_false() const; + BDDDomain get_var() const; + }; +} + +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 651f0324..f75e1235 100644 --- a/include/mata/parser/mintermization.hh +++ b/include/mata/parser/mintermization.hh @@ -17,67 +17,122 @@ #ifndef MATA_MINTERM_HH #define MATA_MINTERM_HH -#include "mata/cudd/cuddObj.hh" - #include "inter-aut.hh" +#include "bdd-domain.hh" namespace mata { +/** + * Class implements algorithms for mintermization of NFA. The mintermization works in the following way. + * It computes for each transition corresponding value in mintermization domain, than it computes minterms + * from the of these values and finally use this miterms to create the mintermized NFA. + * @tparam MintermizationDomain Domain of mintermization values. It should provide the following operations: a) logical + * conjuction (&&), disjunction (||), and negation (!); b) return the constants represnting TRUE or FALSE, c) create a + * new symbolic variable in the domain (eg., the BDD domain returns BDD (which is later used to represent symbol of NFA). + */ +template class Mintermization { private: // data types - struct OptionalBdd { - enum class TYPE {NOTHING_E, BDD_E}; - - TYPE type{}; - BDD val{}; - - OptionalBdd() = default; - explicit OptionalBdd(TYPE t) : type(t) {} - explicit OptionalBdd(const BDD& bdd) : type(TYPE::BDD_E), val(bdd) {} - OptionalBdd(TYPE t, const BDD& bdd) : type(t), val(bdd) {} - - OptionalBdd operator*(const OptionalBdd& b) const; - OptionalBdd operator+(const OptionalBdd& b) const; - OptionalBdd operator!() const; - }; - using DisjunctStatesPair = std::pair; private: // private data members - Cudd bdd_mng{}; // Manager of BDDs from lib cubdd, it allocates and manages BDDs. - std::unordered_map symbol_to_bddvar{}; - std::unordered_map trans_to_bddvar{}; - std::unordered_map> lhs_to_disjuncts_and_states{}; - std::unordered_set bdds{}; // bdds created from transitions + MintermizationDomain domain_base; + std::unordered_map symbol_to_var{}; + std::unordered_map trans_to_var{}; + + void trans_to_vars_nfa(const IntermediateAut &aut) + { + assert(aut.is_nfa()); + + for (const auto& trans : aut.transitions) { + // Foreach transition create a MintermizationDomain + const auto& symbol_part = aut.get_symbol_part_of_transition(trans); + assert((symbol_part.node.is_operator() || symbol_part.children.empty()) && + "Symbol part must be either formula or single symbol"); + const MintermizationDomain val = graph_to_vars_nfa(symbol_part); + if (val.isFalse()) + continue; + vars.insert(val); + trans_to_var.insert(std::make_pair(&symbol_part, val)); + } + } -private: - void trans_to_bdd_nfa(const IntermediateAut& aut); - void trans_to_bdd_afa(const IntermediateAut& aut); + std::unordered_map> lhs_to_disjuncts_and_states{}; + std::unordered_set vars{}; // vars created from transitions public: /** - * Takes a set of BDDs and build a minterm tree over it. - * The leaves of BDDs, which are minterms of input set, are returned - * @param source_bdds BDDs for which minterms are computed + * Takes a set of domain values and build a minterm tree over it. + * The leaves of domain values, which are minterms of input set, are returned + * @param domain_values domain values for which minterms are computed * @return Computed minterms */ - std::unordered_set compute_minterms(const std::unordered_set& source_bdds); + std::unordered_set compute_minterms( + const std::unordered_set& domain_values) + { + std::unordered_set stack{ domain_base.get_true() }; + for (const MintermizationDomain& b: domain_values) { + std::unordered_set next; + /** + * TODO: Possible optimization - we can remember which transition belongs to the currently processed vars + * and mintermize automaton somehow directly here. However, it would be better to do such optimization + * in copy of this function and this one keep clean and straightforward. + */ + for (const auto& minterm : stack) { + MintermizationDomain b1 = minterm && b; + if (!b1.isFalse()) { + next.insert(b1); + } + MintermizationDomain b0 = minterm && !b; + if (!b0.isFalse()) { + next.insert(b0); + } + } + stack = next; + } + + return stack; + } /** * Transforms a graph representing formula at transition to bdd. * @param graph Graph to be transformed * @return Resulting BDD */ - BDD graph_to_bdd_nfa(const FormulaGraph& graph); - - /** - * Transforms a graph representing formula at transition to bdd. - * This version of method is a more general one and accepts also - * formula including states. - * @param graph Graph to be transformed - * @return Resulting BDD - */ - OptionalBdd graph_to_bdd_afa(const FormulaGraph& graph); + MintermizationDomain graph_to_vars_nfa(const FormulaGraph& graph) { + const FormulaNode& node = graph.node; + + if (node.is_operand()) { + if (symbol_to_var.count(node.name)) { + return symbol_to_var.at(node.name); + } else { + MintermizationDomain res = (node.is_true()) ? domain_base.get_true() : + (node.is_false() ? domain_base.get_false() : + domain_base.get_var()); + symbol_to_var.insert(std::make_pair(node.name, res)); + return res; + } + } else if (node.is_operator()) { + if (node.operator_type == FormulaNode::OperatorType::AND) { + assert(graph.children.size() == 2); + const MintermizationDomain op1 = graph_to_vars_nfa(graph.children[0]); + const MintermizationDomain op2 = graph_to_vars_nfa(graph.children[1]); + return op1 && op2; + } else if (node.operator_type == FormulaNode::OperatorType::OR) { + assert(graph.children.size() == 2); + const MintermizationDomain op1 = graph_to_vars_nfa(graph.children[0]); + const MintermizationDomain op2 = graph_to_vars_nfa(graph.children[1]); + return op1 || op2; + } else if (node.operator_type == FormulaNode::OperatorType::NEG) { + assert(graph.children.size() == 1); + const MintermizationDomain op1 = graph_to_vars_nfa(graph.children[0]); + return !op1; + } else + assert(false); + } + + assert(false); + } /** * Method mintermizes given automaton which has bitvector alphabet. @@ -86,7 +141,9 @@ public: * @param aut Automaton to be mintermized. * @return Mintermized automaton */ - mata::IntermediateAut mintermize(const mata::IntermediateAut& aut); + mata::IntermediateAut mintermize(const mata::IntermediateAut& aut) { + return mintermize(std::vector{&aut}).front(); + } /** * Methods mintermize given automata which have bitvector alphabet. @@ -95,8 +152,39 @@ public: * @param auts Automata to be mintermized. * @return Mintermized automata corresponding to the input autamata */ - std::vector mintermize(const std::vector &auts); - std::vector mintermize(const std::vector &auts); + std::vector mintermize(const std::vector &auts) { + std::vector auts_pointers; + for (const mata::IntermediateAut &aut : auts) { + auts_pointers.push_back(&aut); + } + return mintermize(auts_pointers); + } + + std::vector mintermize(const std::vector &auts) { + for (const mata::IntermediateAut *aut : auts) { + if (!aut->is_nfa() || aut->alphabet_type != IntermediateAut::AlphabetType::BITVECTOR) { + throw std::runtime_error("We currently support mintermization only for NFA and AFA with bitvectors"); + } + + trans_to_vars_nfa(*aut); + } + + // Build minterm tree over MintermizationDomains + auto minterms = compute_minterms(vars); + + std::vector res; + for (const mata::IntermediateAut *aut : auts) { + IntermediateAut mintermized_aut = *aut; + mintermized_aut.alphabet_type = IntermediateAut::AlphabetType::EXPLICIT; + mintermized_aut.transitions.clear(); + + minterms_to_aut_nfa(mintermized_aut, *aut, minterms); + + res.push_back(mintermized_aut); + } + + return res; + } /** * The method performs the mintermization over @aut with given @minterms. @@ -106,20 +194,32 @@ public: * @param minterms Set of minterms for mintermization */ void minterms_to_aut_nfa(mata::IntermediateAut& res, const mata::IntermediateAut& aut, - const std::unordered_set& minterms); - - /** - * The method for mintermization of alternating finite automaton using - * a given set of minterms - * @param res The resulting mintermized automaton - * @param aut Automaton to be mintermized - * @param minterms Set of minterms for mintermization - */ - void minterms_to_aut_afa(mata::IntermediateAut& res, const mata::IntermediateAut& aut, - const std::unordered_set& minterms); - - Mintermization() : bdd_mng(0), symbol_to_bddvar{}, trans_to_bddvar() {} + const std::unordered_set& minterms) + { + for (const auto& trans : aut.transitions) { + // for each t=(q1,s,q2) + const auto &symbol_part = trans.second.children[0]; + + size_t symbol = 0; + if(trans_to_var.count(&symbol_part) == 0) + continue; // Transition had zero var so it was not added to map + const MintermizationDomain &var = trans_to_var.at(&symbol_part); + + for (const auto &minterm: minterms) { + // for each minterm x: + if (!((var && minterm).isFalse())) { + // if for symbol s of t is MintermizationDomain_s < x + // add q1,x,q2 to transitions + IntermediateAut::parse_transition(res, {trans.first.raw, std::to_string(symbol), + trans.second.children[1].node.raw}); + } + ++symbol; + } + } + } + + Mintermization() : domain_base(), symbol_to_var{}, trans_to_var() { + } }; // class Mintermization. - } // namespace mata #endif //MATA_MINTERM_HH diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c3b5bbea..9b666d40 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -7,6 +7,7 @@ add_library(libmata STATIC "${CMAKE_CURRENT_BINARY_DIR}/config.cc" inter-aut.cc mintermization.cc + bdd-domain.cc parser.cc re2parser.cc nfa/nfa.cc diff --git a/src/bdd-domain.cc b/src/bdd-domain.cc new file mode 100644 index 00000000..d9e51a41 --- /dev/null +++ b/src/bdd-domain.cc @@ -0,0 +1,29 @@ +/* + * bdd-domain.cc -- Mintermization domain for BDD. + * + * This file is a part of libmata. + * + * This program is free software; you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation; either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + */ + +#include "mata/parser/bdd-domain.hh" + +struct mata::BDDDomain mata::BDDDomain::get_true() const { + return BDDDomain(bdd_mng, bdd_mng.bddOne()); +} + +struct mata::BDDDomain mata::BDDDomain::get_false() const { + return BDDDomain(bdd_mng, bdd_mng.bddZero()); +} + +struct mata::BDDDomain mata::BDDDomain::get_var() const { + return BDDDomain(bdd_mng, bdd_mng.bddVar()); +} diff --git a/src/mintermization.cc b/src/mintermization.cc index f2923598..854004a5 100644 --- a/src/mintermization.cc +++ b/src/mintermization.cc @@ -54,294 +54,3 @@ namespace { } } -void mata::Mintermization::trans_to_bdd_nfa(const IntermediateAut &aut) -{ - assert(aut.is_nfa()); - - for (const auto& trans : aut.transitions) { - // Foreach transition create a BDD - const auto& symbol_part = aut.get_symbol_part_of_transition(trans); - assert((symbol_part.node.is_operator() || symbol_part.children.empty()) && - "Symbol part must be either formula or single symbol"); - const BDD bdd = graph_to_bdd_nfa(symbol_part); - if (bdd.IsZero()) - continue; - bdds.insert(bdd); - trans_to_bddvar[&symbol_part] = bdd; - } -} - -void mata::Mintermization::trans_to_bdd_afa(const IntermediateAut &aut) -{ - assert(aut.is_afa()); - - for (const auto& trans : aut.transitions) { - lhs_to_disjuncts_and_states[&trans.first] = std::vector(); - if (trans.second.node.is_state()) { // node from state to state - lhs_to_disjuncts_and_states[&trans.first].emplace_back(&trans.second, &trans.second); - } - // split transition to disjuncts - const FormulaGraph *act_graph = &trans.second; - - if (!trans.second.node.is_state() && act_graph->node.is_operator() && act_graph->node.operator_type != FormulaNode::OperatorType::OR) // there are no disjuncts - lhs_to_disjuncts_and_states[&trans.first].emplace_back(act_graph, detect_state_part( - act_graph)); - else if (!trans.second.node.is_state()) { - while (act_graph->node.is_operator() && act_graph->node.operator_type == FormulaNode::OperatorType::OR) { - // map lhs to disjunct and its state formula. The content of disjunct is right son of actual graph - // since the left one is a rest of formula - lhs_to_disjuncts_and_states[&trans.first].emplace_back(&act_graph->children[1], - detect_state_part( - &act_graph->children[1])); - act_graph = &(act_graph->children.front()); - } - - // take care of last disjunct - lhs_to_disjuncts_and_states[&trans.first].emplace_back(act_graph, - detect_state_part( - act_graph)); - } - - // Foreach disjunct create a BDD - for (const DisjunctStatesPair& ds_pair : lhs_to_disjuncts_and_states[&trans.first]) { - // create bdd for the whole disjunct - const auto bdd = (ds_pair.first == ds_pair.second) ? // disjunct contains only states - OptionalBdd(bdd_mng.bddOne()) : // transition from state to states -> add true as symbol - graph_to_bdd_afa(*ds_pair.first); - assert(bdd.type == OptionalBdd::TYPE::BDD_E); - if (bdd.val.IsZero()) - continue; - trans_to_bddvar[ds_pair.first] = bdd.val; - bdds.insert(bdd.val); - } - } -} - -std::unordered_set mata::Mintermization::compute_minterms(const std::unordered_set& source_bdds) -{ - std::unordered_set stack{ bdd_mng.bddOne() }; - for (const BDD& b: source_bdds) { - std::unordered_set next; - /** - * TODO: Possible optimization - we can remember which transition belongs to the currently processed bdds - * and mintermize automaton somehow directly here. However, it would be better to do such optimization - * in copy of this function and this one keep clean and straightforward. - */ - for (const auto& minterm : stack) { - BDD b1 = minterm * b; - if (!b1.IsZero()) { - next.insert(b1); - } - BDD b0 = minterm * !b; - if (!b0.IsZero()) { - next.insert(b0); - } - } - stack = next; - } - - return stack; -} - -mata::Mintermization::OptionalBdd mata::Mintermization::graph_to_bdd_afa(const FormulaGraph &graph) -{ - const FormulaNode& node = graph.node; - - if (node.is_operand()) { - if (node.is_state()) - return OptionalBdd(OptionalBdd::TYPE::NOTHING_E); - if (symbol_to_bddvar.count(node.name)) { - return OptionalBdd(symbol_to_bddvar.at(node.name)); - } else { - BDD res = (node.is_true()) ? bdd_mng.bddOne() : - (node.is_false() ? bdd_mng.bddZero() : bdd_mng.bddVar()); - symbol_to_bddvar[node.name] = res; - return OptionalBdd(res); - } - } else if (node.is_operator()) { - if (node.operator_type == FormulaNode::OperatorType::AND) { - assert(graph.children.size() == 2); - const OptionalBdd op1 = graph_to_bdd_afa(graph.children[0]); - const OptionalBdd op2 = graph_to_bdd_afa(graph.children[1]); - return op1 * op2; - } else if (node.operator_type == FormulaNode::OperatorType::OR) { - assert(graph.children.size() == 2); - const OptionalBdd op1 = graph_to_bdd_afa(graph.children[0]); - const OptionalBdd op2 = graph_to_bdd_afa(graph.children[1]); - return op1 + op2; - } else if (node.operator_type == FormulaNode::OperatorType::NEG) { - assert(graph.children.size() == 1); - const OptionalBdd op1 = graph_to_bdd_afa(graph.children[0]); - return !op1; - } else - assert(false && "Unknown type of operation. It should conjunction, disjunction, or negation."); - } - - assert(false); - return {}; -} - -BDD mata::Mintermization::graph_to_bdd_nfa(const FormulaGraph &graph) -{ - const FormulaNode& node = graph.node; - - if (node.is_operand()) { - if (symbol_to_bddvar.count(node.name)) { - return symbol_to_bddvar.at(node.name); - } else { - BDD res = (node.is_true()) ? bdd_mng.bddOne() : - (node.is_false() ? bdd_mng.bddZero() : bdd_mng.bddVar()); - symbol_to_bddvar[node.name] = res; - return res; - } - } else if (node.is_operator()) { - if (node.operator_type == FormulaNode::OperatorType::AND) { - assert(graph.children.size() == 2); - const BDD op1 = graph_to_bdd_nfa(graph.children[0]); - const BDD op2 = graph_to_bdd_nfa(graph.children[1]); - return op1 * op2; - } else if (node.operator_type == FormulaNode::OperatorType::OR) { - assert(graph.children.size() == 2); - const BDD op1 = graph_to_bdd_nfa(graph.children[0]); - const BDD op2 = graph_to_bdd_nfa(graph.children[1]); - return op1 + op2; - } else if (node.operator_type == FormulaNode::OperatorType::NEG) { - assert(graph.children.size() == 1); - const BDD op1 = graph_to_bdd_nfa(graph.children[0]); - return !op1; - } else - assert(false); - } - - assert(false); - return {}; -} - -void mata::Mintermization::minterms_to_aut_nfa(mata::IntermediateAut& res, const mata::IntermediateAut& aut, - const std::unordered_set& minterms) -{ - for (const auto& trans : aut.transitions) { - // for each t=(q1,s,q2) - const auto &symbol_part = trans.second.children[0]; - - size_t symbol = 0; - if(trans_to_bddvar.count(&symbol_part) == 0) - continue; // Transition had zero bdd so it was not added to map - const BDD &bdd = trans_to_bddvar[&symbol_part]; - - for (const auto &minterm: minterms) { - // for each minterm x: - if (!((bdd * minterm).IsZero())) { - // if for symbol s of t is BDD_s < x - // add q1,x,q2 to transitions - IntermediateAut::parse_transition(res, {trans.first.raw, std::to_string(symbol), - trans.second.children[1].node.raw}); - } - symbol++; - } - } -} - -void mata::Mintermization::minterms_to_aut_afa(mata::IntermediateAut& res, const mata::IntermediateAut& aut, - const std::unordered_set& minterms) -{ - for (const auto& trans : aut.transitions) { - for (const auto& ds_pair : lhs_to_disjuncts_and_states[&trans.first]) { - // for each t=(q1,s,q2) - const auto disjunct = ds_pair.first; - - if (!trans_to_bddvar.count(disjunct)) - continue; // Transition had zero bdd so it was not added to map - const BDD &bdd = trans_to_bddvar[disjunct]; - - size_t symbol = 0; - for (const auto &minterm: minterms) { - // for each minterm x: - if (!((bdd * minterm).IsZero())) { - // if for symbol s of t is BDD_s < x - // add q1,x,q2 to transitions - const auto str_symbol = std::to_string(symbol); - FormulaNode node_symbol(FormulaNode::Type::OPERAND, str_symbol, str_symbol, - mata::FormulaNode::OperandType::SYMBOL); - if (ds_pair.second != nullptr) - res.add_transition(trans.first, node_symbol, *ds_pair.second); - else // transition without state on the right handed side - res.add_transition(trans.first, node_symbol); - } - ++symbol; - } - } - } -} - -mata::IntermediateAut mata::Mintermization::mintermize(const mata::IntermediateAut& aut) { - return mintermize(std::vector { &aut})[0]; -} - -std::vector mata::Mintermization::mintermize(const std::vector &auts) -{ - for (const mata::IntermediateAut *aut : auts) { - if ((!aut->is_nfa() && !aut->is_afa()) || aut->alphabet_type != IntermediateAut::AlphabetType::BITVECTOR) { - throw std::runtime_error("We currently support mintermization only for NFA and AFA with bitvectors"); - } - - aut->is_nfa() ? trans_to_bdd_nfa(*aut) : trans_to_bdd_afa(*aut); - } - - // Build minterm tree over BDDs - auto minterms = compute_minterms(bdds); - - std::vector res; - for (const mata::IntermediateAut *aut : auts) { - IntermediateAut mintermized_aut = *aut; - mintermized_aut.alphabet_type = IntermediateAut::AlphabetType::EXPLICIT; - mintermized_aut.transitions.clear(); - - if (aut->is_nfa()) - minterms_to_aut_nfa(mintermized_aut, *aut, minterms); - else if (aut->is_afa()) - minterms_to_aut_afa(mintermized_aut, *aut, minterms); - - res.push_back(mintermized_aut); - } - - return res; -} - -std::vector mata::Mintermization::mintermize(const std::vector &auts) { - std::vector auts_pointers; - for (const mata::IntermediateAut &aut : auts) { - auts_pointers.push_back(&aut); - } - return mintermize(auts_pointers); -} - -mata::Mintermization::OptionalBdd mata::Mintermization::OptionalBdd::operator*( - const mata::Mintermization::OptionalBdd& b) const { - if (this->type == TYPE::NOTHING_E) { - return b; - } else if (b.type == TYPE::NOTHING_E) { - return *this; - } else { - return OptionalBdd{ TYPE::BDD_E, this->val * b.val }; - } -} - -mata::Mintermization::OptionalBdd mata::Mintermization::OptionalBdd::operator+( - const mata::Mintermization::OptionalBdd& b) const { - if (this->type == TYPE::NOTHING_E) { - return b; - } else if (b.type == TYPE::NOTHING_E) { - return *this; - } else { - return OptionalBdd{ TYPE::BDD_E, this->val + b.val }; - } -} - -mata::Mintermization::OptionalBdd mata::Mintermization::OptionalBdd::operator!() const { - if (this->type == TYPE::NOTHING_E) { - return OptionalBdd(TYPE::NOTHING_E); - } else { - return OptionalBdd{ TYPE::BDD_E, !this->val }; - } -} diff --git a/tests-integration/src/utils/utils.cc b/tests-integration/src/utils/utils.cc index e85f8fd4..86891656 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/mintermization.cc b/tests/mintermization.cc index c8dee29c..ee35666c 100644 --- a/tests/mintermization.cc +++ b/tests/mintermization.cc @@ -19,13 +19,14 @@ #include "mata/parser/inter-aut.hh" #include "mata/parser/mintermization.hh" +#include "mata/parser/bdd-domain.hh" using namespace mata::parser; -TEST_CASE("mata::Mintermization::trans_to_bdd_nfa") +TEST_CASE("mata::Mintermization::trans_to_vars_nfa") { Parsed parsed; - mata::Mintermization mintermization{}; + mata::Mintermization mintermization{}; SECTION("Empty trans") { @@ -42,8 +43,8 @@ TEST_CASE("mata::Mintermization::trans_to_bdd_nfa") const auto& aut= auts[0]; REQUIRE(aut.transitions[0].first.is_operand()); REQUIRE(aut.transitions[0].second.children[0].node.is_operand()); - const BDD bdd = mintermization.graph_to_bdd_nfa(aut.transitions[0].second.children[0]); - REQUIRE(bdd.nodeCount() == 2); + const mata::BDDDomain alg = mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]); + REQUIRE(alg.val.nodeCount() == 2); } SECTION("Small bitvector transition") @@ -61,8 +62,8 @@ TEST_CASE("mata::Mintermization::trans_to_bdd_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 BDD bdd = mintermization.graph_to_bdd_nfa(aut.transitions[0].second.children[0]); - REQUIRE(bdd.nodeCount() == 3); + const mata::BDDDomain alg = mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]); + REQUIRE(alg.val.nodeCount() == 3); } SECTION("Complex bitvector transition") @@ -80,19 +81,19 @@ TEST_CASE("mata::Mintermization::trans_to_bdd_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 BDD bdd = mintermization.graph_to_bdd_nfa(aut.transitions[0].second.children[0]); - REQUIRE(bdd.nodeCount() == 4); + 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(bdd.Eval(inputs).IsOne()); + REQUIRE(alg.val.Eval(inputs).IsOne()); int inputs_false[] = {0,1,0,0}; - REQUIRE(bdd.Eval(inputs_false).IsZero()); + REQUIRE(alg.val.Eval(inputs_false).IsZero()); } } // trans to bdd section TEST_CASE("mata::Mintermization::compute_minterms") { Parsed parsed; - mata::Mintermization mintermization{}; + mata::Mintermization mintermization{}; SECTION("Minterm from trans no elimination") { @@ -110,10 +111,10 @@ 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 bdds; - bdds.insert(mintermization.graph_to_bdd_nfa(aut.transitions[0].second.children[0])); - bdds.insert(mintermization.graph_to_bdd_nfa(aut.transitions[1].second.children[0])); - auto res = mintermization.compute_minterms(bdds); + 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); REQUIRE(res.size() == 4); } @@ -133,17 +134,17 @@ 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 bdds; - bdds.insert(mintermization.graph_to_bdd_nfa(aut.transitions[0].second.children[0])); - bdds.insert(mintermization.graph_to_bdd_nfa(aut.transitions[1].second.children[0])); - auto res = mintermization.compute_minterms(bdds); + 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); REQUIRE(res.size() == 3); } } // compute_minterms TEST_CASE("mata::Mintermization::mintermization") { Parsed parsed; - mata::Mintermization mintermization{}; + mata::Mintermization mintermization{}; SECTION("Mintermization small") { std::string file = @@ -201,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"