liquid-fixpoint 0.9.0.2.1 → 0.9.2.5

raw patch · 31 files changed

+906/−562 lines, 31 filesdep +smtlib-backendsdep +smtlib-backends-processdep +smtlib-backends-z3dep ~bytestringdep ~tastynew-uploaderPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: smtlib-backends, smtlib-backends-process, smtlib-backends-z3, typed-process

Dependency ranges changed: bytestring, tasty

API changes (from Hackage documentation)

Files

• liquid-fixpoint.cabal +18/−4
• src-cond/with-z3/Language/Fixpoint/Conditional/Z3.hs +12/−0
• src-cond/without-z3/Language/Fixpoint/Conditional/Z3.hs +7/−0
• src/Language/Fixpoint/Horn/Info.hs +97/−7
• src/Language/Fixpoint/Horn/Parse.hs +7/−0
• src/Language/Fixpoint/Horn/Types.hs +1/−1
• src/Language/Fixpoint/Misc.hs +6/−4
• src/Language/Fixpoint/Parse.hs +19/−13
• src/Language/Fixpoint/Smt/Bitvector.hs +0/−70
• src/Language/Fixpoint/Smt/Interface.hs +111/−186
• src/Language/Fixpoint/Smt/Serialize.hs +23/−24
• src/Language/Fixpoint/Smt/Theories.hs +286/−99
• src/Language/Fixpoint/Smt/Types.hs +8/−13
• src/Language/Fixpoint/Solver.hs +5/−5
• src/Language/Fixpoint/Solver/Instantiate.hs +3/−3
• src/Language/Fixpoint/Solver/Monad.hs +6/−10
• src/Language/Fixpoint/Solver/PLE.hs +14/−15
• src/Language/Fixpoint/Solver/Sanitize.hs +1/−1
• src/Language/Fixpoint/SortCheck.hs +1/−0
• src/Language/Fixpoint/Types/Config.hs +36/−9
• src/Language/Fixpoint/Types/Constraints.hs +3/−2
• src/Language/Fixpoint/Types/Names.hs +36/−20
• src/Language/Fixpoint/Types/PrettyPrint.hs +5/−0
• src/Language/Fixpoint/Types/Refinements.hs +8/−2
• src/Language/Fixpoint/Types/Sorts.hs +24/−15
• src/Language/Fixpoint/Types/Theories.hs +1/−8
• src/Language/Fixpoint/Utils/Builder.hs +5/−45
• tests/pos/bitvec-ii.fq +65/−0
• tests/pos/bitvec.fq +89/−0
• tests/pos/meas00.fq +2/−3
• tests/test.hs +7/−3

@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               liquid-fixpoint-version:            0.9.0.2.1+version:            0.9.2.5 synopsis:           Predicate Abstraction-based Horn-Clause/Implication Constraint Solver description:   This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint@@ -41,6 +41,11 @@   type: git   location: https://github.com/ucsd-progsys/liquid-fixpoint +flag link-z3-as-a-library+  description: link z3 as a library for faster interactions with the SMT solver+  manual: True+  default: False+ flag devel   description: turn on stricter error reporting for development   manual: True@@ -49,6 +54,7 @@ library   import: warnings   exposed-modules:  Data.ShareMap+                    Language.Fixpoint.Conditional.Z3                     Language.Fixpoint.Defunctionalize                     Language.Fixpoint.Graph                     Language.Fixpoint.Graph.Deps@@ -64,7 +70,6 @@                     Language.Fixpoint.Minimize                     Language.Fixpoint.Misc                     Language.Fixpoint.Parse-                    Language.Fixpoint.Smt.Bitvector                     Language.Fixpoint.Smt.Interface                     Language.Fixpoint.Smt.Serialize                     Language.Fixpoint.Smt.Theories@@ -128,7 +133,7 @@                   , base                 >= 4.9.1.0 && < 5                   , binary                   , boxes-                  , bytestring+                  , bytestring >= 0.10.2.1                   , cereal                   , cmdargs                   , containers@@ -145,7 +150,10 @@                   , parser-combinators                   , pretty               >= 1.1.3.1                   , process+                  , typed-process                   , rest-rewrite >= 0.3.0+                  , smtlib-backends >= 0.3+                  , smtlib-backends-process >= 0.3                   , stm                   , store                   , vector < 0.13@@ -156,6 +164,11 @@   ghc-options:     -fwrite-ide-info     -hiedir=.hie+  if flag(link-z3-as-a-library)+    build-depends: smtlib-backends-z3 >= 0.3+    hs-source-dirs: src-cond/with-z3+  else+    hs-source-dirs: src-cond/without-z3    if flag(devel)     ghc-options: -Werror@@ -193,9 +206,10 @@                   , mtl           >= 2.2.2                   , optparse-applicative                   , process+                  , typed-process                   , stm           >= 2.4                   , tagged-                  , tasty         >= 0.10+                  , tasty         >= 0.10 && < 1.5                   , tasty-ant-xml                   , tasty-hunit   >= 0.9                   , tasty-rerun   >= 1.1.12

@@ -0,0 +1,12 @@+module Language.Fixpoint.Conditional.Z3 where++import qualified SMTLIB.Backends+import qualified SMTLIB.Backends.Z3 as Z3++makeZ3 :: IO (SMTLIB.Backends.Backend, IO ())+makeZ3 = do+    handle <- Z3.new Z3.defaultConfig+    return (Z3.toBackend handle, Z3.close handle)++builtWithZ3AsALibrary :: Bool+builtWithZ3AsALibrary = True

@@ -0,0 +1,7 @@+module Language.Fixpoint.Conditional.Z3 where++makeZ3 :: IO a+makeZ3 = error "liquid-fixpoint: Not built with the Z3 backend. Please, enable the cabal flag link-z3-as-a-library."++builtWithZ3AsALibrary :: Bool+builtWithZ3AsALibrary = False

@@ -5,6 +5,7 @@     hornFInfo   ) where +import           Control.Monad (forM) import qualified Data.HashMap.Strict            as M import qualified Data.List                      as L import qualified Data.Tuple                     as Tuple@@ -14,7 +15,7 @@ import qualified Language.Fixpoint.Types        as F import qualified Language.Fixpoint.Types.Config as F import qualified Language.Fixpoint.Horn.Types   as H-import Data.Maybe (fromMaybe)+import qualified Data.Maybe                     as Mb  hornFInfo :: F.Config -> H.Query a -> F.FInfo a hornFInfo cfg q = mempty@@ -22,7 +23,7 @@   , F.bs        = be2   , F.ebinds    = ebs   , F.ws        = kvEnvWfCs kve-  , F.quals     = H.qQuals q+  , F.quals     = H.qQuals q ++ scrapeCstr (F.scrape cfg) hCst   , F.gLits     = F.fromMapSEnv $ H.qCon q   , F.dLits     = F.fromMapSEnv $ H.qDis q   , F.ae        = axEnv cfg q cs@@ -34,6 +35,7 @@     (be2, ebs, cs) = hornSubCs be1 kve hCst     hCst           = H.qCstr q + axEnv :: F.Config -> H.Query a -> M.HashMap F.SubcId b -> F.AxiomEnv axEnv cfg q cs = mempty   { F.aenvEqs    = H.qEqns q@@ -89,7 +91,7 @@ myMkSubC :: F.IBindEnv -> Maybe F.SortedReft -> F.SortedReft -> Maybe Integer -> F.Tag -> a -> F.SubC a myMkSubC be lhsMb rhs x y z = F.mkSubC be lhs rhs x y z   where-    lhs = fromMaybe def lhsMb+    lhs = Mb.fromMaybe def lhsMb     def = F.trueSortedReft (F.sr_sort rhs)  bindSortedReft :: KVEnv a -> H.Bind a -> F.SortedReft@@ -102,10 +104,6 @@                  Just (F.RR ss (F.Reft (vv, _))) -> (ss, vv)                  Nothing                       -> (F.intSort, F.dummySymbol) --- dummyBind :: a -> Bind a--- dummyBind = Bind F.dummySymbol F.intSort (PAnd [])-- predExpr :: KVEnv a -> H.Pred -> F.Expr predExpr kve        = go   where@@ -166,3 +164,95 @@  hvarPrefix :: F.Symbol hvarPrefix = F.symbol "nnf_arg"++-------------------------------------------------------------------------------+-- | Automatically scrape qualifiers from all predicates in a constraint+-------------------------------------------------------------------------------++scrapeCstr :: F.Scrape -> H.Cstr a -> [F.Qualifier]+scrapeCstr F.No _    = []+scrapeCstr m    cstr = Misc.sortNub $ go emptyBindEnv cstr+  where+    go senv (H.Head p _) = scrapePred senv p+    go senv (H.CAnd cs)  = concatMap (go senv) cs+    go senv (H.All b c)  = scrapeBind m senv' b <> go senv' c where senv' = insertBindEnv b senv+    go senv (H.Any b c)  = scrapeBind m senv' b <> go senv' c where senv' = insertBindEnv b senv++scrapeBind :: F.Scrape -> BindEnv -> H.Bind a -> [F.Qualifier]+scrapeBind F.Both senv b = scrapePred senv (H.bPred b)+scrapeBind _      _    _ = []++scrapePred :: BindEnv -> H.Pred -> [F.Qualifier]+scrapePred _    (H.Var _ _) = []+scrapePred senv (H.PAnd ps) = concatMap (scrapePred senv) ps+scrapePred senv (H.Reft e)  = concatMap (mkQual senv) (F.concConjuncts e)++-- NOTE: Constraints.mkQual will do extra stuff like generalizing the sorts...+mkQual :: BindEnv -> F.Expr -> [ F.Qualifier ]+mkQual env e = case qualParams env e of+  Nothing  -> []+  Just xts -> [ mkScrapeQual xts' e | xts' <- shiftCycle xts ]++mkScrapeQual :: [(F.Symbol, F.Sort)] -> F.Expr -> F.Qualifier+mkScrapeQual xts e = F.mkQual (F.symbol "AUTO") qParams (F.subst su e) (F.dummyPos "")+  where+    qParams = [ F.QP {F.qpSym = y, F.qpPat = F.PatNone, F.qpSort = t} | (_, y, t) <- xyts ]+    xyts    = zipWith (\i (x, t) -> (x, F.bindSymbol i, t)) [0..] xts+    su      = F.mkSubst [ (x, F.expr y) | (x, y, _) <- xyts ]+++shiftCycle :: [(F.Symbol, F.Sort)] -> [[(F.Symbol, F.Sort)]]+shiftCycle xts+  | n <= maxQualifierParams = recycle n xts+  | otherwise              = []+  where+    n                      = length xts++recycle :: Int -> [a] -> [[a]]+recycle 0 _      = []+recycle _ []     = []+recycle k (x:xs) = (x:xs) : recycle (k-1) (xs ++ [x])++maxQualifierParams :: Int+maxQualifierParams = 3++{-+  1. Normalize the names+  2. Permute the args?+ -}++qualParams :: BindEnv -> F.Expr -> Maybe [(F.Symbol, F.Sort)]+qualParams env e = do+    let xs = Misc.nubOrd (F.syms e)+    ixts <- forM xs $ \x -> do+              (t, i) <- lookupBindEnv x env+              return (i, x, t)+    return [ (x, t) | (_, x, t) <- reverse . L.sort $ ixts ]++    -- ixts = [ (i, x, t) | x <- xs, (i, t) <- lookupBindEnv x env ]++-------------------------------------------------------------------------------++-- | `BindEnv` maps each symbol to (sort, depth) pair, where shorter depths+--    means bound "earlier" i.e. in (forall (x1:...) (forall (x2:...) ...)+--    the depth of x1 is less than the depth of x2.+--    We use the heuristic that the symbol with the "largest" depth is the+--    "value-variable" in the qualifier.++data BindEnv = BindEnv+  { bSize  :: !Int+  , bBinds :: M.HashMap F.Symbol (F.Sort, Int)+  }++emptyBindEnv :: BindEnv+emptyBindEnv = BindEnv { bSize = 0, bBinds = mempty }++insertBindEnv :: H.Bind a -> BindEnv -> BindEnv+insertBindEnv b senv = BindEnv { bSize = n + 1, bBinds = M.insert x (t, n) (bBinds senv) }+  where+    n = bSize senv+    x = H.bSym b+    t = H.bSort b++lookupBindEnv :: F.Symbol -> BindEnv -> Maybe (F.Sort, Int)+lookupBindEnv x env = M.lookup x (bBinds env)

@@ -50,6 +50,7 @@   | HMat  F.Rewrite   | HDat !F.DataDecl   | HOpt !String+  | HNum ()   deriving (Functor)  hThingP :: Parser (HThing H.Tag)@@ -64,6 +65,12 @@         <|> HDef  <$> (reserved "define"     *> defineP)         <|> HMat  <$> (reserved "match"      *> matchP)         <|> HDat  <$> (reserved "data"       *> dataDeclP)+        <|> HNum  <$> (reserved "numeric"    *> numericDeclP)++numericDeclP :: Parser ()+numericDeclP = do+  sym <- locUpperIdP+  addNumTyCon (F.val sym)  ------------------------------------------------------------------------------- hCstrP :: Parser (H.Cstr H.Tag)

@@ -128,7 +128,7 @@                    (_,so):xts -> F.mkQ "Auto" ((v, so) : xts) p junk                    _          -> F.panic "impossible"   where-    xs         = L.delete v $ Misc.hashNub (F.syms p)+    xs         = L.delete v $ Misc.setNub (F.syms p)     junk       = F.dummyPos "mkQual"  envSort :: F.SEnv F.Sort -> F.Symbol -> (F.Symbol, F.Sort)

@@ -19,6 +19,8 @@ import qualified Data.HashMap.Strict              as M import qualified Data.List                        as L import qualified Data.HashSet                     as S+import qualified Data.Map                         as Map+import qualified Data.Set                         as Set import           Data.Tuple                       (swap) import           Data.Maybe import           Data.Array                       hiding (indices)@@ -205,8 +207,8 @@ allMap :: (Eq k, Hashable k) => (v -> Bool) -> M.HashMap k v -> Bool allMap p = L.foldl' (\a v -> a && p v) True -hashNub :: (Eq k, Hashable k) => [k] -> [k]-hashNub = M.keys . M.fromList . fmap (, ())+setNub :: Ord k => [k] -> [k]+setNub = Set.toList . Set.fromList  sortNub :: (Ord a) => [a] -> [a] sortNub = nubOrd . L.sort@@ -220,8 +222,8 @@   | otherwise = x : nubOrd t nubOrd xs     = xs -hashNubWith :: (Eq b, Hashable b) => (a -> b) -> [a] -> [a]-hashNubWith f xs = M.elems $ M.fromList [ (f x, x) | x <- xs ]+hashNubWith :: Ord b => (a -> b) -> [a] -> [a]+hashNubWith f xs = Map.elems $ Map.fromList [ (f x, x) | x <- xs ]  mFromList :: (Eq k, Hashable k) => [(k, v)] -> M.HashMap k v mFromList = M.fromList

@@ -52,7 +52,6 @@   , refP        -- (Sorted) Refinements   , refDefP     -- (Sorted) Refinements with default binder   , refBindP    -- (Sorted) Refinements with configurable sub-parsers-  , bvSortP     -- Bit-Vector Sort   , defineP     -- function definition equations (PLE)   , matchP      -- measure definition equations (PLE) @@ -94,7 +93,7 @@   , initPState, PState (..)    , LayoutStack(..)-  , Fixity(..), Assoc(..), addOperatorP+  , Fixity(..), Assoc(..), addOperatorP, addNumTyCon    -- * For testing   , expr0P@@ -120,7 +119,6 @@ import           GHC.Generics                (Generic)  import qualified Data.Char                   as Char-import           Language.Fixpoint.Smt.Bitvector import           Language.Fixpoint.Types.Errors import qualified Language.Fixpoint.Misc      as Misc import           Language.Fixpoint.Smt.Types@@ -207,6 +205,7 @@                      , singList    :: Maybe (Expr -> Expr)                      , supply      :: !Integer                      , layoutStack :: LayoutStack+                     , numTyCons   :: !(S.HashSet Symbol)                      }  -- | The layout stack tracks columns at which layout blocks@@ -855,6 +854,10 @@                     , fixityOps   = op:fixityOps s                     } +-- | Add a new numeric FTyCon (symbol) to the parsing state.+addNumTyCon :: Symbol -> Parser ()+addNumTyCon tc = modify $ \s -> s{ numTyCons = S.insert tc (numTyCons s) }+ -- | Parses any of the known infix operators. infixSymbolP :: Parser Symbol infixSymbolP = do@@ -1000,7 +1003,6 @@    =  parens sortP -- parenthesised sort, starts with "("   <|> (reserved "func" >> funcSortP) -- function sort, starts with "func"   <|> (fAppTC listFTyCon . pure <$> brackets sortP)-  -- <|> bvSortP -- Andres: this looks unreachable, as it starts with "("   <|> (fAppTC <$> fTyConP <*> appArgsP)   <|> (fApp   <$> tvarP   <*> appArgsP) @@ -1020,15 +1022,12 @@   <|> (reserved "bool"    >> return boolFTyCon)   <|> (reserved "num"     >> return numFTyCon)   <|> (reserved "Str"     >> return strFTyCon)-  <|> (symbolFTycon      <$> locUpperIdP)+  <|> (mkFTycon          =<<  locUpperIdP) --- | Bit-Vector Sort-bvSortP :: Parser Sort-bvSortP = mkSort <$> (bvSizeP "Size32" S32 <|> bvSizeP "Size64" S64)-  where-    bvSizeP ss s = do-      parens (reserved "BitVec" >> reserved ss)-      return s+mkFTycon :: LocSymbol -> Parser FTycon+mkFTycon locSym = do+  nums  <- gets numTyCons+  return (symbolNumInfoFTyCon locSym (val locSym `S.member` nums) False)   --------------------------------------------------------------------------------@@ -1101,8 +1100,14 @@            , [InfixR (reservedOp "=>"   >> return PImp)]            , [InfixR (reservedOp "==>"  >> return PImp)]            , [InfixR (reservedOp "="    >> return PIff)]-           , [InfixR (reservedOp "<=>"  >> return PIff)]]+           , [InfixR (reservedOp "<=>"  >> return PIff)]+           , [InfixR (reservedOp "!="   >> return pNotIff)]+           , [InfixR (reservedOp "/="   >> return pNotIff)]+           ] +pNotIff :: Expr -> Expr -> Expr+pNotIff x y = PNot (PIff x y)+ -- | Parses a relation predicate. -- -- Binary relations connect expressions and predicates.@@ -1453,6 +1458,7 @@                            , fixityOps   = []                            , supply      = 0                            , layoutStack = Empty+                           , numTyCons   = S.empty                            }  -- | Entry point for parsing, for testing.

