From 46c7ebc760a2ed329f6c53f7c7aa4bccccafd225 Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Mon, 2 Oct 2023 23:10:19 +0200 Subject: [PATCH 1/6] raw prototype of new parser --- CMakeLists.txt | 2 +- examples/example06-mintermization.cc | 49 ----- include/mata/parser/inter-aut.hh | 254 ++++++++++++++-------- src/CMakeLists.txt | 2 +- src/inter-aut.cc | 301 ++++++++++++++------------- src/nfa/builder.cc | 18 +- tests/CMakeLists.txt | 2 +- tests/parser.cc | 136 ++++++------ 8 files changed, 404 insertions(+), 360 deletions(-) delete mode 100644 examples/example06-mintermization.cc diff --git a/CMakeLists.txt b/CMakeLists.txt index e61b668f8..9b2977d1e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -123,7 +123,7 @@ endif() # Build tests only if Mata is the main project and we enabled testing if((CMAKE_PROJECT_NAME STREQUAL PROJECT_NAME) AND BUILD_TESTING) add_subdirectory(tests) - add_subdirectory(tests-integration) + # add_subdirectory(tests-integration) endif() diff --git a/examples/example06-mintermization.cc b/examples/example06-mintermization.cc deleted file mode 100644 index 519d4d7f2..000000000 --- a/examples/example06-mintermization.cc +++ /dev/null @@ -1,49 +0,0 @@ -// example6.cc - mintermization of automaton - -#include "mata/parser/inter-aut.hh" -#include "mata/parser/mintermization.hh" -#include "mata/nfa/nfa.hh" - -#include -#include - -using namespace mata::nfa; - -int main(int argc, char *argv[]) { - if (argc != 2) { - std::cerr << "Input file missing\n"; - return EXIT_FAILURE; - } - - std::string filename = argv[1]; - - std::fstream fs(filename, std::ios::in); - if (!fs) { - std::cerr << "Could not open file \'" << filename << "'\n"; - return EXIT_FAILURE; - } - - mata::parser::Parsed parsed; - Nfa aut; - try { - parsed = mata::parser::parse_mf(fs, true); - fs.close(); - - std::vector inter_auts = mata::IntermediateAut::parse_from_mf(parsed); - for (const auto& ia : inter_auts) { - 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); - assert(ia.transitions.size() <= aut.transitions.size()); - std::cout << aut << '\n'; - } - } - } catch (const std::exception& ex) { - fs.close(); - std::cerr << "libMATA error: " << ex.what() << "\n"; - return EXIT_FAILURE; - } - - return EXIT_SUCCESS; -} diff --git a/include/mata/parser/inter-aut.hh b/include/mata/parser/inter-aut.hh index 514b6d67a..8f4e28b47 100644 --- a/include/mata/parser/inter-aut.hh +++ b/include/mata/parser/inter-aut.hh @@ -36,86 +36,108 @@ namespace mata { * Each node has a name (in case of marking naming, an initial character defining type of node is removed and stored in * name), raw (name including potential type marker), and information about its type. */ -struct FormulaNode { -public: - enum class OperandType { - SYMBOL, - STATE, - NODE, - TRUE, - FALSE, - NOT_OPERAND - }; + struct FormulaNode { + public: + enum class OperandType { + SYMBOL, + STATE, + NODE, + TRUE, + FALSE, + NOT_OPERAND + }; - enum class OperatorType { - NEG, - AND, - OR, - NOT_OPERATOR - }; + enum class OperatorType { + NEG, + AND, + OR, + NOT_OPERATOR + }; - enum class Type { - OPERAND, - OPERATOR, - LEFT_PARENTHESIS, - RIGHT_PARENTHESIS, - UNKNOWN - }; + enum class Type { + OPERAND, + OPERATOR, + LEFT_PARENTHESIS, + RIGHT_PARENTHESIS, + UNKNOWN + }; + + /// Define whether a node is operand or operator + Type type; + /// Raw name of node as it was specified in input text, i.e., including type marker. + std::string raw; + /// Parsed name, i.e., a potential type marker (first character) is removed. + std::string name; // Parsed name. When type marking is used, markers are removed. + /// if a node is operator, it defines which one + OperatorType operator_type; + /// if a node is operand, it defines which one + OperandType operand_type; + + bool is_operand() const { return type == Type::OPERAND; } - /// Define whether a node is operand or operator - Type type; - /// Raw name of node as it was specified in input text, i.e., including type marker. - std::string raw; - /// Parsed name, i.e., a potential type marker (first character) is removed. - std::string name; // Parsed name. When type marking is used, markers are removed. - /// if a node is operator, it defines which one - OperatorType operator_type; - /// if a node is operand, it defines which one - OperandType operand_type; + bool is_operator() const { return type == Type::OPERATOR; } - bool is_operand() const { return type == Type::OPERAND; } + bool is_rightpar() const { return type == Type::RIGHT_PARENTHESIS; } - bool is_operator() const { return type == Type::OPERATOR; } + bool is_leftpar() const { return type == Type::LEFT_PARENTHESIS; } - bool is_rightpar() const { return type == Type::RIGHT_PARENTHESIS; } + bool is_state() const { return operand_type == OperandType::STATE; } - bool is_leftpar() const { return type == Type::LEFT_PARENTHESIS; } + bool is_symbol() const { return operand_type == OperandType::SYMBOL; } - bool is_state() const { return operand_type == OperandType::STATE; } + bool is_and() const { return type == Type::OPERATOR && operator_type == OperatorType::AND; } - bool is_symbol() const { return operand_type == OperandType::SYMBOL; } + bool is_neg() const { return type == Type::OPERATOR && operator_type == OperatorType::NEG; } - bool is_and() const { return type == Type::OPERATOR && operator_type == OperatorType::AND; } + // TODO: should constant be its own operand type? + bool is_constant() const { return is_true() || is_false(); } - bool is_neg() const { return type == Type::OPERATOR && operator_type == OperatorType::NEG; } + bool is_true() const { return is_operand() && operand_type == OperandType::TRUE; } - // TODO: should constant be its own operand type? - bool is_constant() const { return is_true() || is_false(); } - bool is_true() const { return is_operand() && operand_type == OperandType::TRUE; } - bool is_false() const { return is_operand() && operand_type == OperandType::FALSE; } + bool is_false() const { return is_operand() && operand_type == OperandType::FALSE; } - FormulaNode() - : type(Type::UNKNOWN), raw(), name(), operator_type(OperatorType::NOT_OPERATOR), - operand_type(OperandType::NOT_OPERAND) {} + FormulaNode() + : type(Type::UNKNOWN), raw(), name(), operator_type(OperatorType::NOT_OPERATOR), + operand_type(OperandType::NOT_OPERAND) {} - FormulaNode(Type t, std::string raw, std::string name, OperatorType operator_t) - : type(t), raw(std::move(raw)), name(std::move(name)), operator_type(operator_t), operand_type(OperandType::NOT_OPERAND) {} + FormulaNode(Type t, std::string raw, std::string name, OperatorType operator_t) + : type(t), raw(std::move(raw)), name(std::move(name)), operator_type(operator_t), + operand_type(OperandType::NOT_OPERAND) {} - FormulaNode(Type t, std::string raw, std::string name, OperandType operand) - : type(t), raw(std::move(raw)), name(std::move(name)), operator_type(OperatorType::NOT_OPERATOR), operand_type(operand) {} + FormulaNode(Type t, std::string raw, std::string name, OperandType operand) + : type(t), raw(std::move(raw)), name(std::move(name)), operator_type(OperatorType::NOT_OPERATOR), + operand_type(operand) {} - FormulaNode(Type t, const std::string& raw) - : type(t), raw(raw), name(raw), operator_type(OperatorType::NOT_OPERATOR), operand_type(OperandType::NOT_OPERAND) {} + FormulaNode(Type t, const std::string &raw) + : type(t), raw(raw), name(raw), operator_type(OperatorType::NOT_OPERATOR), + operand_type(OperandType::NOT_OPERAND) {} - FormulaNode(const FormulaNode& n) - : type(n.type), raw(n.raw), name(n.name), operator_type(n.operator_type), operand_type(n.operand_type) {} + FormulaNode(const FormulaNode &n) + : type(n.type), raw(n.raw), name(n.name), operator_type(n.operator_type), + operand_type(n.operand_type) {} - FormulaNode(FormulaNode&&) noexcept = default; + FormulaNode(FormulaNode &&) noexcept = default; - FormulaNode& operator=(const FormulaNode& other) = default; - FormulaNode& operator=(FormulaNode&& other) noexcept = default; -}; + FormulaNode &operator=(const FormulaNode &other) = default; + FormulaNode &operator=(FormulaNode &&other) noexcept = default; + + bool operator==(const FormulaNode& other) const { + return this->raw == other.raw; + } + }; +} + +namespace std { + template<> + struct hash { + size_t operator()(const struct mata::FormulaNode &node) const noexcept { + return hash{}(node.raw); + } + }; +} + +namespace mata { /** * Structure representing a transition formula using a graph. * A node of graph consists of node itself and set of children nodes. @@ -123,24 +145,56 @@ public: * E.g., a formula q1 & s1 will be transformed to a tree with & as a root node * and q1 and s2 being children nodes of the root. */ -class FormulaGraph { -public: - FormulaNode node{}; - std::vector children{}; + class FormulaGraph { + public: + FormulaNode *node{}; + FormulaGraph *left{}; + FormulaGraph *right{}; + + FormulaGraph() = default; + + explicit FormulaGraph(FormulaNode *n) : node(n), left(nullptr), right(nullptr) {} + + FormulaGraph(FormulaGraph &g) : node(g.node), left(g.left), right(g.right) {} + + FormulaGraph(const FormulaGraph &g) : node(g.node), left(g.left), right(g.right) {} + + FormulaGraph(FormulaGraph &&g) noexcept: node(g.node), left(g.left), right(g.right) {} - FormulaGraph() = default; - explicit FormulaGraph(const FormulaNode& n) : node(n), children() { children.reserve(2); } - explicit FormulaGraph(FormulaNode&& n) : node(std::move(n)), children() { children.reserve(2); } - FormulaGraph(const FormulaGraph& g) : node(g.node), children(g.children) {} - FormulaGraph(FormulaGraph&& g) noexcept : node(std::move(g.node)), children(std::move(g.children)) {} + FormulaGraph &operator=(const mata::FormulaGraph &) = default; - FormulaGraph& operator=(const mata::FormulaGraph&) = default; - FormulaGraph& operator=(mata::FormulaGraph&&) noexcept = default; + FormulaGraph &operator=(mata::FormulaGraph &&) noexcept = default; - std::unordered_set collect_node_names() const; - void print_tree(std::ostream& os) const; -}; + bool operator==(const FormulaGraph& other) const { + return this->node == other.node && this->left == other.left && this->right == other.right; + } + inline bool both_children_defined() const { + return left != nullptr && right != nullptr; + } + + inline bool both_children_null() const { + return left == nullptr && right == nullptr; + } + + std::unordered_set collect_node_names() const; + + void print_tree(std::ostream &os) const; + }; +} + +namespace std { + template<> + struct hash { + size_t operator()(const mata::FormulaGraph &graph) const noexcept { + return (std::hash{}(graph.node) + 0x9e3779b9) ^ + (std::hash()(graph.left->node) + 0x9e3779b9) ^ + (std::hash()(graph.right->node) + 0x9e3779b9); + } + }; +} + +namespace mata { /** * Structure for a general intermediate representation of parsed automaton. * It contains information about type of automata, type of naming of nodes, symbols and states @@ -197,8 +251,12 @@ public: std::vector symbols_names{}; std::vector nodes_names{}; - FormulaGraph initial_formula{}; - FormulaGraph final_formula{}; + std::unordered_set nodes{}; + std::unordered_set graphs{}; + std::unordered_map raw_to_nodes{}; + + FormulaGraph* initial_formula{}; + FormulaGraph* final_formula{}; bool initial_enumerated = false; bool final_enumerated = false; @@ -207,7 +265,7 @@ public: * Transitions are pairs where the first member is left-hand side of transition (i.e., a state) * and the second item is a graph representing transition formula (which can contain symbols, nodes, and states). */ - struct std::vector> transitions{}; + struct std::vector> transitions{}; /** * Returns symbolic part of transition. That may be just a symbol or bitvector formula. @@ -216,7 +274,7 @@ public: * @param transition Transition from which symbol is returned * @return Graph representing symbol. It maybe just an explicit symbol or graph representing bitvector formula */ - const FormulaGraph& get_symbol_part_of_transition(const std::pair& trans) const; + const FormulaGraph& get_symbol_part_of_transition(const std::pair& trans) const; /** * @brief A method for building a vector of IntermediateAut for a parsed input. @@ -240,11 +298,11 @@ public: bool is_nfa() const {return automaton_type == AutomatonType::NFA;} bool is_afa() const {return automaton_type == AutomatonType::AFA;} - std::unordered_set get_enumerated_initials() const {return initial_formula.collect_node_names();} - std::unordered_set get_enumerated_finals() const {return final_formula.collect_node_names();} + std::unordered_set get_enumerated_initials() const {return initial_formula->collect_node_names();} + std::unordered_set get_enumerated_finals() const {return final_formula->collect_node_names();} bool are_final_states_conjunction_of_negation() const { - return is_graph_conjunction_of_negations(final_formula); + return is_graph_conjunction_of_negations(*final_formula); } static bool is_graph_conjunction_of_negations(const FormulaGraph& graph); @@ -258,9 +316,39 @@ public: size_t get_number_of_disjuncts() const; static void parse_transition(mata::IntermediateAut &aut, const std::vector &tokens); - void add_transition(const FormulaNode& lhs, const FormulaNode& symbol, const FormulaGraph& rhs); - void add_transition(const FormulaNode& lhs, const FormulaNode& rhs); + void add_transition(FormulaNode* lhs, FormulaNode* symbol, FormulaGraph* rhs); + void add_transition(FormulaNode* lhs, FormulaNode* rhs); void print_transitions_trees(std::ostream&) const; + + FormulaGraph* create_graph(FormulaNode* n) { + auto i = (graphs.insert(FormulaGraph{n})).first; + return const_cast(&*i); + } + + FormulaNode* enpool_node(FormulaNode& n) { + auto i = (nodes.insert(std::move(n))).first; + return const_cast(&*i); + } + + FormulaNode* enpool_node(FormulaNode&& n) { + auto i = (nodes.insert(std::move(n))).first; + return const_cast(&*i); + } + + void init_nodes() { + raw_to_nodes["&"] = enpool_node(FormulaNode{ FormulaNode::Type::OPERATOR, "&", "&", + FormulaNode::OperatorType::AND }); + raw_to_nodes["|"] = enpool_node(FormulaNode{ FormulaNode::Type::OPERATOR, "|", "|", + FormulaNode::OperatorType::OR }); + raw_to_nodes["!"] = enpool_node(FormulaNode{ FormulaNode::Type::OPERATOR, "!", "!", + FormulaNode::OperatorType::NEG }); + raw_to_nodes["("] = enpool_node(FormulaNode{ FormulaNode::Type::LEFT_PARENTHESIS, "("}); + raw_to_nodes[")"] = enpool_node(FormulaNode{ FormulaNode::Type::RIGHT_PARENTHESIS, ")"}); + raw_to_nodes["\\true"] = enpool_node(FormulaNode{ FormulaNode::Type::OPERAND, "\\true", + "\\true", mata::FormulaNode::OperandType::TRUE}); + raw_to_nodes["\\false"] = enpool_node(FormulaNode{ FormulaNode::Type::OPERAND, "\\false", + "\\false", mata::FormulaNode::OperandType::FALSE}); + } }; // class IntermediateAut. } // namespace mata. diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c3b5bbea0..6cd07f76f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -6,7 +6,7 @@ add_library(libmata STATIC alphabet.cc "${CMAKE_CURRENT_BINARY_DIR}/config.cc" inter-aut.cc - mintermization.cc + # mintermization.cc parser.cc re2parser.cc nfa/nfa.cc diff --git a/src/inter-aut.cc b/src/inter-aut.cc index d860d85c0..335d6043a 100644 --- a/src/inter-aut.cc +++ b/src/inter-aut.cc @@ -92,11 +92,11 @@ bool has_atmost_one_auto_naming(const mata::IntermediateAut& aut) { return std::find(vec.begin(), vec.end(), item) != vec.end(); } - bool no_operators(const std::vector& nodes) { + bool no_operators(const std::vector& nodes) { // Refactor using all_of() when Clang adds support for it. // return std::ranges::all_of(nodes, [](const mata::FormulaNode& node){ return !node.is_operator();}); for (const auto& node: nodes) { - if (node.is_operator()) { + if (node->is_operator()) { return false; } } @@ -105,83 +105,78 @@ bool has_atmost_one_auto_naming(const mata::IntermediateAut& aut) { std::string serialize_graph(const mata::FormulaGraph& graph) { - if (graph.node.is_operand()) - return graph.node.raw; - - if (graph.children.size() == 1) { // unary operator - const auto& child = graph.children.front(); - std::string child_name = child.node.is_operand() ? child.node.raw : - "(" + serialize_graph(mata::FormulaGraph{ std::move(child.node) }) + ")"; - return graph.node.raw + child_name; + if (graph.node->is_operand()) + return graph.node->raw; + + if (graph.right == nullptr) { // unary operator + const auto& child = *graph.left; + std::string child_name = child.node->is_operand() ? child.node->raw : + "(" + serialize_graph(mata::FormulaGraph(child.node)) + ")"; + return graph.node->raw + child_name; } - assert(graph.node.is_operator() && graph.children.size() == 2); - const auto& left_child = graph.children.front(); - std::string lhs = (left_child.node.is_operand()) ? left_child.node.raw : + assert(graph.node->is_operator() && graph.both_children_defined()); + const auto& left_child = *graph.left; + std::string lhs = (left_child.node->is_operand()) ? left_child.node->raw : serialize_graph(left_child); - if (left_child.children.size() == 2) + if (left_child.both_children_defined()) lhs = "(" + lhs + ")"; - const auto& right_child = graph.children[1]; - std::string rhs = (right_child.node.is_operand()) ? right_child.node.raw : + const auto& right_child = *graph.right; + std::string rhs = (right_child.node->is_operand()) ? right_child.node->raw : serialize_graph(right_child); - if (right_child.children.size() == 2) + if (right_child.both_children_defined()) rhs = "(" + rhs + ")"; - return lhs + " " + graph.node.raw + " " + rhs; + return lhs + " " + graph.node->raw + " " + rhs; } - mata::FormulaNode create_node(const mata::IntermediateAut &mata, const std::string& token) { + mata::FormulaNode* create_node(mata::IntermediateAut &mata, const std::string& token) { if (is_logical_operator(token[0])) { switch (token[0]) { case '&': - return { mata::FormulaNode::Type::OPERATOR, token, token, - mata::FormulaNode::OperatorType::AND }; + return mata.raw_to_nodes.at("&"); case '|': - return { mata::FormulaNode::Type::OPERATOR, token, token, - mata::FormulaNode::OperatorType::OR }; + return mata.raw_to_nodes.at("|"); case '!': - return { mata::FormulaNode::Type::OPERATOR, token, token, - mata::FormulaNode::OperatorType::NEG }; + return mata.raw_to_nodes.at("!"); default: assert(false); } } else if (token == "(") { - return { mata::FormulaNode::Type::LEFT_PARENTHESIS, token}; + return mata.raw_to_nodes.at("("); } else if (token == ")") { - return { mata::FormulaNode::Type::RIGHT_PARENTHESIS, token}; + return mata.raw_to_nodes.at(")"); } else if (token == "\\true") { - return { mata::FormulaNode::Type::OPERAND, token, token, - mata::FormulaNode::OperandType::TRUE}; + return mata.raw_to_nodes.at("\\true"); } else if (token == "\\false") { - return { mata::FormulaNode::Type::OPERAND, token, token, - mata::FormulaNode::OperandType::FALSE}; + return mata.raw_to_nodes.at("\\false"); } else if (is_naming_enum(mata.state_naming) && contains(mata.states_names, token)) { - return { mata::FormulaNode::Type::OPERAND, token, token, - mata::FormulaNode::OperandType::STATE}; + return mata.enpool_node({ mata::FormulaNode::Type::OPERAND, token, token, + mata::FormulaNode::OperandType::STATE}); } else if (is_naming_enum(mata.node_naming) && contains(mata.nodes_names, token)) { - return { mata::FormulaNode::Type::OPERAND, token, token, - mata::FormulaNode::OperandType::NODE}; + return mata.enpool_node({ mata::FormulaNode::Type::OPERAND, token, token, + mata::FormulaNode::OperandType::NODE}); } else if (is_naming_enum(mata.symbol_naming) && contains(mata.symbols_names, token)) { - return { mata::FormulaNode::Type::OPERAND, token, token, - mata::FormulaNode::OperandType::SYMBOL}; + return mata.enpool_node({ mata::FormulaNode::Type::OPERAND, token, token, + mata::FormulaNode::OperandType::SYMBOL}); } else if (is_naming_marker(mata.state_naming) && token[0] == 'q') { - return { mata::FormulaNode::Type::OPERAND, token, token.substr(1), - mata::FormulaNode::OperandType::STATE}; + return mata.enpool_node({ mata::FormulaNode::Type::OPERAND, token, token.substr(1), + mata::FormulaNode::OperandType::STATE}); } else if (is_naming_marker(mata.node_naming) && token[0] == 'n') { - return { mata::FormulaNode::Type::OPERAND, token, token.substr(1), - mata::FormulaNode::OperandType::NODE}; + return mata.enpool_node({ mata::FormulaNode::Type::OPERAND, token, token.substr(1), + mata::FormulaNode::OperandType::NODE}); } else if (is_naming_marker(mata.symbol_naming) && token[0] == 'a') { - return { mata::FormulaNode::Type::OPERAND, token, token.substr(1), - mata::FormulaNode::OperandType::SYMBOL}; + return mata.enpool_node({ mata::FormulaNode::Type::OPERAND, token, token.substr(1), + mata::FormulaNode::OperandType::SYMBOL}); } else if (is_naming_auto(mata.state_naming)) { - return { mata::FormulaNode::Type::OPERAND, token, token, - mata::FormulaNode::OperandType::STATE}; + return mata.enpool_node({ mata::FormulaNode::Type::OPERAND, token, token, + mata::FormulaNode::OperandType::STATE}); } else if (is_naming_auto(mata.node_naming)) { - return { mata::FormulaNode::Type::OPERAND, token, token, - mata::FormulaNode::OperandType::NODE}; + return mata.enpool_node({ mata::FormulaNode::Type::OPERAND, token, token, + mata::FormulaNode::OperandType::NODE}); } else if (is_naming_auto(mata.symbol_naming)) { - return { mata::FormulaNode::Type::OPERAND, token, token, - mata::FormulaNode::OperandType::SYMBOL}; + return mata.enpool_node({ mata::FormulaNode::Type::OPERAND, token, token, + mata::FormulaNode::OperandType::SYMBOL}); } throw std::runtime_error("Unknown token " + token); @@ -206,23 +201,23 @@ bool has_atmost_one_auto_naming(const mata::IntermediateAut& aut) { * @param tokens Series of tokens representing transition formula parsed from the input text * @return A postfix notation for input */ - std::vector infix_to_postfix(const mata::IntermediateAut &aut, + std::vector infix_to_postfix(mata::IntermediateAut &aut, const std::vector& tokens) { - std::vector opstack; - std::vector output; + std::vector opstack; + std::vector output; for (const std::string& token: tokens) { - mata::FormulaNode node = create_node(aut, token); - switch (node.type) { + mata::FormulaNode* node = create_node(aut, token); + switch (node->type) { case mata::FormulaNode::Type::OPERAND: - output.emplace_back(std::move(node)); + output.emplace_back(node); break; case mata::FormulaNode::Type::LEFT_PARENTHESIS: - opstack.emplace_back(std::move(node)); + opstack.emplace_back(node); break; case mata::FormulaNode::Type::RIGHT_PARENTHESIS: - while (!opstack.back().is_leftpar()) { - output.emplace_back(std::move(opstack.back())); + while (!opstack.back()->is_leftpar()) { + output.emplace_back(opstack.back()); opstack.pop_back(); } opstack.pop_back(); @@ -230,12 +225,12 @@ bool has_atmost_one_auto_naming(const mata::IntermediateAut& aut) { case mata::FormulaNode::Type::OPERATOR: for (int j = static_cast(opstack.size())-1; j >= 0; --j) { auto formula_node_opstack_it{ opstack.begin() + j }; - assert(!formula_node_opstack_it->is_operand()); - if (formula_node_opstack_it->is_leftpar()) { + assert(!(*formula_node_opstack_it)->is_operand()); + if ((*formula_node_opstack_it)->is_leftpar()) { break; } - if (lower_precedence(node.operator_type, formula_node_opstack_it->operator_type)) { - output.emplace_back(std::move(*formula_node_opstack_it)); + if (lower_precedence(node->operator_type, (*formula_node_opstack_it)->operator_type)) { + output.emplace_back(*formula_node_opstack_it); opstack.erase(formula_node_opstack_it); } } @@ -246,15 +241,15 @@ bool has_atmost_one_auto_naming(const mata::IntermediateAut& aut) { } while (!opstack.empty()) { - output.push_back(std::move(opstack.back())); + output.push_back(opstack.back()); opstack.pop_back(); } #ifndef NDEBUG for (const auto& node : output) { - assert(node.is_operator() || (node.name != "!" && node.name != "&" && node.name != "|")); - assert(node.is_leftpar() || node.name != "("); - assert(node.is_rightpar() || node.name != ")"); + assert(node->is_operator() || (node->name != "!" && node->name != "&" && node->name != "|")); + assert(node->is_leftpar() || node->name != "("); + assert(node->is_rightpar() || node->name != ")"); } #endif // #ifndef NDEBUG. @@ -266,33 +261,35 @@ bool has_atmost_one_auto_naming(const mata::IntermediateAut& aut) { * @param postfix A postfix representation of transition formula * @return A parsed graph */ - mata::FormulaGraph postfix_to_graph(std::vector postfix) { - std::vector opstack{}; - opstack.reserve(4); - for (mata::FormulaNode& node: postfix) { - switch (node.type) { + mata::FormulaGraph* postfix_to_graph(mata::IntermediateAut& ia, std::vector postfix) { + std::vector opstack{}; + for (mata::FormulaNode* node: postfix) { + switch (node->type) { case mata::FormulaNode::Type::OPERAND: - opstack.emplace_back(std::move(node)); + opstack.emplace_back(ia.create_graph(node)); break; case mata::FormulaNode::Type::OPERATOR: { - switch (node.operator_type) { + switch (node->operator_type) { case mata::FormulaNode::OperatorType::NEG: { // 1 child: graph will be a NEG node. assert(!opstack.empty()); - mata::FormulaGraph child{ std::move(opstack.back()) }; + mata::FormulaGraph* child = opstack.back(); opstack.pop_back(); - mata::FormulaGraph& gr{ opstack.emplace_back(std::move(node)) }; - gr.children.emplace_back(std::move(child)); + mata::FormulaGraph *gr = ia.create_graph(node); + opstack.emplace_back(gr); + gr->left = child; + gr->right = nullptr; break; } default: { // 2 children: Graph will be either an AND node, or an OR node. assert(opstack.size() > 1); - mata::FormulaGraph second_child{ std::move(opstack.back()) }; + mata::FormulaGraph* second_child = opstack.back(); opstack.pop_back(); - mata::FormulaGraph first_child{ std::move(opstack.back()) }; + mata::FormulaGraph* first_child = opstack.back(); opstack.pop_back(); - mata::FormulaGraph& gr{ opstack.emplace_back(std::move(node)) }; - gr.children.emplace_back(std::move(first_child)); - gr.children.emplace_back(std::move(second_child)); + mata::FormulaGraph *gr = ia.create_graph(node); + opstack.emplace_back(gr); + gr->left = first_child; + gr->right = second_child; break; } } @@ -304,7 +301,7 @@ bool has_atmost_one_auto_naming(const mata::IntermediateAut& aut) { } assert(opstack.size() == 1); - return std::move(*opstack.begin()); + return *opstack.begin(); } /** @@ -314,28 +311,29 @@ bool has_atmost_one_auto_naming(const mata::IntermediateAut& aut) { * @param postfix Postfix to which operators are eventually added * @return A postfix with eventually added operators */ - std::vector add_disjunction_implicitly(std::vector postfix) { + std::vector add_disjunction_implicitly(mata::IntermediateAut &aut, + std::vector& postfix) { const size_t postfix_size{ postfix.size() }; if (postfix_size == 1) // no need to add operators return postfix; - for (const auto& op : postfix) { - if (op.is_operator()) // operators provided by user, return the original postfix + for (const auto op : postfix) { + if (op->is_operator()) // operators provided by user, return the original postfix return postfix; } - std::vector res; + std::vector res; if (postfix_size >= 2) { - res.push_back(std::move(postfix[0])); - res.push_back(std::move(postfix[1])); - res.emplace_back( - mata::FormulaNode::Type::OPERATOR, "|", "|", mata::FormulaNode::OperatorType::OR); + res.push_back(postfix[0]); + res.push_back(postfix[1]); + auto node = mata::FormulaNode{mata::FormulaNode::Type::OPERATOR, "|", "|", mata::FormulaNode::OperatorType::OR}; + res.emplace_back(aut.enpool_node(mata::FormulaNode(node))); } for (size_t i{ 2 }; i < postfix_size; ++i) { - res.push_back(std::move(postfix[i])); - res.emplace_back( - mata::FormulaNode::Type::OPERATOR, "|", "|", mata::FormulaNode::OperatorType::OR); + res.push_back(postfix[i]); + auto n = mata::FormulaNode{mata::FormulaNode::Type::OPERATOR, "|", "|", mata::FormulaNode::OperatorType::OR}; + res.emplace_back(aut.enpool_node(n)); } return res; @@ -386,16 +384,16 @@ bool has_atmost_one_auto_naming(const mata::IntermediateAut& aut) { auto postfix = infix_to_postfix(aut, keypair.second); if (no_operators(postfix)) { aut.initial_enumerated = true; - postfix = add_disjunction_implicitly(std::move(postfix)); + postfix = add_disjunction_implicitly(aut, postfix); } - aut.initial_formula = postfix_to_graph(std::move(postfix)); + aut.initial_formula = postfix_to_graph(aut, std::move(postfix)); } else if (key.starts_with("Final")) { auto postfix = infix_to_postfix(aut, keypair.second); if (no_operators(postfix)) { - postfix = add_disjunction_implicitly(std::move(postfix)); + postfix = add_disjunction_implicitly(aut, postfix); aut.final_enumerated = true; } - aut.final_formula = postfix_to_graph(std::move(postfix));; + aut.final_formula = postfix_to_graph(aut, postfix); } } @@ -411,6 +409,7 @@ bool has_atmost_one_auto_naming(const mata::IntermediateAut& aut) { } } // Anonymous namespace. +/* size_t mata::IntermediateAut::get_number_of_disjuncts() const { size_t res = 0; @@ -418,12 +417,12 @@ size_t mata::IntermediateAut::get_number_of_disjuncts() const for (const auto& trans : this->transitions) { size_t trans_disjuncts = 0; std::vector stack; - stack.push_back(&trans.second); + stack.push_back(trans.second); while (!stack.empty()) { const FormulaGraph *gr = stack.back(); stack.pop_back(); - if (gr->node.is_operator() && gr->node.operator_type == FormulaNode::OperatorType::OR) + if (gr->node->is_operator() && gr->node->operator_type == FormulaNode::OperatorType::OR) trans_disjuncts++; for (const auto &ch: gr->children) stack.push_back(&ch); @@ -433,6 +432,7 @@ size_t mata::IntermediateAut::get_number_of_disjuncts() const return res; } + */ /** * Parses a transition by firstly transforming transition formula to postfix form and then creating @@ -443,10 +443,12 @@ size_t mata::IntermediateAut::get_number_of_disjuncts() const void mata::IntermediateAut::parse_transition(mata::IntermediateAut &aut, const std::vector& tokens) { assert(tokens.size() > 1); // transition formula has at least two items - mata::FormulaNode lhs = create_node(aut, tokens[0]); + mata::FormulaNode* lhs = create_node(aut, tokens[0]); std::vector rhs(tokens.begin()+1, tokens.end()); - std::vector postfix; + aut.init_nodes(); + + std::vector postfix; // add implicit conjunction to NFA explicit states, i.e. p a q -> p a & q if (aut.automaton_type == mata::IntermediateAut::AutomatonType::NFA && tokens[tokens.size() - 2] != "&") { @@ -454,7 +456,8 @@ void mata::IntermediateAut::parse_transition(mata::IntermediateAut &aut, const s // symbol and state naming and put conjunction to transition if (aut.alphabet_type != mata::IntermediateAut::AlphabetType::BITVECTOR) { assert(rhs.size() == 2); - postfix.emplace_back(mata::FormulaNode::Type::OPERAND, rhs[0], rhs[0], mata::FormulaNode::OperandType::SYMBOL); + auto node = mata::FormulaNode{mata::FormulaNode::Type::OPERAND, rhs[0], rhs[0], mata::FormulaNode::OperandType::SYMBOL}; + postfix.emplace_back(aut.enpool_node(node)); postfix.emplace_back(create_node(aut, rhs[1])); } else if (aut.alphabet_type == mata::IntermediateAut::AlphabetType::BITVECTOR) { // This is a case where rhs state is not separated by a conjunction from the rest of the transitions. @@ -464,19 +467,19 @@ void mata::IntermediateAut::parse_transition(mata::IntermediateAut &aut, const s postfix.emplace_back(create_node(aut, last_token)); } else assert(false && "Unknown NFA type"); - - postfix.emplace_back(mata::FormulaNode::Type::OPERATOR, "&", "&", mata::FormulaNode::OperatorType::AND); + auto node = mata::FormulaNode{mata::FormulaNode::Type::OPERATOR, "&", "&", mata::FormulaNode::OperatorType::AND}; + postfix.emplace_back(aut.enpool_node(node)); } else postfix = infix_to_postfix(aut, rhs); #ifndef NDEBUG for (const auto& node: postfix) { - assert(node.is_operator() || (node.name != "!" && node.name != "&" && node.name != "|")); - assert(node.is_leftpar() || node.name != "("); - assert(node.is_rightpar() || node.name != ")"); + assert(node->is_operator() || (node->name != "!" && node->name != "&" && node->name != "|")); + assert(node->is_leftpar() || node->name != "("); + assert(node->is_rightpar() || node->name != ")"); } #endif // #ifndef NDEBUG. - aut.transitions.emplace_back(std::move(lhs), postfix_to_graph(std::move(postfix))); + aut.transitions.emplace_back(std::move(lhs), postfix_to_graph(aut, std::move(postfix))); } std::unordered_set mata::FormulaGraph::collect_node_names() const @@ -490,16 +493,17 @@ std::unordered_set mata::FormulaGraph::collect_node_names() const assert(g != nullptr); stack.pop_back(); - if (g->node.type == FormulaNode::Type::UNKNOWN) + if (g->node->type == FormulaNode::Type::UNKNOWN) continue; // skip undefined nodes - if (g->node.is_operand()) { - res.insert(g->node.name); + if (g->node->is_operand()) { + res.insert(g->node->name); } - for (const auto& child : g->children) { - stack.push_back(&child); - } + if (g->left != nullptr) + stack.push_back(g->left); + if (g->right != nullptr) + stack.push_back(g->right); } return res; @@ -516,10 +520,11 @@ void mata::FormulaGraph::print_tree(std::ostream& os) const this_level = next_level; next_level.clear(); for (const auto& graph : this_level) { - for (const auto& child : graph->children) { - next_level.push_back(&child); - } - os << graph->node.raw << " "; + if (graph->left != nullptr) + next_level.push_back(graph->left); + if (graph->right != nullptr) + next_level.push_back(graph->right); + os << graph->node->raw << " "; } os << "\n"; } @@ -541,55 +546,55 @@ std::vector mata::IntermediateAut::parse_from_mf(const ma } const mata::FormulaGraph& mata::IntermediateAut::get_symbol_part_of_transition( - const std::pair& trans) const + const std::pair& trans) const { if (!this->is_nfa()) { throw std::runtime_error("We currently support symbol extraction only for NFA"); } - assert(trans.first.is_operand() && trans.first.operand_type == FormulaNode::OperandType::STATE); - assert(trans.second.node.is_operator()); // conjunction with rhs state - assert(trans.second.children[1].node.is_operand()); // rhs state - return trans.second.children[0]; + assert(trans.first->is_operand() && trans.first->operand_type == FormulaNode::OperandType::STATE); + assert(trans.second->node->is_operator()); // conjunction with rhs state + assert(trans.second->right->node->is_operand()); // rhs state + return *trans.second->left; } -void mata::IntermediateAut::add_transition(const FormulaNode& lhs, const FormulaNode& symbol, const FormulaGraph& rhs) +void mata::IntermediateAut::add_transition(FormulaNode* lhs, FormulaNode* symbol, FormulaGraph* rhs) { FormulaNode conjunction(FormulaNode::Type::OPERATOR, "&", "&", FormulaNode::OperatorType::AND); - FormulaGraph graph(conjunction); - graph.children.emplace_back(symbol); - graph.children.push_back(rhs); - this->transitions.emplace_back(lhs, std::move(graph)); + FormulaGraph *graph = create_graph(&conjunction); + graph->left = create_graph(symbol); + graph->right = rhs; + this->transitions.emplace_back(lhs, graph); } -void mata::IntermediateAut::add_transition(const FormulaNode& lhs, const FormulaNode& rhs) +void mata::IntermediateAut::add_transition(FormulaNode* lhs, FormulaNode* rhs) { - assert(rhs.is_operand()); - FormulaGraph graph(rhs); - this->transitions.emplace_back(lhs, std::move(graph)); + assert(rhs->is_operand()); + FormulaGraph* graph = create_graph(rhs); + this->transitions.emplace_back(lhs, graph); } void mata::IntermediateAut::print_transitions_trees(std::ostream& os) const { for (const auto& trans : transitions) { - os << trans.first.raw << " -> "; - trans.second.print_tree(os); + os << trans.first->raw << " -> "; + trans.second->print_tree(os); } } std::unordered_set mata::IntermediateAut::get_positive_finals() const { - if (!is_graph_conjunction_of_negations(this->final_formula)) + if (!is_graph_conjunction_of_negations(*this->final_formula)) throw (std::runtime_error("Final formula is not a conjunction of negations")); - std::unordered_set all = initial_formula.collect_node_names(); + std::unordered_set all = initial_formula->collect_node_names(); for (const auto& trans : this->transitions) { - all.insert(trans.first.name); + all.insert(trans.first->name); // get names from state part of transition - const auto node_names = trans.second.children[1].collect_node_names(); + const auto node_names = trans.second->right->collect_node_names(); all.insert(node_names.begin(), node_names.end()); } - for (const std::string& nonfinal : final_formula.collect_node_names()) + for (const std::string& nonfinal : final_formula->collect_node_names()) all.erase(nonfinal); return all; @@ -598,17 +603,17 @@ std::unordered_set mata::IntermediateAut::get_positive_finals() con bool mata::IntermediateAut::is_graph_conjunction_of_negations(const mata::FormulaGraph &graph) { const FormulaGraph *act_graph = &graph; - while (act_graph->children.size() == 2) { + while (act_graph->both_children_defined()) { // this node is conjunction and the left son is negation, otherwise returns false - if (act_graph->node.is_operator() && act_graph->node.is_and() && - act_graph->children[0].node.is_operator() && act_graph->children[0].node.is_neg()) - act_graph = &act_graph->children[1]; + if (act_graph->node->is_operator() && act_graph->node->is_and() && + act_graph->left->node->is_operator() && act_graph->right->node->is_neg()) + act_graph = act_graph->right; else return false; } // the last child needs to be negation - return (act_graph->node.is_operator() && act_graph->node.is_neg()); + return (act_graph->node->is_operator() && act_graph->node->is_neg()); } std::ostream& std::operator<<(std::ostream& os, const mata::IntermediateAut& inter_aut) @@ -620,21 +625,21 @@ std::ostream& std::operator<<(std::ostream& os, const mata::IntermediateAut& int os << "Alphabet " << static_cast(inter_aut.alphabet_type) << '\n'; os << "Initial states: "; - for (const auto& state : inter_aut.initial_formula.collect_node_names()) { + for (const auto& state : inter_aut.initial_formula->collect_node_names()) { os << state << ' '; } os << '\n'; os << "Final states: "; - for (const auto& state : inter_aut.final_formula.collect_node_names()) { + for (const auto& state : inter_aut.final_formula->collect_node_names()) { os << state << ' '; } os << '\n'; os << "Transitions: \n"; for (const auto& trans : inter_aut.transitions) { - os << trans.first.raw << " -> "; - os << serialize_graph(trans.second); + os << trans.first->raw << " -> "; + os << serialize_graph(*trans.second); /* for (const auto& rhs : trans.second.collect_node_names()) { os << rhs << ' '; diff --git a/src/nfa/builder.cc b/src/nfa/builder.cc index c5bcf497b..d6b0822c1 100644 --- a/src/nfa/builder.cc +++ b/src/nfa/builder.cc @@ -119,7 +119,7 @@ Nfa builder::construct(const mata::IntermediateAut& inter_aut, mata::Alphabet* a } }; - for (const auto& str : inter_aut.initial_formula.collect_node_names()) + for (const auto& str : inter_aut.initial_formula->collect_node_names()) { State state = get_state_name(str); aut.initial.insert(state); @@ -127,9 +127,9 @@ Nfa builder::construct(const mata::IntermediateAut& inter_aut, mata::Alphabet* a for (const auto& trans : inter_aut.transitions) { - if (trans.second.children.size() != 2) + if (!trans.second->both_children_defined()) { - if (trans.second.children.size() == 1) + if (trans.second->left != nullptr) { throw std::runtime_error("Epsilon transitions not supported"); } @@ -139,20 +139,20 @@ Nfa builder::construct(const mata::IntermediateAut& inter_aut, mata::Alphabet* a } } - State src_state = get_state_name(trans.first.name); - Symbol symbol = alphabet->translate_symb(trans.second.children[0].node.name); - State tgt_state = get_state_name(trans.second.children[1].node.name); + State src_state = get_state_name(trans.first->name); + Symbol symbol = alphabet->translate_symb(trans.second->left->node->name); + State tgt_state = get_state_name(trans.second->right->node->name); aut.delta.add(src_state, symbol, tgt_state); } std::unordered_set final_formula_nodes; - if (!(inter_aut.final_formula.node.is_constant())) { + if (!(inter_aut.final_formula->node->is_constant())) { // we do not want to parse true/false (constant) as a state so we do not collect it - final_formula_nodes = inter_aut.final_formula.collect_node_names(); + final_formula_nodes = inter_aut.final_formula->collect_node_names(); } // for constant true, we will pretend that final nodes are negated with empty final_formula_nodes - bool final_nodes_are_negated = (inter_aut.final_formula.node.is_true() || inter_aut.are_final_states_conjunction_of_negation()); + bool final_nodes_are_negated = (inter_aut.final_formula->node->is_true() || inter_aut.are_final_states_conjunction_of_negation()); if (final_nodes_are_negated) { // we add all states NOT in final_formula_nodes to final states diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index c7a0a17e6..6d765716c 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -6,7 +6,7 @@ add_executable(tests alphabet.cc parser.cc re2parser.cc - mintermization.cc + # mintermization.cc nfa/delta.cc nfa/nfa.cc nfa/builder.cc diff --git a/tests/parser.cc b/tests/parser.cc index d9a91f270..2df09c36e 100644 --- a/tests/parser.cc +++ b/tests/parser.cc @@ -702,25 +702,25 @@ TEST_CASE("parsing automata to intermediate representation") REQUIRE(auts.size() == 1); const mata::IntermediateAut& aut = auts.back(); REQUIRE(aut.transitions.size() == 1); - REQUIRE(aut.transitions.front().first.name == "q"); - REQUIRE(aut.transitions.front().first.is_operand()); - REQUIRE(aut.transitions.front().second.node.is_operator()); - REQUIRE(aut.transitions.front().second.node.name == "&"); - REQUIRE(aut.transitions.front().second.children.size() == 2); - REQUIRE(aut.transitions.front().second.children.front().node.is_operand()); - REQUIRE(aut.transitions.front().second.children.front().node.name == "symbol"); - REQUIRE(aut.transitions.front().second.children.front().children.empty()); - REQUIRE(aut.transitions.front().second.children[1].node.is_operand()); - REQUIRE(aut.transitions.front().second.children[1].node.name == "r"); - REQUIRE(aut.transitions.front().second.children[1].children.empty()); - REQUIRE(aut.initial_formula.node.name == "&"); - REQUIRE(aut.initial_formula.children.size() == 2); - REQUIRE(aut.initial_formula.children[0].node.name == "q"); - REQUIRE(aut.initial_formula.children[1].node.name == "r"); - REQUIRE(aut.final_formula.node.name == "|"); - REQUIRE(aut.final_formula.children.size() == 2); - REQUIRE(aut.final_formula.children[0].node.name == "q"); - REQUIRE(aut.final_formula.children[1].node.name == "r"); + REQUIRE(aut.transitions.front().first->name == "q"); + REQUIRE(aut.transitions.front().first->is_operand()); + REQUIRE(aut.transitions.front().second->node->is_operator()); + REQUIRE(aut.transitions.front().second->node->name == "&"); + REQUIRE(aut.transitions.front().second->both_children_defined()); + REQUIRE(aut.transitions.front().second->left->node->is_operand()); + REQUIRE(aut.transitions.front().second->left->node->name == "symbol"); + REQUIRE(aut.transitions.front().second->left->both_children_null()); + REQUIRE(aut.transitions.front().second->right->node->is_operand()); + REQUIRE(aut.transitions.front().second->right->node->name == "r"); + REQUIRE(aut.transitions.front().second->right->both_children_null()); + REQUIRE(aut.initial_formula->node->name == "&"); + REQUIRE(aut.initial_formula->both_children_defined()); + REQUIRE(aut.initial_formula->left->node->name == "q"); + REQUIRE(aut.initial_formula->right->node->name == "r"); + REQUIRE(aut.final_formula->node->name == "|"); + REQUIRE(aut.final_formula->both_children_defined()); + REQUIRE(aut.final_formula->left->node->name == "q"); + REQUIRE(aut.final_formula->right->node->name == "r"); } SECTION("NFA without &") @@ -736,17 +736,17 @@ TEST_CASE("parsing automata to intermediate representation") REQUIRE(auts.size() == 1); const mata::IntermediateAut& aut = auts.back(); REQUIRE(aut.transitions.size() == 1); - REQUIRE(aut.transitions.front().first.name == "q"); - REQUIRE(aut.transitions.front().first.is_operand()); - REQUIRE(aut.transitions.front().second.node.is_operator()); - REQUIRE(aut.transitions.front().second.node.name == "&"); - REQUIRE(aut.transitions.front().second.children.size() == 2); - REQUIRE(aut.transitions.front().second.children.front().node.is_operand()); - REQUIRE(aut.transitions.front().second.children.front().node.name == "symbol"); - REQUIRE(aut.transitions.front().second.children.front().children.empty()); - REQUIRE(aut.transitions.front().second.children[1].node.is_operand()); - REQUIRE(aut.transitions.front().second.children[1].node.name == "r"); - REQUIRE(aut.transitions.front().second.children[1].children.empty()); + REQUIRE(aut.transitions.front().first->name == "q"); + REQUIRE(aut.transitions.front().first->is_operand()); + REQUIRE(aut.transitions.front().second->node->is_operator()); + REQUIRE(aut.transitions.front().second->node->name == "&"); + REQUIRE(aut.transitions.front().second->both_children_defined()); + REQUIRE(aut.transitions.front().second->left->node->is_operand()); + REQUIRE(aut.transitions.front().second->left->node->name == "symbol"); + REQUIRE(aut.transitions.front().second->left->both_children_null()); + REQUIRE(aut.transitions.front().second->right->node->is_operand()); + REQUIRE(aut.transitions.front().second->right->node->name == "r"); + REQUIRE(aut.transitions.front().second->right->both_children_null()); } SECTION("NFA explicit enumeration of initials and finals") @@ -847,9 +847,9 @@ q1 \false q2 const auto auts = mata::IntermediateAut::parse_from_mf(parse_mf(file)); const mata::IntermediateAut inter_aut = auts[0]; - CHECK(inter_aut.final_formula.node.is_true()); - CHECK(inter_aut.transitions.at(0).second.children.at(0).node.is_true()); - CHECK(inter_aut.transitions.at(1).second.children.at(0).node.is_false()); + CHECK(inter_aut.final_formula->node->is_true()); + CHECK(inter_aut.transitions.at(0).second->left->node->is_true()); + CHECK(inter_aut.transitions.at(1).second->left->node->is_false()); } SECTION("AFA explicit") @@ -866,37 +866,37 @@ q1 \false q2 REQUIRE(auts.size() == 1); const mata::IntermediateAut& aut = auts.back(); REQUIRE(aut.transitions.size() == 2); - REQUIRE(aut.transitions.front().first.name == "q"); - REQUIRE(aut.transitions.front().first.is_operand()); - REQUIRE(aut.transitions.front().second.node.is_operator()); - REQUIRE(aut.transitions.front().second.node.name == "|"); - REQUIRE(aut.transitions.front().second.children.size() == 2); - REQUIRE(aut.transitions.front().second.children.front().node.is_operand()); - REQUIRE(aut.transitions.front().second.children.front().node.name == "symbol"); - REQUIRE(aut.transitions.front().second.children.front().children.empty()); - REQUIRE(aut.transitions.front().second.children[1].node.is_operator()); - REQUIRE(aut.transitions.front().second.children[1].node.name == "&"); - REQUIRE(aut.transitions.front().second.children[1].children.size() == 2); - REQUIRE(aut.transitions.front().second.children[1].children.front().node.is_operand()); - REQUIRE(aut.transitions.front().second.children[1].children.front().node.name == "other_symbol"); - REQUIRE(aut.transitions.front().second.children[1].children[1].node.is_operator()); - REQUIRE(aut.transitions.front().second.children[1].children[1].node.name == "|"); - REQUIRE(aut.transitions.front().second.children[1].children[1].children.front().node.name == "|"); - REQUIRE(aut.transitions.front().second.children[1].children[1].children[1].node.name == "s"); - REQUIRE(aut.transitions.front().second.children[1].children[1].children.front().children.front().node.name == "(r,s)"); - REQUIRE(aut.transitions.front().second.children[1].children[1].children.front().children[1].node.name == "r"); - - REQUIRE(aut.transitions[1].first.name == "r"); - REQUIRE(aut.transitions[1].first.is_operand()); - REQUIRE(aut.transitions[1].second.node.is_operator()); - REQUIRE(aut.transitions[1].second.node.name == "&"); - REQUIRE(aut.transitions[1].second.children.size() == 2); - REQUIRE(aut.transitions[1].second.children.front().node.is_operator()); - REQUIRE(aut.transitions[1].second.children.front().node.name == "!"); - REQUIRE(aut.transitions[1].second.children.front().children.front().node.name == "b"); - REQUIRE(aut.transitions[1].second.children[1].node.is_operator()); - REQUIRE(aut.transitions[1].second.children[1].node.name == "&"); - REQUIRE(aut.transitions[1].second.children[1].children.size() == 2); + REQUIRE(aut.transitions.front().first->name == "q"); + REQUIRE(aut.transitions.front().first->is_operand()); + REQUIRE(aut.transitions.front().second->node->is_operator()); + REQUIRE(aut.transitions.front().second->node->name == "|"); + REQUIRE(aut.transitions.front().second->both_children_defined()); + REQUIRE(aut.transitions.front().second->left->node->is_operand()); + REQUIRE(aut.transitions.front().second->left->node->name == "symbol"); + REQUIRE(aut.transitions.front().second->left->both_children_null()); + REQUIRE(aut.transitions.front().second->right->node->is_operator()); + REQUIRE(aut.transitions.front().second->right->node->name == "&"); + REQUIRE(aut.transitions.front().second->right->both_children_defined()); + REQUIRE(aut.transitions.front().second->right->left->node->is_operand()); + REQUIRE(aut.transitions.front().second->right->left->node->name == "other_symbol"); + REQUIRE(aut.transitions.front().second->right->right->node->is_operator()); + REQUIRE(aut.transitions.front().second->right->right->node->name == "|"); + REQUIRE(aut.transitions.front().second->right->right->left->node->name == "|"); + REQUIRE(aut.transitions.front().second->right->right->right->node->name == "s"); + REQUIRE(aut.transitions.front().second->right->right->left->left->node->name == "(r,s)"); + REQUIRE(aut.transitions.front().second->right->right->left->right->node->name == "r"); + + REQUIRE(aut.transitions[1].first->name == "r"); + REQUIRE(aut.transitions[1].first->is_operand()); + REQUIRE(aut.transitions[1].second->node->is_operator()); + REQUIRE(aut.transitions[1].second->node->name == "&"); + REQUIRE(aut.transitions[1].second->both_children_defined()); + REQUIRE(aut.transitions[1].second->left->node->is_operator()); + REQUIRE(aut.transitions[1].second->left->node->name == "!"); + REQUIRE(aut.transitions[1].second->left->left->node->name == "b"); + REQUIRE(aut.transitions[1].second->right->node->is_operator()); + REQUIRE(aut.transitions[1].second->right->node->name == "&"); + REQUIRE(aut.transitions[1].second->right->both_children_defined()); } SECTION("AFA explicit two automatic naming") @@ -930,8 +930,8 @@ q1 \false q2 parsed = parse_mf(file); std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); const mata::IntermediateAut aut = auts[0]; - REQUIRE(aut.transitions.front().first.name == "1"); - REQUIRE(aut.transitions.front().first.raw == "q1"); + REQUIRE(aut.transitions.front().first->name == "1"); + REQUIRE(aut.transitions.front().first->raw == "q1"); } @@ -946,8 +946,8 @@ q1 \false q2 parsed = parse_mf(file); std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); const mata::IntermediateAut aut = auts[0]; - REQUIRE(aut.transitions.front().first.name == "1"); - REQUIRE(aut.transitions.front().first.raw == "q1"); + REQUIRE(aut.transitions.front().first->name == "1"); + REQUIRE(aut.transitions.front().first->raw == "q1"); } SECTION("AFA explicit non existing symbol error") From d266c0822cb73b352b4d01bbd132578989c7e8e6 Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Wed, 4 Oct 2023 22:43:30 +0200 Subject: [PATCH 2/6] fixing problems in new parsing --- include/mata/parser/inter-aut.hh | 6 +++--- src/inter-aut.cc | 5 ++--- src/nfa/builder.cc | 11 ++++++++--- 3 files changed, 13 insertions(+), 9 deletions(-) diff --git a/include/mata/parser/inter-aut.hh b/include/mata/parser/inter-aut.hh index 8f4e28b47..76918a73d 100644 --- a/include/mata/parser/inter-aut.hh +++ b/include/mata/parser/inter-aut.hh @@ -188,8 +188,8 @@ namespace std { struct hash { size_t operator()(const mata::FormulaGraph &graph) const noexcept { return (std::hash{}(graph.node) + 0x9e3779b9) ^ - (std::hash()(graph.left->node) + 0x9e3779b9) ^ - (std::hash()(graph.right->node) + 0x9e3779b9); + ((graph.left == nullptr ? 0 : std::hash()(graph.left->node)) + 0x9e3779b9) ^ + ((graph.right == nullptr ? 0 : std::hash()(graph.right->node)) + 0x9e3779b9); } }; } @@ -321,7 +321,7 @@ public: void print_transitions_trees(std::ostream&) const; FormulaGraph* create_graph(FormulaNode* n) { - auto i = (graphs.insert(FormulaGraph{n})).first; + auto i = graphs.insert(FormulaGraph{n}).first; return const_cast(&*i); } diff --git a/src/inter-aut.cc b/src/inter-aut.cc index 335d6043a..b8fa4fd0b 100644 --- a/src/inter-aut.cc +++ b/src/inter-aut.cc @@ -348,6 +348,7 @@ bool has_atmost_one_auto_naming(const mata::IntermediateAut& aut) { */ mata::IntermediateAut mf_to_aut(const mata::parser::ParsedSection& section) { mata::IntermediateAut aut; + aut.init_nodes(); if (section.type.find("NFA") != std::string::npos) { aut.automaton_type = mata::IntermediateAut::AutomatonType::NFA; @@ -446,8 +447,6 @@ void mata::IntermediateAut::parse_transition(mata::IntermediateAut &aut, const s mata::FormulaNode* lhs = create_node(aut, tokens[0]); std::vector rhs(tokens.begin()+1, tokens.end()); - aut.init_nodes(); - std::vector postfix; // add implicit conjunction to NFA explicit states, i.e. p a q -> p a & q @@ -606,7 +605,7 @@ bool mata::IntermediateAut::is_graph_conjunction_of_negations(const mata::Formul while (act_graph->both_children_defined()) { // this node is conjunction and the left son is negation, otherwise returns false if (act_graph->node->is_operator() && act_graph->node->is_and() && - act_graph->left->node->is_operator() && act_graph->right->node->is_neg()) + act_graph->left->node->is_operator() && act_graph->left->node->is_neg()) act_graph = act_graph->right; else return false; diff --git a/src/nfa/builder.cc b/src/nfa/builder.cc index d6b0822c1..5040224bc 100644 --- a/src/nfa/builder.cc +++ b/src/nfa/builder.cc @@ -119,10 +119,12 @@ Nfa builder::construct(const mata::IntermediateAut& inter_aut, mata::Alphabet* a } }; - for (const auto& str : inter_aut.initial_formula->collect_node_names()) + if (inter_aut.initial_formula != nullptr) { - State state = get_state_name(str); - aut.initial.insert(state); + for (const auto &str: inter_aut.initial_formula->collect_node_names()) { + State state = get_state_name(str); + aut.initial.insert(state); + } } for (const auto& trans : inter_aut.transitions) @@ -147,6 +149,9 @@ Nfa builder::construct(const mata::IntermediateAut& inter_aut, mata::Alphabet* a } std::unordered_set final_formula_nodes; + if (inter_aut.final_formula == nullptr) + return aut; + if (!(inter_aut.final_formula->node->is_constant())) { // we do not want to parse true/false (constant) as a state so we do not collect it final_formula_nodes = inter_aut.final_formula->collect_node_names(); From 26c46ddab54874793e020f45737f85f112f028c0 Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Fri, 6 Oct 2023 00:10:07 +0200 Subject: [PATCH 3/6] not working solution for mintermization --- include/mata/parser/mintermization.hh | 6 +- src/mintermization.cc | 172 +++++++++++++------------- tests/mintermization.cc | 104 ++++++++-------- 3 files changed, 143 insertions(+), 139 deletions(-) diff --git a/include/mata/parser/mintermization.hh b/include/mata/parser/mintermization.hh index 651f03248..8123069fa 100644 --- a/include/mata/parser/mintermization.hh +++ b/include/mata/parser/mintermization.hh @@ -41,7 +41,7 @@ private: // data types OptionalBdd operator!() const; }; - using DisjunctStatesPair = std::pair; + using DisjunctStatesPair = std::pair; private: // private data members Cudd bdd_mng{}; // Manager of BDDs from lib cubdd, it allocates and manages BDDs. @@ -68,7 +68,7 @@ public: * @param graph Graph to be transformed * @return Resulting BDD */ - BDD graph_to_bdd_nfa(const FormulaGraph& graph); + BDD graph_to_bdd_nfa(const FormulaGraph* graph); /** * Transforms a graph representing formula at transition to bdd. @@ -77,7 +77,7 @@ public: * @param graph Graph to be transformed * @return Resulting BDD */ - OptionalBdd graph_to_bdd_afa(const FormulaGraph& graph); + OptionalBdd graph_to_bdd_afa(const FormulaGraph* graph); /** * Method mintermizes given automaton which has bitvector alphabet. diff --git a/src/mintermization.cc b/src/mintermization.cc index f2923598c..6a07d07e5 100644 --- a/src/mintermization.cc +++ b/src/mintermization.cc @@ -20,7 +20,7 @@ namespace { const mata::FormulaGraph* detect_state_part(const mata::FormulaGraph* node) { - if (node->node.is_state()) + if (node->node->is_state()) return node; std::vector worklist{ node}; @@ -28,25 +28,26 @@ namespace { const auto act_node = worklist.back(); assert(act_node != nullptr); worklist.pop_back(); - if (act_node->children.size() != 2) + if (!act_node->both_children_defined()) continue; - if (act_node->children.front().node.is_and() && act_node->children[1].node.is_state()) + if (act_node->left->node->is_and() && act_node->right->node->is_state()) return act_node; // ... & a1 & q1 ... & qn - else if (act_node->children.front().node.is_state() && act_node->children[1].node.is_and()) + else if (act_node->left->node->is_state() && act_node->right->node->is_and()) return act_node; // ... & a1 & q1 ... & qn - else if (act_node->children.front().node.is_state() && act_node->children[1].node.is_state()) + else if (act_node->left->node->is_state() && act_node->right->node->is_state()) return act_node; // ... & a1 & q1 & q2 - else if (act_node->children.front().node.is_state() && act_node->children[1].node.is_state()) + else if (act_node->left->node->is_state() && act_node->right->node->is_state()) return act_node; // ... & a1 & q1 & q2 - else if (act_node->node.is_operator() && act_node->children[1].node.is_state()) - return &act_node->children[1]; // a1 & q1 - else if (act_node->children.front().node.is_state() && act_node->node.is_operator()) - return &act_node->children.front(); // a1 & q1 + else if (act_node->node->is_operator() && act_node->right->node->is_state()) + return act_node->right; // a1 & q1 + else if (act_node->left->node->is_state() && act_node->node->is_operator()) + return act_node->left; // a1 & q1 else { - for (const mata::FormulaGraph& child : act_node->children) { - worklist.push_back(&child); - } + if (act_node->left != nullptr) + worklist.push_back(act_node->left); + if (act_node->right != nullptr) + worklist.push_back(act_node->right); } } @@ -61,9 +62,9 @@ void mata::Mintermization::trans_to_bdd_nfa(const IntermediateAut &aut) for (const auto& trans : aut.transitions) { // Foreach transition create a BDD const auto& symbol_part = aut.get_symbol_part_of_transition(trans); - assert((symbol_part.node.is_operator() || symbol_part.children.empty()) && + assert((symbol_part.node->is_operator() || symbol_part.both_children_null()) && "Symbol part must be either formula or single symbol"); - const BDD bdd = graph_to_bdd_nfa(symbol_part); + const BDD bdd = graph_to_bdd_nfa(&symbol_part); if (bdd.IsZero()) continue; bdds.insert(bdd); @@ -74,40 +75,37 @@ void mata::Mintermization::trans_to_bdd_nfa(const IntermediateAut &aut) void mata::Mintermization::trans_to_bdd_afa(const IntermediateAut &aut) { assert(aut.is_afa()); - +/* for (const auto& trans : aut.transitions) { - lhs_to_disjuncts_and_states[&trans.first] = std::vector(); - if (trans.second.node.is_state()) { // node from state to state - lhs_to_disjuncts_and_states[&trans.first].emplace_back(&trans.second, &trans.second); + lhs_to_disjuncts_and_states[trans.first] = std::vector(); + if (trans.second->node->is_state()) { // node from state to state + lhs_to_disjuncts_and_states[trans.first].emplace_back(trans.second, trans.second); } // split transition to disjuncts - const FormulaGraph *act_graph = &trans.second; + const FormulaGraph *act_graph = trans.second; - if (!trans.second.node.is_state() && act_graph->node.is_operator() && act_graph->node.operator_type != FormulaNode::OperatorType::OR) // there are no disjuncts - lhs_to_disjuncts_and_states[&trans.first].emplace_back(act_graph, detect_state_part( + if (!trans.second->node->is_state() && act_graph->node->is_operator() && act_graph->node->operator_type != FormulaNode::OperatorType::OR) // there are no disjuncts + lhs_to_disjuncts_and_states[trans.first].emplace_back(act_graph, detect_state_part( act_graph)); - else if (!trans.second.node.is_state()) { - while (act_graph->node.is_operator() && act_graph->node.operator_type == FormulaNode::OperatorType::OR) { + else if (!trans.second->node->is_state()) { + while (act_graph->node->is_operator() && act_graph->node->operator_type == FormulaNode::OperatorType::OR) { // map lhs to disjunct and its state formula. The content of disjunct is right son of actual graph // since the left one is a rest of formula - lhs_to_disjuncts_and_states[&trans.first].emplace_back(&act_graph->children[1], - detect_state_part( - &act_graph->children[1])); - act_graph = &(act_graph->children.front()); + lhs_to_disjuncts_and_states[trans.first].emplace_back(act_graph->right, detect_state_part( + act_graph->right)); + act_graph = act_graph->left; } // take care of last disjunct - lhs_to_disjuncts_and_states[&trans.first].emplace_back(act_graph, - detect_state_part( - act_graph)); + lhs_to_disjuncts_and_states[trans.first].emplace_back(act_graph,detect_state_part(act_graph)); } // Foreach disjunct create a BDD - for (const DisjunctStatesPair& ds_pair : lhs_to_disjuncts_and_states[&trans.first]) { + 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); + graph_to_bdd_afa(ds_pair.first); assert(bdd.type == OptionalBdd::TYPE::BDD_E); if (bdd.val.IsZero()) continue; @@ -115,6 +113,7 @@ void mata::Mintermization::trans_to_bdd_afa(const IntermediateAut &aut) bdds.insert(bdd.val); } } + */ } std::unordered_set mata::Mintermization::compute_minterms(const std::unordered_set& source_bdds) @@ -143,35 +142,34 @@ 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::OptionalBdd mata::Mintermization::graph_to_bdd_afa(const FormulaGraph *graph) { - const FormulaNode& node = graph.node; + const FormulaNode* node = graph->node; - if (node.is_operand()) { - if (node.is_state()) + 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)); + if (symbol_to_bddvar.count(node->name)) { + return OptionalBdd(symbol_to_bddvar.at(node->name)); } else { - BDD res = (node.is_true()) ? bdd_mng.bddOne() : - (node.is_false() ? bdd_mng.bddZero() : bdd_mng.bddVar()); - symbol_to_bddvar[node.name] = res; + BDD res = (node->is_true()) ? bdd_mng.bddOne() : + (node->is_false() ? bdd_mng.bddZero() : bdd_mng.bddVar()); + symbol_to_bddvar[node->name] = res; return OptionalBdd(res); } - } else if (node.is_operator()) { - if (node.operator_type == FormulaNode::OperatorType::AND) { - assert(graph.children.size() == 2); - const OptionalBdd op1 = graph_to_bdd_afa(graph.children[0]); - const OptionalBdd op2 = graph_to_bdd_afa(graph.children[1]); + } else if (node->is_operator()) { + if (node->operator_type == FormulaNode::OperatorType::AND) { + const OptionalBdd op1 = graph_to_bdd_afa(graph->left); + const OptionalBdd op2 = graph_to_bdd_afa(graph->right); 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]); + } else if (node->operator_type == FormulaNode::OperatorType::OR) { + assert(graph->both_children_defined()); + const OptionalBdd op1 = graph_to_bdd_afa(graph->left); + const OptionalBdd op2 = graph_to_bdd_afa(graph->right); 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]); + } else if (node->operator_type == FormulaNode::OperatorType::NEG) { + assert(graph->left != nullptr && graph->right == nullptr); + const OptionalBdd op1 = graph_to_bdd_afa(graph->left); return !op1; } else assert(false && "Unknown type of operation. It should conjunction, disjunction, or negation."); @@ -181,33 +179,33 @@ mata::Mintermization::OptionalBdd mata::Mintermization::graph_to_bdd_afa(const F return {}; } -BDD mata::Mintermization::graph_to_bdd_nfa(const FormulaGraph &graph) +BDD mata::Mintermization::graph_to_bdd_nfa(const FormulaGraph *graph) { - const FormulaNode& node = graph.node; + const FormulaNode* node = graph->node; - if (node.is_operand()) { - if (symbol_to_bddvar.count(node.name)) { - return symbol_to_bddvar.at(node.name); + if (node->is_operand()) { + if (symbol_to_bddvar.count(node->name)) { + return symbol_to_bddvar.at(node->name); } else { - BDD res = (node.is_true()) ? bdd_mng.bddOne() : - (node.is_false() ? bdd_mng.bddZero() : bdd_mng.bddVar()); - symbol_to_bddvar[node.name] = res; + BDD res = (node->is_true()) ? bdd_mng.bddOne() : + (node->is_false() ? bdd_mng.bddZero() : bdd_mng.bddVar()); + symbol_to_bddvar[node->name] = res; return res; } - } else if (node.is_operator()) { - if (node.operator_type == FormulaNode::OperatorType::AND) { - assert(graph.children.size() == 2); - const BDD op1 = graph_to_bdd_nfa(graph.children[0]); - const BDD op2 = graph_to_bdd_nfa(graph.children[1]); + } else if (node->is_operator()) { + if (node->operator_type == FormulaNode::OperatorType::AND) { + assert(graph->both_children_defined()); + const BDD op1 = graph_to_bdd_nfa(graph->left); + const BDD op2 = graph_to_bdd_nfa(graph->right); 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]); + } else if (node->operator_type == FormulaNode::OperatorType::OR) { + assert(graph->both_children_defined()); + const BDD op1 = graph_to_bdd_nfa(graph->left); + const BDD op2 = graph_to_bdd_nfa(graph->right); 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]); + } else if (node->operator_type == FormulaNode::OperatorType::NEG) { + assert(graph->left != nullptr && graph->right == nullptr); + const BDD op1 = graph_to_bdd_nfa(graph->left); return !op1; } else assert(false); @@ -222,20 +220,21 @@ void mata::Mintermization::minterms_to_aut_nfa(mata::IntermediateAut& res, const { for (const auto& trans : aut.transitions) { // for each t=(q1,s,q2) - const auto &symbol_part = trans.second.children[0]; + const auto &symbol_part = trans.second->left; size_t symbol = 0; - if(trans_to_bddvar.count(&symbol_part) == 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]; + const BDD &bdd = trans_to_bddvar[symbol_part]; for (const auto &minterm: minterms) { // for each minterm x: if (!((bdd * minterm).IsZero())) { // if for symbol s of t is BDD_s < x // add q1,x,q2 to transitions - IntermediateAut::parse_transition(res, {trans.first.raw, std::to_string(symbol), - trans.second.children[1].node.raw}); + std::string str_symbol = std::to_string(symbol); + IntermediateAut::parse_transition(res, {trans.first->raw, str_symbol, + trans.second->right->node->raw}); } symbol++; } @@ -246,7 +245,7 @@ void mata::Mintermization::minterms_to_aut_afa(mata::IntermediateAut& res, const const std::unordered_set& minterms) { for (const auto& trans : aut.transitions) { - for (const auto& ds_pair : lhs_to_disjuncts_and_states[&trans.first]) { + for (const auto& ds_pair : lhs_to_disjuncts_and_states[trans.first]) { // for each t=(q1,s,q2) const auto disjunct = ds_pair.first; @@ -261,10 +260,11 @@ void mata::Mintermization::minterms_to_aut_afa(mata::IntermediateAut& res, const // if for symbol s of t is BDD_s < x // add q1,x,q2 to transitions const auto str_symbol = std::to_string(symbol); - FormulaNode node_symbol(FormulaNode::Type::OPERAND, str_symbol, str_symbol, - mata::FormulaNode::OperandType::SYMBOL); + FormulaNode n = FormulaNode(FormulaNode::Type::OPERAND, str_symbol, str_symbol, + mata::FormulaNode::OperandType::SYMBOL); + FormulaNode* node_symbol = res.enpool_node(n); if (ds_pair.second != nullptr) - res.add_transition(trans.first, node_symbol, *ds_pair.second); + res.add_transition(trans.first, node_symbol, ds_pair.second); else // transition without state on the right handed side res.add_transition(trans.first, node_symbol); } @@ -296,13 +296,17 @@ std::vector mata::Mintermization::mintermize(const std::v IntermediateAut mintermized_aut = *aut; mintermized_aut.alphabet_type = IntermediateAut::AlphabetType::EXPLICIT; mintermized_aut.transitions.clear(); + mintermized_aut.graphs.clear(); + mintermized_aut.nodes.clear(); + mintermized_aut.raw_to_nodes.clear(); + mintermized_aut.init_nodes(); if (aut->is_nfa()) minterms_to_aut_nfa(mintermized_aut, *aut, minterms); else if (aut->is_afa()) minterms_to_aut_afa(mintermized_aut, *aut, minterms); - res.push_back(mintermized_aut); + res.push_back(std::move(mintermized_aut)); } return res; diff --git a/tests/mintermization.cc b/tests/mintermization.cc index c8dee29c8..20d7a7257 100644 --- a/tests/mintermization.cc +++ b/tests/mintermization.cc @@ -40,9 +40,9 @@ TEST_CASE("mata::Mintermization::trans_to_bdd_nfa") parsed = parse_mf(file); std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); 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(aut.transitions[0].first->is_operand()); + REQUIRE(aut.transitions[0].second->left->node->is_operand()); + const BDD bdd = mintermization.graph_to_bdd_nfa(aut.transitions[0].second->left); REQUIRE(bdd.nodeCount() == 2); } @@ -59,9 +59,9 @@ TEST_CASE("mata::Mintermization::trans_to_bdd_nfa") parsed = parse_mf(file); std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); 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(aut.transitions[0].second->left->node->is_operator()); + REQUIRE(aut.transitions[0].second->right->node->is_operand()); + const BDD bdd = mintermization.graph_to_bdd_nfa(aut.transitions[0].second->left); REQUIRE(bdd.nodeCount() == 3); } @@ -78,9 +78,9 @@ TEST_CASE("mata::Mintermization::trans_to_bdd_nfa") parsed = parse_mf(file); std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); 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(aut.transitions[0].second->left->node->is_operator()); + REQUIRE(aut.transitions[0].second->right->node->is_operand()); + const BDD bdd = mintermization.graph_to_bdd_nfa(aut.transitions[0].second->left); REQUIRE(bdd.nodeCount() == 4); int inputs[] = {0,0,0,0}; REQUIRE(bdd.Eval(inputs).IsOne()); @@ -108,11 +108,11 @@ TEST_CASE("mata::Mintermization::compute_minterms") parsed = parse_mf(file); std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); 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()); + REQUIRE(aut.transitions[0].second->left->node->is_operator()); + REQUIRE(aut.transitions[0].second->right->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])); + bdds.insert(mintermization.graph_to_bdd_nfa(aut.transitions[0].second->left)); + bdds.insert(mintermization.graph_to_bdd_nfa(aut.transitions[1].second->left)); auto res = mintermization.compute_minterms(bdds); REQUIRE(res.size() == 4); } @@ -131,11 +131,11 @@ TEST_CASE("mata::Mintermization::compute_minterms") parsed = parse_mf(file); std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); 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()); + REQUIRE(aut.transitions[0].second->left->node->is_operator()); + REQUIRE(aut.transitions[0].second->right->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])); + bdds.insert(mintermization.graph_to_bdd_nfa(aut.transitions[0].second->left)); + bdds.insert(mintermization.graph_to_bdd_nfa(aut.transitions[1].second->left)); auto res = mintermization.compute_minterms(bdds); REQUIRE(res.size() == 3); } @@ -158,19 +158,19 @@ TEST_CASE("mata::Mintermization::mintermization") { parsed = parse_mf(file); std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); 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()); + REQUIRE(aut.transitions[0].second->left->node->is_operator()); + REQUIRE(aut.transitions[0].second->right->node->is_operand()); const auto res = mintermization.mintermize(aut); REQUIRE(res.transitions.size() == 4); - REQUIRE(res.transitions[0].first.name == "q"); - REQUIRE(res.transitions[1].first.name == "q"); - REQUIRE(res.transitions[2].first.name == "s"); - REQUIRE(res.transitions[3].first.name == "s"); - REQUIRE(res.transitions[0].second.children[1].node.name == "r"); - REQUIRE(res.transitions[1].second.children[1].node.name == "r"); - REQUIRE(res.transitions[2].second.children[1].node.name == "t"); - REQUIRE(res.transitions[3].second.children[1].node.name == "t"); + REQUIRE(res.transitions[0].first->name == "q"); + REQUIRE(res.transitions[1].first->name == "q"); + REQUIRE(res.transitions[2].first->name == "s"); + REQUIRE(res.transitions[3].first->name == "s"); + REQUIRE(res.transitions[0].second->right->node->name == "r"); + REQUIRE(res.transitions[1].second->right->node->name == "r"); + REQUIRE(res.transitions[2].second->right->node->name == "t"); + REQUIRE(res.transitions[3].second->right->node->name == "t"); } SECTION("Mintermization NFA true and false") { @@ -187,16 +187,16 @@ TEST_CASE("mata::Mintermization::mintermization") { parsed = parse_mf(file); std::vector auts = mata::IntermediateAut::parse_from_mf(parsed); const auto &aut = auts[0]; - REQUIRE(aut.transitions[0].second.children[0].node.is_operand()); - REQUIRE(aut.transitions[0].second.children[0].node.raw == "\\true"); - REQUIRE(aut.transitions[0].second.children[1].node.is_operand()); - REQUIRE(aut.transitions[0].second.children[1].node.raw == "r"); + REQUIRE(aut.transitions[0].second->left->node->is_operand()); + REQUIRE(aut.transitions[0].second->left->node->raw == "\\true"); + REQUIRE(aut.transitions[0].second->right->node->is_operand()); + REQUIRE(aut.transitions[0].second->right->node->raw == "r"); const auto res = mintermization.mintermize(aut); REQUIRE(res.transitions.size() == 3); - REQUIRE(res.transitions[0].first.name == "q"); - REQUIRE(res.transitions[1].first.name == "q"); - REQUIRE(res.transitions[2].first.name == "r"); + REQUIRE(res.transitions[0].first->name == "q"); + REQUIRE(res.transitions[1].first->name == "q"); + REQUIRE(res.transitions[2].first->name == "r"); } SECTION("Mintermization NFA multiple") { @@ -224,24 +224,24 @@ TEST_CASE("mata::Mintermization::mintermization") { const auto res = mintermization.mintermize(auts); REQUIRE(res.size() == 2); REQUIRE(res[0].transitions.size() == 7); - REQUIRE(res[0].transitions[0].first.name == "q"); - REQUIRE(res[0].transitions[1].first.name == "q"); - REQUIRE(res[0].transitions[2].first.name == "q"); - REQUIRE(res[0].transitions[3].first.name == "q"); - REQUIRE(res[0].transitions[4].first.name == "s"); - REQUIRE(res[0].transitions[5].first.name == "s"); - REQUIRE(res[0].transitions[6].first.name == "s"); - REQUIRE(res[0].transitions[0].second.children[1].node.name == "r"); - REQUIRE(res[0].transitions[1].second.children[1].node.name == "r"); - REQUIRE(res[0].transitions[2].second.children[1].node.name == "r"); - REQUIRE(res[0].transitions[3].second.children[1].node.name == "r"); - REQUIRE(res[0].transitions[4].second.children[1].node.name == "t"); - REQUIRE(res[0].transitions[5].second.children[1].node.name == "t"); - REQUIRE(res[0].transitions[6].second.children[1].node.name == "t"); + REQUIRE(res[0].transitions[0].first->name == "q"); + REQUIRE(res[0].transitions[1].first->name == "q"); + REQUIRE(res[0].transitions[2].first->name == "q"); + REQUIRE(res[0].transitions[3].first->name == "q"); + REQUIRE(res[0].transitions[4].first->name == "s"); + REQUIRE(res[0].transitions[5].first->name == "s"); + REQUIRE(res[0].transitions[6].first->name == "s"); + REQUIRE(res[0].transitions[0].second->right->node->name == "r"); + REQUIRE(res[0].transitions[1].second->right->node->name == "r"); + REQUIRE(res[0].transitions[2].second->right->node->name == "r"); + REQUIRE(res[0].transitions[3].second->right->node->name == "r"); + REQUIRE(res[0].transitions[4].second->right->node->name == "t"); + REQUIRE(res[0].transitions[5].second->right->node->name == "t"); + REQUIRE(res[0].transitions[6].second->right->node->name == "t"); REQUIRE(res[1].transitions.size() == 2); - REQUIRE(res[1].transitions[0].first.name == "q"); - REQUIRE(res[1].transitions[1].first.name == "q"); - REQUIRE(res[1].transitions[0].second.children[1].node.name == "r"); - REQUIRE(res[1].transitions[1].second.children[1].node.name == "r"); + REQUIRE(res[1].transitions[0].first->name == "q"); + REQUIRE(res[1].transitions[1].first->name == "q"); + REQUIRE(res[1].transitions[0].second->right->node->name == "r"); + REQUIRE(res[1].transitions[1].second->right->node->name == "r"); } } // TEST_CASE("mata::Mintermization::mintermization") From f89c6714efff675584b08f349e34823e9de16393 Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Sat, 7 Oct 2023 10:53:53 +0200 Subject: [PATCH 4/6] making test passing with static data members --- include/mata/parser/inter-aut.hh | 12 +++++++++--- src/CMakeLists.txt | 3 ++- src/inter-aut.cc | 4 ++++ src/mintermization.cc | 10 +++++----- tests/CMakeLists.txt | 3 ++- tests/nfa/nfa.cc | 1 + 6 files changed, 23 insertions(+), 10 deletions(-) diff --git a/include/mata/parser/inter-aut.hh b/include/mata/parser/inter-aut.hh index 76918a73d..6e526edcb 100644 --- a/include/mata/parser/inter-aut.hh +++ b/include/mata/parser/inter-aut.hh @@ -251,9 +251,9 @@ public: std::vector symbols_names{}; std::vector nodes_names{}; - std::unordered_set nodes{}; - std::unordered_set graphs{}; - std::unordered_map raw_to_nodes{}; + static std::unordered_set nodes; + static std::unordered_set graphs; + static std::unordered_map raw_to_nodes; FormulaGraph* initial_formula{}; FormulaGraph* final_formula{}; @@ -349,6 +349,12 @@ public: raw_to_nodes["\\false"] = enpool_node(FormulaNode{ FormulaNode::Type::OPERAND, "\\false", "\\false", mata::FormulaNode::OperandType::FALSE}); } + + static void clear_static() { + graphs.clear(); + nodes.clear(); + raw_to_nodes.clear(); + } }; // class IntermediateAut. } // namespace mata. diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6cd07f76f..dc212f3de 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1,12 +1,13 @@ # create config.cc file that contains definitions of global variables (such as version, verbosity, etc.) configure_file("${CMAKE_CURRENT_SOURCE_DIR}/config.cc.in" "${CMAKE_CURRENT_BINARY_DIR}/config.cc" @ONLY) + add_library(libmata STATIC # add_library(libmata SHARED alphabet.cc "${CMAKE_CURRENT_BINARY_DIR}/config.cc" inter-aut.cc - # mintermization.cc + mintermization.cc parser.cc re2parser.cc nfa/nfa.cc diff --git a/src/inter-aut.cc b/src/inter-aut.cc index b8fa4fd0b..bdafe26bf 100644 --- a/src/inter-aut.cc +++ b/src/inter-aut.cc @@ -650,3 +650,7 @@ std::ostream& std::operator<<(std::ostream& os, const mata::IntermediateAut& int return os; } + +std::unordered_set mata::IntermediateAut::graphs{}; +std::unordered_set mata::IntermediateAut::nodes{}; +std::unordered_map mata::IntermediateAut::raw_to_nodes{}; diff --git a/src/mintermization.cc b/src/mintermization.cc index 6a07d07e5..ccd4df9d8 100644 --- a/src/mintermization.cc +++ b/src/mintermization.cc @@ -296,17 +296,17 @@ std::vector mata::Mintermization::mintermize(const std::v IntermediateAut mintermized_aut = *aut; mintermized_aut.alphabet_type = IntermediateAut::AlphabetType::EXPLICIT; mintermized_aut.transitions.clear(); - mintermized_aut.graphs.clear(); - mintermized_aut.nodes.clear(); - mintermized_aut.raw_to_nodes.clear(); - mintermized_aut.init_nodes(); + // mintermized_aut.graphs.clear(); + // mintermized_aut.nodes.clear(); + // mintermized_aut.raw_to_nodes.clear(); + // mintermized_aut.init_nodes(); if (aut->is_nfa()) minterms_to_aut_nfa(mintermized_aut, *aut, minterms); else if (aut->is_afa()) minterms_to_aut_afa(mintermized_aut, *aut, minterms); - res.push_back(std::move(mintermized_aut)); + res.push_back(mintermized_aut); } return res; diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index 6d765716c..b84ebc51f 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -6,7 +6,7 @@ add_executable(tests alphabet.cc parser.cc re2parser.cc - # mintermization.cc + mintermization.cc nfa/delta.cc nfa/nfa.cc nfa/builder.cc @@ -19,6 +19,7 @@ add_executable(tests strings/nfa-string-solving.cc ) + target_link_libraries(tests PRIVATE libmata Catch2::Catch2) # Add common compile warnings. diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc index c54e5f878..8a72ac0d0 100644 --- a/tests/nfa/nfa.cc +++ b/tests/nfa/nfa.cc @@ -774,6 +774,7 @@ TEST_CASE("mata::nfa::construct() from IntermediateAut correct calls") "q3 a6 q6\n" "q5 a7 q7\n"; + mata::IntermediateAut::clear_static(); const auto auts = mata::IntermediateAut::parse_from_mf(parse_mf(file)); inter_aut = auts[0]; From 8ced6f1eb24d88ffe8ac5de0c21ea61e6fff71e3 Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Sat, 7 Oct 2023 12:18:16 +0200 Subject: [PATCH 5/6] move things --- include/mata/parser/inter-aut.hh | 12 +++--------- src/inter-aut.cc | 6 +----- src/mintermization.cc | 10 +++++----- tests/nfa/nfa.cc | 1 - 4 files changed, 9 insertions(+), 20 deletions(-) diff --git a/include/mata/parser/inter-aut.hh b/include/mata/parser/inter-aut.hh index 6e526edcb..cea445d7d 100644 --- a/include/mata/parser/inter-aut.hh +++ b/include/mata/parser/inter-aut.hh @@ -251,9 +251,9 @@ public: std::vector symbols_names{}; std::vector nodes_names{}; - static std::unordered_set nodes; - static std::unordered_set graphs; - static std::unordered_map raw_to_nodes; + std::unordered_set nodes; + std::unordered_set graphs; + std::unordered_map raw_to_nodes; FormulaGraph* initial_formula{}; FormulaGraph* final_formula{}; @@ -349,12 +349,6 @@ public: raw_to_nodes["\\false"] = enpool_node(FormulaNode{ FormulaNode::Type::OPERAND, "\\false", "\\false", mata::FormulaNode::OperandType::FALSE}); } - - static void clear_static() { - graphs.clear(); - nodes.clear(); - raw_to_nodes.clear(); - } }; // class IntermediateAut. } // namespace mata. diff --git a/src/inter-aut.cc b/src/inter-aut.cc index bdafe26bf..bb1fa4125 100644 --- a/src/inter-aut.cc +++ b/src/inter-aut.cc @@ -649,8 +649,4 @@ std::ostream& std::operator<<(std::ostream& os, const mata::IntermediateAut& int os << "\n"; return os; -} - -std::unordered_set mata::IntermediateAut::graphs{}; -std::unordered_set mata::IntermediateAut::nodes{}; -std::unordered_map mata::IntermediateAut::raw_to_nodes{}; +} \ No newline at end of file diff --git a/src/mintermization.cc b/src/mintermization.cc index ccd4df9d8..e86e52a8c 100644 --- a/src/mintermization.cc +++ b/src/mintermization.cc @@ -275,7 +275,7 @@ void mata::Mintermization::minterms_to_aut_afa(mata::IntermediateAut& res, const } mata::IntermediateAut mata::Mintermization::mintermize(const mata::IntermediateAut& aut) { - return mintermize(std::vector { &aut})[0]; + return std::move(mintermize(std::vector { &aut})[0]); } std::vector mata::Mintermization::mintermize(const std::vector &auts) @@ -301,12 +301,12 @@ std::vector mata::Mintermization::mintermize(const std::v // mintermized_aut.raw_to_nodes.clear(); // mintermized_aut.init_nodes(); + res.push_back(mintermized_aut); + if (aut->is_nfa()) - minterms_to_aut_nfa(mintermized_aut, *aut, minterms); + minterms_to_aut_nfa(res.back(), *aut, minterms); else if (aut->is_afa()) - minterms_to_aut_afa(mintermized_aut, *aut, minterms); - - res.push_back(mintermized_aut); + minterms_to_aut_afa(res.back(), *aut, minterms); } return res; diff --git a/tests/nfa/nfa.cc b/tests/nfa/nfa.cc index 8a72ac0d0..c54e5f878 100644 --- a/tests/nfa/nfa.cc +++ b/tests/nfa/nfa.cc @@ -774,7 +774,6 @@ TEST_CASE("mata::nfa::construct() from IntermediateAut correct calls") "q3 a6 q6\n" "q5 a7 q7\n"; - mata::IntermediateAut::clear_static(); const auto auts = mata::IntermediateAut::parse_from_mf(parse_mf(file)); inter_aut = auts[0]; From 9038827112b07f4696cd6b9d42f18872aec62d93 Mon Sep 17 00:00:00 2001 From: Martin Hruska Date: Sat, 7 Oct 2023 20:11:55 +0200 Subject: [PATCH 6/6] fixing stuff --- tests-integration/src/utils/utils.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests-integration/src/utils/utils.cc b/tests-integration/src/utils/utils.cc index e85f8fd47..44391e4af 100644 --- a/tests-integration/src/utils/utils.cc +++ b/tests-integration/src/utils/utils.cc @@ -99,7 +99,7 @@ int load_intermediate_automaton( } std::vector inter_auts = mata::IntermediateAut::parse_from_mf(parsed); - out_inter_auts.push_back(inter_auts[0]); + out_inter_auts.push_back(std::move(inter_auts[0])); } catch (const std::exception& ex) { fs.close(); std::cerr << "error: " << ex.what() << "\n";