Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Simplify refinements whenever possible #9

Open
sgpthomas opened this issue May 31, 2023 · 1 comment
Open

Simplify refinements whenever possible #9

sgpthomas opened this issue May 31, 2023 · 1 comment
Labels
enhancement New feature or request low priority

Comments

@sgpthomas
Copy link
Collaborator

If you have 0 <= V and V <= 0 in your set of qualifiers, then you can infer refinements of the shape 0 <=V and V <= 0. We should use an SMT solver to simplify this into V == 0 even if V == 0 isn't in the set of qualifiers.

This will just make the inferred refinement types easier to read.

@dijkstracula
Copy link
Owner

Weirdly, z3's simplify nor some straightforward tactics don't seem to do the needful here: I would have thought it'd be smart enough to figure it out, but I guess I'm misunderstanding its limits or just driving it wrong:

>>> V = Int("V")
>>> simplify(And(0 <= V, V <= 0))
And(V >= 0, V <= 0)
>>>
>>> t = Tactic('solve-eqs')
>>> t(And(0 <= V, V <= 0))
[[V >= 0, V <= 0]]
>>>

Rubbing everyone's favourite CS 386L tactic on the result yields a funny result, too...

>>> t = Tactic('lia')
>>> t(And(0 <= V, V <= 0))
[[]]
>>>

Broadly, though, it's interesting to think about what sequence of tactics might be useful for our domain here. (word to the wise: z3.describe_tactics() will print out all the available ones in the REPL.)

@sgpthomas sgpthomas added enhancement New feature or request low priority labels Jul 29, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request low priority
Projects
None yet
Development

No branches or pull requests

2 participants