Skip to content

Add an identifier-based lookup to constant_propagator_is_constantt [blocks: #3768] #3871

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

Merged
Merged
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
53 changes: 29 additions & 24 deletions src/analyses/constant_propagator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -415,36 +415,42 @@ bool constant_propagator_domaint::ai_simplify(
return partial_evaluate(values, condition, ns);
}


bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
class constant_propagator_is_constantt : public is_constantt
{
class constant_propagator_is_constantt : public is_constantt
public:
explicit constant_propagator_is_constantt(
const replace_symbolt &replace_const)
: replace_const(replace_const)
{
public:
explicit constant_propagator_is_constantt(
const replace_symbolt &replace_const)
: replace_const(replace_const)
{
}
}

protected:
bool is_constant(const exprt &expr) const override
{
if(expr.id() == ID_symbol)
{
return replace_const.replaces_symbol(
to_symbol_expr(expr).get_identifier());
}
bool is_constant(const irep_idt &id) const
{
return replace_const.replaces_symbol(id);
}

return is_constantt::is_constant(expr);
}
protected:
bool is_constant(const exprt &expr) const override
{
if(expr.id() == ID_symbol)
return is_constant(to_symbol_expr(expr).get_identifier());

return is_constantt::is_constant(expr);
}

const replace_symbolt &replace_const;
};
const replace_symbolt &replace_const;
};

bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
{
return constant_propagator_is_constantt(replace_const)(expr);
}

bool constant_propagator_domaint::valuest::is_constant(const irep_idt &id) const
{
return constant_propagator_is_constantt(replace_const).is_constant(id);
}

/// Do not call this when iterating over replace_const.expr_map!
bool constant_propagator_domaint::valuest::set_to_top(
const symbol_exprt &symbol_expr)
Expand Down Expand Up @@ -649,10 +655,9 @@ bool constant_propagator_domaint::partial_evaluate(
// if the current rounding mode is top we can
// still get a non-top result by trying all rounding
// modes and checking if the results are all the same
if(!known_values.is_constant(symbol_exprt(ID_cprover_rounding_mode_str)))
{
if(!known_values.is_constant(ID_cprover_rounding_mode_str))
return partial_evaluate_with_all_rounding_modes(known_values, expr, ns);
}

return replace_constants_and_simplify(known_values, expr, ns);
}

Expand Down
2 changes: 2 additions & 0 deletions src/analyses/constant_propagator.h
Original file line number Diff line number Diff line change
Expand Up @@ -125,6 +125,8 @@ class constant_propagator_domaint:public ai_domain_baset

bool is_constant(const exprt &expr) const;

bool is_constant(const irep_idt &id) const;

bool is_empty() const
{
return replace_const.empty();
Expand Down