Skip to content

Commit

Permalink
Merge pull request #326 from VeriFIT/fix_parsing_copy_constructor
Browse files Browse the repository at this point in the history 
Fix parsing copy constructor
  • Loading branch information
@Adda0
Adda0 authored Sep 11, 2023
2 parents ef71be5 + c86e0b4 commit fc708e7
Show file tree
Hide file tree
Showing 3 changed files with 102 additions and 103 deletions.
8 changes: 6 additions & 2 deletions include/mata/parser/inter-aut.hh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -108,6 +108,8 @@ public:
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&&) = default;

FormulaNode& operator=(const FormulaNode& other) = default;
FormulaNode& operator=(FormulaNode&& other) = default;
};
Expand All @@ -125,10 +127,12 @@ struct FormulaGraph {

FormulaGraph() = default;
FormulaGraph(const FormulaNode& n) : node(n), children() {}
FormulaGraph(FormulaNode&& n) : node(std::move(n)), children() {}
FormulaGraph(const FormulaGraph& g) : node(g.node), children(g.children) {}
FormulaGraph(FormulaGraph&& g) : node(std::move(g.node)), children(std::move(g.children)) {}

FormulaGraph& operator=(const mata::FormulaGraph& other) = default;
FormulaGraph& operator=(mata::FormulaGraph&& other) noexcept = default;
FormulaGraph& operator=(const mata::FormulaGraph&) = default;
FormulaGraph& operator=(mata::FormulaGraph&&) noexcept = default;

std::unordered_set<std::string> collect_node_names() const;
void print_tree(std::ostream& os) const;
Expand Down
163 changes: 80 additions & 83 deletions src/inter-aut.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,12 +92,14 @@ namespace {
return std::find(vec.begin(), vec.end(), item) != vec.end();
}

bool no_operators(const std::vector<mata::FormulaNode> nodes)
{
for (const auto& node : nodes)
if (node.is_operator())
bool no_operators(const std::vector<mata::FormulaNode>& 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()) {
return false;

}
}
return true;
}

Expand Down Expand Up @@ -128,63 +130,61 @@ namespace {
return lhs + " " + graph.node.raw + " " + rhs;
}

