Enumtype smtlib #272
Merged
Enumtype smtlib #272
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Contributor
RipplB
commented
Jun 26, 2024
•
RipplB
commented
- Introduce domain size for types
- Introduce EnumType for enumerations
- Remove enumerated type wrappers from xsts, use EnumType directly
- Have all solver types support EnumType
- Fix Name collision checks for XSTS, enum type rework #122
- Partially solve JavaSMT term transforming: inproper handling of function declarations #270
- Fix floating point number equality simplifications, see 285b991
mondokm
requested changes
Jun 26, 2024
subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/enumtype/EnumNeqExpr.java
Outdated
Show resolved
Hide resolved
subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/enumtype/EnumType.java
Outdated
Show resolved
Hide resolved
subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/ExprSimplifier.java
Show resolved
Hide resolved
subprojects/xsts/xsts-analysis/src/test/java/hu/bme/mit/theta/xsts/analysis/XstsTest.java
Outdated
Show resolved
Hide resolved
...n/java/hu/bme/mit/theta/solver/smtlib/impl/smtinterpol/SMTInterpolSmtLibSolverInstaller.java
Show resolved
Hide resolved
...lib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/generic/GenericSmtLibSolverBinary.java
Outdated
Show resolved
Hide resolved
...olver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/impl/cvc5/CVC5SmtLibItpSolver.java
Outdated
Show resolved
Hide resolved
...s/solver/solver-smtlib/src/main/java/hu/bme/mit/theta/solver/smtlib/solver/SmtLibSolver.java
Outdated
Show resolved
Hide resolved
added 3 commits
June 29, 2024 20:17
Now the test uses solvermanagers and a constant string can be set to easily define which solver to run the tests with. If it is set to an SMTLib solver, a helper BeforeClass method checks if specified version is installed, and if not, installs it.
|
Tests fail for |
Closed
The generic smtlib solver binary checks process health after starting it. If the process didn't fail fast enough, this check reported a running status, but later calls failed. Now introduced a 50ms thread sleep after starting the process, to make sure it catches all startup fails.
NaN floating point values should not be equal to any other value. This behavior is correctly implemented in the FpLitExpr #eq and #neq methods. To utilize that, manual comparison in simplification is now swapped to call these methods, resulting in correct behaviour: (= (NaN) (NaN)) for example now simplifies to false.
mondokm
approved these changes
Jul 8, 2024
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.