@@ -1,70 +0,0 @@-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE DeriveGeneric      #-}--module Language.Fixpoint.Smt.Bitvector-       ( -- * Constructor-         Bv (..)--         -- * Sizes-       , BvSize (..)--         -- * Operators-       , BvOp (..)--         -- * BitVector Sort Constructor-       , mkSort--         -- * BitVector Expression Constructor-       , eOp--         -- * BitVector Type Constructor-       , bvTyCon--       ) where--import           Data.Generics           (Data)-import qualified Data.Text               as T-import           Data.Typeable           (Typeable)-import           GHC.Generics            (Generic)-import           Language.Fixpoint.Types.Names-import           Language.Fixpoint.Types-import           Data.List (foldl')--data Bv     = Bv !BvSize !String--data BvSize = S32   | S64-              deriving (Eq, Ord, Show, Data, Typeable, Generic)--data BvOp   = BvAnd | BvOr-              deriving (Eq, Ord, Show, Data, Typeable, Generic)---- | Construct the bitvector `Sort` from its `BvSize`-mkSort :: BvSize -> Sort-mkSort s = fApp (fTyconSort bvTyCon) [ fTyconSort (sizeTyCon s) ]--bvTyCon :: FTycon-bvTyCon = symbolFTycon $ dummyLoc bitVecName--sizeTyCon    :: BvSize -> FTycon-sizeTyCon    = symbolFTycon . dummyLoc . sizeName--sizeName :: BvSize -> Symbol-sizeName S32 = size32Name-sizeName S64 = size64Name---- | Construct an `Expr` using a raw string, e.g. (Bv S32 "#x02000000")-instance Expression Bv where-  expr (Bv sz v) = ECon $ L (T.pack v) (mkSort sz)---- | Apply some bitvector operator to a list of arguments-eOp :: BvOp -> [Expr] -> Expr-eOp b es = foldl' EApp (EVar $ opName b) es--opName :: BvOp -> Symbol-opName BvAnd = bvAndName-opName BvOr  = bvOrName----- sizeSort     = (`FApp` [fObj $ dummyLoc $ symbol "obj"]) . sizeTC--- s32TyCon     = symbolFTycon $ dummyLoc size32Name--- s64TyCon     = symbolFTycon $ dummyLoc size64Name

