Skip to content

remove ltl_sva_to_stringt::resultt::e #1141

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 10 additions & 20 deletions src/temporal-logic/ltl_sva_to_string.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -35,53 +35,45 @@ ltl_sva_to_stringt::suffix(std::string s, const exprt &expr, modet mode)
{
auto op_rec = rec(to_unary_expr(expr).op(), mode);

auto new_e = to_unary_expr(expr);
new_e.op() = op_rec.e;

if(op_rec.p == precedencet::ATOM || op_rec.p == precedencet::SUFFIX)
return resultt{precedencet::SUFFIX, op_rec.s + s, new_e};
return resultt{precedencet::SUFFIX, op_rec.s + s};
else
return resultt{precedencet::SUFFIX, '(' + op_rec.s + ')' + s, new_e};
return resultt{precedencet::SUFFIX, '(' + op_rec.s + ')' + s};
}

ltl_sva_to_stringt::resultt
ltl_sva_to_stringt::prefix(std::string s, const exprt &expr, modet mode)
{
auto op_rec = rec(to_unary_expr(expr).op(), mode);

auto new_e = to_unary_expr(expr);
new_e.op() = op_rec.e;

if(op_rec.p == precedencet::ATOM || op_rec.p == precedencet::PREFIX)
return resultt{precedencet::PREFIX, s + op_rec.s, new_e};
return resultt{precedencet::PREFIX, s + op_rec.s};
else
return resultt{precedencet::PREFIX, s + '(' + op_rec.s + ')', new_e};
return resultt{precedencet::PREFIX, s + '(' + op_rec.s + ')'};
}

ltl_sva_to_stringt::resultt
ltl_sva_to_stringt::infix(std::string s, const exprt &expr, modet mode)
{
std::string result;
bool first = true;
exprt new_e = expr; // copy

for(auto &op : new_e.operands())
for(auto &op : expr.operands())
{
if(first)
first = false;
else
result += s;

auto op_rec = rec(op, mode);
op = op_rec.e;

if(op_rec.p == precedencet::ATOM)
result += op_rec.s;
else
result += '(' + op_rec.s + ')';
}

return resultt{precedencet::INFIX, result, new_e};
return resultt{precedencet::INFIX, result};
}

ltl_sva_to_stringt::resultt
Expand Down Expand Up @@ -110,12 +102,12 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
else if(expr.is_true())
{
// 1 is preferred, but G1 is parsed as an atom
return resultt{precedencet::ATOM, "true", expr};
return resultt{precedencet::ATOM, "true"};
}
else if(expr.is_false())
{
// 0 is preferred, but G0 is parsed as an atom
return resultt{precedencet::ATOM, "false", expr};
return resultt{precedencet::ATOM, "false"};
}
else if(expr.id() == ID_F)
{
Expand Down Expand Up @@ -297,7 +289,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
// weak closure
auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
auto op_rec = rec(sequence, SVA_SEQUENCE);
return resultt{precedencet::ATOM, '{' + op_rec.s + '}', expr};
return resultt{precedencet::ATOM, '{' + op_rec.s + '}'};
}
else if(expr.id() == ID_sva_or)
{
Expand Down Expand Up @@ -539,9 +531,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
// a0, a1, a2, a3, a4, ...
std::string s = "a" + std::to_string(number);

symbol_exprt new_e{s, expr.type()};

return resultt{precedencet::ATOM, s, new_e};
return resultt{precedencet::ATOM, s};
}
else
throw ebmc_errort{} << "cannot convert " << expr.id() << " to Buechi";
Expand Down
4 changes: 1 addition & 3 deletions src/temporal-logic/ltl_sva_to_string.h
Original file line number Diff line number Diff line change
Expand Up @@ -34,13 +34,11 @@ class ltl_sva_to_stringt

struct resultt
{
resultt(precedencet _p, std::string _s, exprt _e)
: p(_p), s(std::move(_s)), e(std::move(_e))
resultt(precedencet _p, std::string _s) : p(_p), s(std::move(_s))
{
}
precedencet p;
std::string s;
exprt e;
};

numberingt<exprt, irep_hash> atoms;
Expand Down
Loading