CVC5: Add parser support #474
Conversation
…s for the same symbol CVC5 seems to not always throw exceptions when there is a parse error. An error message is printed to the screen in C++, but this seems to get lost in the Java bindings.
| @Override | ||
| public Term makeVariable(Sort sort, String name) { | ||
| Term existingVar = variablesCache.get(name, sort.toString()); |
There was a problem hiding this comment.
As far as i remember i chose the string representation as it was possible to get equal sorts that were not equal, thus it was not possible to find already existing variables. Have you checked for this?
There was a problem hiding this comment.
I can look into that, but so far I've not had any issues with it. Do you still remember if it used to fail for any specific sorts?
There was a problem hiding this comment.
I went thought the git log and it seems like we switched to using the String representation here. I wasn't able to reproduce the problem with Bitvector sorts even when using the old version of the commit.
Could it be that this was linked to the parallel issues that CVC5 has? Sorts are "per thread" in CVC5 and this may have caused issues with finding existing variables in the cache.
| @@ -426,21 +424,14 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) { | |||
| getFormulaType(f), | |||
| f.getKind())); | |||
|
|
|||
| } else if (f.getKind() == Kind.VARIABLE) { | |||
There was a problem hiding this comment.
What changed that there are no more bound variables? We still support quantifiers, so there should be bound variables.
Is the kind deprecated?
There was a problem hiding this comment.
Bound variables are substituted when the quantifier is matched here. I think this makes this code unreachable as there should be no way to create a bound variable by itself? Then again it probably wouldn't hurt to leave the code in.
Hello,
this PR will add support for parsing to CVC5. The approach taken is very similar to what we're doing in the Bitwuzla code as we again have to carefully synchronize symbol definitions from the parser with those from our variable/uf cache. Note that we also included some changes to the way that CVC5 array values from the model are translate into
ValueAssignmentsfor JavaSMT. This was needed to fix tests that became possible with the new parser support.