search

ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.2k stars 139 forks source link

Z3 required #1391

Open mhwombat opened 5 years ago

mhwombat commented 5 years ago

Installation instructions say that at least one of Z3, CVC4 or MathSat is required.

However, according to issue #1314, Z3 is required. Like the reporter of that issue, I had CVC4 installed, and it was findable on my path, but when I tried to run liquid I got an error message. Installing Z3 solved the problem. So perhaps the documentation is incorrect?

mhwombat commented 5 years ago

In case the information is useful, here's what I got when I had CVC4 installed, but not Z3.

$ liquid --version
LiquidHaskell Version 0.8.4.0, Git revision 57213512a9d69093c12d644b21dbf9da95811894
Copyright 2013-18 Regents of the University of California. All Rights Reserved.
$ cat Wombat.hs
{-@ LIQUID "--no-termination" @-}
module Wombat where

{-@ type Even = {v:Int | v mod 2 = 0} @-}

{-@ weAreEven :: [Even] @-}
weAreEven     = [(0-10), (0-4), 0, 2, 666]

weAreEven  :: [Int]
$ liquid --verbose --no-termination Wombat.hs
LiquidHaskell Version 0.8.4.0, Git revision 57213512a9d69093c12d644b21dbf9da95811894
Copyright 2013-18 Regents of the University of California. All Rights Reserved.

