Add better error messages for duplicate symbols #581
Conversation
…d variable, and vice versa
MathSAT passed these tests by accident as it does not allow Ufs with boolean arguments and will throw an IllegalArgumentException. The tests expects this exception, but for a completely different reason
kfriedberger
left a comment
kfriedberger
left a comment
There was a problem hiding this comment.
Looks good to me, overall,
I have not tested it on larger scale, so maybe one could execute some CPAchecker benchmarks with the new implementation sooner or later.
| new ITermITE( | ||
| (IFormula) arg, new IIntLit(IdealInt.ZERO()), new IIntLit(IdealInt.ONE())); | ||
| } else if (!exprIsRational(arg) && functionTakesRational(i)) { | ||
| } else if (actualType.isIntegerType() && expectedType.isRationalType()) { |
There was a problem hiding this comment.
interesting. This looks simpler than before. Maybe Princess improved its API in the last years. 😄 Does this really hold for all inputs?
There was a problem hiding this comment.
No, the API didn't change. Princess uses IFunctions for function declarations and it's not always possible to get a type signature from them as they may be polymorphic. When declaring a UF symbol it's generally possible to cast the IFunction to a MonoSortedIFunction with a fixed type that can then be accessed. However, the cast doesn't always seem to work and sometimes the signature just isn't available. Because of that we're now storing the signature inside PrincessIFunctionDeclaration, which wraps around the actual IFunction. The function cache now also maps to PrincessIFunctionDeclaration, instead of IFuntion. This allows us to check for collisions when declaring a new UF symbol.. and it also has the side-effect of simplifying the code above as we can just compare the type of the arguments to the stored function type
2 participants
Hello
this PR fixes issues with name collisions on CVC4/5 and Princess. None of these solvers support variable/Uf names to be overloaded, however, checks for name collisions were missing or broken. Because of this, duplicate symbols could be declared, but the solver would still crash when trying to use these new symbols. This PR fixes the checks and makes sure that a more user-friendly error message is printed when trying to redefine an existing symbol