Princess: Add work-around for parsing issues#684
Conversation
…he variable caches We used to rely on a visitor to collect new symbols after parsing, so that they can be added to our variable cache. However, Princess will often use epsilon terms in its formula, which are not supported by JavaSMT and may lead to crashes in the visitor. By extending the variable caches with the symbols that were returned by the solver we try to work around this problem Note, that this slightly changes the behavior, and that we're now also adding variables to the cache that were declared in the SMTLIB input but never used
|
@daniel-raffler would you be so kind and run this, as well as the previous version in CPAchecker to evaluate the changes and make sure there are no regressions? BMC-Incremental + something that uses interpolation (IMC or Predicate Abstraction) seems reasonable. I propose the ReachSafety category without Floats (due to Princess not supporting them) + setting Floats to UNSUPPORTED to speed things up. Note: Apollon is currently blocked. You need to use other CPU models! |
| for (ConstantTerm constant : constants.keySet()) { | ||
| sortedVariablesCache.put(constant.name(), new IConstant(constant)); | ||
| } | ||
| for (Predicate predicate : nullaryPredicates.keySet()) { |
There was a problem hiding this comment.
Note: Predicates may not always be just boolean variables! We should add a check so that we know whether they are not! This is especially important since we are adding Eldarica currently on the basis of Princess, and it uses quantified constructs a lot (and those might be predicates!).
There was a problem hiding this comment.
Good point! I've added a check now
Hello Daniel, |
You could run Predicate Abstraction (mainly because you already used IMC) with a distinct solver used for interpolation if you want to be thorough. |
Thanks for the hint! I've now run predicate analysis with MathSAT5 for interpolation (link) and the results also appear to be good |
2 participants
Hello,
this PR fixes some parsing issues in Princess. We've so far used a visitor to collect terms after parsing, so that they can be added to the variable cache. This can cause crashes as Princess will often rewrite formulas with epsilon terms, and epsilon terms are not supported by our visitor. To avoid the issue, this PR now switches to getting the parsed symbols from the parser itself