re-subclass Z3CAPITest #372
Closed
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
Thus, the keyword #smt2: is gone in favor of unary #smt2. This has the advantage that we don't have to lug the SymEnv as argument to unFApp, z3sort etc.
A "bind" ties a name to a (refined) type.
Liquid-Fixpoint has two grammars for tests, the "Horn format"
and the "new format". In the Horn format we write something like
``` (forall ((x int) (x>0)) ... )
and the above parses to an H.All over H.Bind, see `hBindP` in `Horn/Parse.hs`.
The "new format" for the same bind would be
``` {x: int | x > 0 }
see top-level `Parse.hs`.
Until today, we got away with simply calling them "bind" because we only
deal with the Horn format now, but introducing the "new format" leads to
confusion between the two; this commit renames those binds which mean hBind.
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
This commit is merely refactoring of existing code to make it easier to extend the list of "no-error-checked" APIs.
Some Z3 APIs don't clear error (like some dec_refs and possibly others), so it could happen that, after encounting error (and reporting it) we call another Z3 functions which does not clear it and subsequent `#errorCheck` would report an error again (see [1]). An obvious solution - not to call `#errorCheck` for those API - is bit fragile - Z3 API is not explicit about which do and which don't and this is known to change version to version. So instead, we took the approach of clearing the error - this way each (detected) error is reported only once. [1]: #348
|
Not meant for merging. This is just to see what CI will say, esp. about |
|
Bad idea. |
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.
No description provided.