("Module Dependencies",[Wombat])
***************************** GHC CoreBinds ***************************
[Wombat.$trModule :: GHC.Types.Module
 [LclIdX]
 Wombat.$trModule
   = scc<CAF>
     (scc<CAF>
      (scc<CAF> GHC.Types.Module)
        (scc<CAF> (scc<CAF> GHC.Types.TrNameS) "main"#))
       (scc<CAF> (scc<CAF> GHC.Types.TrNameS) "Wombat"#),
 Wombat.weAreEven :: [GHC.Types.Int]
 [LclIdX]
 Wombat.weAreEven
   = break<2>()
     GHC.Types.:
       @ GHC.Types.Int
       (scc<CAF>
        scc<CAF>
        scc<CAF>
        scc<CAF>
        break<0>()
        (scc<CAF> GHC.Num.- @ GHC.Types.Int GHC.Num.$fNumInt)
          (GHC.Types.I# 0#) (GHC.Types.I# 10#))
       (GHC.Types.:
          @ GHC.Types.Int
          (scc<CAF>
           scc<CAF>
           scc<CAF>
           scc<CAF>
           break<1>()
           (scc<CAF> GHC.Num.- @ GHC.Types.Int GHC.Num.$fNumInt)
             (GHC.Types.I# 0#) (GHC.Types.I# 4#))
          (GHC.Types.:
             @ GHC.Types.Int
             (GHC.Types.I# 0#)
             (GHC.Types.:
                @ GHC.Types.Int
                (GHC.Types.I# 2#)
                (GHC.Types.:
                   @ GHC.Types.Int
                   (GHC.Types.I# 666#)
                   (GHC.Types.[] @ GHC.Types.Int)))))]
***************************** REC CoreBinds ***************************
[Wombat.$trModule :: GHC.Types.Module
 [LclIdX]
 Wombat.$trModule
   = scc<CAF>
     (scc<CAF>
      (scc<CAF> GHC.Types.Module)
        (scc<CAF> (scc<CAF> GHC.Types.TrNameS) "main"#))
       (scc<CAF> (scc<CAF> GHC.Types.TrNameS) "Wombat"#),
 Wombat.weAreEven :: [GHC.Types.Int]
 [LclIdX]
 Wombat.weAreEven
   = break<2>()
     GHC.Types.:
       @ GHC.Types.Int
       (scc<CAF>
        scc<CAF>
        scc<CAF>
        scc<CAF>
        break<0>()
        (scc<CAF> GHC.Num.- @ GHC.Types.Int GHC.Num.$fNumInt)
          (GHC.Types.I# 0#) (GHC.Types.I# 10#))
       (GHC.Types.:
          @ GHC.Types.Int
          (scc<CAF>
           scc<CAF>
           scc<CAF>
           scc<CAF>
           break<1>()
           (scc<CAF> GHC.Num.- @ GHC.Types.Int GHC.Num.$fNumInt)
             (GHC.Types.I# 0#) (GHC.Types.I# 4#))
          (GHC.Types.:
             @ GHC.Types.Int
             (GHC.Types.I# 0#)
             (GHC.Types.:
                @ GHC.Types.Int
                (GHC.Types.I# 2#)
                (GHC.Types.:
                   @ GHC.Types.Int
                   (GHC.Types.I# 666#)
                   (GHC.Types.[] @ GHC.Types.Int)))))]
***************************** RWR CoreBinds ***************************
[Wombat.$trModule :: GHC.Types.Module
 [LclIdX]
 Wombat.$trModule
   = scc<CAF>
     (scc<CAF>
      (scc<CAF> GHC.Types.Module)
        (scc<CAF> (scc<CAF> GHC.Types.TrNameS) "main"#))
       (scc<CAF> (scc<CAF> GHC.Types.TrNameS) "Wombat"#),
 Wombat.weAreEven :: [GHC.Types.Int]
 [LclIdX]
 Wombat.weAreEven
   = break<2>()
     GHC.Types.:
       @ GHC.Types.Int
       (scc<CAF>
        scc<CAF>
        scc<CAF>
        scc<CAF>
        break<0>()
        (scc<CAF> GHC.Num.- @ GHC.Types.Int GHC.Num.$fNumInt)
          (GHC.Types.I# 0#) (GHC.Types.I# 10#))
       (GHC.Types.:
          @ GHC.Types.Int
          (scc<CAF>
           scc<CAF>
           scc<CAF>
           scc<CAF>
           break<1>()
           (scc<CAF> GHC.Num.- @ GHC.Types.Int GHC.Num.$fNumInt)
             (GHC.Types.I# 0#) (GHC.Types.I# 4#))
          (GHC.Types.:
             @ GHC.Types.Int
             (GHC.Types.I# 0#)
             (GHC.Types.:
                @ GHC.Types.Int
                (GHC.Types.I# 2#)
                (GHC.Types.:
                   @ GHC.Types.Int
                   (GHC.Types.I# 666#)
                   (GHC.Types.[] @ GHC.Types.Int)))))]

**** DONE:  A-Normalization ****************************************************

paths = ["/home/amy/liquidhaskell/.stack-work/install/x86_64-linux-tinfo6/lts-12.2/8.4.3/share/x86_64-linux-ghc-8.4.3/liquidhaskell-0.8.4.0/include/","/home/amy/liquidhaskell/.stack-work/install/x86_64-linux-tinfo6/lts-12.2/8.4.3/share/x86_64-linux-ghc-8.4.3/liquidhaskell-0.8.4.0/include/804","."]

**** DONE:  Extracted Core using GHC *******************************************

**** DONE:  Transformed Core ***************************************************

**** DONE:  transformRecExpr ***************************************************

*************** Transform Rec Expr CoreBinds *****************
[Wombat.$trModule :: GHC.Types.Module
 [LclIdX]
 Wombat.$trModule
   = let {
       lq_anf$##7205759403792797994 :: GHC.Prim.Addr#
       [LclId]
       lq_anf$##7205759403792797994 = "main"# } in
     let {
       lq_anf$##7205759403792797995 :: GHC.Types.TrName
       [LclId]
       lq_anf$##7205759403792797995
         = (scc<CAF> GHC.Types.TrNameS) lq_anf$##7205759403792797994 } in
     let {
       lq_anf$##7205759403792797996 :: GHC.Prim.Addr#
       [LclId]
       lq_anf$##7205759403792797996 = "Wombat"# } in
     let {
       lq_anf$##7205759403792797997 :: GHC.Types.TrName
       [LclId]
       lq_anf$##7205759403792797997
         = (scc<CAF> GHC.Types.TrNameS) lq_anf$##7205759403792797996 } in
     scc<CAF>
     (scc<CAF>
      (scc<CAF> GHC.Types.Module)
        (scc<CAF> lq_anf$##7205759403792797995))
       (scc<CAF> lq_anf$##7205759403792797997),
 Wombat.weAreEven :: [GHC.Types.Int]
 [LclIdX]
 Wombat.weAreEven
   = let {
       lq_anf$##7205759403792797998 :: GHC.Types.Int
       [LclId]
       lq_anf$##7205759403792797998 = GHC.Types.I# 0# } in
     let {
       lq_anf$##7205759403792797999 :: GHC.Types.Int
       [LclId]
       lq_anf$##7205759403792797999 = GHC.Types.I# 10# } in
     let {
       lq_anf$##7205759403792798000 :: GHC.Types.Int
       [LclId]
       lq_anf$##7205759403792798000
         = (scc<CAF> GHC.Num.- @ GHC.Types.Int GHC.Num.$fNumInt)
             lq_anf$##7205759403792797998 lq_anf$##7205759403792797999 } in
     let {
       lq_anf$##7205759403792798001 :: GHC.Types.Int
       [LclId]
       lq_anf$##7205759403792798001 = GHC.Types.I# 0# } in
     let {
       lq_anf$##7205759403792798002 :: GHC.Types.Int
       [LclId]
       lq_anf$##7205759403792798002 = GHC.Types.I# 4# } in
     let {
       lq_anf$##7205759403792798003 :: GHC.Types.Int
       [LclId]
       lq_anf$##7205759403792798003
         = (scc<CAF> GHC.Num.- @ GHC.Types.Int GHC.Num.$fNumInt)
             lq_anf$##7205759403792798001 lq_anf$##7205759403792798002 } in
     let {
       lq_anf$##7205759403792798004 :: GHC.Types.Int
       [LclId]
       lq_anf$##7205759403792798004 = GHC.Types.I# 0# } in
     let {
       lq_anf$##7205759403792798005 :: GHC.Types.Int
       [LclId]
       lq_anf$##7205759403792798005 = GHC.Types.I# 2# } in
     let {
       lq_anf$##7205759403792798006 :: GHC.Types.Int
       [LclId]
       lq_anf$##7205759403792798006 = GHC.Types.I# 666# } in
     let {
       lq_anf$##7205759403792798007 :: [GHC.Types.Int]
       [LclId]
       lq_anf$##7205759403792798007 = GHC.Types.[] @ GHC.Types.Int } in
     let {
       lq_anf$##7205759403792798008 :: [GHC.Types.Int]
       [LclId]
       lq_anf$##7205759403792798008
         = GHC.Types.:
             @ GHC.Types.Int
             lq_anf$##7205759403792798006
             lq_anf$##7205759403792798007 } in
     let {
       lq_anf$##7205759403792798009 :: [GHC.Types.Int]
       [LclId]
       lq_anf$##7205759403792798009
         = GHC.Types.:
             @ GHC.Types.Int
             lq_anf$##7205759403792798005
             lq_anf$##7205759403792798008 } in
     let {
       lq_anf$##7205759403792798010 :: [GHC.Types.Int]
       [LclId]
       lq_anf$##7205759403792798010
         = GHC.Types.:
             @ GHC.Types.Int
             lq_anf$##7205759403792798004
             lq_anf$##7205759403792798009 } in
     let {
       lq_anf$##7205759403792798011 :: [GHC.Types.Int]
       [LclId]
       lq_anf$##7205759403792798011
         = GHC.Types.:
             @ GHC.Types.Int
             (scc<CAF>
              scc<CAF> scc<CAF> scc<CAF> break<1>() lq_anf$##7205759403792798003)
             lq_anf$##7205759403792798010 } in
     break<2>()
     GHC.Types.:
       @ GHC.Types.Int
       (scc<CAF>
        scc<CAF> scc<CAF> scc<CAF> break<0>() lq_anf$##7205759403792798000)
       lq_anf$##7205759403792798011]
Number of partitions : 1
number of cores      : Nothing
minimum part size    : 500
maximum part size    : 700

**** DONE:  Uniqify & Rename ***************************************************

**** DONE:  Worklist Initialize ************************************************

Working   0% [.................................................................]
SMT READ 25% [=================
liquid: 
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************
SMTREAD:string
**** ERROR *********************************************************************
**** ERROR *********************************************************************
**** ERROR *********************************************************************

CallStack (from HasCallStack):
  error, called at src/Language/Fixpoint/Misc.hs:154:14 in liquid-fixpoint-0.8.0.1-5lBHQ0phVgG9Ya0ErK2yUa:Language.Fixpoint.Misc
  errorstar, called at src/Language/Fixpoint/Smt/Interface.hs:177:16 in liquid-fixpoint-0.8.0.1-5lBHQ0phVgG9Ya0ErK2yUa:Language.Fixpoint.Smt.Interface
ranjitjhala commented 5 years ago

Thanks for pointing this out @mhwombat ! Will fix either the code or docs. More likely the former, looks like some "hard" Z3 dependency has crept in...

facundominguez commented 5 months ago

With the latest LH, we get a panic. If I try the example in liquid fixpoint I get:

$ cabal exec fixpoint -- .liquid/Test.hs.bfq --solver=cvc4

Liquid-Fixpoint Copyright 2013-21 Regents of the University of California.
All Rights Reserved.

Working   4% [===..............................................................]
Crash!: :1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "Parse Error: Symbol 'strLen' not declared as a variable  ...GHC.Types.EQ))(assert (= (strLen lit$36$Main) 4))(assert (= (strLen li...                               ^"
CRASH: -1
clayrat commented 5 months ago

I think at this point we should aim to support CVC5. The theory of strings should be quite similar in both Z3 and CVC5, so this is probably just some encoding artifact. However AFAIU the current treatment of Sets/Maps in liquid-fixpoint couples us to Z3 - this is because CVC5 doesn't support map operator over arrays which we use to express most of set operations, instead it has dedicated theories for Sets and Bags. I'm planning to refactor our Maps in the coming weeks by splitting them into Maps proper and Bags, the next step would be to start parameterizing the elaboration process over supported solver theories, which would give us CVC5 support back.