SMT-LIB 2.6 conformance, support for cvc5, and generalization for alternative SMT-solvers#609
Conversation
Pull master into cvc5
| case Some(t) => t | ||
| // Not set, so compute default value based on prover selected. | ||
| case _ => prover.toOption match { | ||
| case Some(Cvc5ProverStdIO.name) => 180 |
There was a problem hiding this comment.
Why? It seems strange to have a different default based on the prover. The description of this in line 191 is also not great.
There was a problem hiding this comment.
I changed the description in commit 2924e00 and added a comment to the file.
The default timeout for cvc5 is set to 180 since it does not support per-checks timeouts set after instantiation of the solver so any checks or saturation checks can cause the verifier to hang indefinitely.
But maybe we just let the default be 0 for all provers and we let cvc5 users deal with this themselves?
I appreciate any input on this :)
There was a problem hiding this comment.
I don't have a strong opinion here, but it seems cleaner to not "misuse" the global timeout to compensate for cvc5's lack of per-check timeouts. Please revert to a default of 0 for all provers.
| // pathConditions = other | ||
| // pathConditions.assumptions foreach prover.assume | ||
| // } | ||
| private def getProverStdIO(prover: String): ProverStdIO = prover match { |
There was a problem hiding this comment.
Could this be an enum at this point (created when parsing config flags) rather than a String?
There was a problem hiding this comment.
Letting the factory handle strings instead of anything else was primarily motivated by its simplicity.
We could create an enum and an extra ValueConverter in Config.scala that converts the strings to an enum but wouldn't we still need a factory that just matches on the enum to create new ProverStdIO objects? To me it seems like this would add another place in the code to update when introducing additional SMT solvers with no added benefits. Admittedly, I am very new to Scala so there are likely advantages that I do not see or a way to easily create a factory with enums.
If you have any suggestions on a clean/nice way to do this, I would be more than happy to introduce the changes if I have time.
There was a problem hiding this comment.
Enums (or sealed traits) have the advantage over strings that the compiler can perform exhaustiveness checks for the former. It is therefore good practice to turn strings into enums as early as possible (i.e. in the command-line parser). Another disadvantage of strings is that you always need to account for upper-/lowercase spelling.
There was a problem hiding this comment.
Great, thanks for the explanation.
I will introduce enums instead of the string factory if I have time. :)
| "min", "List", "const", | ||
|
|
||
| /* cvc5 - Transcendental operators, see https://github.com/cvc5/cvc5/blob/main/src/parser/smt2/smt2.cpp */ | ||
| "exp", "sin", "cos", "tan", "csc", "sec", "cot", "arcsin", "arccos", "arctan", "arccsc", "arcsec", "arccot", "sqrt", |
There was a problem hiding this comment.
How much of this is CVC5 specific? Are most of these also keywords to Z3? (I see some duplicates.)
There was a problem hiding this comment.
I removed any duplicates already defined for Z3 or SMTLIB in commit 6bc0d29. All the keywords I added are defined in the cvc5 source code and if used in verification will lead to an exception when running the cvc5 prover on the smt file.
| object Z3ProverStdIO { | ||
| val name = "Z3" | ||
| val minVersion = Version("4.5.0") | ||
| val maxVersion = None // Some(Version("4.5.0")) /* X.Y.Z if that is the *last supported* version */ |
There was a problem hiding this comment.
I thought there were actual problems with higher versions @mschwerhoff ?
There was a problem hiding this comment.
I cannot offer any input on this since I have not tested it. The minVersion and maxVersion are just moved from Silicon.scala and the values are kept the same.
There was a problem hiding this comment.
@Aurel300 maxVersion is currently disabled because no Z3 version really brakes Silicon - whereas Z3 prior to 4.5.0 isn't supported anymore due to configuration option changes. Currently, newer versions make a specify subset of our tests fail (old VerCors examples we suspect of matching loops), but ignoring those, newer versions are supported.
|
The CVC5 support should be tested on the CI also. |
@Aurel300 How would I go about this? |
|
@lfwa The CI file is here. Z3 is installed as part of the base "Gobra" container, I think. I don't think this includes CVC5, so it would have to be installed manually. Then, the whole test suite should be run with the (You say in the description that 100 tests fail with CVC5, so maybe this should be an optional step. @mschwerhoff Do we want to skip some tests with CVC5? Or try to find out why they are timing out and fix them?) |
3 participants
This pull request contains the following:
prover.All tests pass with the Z3 solver, but using cvc5 results in ~100 tests failing mostly due to timeouts when using quantifiers.