Set_mem fails on simple test

[deian]

Hey guys,

I'm running into trouble using the set membership measures. I simplified the problem to the following:

import Prelude  hiding (reverse, filter)
import Data.Set hiding (filter, split)

{-@ test :: n:Int -> (Set Int) -> { t:(Set Int) | (Set_mem n t) } @-}
test :: Int -> Set Int -> Set Int
test n addrs = insert n addrs

main = return ()

and am getting the following error:

pure.hs:6:16-29: Error: Liquid Type Mismatch

I'm running liquidhaskell with CVC4 (coudn't get it working with Z3, but I'll file a bug another time with that).

Thanks, Deian

Here is the more detailed output:

========================================================
© Copyright 2009 Regents of the University of California.
All Rights Reserved.
========================================================
.|./Unsatisfied Constraints:
 constraint:
 env  [ xsListSelector:{VV : func(1, [FAppTy (List ) @(0) ; FAppTy (List ) @(0)]) | []}
      ; x_Tuple77:{VV : func(7, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4)) @(5)) @(6) ; @(6)]) | []}
      ; x_Tuple76:{VV : func(7, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4)) @(5)) @(6) ; @(5)]) | []}
      ; x_Tuple75:{VV : func(7, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4)) @(5)) @(6) ; @(4)]) | []}
      ; x_Tuple74:{VV : func(7, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4)) @(5)) @(6) ; @(3)]) | []}
      ; x_Tuple73:{VV : func(7, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4)) @(5)) @(6) ; @(2)]) | []}
      ; x_Tuple72:{VV : func(7, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4)) @(5)) @(6) ; @(1)]) | []}
      ; x_Tuple71:{VV : func(7, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4)) @(5)) @(6) ; @(0)]) | []}
      ; x_Tuple66:{VV : func(6, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4)) @(5) ; @(5)]) | []}
      ; x_Tuple65:{VV : func(6, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4)) @(5) ; @(4)]) | []}
      ; x_Tuple64:{VV : func(6, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4)) @(5) ; @(3)]) | []}
      ; x_Tuple63:{VV : func(6, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4)) @(5) ; @(2)]) | []}
      ; x_Tuple62:{VV : func(6, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4)) @(5) ; @(1)]) | []}
      ; x_Tuple61:{VV : func(6, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4)) @(5) ; @(0)]) | []}
      ; x_Tuple55:{VV : func(5, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4) ; @(4)]) | []}
      ; x_Tuple54:{VV : func(5, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4) ; @(3)]) | []}
      ; x_Tuple53:{VV : func(5, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4) ; @(2)]) | []}
      ; x_Tuple52:{VV : func(5, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4) ; @(1)]) | []}
      ; x_Tuple51:{VV : func(5, [FAppTy (FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3)) @(4) ; @(0)]) | []}
      ; x_Tuple44:{VV : func(4, [FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3) ; @(3)]) | []}
      ; x_Tuple43:{VV : func(4, [FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3) ; @(2)]) | []}
      ; x_Tuple42:{VV : func(4, [FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3) ; @(1)]) | []}
      ; x_Tuple41:{VV : func(4, [FAppTy (FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2)) @(3) ; @(0)]) | []}
      ; x_Tuple33:{VV : func(3, [FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2) ; @(2)]) | []}
      ; x_Tuple32:{VV : func(3, [FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2) ; @(1)]) | []}
      ; x_Tuple31:{VV : func(3, [FAppTy (FAppTy (FAppTy fix##40##41# @(0)) @(1)) @(2) ; @(0)]) | []}
      ; x_Tuple22:{VV : func(2, [FAppTy (FAppTy fix##40##41# @(0)) @(1) ; @(1)]) | []}
      ; x_Tuple21:{VV : func(2, [FAppTy (FAppTy fix##40##41# @(0)) @(1) ; @(0)]) | []}
      ; x_Tuple11:{VV : func(1, [FAppTy fix##40##41# @(0) ; @(0)]) | []}
      ; xListSelector:{VV : func(1, [FAppTy (List ) @(0) ; @(0)]) | []}
      ; snd:{VV : func(2, [FAppTy (FAppTy fix##40##41# @(0)) @(1) ; @(1)]) | []}
      ; papp3:{VV : func(6, [FAppTy (FAppTy (FAppTy (Pred ) @(0)) @(1)) @(2) ; @(3) ; @(4) ; @(5) ; bool]) | []}
      ; papp2:{VV : func(4, [FAppTy (FAppTy (Pred ) @(0)) @(1) ; @(2) ; @(3) ; bool]) | []}
      ; papp1:{VV : func(1, [FAppTy (Pred ) @(0) ; @(0) ; bool]) | []}
      ; null:{VV : func(1, [FAppTy (List ) @(0) ; bool]) | []}
      ; n#a18V:{VV#155 : int | []}
      ; listElts:{VV : func(1, [FAppTy (List ) @(0) ; FAppTy (Set_Set ) @(0)]) | []}
      ; len:{VV : func(1, [FAppTy (List ) @(0) ; int]) | []}
      ; isJust:{VV : func(1, [FAppTy (Data.Maybe.Maybe ) @(0) ; bool]) | []}
      ; fst:{VV : func(2, [FAppTy (FAppTy fix##40##41# @(0)) @(1) ; @(0)]) | []}
      ; fromJust:{VV : func(1, [FAppTy (Data.Maybe.Maybe ) @(0) ; @(0)]) | []}
      ; fix#GHC.Tuple.#40##41##35#70:{VV : fix##40##41# | []}
      ; fix#GHC.Prim.#62##61##35##35#9j:{VV : func(0, [int ; int ; GHC.Types.Bool ]) | []}
      ; fix#GHC.Prim.#62##35##35#9i:{VV : func(0, [int ; int ; GHC.Types.Bool ]) | []}
      ; fix#GHC.Prim.#61##61##35##35#9k:{VV : func(0, [int ; int ; GHC.Types.Bool ]) | []}
      ; fix#GHC.Prim.#60##61##35##35#9n:{VV : func(0, [int ; int ; GHC.Types.Bool ]) | []}
      ; fix#GHC.Prim.#60##35##35#9m:{VV : func(0, [int ; int ; GHC.Types.Bool ]) | []}
      ; fix#GHC.Prim.#45##35##35#99:{VV : func(0, [int ; int ; int]) | []}
      ; fix#GHC.Prim.#43##35##35#98:{VV : func(0, [int ; int ; int]) | []}
      ; cmp:{VV : func(0, [GHC.Types.Ordering  ; GHC.Types.Ordering ]) | []}
      ; addrs#a18W:{VV#156 : FAppTy (Set_Set ) int | []}
      ; addrLen:{VV : func(0, [int ; int]) | []}
      ; Set_sub:{VV : func(1, [FAppTy (Set_Set ) @(0) ; FAppTy (Set_Set ) @(0) ; bool]) | []}
      ; Set_sng:{VV : func(1, [@(0) ; FAppTy (Set_Set ) @(0)]) | []}
      ; Set_mem:{VV : func(1, [@(0) ; FAppTy (Set_Set ) @(0) ; bool]) | []}
      ; Set_emp:{VV : func(1, [FAppTy (Set_Set ) @(0) ; bool]) | []}
      ; Set_dif:{VV : func(1, [FAppTy (Set_Set ) @(0) ; FAppTy (Set_Set ) @(0) ; FAppTy (Set_Set ) @(0)]) | []}
      ; Set_cup:{VV : func(1, [FAppTy (Set_Set ) @(0) ; FAppTy (Set_Set ) @(0) ; FAppTy (Set_Set ) @(0)]) | []}
      ; Set_cap:{VV : func(1, [FAppTy (Set_Set ) @(0) ; FAppTy (Set_Set ) @(0) ; FAppTy (Set_Set ) @(0)]) | []}
      ; Prop:{VV : func(0, [GHC.Types.Bool  ; bool]) | []}
      ; GHC.Types.LT#6S:{VV#142 : GHC.Types.Ordering  | [(cmp([VV#142]) = GHC.Types.LT#6S)]}
      ; GHC.Types.I##6c:{VV : func(0, [int ; int]) | []}
      ; GHC.Types.GT#6W:{VV#145 : GHC.Types.Ordering  | [(cmp([VV#145]) = GHC.Types.GT#6W)]}
      ; GHC.Types.EQ#6U:{VV#141 : GHC.Types.Ordering  | [(cmp([VV#141]) = GHC.Types.EQ#6U)]}
      ; GHC.Integer.Type.smallInteger#0Z:{VV : func(0, [int ; int]) | []}] 
 grd true 
 lhs {VV#F3 : FAppTy (Set_Set ) int | [(VV#F3 = Set_cup([addrs#a18W; Set_sng([n#a18V])]))]} 
 rhs {VV#F3 : FAppTy (Set_Set ) int | [Set_mem(n#a18V, VV#F3)]} 
 id 3 tag [2] // 

UNSAT
LiquidHaskell © Copyright 2009-13 Regents of the University of California. All Rights Reserved.

Warning: Couldn't do create temp directory: ./.liquid: createDirectory: already exists (File exists)

**** DONE:  Extracted Core From GHC ********************************************
 

**** DONE:  generateConstraints ************************************************
 

**** START: fixpoint ***********************************************************
 

**** DONE:  fixpoint ***********************************************************
 

**** DONE:  solve **************************************************************
 

**** DONE:  annotate ***********************************************************
 

**** UNSAFE ********************************************************************


 pure.hs:6:16-29: Error: Liquid Type Mismatch

[ranjitjhala]

Hi @deian,

unfortunately this is because only Z3 supports the set theory. (CVC4 and mathsat still don't -- I think its not yet part of the SMTLIB2 standard... though the more use cases we can round up the more they'll be persuaded to add it!) However, if you run with Z3, it should work, see:

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1399471920.hs

Can you tell me what the problem with z3 was? (It ought to work just like cvc4 and mathsat...?)

Thanks!

Ranjit.

[gridaphobe]

If you're trying to use a prebuilt Z3 binary from CodePlex, make sure you get version 4.3.2 (I think this is in the unstable section). Earlier versions of Z3 have a different command-line interface :(

On Wednesday, May 7, 2014, Ranjit Jhala notifications@github.com wrote:

Hi @deian https://github.com/deian,

unfortunately this is because only Z3 supports the set theory. (CVC4 and mathsat still don't -- I think its not yet part of the SMTLIB2 standard... though the more use cases we can round up the more they'll be persuaded to add it!) However, if you run with Z3, it should work, see:

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1399471920.hs

Can you tell me what the problem with z3 was? (It ought to work just like cvc4 and mathsat...?)

Thanks!

Ranjit.

— Reply to this email directly or view it on GitHubhttps://github.com/ucsd-progsys/liquidhaskell/issues/207#issuecomment-42431878 .

Sent from Gmail Mobile

[deian]

@ranjitjhala: I suspected that the set support was limited, thanks for the clarification.

I tried several versions of z3 (from source and Arch's pacman/yaourt); first there was the issue of unknown argument -r (I suspect this may be what @gridaphobe is referring to). With 4.3.1 I ran into:

Error setting 'MODEL.PARTIAL', reason: unknown option.
ERROR: invalid INI file
Fatal error: exception Failure("bracket hits exn: Failure("bracket hits exn: End_of_file \n") 
")

But things are working with 4.3.2 -- thanks guys!

[ranjitjhala]

Hmm. Didn't realize there was this 4.3.2 issue -- or that the source for z3 was available...

Thanks for pointing out, will update the README.

On Wed, May 7, 2014 at 4:19 PM, Deian Stefan notifications@github.comwrote:

Closed #207 https://github.com/ucsd-progsys/liquidhaskell/issues/207.

Reply to this email directly or view it on GitHubhttps://github.com/ucsd-progsys/liquidhaskell/issues/207#event-118920335 .

[ranjitjhala]

Btw, @deian -- please do shoot me an email if you get stuck elsewhere or you'd like some help. Have every intention of getting back to the nice list of problems you sent earlier this year -- but was distracted by ICFP and such!

[deian]

@ranjitjhala sounds great, thanks!