liquid-fixpoint 0.9.6.3.2 → 0.9.6.3.3

raw patch · 22 files changed

+277/−113 lines, 22 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGES.md +8/−0
• liquid-fixpoint.cabal +2/−2
• src/Language/Fixpoint/Horn/Info.hs +1/−0
• src/Language/Fixpoint/Horn/Parse.hs +1/−0
• src/Language/Fixpoint/Horn/SMTParse.hs +13/−10
• src/Language/Fixpoint/Horn/Solve.hs +3/−3
• src/Language/Fixpoint/Horn/Transformations.hs +2/−1
• src/Language/Fixpoint/Horn/Types.hs +7/−4
• src/Language/Fixpoint/Parse.hs +1/−1
• src/Language/Fixpoint/Smt/Interface.hs +26/−41
• src/Language/Fixpoint/Smt/Theories.hs +23/−9
• src/Language/Fixpoint/Smt/Types.hs +1/−0
• src/Language/Fixpoint/Solver.hs +111/−5
• src/Language/Fixpoint/Solver/Extensionality.hs +5/−0
• src/Language/Fixpoint/Solver/Instantiate.hs +5/−5
• src/Language/Fixpoint/Solver/Monad.hs +1/−1
• src/Language/Fixpoint/Solver/PLE.hs +6/−5
• src/Language/Fixpoint/Solver/Sanitize.hs +16/−10
• src/Language/Fixpoint/SortCheck.hs +22/−14
• src/Language/Fixpoint/Types/Constraints.hs +6/−2
• src/Language/Fixpoint/Types/Sorts.hs +11/−0
• src/Language/Fixpoint/Types/Theories.hs +6/−0

@@ -2,6 +2,14 @@  ## NEXT +## 0.9.6.3.3 (2025-03-22)++- Add support for GHC HEAD (9.13) [#745](https://github.com/ucsd-progsys/liquid-fixpoint/pull/745).+- Expose SMTLIB define-fun to users of liquid-fixpoint [#744](https://github.com/ucsd-progsys/liquid-fixpoint/pull/744).+- Check that expressions in refinements are Bool-sorted [#743](https://github.com/ucsd-progsys/liquid-fixpoint/pull/743).+- Fix crashes when a datatype is declared with a `Map_t` field [#738](https://github.com/ucsd-progsys/liquid-fixpoint/issues/738).+- Simplify expressions in fqout files [#741](https://github.com/ucsd-progsys/liquid-fixpoint/pull/741).+ ## 0.9.6.3.2 (2025-03-06)  - Expose relatedSymbols from EnvironmentReduction. Needed for improving error

