BDD engine: only look for atomic propositions in supported properties #1043
Conversation
kroening
force-pushed
the
bdd-property-supported
branch
from
07e760f to
92595b3
Compare
| if(!property_supported(property.normalized_expr)) | ||
| { | ||
| property.failure("property not supported by BDD engine"); | ||
| return; | ||
| } | ||
|
|
There was a problem hiding this comment.
Should the code that follows (the code that actually does the transform to CTL) be combined with the property_supported code? That is, should property_supported right away do the transform?
There was a problem hiding this comment.
The duplication is also bugging me, but it seems even less desirable to make the creation of some new data structure a side-effect of property_supported.
There was a problem hiding this comment.
How about making property_supported (though then perhaps by the name of make_CTL_property or the likes) return a std::optional<exprt> where an unsupported property would cause {} to be returned?
| bool is_AGp(const exprt &expr) | ||
| { | ||
| return expr.id() == ID_AG && !has_temporal_operator(to_AG_expr(expr).op()); | ||
| } |
There was a problem hiding this comment.
Surprisingly, this is different from is_AGp in bdd_enginet::check_property?!
There was a problem hiding this comment.
Now clearer, avoiding labeling expressions as AGp that are just equivalent.
kroening
force-pushed
the
bdd-property-supported
branch
from
92595b3 to
5196b58
Compare
The BDD engine is changed to avoid searching unsupported properties for atomic propositions.
kroening
force-pushed
the
bdd-property-supported
branch
from
5196b58 to
6bc4a23
Compare
There was a problem hiding this comment.
Approving with the assumption that #1051 will bring about further improvements.
The BDD engine is changed to avoid searching unsupported properties for atomic propositions.