@@ -1,4 +1,3 @@-{-# LANGUAGE CPP                       #-} {-# LANGUAGE BangPatterns              #-} {-# LANGUAGE FlexibleInstances         #-} {-# LANGUAGE NoMonomorphismRestriction #-}@@ -7,6 +6,7 @@ {-# LANGUAGE UndecidableInstances      #-} {-# LANGUAGE ScopedTypeVariables       #-} {-# LANGUAGE PatternGuards             #-}+{-# LANGUAGE DoAndIfThenElse           #-}  {-# OPTIONS_GHC -Wno-name-shadowing #-} @@ -18,23 +18,6 @@ --   http://www.smt-lib.org/ --   http://www.grammatech.com/resource/smt/SMTLIBTutorial.pdf --- Note [Async SMT API]------ The SMT solver is started in a separate process and liquid-fixpoint--- communicates with it via pipes. This mechanism introduces some latency--- since the queries need to reach the buffers in a separate process and--- the OS has to switch contexts.------ A remedy we currently try for this is to send multiple queries--- together without waiting for the reply to each one, i.e. asynchronously.--- We then collect the multiple answers after sending all of the queries.------ The functions named @smt*Async@ implement this scheme.------ An asynchronous thread is used to write the queries to prevent the--- caller from blocking on IO, should the write buffer be full or should--- an 'hFlush' call be necessary.- module Language.Fixpoint.Smt.Interface (      -- * Commands@@ -55,7 +38,6 @@      -- * Execute Queries     , command-    , smtExit     , smtSetMbqi      -- * Query API@@ -70,12 +52,6 @@     , smtBracket, smtBracketAt     , smtDistinct     , smtPush, smtPop-    , smtAssertAsync-    , smtCheckUnsatAsync-    , readCheckUnsat-    , smtBracketAsyncAt-    , smtPushAsync-    , smtPopAsync      -- * Check Validity     , checkValid@@ -85,9 +61,6 @@      ) where -import           Control.Concurrent.Async (async, cancel)-import           Control.Concurrent.STM-  (TVar, atomically, modifyTVar, newTVarIO, readTVar, retry, writeTVar) import           Language.Fixpoint.Types.Config ( SMTSolver (..)                                                 , Config                                                 , solver@@ -105,20 +78,22 @@ import           Control.Applicative      ((<|>)) import           Control.Monad import           Control.Exception+import           Data.ByteString.Builder (Builder)+import qualified Data.ByteString.Builder as BS+import qualified Data.ByteString.Lazy as LBS+import qualified Data.ByteString.Lazy.Char8 as Char8 import           Data.Char import qualified Data.HashMap.Strict      as M import           Data.Maybe              (fromMaybe) import qualified Data.Text                as T+import qualified Data.Text.Encoding       as TE+import qualified Data.Text.IO -- import           Data.Text.Format-import qualified Data.Text.IO             as TIO-import qualified Data.Text.Lazy           as LT import qualified Data.Text.Lazy.IO        as LTIO import           System.Directory import           System.Console.CmdArgs.Verbosity-import           System.Exit              hiding (die) import           System.FilePath import           System.IO-import           System.Process import qualified Data.Attoparsec.Text     as A -- import qualified Data.HashMap.Strict      as M import           Data.Attoparsec.Internal.Types (Parser)@@ -127,6 +102,10 @@ import           Language.Fixpoint.Utils.Builder as Builder -- import qualified Language.Fixpoint.Types as F -- import           Language.Fixpoint.Types.PrettyPrint (tracepp)+import qualified SMTLIB.Backends+import qualified SMTLIB.Backends.Process as Process+import qualified Language.Fixpoint.Conditional.Z3 as Conditional.Z3+import Control.Concurrent.Async (async)  {- runFile f@@ -183,36 +162,37 @@ {-# SCC command #-} command              :: Context -> Command -> IO Response ---------------------------------------------------------------------------------command me !cmd       = say >> hear cmd+command Ctx {..} !cmd       = do+  -- whenLoud $ do LTIO.appendFile debugFile (s <> "\n")+  --               LTIO.putStrLn ("CMD-RAW:" <> s <> ":CMD-RAW:DONE")+  forM_ ctxLog $ \h -> do+    BS.hPutBuilder h cmdBS+    LBS.hPutStr h "\n"+  case cmd of+    CheckSat   -> commandRaw+    GetValue _ -> commandRaw+    _          -> SMTLIB.Backends.command_ ctxSolver cmdBS >> return Ok   where-    env               = ctxSymEnv me-    say               = smtWrite me ({-# SCC "Command-runSmt2" #-} Builder.toLazyText (runSmt2 env cmd))-    hear CheckSat     = smtRead me-    hear (GetValue _) = smtRead me-    hear _            = return Ok--smtExit :: Context -> IO ()-smtExit me = asyncCommand me Exit+    commandRaw      = do+      resp <- SMTLIB.Backends.command ctxSolver cmdBS+      let respTxt =+            TE.decodeUtf8With (const $ const $ Just ' ') $+            LBS.toStrict resp+      parse respTxt+    cmdBS = {-# SCC "Command-runSmt2" #-} runSmt2 ctxSymEnv cmd+    parse resp      = do+      case A.parseOnly responseP resp of+        Left e  -> Misc.errorstar $ "SMTREAD:" ++ e+        Right r -> do+          let textResponse = "; SMT Says: " <> T.pack (show r)+          forM_ ctxLog $ \h ->+            Data.Text.IO.hPutStrLn h textResponse+          when ctxVerbose $+            Data.Text.IO.putStrLn textResponse+          return r  smtSetMbqi :: Context -> IO ()-smtSetMbqi me = asyncCommand me SetMbqi--smtWrite :: Context -> Raw -> IO ()-smtWrite me !s = smtWriteRaw me s--smtRead :: Context -> IO Response-smtRead me = {- SCC "smtRead" -} do-  when (ctxVerbose me) $ LTIO.putStrLn "SMT READ"-  ln  <- smtReadRaw me-  res <- A.parseWith (smtReadRaw me) responseP ln-  case A.eitherResult res of-    Left e  -> Misc.errorstar $ "SMTREAD:" ++ e-    Right r -> do-      maybe (return ()) (\h -> LTIO.hPutStrLn h $ blt ("; SMT Says: " <> bShow r)) (ctxLog me)-      when (ctxVerbose me) $ LTIO.putStrLn $ blt ("SMT Says: " <> bShow r)-      return r--+smtSetMbqi me = interact' me SetMbqi  type SmtParser a = Parser T.Text a @@ -254,42 +234,21 @@   = do v <- A.char '(' *> A.takeWhile1 (/=')') <* A.char ')'        return $ "(" <> v <> ")" --- | Writes a line of input for the SMT solver and to the log if there is one.-smtWriteRaw :: Context -> Raw -> IO ()-smtWriteRaw me !s = {- SCC "smtWriteRaw" -} do-  -- whenLoud $ do LTIO.appendFile debugFile (s <> "\n")-  --               LTIO.putStrLn ("CMD-RAW:" <> s <> ":CMD-RAW:DONE")-  hPutStrLnNow (ctxIn me) s-  maybe (return ()) (`LTIO.hPutStrLn` s) (ctxLog me)---- | Reads a line of output from the SMT solver.-smtReadRaw :: Context -> IO T.Text-smtReadRaw me = do-  eof <- hIsEOF (ctxOut me)-  if eof then Misc.errorstar "SMT returned End of File" else-    TIO.hGetLine (ctxOut me)-{-# SCC smtReadRaw  #-}--hPutStrLnNow :: Handle -> LT.Text -> IO ()-hPutStrLnNow h !s = LTIO.hPutStrLn h s >> hFlush h-{-# SCC hPutStrLnNow #-}- -------------------------------------------------------------------------- -- | SMT Context --------------------------------------------------------- --------------------------------------------------------------------------  ---------------------------------------------------------------------------makeContext   :: Config -> FilePath -> IO Context+makeContext :: Config -> FilePath -> IO Context -------------------------------------------------------------------------- makeContext cfg f-  = do me   <- makeProcess cfg-       pre  <- smtPreamble cfg (solver cfg) me-       createDirectoryIfMissing True $ takeDirectory smtFile+  = do createDirectoryIfMissing True $ takeDirectory smtFile        hLog <- openFile smtFile WriteMode-       hSetBuffering hLog $ BlockBuffering $ Just $ 1024*1024*64-       let me' = me { ctxLog = Just hLog }-       mapM_ (smtWrite me') pre-       return me'+       hSetBuffering hLog $ BlockBuffering $ Just $ 1024 * 1024 * 64+       me   <- makeContext' cfg $ Just hLog+       pre  <- smtPreamble cfg (solver cfg) me+       mapM_ (SMTLIB.Backends.command_ (ctxSolver me)) pre+       return me     where        smtFile = extFileName Smt2 f @@ -303,75 +262,82 @@  makeContextNoLog :: Config -> IO Context makeContextNoLog cfg-  = do me  <- makeProcess cfg+  = do me  <- makeContext' cfg Nothing        pre <- smtPreamble cfg (solver cfg) me-       mapM_ (smtWrite me) pre+       mapM_ (SMTLIB.Backends.command_ (ctxSolver me)) pre        return me -makeProcess :: Config -> IO Context-makeProcess cfg-  = do (hIn, hOut, _ ,pid) <- runInteractiveCommand $ smtCmd (solver cfg)+makeProcess+  :: Maybe Handle+  -> Process.Config+  -> IO (SMTLIB.Backends.Backend, IO ())+makeProcess ctxLog cfg+  = do handle@Process.Handle {hMaybeErr = Just hErr, ..} <- Process.new cfg+       case ctxLog of+         Nothing -> return ()+         Just hLog -> void $ async $ forever+           (do err <- LTIO.hGetLine hErr+               LTIO.hPutStrLn hLog $ "OOPS, SMT solver error:" <> err+           ) `catch` \ SomeException {} -> return ()+       let backend = Process.toBackend handle+       hSetBuffering hOut $ BlockBuffering $ Just $ 1024 * 1024 * 64+       hSetBuffering hIn $ BlockBuffering $ Just $ 1024 * 1024 * 64+       return (backend, Process.close handle)++makeContext' :: Config -> Maybe Handle -> IO Context+makeContext' cfg ctxLog+  = do (backend, closeIO) <- case solver cfg of+         Z3      ->+           {- "z3 -smt2 -in"                   -}+           {- "z3 -smtc SOFT_TIMEOUT=1000 -in" -}+           {- "z3 -smtc -in MBQI=false"        -}+           makeProcess ctxLog $ Process.defaultConfig+                             { Process.exe = "z3"+                             , Process.args = ["-smt2", "-in"] }+         Z3mem   -> Conditional.Z3.makeZ3+         Mathsat -> makeProcess ctxLog $ Process.defaultConfig+                             { Process.exe = "mathsat"+                             , Process.args = ["-input=smt2"] }+         Cvc4    -> makeProcess ctxLog $+                      Process.defaultConfig+                             { Process.exe = "cvc4"+                             , Process.args = ["--incremental", "-L", "smtlib2"] }+       solver <- SMTLIB.Backends.initSolver SMTLIB.Backends.Queuing backend        loud <- isLoud-       hSetBuffering hOut $ BlockBuffering $ Just $ 1024*1024*64-       hSetBuffering hIn $ BlockBuffering $ Just $ 1024*1024*64-       -- See Note [Async SMT API]-       queueTVar <- newTVarIO mempty-       writerAsync <- async $ forever $ do-         t <- atomically $ do-           builder <- readTVar queueTVar-           let t = Builder.toLazyText builder-           when (LT.null t) retry-           writeTVar queueTVar mempty-           return t-         LTIO.hPutStr hIn t-         hFlush hIn-       return Ctx { ctxPid     = pid-                  , ctxIn      = hIn-                  , ctxOut     = hOut-                  , ctxLog     = Nothing+       return Ctx { ctxSolver  = solver+                  , ctxClose   = closeIO+                  , ctxLog     = ctxLog                   , ctxVerbose = loud                   , ctxSymEnv  = mempty-                  , ctxAsync   = writerAsync-                  , ctxTVar    = queueTVar                   } --- | Close file handles and wait for the solver process to terminate.-cleanupContext :: Context -> IO ExitCode-cleanupContext Ctx{..} = do-  cancel ctxAsync-  hCloseMe "ctxIn" ctxIn-  hCloseMe "ctxOut"  ctxOut+-- | Close file handles and release the solver backend's resources.+cleanupContext :: Context -> IO ()+cleanupContext Ctx {..} = do   maybe (return ()) (hCloseMe "ctxLog") ctxLog-  waitForProcess ctxPid+  ctxClose  hCloseMe :: String -> Handle -> IO () hCloseMe msg h = hClose h `catch` (\(exn :: IOException) -> putStrLn $ "OOPS, hClose breaks: " ++ msg ++ show exn) -{- "z3 -smt2 -in"                   -}-{- "z3 -smtc SOFT_TIMEOUT=1000 -in" -}-{- "z3 -smtc -in MBQI=false"        -}--smtCmd         :: SMTSolver -> String --  T.Text-smtCmd Z3      = "z3 -smt2 -in"-smtCmd Mathsat = "mathsat -input=smt2"-smtCmd Cvc4    = "cvc4 --incremental -L smtlib2"--smtPreamble :: Config -> SMTSolver -> Context -> IO [LT.Text]-smtPreamble cfg Z3 me-  = do v <- getZ3Version me-       checkValidStringFlag Z3 v cfg-       return $ z3_options ++ makeMbqi cfg ++ makeTimeout cfg ++ Thy.preamble cfg Z3-smtPreamble cfg s _-  = checkValidStringFlag s [] cfg >> return (Thy.preamble cfg s)+smtPreamble :: Config -> SMTSolver -> Context -> IO [Builder]+smtPreamble cfg s me+  | s == Z3 || s == Z3mem+    = do v <- getZ3Version me+         checkValidStringFlag Z3 v cfg+         return $ z3_options ++ makeMbqi cfg ++ makeTimeout cfg ++ Thy.preamble cfg Z3+  | otherwise+    = checkValidStringFlag s [] cfg >> return (Thy.preamble cfg s)  getZ3Version :: Context -> IO [Int] getZ3Version me-  = do smtWrite me "(get-info :version)"-       -- resp is like (:version "4.8.15")-       resp <- smtReadRaw me-       case T.splitOn "\"" resp of-         _:vText:_ -> do-           let parsedComponents = [ reads (T.unpack cText) | cText <- T.splitOn "." vText ]+  = do -- resp is like (:version "4.8.15")+       resp <- SMTLIB.Backends.command (ctxSolver me) "(get-info :version)"+       case Char8.split '"' resp of+         _:rText:_ -> do+           -- strip off potential " - build hashcode ..." suffix+           let vText = Char8.takeWhile (not . isSpace) rText+           let parsedComponents = [ reads (Char8.unpack cText) | cText <- Char8.split '.' vText ]            sequence              [ case pComponent of                  [(c, "")] -> return c@@ -419,7 +385,7 @@ deconSort :: Sort -> ([Sort], Sort) deconSort t = case functionSort t of                 Just (_, ins, out) -> (ins, out)-                Nothing            -> ([] , t  )+                Nothing            -> ([], t)  -- hack now this is used only for checking gradual condition. smtCheckSat :: Context -> Expr -> IO Bool@@ -443,48 +409,7 @@           e  -------------------------------------------------------------------- Async calls to the smt------ See Note [Async SMT API]------------------------------------------------------------------ -asyncCommand :: Context -> Command -> IO ()-asyncCommand me cmd = do-  let env = ctxSymEnv me-      cmdText = {-# SCC "asyncCommand-runSmt2" #-} Builder.toLazyText $ runSmt2 env cmd-  asyncPutStrLn (ctxTVar me) cmdText-  maybe (return ()) (`LTIO.hPutStrLn` cmdText) (ctxLog me)-  where-    asyncPutStrLn :: TVar Builder.Builder -> LT.Text -> IO ()-    asyncPutStrLn tv t = atomically $-      modifyTVar tv (`mappend` (Builder.fromLazyText t `mappend` Builder.fromString "\n"))--smtAssertAsync :: Context -> Expr -> IO ()-smtAssertAsync me p  = asyncCommand me $ Assert Nothing p--smtCheckUnsatAsync :: Context -> IO ()-smtCheckUnsatAsync me = asyncCommand me CheckSat--smtBracketAsyncAt :: SrcSpan -> Context -> String -> IO a -> IO a-smtBracketAsyncAt sp x y z = smtBracketAsync x y z `catch` dieAt sp--smtBracketAsync :: Context -> String -> IO a -> IO a-smtBracketAsync me _msg a   = do-  smtPushAsync me-  r <- a-  smtPopAsync me-  return r--smtPushAsync, smtPopAsync   :: Context -> IO ()-smtPushAsync me = asyncCommand me Push-smtPopAsync me = asyncCommand me Pop---------------------------------------------------------------------{-# SCC readCheckUnsat #-}-readCheckUnsat :: Context -> IO Bool-readCheckUnsat me = respSat <$> smtRead me- smtAssertAxiom :: Context -> Triggered Expr -> IO () smtAssertAxiom me p  = interact' me (AssertAx p) @@ -514,18 +439,18 @@ interact' me cmd  = void $ command me cmd  -makeTimeout :: Config -> [LT.Text]+makeTimeout :: Config -> [Builder] makeTimeout cfg-  | Just i <- smtTimeout cfg = [ LT.pack ("\n(set-option :timeout " ++ show i ++ ")\n")]+  | Just i <- smtTimeout cfg = [ "\n(set-option :timeout " <> fromString (show i) <> ")\n"]   | otherwise                = [""]  -makeMbqi :: Config -> [LT.Text]+makeMbqi :: Config -> [Builder] makeMbqi cfg   | gradual cfg = [""]   | otherwise   = ["\n(set-option :smt.mbqi false)"] -z3_options :: [LT.Text]+z3_options :: [Builder] z3_options   = [ "(set-option :auto-config false)"     , "(set-option :model true)" ]

@@ -15,6 +15,7 @@  module Language.Fixpoint.Smt.Serialize (smt2SortMono) where +import           Data.ByteString.Builder (Builder) import           Language.Fixpoint.SortCheck import           Language.Fixpoint.Types import qualified Language.Fixpoint.Types.Visitor as Vis@@ -30,44 +31,44 @@   smt2 env c@(sym, t) = -- build "({} {})" (smt2 env sym, smt2SortMono c env t)                         parenSeqs [smt2 env sym, smt2SortMono c env t] -smt2SortMono, smt2SortPoly :: (PPrint a) => a -> SymEnv -> Sort -> Builder.Builder+smt2SortMono, smt2SortPoly :: (PPrint a) => a -> SymEnv -> Sort -> Builder smt2SortMono = smt2Sort False smt2SortPoly = smt2Sort True -smt2Sort :: (PPrint a) => Bool -> a -> SymEnv -> Sort -> Builder.Builder+smt2Sort :: (PPrint a) => Bool -> a -> SymEnv -> Sort -> Builder smt2Sort poly _ env t = smt2 env (Thy.sortSmtSort poly (seData env) t) -smt2data :: SymEnv -> [DataDecl] -> Builder.Builder+smt2data :: SymEnv -> [DataDecl] -> Builder smt2data env = smt2data' env . map padDataDecl -smt2data' :: SymEnv -> [DataDecl] -> Builder.Builder+smt2data' :: SymEnv -> [DataDecl] -> Builder smt2data' env ds = seqs [ parens $ smt2many (smt2dataname env <$> ds)                          , parens $ smt2many (smt2datactors env <$> ds)                          ]  -smt2dataname :: SymEnv -> DataDecl -> Builder.Builder+smt2dataname :: SymEnv -> DataDecl -> Builder smt2dataname env (DDecl tc as _) = parenSeqs [name, n]   where     name  = smt2 env (symbol tc)     n     = smt2 env as  -smt2datactors :: SymEnv -> DataDecl -> Builder.Builder+smt2datactors :: SymEnv -> DataDecl -> Builder smt2datactors env (DDecl _ as cs) = parenSeqs ["par", parens tvars, parens ds]   where     tvars        = smt2many (smt2TV <$> [0..(as-1)])     smt2TV       = smt2 env . SVar     ds           = smt2many (smt2ctor env as <$> cs) -smt2ctor :: SymEnv -> Int -> DataCtor -> Builder.Builder+smt2ctor :: SymEnv -> Int -> DataCtor -> Builder smt2ctor env _  (DCtor c [])  = smt2 env c smt2ctor env as (DCtor c fs)  = parenSeqs [smt2 env c, fields]    where     fields                 = smt2many (smt2field env as <$> fs) -smt2field :: SymEnv -> Int -> DataField -> Builder.Builder+smt2field :: SymEnv -> Int -> DataField -> Builder smt2field env as d@(DField x t) = parenSeqs [smt2 env x, smt2SortPoly d env $ mkPoly as t]  -- | SMTLIB/Z3 don't like "unused" type variables; they get pruned away and@@ -112,7 +113,7 @@ instance SMTLIB2 Constant where   smt2 _ (I n)   = bShow n   smt2 _ (R d)   = bFloat d-  smt2 _ (L t _) = lbb t+  smt2 _ (L t _) = fromText t  instance SMTLIB2 Bop where   smt2 _ Plus   = "+"@@ -165,24 +166,24 @@ -- | smt2Cast uses the 'as x T' pattern needed for polymorphic ADT constructors --   like Nil, see `tests/pos/adt_list_1.fq` -smt2Cast :: SymEnv -> Expr -> Sort -> Builder.Builder+smt2Cast :: SymEnv -> Expr -> Sort -> Builder smt2Cast env (EVar x) t = smt2Var env x t smt2Cast env e        _ = smt2    env e -smt2Var :: SymEnv -> Symbol -> Sort -> Builder.Builder+smt2Var :: SymEnv -> Symbol -> Sort -> Builder smt2Var env x t   | isLamArgSymbol x            = smtLamArg env x t   | Just s <- symEnvSort x env   , isPolyInst s t              = smt2VarAs env x t   | otherwise                   = smt2 env x -smtLamArg :: SymEnv -> Symbol -> Sort -> Builder.Builder+smtLamArg :: SymEnv -> Symbol -> Sort -> Builder smtLamArg env x t = Builder.fromText $ symbolAtName x env () (FFunc t FInt) -smt2VarAs :: SymEnv -> Symbol -> Sort -> Builder.Builder+smt2VarAs :: SymEnv -> Symbol -> Sort -> Builder smt2VarAs env x t = parenSeqs ["as", smt2 env x, smt2SortMono x env t] -smt2Lam :: SymEnv -> (Symbol, Sort) -> Expr -> Builder.Builder+smt2Lam :: SymEnv -> (Symbol, Sort) -> Expr -> Builder smt2Lam env (x, xT) (ECst e eT) = parenSeqs [Builder.fromText lambda, x', smt2 env e]   where     x'                          = smtLamArg env x xT@@ -191,7 +192,7 @@ smt2Lam _ _ e   = panic ("smtlib2: Cannot serialize unsorted lambda: " ++ showpp e) -smt2App :: SymEnv -> Expr -> Builder.Builder+smt2App :: SymEnv -> Expr -> Builder smt2App env e@(EApp (EApp f e1) e2)   | Just t <- unApplyAt f   = parenSeqs [Builder.fromText (symbolAtName applyName env e t), smt2s env [e1, e2]]@@ -203,15 +204,13 @@   where     (f, es)   = splitEApp' e -smt2Coerc :: SymEnv -> Sort -> Sort -> Expr -> Builder.Builder+smt2Coerc :: SymEnv -> Sort -> Sort -> Expr -> Builder smt2Coerc env t1 t2 e-  | t1' == t2'  = smt2 env e+  | t1 == t2  = smt2 env e   | otherwise = parenSeqs [Builder.fromText coerceFn , smt2 env e]   where     coerceFn  = symbolAtName coerceName env (ECoerc t1 t2 e) t     t         = FFunc t1 t2-    t1'       = smt2SortMono e env t1-    t2'       = smt2SortMono e env t2  splitEApp' :: Expr -> (Expr, [Expr]) splitEApp'            = go []@@ -220,12 +219,12 @@   --   go acc (ECst e _) = go acc e     go acc e          = (e, acc) -mkRel :: SymEnv -> Brel -> Expr -> Expr -> Builder.Builder+mkRel :: SymEnv -> Brel -> Expr -> Expr -> Builder mkRel env Ne  e1 e2 = mkNe env e1 e2 mkRel env Une e1 e2 = mkNe env e1 e2 mkRel env r   e1 e2 = parenSeqs [smt2 env r, smt2 env e1, smt2 env e2] -mkNe :: SymEnv -> Expr -> Expr -> Builder.Builder+mkNe :: SymEnv -> Expr -> Expr -> Builder mkNe env e1 e2      = key "not" (parenSeqs ["=",  smt2 env e1, smt2 env e2])  instance SMTLIB2 Command where@@ -258,13 +257,13 @@   smt2 env (TR _ e)               = smt2 env e  {-# INLINE smtTr #-}-smtTr :: SymEnv -> Builder.Builder -> [(Symbol, Sort)] -> Expr -> Triggered Expr -> Builder.Builder+smtTr :: SymEnv -> Builder -> [(Symbol, Sort)] -> Expr -> Triggered Expr -> Builder smtTr env q bs p t = key q (parens (smt2s env bs) <+> key "!" (smt2 env p <+> ":pattern" <> parens (smt2s env (makeTriggers t))))  {-# INLINE smt2s #-}-smt2s    :: SMTLIB2 a => SymEnv -> [a] -> Builder.Builder+smt2s    :: SMTLIB2 a => SymEnv -> [a] -> Builder smt2s env as = smt2many (smt2 env <$> as)  {-# INLINE smt2many #-}-smt2many :: [Builder.Builder] -> Builder.Builder+smt2many :: [Builder] -> Builder smt2many = seqs

@@ -42,13 +42,13 @@      ) where  import           Prelude hiding (map)+import           Data.ByteString.Builder (Builder) import           Language.Fixpoint.Types.Sorts import           Language.Fixpoint.Types.Config import           Language.Fixpoint.Types import           Language.Fixpoint.Smt.Types -- import qualified Data.HashMap.Strict      as M import           Data.Maybe (catMaybes)-import qualified Data.Text.Lazy           as T -- import           Data.Text.Format import qualified Data.Text import           Data.String                 (IsString(..))@@ -92,7 +92,61 @@ mshift = "smt_map_shift" mToSet = "smt_map_to_set" +---- Size changes+bvConcatName, bvExtractName, bvRepeatName, bvZeroExtName, bvSignExtName :: Symbol+bvConcatName   = "concat"+bvExtractName  = "extract"+bvRepeatName   = "repeat"+bvZeroExtName  = "zero_extend"+bvSignExtName  = "sign_extend" +-- Unary Logic+bvNotName, bvNegName :: Symbol+bvNotName = "bvnot"+bvNegName = "bvneg"++-- Binary Logic+bvAndName, bvNandName, bvOrName, bvNorName, bvXorName, bvXnorName :: Symbol+bvAndName  = "bvand"+bvNandName = "bvnand"+bvOrName   = "bvor"+bvNorName  = "bvnor"+bvXorName  = "bvxor"+bvXnorName = "bvxnor"++-- Shifts+bvShlName, bvLShrName, bvAShrName, bvLRotName, bvRRotName :: Symbol+bvShlName  = "bvshl"+bvLShrName = "bvlshr"+bvAShrName = "bvashr"+bvLRotName = "rotate_left"+bvRRotName = "rotate_right"++-- Arithmetic+bvAddName, bvSubName, bvMulName, bvUDivName :: Symbol+bvURemName, bvSDivName, bvSRemName, bvSModName :: Symbol+bvAddName  = "bvadd"+bvSubName  = "bvsub"+bvMulName  = "bvmul"+bvUDivName = "bvudiv"+bvURemName = "bvurem"+bvSDivName = "bvsdiv"+bvSRemName = "bvsrem"+bvSModName = "bvsmod"++-- Comparisons+bvCompName, bvULtName, bvULeName, bvUGtName, bvUGeName :: Symbol+bvSLtName, bvSLeName, bvSGtName, bvSGeName :: Symbol+bvCompName = "bvcomp"+bvULtName  = "bvult"+bvULeName  = "bvule"+bvUGtName  = "bvugt"+bvUGeName  = "bvuge"+bvSLtName  = "bvslt"+bvSLeName  = "bvsle"+bvSGtName  = "bvsgt"+bvSGeName  = "bvsge"+ setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup :: Symbol setDif, setSng :: Symbol setEmpty = "Set_empty"@@ -169,199 +223,196 @@ string :: Raw string = strConName -bFun :: Raw -> [(Builder, Builder)] -> Builder -> Builder -> T.Text-bFun name xts out body = blt $ key "define-fun" (seqs [bb name, args, out, body])+bFun :: Raw -> [(Builder, Builder)] -> Builder -> Builder -> Builder+bFun name xts out body = key "define-fun" (seqs [fromText name, args, out, body])   where     args = parenSeqs [parens (x <+> t) | (x, t) <- xts] -bFun' :: Raw -> [Builder] -> Builder -> T.Text-bFun' name ts out = blt $ key "declare-fun" (seqs [bb name, args, out])+bFun' :: Raw -> [Builder] -> Builder -> Builder+bFun' name ts out = key "declare-fun" (seqs [fromText name, args, out])   where     args = parenSeqs ts -bSort :: Raw -> Builder -> T.Text-bSort name def = blt $ key "define-sort" (bb name <+> "()" <+> def)+bSort :: Raw -> Builder -> Builder+bSort name def = key "define-sort" (fromText name <+> "()" <+> def) -z3Preamble :: Config -> [T.Text]+z3Preamble :: Config -> [Builder] z3Preamble u   = stringPreamble u ++     [ bSort elt         "Int"     , bSort set-        (key2 "Array" (bb elt) "Bool")+        (key2 "Array" (fromText elt) "Bool")     , bFun emp         []-        (bb set)-        (parens (key "as const" (bb set) <+> "false"))+        (fromText set)+        (parens (key "as const" (fromText set) <+> "false"))     , bFun sng-        [("x", bb elt)]-        (bb set)-        (key3 "store" (parens (key "as const" (bb set) <+> "false")) "x" "true")+        [("x", fromText elt)]+        (fromText set)+        (key3 "store" (parens (key "as const" (fromText set) <+> "false")) "x" "true")     , bFun mem-        [("x", bb elt), ("s", bb set)]+        [("x", fromText elt), ("s", fromText set)]         "Bool"         "(select s x)"     , bFun add-        [("s", bb set), ("x", bb elt)]-        (bb set)+        [("s", fromText set), ("x", fromText elt)]+        (fromText set)         "(store s x true)"     , bFun cup-        [("s1", bb set), ("s2", bb set)]-        (bb set)+        [("s1", fromText set), ("s2", fromText set)]+        (fromText set)         "((_ map or) s1 s2)"     , bFun cap-        [("s1", bb set), ("s2", bb set)]-        (bb set)+        [("s1", fromText set), ("s2", fromText set)]+        (fromText set)         "((_ map and) s1 s2)"     , bFun com-        [("s", bb set)]-        (bb set)+        [("s", fromText set)]+        (fromText set)         "((_ map not) s)"     , bFun dif-        [("s1", bb set), ("s2", bb set)]-        (bb set)-        (key2 (bb cap) "s1" (key (bb com) "s2"))+        [("s1", fromText set), ("s2", fromText set)]+        (fromText set)+        (key2 (fromText cap) "s1" (key (fromText com) "s2"))     , bFun sub-        [("s1", bb set), ("s2", bb set)]+        [("s1", fromText set), ("s2", fromText set)]         "Bool"-        (key2 "=" (bb emp) (key2 (bb dif) "s1" "s2"))+        (key2 "=" (fromText emp) (key2 (fromText dif) "s1" "s2"))      -- Maps     , bSort map-        (key2 "Array" (bb elt) (bb elt))+        (key2 "Array" (fromText elt) (fromText elt))     , bFun sel-        [("m", bb map), ("k", bb elt)]-        (bb elt)+        [("m", fromText map), ("k", fromText elt)]+        (fromText elt)         "(select m k)"     , bFun sto-        [("m", bb map), ("k", bb elt), ("v", bb elt)]-        (bb map)+        [("m", fromText map), ("k", fromText elt), ("v", fromText elt)]+        (fromText map)         "(store m k v)"     , bFun mcup-        [("m1", bb map), ("m2", bb map)]-        (bb map)-        (key2 (key "_ map" (key2 "+" (parens (bb elt <+> bb elt)) (bb elt))) "m1" "m2")+        [("m1", fromText map), ("m2", fromText map)]+        (fromText map)+        (key2 (key "_ map" (key2 "+" (parens (fromText elt <+> fromText elt)) (fromText elt))) "m1" "m2")     , bFun mprj -- See [Interaction Between Map and Set]-        [("s", bb set), ("m", bb map)]-        (bb map)+        [("s", fromText set), ("m", fromText map)]+        (fromText map)         (key3           (key "_ map"             (key2 "ite"-              (parens ("Bool" <+> bb elt <+> bb elt))-              (bb elt)+              (parens ("Bool" <+> fromText elt <+> fromText elt))+              (fromText elt)             )           )           "s"           "m"-          (parens (key "as const" (key2 "Array" (bb elt) (bb elt)) <+> "0"))+          (parens (key "as const" (key2 "Array" (fromText elt) (fromText elt)) <+> "0"))         )     , bFun mToSet -- See [Interaction Between Map and Set]-        [("m", bb map)]-        (bb set)+        [("m", fromText map)]+        (fromText set)         (key2           (key "_ map"             (key2 ">"-              (parens (bb elt <+> bb elt))+              (parens (fromText elt <+> fromText elt))               "Bool"             )           )           "m"-          (parens (key "as const" (key2 "Array" (bb elt) (bb elt)) <+> "0"))+          (parens (key "as const" (key2 "Array" (fromText elt) (fromText elt)) <+> "0"))         )     , bFun mmax -- See [Map max and min]-        [("m1", bb map),("m2", bb map)]-        (bb map)+        [("m1", fromText map),("m2", fromText map)]+        (fromText map)         "(lambda ((i Int)) (ite (> (select m1 i) (select m2 i)) (select m1 i) (select m2 i)))"     , bFun mmin -- See [Map max and min]-        [("m1", bb map),("m2", bb map)]-        (bb map)+        [("m1", fromText map),("m2", fromText map)]+        (fromText map)         "(lambda ((i Int)) (ite (< (select m1 i) (select m2 i)) (select m1 i) (select m2 i)))"     , bFun mshift -- See [Map key shift]-        [("n", "Int"),("m", bb map)]-        (bb map)+        [("n", "Int"),("m", fromText map)]+        (fromText map)         "(lambda ((i Int)) (select m (- i n)))"     , bFun mdef-        [("v", bb elt)]-        (bb map)-        (key (key "as const" (parens (bb map))) "v")+        [("v", fromText elt)]+        (fromText map)+        (key (key "as const" (parens (fromText map))) "v")     , bFun boolToIntName         [("b", "Bool")]         "Int"         "(ite b 1 0)" -    , uifDef u (symbolLText mulFuncName) "*"-    , uifDef u (symbolLText divFuncName) "div"+    , uifDef u (symbolText mulFuncName) "*"+    , uifDef u (symbolText divFuncName) "div"     ] -symbolLText :: Symbol -> T.Text-symbolLText = T.fromStrict . symbolText- -- RJ: Am changing this to `Int` not `Real` as (1) we usually want `Int` and -- (2) have very different semantics. TODO: proper overloading, post genEApp-uifDef :: Config -> T.Text -> T.Text -> T.Text+uifDef :: Config -> Data.Text.Text -> Data.Text.Text -> Builder uifDef cfg f op   | linear cfg || Z3 /= solver cfg   = bFun' f ["Int", "Int"] "Int"   | otherwise-  = bFun f [("x", "Int"), ("y", "Int")] "Int" (key2 (bb op) "x" "y")+  = bFun f [("x", "Int"), ("y", "Int")] "Int" (key2 (fromText op) "x" "y") -cvc4Preamble :: Config -> [T.Text]+cvc4Preamble :: Config -> [Builder] cvc4Preamble z   = [        "(set-logic ALL_SUPPORTED)"]   ++ commonPreamble z   ++ cvc4MapPreamble z -commonPreamble :: Config -> [T.Text]+commonPreamble :: Config -> [Builder] commonPreamble _ --TODO use uif flag u (see z3Preamble)   = [ bSort elt    "Int"     , bSort set    "Int"     , bSort string "Int"-    , bFun' emp []               (bb set)-    , bFun' sng [bb elt]         (bb set)-    , bFun' add [bb set, bb elt] (bb set)-    , bFun' cup [bb set, bb set] (bb set)-    , bFun' cap [bb set, bb set] (bb set)-    , bFun' dif [bb set, bb set] (bb set)-    , bFun' sub [bb set, bb set] "Bool"-    , bFun' mem [bb elt, bb set] "Bool"+    , bFun' emp []               (fromText set)+    , bFun' sng [fromText elt]         (fromText set)+    , bFun' add [fromText set, fromText elt] (fromText set)+    , bFun' cup [fromText set, fromText set] (fromText set)+    , bFun' cap [fromText set, fromText set] (fromText set)+    , bFun' dif [fromText set, fromText set] (fromText set)+    , bFun' sub [fromText set, fromText set] "Bool"+    , bFun' mem [fromText elt, fromText set] "Bool"     , bFun boolToIntName [("b", "Bool")] "Int" "(ite b 1 0)"     ] -cvc4MapPreamble :: Config -> [T.Text]+cvc4MapPreamble :: Config -> [Builder] cvc4MapPreamble _ =-    [ bSort map    (key2 "Array" (bb elt) (bb elt))-    , bFun sel [("m", bb map), ("k", bb elt)]                (bb elt) "(select m k)"-    , bFun sto [("m", bb map), ("k", bb elt), ("v", bb elt)] (bb map) "(store m k v)"+    [ bSort map    (key2 "Array" (fromText elt) (fromText elt))+    , bFun sel [("m", fromText map), ("k", fromText elt)]                (fromText elt) "(select m k)"+    , bFun sto [("m", fromText map), ("k", fromText elt), ("v", fromText elt)] (fromText map) "(store m k v)"     ] -smtlibPreamble :: Config -> [T.Text]+smtlibPreamble :: Config -> [Builder] smtlibPreamble z --TODO use uif flag u (see z3Preamble)   = commonPreamble z  ++ [ bSort map "Int"-    , bFun' sel [bb map, bb elt] (bb elt)-    , bFun' sto [bb map, bb elt, bb elt] (bb map)+    , bFun' sel [fromText map, fromText elt] (fromText elt)+    , bFun' sto [fromText map, fromText elt, fromText elt] (fromText map)     ] -stringPreamble :: Config -> [T.Text]+stringPreamble :: Config -> [Builder] stringPreamble cfg | stringTheory cfg   = [ bSort string "String"-    , bFun strLen [("s", bb string)] "Int" (key (bb z3strlen) "s")-    , bFun strSubstr [("s", bb string), ("i", "Int"), ("j", "Int")] (bb string) (key (bb z3strsubstr) "s i j")-    , bFun strConcat [("x", bb string), ("y", bb string)] (bb string) (key (bb z3strconcat) "x y")+    , bFun strLen [("s", fromText string)] "Int" (key (fromText z3strlen) "s")+    , bFun strSubstr [("s", fromText string), ("i", "Int"), ("j", "Int")] (fromText string) (key (fromText z3strsubstr) "s i j")+    , bFun strConcat [("x", fromText string), ("y", fromText string)] (fromText string) (key (fromText z3strconcat) "x y")     ]  stringPreamble _   = [ bSort string "Int"-    , bFun' strLen [bb string] "Int"-    , bFun' strSubstr [bb string, "Int", "Int"] (bb string)-    , bFun' strConcat [bb string, bb string] (bb string)+    , bFun' strLen [fromText string] "Int"+    , bFun' strSubstr [fromText string, "Int", "Int"] (fromText string)+    , bFun' strConcat [fromText string, fromText string] (fromText string)     ]  -------------------------------------------------------------------------------- -- | Exported API -------------------------------------------------------------- -------------------------------------------------------------------------------- smt2Symbol :: SymEnv -> Symbol -> Maybe Builder-smt2Symbol env x = fromLazyText . tsRaw <$> symEnvTheory x env+smt2Symbol env x = fromText . tsRaw <$> symEnvTheory x env  instance SMTLIB2 SmtSort where   smt2 _ = smt2SmtSort@@ -370,9 +421,9 @@ smt2SmtSort SInt         = "Int" smt2SmtSort SReal        = "Real" smt2SmtSort SBool        = "Bool"-smt2SmtSort SString      = bb string-smt2SmtSort SSet         = bb set-smt2SmtSort SMap         = bb map+smt2SmtSort SString      = fromText string+smt2SmtSort SSet         = fromText set+smt2SmtSort SMap         = fromText map smt2SmtSort (SBitVec n)  = key "_ BitVec" (bShow n) smt2SmtSort (SVar n)     = "T" <> bShow n smt2SmtSort (SData c []) = symbolBuilder c@@ -388,9 +439,9 @@ smt2App :: VarAs -> SymEnv -> Expr -> [Builder] -> Maybe Builder -------------------------------------------------------------------------------- smt2App _ _ (dropECst -> EVar f) [d]-  | f == setEmpty = Just (bb emp)-  | f == setEmp   = Just (key2 "=" (bb emp) d)-  | f == setSng   = Just (key (bb sng) d) -- Just (key2 (bb add) (bb emp) d)+  | f == setEmpty = Just (fromText emp)+  | f == setEmp   = Just (key2 "=" (fromText emp) d)+  | f == setSng   = Just (key (fromText sng) d) -- Just (key2 (bb add) (bb emp) d)  smt2App k env f (d:ds)   | Just fb <- smt2AppArg k env f@@ -403,7 +454,7 @@   | Just fThy <- symEnvTheory f env   = Just $ if isPolyCtor fThy t             then k env f (ffuncOut t)-            else bb (tsRaw fThy)+            else fromText (tsRaw fThy)  smt2AppArg _ _ _   = Nothing@@ -434,7 +485,7 @@   Just (_, ts) -> Just (length ts - 1)   Nothing      -> Nothing -preamble :: Config -> SMTSolver -> [T.Text]+preamble :: Config -> SMTSolver -> [Builder] preamble u Z3   = z3Preamble u preamble u Cvc4 = cvc4Preamble u preamble u _    = smtlibPreamble u@@ -467,6 +518,7 @@   , interpSym setDif   dif   setBopSort   , interpSym setSub   sub   setCmpSort   , interpSym setCom   com   setCmpSort+   , interpSym mapSel   sel   mapSelSort   , interpSym mapSto   sto   mapStoSort   , interpSym mapCup   mcup  mapCupSort@@ -476,21 +528,80 @@   , interpSym mapPrj   mprj  mapPrjSort   , interpSym mapShift mshift mapShiftSort   , interpSym mapToSet mToSet mapToSetSort-  , interpSym bvOrName "bvor"   bvBopSort-  , interpSym bvAndName "bvand" bvBopSort+  -- , interpSym bvOrName  "bvor"  bvBopSort+  -- , interpSym bvAndName "bvand" bvBopSort+  -- , interpSym bvAddName "bvadd" bvBopSort+  -- , interpSym bvSubName "bvsub" bvBopSort+   , interpSym strLen    strLen    strLenSort   , interpSym strSubstr strSubstr substrSort   , interpSym strConcat strConcat concatstrSort   , interpSym boolInt   boolInt   (FFunc boolSort intSort)++  -- Function mappings for indexed identifier functions+  , interpSym' "_" iiSort+  , interpSym "app" "" appSort++  , interpSym' bvConcatName bvConcatSort+  , interpSym' bvExtractName (FFunc FInt bvExtendSort)+  , interpBvExt bvRepeatName+  , interpBvExt bvZeroExtName+  , interpBvExt bvSignExtName++  , interpBvUop bvNotName+  , interpBvUop bvNegName++  , interpBvBop bvAndName+  , interpBvBop bvNandName+  , interpBvBop bvOrName+  , interpBvBop bvNorName+  , interpBvBop bvXorName+  , interpBvBop bvXnorName++  , interpBvBop bvShlName+  , interpBvBop bvLShrName+  , interpBvBop bvAShrName+  , interpBvRot bvLRotName+  , interpBvRot bvRRotName++  , interpBvBop bvAddName+  , interpBvBop bvSubName+  , interpBvBop bvMulName+  , interpBvBop bvUDivName+  , interpBvBop bvURemName+  , interpBvBop bvSDivName+  , interpBvBop bvSRemName+  , interpBvBop bvSModName++  , interpSym' bvCompName bvEqSort+  , interpBvCmp bvULtName+  , interpBvCmp bvULeName+  , interpBvCmp bvUGtName+  , interpBvCmp bvUGeName+  , interpBvCmp bvSLtName+  , interpBvCmp bvSLeName+  , interpBvCmp bvSGtName+  , interpBvCmp bvSGeName++  , interpSym intbv32Name "(_ int2bv 32)"   (FFunc intSort bv32)+  , interpSym intbv64Name "(_ int2bv 64)"   (FFunc intSort bv64)+  , interpSym bv32intName  "(_ bv2int 32)"  (FFunc bv32    intSort)+  , interpSym bv64intName   "(_ bv2int 64)" (FFunc bv64    intSort)+   ]   where+    -- (sizedBitVecSort "Size1")+    bv32       = sizedBitVecSort "Size32"+    bv64       = sizedBitVecSort "Size64"     boolInt    = boolToIntName     setAddSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (FVar 0)           (setSort $ FVar 0)     setBopSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) (setSort $ FVar 0)     setMemSort = FAbs 0 $ FFunc (FVar 0) $ FFunc (setSort $ FVar 0) boolSort     setCmpSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) boolSort+    -- select :: forall i a. Map i a -> i -> a     mapSelSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1))                                  $ FFunc (FVar 0) (FVar 1)+    -- cup :: forall i. Map i Int -> Map i Int -> Map i Int     mapCupSort = FAbs 0          $ FFunc (mapSort (FVar 0) intSort)                                  $ FFunc (mapSort (FVar 0) intSort)                                          (mapSort (FVar 0) intSort)@@ -503,6 +614,7 @@                                  $ FFunc (mapSort intSort (FVar 0))                                          (mapSort intSort (FVar 0))     mapToSetSort = FAbs 0        $ FFunc (mapSort (FVar 0) intSort) (setSort (FVar 0))+    -- store :: forall i a. Map i a -> i -> a -> Map i a     mapStoSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1))                                  $ FFunc (FVar 0)                                  $ FFunc (FVar 1)@@ -510,8 +622,83 @@     mapDefSort = FAbs 0 $ FAbs 1 $ FFunc (FVar 1)                                          (mapSort (FVar 0) (FVar 1)) -    bvBopSort  = FFunc bitVecSort $ FFunc bitVecSort bitVecSort +interpBvUop :: Symbol -> (Symbol, TheorySymbol)+interpBvUop name = interpSym' name bvUopSort+interpBvBop :: Symbol -> (Symbol, TheorySymbol)+interpBvBop name = interpSym' name bvBopSort+interpBvCmp :: Symbol -> (Symbol, TheorySymbol)+interpBvCmp name = interpSym' name bvCmpSort+interpBvExt :: Symbol -> (Symbol, TheorySymbol)+interpBvExt name = interpSym' name bvExtendSort+interpBvRot :: Symbol -> (Symbol, TheorySymbol)+interpBvRot name = interpSym' name bvRotSort++interpSym' :: Symbol -> Sort -> (Symbol, TheorySymbol)+interpSym' name = interpSym name (Data.Text.pack $ symbolString name)++-- Indexed Identifier sort.+-- Together with 'app', this allows one to write indexed identifier+-- functions (smtlib2 specific functions). (e.g. ((_ sign_extend 1) bv))+--+-- The idea here is that 'app' is elaborated to the empty string,+-- and '_' does the typelit application as it does in smtlib2.+--+-- Then if we write, (app (_ sign_extend 1) bv), LF will elaborate+-- it as ( (_ sign_extend 1) bv). Fitting the smtlib2 format exactly!+--+-- One thing to note, is that any indexed identifier function (like+-- sign_extend) has to have no FAbs in it. Otherwise, they will be+-- elaborated like e.g. ( (_ (as sign_extend Int) 1) bv), which is wrong!+--+-- _ :: forall a b c. (a -> b -> c) -> a -> (b -> c)+iiSort :: Sort+iiSort = FAbs 0 $ FAbs 1 $ FAbs 2 $ FFunc+               (FFunc (FVar 0) $ FFunc (FVar 1) (FVar 2))+               (FFunc (FVar 0) $ FFunc (FVar 1) (FVar 2))++-- Simple application, used for indexed identifier function, check '_'.+--+-- app :: forall a b. (a -> b) -> a -> b+appSort :: Sort+appSort = FAbs 0 $ FAbs 1 $ FFunc+                (FFunc (FVar 0) (FVar 1))+                (FFunc (FVar 0) (FVar 1))++-- Indexed identifier operation, purposely didn't place FAbs!+--+-- extend :: Int -> BitVec a -> BitVec b+bvExtendSort :: Sort+bvExtendSort  = FFunc FInt $ FFunc (bitVecSort 1) (bitVecSort 2)++-- Indexed identifier operation, purposely didn't place FAbs!+--+-- rot :: Int -> BitVec a -> BitVec a+bvRotSort :: Sort+bvRotSort  = FFunc FInt $ FFunc (bitVecSort 0) (bitVecSort 0)++-- uOp :: forall a. BitVec a -> BitVec a+bvUopSort :: Sort+bvUopSort = FAbs 0 $ FFunc (bitVecSort 0) (bitVecSort 0)++-- bOp :: forall a. BitVec a -> BitVec a -> BitVec a+bvBopSort :: Sort+bvBopSort = FAbs 0 $ FFunc (bitVecSort 0) $ FFunc (bitVecSort 0) (bitVecSort 0)+-- bvBopSort = FAbs 0 $ FFunc (bitVecSort (FVar 0)) (FFunc (bitVecSort (FVar 0)) (bitVecSort (FVar 0)))++-- cmp :: forall a. BitVec a -> BitVec a -> Bool+bvCmpSort :: Sort+bvCmpSort = FAbs 0 $ FFunc (bitVecSort 0) $ FFunc (bitVecSort 0) boolSort++-- eq :: forall a. BitVec a -> BitVec a -> BitVec 1+bvEqSort :: Sort+bvEqSort = FAbs 0 $ FFunc (bitVecSort 0) $ FFunc (bitVecSort 0) (sizedBitVecSort "Size1")++-- concat :: forall a b c. BitVec a -> BitVec b -> BitVec c+bvConcatSort :: Sort+bvConcatSort = FAbs 0 $ FAbs 1 $ FAbs 2 $+                     FFunc (bitVecSort 0) $ FFunc (bitVecSort 1) (bitVecSort 2)+ interpSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol) interpSym x n t = (x, Thy x n t Theory) @@ -570,8 +757,8 @@     sx         = testSymbol x     raw        = "is-" <> symbolRaw x -symbolRaw :: Symbol -> T.Text-symbolRaw = T.fromStrict . symbolSafeText+symbolRaw :: Symbol -> Data.Text.Text+symbolRaw = symbolSafeText  -------------------------------------------------------------------------------- selectSymbols :: DataDecl -> [(Symbol, TheorySymbol)]

