Skip to content

BMC: LHS of SVA throughout is a state predicate #1204

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

Merged
merged 1 commit into from
Jul 16, 2025
Merged

BMC: LHS of SVA throughout is a state predicate #1204

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
5 changes: 3 additions & 2 deletions src/trans-word-level/instantiate_word_level.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -207,7 +207,7 @@ exprt instantiate(

/*******************************************************************\
Function: instantiate_property
Function: instantiate_state_predicate
Inputs:
Expand All @@ -217,11 +217,12 @@ Function: instantiate_property
\*******************************************************************/

exprt instantiate_property(
exprt instantiate_state_predicate(
const exprt &expr,
const mp_integer &current,
const mp_integer &no_timeframes)
{
PRECONDITION(expr.type().id() == ID_bool);
wl_instantiatet wl_instantiate(no_timeframes, false);
return wl_instantiate(expr, current);
}
2 changes: 1 addition & 1 deletion src/trans-word-level/instantiate_word_level.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ exprt instantiate(

// Instantiate an atomic state predicate in the given time frame.
// Must not contain next_symbol or any temporal operators.
exprt instantiate_property(
exprt instantiate_state_predicate(
const exprt &,
const mp_integer &current,
const mp_integer &no_timeframes);
Expand Down
29 changes: 6 additions & 23 deletions src/trans-word-level/property.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -511,7 +511,8 @@ static obligationst property_obligations_rec(
{
// we rely on NNF
auto &if_expr = to_if_expr(property_expr);
auto cond = instantiate_property(if_expr.cond(), current, no_timeframes);
auto cond =
instantiate_state_predicate(if_expr.cond(), current, no_timeframes);
auto obligations_true =
property_obligations_rec(if_expr.true_case(), current, no_timeframes)
.conjunction();
Expand Down Expand Up @@ -571,7 +572,8 @@ static obligationst property_obligations_rec(
{
// state formula
return obligationst{
current, instantiate_property(property_expr, current, no_timeframes)};
current,
instantiate_state_predicate(property_expr, current, no_timeframes)};
}
}
else if(property_expr.id() == ID_sva_implies)
Expand Down Expand Up @@ -739,7 +741,8 @@ static obligationst property_obligations_rec(
else
{
return obligationst{
current, instantiate_property(property_expr, current, no_timeframes)};
current,
instantiate_state_predicate(property_expr, current, no_timeframes)};
}
}

Expand All @@ -755,26 +758,6 @@ Function: property_obligations
\*******************************************************************/

obligationst property_obligations(
const exprt &property_expr,
const mp_integer &t,
const mp_integer &no_timeframes)
{
return property_obligations_rec(property_expr, t, no_timeframes);
}

/*******************************************************************\
Function: property_obligations
Inputs:
Outputs:
Purpose:
\*******************************************************************/

obligationst property_obligations(
const exprt &property_expr,
const mp_integer &no_timeframes)
Expand Down
7 changes: 0 additions & 7 deletions src/trans-word-level/property.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,11 +22,4 @@ exprt::operandst property(
/// Is the given property supported by word-level unwinding?
bool bmc_supports_property(const exprt &);

class obligationst;

obligationst property_obligations(
const exprt &,
const mp_integer &t,
const mp_integer &no_timeframes);

#endif
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 @@ -18,7 +18,6 @@ Author: Daniel Kroening, [email protected]

#include "instantiate_word_level.h"
#include "obligations.h"
#include "property.h"

// condition on counters for ocurrences of non-consecutive repetitions
exprt sequence_count_condition(
Expand Down Expand Up @@ -259,9 +258,9 @@ sequence_matchest instantiate_sequence_rec(

for(mp_integer new_t = t; new_t <= match.end_time; ++new_t)
{
auto obligations =
property_obligations(throughout.lhs(), new_t, no_timeframes);
conjuncts.push_back(obligations.conjunction().second);
auto lhs_inst =
instantiate_state_predicate(throughout.lhs(), new_t, no_timeframes);
conjuncts.push_back(lhs_inst);
}

result.emplace_back(match.end_time, conjunction(conjuncts));
Expand Down Expand Up @@ -437,7 +436,8 @@ sequence_matchest instantiate_sequence_rec(
{
// a state predicate
auto &predicate = to_sva_boolean_expr(expr).op();
auto instantiated = instantiate_property(predicate, t, no_timeframes);
auto instantiated =
instantiate_state_predicate(predicate, t, no_timeframes);
return {{t, instantiated}};
}
else
Expand Down
Loading