mata::FormulaNode create_node(const mata::IntermediateAut &mata, const std::string &token)
{
mata::FormulaNode create_node(const mata::IntermediateAut &mata, const std::string &token) {
if (is_logical_operator(token[0])) {
switch (token[0]) {
case '&':
return mata::FormulaNode{ mata::FormulaNode::Type::OPERATOR, token, token,
mata::FormulaNode::OperatorType::AND};
return { mata::FormulaNode::Type::OPERATOR, token, token,
mata::FormulaNode::OperatorType::AND };
case '|':
return mata::FormulaNode{ mata::FormulaNode::Type::OPERATOR, token, token,
mata::FormulaNode::OperatorType::OR};
return { mata::FormulaNode::Type::OPERATOR, token, token,
mata::FormulaNode::OperatorType::OR };
case '!':
return mata::FormulaNode{ mata::FormulaNode::Type::OPERATOR, token, token,
mata::FormulaNode::OperatorType::NEG};
return { mata::FormulaNode::Type::OPERATOR, token, token,
mata::FormulaNode::OperatorType::NEG };
default:
assert(false);
}
} else if (token == "(") {
return mata::FormulaNode{ mata::FormulaNode::Type::LEFT_PARENTHESIS, token};
return { mata::FormulaNode::Type::LEFT_PARENTHESIS, token};
} else if (token == ")") {
return mata::FormulaNode{ mata::FormulaNode::Type::RIGHT_PARENTHESIS, token};
return { mata::FormulaNode::Type::RIGHT_PARENTHESIS, token};
} else if (token == "true") {
return mata::FormulaNode{ mata::FormulaNode::Type::OPERAND, token, token,
return { mata::FormulaNode::Type::OPERAND, token, token,
mata::FormulaNode::OperandType::SYMBOL};
} else if (token == "false") {
return mata::FormulaNode{ mata::FormulaNode::Type::OPERAND, token, token,
return { mata::FormulaNode::Type::OPERAND, token, token,
mata::FormulaNode::OperandType::SYMBOL};
} else if (is_naming_enum(mata.state_naming) && contains(mata.states_names, token)) {
return mata::FormulaNode{ mata::FormulaNode::Type::OPERAND, token, token,
return { 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{ mata::FormulaNode::Type::OPERAND, token, token,
return { 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{ mata::FormulaNode::Type::OPERAND, token, token,
return { mata::FormulaNode::Type::OPERAND, token, token,
mata::FormulaNode::OperandType::SYMBOL};
} else if (is_naming_marker(mata.state_naming) && token[0] == 'q') {
return mata::FormulaNode{ mata::FormulaNode::Type::OPERAND, token, token.substr(1),
return { 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{ mata::FormulaNode::Type::OPERAND, token, token.substr(1),
return { 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{ mata::FormulaNode::Type::OPERAND, token, token.substr(1),
return { mata::FormulaNode::Type::OPERAND, token, token.substr(1),
mata::FormulaNode::OperandType::SYMBOL};
} else if (is_naming_auto(mata.state_naming)) {
return mata::FormulaNode{ mata::FormulaNode::Type::OPERAND, token, token,
return { mata::FormulaNode::Type::OPERAND, token, token,
mata::FormulaNode::OperandType::STATE};
} else if (is_naming_auto(mata.node_naming)) {
return mata::FormulaNode{ mata::FormulaNode::Type::OPERAND, token, token,
return { mata::FormulaNode::Type::OPERAND, token, token,
mata::FormulaNode::OperandType::NODE};
} else if (is_naming_auto(mata.symbol_naming)) {
return mata::FormulaNode{ mata::FormulaNode::Type::OPERAND, token, token,
return { mata::FormulaNode::Type::OPERAND, token, token,
mata::FormulaNode::OperandType::SYMBOL};
}

throw std::runtime_error("Unknown token " + token);
assert(false);
}

/**
Expand All @@ -207,22 +207,22 @@ namespace {
* @return A postfix notation for input
*/
std::vector<mata::FormulaNode> infix_to_postfix(
const mata::IntermediateAut &aut, const std::vector<std::string> &tokens) {
const mata::IntermediateAut &aut, const std::vector<std::string>& tokens) {
std::vector<mata::FormulaNode> opstack;
std::vector<mata::FormulaNode> output;

for (const auto& token : tokens) {
for (const std::string& token: tokens) {
mata::FormulaNode node = create_node(aut, token);
switch (node.type) {
case mata::FormulaNode::Type::OPERAND:
output.push_back(node);
output.emplace_back(std::move(node));
break;
case mata::FormulaNode::Type::LEFT_PARENTHESIS:
opstack.push_back(node);
opstack.emplace_back(std::move(node));
break;
case mata::FormulaNode::Type::RIGHT_PARENTHESIS:
while (!opstack.back().is_leftpar()) {
output.push_back(opstack.back());
output.emplace_back(std::move(opstack.back()));
opstack.pop_back();
}
opstack.pop_back();
Expand All @@ -234,18 +234,18 @@ namespace {
if (opstack[j_size_t].is_leftpar())
break;
if (lower_precedence(node.operator_type, opstack[j_size_t].operator_type)) {
output.push_back(opstack[j_size_t]);
output.emplace_back(std::move(opstack[j_size_t]));
opstack.erase(opstack.begin()+j);
}
}
opstack.push_back(node);
opstack.emplace_back(std::move(node));
break;
default: assert(false);
}
}

while (!opstack.empty()) {
output.push_back(opstack.back());
output.push_back(std::move(opstack.back()));
opstack.pop_back();
}

Expand All @@ -265,41 +265,40 @@ namespace {
* @param postfix A postfix representation of transition formula
* @return A parsed graph
*/
mata::FormulaGraph postfix_to_graph(const std::vector<mata::FormulaNode> &postfix)
{
std::vector<mata::FormulaGraph> opstack;

for (const auto& node : postfix) {
mata::FormulaGraph gr(node);
switch (node.type) {
mata::FormulaGraph postfix_to_graph(std::vector<mata::FormulaNode> postfix) {
std::vector<mata::FormulaGraph> opstack{};
opstack.reserve(4);
for (mata::FormulaNode& node: postfix) {
mata::FormulaGraph gr(std::move(node));
switch (gr.node.type) {
case mata::FormulaNode::Type::OPERAND:
opstack.push_back(gr);
opstack.emplace_back(std::move(gr));
break;
case mata::FormulaNode::Type::OPERATOR:
switch (node.operator_type) {
switch (gr.node.operator_type) {
case mata::FormulaNode::OperatorType::NEG:
assert(!opstack.empty());
gr.children.push_back(opstack.back());
gr.children.emplace_back(std::move(opstack.back()));
opstack.pop_back();
opstack.push_back(gr);
opstack.emplace_back(std::move(gr));
break;
default:
assert(opstack.size() > 1);
gr.children.push_back(opstack.back());
mata::FormulaGraph second_child{ std::move(opstack.back()) };
opstack.pop_back();
gr.children.insert(gr.children.begin(), opstack.back());
gr.children.emplace_back(std::move(opstack.back()));
opstack.pop_back();
opstack.push_back(gr);
gr.children.emplace_back(std::move(second_child));
opstack.emplace_back(std::move(gr));
}
break;
default: assert(false && "Unknown type of node");
}
}

assert(opstack.size() == 1);

return opstack.back();
}
return std::move(opstack[0]);
}

/**
* Function adds disjunction operators to a postfix form when there are no operators at all.
Expand All @@ -308,7 +307,7 @@ namespace {
* @param postfix Postfix to which operators are eventually added
* @return A postfix with eventually added operators
*/
std::vector<mata::FormulaNode> add_disjunction_implicitly(const std::vector<mata::FormulaNode> &postfix)
std::vector<mata::FormulaNode> add_disjunction_implicitly(std::vector<mata::FormulaNode> postfix)
{
if (postfix.size() == 1) // no need to add operators
return postfix;
Expand All @@ -322,14 +321,14 @@ namespace {
if (postfix.size() >= 2) {
res.push_back(postfix[0]);
res.push_back(postfix[1]);
res.push_back(mata::FormulaNode(
mata::FormulaNode::Type::OPERATOR, "|", "|", mata::FormulaNode::OperatorType::OR));
res.emplace_back(
mata::FormulaNode::Type::OPERATOR, "|", "|", mata::FormulaNode::OperatorType::OR);
}

for (size_t i = 2; i < postfix.size(); ++i) {
res.push_back(postfix[i]);
res.push_back(mata::FormulaNode(
mata::FormulaNode::Type::OPERATOR, "|", "|", mata::FormulaNode::OperatorType::OR));
res.emplace_back(
mata::FormulaNode::Type::OPERATOR, "|", "|", mata::FormulaNode::OperatorType::OR);
}

return res;
Expand All @@ -342,8 +341,7 @@ namespace {
* @param section A section of input MATA format
* @return Parsed InterAutomata representing an automaton from input.
*/
mata::IntermediateAut mf_to_aut(const mata::parser::ParsedSection &section)
{
mata::IntermediateAut mf_to_aut(const mata::parser::ParsedSection& section) {
mata::IntermediateAut aut;

if (section.type.find("NFA") != std::string::npos) {
Expand Down Expand Up @@ -381,16 +379,17 @@ namespace {
auto postfix = infix_to_postfix(aut, keypair.second);
if (no_operators(postfix)) {
aut.initial_enumerated = true;
postfix = add_disjunction_implicitly(postfix);
postfix = add_disjunction_implicitly(std::move(postfix));
}
aut.initial_formula = postfix_to_graph(postfix);
aut.initial_formula = postfix_to_graph(std::move(postfix));
} else if (key.find("Final") != std::string::npos) {
auto postfix = infix_to_postfix(aut, keypair.second);
if (no_operators(postfix)) {
postfix = add_disjunction_implicitly(postfix);
postfix = add_disjunction_implicitly(std::move(postfix));
aut.final_enumerated = true;
}
aut.final_formula = postfix_to_graph(postfix);

aut.final_formula = postfix_to_graph(std::move(postfix));;
}
}

Expand Down Expand Up @@ -435,11 +434,11 @@ size_t mata::IntermediateAut::get_number_of_disjuncts() const
* @param aut Automaton to which transition will be added.
* @param tokens Series of tokens representing transition formula
*/
void mata::IntermediateAut::parse_transition(mata::IntermediateAut &aut, const std::vector<std::string> &tokens)
void mata::IntermediateAut::parse_transition(mata::IntermediateAut &aut, const std::vector<std::string>& tokens)
{
assert(tokens.size() > 1); // transition formula has at least two items
const mata::FormulaNode lhs = create_node(aut, tokens[0]);
const std::vector<std::string> rhs(tokens.begin()+1, tokens.end());
mata::FormulaNode lhs = create_node(aut, tokens[0]);
std::vector<std::string> rhs(tokens.begin()+1, tokens.end());

std::vector<mata::FormulaNode> postfix;

Expand All @@ -449,39 +448,37 @@ 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.push_back(mata::FormulaNode{ mata::FormulaNode::Type::OPERAND, rhs[0], rhs[0],
mata::FormulaNode::OperandType::SYMBOL});
postfix.push_back(create_node(aut,rhs[1]));
postfix.emplace_back(mata::FormulaNode::Type::OPERAND, rhs[0], rhs[0], mata::FormulaNode::OperandType::SYMBOL);
postfix.emplace_back(create_node(aut, rhs[1]));
} else if (aut.alphabet_type == mata::IntermediateAut::AlphabetType::BITVECTOR) {
// this is a case where rhs state not separated by conjunction from rest of trans
postfix = infix_to_postfix(aut, std::vector<std::string>(rhs.begin(), rhs.end()-1));
postfix.push_back(create_node(aut,rhs.back()));
// This is a case where rhs state is not separated by a conjunction from the rest of the transitions.
std::string last_token{ rhs.back() };
rhs.pop_back();
postfix = infix_to_postfix(aut, rhs);
postfix.emplace_back(create_node(aut, last_token));
} else
assert(false && "Unknown NFA type");

postfix.push_back(mata::FormulaNode(
mata::FormulaNode::Type::OPERATOR, "&", "&", mata::FormulaNode::OperatorType::AND));
postfix.emplace_back(mata::FormulaNode::Type::OPERATOR, "&", "&", mata::FormulaNode::OperatorType::AND);
} else
postfix = infix_to_postfix(aut, rhs);

#ifndef NDEBUG
for (const auto& node : postfix) {
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 != ")");
}
#endif // #ifndef NDEBUG.
const mata::FormulaGraph graph = postfix_to_graph(postfix);

aut.transitions.emplace_back(lhs, graph);
aut.transitions.emplace_back(std::move(lhs), postfix_to_graph(std::move(postfix)));
}

std::unordered_set<std::string> mata::FormulaGraph::collect_node_names() const
{
std::unordered_set<std::string> res;
std::vector<const mata::FormulaGraph *> stack;

stack.push_back(reinterpret_cast<const FormulaGraph*>(&(this->node)));
stack.emplace_back(reinterpret_cast<const FormulaGraph*>(&(this->node)));
while (!stack.empty()) {
const FormulaGraph* g = stack.back();
assert(g != nullptr);
Expand Down Expand Up @@ -527,7 +524,7 @@ std::vector<mata::IntermediateAut> mata::IntermediateAut::parse_from_mf(const ma
std::vector<mata::IntermediateAut> result;
result.reserve(parsed.size());

for (const auto& parsed_section : parsed) {
for (const parser::ParsedSection& parsed_section: parsed) {
if (parsed_section.type.find("FA") == std::string::npos) {
continue;
}
Expand All @@ -553,16 +550,16 @@ void mata::IntermediateAut::add_transition(const FormulaNode& lhs, const Formula
{
FormulaNode conjunction(FormulaNode::Type::OPERATOR, "&", "&", FormulaNode::OperatorType::AND);
FormulaGraph graph(conjunction);
graph.children.push_back(FormulaGraph(symbol));
graph.children.emplace_back(symbol);
graph.children.push_back(rhs);
this->transitions.push_back(std::pair<FormulaNode, FormulaGraph>(lhs, graph));
this->transitions.emplace_back(lhs, std::move(graph));
}

void mata::IntermediateAut::add_transition(const FormulaNode& lhs, const FormulaNode& rhs)
{
assert(rhs.is_operand());
FormulaGraph graph(rhs);
this->transitions.push_back(std::pair<FormulaNode, FormulaGraph>(lhs, graph));
this->transitions.emplace_back(lhs, std::move(graph));
}

void mata::IntermediateAut::print_transitions_trees(std::ostream& os) const
Expand Down
Loading

0 comments on commit fc708e7

Please sign in to comment.