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.
There was a problem hiding this comment.
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.
No i am pretty sure that that was not the case.
This is actually a funny problem; using the String should be fine in theory, but so should be using the term itself. In the former, we might have a clash of 2 sorts whose terms are not equal, but their string representation. In the later we might have the reverse. I would prefer to trust the sort terms, as they are what the solver itself uses.
| @@ -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.
There was a problem hiding this comment.
Makes sense. We should be careful to take another look if #491 is merged before this PR!
|
@daniel-raffler whats the current state of this PR? |
# Conflicts: # src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java
I think we need to decide whether we want such a workaround for CVC5 or not. We're already doing something similar in Bitwuzla to support parsing, and it seems to be working well so far. Then again it does introduce 100+ lines of extra code that are rather complex and may be hard to maintain. Other than that this PR should be complete and I did test it with CPAchecker to fix any remaining issues |
|
At some point we can simply use the independent SMTLib2 parser. Up until then its a hard choice, as CVC5 can not be fully used in some applications, but also it would add more maintenance effort. Since this has been untouched for a while, could you merge main to it and run it again with CPAchecker such that we use the parser? (e.g. CVC5 als main solver with another as interpolation solver) |
I ran the svcomp test set today. Since the cluster is still busy I could only do And here are the results for this branch: Overall I think this helps quite a bit to improve the performance of CVC5 and we can still fix any remaining bugs later |
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.