@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               liquid-fixpoint-version:            0.9.6.3.2+version:            0.9.6.3.3 synopsis:           Predicate Abstraction-based Horn-Clause/Implication Constraint Solver description:   This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint@@ -25,7 +25,7 @@ license:            BSD-3-Clause license-file:       LICENSE build-type:         Simple-tested-with:        GHC == 9.10.1, GHC == 9.8.2, GHC == 9.6.5+tested-with:        GHC == 9.12.2, GHC == 9.10.1, GHC == 9.8.2 extra-source-files: tests/neg/*.fq                     tests/pos/*.fq                     unix/Language/Fixpoint/Utils/*.hs

@@ -30,6 +30,7 @@   , F.ae        = axEnv cfg q cs   , F.ddecls    = H.qData q   , F.hoInfo    = F.cfgHoInfo cfg+  , F.defns     = H.qDefs q   }   where     be0         = F.emptyBindEnv

@@ -36,6 +36,7 @@   , H.qData  =            [ dd    | HDat dd <- things ]   , H.qOpts  =            [ o     | HOpt o  <- things ]   , H.qNums  =            [ n     | HNum n  <- things ]+  , H.qDefs  =            []   }  -- | A @HThing@ describes the kinds of things we may see, in no particular order

@@ -126,16 +126,17 @@  mkQuery :: [HThing a] -> H.Query a mkQuery things = H.Query-  { H.qQuals =            [ q     | HQual q  <- things ]-  , H.qVars  =            [ k     | HVar  k  <- things ]-  , H.qCstr  = H.CAnd     [ c     | HCstr c  <- things ]-  , H.qCon   = M.fromList [ (x,t) | HCon x t <- things ]-  , H.qDis   = M.fromList [ (x,t) | HDis x t <- things ]-  , H.qEqns  =            [ e     | HDef e   <- things ]-  , H.qMats  =            [ m     | HMat m   <- things ]-  , H.qData  =            [ dd    | HDat dd  <- things ]-  , H.qOpts  =            [ o     | HOpt o   <- things ]-  , H.qNums  =            [ s     | HNum s   <- things ]+  { H.qQuals =              [ q     | HQual q  <- things ]+  , H.qVars  =              [ k     | HVar  k  <- things ]+  , H.qCstr  = H.CAnd       [ c     | HCstr c  <- things ]+  , H.qCon   = M.fromList   [ (x,t) | HCon x t <- things ]+  , H.qDis   = M.fromList   [ (x,t) | HDis x t <- things ]+  , H.qEqns  =              [ e     | HDef e   <- things ]+  , H.qDefs  =              [ e     | HDfn e   <- things ]+  , H.qMats  =              [ m     | HMat m   <- things ]+  , H.qData  =              [ dd    | HDat dd  <- things ]+  , H.qOpts  =              [ o     | HOpt o   <- things ]+  , H.qNums  =              [ s     | HNum s   <- things ]   }  -- | A @HThing@ describes the kinds of things we may see, in no particular order@@ -150,6 +151,7 @@   | HCon  F.Symbol F.Sort   | HDis  F.Symbol F.Sort   | HDef  F.Equation+  | HDfn  F.Equation   | HMat  F.Rewrite   | HDat !F.DataDecl   | HOpt !String@@ -166,6 +168,7 @@         <|> HCon  <$> (reserved "constant"   *> symbolP) <*> sortP         <|> HDis  <$> (reserved "distinct"   *> symbolP) <*> sortP         <|> HDef  <$> (reserved "define"     *> defineP)+        <|> HDfn  <$> (reserved "define_fun" *> defineP)         <|> HMat  <$> (reserved "match"      *> matchP)         <|> HDat  <$> (reserved "datatype"   *> dataDeclP)         <|> HNum  <$> (reserved "numeric"    *> numericDeclP)

@@ -34,9 +34,9 @@   q <- parseQuery baseCfg    -- If you want to set --eliminate=none, you better make it a pragma-  cfgElim <- if F.eliminate baseCfg == F.None-           then pure (baseCfg { F.eliminate =  F.Some })-           else pure baseCfg+  let cfgElim = if F.eliminate baseCfg == F.None+                  then baseCfg { F.eliminate =  F.Some }+                  else baseCfg    cfgPragmas <- F.withPragmas cfgElim (H.qOpts q) 

@@ -647,7 +647,8 @@       Nothing -> []       Just vertex -> nub $ filter (/= F.EVar x) $ mconcat [es | ((_, es), _, _) <- vf <$> DG.reachable eGraph vertex] -    argsAndPrims = args `S.union` S.fromList (map fst $ F.toListSEnv $ F.theorySymbols (F.solver cfg) []) `S.union`measures+    argsAndPrims = args `S.union` S.fromList (fst <$> F.toListSEnv thySyms) `S.union`measures+    thySyms = F.theorySymbols (F.solver cfg)      isWellFormed :: F.Expr -> Bool     isWellFormed e = S.fromList (F.syms e) `S.isSubsetOf` argsAndPrims

@@ -196,9 +196,10 @@   { qQuals :: ![F.Qualifier]             -- ^ qualifiers over which to solve cstrs   , qVars  :: ![Var a]                   -- ^ kvars, with parameter-sorts   , qCstr  :: !(Cstr a)                  -- ^ list of constraints-  , qCon   :: M.HashMap F.Symbol F.Sort  -- ^ list of constants (uninterpreted functions)+  , qCon   :: M.HashMap F.Symbol F.Sort  -- ^ list of constants (un/interpreted functions)   , qDis   :: M.HashMap F.Symbol F.Sort  -- ^ list of *distinct* constants (uninterpreted functions)   , qEqns  :: ![F.Equation]              -- ^ list of equations+  , qDefs  :: ![F.Equation]              -- ^ list of equations to be sent to SMT as define-fun   , qMats  :: ![F.Rewrite]               -- ^ list of match-es   , qData  :: ![F.DataDecl]              -- ^ list of data-declarations   , qOpts  :: ![String]                  -- ^ list of fixpoint options@@ -340,7 +341,8 @@     , P.vcat   (toHornSMT <$> qQuals q)     , P.vcat   (toHornSMT <$> qVars q)     , P.vcat   [toHornCon x t | (x, t) <- M.toList (qCon q)]-    , P.vcat   (toHornSMT <$> qEqns q)+    , P.vcat   (eqnToHornSMT "define"     <$> qEqns q)+    , P.vcat   (eqnToHornSMT "define_fun" <$> qDefs q)     , P.vcat   (toHornSMT <$> qData q)     , P.vcat   (toHornSMT <$> qMats q)     , P.parens (P.vcat ["constraint", P.nest 1 (toHornSMT (qCstr q))])@@ -371,8 +373,9 @@ toHornAnd :: (a -> P.Doc) -> [a] -> P.Doc toHornAnd f xs = P.parens (P.vcat ("and" : (P.nest 1 . f <$> xs))) -instance ToHornSMT F.Equation where-  toHornSMT (F.Equ f xs e s _) = P.parens ("define" P.<+> F.pprint f P.<+> toHornSMT xs P.<+> toHornSMT s P.<+> toHornSMT e)+eqnToHornSMT :: P.Doc -> F.Equation -> P.Doc+eqnToHornSMT keyword (F.Equ f xs e s _) = P.parens (keyword P.<+> F.pprint f P.<+> toHornSMT xs P.<+> toHornSMT s P.<+> toHornSMT e)+  instance ToHornSMT F.DataDecl where   toHornSMT (F.DDecl tc n ctors) =

@@ -1449,7 +1449,7 @@     <|> (reserved "False" >> return False)  defsFInfo :: [Def a] -> FInfo a-defsFInfo defs = {- SCC "defsFI" -} Types.FI cm ws bs ebs lts dts kts qs binfo adts mempty mempty ae lrws+defsFInfo defs = {- SCC "defsFI" -} Types.FI cm ws bs ebs lts dts kts qs binfo adts mempty mempty ae lrws mempty   where     cm         = Misc.safeFromList                    "defs-cm"        [(cid c, c)         | Cst c       <- defs]

@@ -7,6 +7,8 @@ {-# LANGUAGE ScopedTypeVariables       #-} {-# LANGUAGE PatternGuards             #-} {-# LANGUAGE DoAndIfThenElse           #-}+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}+{-# HLINT ignore "Use isNothing" #-}  -- | This module contains an SMTLIB2 interface for --   1. checking the validity, and,@@ -252,20 +254,19 @@     where        smtFile = extFileName Smt2 f -makeContextWithSEnv :: Config -> FilePath -> SymEnv -> IO Context-makeContextWithSEnv cfg f env = do+makeContextWithSEnv :: Config -> FilePath -> SymEnv -> [Equation] -> IO Context+makeContextWithSEnv cfg f env defns = do   ctx     <- makeContext cfg f-  let ctx' = ctx {ctxSymEnv = env}+  let ctx' = ctx {ctxSymEnv = env, ctxDefines = defns}   declare ctx'   return ctx'-  -- where msg = "makeContextWithSEnv" ++ show env  makeContextNoLog :: Config -> IO Context-makeContextNoLog cfg-  = do me  <- makeContext' cfg Nothing-       pre <- smtPreamble cfg (solver cfg) me-       mapM_ (SMTLIB.Backends.command_ (ctxSolver me)) pre-       return me+makeContextNoLog cfg = do+  me  <- makeContext' cfg Nothing+  pre <- smtPreamble cfg (solver cfg) me+  mapM_ (SMTLIB.Backends.command_ (ctxSolver me)) pre+  return me  makeProcess   :: Maybe Handle@@ -302,11 +303,11 @@          Cvc4    -> makeProcess ctxLog $                       Process.defaultConfig                              { Process.exe = "cvc4"-                             , Process.args = ["--incremental", "-L", "smtlib2"] }+                             , Process.args = ["-L", "smtlib2"] }          Cvc5    -> makeProcess ctxLog $                       Process.defaultConfig                              { Process.exe = "cvc5"-                             , Process.args = ["--incremental", "-L", "smtlib2"] }+                             , Process.args = ["-L", "smtlib2"] }        solver <- SMTLIB.Backends.initSolver SMTLIB.Backends.Queuing backend        loud <- isLoud        return Ctx { ctxSolver    = solver@@ -315,6 +316,7 @@                   , ctxLog       = ctxLog                   , ctxVerbose   = loud                   , ctxSymEnv    = mempty+                  , ctxDefines   = mempty                   }  -- | Close file handles and release the solver backend's resources.@@ -331,7 +333,7 @@   | s == Z3 || s == Z3mem     = do v <- getZ3Version me          checkValidStringFlag Z3 v cfg-         return $ z3_options ++ makeMbqi cfg ++ makeTimeout cfg ++ Thy.preamble cfg Z3+         return $ makeMbqi cfg ++ makeTimeout cfg ++ Thy.preamble cfg Z3   | otherwise     = checkValidStringFlag s [] cfg >> return (Thy.preamble cfg s) @@ -404,10 +406,13 @@ smtAssert :: Context -> Expr -> IO () smtAssert me p = interact' me (Assert Nothing p) +smtDefineEqn :: Context -> Equation -> IO ()+smtDefineEqn me Equ {..} = smtDefineFunc me eqName eqArgs eqSort eqBody+ smtDefineFunc :: Context -> Symbol -> [(Symbol, F.Sort)] -> F.Sort -> Expr -> IO () smtDefineFunc me name symList rsort e =   let env = seData (ctxSymEnv me)-   in interact' me $+  in interact' me $         DefineFunc           name           (map (sortSmtSort False env <$>) symList)@@ -456,13 +461,7 @@   | gradual cfg = [""]   | otherwise   = ["\n(set-option :smt.mbqi false)"] -z3_options :: [Builder]-z3_options-  = [ "(set-option :auto-config false)"-    , "(set-option :model true)" ] -- -------------------------------------------------------------------------------- declare :: Context -> IO () --------------------------------------------------------------------------------@@ -471,6 +470,7 @@   forM_ thyXTs $ uncurry $ smtDecl     me   forM_ qryXTs $ uncurry $ smtDecl     me   forM_ ats    $ uncurry $ smtFuncDecl me+  forM_ defs   $           smtDefineEqn me   forM_ ess    $           smtDistinct me   forM_ axs    $           smtAssert   me   where@@ -479,12 +479,13 @@     lts        = F.toListSEnv . F.seLits $ env     ess        = distinctLiterals  lts     axs        = Thy.axiomLiterals lts-    thyXTs     =                    filter (isKind 1) xts-    qryXTs     = fmap tx <$> filter (isKind 2) xts-    isKind n   = (n ==)  . symKind env . fst-    xts        = {- tracepp "symbolSorts" $ -} symbolSorts (F.seSort env)+    thyXTs     =             [ (x, t) | (x, t) <- xts, symKind env x == Just F.Uninterp ]+    qryXTs     = fmap tx <$> [ (x, t) | (x, t) <- xts, symKind env x == Nothing ]+    -- isKind n   = (n ==)  . symKind env . fst+    xts        = symbolSorts (F.seSort env)     tx         = elaborate (ElabParam (ctxElabF me) "declare" env)     ats        = funcSortVars env+    defs       = ctxDefines me  symbolSorts :: F.SEnv F.Sort -> [(F.Symbol, F.Sort)] symbolSorts env = [(x, tx t) | (x, t) <- F.toListSEnv env ]@@ -507,24 +508,8 @@     lamSort (s,t) = ([s, t], F.SInt)     argSort (s,_) = ([]    , s) --- | 'symKind' returns {0, 1, 2} where:---   0 = Theory-Definition,---   1 = Theory-Declaration,---   2 = Query-Binder--symKind :: F.SymEnv -> F.Symbol -> Int-symKind env x = case F.tsInterp <$> F.symEnvTheory x env of-                  Just F.Theory   -> 0-                  Just F.Ctor     -> 0-                  Just F.Test     -> 0-                  Just F.Field    -> 0-                  Just F.Uninterp -> 1-                  Nothing         -> 2-              -- Just t  -> if tsInterp t then 0 else 1----- assumes :: [F.Expr] -> SolveM ()--- assumes es = withContext $ \me -> forM_  es $ smtAssert me+symKind :: F.SymEnv -> F.Symbol -> Maybe Sem+symKind env x = F.tsInterp <$> F.symEnvTheory x env  -- | `distinctLiterals` is used solely to determine the set of literals --   (of each sort) that are *disequal* to each other, e.g. EQ, LT, GT,

@@ -8,6 +8,7 @@  {-# OPTIONS_GHC -Wno-orphans           #-} {-# LANGUAGE TupleSections #-}+{-# LANGUAGE InstanceSigs #-}  module Language.Fixpoint.Smt.Theories      (@@ -237,7 +238,7 @@   = bFun f [("x", "Int"), ("y", "Int")] "Int" (key2 (fromText op) "x" "y")  onlyLinearArith :: Config -> Bool-onlyLinearArith cfg = linear cfg || solver cfg `notElem` [Z3, Cvc5]+onlyLinearArith cfg = linear cfg || solver cfg `notElem` [Z3, Z3mem, Cvc5]  preamble :: Config -> SMTSolver -> [Builder] preamble cfg s = snd <$> filter (matchesCondition s . fst) (solverPreamble cfg)@@ -249,8 +250,12 @@  solverPreamble :: Config -> [Preamble] solverPreamble cfg-  =  [(SOnly [Cvc4], "(set-logic ALL_SUPPORTED)")]-  ++ [(SOnly [Cvc5], "(set-logic ALL)")]+  =  [ (SOnly [Z3, Z3mem],  "(set-option :auto-config false)")+     , (SOnly [Z3, Z3mem],  "(set-option :model true)")+     , (SOnly [Cvc4],       "(set-logic ALL_SUPPORTED)")+     , (SOnly [Cvc5],       "(set-logic ALL)")+     , (SOnly [Cvc4, Cvc5], "(set-option :incremental true)")+     ]   ++ boolPreamble cfg   ++ arithPreamble cfg   ++ stringPreamble cfg@@ -375,13 +380,22 @@ --   symbols, and `interpSEnv` is for interpreted symbols. -------------------------------------------------------------------------------- --- | `theorySymbols` contains the list of ALL SMT symbols with interpretations,---   i.e. which are given via `define-fun` (as opposed to `declare-fun`)-theorySymbols :: SMTSolver -> [DataDecl] -> SEnv TheorySymbol -- M.HashMap Symbol TheorySymbol-theorySymbols cfg ds = fromListSEnv $  -- SHIFTLAM uninterpSymbols-                                  interpSymbols cfg-                               ++ concatMap dataDeclSymbols ds+instance TheorySymbols SMTSolver where+  theorySymbols :: SMTSolver -> SEnv TheorySymbol+  theorySymbols = fromListSEnv . interpSymbols +instance TheorySymbols [DataDecl] where+  theorySymbols :: [DataDecl] -> SEnv TheorySymbol+  theorySymbols = fromListSEnv . concatMap dataDeclSymbols++instance TheorySymbols [Equation] where+  theorySymbols = fromListSEnv . fmap equationSymbol++equationSymbol :: Equation -> (Symbol, TheorySymbol)+equationSymbol eq = (sym, Thy sym (symbolRaw sym) sort Defined)+  where+    sym  = eqName eq+    sort = mkFFunc 0 ((snd <$> eqArgs eq) <> [eqSort eq])  -------------------------------------------------------------------------------- interpSymbols :: SMTSolver -> [(Symbol, TheorySymbol)]

@@ -102,6 +102,7 @@   , ctxLog     :: !(Maybe Handle)   , ctxVerbose :: !Bool   , ctxSymEnv  :: !SymEnv+  , ctxDefines :: ![Equation]   }  --------------------------------------------------------------------------------

@@ -34,7 +34,7 @@ import           System.Exit                        (ExitCode (..)) import           System.Console.CmdArgs.Verbosity   (whenNormal, whenLoud) import           Text.PrettyPrint.HughesPJ          (render)-import           Control.Monad                      (when)+import           Control.Monad                      (mplus, when) import           Control.Exception                  (catch) import           Language.Fixpoint.Solver.EnvironmentReduction   (reduceEnvironments, simplifyBindings)@@ -59,7 +59,7 @@ import           Language.Fixpoint.Solver.Instantiate (instantiate) import           Control.DeepSeq import qualified Data.ByteString as B-import Data.Maybe (catMaybes)+import Data.Maybe (catMaybes, mapMaybe)  --------------------------------------------------------------------------- -- | Solve an .fq file ----------------------------------------------------@@ -271,7 +271,8 @@  solveNative' !cfg !fi0 = do   si6 <- simplifyFInfo cfg fi0-  res <- {- SCC "Sol.solve" -} Sol.solve cfg $!! si6+  res0 <- {- SCC "Sol.solve" -} Sol.solve cfg $!! si6+  let res = simplifyResult res0   -- rnf soln `seq` donePhase Loud "Solve2"   --let stat = resStatus res   -- saveSolution cfg res@@ -305,8 +306,10 @@     , "Solution:"     , showpp (resSolution  res)     ] ++-    ( if gradual cfg then ["", "", showpp (gresSolution res)]-      else []+    ( if gradual cfg then+        ["", "", showpp $ gresSolution res]+      else+        []     ) ++     [ ""     , ""@@ -314,3 +317,106 @@     , ""     , showpp (HashMap.map unElab $ resNonCutsSolution res)     ]++simplifyResult :: Result a -> Result a+simplifyResult res =+    res+      { resSolution = HashMap.map simplifyKVar (resSolution res)+      , resNonCutsSolution = HashMap.map simplifyKVar (resNonCutsSolution res)+      }++-- | Simplifies existential expressions with unused or inconsequential bindings.+--+-- For instance, in the following example, "x" is not used at all.+--+-- > simplifyKVar "exists x y. y == z && y == C" == "exists y. y == z && y == C"+--+-- And in the following example, @x@ is used but in a way that doesn't+-- contribute any useful knowledge.+--+-- > simplifyKVar "exists x y. x == C && y == z && y == C"+-- >   ==+-- > "exists y. y == z && y == C"+--+-- We require that relevant variables occur more than once, or that+-- they occur in some other place than as an argument to @==@.+--+simplifyKVar :: Expr -> Expr+simplifyKVar (POr es) = POr $ map simplifyKVar es+simplifyKVar (PExist bs e@(PAnd es)) =+    let fvs = L.group $ L.sort $ collectFreeVarOccurrences e+        esv = map (isUniqueEq fvs) es+        removed = mapMaybe fst esv+        needed = map head fvs L.\\ removed+        bs' = filter ((`elem` needed) . fst) bs+     in+        PExist bs' $ PAnd $ [ei | (Nothing, ei) <- esv]+  where+    -- | Determine if the expression is an equality that sets the value of+    -- a variable that doesn't occur elsewhere.+    --+    -- In @isUniqueEq fvs e@, @fvs@ contains the occurrences of the free+    -- variables, so we can infer if there is more than one occurrence+    -- of a given free variable, and @e@ is the equality to analyze.+    --+    -- Yields @(Just v, e)@ if @v@ doesn't occur elsewhere, and @e@ has+    -- the form @v == e'@.+    isUniqueEq :: [[Symbol]] -> Expr -> (Maybe Symbol, Expr)+    isUniqueEq fvs er = case unElab er of+      PAtom brel e0 e1+        | isEqRel brel ->+          let m = isVarToDrop fvs e0 `mplus` isVarToDrop fvs e1+           in (m, er)+      _ ->+        (Nothing, er)++    -- | Tells if the binary relation is an equality.+    isEqRel Eq = True+    isEqRel Ueq = True+    isEqRel _ = False++    -- | @isVarToDrop fvs s@ yields @Just s@ if the variable @s@ doesn't occur+    -- elsewhere according to @fvs@.+    --+    -- > isVarToDrop fvs (cast_as_int s) == isVarToDrop fvs s+    --+    isVarToDrop fvs (EApp (EVar "cast_as_int") ei) = isVarToDrop fvs ei+    isVarToDrop fvs (EVar s)+      | elem [s] fvs = Just s+    isVarToDrop _fvs _ = Nothing++simplifyKVar e = e++-- | Produces the free variables of an expressions as many times as they occur.+--+-- There are no guarantees on the order in which the variables are produced. For+-- instance,+--+-- > collectFreeVarOccurrences "z (y x) (y x)" == ["z", "y", "x", "y", "x"]+--+collectFreeVarOccurrences :: Expr -> [Symbol]+collectFreeVarOccurrences = go []+  where+    go acc e0 = case e0 of+      ESym _ -> acc+      ECon _ -> acc+      EVar v -> v : acc+      PKVar _ (Su m) -> foldr (flip go) acc $ HashMap.elems m+      PGrad _ (Su m) _ e -> foldr (flip go) acc $ e : HashMap.elems m+      ENeg e -> go acc e+      PNot p -> go acc p+      ECst e _t -> go acc e+      PAll _xts p -> go acc p+      ELam (b, _) e -> go acc e L.\\ [b]+      ECoerc _a _t e -> go acc e+      PExist _xts p -> go acc p+      ETApp e _s -> go acc e+      ETAbs e _s -> go acc e+      EApp g e -> go (go acc e) g+      EBin _o e1 e2 -> go (go acc e2) e1+      PImp p1 p2 -> go (go acc p2) p1+      PIff p1 p2 -> go (go acc p2) p1+      PAtom _r e1 e2 -> go (go acc e2) e1+      EIte p e1 e2 -> go (go (go acc e2) e1) p+      PAnd ps -> foldr (flip go) acc ps+      POr ps -> foldr (flip go) acc ps

@@ -214,6 +214,11 @@             DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.Prim.(,)$1")) (FVar 0)           , DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.Prim.(,)$2")) (FVar 1)           ]+#elif MIN_TOOL_VERSION_ghc(9,13,0)+    ct = DCtor (dummyLoc (symbol "GHC.Internal.Tuple.(,)")) [+            DField (dummyLoc (symbol "lqdc$select$GHC.Internal.Tuple.(,)$1")) (FVar 0)+          , DField (dummyLoc (symbol "lqdc$select$GHC.Internal.Tuple.(,)$2")) (FVar 1)+          ] #else     ct = DCtor (dummyLoc (symbol "GHC.Tuple.(,)")) [             DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.(,)$1")) (FVar 0)

@@ -82,7 +82,7 @@                       ,  maybe True (i `L.elem`) subcIds ]     let t  = mkCTrie cs                                               -- 1. BUILD the Trie     res   <- withProgress (1 + length cs) $-               withCtx cfg file sEnv (pleTrie t . instEnv cfg info cs)  -- 2. TRAVERSE Trie to compute InstRes+               withCtx cfg file sEnv (defns info) (pleTrie t . instEnv cfg info cs)  -- 2. TRAVERSE Trie to compute InstRes     return $ resSInfo cfg sEnv info res                                 -- 3. STRENGTHEN SInfo using InstRes   where     file   = srcFile cfg ++ ".evals"@@ -296,7 +296,7 @@ -- | "Old" GLOBAL PLE -------------------------------------------------------------------------------- instantiate' :: (Loc a) => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)-instantiate' cfg info subcIds = sInfo cfg env info <$> withCtx cfg file env act+instantiate' cfg info subcIds = sInfo cfg env info <$> withCtx cfg file env (defns info) act   where     act ctx         = forM cstrs $ \(i, c) ->                         ((i,srcSpan c),) . mytracepp  ("INSTANTIATE i = " ++ show i) <$> instSimpC cfg ctx (bs info) aenv i c@@ -800,9 +800,9 @@ -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -withCtx :: Config -> FilePath -> SymEnv -> (SMT.Context -> IO a) -> IO a-withCtx cfg file env k = do-  ctx <- SMT.makeContextWithSEnv cfg file env+withCtx :: Config -> FilePath -> SymEnv -> [Equation] -> (SMT.Context -> IO a) -> IO a+withCtx cfg file env defns k = do+  ctx <- SMT.makeContextWithSEnv cfg file env defns   _   <- SMT.smtPush ctx   res <- k ctx   SMT.cleanupContext ctx

@@ -84,7 +84,7 @@     s0 ctx   = SS ctx be (stats0 fi)     act'     = assumesAxioms (F.asserts fi) >> act     release  = cleanupContext-    acquire  = makeContextWithSEnv cfg file initEnv+    acquire  = makeContextWithSEnv cfg file initEnv (F.defns fi)     initEnv  = symbolEnv cfg fi     be       = F.bs fi     file     = C.srcFile cfg

@@ -80,7 +80,7 @@                (cm info)     let t  = mkCTrie (M.toList cs)                                          -- 1. BUILD the Trie     res   <- withRESTSolver $ \solver -> withProgress (1 + M.size cs) $-               withCtx cfg file sEnv $ \ctx -> do+               withCtx cfg file sEnv (defns fi') $ \ctx -> do                   env <- instEnv cfg info cs solver ctx                   pleTrie t env                                             -- 2. TRAVERSE Trie to compute InstRes     savePLEEqualities cfg info sEnv res@@ -107,6 +107,7 @@   where     equalitiesPerConstraint (cid, c) =       (cid, L.sort [ e | i <- elemsIBindEnv (senv c), Just e <- [M.lookup i res] ])+    elabParam = ElabParam (solverFlags $ solver cfg) "savePLEEqualities" sEnv     renderConstraintRewrite (cid, eqs) =       "constraint id" <+> text (show cid ++ ":")       $+$ nest 2@@ -114,7 +115,7 @@             map (toFix . unElab) $ Set.toList $ Set.fromList $             -- call elabExpr to try to bring equations that are missing             -- some casts into a fully annotated form for comparison-            map (elabExpr (ElabParam (solverFlags $ solver cfg) "savePLEEqualities" sEnv)) $+            map (elabExpr elabParam (Just boolSort)) $             concatMap conjuncts eqs            )       $+$ ""@@ -1334,9 +1335,9 @@ -------------------------------------------------------------------------------- -------------------------------------------------------------------------------- -withCtx :: Config -> FilePath -> SymEnv -> (SMT.Context -> IO a) -> IO a-withCtx cfg file env k = do-  ctx <- SMT.makeContextWithSEnv cfg file env+withCtx :: Config -> FilePath -> SymEnv -> [Equation] -> (SMT.Context -> IO a) -> IO a+withCtx cfg file env defns k = do+  ctx <- SMT.makeContextWithSEnv cfg file env defns   _   <- SMT.smtPush ctx   res <- k ctx   SMT.cleanupContext ctx

@@ -34,12 +34,12 @@ import qualified Data.Text                                         as T import           Data.Maybe          (isNothing, mapMaybe, fromMaybe) import           Control.Monad       ((>=>))-import           Text.PrettyPrint.HughesPJ+import           Text.PrettyPrint.HughesPJ hiding ((<>))  type SanitizeM a = Either E.Error a  ---------------------------------------------------------------------------------sanitize :: Config -> F.SInfo a -> SanitizeM (F.SInfo a)+sanitize :: (Show a) => Config -> F.SInfo a -> SanitizeM (F.SInfo a) -------------------------------------------------------------------------------- sanitize cfg =       banIrregularData          >=> Misc.fM dropFuncSortedShadowedBinders@@ -152,14 +152,20 @@       splitApp (fvar, arg:args)     fapp' e = pure (e, []) -    theorySymbols = F.notracepp "theorySymbols" $ Thy.theorySymbols (Cfg.solver cfg) $ F.ddecls si+    thySyms = theoryEnv cfg si      splitApp (e, es)-      | isNothing $ F.notracepp ("isSmt2App? " ++ showpp e) $ Thy.isSmt2App theorySymbols $ stripCasts e+      | isNothing $ F.notracepp ("isSmt2App? " ++ showpp e) $ Thy.isSmt2App thySyms (stripCasts e)       = pure (e,es)       | otherwise       = Nothing +theoryEnv :: Config -> F.GInfo c a -> F.SEnv F.TheorySymbol+theoryEnv cfg si+  =  Thy.theorySymbols (Cfg.solver cfg)+  <> Thy.theorySymbols (F.defns si)+  <> Thy.theorySymbols (F.ddecls si)+ -------------------------------------------------------------------------------- -- | See issue liquid-fixpoint issue #230. This checks that whenever we have, --      G1        |- K.su1@@ -317,8 +323,9 @@ known cfg fi  = \x -> F.memberSEnv x lits || F.memberSEnv x prims   where     lits  = F.gLits fi-    prims = Thy.theorySymbols (Cfg.solver cfg) . F.ddecls $ fi+    prims = theoryEnv cfg fi + cNoFreeVars :: F.SInfo a -> (F.Symbol -> Bool) -> F.SimpC a -> Maybe [F.Symbol] cNoFreeVars fi knownSym c = if S.null fv then Nothing else Just (S.toList fv)   where@@ -387,15 +394,15 @@ --   it makes it hard to actually find the fundefs within (breaking PLE.) -------------------------------------------------------------------------------- symbolEnv :: Config -> F.SInfo a -> F.SymEnv-symbolEnv cfg si = F.symEnv sEnv tEnv ds lits (ts ++ ts')+symbolEnv cfg si = F.symEnv sEnv thyEnv ds lits (ts ++ ts')   where     ts'          = applySorts ae'     ae'          = elaborate (ElabParam ef (F.atLoc E.dummySpan "symbolEnv") env0) (F.ae si)-    env0         = F.symEnv sEnv tEnv ds lits ts-    tEnv         = Thy.theorySymbols slv ds+    env0         = F.symEnv sEnv thyEnv ds lits ts+    thyEnv       = theoryEnv cfg si     ds           = F.ddecls si     ts           = Misc.setNub (applySorts si ++ [t | (_, t) <- F.toListSEnv sEnv])-    sEnv         = F.coerceSortEnv ef $ (F.tsSort <$> tEnv) `mappend` F.fromListSEnv xts+    sEnv         = F.coerceSortEnv ef $ (F.tsSort <$> thyEnv) `mappend` F.fromListSEnv xts     slv          = Cfg.solver cfg     ef           = solverFlags slv     xts          = symbolSorts cfg si ++ alits@@ -488,7 +495,6 @@     ws'        = deleteWfCBinds drops <$> F.ws si     (_,drops)  = filterBindEnv keepF   $  F.bs si     keepF      = conjKF [nonConstantF si, nonFunctionF si, _nonDerivedLH]-    -- drops   = F.tracepp "sanitizeWfC: dropping" $ L.sort drops'  conjKF :: [KeepBindF] -> KeepBindF conjKF fs x t = and [f x t | f <- fs]

@@ -141,6 +141,7 @@     { F.cm      = elaborate ep <$> F.cm      si     , F.bs      = elaborate ep  $  F.bs      si     , F.asserts = elaborate ep <$> F.asserts si+    , F.ddecls  = coerceDataDecl (epFlags ep) <$> F.ddecls si     }  @@ -178,13 +179,16 @@       ep' = ep { epEnv = insertsSymEnv (epEnv ep) (eqArgs eq) }  instance Elaborate Expr where-  elaborate (ElabParam ef msg env) =-    elabNumeric . elabApply env' . elabExpr (ElabParam ef msg env') . elabFMap . (if Cfg.elabSetBag ef then elabFSetBagZ3 else id)+  elaborate p e = elaborateExpr p e Nothing++elaborateExpr :: ElabParam -> Expr -> Maybe Sort -> Expr+elaborateExpr (ElabParam ef msg env) e t =+    elabNumeric . elabApply env' . elabExpr (ElabParam ef msg env') t . elabFMap . (if Cfg.elabSetBag ef then elabFSetBagZ3 else id) $ e       where         env' = coerceEnv ef env  skipElabExpr :: ElabParam -> Expr -> Expr-skipElabExpr ep e = case elabExprE ep e of+skipElabExpr ep e = case elabExprE ep Nothing e of   Left _   -> e   Right e' -> elabNumeric . elabApply (epEnv ep) $ e' @@ -211,7 +215,7 @@ instance Elaborate SortedReft where   elaborate ep (RR s (Reft (v, e))) = RR s (Reft (v, e'))     where-      e'   = elaborate ep' e+      e'   = elaborateExpr ep' e (Just boolSort) -- check that a SortedReft is in fact a bool       ep' = ep { epEnv = insertSymEnv v s (epEnv ep) }  instance (Loc a) => Elaborate (BindEnv a) where@@ -307,21 +311,28 @@ -------------------------------------------------------------------------------- -- | 'elabExpr' adds "casts" to decorate polymorphic instantiation sites. ---------------------------------------------------------------------------------elabExpr :: ElabParam -> Expr -> Expr-elabExpr ep e = case elabExprE ep e of+elabExpr :: ElabParam -> Maybe Sort -> Expr ->  Expr+elabExpr ep t e = case elabExprE ep t e of   Left ex  -> die ex   Right e' -> F.notracepp ("elabExp " ++ showpp e) e' -elabExprE :: ElabParam -> Expr -> Either Error Expr-elabExprE (ElabParam ef msg env) e =+validateSort :: Sort -> Maybe Sort -> CheckM ()+validateSort t (Just t')+  | t == t'            = return ()+  | otherwise          = throwErrorAt $ printf "unexpected sort: got `%s` but expected `%s`" (showpp t) (showpp t')+validateSort _ Nothing = return ()++elabExprE :: ElabParam -> Maybe Sort -> Expr -> Either Error Expr+elabExprE (ElabParam ef msg env) t e =   case runCM0 (srcSpan msg) (Just ef) $ do-    (!e', _) <- elab (env, envLookup) e+    (!e', eSort) <- elab (env, envLookup) e+    validateSort eSort t     finalThetaRef <- asks chTVSubst     finalTheta <- liftIO $ readIORef finalThetaRef     return (applyExpr finalTheta e') of     Left (ChError f') ->       let e' = f' ()-       in Left $ err (srcSpan e') (d (val e'))+      in Left $ err (srcSpan e') (d (val e'))     Right s  -> Right s   where     sEnv = seSort env@@ -334,6 +345,7 @@                 , nest 4 (pprint $ subEnv sEnv e)                 ] + -------------------------------------------------------------------------------- -- | 'elabApply' replaces all direct function calls indirect calls via `apply` --------------------------------------------------------------------------------@@ -431,9 +443,6 @@ -------------------------------------------------------------------------------- mkSearchEnv env x = lookupSEnvWithDistance x env --- withError :: CheckM a -> ChError -> CheckM a--- act `withError` e' = act `catchError` (\e -> throwError (atLoc e (val e ++ "\n  because\n" ++ val e')))- withError :: HasCallStack => CheckM a -> String -> CheckM a act `withError` msg = do   r <- ask@@ -730,7 +739,6 @@ isUndef s = case bkAbs s of   (is, FVar j) -> j `elem` is   _            -> False-  elabAddEnv :: Eq a => (t, a -> SESearch b) -> [(a, b)] -> (t, a -> SESearch b) elabAddEnv (g, f) bs = (g, addEnv f bs)

@@ -697,7 +697,8 @@        , ae       = axe        , ddecls   = adts        , ebinds   = ebs-       , lrws = mempty+       , lrws     = mempty+       , defns    = mempty        }   where     --TODO handle duplicates gracefully instead (merge envs by intersect?)@@ -744,6 +745,7 @@   , asserts  :: ![Triggered Expr]          -- ^ TODO: what is this?   , ae       :: AxiomEnv                   -- ^ Information about reflected function defs   , lrws     :: LocalRewritesEnv           -- ^ Local rewrites+  , defns    :: ![Equation]                -- ^ `define_fun` definitions to be passed to SMT   }   deriving (Eq, Show, Functor, Generic) @@ -773,6 +775,7 @@                 , asserts  = asserts i1  <> asserts i2                 , ae       = ae i1       <> ae i2                 , lrws     = lrws i1     <> lrws i2+                , defns    = defns i1    <> defns i2                 }  @@ -791,6 +794,7 @@                      , asserts  = mempty                      , ae       = mempty                      , lrws     = mempty+                     , defns    = mempty                      }  instance PTable (SInfo a) where@@ -1073,7 +1077,7 @@ instance Fixpoint LocalRewritesEnv where   toFix (LocalRewritesMap rws) = vcat $ uncurry toFixLocal <$> M.toList rws     where-      toFixLocal bid (LocalRewrites rws) = text "defineLocal" <+> toFix bid +      toFixLocal bid (LocalRewrites rws) = text "defineLocal" <+> toFix bid         <+> brackets (vcat $ punctuate ";" $ uncurry toFixRewrite <$> M.toList rws)       toFixRewrite sym eq = toFix sym <+> text ":=" <+> toFix eq 

@@ -87,6 +87,7 @@   -- * Sort coercion for SMT theory encoding   , coerceMapToArray   , coerceSetBagToArray+  , coerceDataDecl   ) where  import qualified Data.Store as S@@ -104,6 +105,7 @@ #endif import           Control.DeepSeq import           Data.Maybe                (fromMaybe)+import           Language.Fixpoint.Types.Config (ElabFlags, elabSetBag) import           Language.Fixpoint.Types.Names import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Spans@@ -706,3 +708,12 @@   | isBag sf = arraySort (coerceSetBagToArray sa) intSort   | otherwise = FApp (coerceSetBagToArray sf) (coerceSetBagToArray sa) coerceSetBagToArray s = s++coerceDataField :: ElabFlags -> DataField -> DataField+coerceDataField ef (DField x t)  = DField x (((if elabSetBag ef then coerceSetBagToArray else id) . coerceMapToArray) t)++coerceDataCtor :: ElabFlags -> DataCtor -> DataCtor+coerceDataCtor ef (DCtor x flds) = DCtor x (coerceDataField ef <$> flds)++coerceDataDecl :: ElabFlags -> DataDecl -> DataDecl+coerceDataDecl ef (DDecl tc n ctors) = DDecl tc n (coerceDataCtor ef <$> ctors)

@@ -37,6 +37,7 @@     -- * Coercing sorts in environments     , coerceEnv     , coerceSortEnv+    , TheorySymbols(..)     ) where  @@ -250,6 +251,10 @@   }   deriving (Eq, Ord, Show, Data, Typeable, Generic) ++class TheorySymbols a where+  theorySymbols :: a ->  SEnv TheorySymbol+ instance NFData Sem instance NFData TheorySymbol instance S.Store TheorySymbol@@ -273,6 +278,7 @@   | Test          -- ^ for ADT tests : `is$cons`   | Field         -- ^ for ADT field: `hd`, `tl`   | Theory        -- ^ for theory ops: mem, cup, select+  | Defined       -- ^ for user-defined `define-fun`   deriving (Eq, Ord, Show, Data, Typeable, Generic)  instance S.Store Sem