Bitwuzla: Fix performance issues in FloatingPointFormulaManagerTest #396
Conversation
…erformance by reusing the ProverEnvironment for all test values
…Test.checkIEEEFpConversion for Bitwuzla. The solver seems to have performance issues in this task." This reverts commit 2df6010
…re created for fp-to-bv casts are unique
…sh casts as side-conditions that are actually needed
…tack to avoid recalculations
src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java
Outdated
Show resolved
Hide resolved
src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java
Outdated
Show resolved
Hide resolved
| return builder.build(); | ||
| } | ||
|
|
||
| public Iterable<Term> getVariableCasts(Iterable<Term> pTerms) { |
There was a problem hiding this comment.
What does this code? This needs to be commented and explained.
There was a problem hiding this comment.
Looks like a fixedpoint iteration that collects variables from terms, and from related terms, and from their related terms,...
It is written as possibly complex code.
There was a problem hiding this comment.
Looks like a fixedpoint iteration that collects variables from terms, and from related terms, and from their related terms,..
Yes, that's the idea. Whenever a formula is pushed onto the assertion stack we need to check if it uses any variables that come from fp-to-bv casts and then include side-conditions for those casts. This needs to be done recursively until all casts are covered.
I think there are a few other solvers (like CVC5) that don't allow fp-to-bv casting? It would be possible to include this code in AbstractBitformulaManager so that it than can be used by those solvers as well.
| * @param f A function that takes values from the list and returns assertions | ||
| * @param args A list of arguments to the function | ||
| */ | ||
| private <T> void proveForAll(Function<T, BooleanFormula> f, List<T> args) |
There was a problem hiding this comment.
just styling and personal preference: switch parameters. Using the list of args upfront makes it sound like prove for all <numbers> that <function> is satisfiable.
|
Thanks for the review! I've opened a new issue about the rotations (#397). Once this has been resolved the workaround can be removed here. I've also added some more documentations about |
…a visitor" This reverts commit 328a5ec.
…nce-in-floatingpointmanagertest
src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java
Outdated
Show resolved
Hide resolved
kfriedberger
force-pushed
the
371-better-performance-in-floatingpointmanagertest
branch
2 times, most recently
from
5e90916
to
04b0a0a
Compare
The new approach has several improvements: - only analyse those constraints that are referenced in terms, - do not compare Sets for the fixed-point, but wait for an empty waitlist.
kfriedberger
force-pushed
the
371-better-performance-in-floatingpointmanagertest
branch
from
04b0a0a
to
d00c4c2
Compare
daniel-raffler
deleted the
371-better-performance-in-floatingpointmanagertest
branch
Hello,
this MR aims to fix the performance issues described in #371. The problem was not about the conversion operation itself, but about the large number of ProverEnvironments that would be created, one for each test input. We solve this by reusing the same ProverEnvironment for all inputs of the test. This also improves the performance of Z3 for those same tests.
In addition to that the MR includes a number of minor fixes:
FunctionDeclarationKindgets a new SymbolFP_REMwhich was missingBV_SHRandBV_ROL,BV_ROLI,BV_ROR,BV_RORIto the BitwuzlaFormulaCreator