@@ -28,15 +28,13 @@      ) where -import           Control.Concurrent.Async (Async)-import           Control.Concurrent.STM (TVar)+import           Data.ByteString.Builder (Builder) import           Language.Fixpoint.Types-import           Language.Fixpoint.Utils.Builder (Builder) import qualified Data.Text                as T import           Text.PrettyPrint.HughesPJ+import qualified SMTLIB.Backends  import           System.IO                (Handle)-import           System.Process -- import           Language.Fixpoint.Misc   (traceShow)  --------------------------------------------------------------------------------@@ -93,19 +91,16 @@                   | Error !T.Text                   deriving (Eq, Show) --- | Information about the external SMT process+-- | Additional information around the SMT solver backend data Context = Ctx-  { ctxPid     :: !ProcessHandle-    -- | The handle for writing queries to, for input to the SMT solver.-  , ctxIn      :: !Handle-    -- | The handle for reading responses from, the output from the SMT solver.-  , ctxOut     :: !Handle+  {+  -- | The high-level interface for interacting with the SMT solver backend.+    ctxSolver  :: SMTLIB.Backends.Solver+  -- | The close operation of the SMT solver backend.+  , ctxClose   :: IO ()   , ctxLog     :: !(Maybe Handle)   , ctxVerbose :: !Bool   , ctxSymEnv  :: !SymEnv-  , ctxAsync   :: Async ()-    -- | The next batch of queries to send to the SMT solver-  , ctxTVar    :: TVar Builder   }  --------------------------------------------------------------------------------

@@ -98,7 +98,7 @@ -------------------------------------------------------------------------------- -- | Solve FInfo system of horn-clause constraints ----------------------------- ---------------------------------------------------------------------------------solve :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a+solve :: (PPrint a, NFData a, Fixpoint a, Show a, Loc a) => Solver a -------------------------------------------------------------------------------- solve cfg q   | parts cfg      = partition  cfg        $!! q@@ -108,7 +108,7 @@   | minimizeKs cfg = minKvars cfg solve'   $!! q   | otherwise      = solve'     cfg        $!! q -solve' :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a+solve' :: (PPrint a, NFData a, Fixpoint a, Show a, Loc a) => Solver a solve' cfg q = do   when (save cfg) $ saveQuery   cfg q   configSW  cfg     solveNative cfg q@@ -181,19 +181,19 @@ -------------------------------------------------------------------------------- -- | Native Haskell Solver ----------------------------------------------------- ---------------------------------------------------------------------------------solveNative, solveNative' :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a+solveNative, solveNative' :: (NFData a, Fixpoint a, Show a, Loc a, PPrint a) => Solver a -------------------------------------------------------------------------------- solveNative !cfg !fi0 = solveNative' cfg fi0                           `catch`                              (return . crashResult (errorMap fi0)) -crashResult :: ErrorMap a -> Error -> Result (Integer, a)+crashResult :: (PPrint a) => ErrorMap a -> Error -> Result (Integer, a) crashResult m e = Result res mempty mempty mempty   where     res           = Crash es msg     es            = catMaybes [ findError m e | e <- errs e ]     msg | null es = showpp e-        | otherwise = "Sorry, unexpected panic in liquid-fixpoint!"+        | otherwise = "Sorry, unexpected panic in liquid-fixpoint!" -- ++ showpp e  -- | Unpleasant hack to save meta-data that can be recovered from SrcSpan type ErrorMap a = HashMap.HashMap SrcSpan a

@@ -345,7 +345,7 @@ evaluate cfg ctx aenv facts es sid = do   let eqs      = initEqualities ctx aenv facts   let γ        = knowledge cfg ctx aenv-  let cands    = mytracepp  ("evaluate-cands " ++ showpp sid) $ Misc.hashNub (concatMap topApps es)+  let cands    = mytracepp  ("evaluate-cands " ++ showpp sid) $ Misc.setNub (concatMap topApps es)   let s0       = EvalEnv 0 [] aenv (SMT.ctxSymEnv ctx) cfg   let ctxEqs   = [ toSMT cfg ctx [] (EEq e1 e2) | (e1, e2)  <- eqs ]               ++ [ toSMT cfg ctx [] (expr xr)   | xr@(_, r) <- facts, null (Vis.kvarsExpr $ reftPred $ sr_reft r) ]@@ -694,7 +694,7 @@ initEqualities :: SMT.Context -> AxiomEnv -> [(Symbol, SortedReft)] -> [(Expr, Expr)] initEqualities ctx aenv es = concatMap (makeSimplifications (aenvSimpl aenv)) dcEqs   where-    dcEqs                  = Misc.hashNub (Mb.catMaybes [getDCEquality senv e1 e2 | EEq e1 e2 <- atoms])+    dcEqs                  = Misc.setNub (Mb.catMaybes [getDCEquality senv e1 e2 | EEq e1 e2 <- atoms])     atoms                  = splitPAnd . expr =<< filter isProof es     senv                   = SMT.ctxSymEnv ctx @@ -799,7 +799,7 @@   ctx <- SMT.makeContextWithSEnv cfg file env   _   <- SMT.smtPush ctx   res <- k ctx-  _   <- SMT.cleanupContext ctx+  SMT.cleanupContext ctx   return res  infixl 9 ~>

@@ -77,7 +77,6 @@ runSolverM cfg sI act =   bracket acquire release $ \ctx -> do     res <- runStateT act' (s0 ctx)-    smtExit ctx     return (fst res)   where     s0 ctx   = SS ctx be (stats0 fi)@@ -200,15 +199,12 @@ {-# SCC filterValid_ #-} filterValid_ :: F.SrcSpan -> F.Expr -> F.Cand a -> Context -> IO [a] filterValid_ sp p qs me = catMaybes <$> do-  smtAssertAsync me p-  forM_ qs $ \(q, _x) ->-    smtBracketAsyncAt sp me "filterValidRHS" $ do-      smtAssertAsync me (F.PNot q)-      smtCheckUnsatAsync me-  forM qs $ \(_, x) -> do-    valid <- readCheckUnsat me-    return $ if valid then Just x else Nothing-+  smtAssert me p+  forM qs $ \(q, x) ->+    smtBracketAt sp me "filterValidRHS" $ do+      smtAssert me (F.PNot q)+      valid <- smtCheckUnsat me+      return $ if valid then Just x else Nothing  -------------------------------------------------------------------------------- -- | `filterValidGradual ps [(x1, q1),...,(xn, qn)]` returns the list `[ xi | p => qi]`

@@ -792,24 +792,15 @@                 let (es1,es2) = splitAt (length (eqArgs eq)) es                     newE = substEq env eq es1                 (e', fe) <- evalIte γ ctx et newE -- TODO:FUEL this is where an "unfolding" happens, CHECK/BUMP counter-                let mPLEUnfold = startsWithPLEUnfold e'-                    e2' = Mb.fromMaybe e' mPLEUnfold+                let e2' = stripPLEUnfold e'                     e3' = simplify γ ctx (eApps e2' es2) -- reduces a bit the equations                     undecidedGuards = case e' of                       EIte{} -> True                       _ -> False -                if not undecidedGuards || Mb.isJust mPLEUnfold+                if undecidedGuards                   then do-                    useFuel f                     modify $ \st ->-                      st-                        { evNewEqualities = S.insert (eApps e0 es, e3') (evNewEqualities st)-                        , evPendingUnfoldings = M.delete (eApps e0 es) (evPendingUnfoldings st)-                        }-                    return (Just e2', fe)-                  else do-                    modify $ \st ->                       st {                         evPendingUnfoldings = M.insert (eApps e0 es) e3' (evPendingUnfoldings st)                       }@@ -817,6 +808,14 @@                     -- guarding it, just to preserve the size of further                     -- rewrites.                     return (Nothing, noExpand)+                  else do+                    useFuel f+                    modify $ \st ->+                      st+                        { evNewEqualities = S.insert (eApps e0 es, e3') (evNewEqualities st)+                        , evPendingUnfoldings = M.delete (eApps e0 es) (evPendingUnfoldings st)+                        }+                    return (Just e2', fe)          else return (Nothing, noExpand)   where     -- At the time of writing, any function application wrapping an@@ -824,12 +823,12 @@     -- However, using pleUnfold still has the advantage of not generating     -- extra equations to unfold pleUnfold itself. Using pleUnfold also     -- makes the intention of the user rather explicit.-    startsWithPLEUnfold e+    stripPLEUnfold e       | (ef, [arg]) <- splitEAppThroughECst e       , EVar f <- dropECst ef       , f == "Language.Haskell.Liquid.ProofCombinators.pleUnfold"-      = Just arg-      | otherwise = Nothing+      = arg+      | otherwise = e  evalApp γ ctx e0 args@(e:es) _   | EVar f <- dropECst e0@@ -1094,7 +1093,7 @@   ctx <- SMT.makeContextWithSEnv cfg file env   _   <- SMT.smtPush ctx   res <- k ctx-  _   <- SMT.cleanupContext ctx+  SMT.cleanupContext ctx   return res  

@@ -409,7 +409,7 @@     env0         = F.symEnv sEnv tEnv ds lits ts     tEnv         = Thy.theorySymbols ds     ds           = F.ddecls si-    ts           = Misc.hashNub (applySorts si ++ [t | (_, t) <- F.toListSEnv sEnv])+    ts           = Misc.setNub (applySorts si ++ [t | (_, t) <- F.toListSEnv sEnv])     sEnv         = (F.tsSort <$> tEnv) `mappend` F.fromListSEnv xts     xts          = symbolSorts cfg si ++ alits     lits         = F.dLits si `F.unionSEnv'` F.fromListSEnv alits

@@ -209,6 +209,7 @@ instance (Loc a) => Elaborate (SimpC a) where   elaborate msg env c = c {_crhs = elaborate msg' env (_crhs c) }     where msg'        = atLoc c (val msg)+ -------------------------------------------------------------------------------- -- | 'elabExpr' adds "casts" to decorate polymorphic instantiation sites. --------------------------------------------------------------------------------

@@ -22,6 +22,9 @@   , Eliminate (..)   , useElim +  -- * Scrape options+  , Scrape (..)+   -- * parallel solving options   , defaultMinPartSize   , defaultMaxPartSize@@ -33,24 +36,24 @@ import qualified Data.Store as S import qualified Data.List as L import Data.Serialize                (Serialize (..))-import Control.Monad import Control.DeepSeq import GHC.Generics import System.Console.CmdArgs import System.Console.CmdArgs.Explicit-import System.Environment +import qualified Language.Fixpoint.Conditional.Z3 as Conditional.Z3 import Language.Fixpoint.Utils.Files   -------------------------------------------------------------------------------- withPragmas :: Config -> [String] -> IO Config ---------------------------------------------------------------------------------withPragmas = foldM withPragma--withPragma :: Config -> String -> IO Config-withPragma c s = withArgs [s] $ cmdArgsRun-          config { modeValue = (modeValue config) { cmdArgsValue = c } }+withPragmas c s =+    processValueIO+      config { modeValue = (modeValue config) { cmdArgsValue = c } }+      s+    >>=+      cmdArgsApply  -------------------------------------------------------------------------------- -- | Configuration Options -----------------------------------------------------@@ -75,6 +78,7 @@   , allowHO     :: Bool                -- ^ allow higher order binders in the logic environment   , allowHOqs   :: Bool                -- ^ allow higher order qualifiers   , eliminate   :: Eliminate           -- ^ eliminate non-cut KVars+  , scrape      :: Scrape              -- ^ configure auto-scraping of qualifiers from constraints   , elimBound   :: Maybe Int           -- ^ maximum length of KVar chain to eliminate   , smtTimeout  :: Maybe Int           -- ^ smt timeout in msec   , elimStats   :: Bool                -- ^ print eliminate stats@@ -139,20 +143,42 @@  --------------------------------------------------------------------------------------- -data SMTSolver = Z3 | Cvc4 | Mathsat+data SMTSolver = Z3 | Z3mem | Cvc4 | Mathsat                  deriving (Eq, Data, Typeable, Generic)  instance Default SMTSolver where-  def = Z3+  def = if Conditional.Z3.builtWithZ3AsALibrary then Z3mem else Z3  instance Show SMTSolver where   show Z3      = "z3"+  show Z3mem   = "z3 API"   show Cvc4    = "cvc4"   show Mathsat = "mathsat"  instance S.Store SMTSolver  ---------------------------------------------------------------------------------------+-- | `Scrape` describes which (Horn) constraints to scrape qualifiers from+--   None = do not scrape, only use the supplied qualifiers+--   Head = scrape only from the constraint heads (i.e. "rhs")+--   All  = scrape all concrete predicates (i.e. "rhs" + "lhs")++data Scrape = No | Head | Both+  deriving (Eq, Data, Typeable, Generic)++instance Serialize Scrape+instance S.Store Scrape+instance NFData Scrape++instance Default Scrape where+  def = No++instance Show Scrape where+  show No   = "no"+  show Head = "head"+  show Both = "both"++--------------------------------------------------------------------------------------- -- | Eliminate describes the number of KVars to eliminate: --   None = use PA/Quals for ALL k-vars, i.e. no eliminate --   Some = use PA/Quals for CUT k-vars, i.e. eliminate non-cuts@@ -199,6 +225,7 @@   , allowHO                  = False   &= help "Allow higher order binders into fixpoint environment"   , allowHOqs                = False   &= help "Allow higher order qualifiers"   , eliminate                = None    &= help "Eliminate KVars [none = quals for all-kvars, cuts = quals for cut-kvars, all = eliminate all-kvars (TRUE for cuts)]"+  , scrape                   = def     &= help "Scrape qualifiers from constraint (Horn format only) [ no = do not, head = scrape from heads, both = scrape from everywhere ]"   , elimBound                = Nothing &= name "elimBound"   &= help "(alpha) Maximum eliminate-chain depth"   , smtTimeout               = Nothing &= name "smtTimeout"  &= help "smt timeout in msec"   , elimStats                = False   &= help "(alpha) Print eliminate stats"

@@ -473,8 +473,8 @@ addIds = zipWith (\i c -> (i, shiftId i $ c {_sid = Just i})) [1..]   where     -- Adding shiftId to have distinct VV for SMT conversion-    shiftId i c = c { slhs = shiftSR i $ slhs c }-                    { srhs = shiftSR i $ srhs c }+    shiftId i c = c { slhs = shiftSR i (slhs c) }+                    { srhs = shiftSR i (srhs c) }     shiftSR i sr = sr { sr_reft = shiftR i $ sr_reft sr }     shiftR i r@(Reft (v, _)) = shiftVV r (intSymbol v i) @@ -542,6 +542,7 @@  instance PPrint Qualifier where   pprintTidy k q = "qualif" <+> pprintTidy k (qName q) <+> "defined at" <+> pprintTidy k (qPos q)+  -- pprintTidy _ q = pprQual q  pprQual :: Qualifier -> Doc pprQual (Q n xts p l) = text "qualif" <+> text (symbolString n) <-> parens args <-> colon <+> parens (toFix p) <+> text "//" <+> toFix l

@@ -102,12 +102,12 @@   , nilName   , consName   , vvName-  , size32Name-  , size64Name+  , sizeName   , bitVecName-  , bvAndName-  , bvOrName+  -- , bvAndName, bvOrName, bvSubName, bvAddName+  , intbv32Name, intbv64Name, bv32intName, bv64intName   , propConName+   -- HKT , tyAppName   , isPrim   , prims@@ -128,6 +128,7 @@  import           Control.DeepSeq             (NFData (..)) import           Control.Arrow               (second)+import           Data.ByteString.Builder     (Builder) import           Data.Char                   (ord) import           Data.Maybe                  (fromMaybe) import           Data.Generics               (Data)@@ -144,7 +145,7 @@ import           Text.PrettyPrint.HughesPJ   (text) import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Spans-import           Language.Fixpoint.Utils.Builder as Builder (Builder, fromText)+import           Language.Fixpoint.Utils.Builder as Builder (fromText) import Data.Functor.Contravariant (Contravariant(contramap)) import qualified Data.Binary as B @@ -546,7 +547,7 @@ symbolBuilder = Builder.fromText . symbolSafeText . symbol  {-# INLINE buildMany #-}-buildMany :: [Builder.Builder] -> Builder.Builder+buildMany :: [Builder] -> Builder buildMany []     = mempty buildMany [b]    = b buildMany (b:bs) = b <> mconcat [ " " <> b' | b' <- bs ]@@ -618,18 +619,31 @@ symSepName   :: (IsString a) => a symSepName   = "##" -nilName, consName, size32Name, size64Name, bitVecName, bvOrName, bvAndName :: Symbol-nilName      = "nil"-consName     = "cons"-size32Name   = "Size32"-size64Name   = "Size64"-bitVecName   = "BitVec"-bvOrName     = "bvor"-bvAndName    = "bvand"+-- nilName, consName, size32Name, size64Name, bitVecName :: Symbol+-- nilName      = "nil"+-- consName     = "cons"+-- size32Name   = "Size32"+-- size64Name   = "Size64"+-- bitVecName   = "BitVec" --- HKT tyAppName :: Symbol--- HKT tyAppName    = "LF-App"+-- bvOrName, bvAndName, bvSubName, bvAddName,+intbv32Name, intbv64Name, bv32intName, bv64intName :: Symbol+-- bvOrName    = "bvor"+-- bvAndName   = "bvand"+-- bvSubName   = "bvsub"+-- bvAddName   = "bvadd"+intbv32Name = "int_to_bv32"+intbv64Name = "int_to_bv64"+bv32intName = "bv32_to_int"+bv64intName = "bv64_to_int" +nilName, consName, sizeName, bitVecName :: Symbol+nilName       = "nil"+consName      = "cons"+sizeName      = "Size"+bitVecName    = "BitVec"++ mulFuncName, divFuncName :: Symbol mulFuncName  = "Z3_OP_MUL" divFuncName  = "Z3_OP_DIV"@@ -663,11 +677,13 @@   , "Map_store"   , "Map_union"   , "Map_default"-  , size32Name-  , size64Name+  -- Currently we parse X in "SizeX" to get the bitvec size+  -- so there is no finite set of names to add here...+  -- , size32Name+  -- , size64Name   , bitVecName-  , bvOrName-  , bvAndName+  -- , bvOrName+  -- , bvAndName   , "FAppTy"   , nilName   , consName

@@ -93,6 +93,7 @@ notracepp :: (PPrint a) => String -> a -> a notracepp _ x = x + instance PPrint Doc where   pprintTidy _ = id @@ -111,6 +112,10 @@  instance (Ord a, PPrint a, PPrint b) => PPrint (M.HashMap a b) where   pprintTidy k = pprintKVs k . hashMapToAscList++instance PPrint Char where+  pprintTidy _ = char+  pprintKVs   :: (PPrint k, PPrint v) => Tidy -> [(k, v)] -> Doc pprintKVs t = vcat . punctuate "\n" . map pp1

@@ -77,7 +77,7 @@    -- * Destructing   , flattenRefas-  , conjuncts+  , conjuncts, concConjuncts   , dropECst   , eApps   , eAppC@@ -183,9 +183,13 @@ reftConjuncts (Reft (v, ra)) = [Reft (v, ra') | ra' <- ras']   where     ras'                     = if null ps then ks else conj ps : ks  -- see [NOTE:pAnd-SLOW]-    (ks, ps)                 = partition (\p -> isKvar p || isGradual p) $ refaConjuncts ra+    (ps, ks)                 = partition isConc (refaConjuncts ra) +isConc :: Expr -> Bool+isConc p = not (isKvar p || isGradual p) +concConjuncts :: Expr -> [Expr]+concConjuncts e = filter isConc (refaConjuncts e)  isKvar :: Expr -> Bool isKvar (PKVar _ _) = True@@ -224,6 +228,8 @@  refaConjuncts :: Expr -> [Expr] refaConjuncts p = [p' | p' <- conjuncts p, not $ isTautoPred p']++  -------------------------------------------------------------------------------- -- | Kvars ---------------------------------------------------------------------

@@ -16,10 +16,7 @@  -- | This module contains the data types, operations and --   serialization functions for representing Fixpoint's---   implication (i.e. subtyping) and well-formedness---   constraints in Haskell. The actual constraint---   solving is done by the `fixpoint.native` which---   is written in Ocaml.+--   Horn and well-formedness constraints.  module Language.Fixpoint.Types.Sorts ( @@ -37,10 +34,11 @@   , setFTyCon   , mapFTyCon -- TODO: hide these   , mapFVar-   , basicSorts, intSort, realSort, boolSort, strSort, funcSort-  , setSort, bitVecSort, mapSort, charSort-+  -- , bitVec32Sort, bitVec64Sort+  , setSort, bitVecSort+  , sizedBitVecSort+  , mapSort, charSort   , listFTyCon   , isListTC   , sizeBv@@ -102,6 +100,7 @@ import qualified Data.HashMap.Strict       as M import qualified Data.List                 as L import qualified Data.Binary as B+import Text.Read (readMaybe)  data FTycon   = TC LocSymbol TCInfo deriving (Ord, Show, Data, Typeable, Generic) @@ -160,12 +159,10 @@ isListTC (TC z _) = isListConName z  sizeBv :: FTycon -> Maybe Int-sizeBv tc-  | s == size32Name = Just 32-  | s == size64Name = Just 64-  | otherwise       = Nothing-  where-    s               = val $ fTyconSymbol tc+sizeBv tc = do+  let s = val $ fTyconSymbol tc+  size <- stripPrefix sizeName s+  readMaybe $ symbolString size  fTyconSymbol :: FTycon -> Located Symbol fTyconSymbol (TC s _) = s@@ -485,8 +482,20 @@ setSort :: Sort -> Sort setSort    = FApp (FTC setFTyCon) -bitVecSort :: Sort-bitVecSort = FApp (FTC $ symbolFTycon' bitVecName) (FTC $ symbolFTycon' size32Name)+-- bitVecSort :: Sort -> Sort+-- bitVecSort = FApp (FTC $ symbolFTycon' bitVecName)++-- bitVec32Sort :: Sort+-- bitVec32Sort = bitVecSort (FTC (symbolFTycon' size32Name))+--+-- bitVec64Sort :: Sort+-- bitVec64Sort = bitVecSort (FTC (symbolFTycon' size64Name))++bitVecSort :: Int -> Sort+bitVecSort i = FApp (FTC $ symbolFTycon' bitVecName) (FVar i)++sizedBitVecSort :: Symbol -> Sort+sizedBitVecSort i = FApp (FTC $ symbolFTycon' bitVecName) (FTC $ symbolFTycon' i)  mapSort :: Sort -> Sort -> Sort mapSort = FApp . FApp (FTC (symbolFTycon' mapConName))

@@ -52,21 +52,14 @@ import qualified Data.List                as L import           Data.Text (Text) import qualified Data.Text                as Text-import qualified Data.Text.Lazy           as LT import qualified Data.Store              as S import qualified Data.HashMap.Strict      as M import qualified Language.Fixpoint.Misc   as Misc-import Data.Functor.Contravariant (Contravariant(contramap))  -------------------------------------------------------------------------------- -- | 'Raw' is the low-level representation for SMT values ---------------------------------------------------------------------------------type Raw = LT.Text--instance S.Store Raw where-  peek = LT.fromStrict <$> S.peek-  poke = S.poke . LT.toStrict-  size = contramap LT.toStrict S.size+type Raw = Text  -------------------------------------------------------------------------------- -- | 'SymEnv' is used to resolve the 'Sort' and 'Sem' of each 'Symbol'

@@ -3,11 +3,8 @@ -- | Wrapper around `Data.Text.Builder` that exports some useful combinators  module Language.Fixpoint.Utils.Builder-  ( Builder-  , fromLazyText+  ( fromText   , fromString-  , fromText-  , toLazyText   , parens   , (<+>)   , parenSeqs@@ -17,47 +14,20 @@   , key3   , bShow   , bFloat-  , bb-  , lbb-  , blt   ) where  import           Data.Foldable (fold) import           Data.String-import qualified Data.Text.Lazy.Builder as B-import qualified Data.Text.Lazy         as LT+import Data.ByteString.Builder (Builder)+import qualified Data.ByteString.Builder as B import qualified Data.Text              as T+import qualified Data.Text.Encoding     as T import qualified Data.List              as L import qualified Numeric --- | Offers efficient concatenation, no matter the associativity-data Builder-  = Node Builder Builder-  | Leaf B.Builder -instance Eq Builder where-  b0 == b1 = toLazyText b0 == toLazyText b1--instance IsString Builder where-  fromString = Leaf . fromString--instance Semigroup Builder where-  (<>) = Node--instance Monoid Builder where-  mempty = Leaf mempty--toLazyText :: Builder -> LT.Text-toLazyText = B.toLazyText . go mempty-  where-    go tl (Leaf b) = b <> tl-    go tl (Node t0 t1) = go (go tl t1) t0--fromLazyText :: LT.Text -> Builder-fromLazyText = Leaf . B.fromLazyText- fromText :: T.Text -> Builder-fromText = Leaf . B.fromText+fromText t = B.byteString $ T.encodeUtf8 t  parens :: Builder -> Builder parens b = "(" <>  b <> ")"@@ -86,13 +56,3 @@  bFloat :: RealFloat a => a -> Builder bFloat d = fromString (Numeric.showFFloat Nothing d "")--bb :: LT.Text -> Builder-bb = fromLazyText--lbb :: T.Text -> Builder-lbb = bb . LT.fromStrict--blt :: Builder -> LT.Text-blt = toLazyText-

@@ -0,0 +1,65 @@+// This file showcases bitvector functions that in smtlib2 are+// indexed identifiers. This means that instead of writing+// (zero_extend 2 bv) to extend a bitvector by 2 bits, we+// write ((_ zero_extend 2) bv).++// You can see the '_' as kind of applying type level arguments.+// In the case of 'zero_extend', it determines the size of the+// output bitvector. ++// To emulate this in liquid fixpoint, we want the output to +// match exactly the format of indexed identifiers of smtlib2. +// This comes down to defining our own '_' and parenthesizing +// the expression in LF exactly as we would in the smt format.++// The last trick here, is that we cannot apply a parenthesized+// expression to an expression. For this we have defined the +// additional expression 'app', which simply applies its operands.+// 'app' is elaborated to the empty string to the SMT solver, such+// that (app (_ zero_extend 2) bv) becomes ( (_ zero_extend 2) bv).++bind 0 x : {v : (BitVec Size4) | v = (lit "#b1000" (BitVec Size4))}+bind 1 y : {v : (BitVec Size4) | v = (app (_ rotate_right 7) x)}+bind 2 z : {v : (BitVec Size4) | v = (lit "#b0001" (BitVec Size4))}++constraint:+  env [0;1;2]+  lhs {v : (BitVec Size4) | [ v = y ] }+  rhs {v : (BitVec Size4) | [ v = z ] }+  id 0 tag []++bind 3 y : {v : (BitVec Size6) | v = (app (_ zero_extend 2) x)}+bind 4 z : {v : (BitVec Size6) | v = (lit "#b001000" (BitVec Size6))}++constraint:+  env [0;3;4]+  lhs {v : (BitVec Size6) | [ v = y ] }+  rhs {v : (BitVec Size6) | [ v = z ] }+  id 1 tag []++bind 5 y : {v : (BitVec Size6) | v = (app (_ sign_extend 2) x)}+bind 6 z : {v : (BitVec Size6) | v = (lit "#b111000" (BitVec Size6))}++constraint:+  env [0;5;6]+  lhs {v : (BitVec Size6) | [ v = y ] }+  rhs {v : (BitVec Size6) | [ v = z ] }+  id 2 tag []++bind 7 y : {v : (BitVec Size8) | v = (app (_ repeat 2) x)}+bind 8 z : {v : (BitVec Size8) | v = (lit "#b10001000" (BitVec Size8))}++constraint:+  env [0;7;8]+  lhs {v : (BitVec Size8) | [ v = y ] }+  rhs {v : (BitVec Size8) | [ v = z ] }+  id 3 tag []++bind 9  y : {v : (BitVec Size2) | v = (app (_ extract 3 2) x)}+bind 10 z : {v : (BitVec Size2) | v = (lit "#b10" (BitVec Size2))}++constraint:+  env [0;9;10]+  lhs {v : (BitVec Size2) | [ v = y ] }+  rhs {v : (BitVec Size2) | [ v = z ] }+  id 4 tag []

@@ -0,0 +1,89 @@+bind 0 x : {v : (BitVec Size32) | [ v = (lit "#x0000000f" (BitVec Size32))]}+bind 1 y : {v : (BitVec Size32) | [ v = (lit "#x000000f0" (BitVec Size32))]}+bind 2 z : {v : (BitVec Size32) | [ v = (lit "#x000000ff" (BitVec Size32))]}++constraint:+  env [0;1;2]+  lhs {v : (BitVec Size32) | [ v = bvor x y ] }+  rhs {v : (BitVec Size32) | [ v = z ] }+  id 0 tag []++bind 4 x : {v : (BitVec Size60) | [ v = (lit "#x00000000000000f" (BitVec Size60))]}+bind 5 y : {v : (BitVec Size60) | [ v = (lit "#x0000000000000f0" (BitVec Size60))]}+bind 6 z : {v : (BitVec Size60) | [ v = (lit "#x000000000000000" (BitVec Size60))]}++constraint:+  env [4;5;6]+  lhs {v : (BitVec Size60) | [ v = bvand x y ] }+  rhs {v : (BitVec Size60) | [ v = z ] }+  id 1 tag []++bind 7 x : {v : (BitVec Size4) | [ v = (lit "#x5" (BitVec Size4))]}+bind 8 y : {v : (BitVec Size4) | [ v = (lit "#xb" (BitVec Size4))]}+bind 9 z : {v : (BitVec Size4) | [ v = (lit "#x1" (BitVec Size4))]}++constraint:+  env [7;8;9]+  lhs {v : (BitVec Size4) | [ v = bvxnor x y ] }+  rhs {v : (BitVec Size4) | [ v = z ] }+  id 2 tag []++bind 10 x : {v : (BitVec Size4) | [ v = (lit "#x4" (BitVec Size4))]}+bind 11 y : {v : (BitVec Size4) | [ v = (lit "#xb" (BitVec Size4))]}++constraint:+  env [10;11]+  lhs {v : (BitVec Size4) | [ v = bvnot x ] }+  rhs {v : (BitVec Size4) | [ v = y; y != bvneg x] }+  id 3 tag []++bind 12 x : {v : (BitVec Size4) | [ v = (lit "#x4" (BitVec Size4))]}+bind 13 y : {v : (BitVec Size4) | [ v = (lit "#xc" (BitVec Size4))]}++constraint:+  env [12;13]+  lhs {v : (BitVec Size4) | [ v = bvneg x ] }+  rhs {v : (BitVec Size4) | [ v = y; y != bvnot x ] }+  id 4 tag []++bind 14 x : {v : (BitVec Size4) | true }+bind 15 y : {v : (BitVec Size4) | true }++constraint:+  env [14;15]+  lhs {v : (BitVec Size4) | [ v = bvand x y ] }+  rhs {v : (BitVec Size4) | [ v = bvand y x ] }+  id 5 tag []++bind 16 x : {v : (BitVec Size4) | [ v = (lit "#b1010" (BitVec Size4))]}+bind 17 y : {v : (BitVec Size4) | [ v = (lit "#x1" (BitVec Size4))]}+bind 18 z : {v : (BitVec Size4) | [ v = (lit "#b0101" (BitVec Size4))]}++constraint:+  env [16;17;18]+  lhs {v : (BitVec Size4) | [ v = bvlshr x y ] }+  rhs {v : (BitVec Size4) | [ v = z ] }+  id 6 tag []++constraint:+  env [16;18]+  lhs {v : (BitVec Size4) | [ v = z ] }+  rhs {v : (BitVec Size4) | [ v = z; bvult z x ] }+  id 7 tag []++bind 19 z : {v : (BitVec Size8) | [ v = (lit "#b10100001" (BitVec Size8))]}++constraint:+  env [16;17;19]+  lhs {v : (BitVec Size8) | [ v = concat x y ] }+  rhs {v : (BitVec Size8) | [ v = z ] }+  id 8 tag []++constraint:+  env [19]+  lhs {v : (BitVec Size1) | [ v = bvcomp z z ] }+  rhs {v : (BitVec Size1) | [ v = (lit "#b1" (BitVec Size1)) ] }+  id 9 tag []+++

@@ -1,5 +1,4 @@-qualif Sz(v: Tree): (0 < thinginess v)-qualif Sz(v: Tree): (1 < 0)+fixpoint "--eliminate=some"  constant thinginess : func(0, [Tree; int]) @@ -16,6 +15,6 @@   rhs {v : Tree | 0 < thinginess v }   id 2 tag [] -wf: +wf:   env [ ]   reft { v: Tree | $k1 }

@@ -7,6 +7,7 @@ import qualified Control.Concurrent.STM as STM import qualified Data.Functor.Compose   as Functor import qualified Data.IntMap            as IntMap+import Control.Monad (when) import qualified Control.Monad.State    as State import Control.Monad.Trans.Class (lift) @@ -134,11 +135,14 @@         assertEqual "" True True       else do         createDirectoryIfMissing True $ takeDirectory log-        withFile log WriteMode $ \h -> do+        c <- withFile log WriteMode $ \h -> do           let cmd     = testCmd opts "fixpoint" dir file           (_,_,_,ph) <- createProcess $ (shell cmd) {std_out = UseHandle h, std_err = UseHandle h}-          c          <- waitForProcess ph-          assertEqual "Wrong exit code" code c+          waitForProcess ph+        when (code /= c) $+          readFile log >>= putStrLn+        assertEqual "Wrong exit code" code c+   where     test = dir </> file     log  = let (d,f) = splitFileName file in dir </> d </> ".liquid" </> f <.> "log"