From 2df9bb16c089b5d86877199793f825665678ec12 Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Sun, 13 Aug 2023 17:18:59 +0200 Subject: [PATCH 01/18] Towards generalized mintermization --- include/mata/parser/mintermization.hh | 94 ++++++++++---- src/mintermization.cc | 169 ++++++++++++++------------ tests/mintermization.cc | 36 +++--- 3 files changed, 184 insertions(+), 115 deletions(-) diff --git a/include/mata/parser/mintermization.hh b/include/mata/parser/mintermization.hh index 805d47fd..fe4f630d 100644 --- a/include/mata/parser/mintermization.hh +++ b/include/mata/parser/mintermization.hh @@ -21,38 +21,86 @@ #include "inter-aut.hh" + namespace Mata { + struct MintermizationAlgebra { + static Cudd bdd_mng; // Manager of BDDs from lib cubdd, it allocates and manages BDDs. + BDD val; + + MintermizationAlgebra() { + this->val = BDD(); + } + + MintermizationAlgebra(BDD val) { + this->val = val; + } + + friend MintermizationAlgebra operator&&(const MintermizationAlgebra& lhs, const MintermizationAlgebra &rhs) { + return {lhs.val * rhs.val}; + } + + friend MintermizationAlgebra operator||(const MintermizationAlgebra& lhs, const MintermizationAlgebra &rhs) { + return {lhs.val + rhs.val}; + } + + friend MintermizationAlgebra operator!(const MintermizationAlgebra &lhs) { + return {!lhs.val}; + } + + bool operator==(const MintermizationAlgebra &rhs) const { + return this->val == rhs.val; + } + + bool isFalse() const { + return val.IsZero(); + } + + static MintermizationAlgebra getTrue(); + static MintermizationAlgebra getFalse(); + static MintermizationAlgebra getVar(); +}; +} + +// custom specialization of std::hash can be injected in namespace std +namespace std { + template<> + struct hash { + size_t operator()(const struct Mata::MintermizationAlgebra &algebra) const noexcept { + return hash{}(algebra.val); + } + }; +} +namespace Mata { class Mintermization { private: // data types - struct OptionalBdd { - enum class TYPE {NOTHING_E, BDD_E}; + struct OptionalValue { + enum class TYPE {NOTHING_E, VALUE_E}; TYPE type{}; - BDD val{}; + MintermizationAlgebra 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) {} + OptionalValue() = default; + explicit OptionalValue(TYPE t) : type(t) {} + explicit OptionalValue(const MintermizationAlgebra& algebra) : type(TYPE::VALUE_E), val(algebra) {} + OptionalValue(TYPE t, const MintermizationAlgebra& algebra) : type(t), val(algebra) {} - OptionalBdd operator*(const OptionalBdd& b) const; - OptionalBdd operator+(const OptionalBdd& b) const; - OptionalBdd operator!() const; + OptionalValue operator*(const OptionalValue& b) const; + OptionalValue operator+(const OptionalValue& b) const; + OptionalValue 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 symbol_to_var{}; + std::unordered_map trans_to_var{}; std::unordered_map> lhs_to_disjuncts_and_states{}; - std::unordered_set bdds{}; // bdds created from transitions + std::unordered_set vars{}; // vars created from transitions private: - void trans_to_bdd_nfa(const IntermediateAut& aut); - void trans_to_bdd_afa(const IntermediateAut& aut); + void trans_to_vars_nfa(const IntermediateAut& aut); + void trans_to_vars_afa(const IntermediateAut& aut); public: /** @@ -61,14 +109,15 @@ public: * @param source_bdds BDDs 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& source_bdds); /** * 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); + MintermizationAlgebra graph_to_vars_nfa(const FormulaGraph& graph); /** * Transforms a graph representing formula at transition to bdd. @@ -77,7 +126,7 @@ public: * @param graph Graph to be transformed * @return Resulting BDD */ - OptionalBdd graph_to_bdd_afa(const FormulaGraph& graph); + OptionalValue graph_to_vars_afa(const FormulaGraph& graph); /** * Method mintermizes given automaton which has bitvector alphabet. @@ -106,7 +155,7 @@ 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); + const std::unordered_set& minterms); /** * The method for mintermization of alternating finite automaton using @@ -116,10 +165,11 @@ public: * @param minterms Set of minterms for mintermization */ void minterms_to_aut_afa(Mata::IntermediateAut& res, const Mata::IntermediateAut& aut, - const std::unordered_set& minterms); + const std::unordered_set& minterms); - Mintermization() : bdd_mng(0), symbol_to_bddvar{}, trans_to_bddvar() {} + Mintermization() : symbol_to_var{}, trans_to_var() {} }; // class Mintermization. } // namespace Mata + #endif //MATA_MINTERM_HH diff --git a/src/mintermization.cc b/src/mintermization.cc index 5edac3cd..1d03b9d4 100644 --- a/src/mintermization.cc +++ b/src/mintermization.cc @@ -17,6 +17,10 @@ #include "mata/parser/mintermization.hh" +#include + +using MintermizationAlgebra = struct Mata::MintermizationAlgebra; + namespace { const Mata::FormulaGraph* detect_state_part(const Mata::FormulaGraph* node) { @@ -54,24 +58,38 @@ namespace { } } -void Mata::Mintermization::trans_to_bdd_nfa(const IntermediateAut &aut) +Cudd Mata::MintermizationAlgebra::bdd_mng = Cudd{}; + +struct Mata::MintermizationAlgebra Mata::MintermizationAlgebra::getTrue() { + return MintermizationAlgebra(MintermizationAlgebra::bdd_mng.bddOne()); +} + +struct Mata::MintermizationAlgebra Mata::MintermizationAlgebra::getFalse() { + return MintermizationAlgebra(MintermizationAlgebra::bdd_mng.bddZero()); +} + +struct Mata::MintermizationAlgebra Mata::MintermizationAlgebra::getVar() { + return MintermizationAlgebra(MintermizationAlgebra::bdd_mng.bddVar()); +} + +void Mata::Mintermization::trans_to_vars_nfa(const IntermediateAut &aut) { assert(aut.is_nfa()); for (const auto& trans : aut.transitions) { - // Foreach transition create a BDD + // Foreach transition create a MintermizationAlgebra 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()) + const MintermizationAlgebra val = graph_to_vars_nfa(symbol_part); + if (val.isFalse()) continue; - bdds.insert(bdd); - trans_to_bddvar[&symbol_part] = bdd; + vars.insert(val); + trans_to_var[&symbol_part] = val; } } -void Mata::Mintermization::trans_to_bdd_afa(const IntermediateAut &aut) +void Mata::Mintermization::trans_to_vars_afa(const IntermediateAut &aut) { assert(aut.is_afa()); @@ -102,38 +120,39 @@ void Mata::Mintermization::trans_to_bdd_afa(const IntermediateAut &aut) act_graph)); } - // Foreach disjunct create a BDD + // Foreach disjunct create a MintermizationAlgebra 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()) + // create val for the whole disjunct + const auto val = (ds_pair.first == ds_pair.second) ? // disjunct contains only states + OptionalValue(MintermizationAlgebra::getTrue()) : // transition from state to states -> add true as symbol + graph_to_vars_afa(*ds_pair.first); + assert(val.type == OptionalValue::TYPE::VALUE_E); + if (val.val.isFalse()) continue; - trans_to_bddvar[ds_pair.first] = bdd.val; - bdds.insert(bdd.val); + trans_to_var[ds_pair.first] = val.val; + vars.insert(val.val); } } } -std::unordered_set Mata::Mintermization::compute_minterms(const std::unordered_set& source_bdds) +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; + std::unordered_set stack{ MintermizationAlgebra::getTrue() }; + for (const MintermizationAlgebra& b: source_bdds) { + std::unordered_set next; /** - * TODO: Possible optimization - we can remember which transition belongs to the currently processed bdds + * 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) { - BDD b1 = minterm * b; - if (!b1.IsZero()) { + MintermizationAlgebra b1 = minterm && b; + if (!b1.isFalse()) { next.insert(b1); } - BDD b0 = minterm * !b; - if (!b0.IsZero()) { + MintermizationAlgebra b0 = minterm && !b; + if (!b0.isFalse()) { next.insert(b0); } } @@ -143,35 +162,35 @@ std::unordered_set Mata::Mintermization::compute_minterms(const std::unorde return stack; } -Mata::Mintermization::OptionalBdd Mata::Mintermization::graph_to_bdd_afa(const FormulaGraph &graph) +Mata::Mintermization::OptionalValue Mata::Mintermization::graph_to_vars_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)); + return OptionalValue(OptionalValue::TYPE::NOTHING_E); + if (symbol_to_var.count(node.name)) { + return OptionalValue(symbol_to_var.at(node.name)); } else { - BDD res = (node.name == "true") ? bdd_mng.bddOne() : - (node.name == "false" ? bdd_mng.bddZero() : bdd_mng.bddVar()); - symbol_to_bddvar[node.name] = res; - return OptionalBdd(res); + MintermizationAlgebra res = (node.name == "true") ? MintermizationAlgebra::getTrue() : + (node.name == "false" ? MintermizationAlgebra::getFalse() : MintermizationAlgebra::getVar()); + symbol_to_var[node.name] = res; + return OptionalValue(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]); + const OptionalValue op1 = graph_to_vars_afa(graph.children[0]); + const OptionalValue op2 = graph_to_vars_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]); + const OptionalValue op1 = graph_to_vars_afa(graph.children[0]); + const OptionalValue op2 = graph_to_vars_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]); + const OptionalValue op1 = graph_to_vars_afa(graph.children[0]); return !op1; } else assert(false && "Unknown type of operation. It should conjunction, disjunction, or negation."); @@ -181,33 +200,33 @@ Mata::Mintermization::OptionalBdd Mata::Mintermization::graph_to_bdd_afa(const F return {}; } -BDD Mata::Mintermization::graph_to_bdd_nfa(const FormulaGraph &graph) +MintermizationAlgebra Mata::Mintermization::graph_to_vars_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); + if (symbol_to_var.count(node.name)) { + return symbol_to_var.at(node.name); } else { - BDD res = (node.name == "true") ? bdd_mng.bddOne() : - (node.name == "false" ? bdd_mng.bddZero() : bdd_mng.bddVar()); - symbol_to_bddvar[node.name] = res; + MintermizationAlgebra res = (node.name == "true") ? MintermizationAlgebra::getTrue() : + (node.name == "false" ? MintermizationAlgebra::getFalse() : MintermizationAlgebra::getVar()); + symbol_to_var[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; + const MintermizationAlgebra op1 = graph_to_vars_nfa(graph.children[0]); + const MintermizationAlgebra 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 BDD op1 = graph_to_bdd_nfa(graph.children[0]); - const BDD op2 = graph_to_bdd_nfa(graph.children[1]); - return op1 + op2; + const MintermizationAlgebra op1 = graph_to_vars_nfa(graph.children[0]); + const MintermizationAlgebra 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 BDD op1 = graph_to_bdd_nfa(graph.children[0]); + const MintermizationAlgebra op1 = graph_to_vars_nfa(graph.children[0]); return !op1; } else assert(false); @@ -218,21 +237,21 @@ BDD Mata::Mintermization::graph_to_bdd_nfa(const FormulaGraph &graph) } void Mata::Mintermization::minterms_to_aut_nfa(Mata::IntermediateAut& res, const Mata::IntermediateAut& aut, - const std::unordered_set& minterms) + 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]; + if(trans_to_var.count(&symbol_part) == 0) + continue; // Transition had zero var so it was not added to map + const MintermizationAlgebra &var = trans_to_var[&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 + if (!((var && minterm).isFalse())) { + // if for symbol s of t is MintermizationAlgebra_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}); @@ -243,22 +262,22 @@ void Mata::Mintermization::minterms_to_aut_nfa(Mata::IntermediateAut& res, const } void Mata::Mintermization::minterms_to_aut_afa(Mata::IntermediateAut& res, const Mata::IntermediateAut& aut, - const std::unordered_set& minterms) + 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]; + if (!trans_to_var.count(disjunct)) + continue; // Transition had zero var so it was not added to map + const MintermizationAlgebra &var = trans_to_var[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 + if (!((var && minterm).isFalse())) { + // if for symbol s of t is MintermizationAlgebra_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, @@ -285,11 +304,11 @@ std::vector Mata::Mintermization::mintermize(const std::v 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); + aut->is_nfa() ? trans_to_vars_nfa(*aut) : trans_to_vars_afa(*aut); } - // Build minterm tree over BDDs - auto minterms = compute_minterms(bdds); + // Build minterm tree over MintermizationAlgebras + auto minterms = compute_minterms(vars); std::vector res; for (const Mata::IntermediateAut *aut : auts) { @@ -316,32 +335,32 @@ std::vector Mata::Mintermization::mintermize(const std::v return mintermize(auts_pointers); } -Mata::Mintermization::OptionalBdd Mata::Mintermization::OptionalBdd::operator*( - const Mata::Mintermization::OptionalBdd& b) const { +Mata::Mintermization::OptionalValue Mata::Mintermization::OptionalValue::operator*( + const Mata::Mintermization::OptionalValue& 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 }; + return OptionalValue{TYPE::VALUE_E, this->val && b.val }; } } -Mata::Mintermization::OptionalBdd Mata::Mintermization::OptionalBdd::operator+( - const Mata::Mintermization::OptionalBdd& b) const { +Mata::Mintermization::OptionalValue Mata::Mintermization::OptionalValue::operator+( + const Mata::Mintermization::OptionalValue& 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 }; + return OptionalValue{TYPE::VALUE_E, this->val || b.val }; } } -Mata::Mintermization::OptionalBdd Mata::Mintermization::OptionalBdd::operator!() const { +Mata::Mintermization::OptionalValue Mata::Mintermization::OptionalValue::operator!() const { if (this->type == TYPE::NOTHING_E) { - return OptionalBdd(TYPE::NOTHING_E); + return OptionalValue(TYPE::NOTHING_E); } else { - return OptionalBdd{ TYPE::BDD_E, !this->val }; + return OptionalValue{TYPE::VALUE_E, !this->val }; } } diff --git a/tests/mintermization.cc b/tests/mintermization.cc index 4fe483fb..e16abb6c 100644 --- a/tests/mintermization.cc +++ b/tests/mintermization.cc @@ -22,7 +22,7 @@ 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{}; @@ -42,8 +42,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::MintermizationAlgebra alg = mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]); + REQUIRE(alg.val.nodeCount() == 2); } SECTION("Small bitvector transition") @@ -61,8 +61,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::MintermizationAlgebra alg = mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]); + REQUIRE(alg.val.nodeCount() == 3); } SECTION("Complex bitvector transition") @@ -80,12 +80,12 @@ 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::MintermizationAlgebra 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 @@ -110,10 +110,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,10 +133,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() == 3); } } // compute_minterms @@ -485,7 +485,7 @@ TEST_CASE("Mata::Mintermization::mintermization") } } -TEST_CASE("Mata::Mintermization::trans_to_bdd_nfa with big AFA","[.expensive]") +TEST_CASE("Mata::Mintermization::trans_to_vars_nfa with big AFA","[.expensive]") { Parsed parsed; From b6cfacb7a9d3f2dda9a7435fa84cee259c1f18c4 Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Fri, 8 Sep 2023 23:50:48 +0200 Subject: [PATCH 02/18] mintermization is ugly but working, needs to find out what to do with the bloody bdd manager --- include/mata/parser/mintermization.hh | 31 +++++++++---------- src/mintermization.cc | 43 ++++++++++++++------------- 2 files changed, 38 insertions(+), 36 deletions(-) diff --git a/include/mata/parser/mintermization.hh b/include/mata/parser/mintermization.hh index fe4f630d..1f11aa36 100644 --- a/include/mata/parser/mintermization.hh +++ b/include/mata/parser/mintermization.hh @@ -24,27 +24,25 @@ namespace Mata { struct MintermizationAlgebra { - static Cudd bdd_mng; // Manager of BDDs from lib cubdd, it allocates and manages BDDs. + Cudd* bdd_mng; // Manager of BDDs from lib cubdd, it allocates and manages BDDs. BDD val; - MintermizationAlgebra() { - this->val = BDD(); - } + MintermizationAlgebra(Cudd* mng) : bdd_mng(mng), val(BDD()) {} - MintermizationAlgebra(BDD val) { - this->val = val; - } + MintermizationAlgebra(BDD val, Cudd* mng) : val(val), bdd_mng(mng) {}; + + MintermizationAlgebra(const MintermizationAlgebra& alg) : bdd_mng(alg.bdd_mng), val(alg.val) {}; friend MintermizationAlgebra operator&&(const MintermizationAlgebra& lhs, const MintermizationAlgebra &rhs) { - return {lhs.val * rhs.val}; + return MintermizationAlgebra(lhs.val * rhs.val, lhs.bdd_mng); } friend MintermizationAlgebra operator||(const MintermizationAlgebra& lhs, const MintermizationAlgebra &rhs) { - return {lhs.val + rhs.val}; + return {lhs.val + rhs.val, lhs.bdd_mng}; } friend MintermizationAlgebra operator!(const MintermizationAlgebra &lhs) { - return {!lhs.val}; + return {!lhs.val, lhs.bdd_mng}; } bool operator==(const MintermizationAlgebra &rhs) const { @@ -55,9 +53,9 @@ namespace Mata { return val.IsZero(); } - static MintermizationAlgebra getTrue(); - static MintermizationAlgebra getFalse(); - static MintermizationAlgebra getVar(); + MintermizationAlgebra getTrue() const; + MintermizationAlgebra getFalse() const; + MintermizationAlgebra getVar() const; }; } @@ -78,7 +76,7 @@ private: // data types enum class TYPE {NOTHING_E, VALUE_E}; TYPE type{}; - MintermizationAlgebra val{}; + MintermizationAlgebra val{&bdd_mng}; OptionalValue() = default; explicit OptionalValue(TYPE t) : type(t) {} @@ -93,6 +91,7 @@ private: // data types using DisjunctStatesPair = std::pair; private: // private data members + static Cudd bdd_mng; std::unordered_map symbol_to_var{}; std::unordered_map trans_to_var{}; std::unordered_map> lhs_to_disjuncts_and_states{}; @@ -167,7 +166,9 @@ public: void minterms_to_aut_afa(Mata::IntermediateAut& res, const Mata::IntermediateAut& aut, const std::unordered_set& minterms); - Mintermization() : symbol_to_var{}, trans_to_var() {} + Mintermization() : symbol_to_var{}, trans_to_var() { + Mintermization::bdd_mng = Cudd(0); + } }; // class Mintermization. } // namespace Mata diff --git a/src/mintermization.cc b/src/mintermization.cc index 1d03b9d4..d6ea6249 100644 --- a/src/mintermization.cc +++ b/src/mintermization.cc @@ -58,20 +58,20 @@ namespace { } } -Cudd Mata::MintermizationAlgebra::bdd_mng = Cudd{}; - -struct Mata::MintermizationAlgebra Mata::MintermizationAlgebra::getTrue() { - return MintermizationAlgebra(MintermizationAlgebra::bdd_mng.bddOne()); +struct Mata::MintermizationAlgebra Mata::MintermizationAlgebra::getTrue() const { + return MintermizationAlgebra(bdd_mng->bddOne(), bdd_mng); } -struct Mata::MintermizationAlgebra Mata::MintermizationAlgebra::getFalse() { - return MintermizationAlgebra(MintermizationAlgebra::bdd_mng.bddZero()); +struct Mata::MintermizationAlgebra Mata::MintermizationAlgebra::getFalse() const { + return MintermizationAlgebra(bdd_mng->bddZero(), bdd_mng); } -struct Mata::MintermizationAlgebra Mata::MintermizationAlgebra::getVar() { - return MintermizationAlgebra(MintermizationAlgebra::bdd_mng.bddVar()); +struct Mata::MintermizationAlgebra Mata::MintermizationAlgebra::getVar() const { + return MintermizationAlgebra(bdd_mng->bddVar(), bdd_mng); } +Cudd Mata::Mintermization::bdd_mng = Cudd(0); + void Mata::Mintermization::trans_to_vars_nfa(const IntermediateAut &aut) { assert(aut.is_nfa()); @@ -85,7 +85,7 @@ void Mata::Mintermization::trans_to_vars_nfa(const IntermediateAut &aut) if (val.isFalse()) continue; vars.insert(val); - trans_to_var[&symbol_part] = val; + trans_to_var.insert(std::make_pair(&symbol_part, val)); } } @@ -124,12 +124,12 @@ void Mata::Mintermization::trans_to_vars_afa(const IntermediateAut &aut) for (const DisjunctStatesPair& ds_pair : lhs_to_disjuncts_and_states[&trans.first]) { // create val for the whole disjunct const auto val = (ds_pair.first == ds_pair.second) ? // disjunct contains only states - OptionalValue(MintermizationAlgebra::getTrue()) : // transition from state to states -> add true as symbol + OptionalValue(MintermizationAlgebra(&bdd_mng).getTrue()) : // transition from state to states -> add true as symbol graph_to_vars_afa(*ds_pair.first); assert(val.type == OptionalValue::TYPE::VALUE_E); if (val.val.isFalse()) continue; - trans_to_var[ds_pair.first] = val.val; + trans_to_var.insert(std::make_pair(ds_pair.first, val.val)); vars.insert(val.val); } } @@ -138,7 +138,7 @@ void Mata::Mintermization::trans_to_vars_afa(const IntermediateAut &aut) std::unordered_set Mata::Mintermization::compute_minterms( const std::unordered_set& source_bdds) { - std::unordered_set stack{ MintermizationAlgebra::getTrue() }; + std::unordered_set stack{ MintermizationAlgebra(&bdd_mng).getTrue() }; for (const MintermizationAlgebra& b: source_bdds) { std::unordered_set next; /** @@ -172,9 +172,10 @@ Mata::Mintermization::OptionalValue Mata::Mintermization::graph_to_vars_afa(cons if (symbol_to_var.count(node.name)) { return OptionalValue(symbol_to_var.at(node.name)); } else { - MintermizationAlgebra res = (node.name == "true") ? MintermizationAlgebra::getTrue() : - (node.name == "false" ? MintermizationAlgebra::getFalse() : MintermizationAlgebra::getVar()); - symbol_to_var[node.name] = res; + MintermizationAlgebra res = (node.name == "true") ? MintermizationAlgebra(&bdd_mng).getTrue() : + (node.name == "false" ? MintermizationAlgebra(&bdd_mng).getFalse() : + MintermizationAlgebra(&bdd_mng).getVar()); + symbol_to_var.insert(std::make_pair(node.name, res)); return OptionalValue(res); } } else if (node.is_operator()) { @@ -208,9 +209,10 @@ MintermizationAlgebra Mata::Mintermization::graph_to_vars_nfa(const FormulaGraph if (symbol_to_var.count(node.name)) { return symbol_to_var.at(node.name); } else { - MintermizationAlgebra res = (node.name == "true") ? MintermizationAlgebra::getTrue() : - (node.name == "false" ? MintermizationAlgebra::getFalse() : MintermizationAlgebra::getVar()); - symbol_to_var[node.name] = res; + MintermizationAlgebra res = (node.name == "true") ? MintermizationAlgebra(&bdd_mng).getTrue() : + (node.name == "false" ? MintermizationAlgebra(&bdd_mng).getFalse() : + MintermizationAlgebra(&bdd_mng).getVar()); + symbol_to_var.insert(std::make_pair(node.name, res)); return res; } } else if (node.is_operator()) { @@ -233,7 +235,6 @@ MintermizationAlgebra Mata::Mintermization::graph_to_vars_nfa(const FormulaGraph } assert(false); - return {}; } void Mata::Mintermization::minterms_to_aut_nfa(Mata::IntermediateAut& res, const Mata::IntermediateAut& aut, @@ -246,7 +247,7 @@ void Mata::Mintermization::minterms_to_aut_nfa(Mata::IntermediateAut& res, const 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 MintermizationAlgebra &var = trans_to_var[&symbol_part]; + const MintermizationAlgebra &var = trans_to_var.at(&symbol_part); for (const auto &minterm: minterms) { // for each minterm x: @@ -271,7 +272,7 @@ void Mata::Mintermization::minterms_to_aut_afa(Mata::IntermediateAut& res, const if (!trans_to_var.count(disjunct)) continue; // Transition had zero var so it was not added to map - const MintermizationAlgebra &var = trans_to_var[disjunct]; + const MintermizationAlgebra var = trans_to_var.at(disjunct); size_t symbol = 0; for (const auto &minterm: minterms) { From b6f2227fe924e78e8de658bae99e136a83f039ba Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Wed, 13 Sep 2023 07:38:52 +0200 Subject: [PATCH 03/18] removing static bdd_mng --- include/mata/parser/mintermization.hh | 15 ++++++++------- src/mintermization.cc | 6 ++---- 2 files changed, 10 insertions(+), 11 deletions(-) diff --git a/include/mata/parser/mintermization.hh b/include/mata/parser/mintermization.hh index 1f11aa36..5591490a 100644 --- a/include/mata/parser/mintermization.hh +++ b/include/mata/parser/mintermization.hh @@ -27,11 +27,13 @@ namespace Mata { Cudd* bdd_mng; // Manager of BDDs from lib cubdd, it allocates and manages BDDs. BDD val; + MintermizationAlgebra() : bdd_mng(nullptr), val(BDD()) {} + MintermizationAlgebra(Cudd* mng) : bdd_mng(mng), val(BDD()) {} - MintermizationAlgebra(BDD val, Cudd* mng) : val(val), bdd_mng(mng) {}; + MintermizationAlgebra(BDD val, Cudd* mng) : bdd_mng(mng), val(val) {}; - MintermizationAlgebra(const MintermizationAlgebra& alg) : bdd_mng(alg.bdd_mng), val(alg.val) {}; + MintermizationAlgebra(const MintermizationAlgebra& alg) = default; friend MintermizationAlgebra operator&&(const MintermizationAlgebra& lhs, const MintermizationAlgebra &rhs) { return MintermizationAlgebra(lhs.val * rhs.val, lhs.bdd_mng); @@ -75,11 +77,10 @@ private: // data types struct OptionalValue { enum class TYPE {NOTHING_E, VALUE_E}; - TYPE type{}; - MintermizationAlgebra val{&bdd_mng}; + TYPE type; + MintermizationAlgebra val; - OptionalValue() = default; - explicit OptionalValue(TYPE t) : type(t) {} + OptionalValue() : type(TYPE::NOTHING_E) {} explicit OptionalValue(const MintermizationAlgebra& algebra) : type(TYPE::VALUE_E), val(algebra) {} OptionalValue(TYPE t, const MintermizationAlgebra& algebra) : type(t), val(algebra) {} @@ -91,7 +92,7 @@ private: // data types using DisjunctStatesPair = std::pair; private: // private data members - static Cudd bdd_mng; + Cudd bdd_mng; std::unordered_map symbol_to_var{}; std::unordered_map trans_to_var{}; std::unordered_map> lhs_to_disjuncts_and_states{}; diff --git a/src/mintermization.cc b/src/mintermization.cc index d6ea6249..edb7c61b 100644 --- a/src/mintermization.cc +++ b/src/mintermization.cc @@ -70,8 +70,6 @@ struct Mata::MintermizationAlgebra Mata::MintermizationAlgebra::getVar() const { return MintermizationAlgebra(bdd_mng->bddVar(), bdd_mng); } -Cudd Mata::Mintermization::bdd_mng = Cudd(0); - void Mata::Mintermization::trans_to_vars_nfa(const IntermediateAut &aut) { assert(aut.is_nfa()); @@ -168,7 +166,7 @@ Mata::Mintermization::OptionalValue Mata::Mintermization::graph_to_vars_afa(cons if (node.is_operand()) { if (node.is_state()) - return OptionalValue(OptionalValue::TYPE::NOTHING_E); + return OptionalValue(); if (symbol_to_var.count(node.name)) { return OptionalValue(symbol_to_var.at(node.name)); } else { @@ -360,7 +358,7 @@ Mata::Mintermization::OptionalValue Mata::Mintermization::OptionalValue::operato Mata::Mintermization::OptionalValue Mata::Mintermization::OptionalValue::operator!() const { if (this->type == TYPE::NOTHING_E) { - return OptionalValue(TYPE::NOTHING_E); + return OptionalValue(); } else { return OptionalValue{TYPE::VALUE_E, !this->val }; } From addb9251aa57dece1cd6d6bcc1667d6bd5d16ecd Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Wed, 13 Sep 2023 22:17:46 +0200 Subject: [PATCH 04/18] final encapsulation of bdd manager --- include/mata/parser/mintermization.hh | 19 +++++++++---------- src/mintermization.cc | 22 +++++++++++----------- 2 files changed, 20 insertions(+), 21 deletions(-) diff --git a/include/mata/parser/mintermization.hh b/include/mata/parser/mintermization.hh index 5591490a..665ce350 100644 --- a/include/mata/parser/mintermization.hh +++ b/include/mata/parser/mintermization.hh @@ -24,27 +24,27 @@ namespace Mata { struct MintermizationAlgebra { - Cudd* bdd_mng; // Manager of BDDs from lib cubdd, it allocates and manages BDDs. + Cudd bdd_mng; // Manager of BDDs from lib cubdd, it allocates and manages BDDs. BDD val; - MintermizationAlgebra() : bdd_mng(nullptr), val(BDD()) {} + MintermizationAlgebra() : bdd_mng(0), val(BDD()) {} - MintermizationAlgebra(Cudd* mng) : bdd_mng(mng), val(BDD()) {} + MintermizationAlgebra(Cudd mng) : bdd_mng(mng), val(BDD()) {} - MintermizationAlgebra(BDD val, Cudd* mng) : bdd_mng(mng), val(val) {}; + MintermizationAlgebra(Cudd mng, BDD val) : bdd_mng(mng), val(val) {}; MintermizationAlgebra(const MintermizationAlgebra& alg) = default; friend MintermizationAlgebra operator&&(const MintermizationAlgebra& lhs, const MintermizationAlgebra &rhs) { - return MintermizationAlgebra(lhs.val * rhs.val, lhs.bdd_mng); + return {lhs.bdd_mng, lhs.val * rhs.val}; } friend MintermizationAlgebra operator||(const MintermizationAlgebra& lhs, const MintermizationAlgebra &rhs) { - return {lhs.val + rhs.val, lhs.bdd_mng}; + return {lhs.bdd_mng, lhs.val + rhs.val}; } friend MintermizationAlgebra operator!(const MintermizationAlgebra &lhs) { - return {!lhs.val, lhs.bdd_mng}; + return {lhs.bdd_mng, !lhs.val}; } bool operator==(const MintermizationAlgebra &rhs) const { @@ -92,7 +92,7 @@ private: // data types using DisjunctStatesPair = std::pair; private: // private data members - Cudd bdd_mng; + MintermizationAlgebra domain_base; std::unordered_map symbol_to_var{}; std::unordered_map trans_to_var{}; std::unordered_map> lhs_to_disjuncts_and_states{}; @@ -167,8 +167,7 @@ public: void minterms_to_aut_afa(Mata::IntermediateAut& res, const Mata::IntermediateAut& aut, const std::unordered_set& minterms); - Mintermization() : symbol_to_var{}, trans_to_var() { - Mintermization::bdd_mng = Cudd(0); + Mintermization() : symbol_to_var{}, trans_to_var(), domain_base() { } }; // class Mintermization. diff --git a/src/mintermization.cc b/src/mintermization.cc index edb7c61b..58bef3ba 100644 --- a/src/mintermization.cc +++ b/src/mintermization.cc @@ -59,15 +59,15 @@ namespace { } struct Mata::MintermizationAlgebra Mata::MintermizationAlgebra::getTrue() const { - return MintermizationAlgebra(bdd_mng->bddOne(), bdd_mng); + return MintermizationAlgebra(bdd_mng, bdd_mng.bddOne()); } struct Mata::MintermizationAlgebra Mata::MintermizationAlgebra::getFalse() const { - return MintermizationAlgebra(bdd_mng->bddZero(), bdd_mng); + return MintermizationAlgebra(bdd_mng, bdd_mng.bddZero()); } struct Mata::MintermizationAlgebra Mata::MintermizationAlgebra::getVar() const { - return MintermizationAlgebra(bdd_mng->bddVar(), bdd_mng); + return MintermizationAlgebra(bdd_mng, bdd_mng.bddVar()); } void Mata::Mintermization::trans_to_vars_nfa(const IntermediateAut &aut) @@ -122,7 +122,7 @@ void Mata::Mintermization::trans_to_vars_afa(const IntermediateAut &aut) for (const DisjunctStatesPair& ds_pair : lhs_to_disjuncts_and_states[&trans.first]) { // create val for the whole disjunct const auto val = (ds_pair.first == ds_pair.second) ? // disjunct contains only states - OptionalValue(MintermizationAlgebra(&bdd_mng).getTrue()) : // transition from state to states -> add true as symbol + OptionalValue(domain_base.getTrue()) : // transition from state to states -> add true as symbol graph_to_vars_afa(*ds_pair.first); assert(val.type == OptionalValue::TYPE::VALUE_E); if (val.val.isFalse()) @@ -136,7 +136,7 @@ void Mata::Mintermization::trans_to_vars_afa(const IntermediateAut &aut) std::unordered_set Mata::Mintermization::compute_minterms( const std::unordered_set& source_bdds) { - std::unordered_set stack{ MintermizationAlgebra(&bdd_mng).getTrue() }; + std::unordered_set stack{ domain_base.getTrue() }; for (const MintermizationAlgebra& b: source_bdds) { std::unordered_set next; /** @@ -170,9 +170,9 @@ Mata::Mintermization::OptionalValue Mata::Mintermization::graph_to_vars_afa(cons if (symbol_to_var.count(node.name)) { return OptionalValue(symbol_to_var.at(node.name)); } else { - MintermizationAlgebra res = (node.name == "true") ? MintermizationAlgebra(&bdd_mng).getTrue() : - (node.name == "false" ? MintermizationAlgebra(&bdd_mng).getFalse() : - MintermizationAlgebra(&bdd_mng).getVar()); + MintermizationAlgebra res = (node.name == "true") ? domain_base.getTrue() : + (node.name == "false" ? domain_base.getFalse() : + domain_base.getVar()); symbol_to_var.insert(std::make_pair(node.name, res)); return OptionalValue(res); } @@ -207,9 +207,9 @@ MintermizationAlgebra Mata::Mintermization::graph_to_vars_nfa(const FormulaGraph if (symbol_to_var.count(node.name)) { return symbol_to_var.at(node.name); } else { - MintermizationAlgebra res = (node.name == "true") ? MintermizationAlgebra(&bdd_mng).getTrue() : - (node.name == "false" ? MintermizationAlgebra(&bdd_mng).getFalse() : - MintermizationAlgebra(&bdd_mng).getVar()); + MintermizationAlgebra res = (node.name == "true") ? domain_base.getTrue() : + (node.name == "false" ? domain_base.getFalse() : + domain_base.getVar()); symbol_to_var.insert(std::make_pair(node.name, res)); return res; } From dddc8fbd265e1693f24a18f4aff662a55b2027cb Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Wed, 13 Sep 2023 22:25:09 +0200 Subject: [PATCH 05/18] Renamed MintermizationAlgebra to MintermizationDomain to make it comprehensible for stupid computer scientists --- include/mata/parser/mintermization.hh | 52 +++++++++++----------- src/mintermization.cc | 64 +++++++++++++-------------- tests/mintermization.cc | 10 ++--- 3 files changed, 63 insertions(+), 63 deletions(-) diff --git a/include/mata/parser/mintermization.hh b/include/mata/parser/mintermization.hh index 665ce350..abcacc75 100644 --- a/include/mata/parser/mintermization.hh +++ b/include/mata/parser/mintermization.hh @@ -23,31 +23,31 @@ namespace Mata { - struct MintermizationAlgebra { + struct MintermizationDomain { Cudd bdd_mng; // Manager of BDDs from lib cubdd, it allocates and manages BDDs. BDD val; - MintermizationAlgebra() : bdd_mng(0), val(BDD()) {} + MintermizationDomain() : bdd_mng(0), val(BDD()) {} - MintermizationAlgebra(Cudd mng) : bdd_mng(mng), val(BDD()) {} + MintermizationDomain(Cudd mng) : bdd_mng(mng), val(BDD()) {} - MintermizationAlgebra(Cudd mng, BDD val) : bdd_mng(mng), val(val) {}; + MintermizationDomain(Cudd mng, BDD val) : bdd_mng(mng), val(val) {}; - MintermizationAlgebra(const MintermizationAlgebra& alg) = default; + MintermizationDomain(const MintermizationDomain& alg) = default; - friend MintermizationAlgebra operator&&(const MintermizationAlgebra& lhs, const MintermizationAlgebra &rhs) { + friend MintermizationDomain operator&&(const MintermizationDomain& lhs, const MintermizationDomain &rhs) { return {lhs.bdd_mng, lhs.val * rhs.val}; } - friend MintermizationAlgebra operator||(const MintermizationAlgebra& lhs, const MintermizationAlgebra &rhs) { + friend MintermizationDomain operator||(const MintermizationDomain& lhs, const MintermizationDomain &rhs) { return {lhs.bdd_mng, lhs.val + rhs.val}; } - friend MintermizationAlgebra operator!(const MintermizationAlgebra &lhs) { + friend MintermizationDomain operator!(const MintermizationDomain &lhs) { return {lhs.bdd_mng, !lhs.val}; } - bool operator==(const MintermizationAlgebra &rhs) const { + bool operator==(const MintermizationDomain &rhs) const { return this->val == rhs.val; } @@ -55,17 +55,17 @@ namespace Mata { return val.IsZero(); } - MintermizationAlgebra getTrue() const; - MintermizationAlgebra getFalse() const; - MintermizationAlgebra getVar() const; + MintermizationDomain getTrue() const; + MintermizationDomain getFalse() const; + MintermizationDomain getVar() const; }; } // custom specialization of std::hash can be injected in namespace std namespace std { template<> - struct hash { - size_t operator()(const struct Mata::MintermizationAlgebra &algebra) const noexcept { + struct hash { + size_t operator()(const struct Mata::MintermizationDomain &algebra) const noexcept { return hash{}(algebra.val); } }; @@ -78,11 +78,11 @@ private: // data types enum class TYPE {NOTHING_E, VALUE_E}; TYPE type; - MintermizationAlgebra val; + MintermizationDomain val; OptionalValue() : type(TYPE::NOTHING_E) {} - explicit OptionalValue(const MintermizationAlgebra& algebra) : type(TYPE::VALUE_E), val(algebra) {} - OptionalValue(TYPE t, const MintermizationAlgebra& algebra) : type(t), val(algebra) {} + explicit OptionalValue(const MintermizationDomain& algebra) : type(TYPE::VALUE_E), val(algebra) {} + OptionalValue(TYPE t, const MintermizationDomain& algebra) : type(t), val(algebra) {} OptionalValue operator*(const OptionalValue& b) const; OptionalValue operator+(const OptionalValue& b) const; @@ -92,11 +92,11 @@ private: // data types using DisjunctStatesPair = std::pair; private: // private data members - MintermizationAlgebra domain_base; - std::unordered_map symbol_to_var{}; - std::unordered_map trans_to_var{}; + MintermizationDomain domain_base; + std::unordered_map symbol_to_var{}; + std::unordered_map trans_to_var{}; std::unordered_map> lhs_to_disjuncts_and_states{}; - std::unordered_set vars{}; // vars created from transitions + std::unordered_set vars{}; // vars created from transitions private: void trans_to_vars_nfa(const IntermediateAut& aut); @@ -109,15 +109,15 @@ public: * @param source_bdds BDDs 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& source_bdds); /** * Transforms a graph representing formula at transition to bdd. * @param graph Graph to be transformed * @return Resulting BDD */ - MintermizationAlgebra graph_to_vars_nfa(const FormulaGraph& graph); + MintermizationDomain graph_to_vars_nfa(const FormulaGraph& graph); /** * Transforms a graph representing formula at transition to bdd. @@ -155,7 +155,7 @@ 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); + const std::unordered_set& minterms); /** * The method for mintermization of alternating finite automaton using @@ -165,7 +165,7 @@ public: * @param minterms Set of minterms for mintermization */ void minterms_to_aut_afa(Mata::IntermediateAut& res, const Mata::IntermediateAut& aut, - const std::unordered_set& minterms); + const std::unordered_set& minterms); Mintermization() : symbol_to_var{}, trans_to_var(), domain_base() { } diff --git a/src/mintermization.cc b/src/mintermization.cc index 58bef3ba..c093a2ab 100644 --- a/src/mintermization.cc +++ b/src/mintermization.cc @@ -19,7 +19,7 @@ #include -using MintermizationAlgebra = struct Mata::MintermizationAlgebra; +using MintermizationDomain = struct Mata::MintermizationDomain; namespace { const Mata::FormulaGraph* detect_state_part(const Mata::FormulaGraph* node) @@ -58,16 +58,16 @@ namespace { } } -struct Mata::MintermizationAlgebra Mata::MintermizationAlgebra::getTrue() const { - return MintermizationAlgebra(bdd_mng, bdd_mng.bddOne()); +struct Mata::MintermizationDomain Mata::MintermizationDomain::getTrue() const { + return MintermizationDomain(bdd_mng, bdd_mng.bddOne()); } -struct Mata::MintermizationAlgebra Mata::MintermizationAlgebra::getFalse() const { - return MintermizationAlgebra(bdd_mng, bdd_mng.bddZero()); +struct Mata::MintermizationDomain Mata::MintermizationDomain::getFalse() const { + return MintermizationDomain(bdd_mng, bdd_mng.bddZero()); } -struct Mata::MintermizationAlgebra Mata::MintermizationAlgebra::getVar() const { - return MintermizationAlgebra(bdd_mng, bdd_mng.bddVar()); +struct Mata::MintermizationDomain Mata::MintermizationDomain::getVar() const { + return MintermizationDomain(bdd_mng, bdd_mng.bddVar()); } void Mata::Mintermization::trans_to_vars_nfa(const IntermediateAut &aut) @@ -75,11 +75,11 @@ void Mata::Mintermization::trans_to_vars_nfa(const IntermediateAut &aut) assert(aut.is_nfa()); for (const auto& trans : aut.transitions) { - // Foreach transition create a MintermizationAlgebra + // 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 MintermizationAlgebra val = graph_to_vars_nfa(symbol_part); + const MintermizationDomain val = graph_to_vars_nfa(symbol_part); if (val.isFalse()) continue; vars.insert(val); @@ -118,7 +118,7 @@ void Mata::Mintermization::trans_to_vars_afa(const IntermediateAut &aut) act_graph)); } - // Foreach disjunct create a MintermizationAlgebra + // Foreach disjunct create a MintermizationDomain for (const DisjunctStatesPair& ds_pair : lhs_to_disjuncts_and_states[&trans.first]) { // create val for the whole disjunct const auto val = (ds_pair.first == ds_pair.second) ? // disjunct contains only states @@ -133,23 +133,23 @@ void Mata::Mintermization::trans_to_vars_afa(const IntermediateAut &aut) } } -std::unordered_set Mata::Mintermization::compute_minterms( - const std::unordered_set& source_bdds) +std::unordered_set Mata::Mintermization::compute_minterms( + const std::unordered_set& source_bdds) { - std::unordered_set stack{ domain_base.getTrue() }; - for (const MintermizationAlgebra& b: source_bdds) { - std::unordered_set next; + std::unordered_set stack{ domain_base.getTrue() }; + for (const MintermizationDomain& b: source_bdds) { + 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) { - MintermizationAlgebra b1 = minterm && b; + MintermizationDomain b1 = minterm && b; if (!b1.isFalse()) { next.insert(b1); } - MintermizationAlgebra b0 = minterm && !b; + MintermizationDomain b0 = minterm && !b; if (!b0.isFalse()) { next.insert(b0); } @@ -170,7 +170,7 @@ Mata::Mintermization::OptionalValue Mata::Mintermization::graph_to_vars_afa(cons if (symbol_to_var.count(node.name)) { return OptionalValue(symbol_to_var.at(node.name)); } else { - MintermizationAlgebra res = (node.name == "true") ? domain_base.getTrue() : + MintermizationDomain res = (node.name == "true") ? domain_base.getTrue() : (node.name == "false" ? domain_base.getFalse() : domain_base.getVar()); symbol_to_var.insert(std::make_pair(node.name, res)); @@ -199,7 +199,7 @@ Mata::Mintermization::OptionalValue Mata::Mintermization::graph_to_vars_afa(cons return {}; } -MintermizationAlgebra Mata::Mintermization::graph_to_vars_nfa(const FormulaGraph &graph) +MintermizationDomain Mata::Mintermization::graph_to_vars_nfa(const FormulaGraph &graph) { const FormulaNode& node = graph.node; @@ -207,7 +207,7 @@ MintermizationAlgebra Mata::Mintermization::graph_to_vars_nfa(const FormulaGraph if (symbol_to_var.count(node.name)) { return symbol_to_var.at(node.name); } else { - MintermizationAlgebra res = (node.name == "true") ? domain_base.getTrue() : + MintermizationDomain res = (node.name == "true") ? domain_base.getTrue() : (node.name == "false" ? domain_base.getFalse() : domain_base.getVar()); symbol_to_var.insert(std::make_pair(node.name, res)); @@ -216,17 +216,17 @@ MintermizationAlgebra Mata::Mintermization::graph_to_vars_nfa(const FormulaGraph } else if (node.is_operator()) { if (node.operator_type == FormulaNode::OperatorType::AND) { assert(graph.children.size() == 2); - const MintermizationAlgebra op1 = graph_to_vars_nfa(graph.children[0]); - const MintermizationAlgebra op2 = graph_to_vars_nfa(graph.children[1]); + 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 MintermizationAlgebra op1 = graph_to_vars_nfa(graph.children[0]); - const MintermizationAlgebra op2 = graph_to_vars_nfa(graph.children[1]); + 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 MintermizationAlgebra op1 = graph_to_vars_nfa(graph.children[0]); + const MintermizationDomain op1 = graph_to_vars_nfa(graph.children[0]); return !op1; } else assert(false); @@ -236,7 +236,7 @@ MintermizationAlgebra Mata::Mintermization::graph_to_vars_nfa(const FormulaGraph } void Mata::Mintermization::minterms_to_aut_nfa(Mata::IntermediateAut& res, const Mata::IntermediateAut& aut, - const std::unordered_set& minterms) + const std::unordered_set& minterms) { for (const auto& trans : aut.transitions) { // for each t=(q1,s,q2) @@ -245,12 +245,12 @@ void Mata::Mintermization::minterms_to_aut_nfa(Mata::IntermediateAut& res, const 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 MintermizationAlgebra &var = trans_to_var.at(&symbol_part); + 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 MintermizationAlgebra_s < x + // 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}); @@ -261,7 +261,7 @@ void Mata::Mintermization::minterms_to_aut_nfa(Mata::IntermediateAut& res, const } void Mata::Mintermization::minterms_to_aut_afa(Mata::IntermediateAut& res, const Mata::IntermediateAut& aut, - const std::unordered_set& minterms) + const std::unordered_set& minterms) { for (const auto& trans : aut.transitions) { for (const auto& ds_pair : lhs_to_disjuncts_and_states[&trans.first]) { @@ -270,13 +270,13 @@ void Mata::Mintermization::minterms_to_aut_afa(Mata::IntermediateAut& res, const if (!trans_to_var.count(disjunct)) continue; // Transition had zero var so it was not added to map - const MintermizationAlgebra var = trans_to_var.at(disjunct); + const MintermizationDomain var = trans_to_var.at(disjunct); size_t symbol = 0; for (const auto &minterm: minterms) { // for each minterm x: if (!((var && minterm).isFalse())) { - // if for symbol s of t is MintermizationAlgebra_s < x + // if for symbol s of t is MintermizationDomain_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, @@ -306,7 +306,7 @@ std::vector Mata::Mintermization::mintermize(const std::v aut->is_nfa() ? trans_to_vars_nfa(*aut) : trans_to_vars_afa(*aut); } - // Build minterm tree over MintermizationAlgebras + // Build minterm tree over MintermizationDomains auto minterms = compute_minterms(vars); std::vector res; diff --git a/tests/mintermization.cc b/tests/mintermization.cc index e16abb6c..8684df44 100644 --- a/tests/mintermization.cc +++ b/tests/mintermization.cc @@ -42,7 +42,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::MintermizationAlgebra alg = mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]); + const Mata::MintermizationDomain alg = mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]); REQUIRE(alg.val.nodeCount() == 2); } @@ -61,7 +61,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::MintermizationAlgebra alg = mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]); + const Mata::MintermizationDomain alg = mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]); REQUIRE(alg.val.nodeCount() == 3); } @@ -80,7 +80,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::MintermizationAlgebra alg = mintermization.graph_to_vars_nfa(aut.transitions[0].second.children[0]); + const Mata::MintermizationDomain 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()); @@ -110,7 +110,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); @@ -133,7 +133,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); From a72b5b3178ea9e5f9b7a919cedc1703bdc07d11b Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Fri, 29 Sep 2023 22:11:06 +0200 Subject: [PATCH 06/18] fixing constant problem in mintermization --- src/mintermization.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/mintermization.cc b/src/mintermization.cc index d972069c..12ecdc4c 100644 --- a/src/mintermization.cc +++ b/src/mintermization.cc @@ -122,8 +122,8 @@ MintermizationDomain mata::Mintermization::graph_to_vars_nfa(const FormulaGraph if (symbol_to_var.count(node.name)) { return symbol_to_var.at(node.name); } else { - MintermizationDomain res = (node.name == "true") ? domain_base.getTrue() : - (node.name == "false" ? domain_base.getFalse() : + MintermizationDomain res = (node.name == "\\true") ? domain_base.getTrue() : + (node.name == "\\false" ? domain_base.getFalse() : domain_base.getVar()); symbol_to_var.insert(std::make_pair(node.name, res)); return res; From c95e9be202d56b6c59379702acaca31170bc29bd Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Fri, 29 Sep 2023 22:15:34 +0200 Subject: [PATCH 07/18] proper constant handling in mintermization --- src/mintermization.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/mintermization.cc b/src/mintermization.cc index 12ecdc4c..4f896ce3 100644 --- a/src/mintermization.cc +++ b/src/mintermization.cc @@ -122,8 +122,8 @@ MintermizationDomain mata::Mintermization::graph_to_vars_nfa(const FormulaGraph if (symbol_to_var.count(node.name)) { return symbol_to_var.at(node.name); } else { - MintermizationDomain res = (node.name == "\\true") ? domain_base.getTrue() : - (node.name == "\\false" ? domain_base.getFalse() : + MintermizationDomain res = (node.is_true()) ? domain_base.getTrue() : + (node.is_false() ? domain_base.getFalse() : domain_base.getVar()); symbol_to_var.insert(std::make_pair(node.name, res)); return res; From a669c696960cf0ba19b99df387e89258ccdee809 Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Fri, 29 Sep 2023 22:31:52 +0200 Subject: [PATCH 08/18] fixing warning causing issues --- include/mata/parser/mintermization.hh | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/include/mata/parser/mintermization.hh b/include/mata/parser/mintermization.hh index 6b931207..57df4ce4 100644 --- a/include/mata/parser/mintermization.hh +++ b/include/mata/parser/mintermization.hh @@ -32,8 +32,6 @@ namespace mata { MintermizationDomain(Cudd mng, BDD val) : bdd_mng(mng), val(val) {}; - MintermizationDomain(const MintermizationDomain& alg) = default; - friend MintermizationDomain operator&&(const MintermizationDomain& lhs, const MintermizationDomain &rhs) { return {lhs.bdd_mng, lhs.val * rhs.val}; } @@ -146,7 +144,7 @@ public: void minterms_to_aut_nfa(mata::IntermediateAut& res, const mata::IntermediateAut& aut, const std::unordered_set& minterms); - Mintermization() : symbol_to_var{}, trans_to_var(), domain_base() { + Mintermization() : domain_base(), symbol_to_var{}, trans_to_var() { } }; // class Mintermization. } // namespace mata From d4b9a5e45fab111b0d9734ee3540976f23902b6b Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Sat, 30 Sep 2023 21:31:30 +0200 Subject: [PATCH 09/18] Templatization of mintermization --- examples/example06-mintermization.cc | 2 +- include/mata/parser/mintermization.hh | 217 ++++++++++++++++++++------ src/CMakeLists.txt | 1 + src/mintermization.cc | 185 ---------------------- tests-integration/src/utils/utils.cc | 4 +- tests/mintermization.cc | 9 +- 6 files changed, 175 insertions(+), 243 deletions(-) diff --git a/examples/example06-mintermization.cc b/examples/example06-mintermization.cc index 519d4d7f..b90c7c89 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.hh b/include/mata/parser/mintermization.hh index 57df4ce4..49a09e65 100644 --- a/include/mata/parser/mintermization.hh +++ b/include/mata/parser/mintermization.hh @@ -17,46 +17,8 @@ #ifndef MATA_MINTERM_HH #define MATA_MINTERM_HH -#include "mata/cudd/cuddObj.hh" - #include "inter-aut.hh" - -namespace mata { - struct MintermizationDomain { - Cudd bdd_mng; // Manager of BDDs from lib cubdd, it allocates and manages BDDs. - BDD val; - - MintermizationDomain() : bdd_mng(0), val(BDD()) {} - - MintermizationDomain(Cudd mng) : bdd_mng(mng), val(BDD()) {} - - MintermizationDomain(Cudd mng, BDD val) : bdd_mng(mng), val(val) {}; - - friend MintermizationDomain operator&&(const MintermizationDomain& lhs, const MintermizationDomain &rhs) { - return {lhs.bdd_mng, lhs.val * rhs.val}; - } - - friend MintermizationDomain operator||(const MintermizationDomain& lhs, const MintermizationDomain &rhs) { - return {lhs.bdd_mng, lhs.val + rhs.val}; - } - - friend MintermizationDomain operator!(const MintermizationDomain &lhs) { - return {lhs.bdd_mng, !lhs.val}; - } - - bool operator==(const MintermizationDomain &rhs) const { - return this->val == rhs.val; - } - - bool isFalse() const { - return val.IsZero(); - } - - MintermizationDomain getTrue() const; - MintermizationDomain getFalse() const; - MintermizationDomain getVar() const; - }; -} +#include "mintermization-domain.hh" // custom specialization of std::hash can be injected in namespace std namespace std { @@ -69,6 +31,8 @@ namespace std { } namespace mata { + +template class Mintermization { private: // data types struct OptionalValue { @@ -81,9 +45,33 @@ private: // data types explicit OptionalValue(const MintermizationDomain& algebra) : type(TYPE::VALUE_E), val(algebra) {} OptionalValue(TYPE t, const MintermizationDomain& algebra) : type(t), val(algebra) {} - OptionalValue operator*(const OptionalValue& b) const; - OptionalValue operator+(const OptionalValue& b) const; - OptionalValue operator!() const; + OptionalValue operator*(const OptionalValue& b) const { + if (this->type == TYPE::NOTHING_E) { + return b; + } else if (b.type == TYPE::NOTHING_E) { + return *this; + } else { + return OptionalValue{TYPE::VALUE_E, this->val && b.val }; + } + } + + OptionalValue operator+(const OptionalValue& b) const { + if (this->type == TYPE::NOTHING_E) { + return b; + } else if (b.type == TYPE::NOTHING_E) { + return *this; + } else { + return OptionalValue{TYPE::VALUE_E, this->val || b.val }; + } + } + + OptionalValue operator!() const { + if (this->type == TYPE::NOTHING_E) { + return OptionalValue(); + } else { + return OptionalValue{TYPE::VALUE_E, !this->val }; + } + } }; using DisjunctStatesPair = std::pair; @@ -92,12 +80,27 @@ private: // private data members 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)); + } + } + std::unordered_map> lhs_to_disjuncts_and_states{}; std::unordered_set vars{}; // vars created from transitions -private: - void trans_to_vars_nfa(const IntermediateAut& aut); - public: /** * Takes a set of BDDs and build a minterm tree over it. @@ -106,14 +109,71 @@ public: * @return Computed minterms */ std::unordered_set compute_minterms( - const std::unordered_set& source_bdds); + const std::unordered_set& source_bdds) + { + std::unordered_set stack{ domain_base.getTrue() }; + for (const MintermizationDomain& b: source_bdds) { + 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 */ - MintermizationDomain graph_to_vars_nfa(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.getTrue() : + (node.is_false() ? domain_base.getFalse() : + domain_base.getVar()); + 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. @@ -122,7 +182,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})[0]; + } /** * Methods mintermize given automata which have bitvector alphabet. @@ -131,8 +193,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. @@ -142,7 +235,29 @@ 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); + 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() { } diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c3b5bbea..27a1cd85 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 + mintermization-domain.cc parser.cc re2parser.cc nfa/nfa.cc diff --git a/src/mintermization.cc b/src/mintermization.cc index 4f896ce3..f4ecf00a 100644 --- a/src/mintermization.cc +++ b/src/mintermization.cc @@ -58,188 +58,3 @@ namespace { } } -struct mata::MintermizationDomain mata::MintermizationDomain::getTrue() const { - return MintermizationDomain(bdd_mng, bdd_mng.bddOne()); -} - -struct mata::MintermizationDomain mata::MintermizationDomain::getFalse() const { - return MintermizationDomain(bdd_mng, bdd_mng.bddZero()); -} - -struct mata::MintermizationDomain mata::MintermizationDomain::getVar() const { - return MintermizationDomain(bdd_mng, bdd_mng.bddVar()); -} - -void mata::Mintermization::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)); - } -} - -std::unordered_set mata::Mintermization::compute_minterms( - const std::unordered_set& source_bdds) -{ - std::unordered_set stack{ domain_base.getTrue() }; - for (const MintermizationDomain& b: source_bdds) { - 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; -} - -MintermizationDomain mata::Mintermization::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.getTrue() : - (node.is_false() ? domain_base.getFalse() : - domain_base.getVar()); - 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); -} - -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_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++; - } - } -} - -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->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; -} - -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::OptionalValue mata::Mintermization::OptionalValue::operator*( - const mata::Mintermization::OptionalValue& b) const { - if (this->type == TYPE::NOTHING_E) { - return b; - } else if (b.type == TYPE::NOTHING_E) { - return *this; - } else { - return OptionalValue{TYPE::VALUE_E, this->val && b.val }; - } -} - -mata::Mintermization::OptionalValue mata::Mintermization::OptionalValue::operator+( - const mata::Mintermization::OptionalValue& b) const { - if (this->type == TYPE::NOTHING_E) { - return b; - } else if (b.type == TYPE::NOTHING_E) { - return *this; - } else { - return OptionalValue{TYPE::VALUE_E, this->val || b.val }; - } -} - -mata::Mintermization::OptionalValue mata::Mintermization::OptionalValue::operator!() const { - if (this->type == TYPE::NOTHING_E) { - return OptionalValue(); - } else { - return OptionalValue{TYPE::VALUE_E, !this->val }; - } -} diff --git a/tests-integration/src/utils/utils.cc b/tests-integration/src/utils/utils.cc index e85f8fd4..86a5a58a 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 61d56f96..aacea3aa 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/mintermization-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") { @@ -92,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") { @@ -143,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 = @@ -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" From 99a20ea0b898a851b89f9cd07de60997dafa103e Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Sat, 30 Sep 2023 21:42:57 +0200 Subject: [PATCH 10/18] added forgotten files --- include/mata/parser/mintermization-domain.hh | 60 ++++++++++++++++++++ src/mintermization-domain.cc | 29 ++++++++++ 2 files changed, 89 insertions(+) create mode 100644 include/mata/parser/mintermization-domain.hh create mode 100644 src/mintermization-domain.cc diff --git a/include/mata/parser/mintermization-domain.hh b/include/mata/parser/mintermization-domain.hh new file mode 100644 index 00000000..47c10b9c --- /dev/null +++ b/include/mata/parser/mintermization-domain.hh @@ -0,0 +1,60 @@ +/* + * mintermization-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 MintermizationDomain { + Cudd bdd_mng; // Manager of BDDs from lib cubdd, it allocates and manages BDDs. + BDD val; + + MintermizationDomain() : bdd_mng(0), val(BDD()) {} + + MintermizationDomain(Cudd mng) : bdd_mng(mng), val(BDD()) {} + + MintermizationDomain(Cudd mng, BDD val) : bdd_mng(mng), val(val) {}; + + friend MintermizationDomain operator&&(const MintermizationDomain& lhs, const MintermizationDomain &rhs) { + return {lhs.bdd_mng, lhs.val * rhs.val}; + } + + friend MintermizationDomain operator||(const MintermizationDomain& lhs, const MintermizationDomain &rhs) { + return {lhs.bdd_mng, lhs.val + rhs.val}; + } + + friend MintermizationDomain operator!(const MintermizationDomain &lhs) { + return {lhs.bdd_mng, !lhs.val}; + } + + bool operator==(const MintermizationDomain &rhs) const { + return this->val == rhs.val; + } + + bool isFalse() const { + return val.IsZero(); + } + + MintermizationDomain getTrue() const; + MintermizationDomain getFalse() const; + MintermizationDomain getVar() const; + }; +} + +#endif //LIBMATA_MINTERMIZATION_DOMAIN_HH diff --git a/src/mintermization-domain.cc b/src/mintermization-domain.cc new file mode 100644 index 00000000..ee7ef5ef --- /dev/null +++ b/src/mintermization-domain.cc @@ -0,0 +1,29 @@ +/* + * mintermization-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/mintermization-domain.hh" + +struct mata::MintermizationDomain mata::MintermizationDomain::getTrue() const { + return MintermizationDomain(bdd_mng, bdd_mng.bddOne()); +} + +struct mata::MintermizationDomain mata::MintermizationDomain::getFalse() const { + return MintermizationDomain(bdd_mng, bdd_mng.bddZero()); +} + +struct mata::MintermizationDomain mata::MintermizationDomain::getVar() const { + return MintermizationDomain(bdd_mng, bdd_mng.bddVar()); +} From 8ce5282a6a8f77a4c0c78f28cc2859573f603993 Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Sat, 30 Sep 2023 21:52:37 +0200 Subject: [PATCH 11/18] 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 b90c7c89..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/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 47c10b9c..fde942fe 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 49a09e65..903c1671 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 27a1cd85..fd913e51 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 ee7ef5ef..910020d6 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 f4ecf00a..f11a7960 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 86a5a58a..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/CMakeLists.txt b/tests/CMakeLists.txt index c7a0a17e..73c532c1 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 aacea3aa..121da290 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" From 2815fd6ec2f93cdce4b2f4e36dbad7309073c642 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Hru=C5=A1ka?= Date: Sat, 7 Oct 2023 11:05:54 +0200 Subject: [PATCH 12/18] Update tests/mintermization.cc MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: David Chocholatý --- tests/mintermization.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/mintermization.cc b/tests/mintermization.cc index 121da290..ee35666c 100644 --- a/tests/mintermization.cc +++ b/tests/mintermization.cc @@ -23,7 +23,7 @@ using namespace mata::parser; -TEST_CASE("Mata::Mintermization::trans_to_vars_nfa") +TEST_CASE("mata::Mintermization::trans_to_vars_nfa") { Parsed parsed; mata::Mintermization mintermization{}; From fb8c9d4b1a53f6616a06b647f3d2056765470114 Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Sat, 7 Oct 2023 11:03:21 +0200 Subject: [PATCH 13/18] removing debug flags from cmake --- src/CMakeLists.txt | 2 -- tests/CMakeLists.txt | 2 -- 2 files changed, 4 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index fd913e51..9b666d40 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -24,8 +24,6 @@ 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/tests/CMakeLists.txt b/tests/CMakeLists.txt index 73c532c1..c7a0a17e 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -19,8 +19,6 @@ 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. From a772b878513e8e3f76cf89e2af0e252da6ba745f Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Sat, 7 Oct 2023 11:06:37 +0200 Subject: [PATCH 14/18] removed unnecessary include --- src/mintermization.cc | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/mintermization.cc b/src/mintermization.cc index f11a7960..854004a5 100644 --- a/src/mintermization.cc +++ b/src/mintermization.cc @@ -17,8 +17,6 @@ #include "mata/parser/mintermization.hh" -#include - namespace { const mata::FormulaGraph* detect_state_part(const mata::FormulaGraph* node) { From 6c745e3fca2a929f035599c8b3c9ce7cba12f0f7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Hru=C5=A1ka?= Date: Sat, 7 Oct 2023 11:09:53 +0200 Subject: [PATCH 15/18] Update include/mata/parser/mintermization.hh MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: David Chocholatý --- include/mata/parser/mintermization.hh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/mata/parser/mintermization.hh b/include/mata/parser/mintermization.hh index 903c1671..7569ad4b 100644 --- a/include/mata/parser/mintermization.hh +++ b/include/mata/parser/mintermization.hh @@ -26,7 +26,7 @@ template class Mintermization { private: // data types struct OptionalValue { - enum class TYPE {NOTHING_E, VALUE_E}; + enum class Type {NOTHING_E, VALUE_E}; TYPE type; MintermizationDomain val; From 637630c0b4410f839d8ffc7a1fa8c4023d920af5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Hru=C5=A1ka?= Date: Sat, 7 Oct 2023 11:14:18 +0200 Subject: [PATCH 16/18] Update include/mata/parser/mintermization.hh Co-authored-by: Tomas Fiedor --- include/mata/parser/mintermization.hh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/include/mata/parser/mintermization.hh b/include/mata/parser/mintermization.hh index 7569ad4b..916cfa28 100644 --- a/include/mata/parser/mintermization.hh +++ b/include/mata/parser/mintermization.hh @@ -244,7 +244,7 @@ public: IntermediateAut::parse_transition(res, {trans.first.raw, std::to_string(symbol), trans.second.children[1].node.raw}); } - symbol++; + ++symbol; } } } From c1f4b1624e875ca2578e8d48494246aad8cd0865 Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Sat, 7 Oct 2023 11:16:37 +0200 Subject: [PATCH 17/18] making reviewrs happy --- include/mata/parser/bdd-domain.hh | 6 +++--- include/mata/parser/mintermization.hh | 20 ++++++++++---------- src/bdd-domain.cc | 6 +++--- 3 files changed, 16 insertions(+), 16 deletions(-) diff --git a/include/mata/parser/bdd-domain.hh b/include/mata/parser/bdd-domain.hh index fde942fe..fba4ff18 100644 --- a/include/mata/parser/bdd-domain.hh +++ b/include/mata/parser/bdd-domain.hh @@ -51,9 +51,9 @@ namespace mata { return val.IsZero(); } - BDDDomain getTrue() const; - BDDDomain getFalse() const; - BDDDomain getVar() const; + BDDDomain get_true() const; + BDDDomain get_false() const; + BDDDomain get_var() const; }; } diff --git a/include/mata/parser/mintermization.hh b/include/mata/parser/mintermization.hh index 916cfa28..142f3a11 100644 --- a/include/mata/parser/mintermization.hh +++ b/include/mata/parser/mintermization.hh @@ -93,16 +93,16 @@ private: // private data members 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) + const std::unordered_set& domain_values) { - std::unordered_set stack{ domain_base.getTrue() }; - for (const MintermizationDomain& b: source_bdds) { + 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 @@ -137,9 +137,9 @@ public: if (symbol_to_var.count(node.name)) { return symbol_to_var.at(node.name); } else { - MintermizationDomain res = (node.is_true()) ? domain_base.getTrue() : - (node.is_false() ? domain_base.getFalse() : - domain_base.getVar()); + 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; } @@ -173,7 +173,7 @@ public: * @return Mintermized automaton */ mata::IntermediateAut mintermize(const mata::IntermediateAut& aut) { - return mintermize(std::vector{&aut})[0]; + return mintermize(std::vector{&aut}).front(); } /** diff --git a/src/bdd-domain.cc b/src/bdd-domain.cc index 910020d6..d9e51a41 100644 --- a/src/bdd-domain.cc +++ b/src/bdd-domain.cc @@ -16,14 +16,14 @@ #include "mata/parser/bdd-domain.hh" -struct mata::BDDDomain mata::BDDDomain::getTrue() const { +struct mata::BDDDomain mata::BDDDomain::get_true() const { return BDDDomain(bdd_mng, bdd_mng.bddOne()); } -struct mata::BDDDomain mata::BDDDomain::getFalse() const { +struct mata::BDDDomain mata::BDDDomain::get_false() const { return BDDDomain(bdd_mng, bdd_mng.bddZero()); } -struct mata::BDDDomain mata::BDDDomain::getVar() const { +struct mata::BDDDomain mata::BDDDomain::get_var() const { return BDDDomain(bdd_mng, bdd_mng.bddVar()); } From eac2b4987f1a1a929c12a0d384e1926d6640b8fb Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Sat, 7 Oct 2023 11:25:17 +0200 Subject: [PATCH 18/18] Added documentation and removed obsolete struct OptionalValue --- include/mata/parser/mintermization.hh | 47 +++++---------------------- 1 file changed, 8 insertions(+), 39 deletions(-) diff --git a/include/mata/parser/mintermization.hh b/include/mata/parser/mintermization.hh index 142f3a11..f75e1235 100644 --- a/include/mata/parser/mintermization.hh +++ b/include/mata/parser/mintermization.hh @@ -22,48 +22,17 @@ 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 OptionalValue { - enum class Type {NOTHING_E, VALUE_E}; - - TYPE type; - MintermizationDomain val; - - OptionalValue() : type(TYPE::NOTHING_E) {} - explicit OptionalValue(const MintermizationDomain& algebra) : type(TYPE::VALUE_E), val(algebra) {} - OptionalValue(TYPE t, const MintermizationDomain& algebra) : type(t), val(algebra) {} - - OptionalValue operator*(const OptionalValue& b) const { - if (this->type == TYPE::NOTHING_E) { - return b; - } else if (b.type == TYPE::NOTHING_E) { - return *this; - } else { - return OptionalValue{TYPE::VALUE_E, this->val && b.val }; - } - } - - OptionalValue operator+(const OptionalValue& b) const { - if (this->type == TYPE::NOTHING_E) { - return b; - } else if (b.type == TYPE::NOTHING_E) { - return *this; - } else { - return OptionalValue{TYPE::VALUE_E, this->val || b.val }; - } - } - - OptionalValue operator!() const { - if (this->type == TYPE::NOTHING_E) { - return OptionalValue(); - } else { - return OptionalValue{TYPE::VALUE_E, !this->val }; - } - } - }; - using DisjunctStatesPair = std::pair; private: // private data members