Move ConstantTermNormalizer #150
Open
Conversation
This file contains hidden or 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
* Move class ConstantTermNormalizer from SMTInterpol to Library-SMTLIB * Extract method * Add support for new representation of bitvector constants (ConstantTerm with BigInteger value) * Add documentation This class is currently not used by SMTInterpol. However, this class is used by several projects of Ultimate, e.g., by the SMTSolverBridge. Ultimate's projects should not depend on SMTInterpol or the SMTSolverBridge. Hence Ultimate currently duplicates this class to make the code available to its projects.
jhoenicke
reviewed
Jun 23, 2024
| } | ||
| } | ||
|
|
||
| private static Term convertConstantTerm(final Term term, final ConstantTerm ct) { |
There was a problem hiding this comment.
Why two input parameters? You can also use ct.getSort().
|
I have a few questions:
|
|
I will respond to your questions in a few days... |
schuessf
added a commit
to ultimate-pa/ultimate
that referenced
this pull request
Mar 21, 2025
Even though this class is present in SMTInterpol, it is only used by Ultimate and it was modified to fix a bug (see ddd1310 and 6d19ff8). See also ultimate-pa/smtinterpol#150
schuessf
added a commit
to ultimate-pa/ultimate
that referenced
this pull request
Mar 24, 2025
TermParseUtils requires also the fixed ConstantTermNormalizer, otherwise some tests fail. Since it cannot be imported from Library-SmtLibUtils, because of cyclic imports, I copied it as a workaround. But the long term solution should be to fix ConstantTermNormalizer in SMTInterpol, i.e., ultimate-pa/smtinterpol#150 should be revisited and merged.
schuessf
added a commit
to ultimate-pa/ultimate
that referenced
this pull request
Mar 25, 2025
Even though this class is present in SMTInterpol, it is only used by Ultimate and it was modified to fix a bug (see ddd1310 and 6d19ff8). Therefore, it was copied to Library-SmtLibUtils and SMTSolverBridge (it has to be duplicated, as there is no matching common import of those and they cannot imported by each other because of cyclic dependenices). But the long term solution should be to fix ConstantTermNormalizer in SMTInterpol, i.e., ultimate-pa/smtinterpol#150 should be revisited and merged.
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.
This class is currently not used by SMTInterpol. However, this class is used by several projects of Ultimate, e.g., by the SMTSolverBridge. Ultimate's projects should not depend on SMTInterpol or the SMTSolverBridge. Hence Ultimate currently duplicates this class to make the code available to its projects.