Conversation
We need to always remove quotes before accessing the variable cache. Otherwise, duplicate variables will be created for "|var|" and "var"
baierd
left a comment
baierd
left a comment
There was a problem hiding this comment.
Thanks for the fix!
I have some small requests, nothing mayor.
|
|
||
| /** Variable names (symbols) can be wrapped with "|". This function removes those chars. */ | ||
| protected static String dequote(String s) { | ||
| public String dequote(String s) { |
There was a problem hiding this comment.
We usually don't want anything from the creator publicly accessible, as the creator itself is hidden. Maybe the better move would be to make this available in the FormulaManager as a common method in a protected way for now? (Possibly a parsing/dumping util class would be helpful in the future)
There was a problem hiding this comment.
I've moved dequote to Tokenizer as it is the closest thing we have to a parsing/dumping util class
| } | ||
|
|
||
| @Test | ||
| public void testParseall_quotedSymbol() { |
There was a problem hiding this comment.
Try to stick to the Java naming scheme ;D
testParseall_quotedSymbol -> parseAllQuotedSymbolTest
There was a problem hiding this comment.
All the names in the class should be updated now
| var str = mgr.dumpFormula(f).toString(); | ||
| var g = mgr.parse(str); | ||
|
|
||
| assertThat(g).isEqualTo(f); |
There was a problem hiding this comment.
You should also assert that it was really quoted in str.
There was a problem hiding this comment.
The variable name contains a space character. So it needs to be quoted or parsing would fail. However, it's difficult to assert that as different solvers will generate different output in mgr.dumpFormula
I've now changed the test to use a fixed String as input
2 participants
Hello,
our CVC5 parsing code has an issue that allows duplicate versions of the same variable to be created. The problem is that quotes are not removed from symbols when looking them up in the variable cache. Because of a new variable may be created when looking up a quoted symbol, even though the variable already exists without the quotes