Port LiquidFixpoint's FQ ("new-format") tests #363
Merged
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
shingarov
force-pushed
the
fq-parser
branch
2 times, most recently
from
150cd2c to
05de807
Compare
shingarov
force-pushed
the
fq-parser
branch
3 times, most recently
from
9172dc3 to
8f68418
Compare
… NNFParser/FQParser
It's not recursive, either, so no need for Delegate.
Tok isn't recursive, either, so no need for Delegate. On the other hand, matchedParen is more generally useful than just in the context of Fixpoint so it might make sense to have it somewhere higher, but I don't feel good about adding an inst var (to which class def, really?)
Consistency with LF.
shingarov
added a commit
that referenced
this pull request
Oct 18, 2024
The initial objective of this work has been to factor common (non-Horn) elements ouf of NNFParser to FixpointParser (so that the latter would serve as a common superclass for NNFParser and FQParser, see #363). As the work progressed, two other defects became evident: nomenclature inconsistent with LiquidFixpoint, and the use of (extremely broken) matchedParen even though we already have RefinementExpressionParser. This commit addresses all three issues. This is a combination of 23 commits: Introduce FixpointParser which will serve as the common superclass of NNFParser/FQParser Pull 'fixpoint' up to FixpointParser Pull matchedParen and tok up to FixpointParser Pull lowerId, upperId up to FixpointParser class Consistently name hThing Place parens in symSort (not its senders) for consistency with LF Use naming for hCstr consistent with LF Inline cstrAnd for consistency with LF Parenthesize hBind consistently with LF Inline #forall, #exists for consistency with LF [cosmetic] Add "tag" TODO Use naming for hCstr consistent with LF Use naming for hPred consistent with LF Inline predAnd for consistency with LF Inline kappaApp, use kvSym for consistency with LF Clear up confusion between pred, hPred and decidablePred Inline #constant for consistency with LF Rename qualif to hQualifier for consistency and to avoid confusion with F.qualifierP Inline #constraint for consistency with LF Rename var to hVar for consistency with LF Pull common (i.e. non-Horn) elements from NNFParser to FixpointParser Remove #matchedParen in favor of consistent use of RefinementExpressionParser Route uses of RefinementExpressionParser through DecidableRefinement
Merged
shingarov
added a commit
that referenced
this pull request
Oct 18, 2024
The initial objective of this work has been to factor common (non-Horn) elements ouf of NNFParser to FixpointParser (so that the latter would serve as a common superclass for NNFParser and FQParser, see #363). As the work progressed, two other defects became evident: nomenclature inconsistent with LiquidFixpoint, and the use of (extremely broken) matchedParen even though we already have RefinementExpressionParser. This commit addresses all three issues. This is a combination of 23 commits: Introduce FixpointParser which will serve as the common superclass of NNFParser/FQParser Pull 'fixpoint' up to FixpointParser Pull matchedParen and tok up to FixpointParser Pull lowerId, upperId up to FixpointParser class Consistently name hThing Place parens in symSort (not its senders) for consistency with LF Use naming for hCstr consistent with LF Inline cstrAnd for consistency with LF Parenthesize hBind consistently with LF Inline #forall, #exists for consistency with LF [cosmetic] Add "tag" TODO Use naming for hCstr consistent with LF Use naming for hPred consistent with LF Inline predAnd for consistency with LF Inline kappaApp, use kvSym for consistency with LF Clear up confusion between pred, hPred and decidablePred Inline #constant for consistency with LF Rename qualif to hQualifier for consistency and to avoid confusion with F.qualifierP Inline #constraint for consistency with LF Rename var to hVar for consistency with LF Pull common (i.e. non-Horn) elements from NNFParser to FixpointParser Remove #matchedParen in favor of consistent use of RefinementExpressionParser Route uses of RefinementExpressionParser through DecidableRefinement
|
Contrary to how GitHub shows it, this PR is NOT merged; it's a zombie in an inconsistent state, so we create #368 instead. |
shingarov
added a commit
that referenced
this pull request
Oct 28, 2024
The initial objective of this work has been to factor common (non-Horn) elements ouf of NNFParser to FixpointParser (so that the latter would serve as a common superclass for NNFParser and FQParser, see #363). As the work progressed, two other defects became evident: nomenclature inconsistent with LiquidFixpoint, and the use of (extremely broken) matchedParen even though we already have RefinementExpressionParser. This commit addresses all three issues. This is a combination of 23 commits: Introduce FixpointParser which will serve as the common superclass of NNFParser/FQParser Pull 'fixpoint' up to FixpointParser Pull matchedParen and tok up to FixpointParser Pull lowerId, upperId up to FixpointParser class Consistently name hThing Place parens in symSort (not its senders) for consistency with LF Use naming for hCstr consistent with LF Inline cstrAnd for consistency with LF Parenthesize hBind consistently with LF Inline #forall, #exists for consistency with LF [cosmetic] Add "tag" TODO Use naming for hCstr consistent with LF Use naming for hPred consistent with LF Inline predAnd for consistency with LF Inline kappaApp, use kvSym for consistency with LF Clear up confusion between pred, hPred and decidablePred Inline #constant for consistency with LF Rename qualif to hQualifier for consistency and to avoid confusion with F.qualifierP Inline #constraint for consistency with LF Rename var to hVar for consistency with LF Pull common (i.e. non-Horn) elements from NNFParser to FixpointParser Remove #matchedParen in favor of consistent use of RefinementExpressionParser Route uses of RefinementExpressionParser through DecidableRefinement
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.
The "chain of tests" (as explained in the "Towards a Dynabook…" paper) follows the structure of the processing pipeline, i.e., for MachineArithmetic in particular,
meaning we have 6 kinds of tests. However, if we zoom in, we shall see an intermediate processing stage:
In March 2024, the upstream LiquidFixpoint switched to "new format" tests (e.g.
tests/pos/*.fq) where FInfos are spelled out explicitly. This PR ports these "new-format" capability to MA. This is important because much of essential functionality is covered by the "new-format" tests but not the Horn tests.