Skip to content

add sequence_matcht::condition() #1144

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.

Sign up for GitHub

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

add sequence_matcht::condition() #1144

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
11 changes: 6 additions & 5 deletions src/trans-word-level/property.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -558,7 +558,7 @@ static obligationst property_obligations_rec(
{
// The sequence must not match.
if(!match.empty_match())
obligations.add(match.end_time, not_exprt{match.condition});
obligations.add(match.end_time, not_exprt{match.condition()});
}

return obligations;
Expand Down Expand Up @@ -629,7 +629,7 @@ static obligationst property_obligations_rec(
for(auto &rhs_obligation : rhs_obligations_rec.map)
{
auto rhs_conjunction = conjunction(rhs_obligation.second);
auto cond = implies_exprt{lhs_match_point.condition, rhs_conjunction};
auto cond = implies_exprt{lhs_match_point.condition(), rhs_conjunction};
result.add(rhs_obligation.first, cond);
}
}
Expand Down Expand Up @@ -667,7 +667,7 @@ static obligationst property_obligations_rec(
{
// relies on NNF
t = std::max(t, no_timeframes - 1);
disjuncts.push_back(match.condition);
disjuncts.push_back(match.condition());
}
else
{
Expand All @@ -676,7 +676,8 @@ static obligationst property_obligations_rec(
followed_by.consequent(), property_start, no_timeframes)
.conjunction();

disjuncts.push_back(and_exprt{match.condition, obligations_rec.second});
disjuncts.push_back(
and_exprt{match.condition(), obligations_rec.second});
t = std::max(t, obligations_rec.first);
}
}
Expand Down Expand Up @@ -704,7 +705,7 @@ static obligationst property_obligations_rec(
// empty matches are not considered
if(!match.empty_match())
{
disjuncts.push_back(match.condition);
disjuncts.push_back(match.condition());
max = std::max(max, match.end_time);
}
}
Expand Down
10 changes: 5 additions & 5 deletions src/trans-word-level/sequence.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -189,7 +189,7 @@ sequence_matchest instantiate_sequence(

for(auto &rhs_match : rhs_matches)
{
auto cond = and_exprt{lhs_match.condition, rhs_match.condition};
auto cond = and_exprt{lhs_match.condition(), rhs_match.condition()};
result.push_back({rhs_match.end_time, cond});
}
}
Expand Down Expand Up @@ -221,7 +221,7 @@ sequence_matchest instantiate_sequence(
{
result.emplace_back(
lhs_match.end_time,
and_exprt{lhs_match.condition, rhs_match.condition});
and_exprt{lhs_match.condition(), rhs_match.condition()});
}
}
}
Expand Down Expand Up @@ -276,7 +276,7 @@ sequence_matchest instantiate_sequence(

for(auto &rhs_match : rhs_matches)
{
exprt::operandst conjuncts = {rhs_match.condition};
exprt::operandst conjuncts = {rhs_match.condition()};

for(mp_integer new_t = t; new_t <= rhs_match.end_time; ++new_t)
{
Expand Down Expand Up @@ -315,7 +315,7 @@ sequence_matchest instantiate_sequence(
if(match_lhs.end_time <= match_rhs.end_time)
{
// return the rhs end_time
auto cond = and_exprt{match_lhs.condition, match_rhs.condition};
auto cond = and_exprt{match_lhs.condition(), match_rhs.condition()};
result.emplace_back(match_rhs.end_time, std::move(cond));
}
}
Expand Down Expand Up @@ -343,7 +343,7 @@ sequence_matchest instantiate_sequence(
for(auto &match_rhs : matches_rhs)
{
auto end_time = std::max(match_lhs.end_time, match_rhs.end_time);
auto cond = and_exprt{match_lhs.condition, match_rhs.condition};
auto cond = and_exprt{match_lhs.condition(), match_rhs.condition()};
result.emplace_back(std::move(end_time), std::move(cond));
}

Expand Down
11 changes: 8 additions & 3 deletions src/trans-word-level/sequence.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,22 +20,27 @@ class sequence_matcht
public:
sequence_matcht(mp_integer __end_time, exprt __condition)
: _is_empty_match(false),
end_time(std::move(__end_time)),
condition(std::move(__condition))
_condition(std::move(__condition)),
end_time(std::move(__end_time))
{
}

exprt condition() const
{
return _condition;
}

bool empty_match() const
{
return _is_empty_match;
}

protected:
bool _is_empty_match;
exprt _condition;

public:
mp_integer end_time;
exprt condition;

static sequence_matcht empty_match(mp_integer end_time)
{
Expand Down
Loading