Skip to content

Commit 608e310

Browse files
author
martin
committed
Add a method to convert the domain to a predicate to the basic domain API.
This allows the domain to be converted to an assumption or an assertion amongst other applications.
1 parent e4a0a32 commit 608e310

File tree

1 file changed

+10
-0
lines changed

1 file changed

+10
-0
lines changed

src/analyses/ai_domain.h

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -119,6 +119,16 @@ class ai_domain_baset
119119
virtual bool ai_simplify_lhs(
120120
exprt &condition,
121121
const namespacet &ns) const;
122+
123+
// Gives a Boolean condition that is true for all values represented by the
124+
// domain. This allows domains to be converted into program invariants.
125+
virtual exprt to_predicate(void) const
126+
{
127+
if(is_bottom())
128+
return false_exprt();
129+
else
130+
return true_exprt();
131+
}
122132
};
123133

124134
#endif

0 commit comments

Comments
 (0)