zhezhouzz
commented
6 months ago It seems that there is free variable b1!12 in your showed path condition. If there is a free variable, it means the SMT solver can assign any assignment to it and can easily find a "counterexample" which fails subtyping check.
I am not sure if that it the reason, however, you can try to use functions has prefix fv (e.g., Languagez.fv_prop function lives in file syntax/prop.ml in meta branch) to check if the property has free variable.
I have add new interface ..._infer (see file typing/termsyn.ml in meta branch) which can partially infer the type of a function (you still need to provide a function refinement type, since the implementation may be a recursive function, however, the result would be the inferred type instead of the provided one). You can try it via:
dune exec -- bin/main.exe type-infer meta-config.json data/abduction/prog.mlwhich will return
Type Infer:
∅
⊢ fun (s : int) ->
(let ((x!0 : bool)) = (((s : in
...
int list) : int list) : int list) : int list) ⇨ (s:{v:int | 0 <= v}) → [v:int list | (s == 0 ∧ (lenF v) == 0) ∨ (¬s == 0 ∧ (∃x!1. ((x!1 ∧ (lenF v) == 0) ∨ (¬x!1 ∧ (∃s!1. ((0 <= s!1 ∧ s!1 == (s - 1)) ∧ (∃x!3. (((s!1 < s ∧ s!1 >= 0) ∧ 0 <= (lenF x!3) ∧ (lenF x!3) <= s!1) ∧ (∃x!4. v == (consF x!4 x!3))))))))))]that contains three types
(s:{v:int | 0 <= v}) → [v:int list | (s == 0 ∧ (lenF v) == 0)]
(s:{v:int | 0 <= v}) → [v:int list | (¬s == 0 ∧ (∃x!1. ((x!1 ∧ (lenF v) == 0)]
(s:{v:int | 0 <= v}) → [v:int list | ∃x!1. (¬x!1 ∧ (∃s!1. ((0 <= s!1 ∧ s!1 == (s - 1)) ∧ (∃x!3. (((s!1 < s ∧ s!1 >= 0) ∧ 0 <= (lenF x!3) ∧ (lenF x!3) <= s!1) ∧ (∃x!4. v == (consF x!4 x!3))))))))))]
Pat-Lafon
I discussed this with you on Tuesday. I wanted to post the queries here to get your input and clarify if there is an issue on my end or if your improved typechecker better handles this.
As a reminder, I have inferred path conditions of the form:
For the sizedlist example. Most of the existentials there are unused and I believe could be safely simplified away.
I have a target type of
[v:int list | ((∀ u, ((len v u) => ((0 <= u) ∧ (u <= size!0)))))]as provided in the specification with(0 <= size!0)in my context.The path conditions are negated using the provided
negatefunction to give versions like:I am testing the subtyping checks when I conjunct this negated path condition onto the target type. The goal is to use this to limit the input space that the final coverage needs to consider(rule out certain branches). The following is the outputted query using the meta-config.json
show queries, the result of the subtyping check(true or false), and the coverage type I was using in relation to the target type.Not that it is false in both directions. I have checked that this is not the result of a timeout in either direction. I have also checked that this has errored in some other fashion but I could be wrong. At the very least, I am looking to see whether you can replicate this on your end. Most of my other subtyping checks that I run work as expected, even using some of the other path constraints... this one just seems unusual.