Skip to content

Commit

Permalink
Add a method to convert the domain to a predicate to the basic domain…
Browse files Browse the repository at this point in the history
… API.

This allows the domain to be converted to an assumption or an assertion
amongst other applications.
  • Loading branch information
martin committed Jul 24, 2018
1 parent 918e947 commit 028d8b6
Showing 1 changed file with 10 additions and 0 deletions.
10 changes: 10 additions & 0 deletions src/analyses/ai_domain.h
Original file line number Diff line number Diff line change
Expand Up @@ -119,6 +119,16 @@ class ai_domain_baset
virtual bool ai_simplify_lhs(
exprt &condition,
const namespacet &ns) const;

// Gives a Boolean condition that is true for all values represented by the
// domain. This allows domains to be converted into program invariants.
virtual exprt to_predicate(void) const
{
if(is_bottom())
return false_exprt();
else
return true_exprt();
}
};

#endif

0 comments on commit 028d8b6

Please sign in to comment.