raw prototype of new parser

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()
 
 

include/mata/parser/inter-aut.hh

@@ -36,111 +36,165 @@ 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<struct mata::FormulaNode> {
+        size_t operator()(const struct mata::FormulaNode &node) const noexcept {
+            return hash<string>{}(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.
  * Nodes are operators and operands of the formula.
  * 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<FormulaGraph> 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<std::string> 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<std::string> collect_node_names() const;
+
+        void print_tree(std::ostream &os) const;
+    };
+}
+
+namespace std {
+    template<>
+    struct hash<mata::FormulaGraph> {
+        size_t operator()(const mata::FormulaGraph &graph) const noexcept {
+            return (std::hash<mata::FormulaNode*>{}(graph.node) + 0x9e3779b9) ^
+                ((graph.left == nullptr ? 0 : std::hash<mata::FormulaNode*>()(graph.left->node)) + 0x9e3779b9) ^
+                ((graph.right == nullptr ? 0 : std::hash<mata::FormulaNode*>()(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<std::string> symbols_names{};
     std::vector<std::string> nodes_names{};
 
-    FormulaGraph initial_formula{};
-    FormulaGraph final_formula{};
+    std::unordered_set<FormulaNode> nodes;
+    std::unordered_set<FormulaGraph> graphs;
+    std::unordered_map<std::string, FormulaNode*> 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<std::pair<FormulaNode, FormulaGraph>> transitions{};
+    struct std::vector<std::pair<FormulaNode*, FormulaGraph*>> 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<FormulaNode, FormulaGraph>& trans) const;
+    const FormulaGraph& get_symbol_part_of_transition(const std::pair<FormulaNode*, FormulaGraph*>& 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<std::string> get_enumerated_initials() const {return initial_formula.collect_node_names();}
-    std::unordered_set<std::string> get_enumerated_finals() const {return final_formula.collect_node_names();}
+    std::unordered_set<std::string> get_enumerated_initials() const {return initial_formula->collect_node_names();}
+    std::unordered_set<std::string> 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<std::string> &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<FormulaGraph*>(&*i);
+    }
+
+    FormulaNode* enpool_node(FormulaNode& n) {
+        auto i = (nodes.insert(std::move(n))).first;
+        return const_cast<FormulaNode*>(&*i);
+    }
+
+    FormulaNode* enpool_node(FormulaNode&& n) {
+        auto i = (nodes.insert(std::move(n))).first;
+        return const_cast<FormulaNode*>(&*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.