.github/workflows/cabal.yml

@@ -14,8 +14,9 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        cabal: ["3.6"]
+        cabal: ["3.10.1.0"]
         ghc:
+          - "9.6.3"
           - "9.4.7"
           - "9.2.3"
         z3:

.github/workflows/stack.yml

@@ -3,6 +3,9 @@ name: stack
 on:
   push:
   pull_request:
+env:
+  # We test in stack jobs that we can build with link-z3-as-a-library
+  STACK_FLAGS: --no-terminal --flag liquid-fixpoint:link-z3-as-a-library
 
 jobs:
   build:
@@ -45,7 +48,7 @@ jobs:
           key: ${{ runner.os }}-${{ matrix.ghc }}-stack-${{ hashFiles('**/*.cabal', './stack/stack-${{ matrix.ghc }}.yaml', './stack/stack-${{ matrix.ghc }}.yaml.lock') }}
 
       - name: Build
-        run: stack test --no-run-tests --no-terminal
+        run: stack test --no-run-tests $STACK_FLAGS
 
       - name: Test
-        run: stack test --no-terminal --test-arguments "--color=always"
+        run: stack test --test-arguments "--color=always" $STACK_FLAGS

CHANGES.md

@@ -2,6 +2,28 @@
 
 ## NEXT
 
+## 0.9.4.7
+
+- Support GHC 9.6 tuples with `--extensionality` [#666](https://github.com/ucsd-progsys/liquid-fixpoint/issues/641) [#667](https://github.com/ucsd-progsys/liquid-fixpoint/issues/641)
+
+## 0.9.2.5
+
+- Adopt smtlib-backends for interactions with the SMT solvers [#641](https://github.com/ucsd-progsys/liquid-fixpoint/issues/641)
+
+## 0.9.0.2
+
+- Simplified the equalities dumped by PLE [#569](https://github.com/ucsd-progsys/liquid-fixpoint/issues/569) [#605](https://github.com/ucsd-progsys/liquid-fixpoint/issues/605)
+- Add PLE implementation based on interpreting expressions [#502](https://github.com/ucsd-progsys/liquid-fixpoint/pull/502)
+
+## 0.8.10.2
+
+- Dump equalities discovered by PLE [#491](https://github.com/ucsd-progsys/liquid-fixpoint/pull/491) [#569](https://github.com/ucsd-progsys/liquid-fixpoint/issues/569)
+- Dump prettified version of constraints [#473](https://github.com/ucsd-progsys/liquid-fixpoint/pull/473)
+- Constraints now indicate the source code location that originated them [#471](https://github.com/ucsd-progsys/liquid-fixpoint/pull/471)
+- Add support for term rewriting to PLE [#428](https://github.com/ucsd-progsys/liquid-fixpoint/pull/428)
+
+## 0.8.6.4
+
 - Fix bugs in PLE
 - Move to GHC 8.6.4 
 - Add `fuel` parameter to debug unfolding in PLE

cabal.project

@@ -1,4 +1,8 @@
 packages: .
 
 package liquid-fixpoint
-  flags: +devel +link-z3-as-a-library
+--  Don't enable z3 linking by default
+--  Most of the time, devs don't care about it and it demands the
+--  z3 library to be at the linker's reach.
+--  flags: +devel +link-z3-as-a-library
+  flags: +devel

liquid-fixpoint.cabal

@@ -1,6 +1,6 @@
 cabal-version:      2.4
 name:               liquid-fixpoint
-version:            0.9.2.5
+version:            0.9.4.7
 synopsis:           Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
 description:
   This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint
@@ -25,13 +25,15 @@ copyright:          2010-17 Ranjit Jhala, University of California, San Diego.
 license:            BSD-3-Clause
 license-file:       LICENSE
 build-type:         Simple
-tested-with:        GHC == 7.10.3, GHC == 8.0.1, GHC == 8.4.3, GHC == 8.6.4, GHC == 8.10.1, GHC == 8.10.7
+tested-with:        GHC == 9.6.3, GHC == 9.4.7, GHC == 9.2.3
 extra-source-files: tests/neg/*.fq
                     tests/pos/*.fq
                     unix/Language/Fixpoint/Utils/*.hs
                     win/Language/Fixpoint/Utils/*.hs
                     tests/logs/cur/pin
                     Makefile
+extra-doc-files:    CHANGES.md
+                    README.md
 
 common warnings
   ghc-options:
@@ -170,6 +172,8 @@ library
   else
     hs-source-dirs: src-cond/without-z3
 
+  if impl(ghc<9.6)
+    ghc-options: -Wno-unused-imports
   if flag(devel)
     ghc-options: -Werror
   if !os(windows)

src/Language/Fixpoint/Defunctionalize.hs

@@ -26,6 +26,7 @@ module Language.Fixpoint.Defunctionalize
 
 import qualified Data.HashMap.Strict as M
 import           Data.Hashable
+import           Control.Monad ((>=>))
 import           Control.Monad.State
 import           Language.Fixpoint.Misc            (fM, secondM, mapSnd)
 import           Language.Fixpoint.Solver.Sanitize (symbolEnv)

src/Language/Fixpoint/Parse.hs

@@ -103,6 +103,7 @@ module Language.Fixpoint.Parse (
 
   ) where
 
+import           Control.Monad (unless, void)
 import           Control.Monad.Combinators.Expr
 import qualified Data.IntMap.Strict          as IM
 import qualified Data.HashMap.Strict         as M

src/Language/Fixpoint/Solver/Extensionality.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP                  #-}
 {-# LANGUAGE FlexibleInstances    #-}
 {-# LANGUAGE PatternGuards        #-}
 {-# LANGUAGE FlexibleContexts     #-}
@@ -201,11 +202,17 @@ initST env dd = ExSt 0 (d:dd) env mempty mempty mempty
   where
     -- NV: hardcore Haskell pairs because they do not appear in DataDecl (why?)
     d = mytracepp "Tuple DataDecl" $ DDecl (symbolFTycon (dummyLoc tupConName)) 2 [ct]
+#if MIN_TOOL_VERSION_ghc(9,6,0)
+    ct = DCtor (dummyLoc (symbol "GHC.Tuple.Prim.(,)")) [
+            DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.Prim.(,)$1")) (FVar 0)
+          , DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.Prim.(,)$2")) (FVar 1)
+          ]
+#else
     ct = DCtor (dummyLoc (symbol "GHC.Tuple.(,)")) [
             DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.(,)$1")) (FVar 0)
           , DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.(,)$2")) (FVar 1)
           ]
-
+#endif
 
 setBEnv :: BindEnv a -> Ex a ()
 setBEnv benv = modify (\st -> st{exbenv = benv})

src/Language/Fixpoint/Solver/Instantiate.hs

@@ -35,6 +35,7 @@ import           Language.Fixpoint.Solver.Sanitize        (symbolEnv)
 import qualified Language.Fixpoint.Solver.PLE as PLE      (instantiate)
 import qualified Language.Fixpoint.Solver.Common as Common (toSMT)
 import           Language.Fixpoint.Solver.Common          (askSMT)
+import           Control.Monad ((>=>), foldM, forM, forM_, join)
 import           Control.Monad.State
 import           Data.Bifunctor (second)
 import qualified Data.Text            as T

src/Language/Fixpoint/Solver/Interpreter.hs

@@ -41,6 +41,7 @@ import           Language.Fixpoint.SortCheck
 import           Language.Fixpoint.Graph.Deps             (isTarget)
 import           Language.Fixpoint.Solver.Sanitize        (symbolEnv)
 import           Language.Fixpoint.Solver.Simplify
+import           Control.Monad (foldM)
 import           Control.Monad.State
 import qualified Data.HashMap.Strict  as M
 import qualified Data.HashSet         as S

src/Language/Fixpoint/Solver/Monad.hs

@@ -29,6 +29,7 @@ module Language.Fixpoint.Solver.Monad
        )
        where
 
+import           Control.Monad (foldM, forM, forM_, when)
 import           Language.Fixpoint.Utils.Progress
 import qualified Language.Fixpoint.Types.Config  as C
 import           Language.Fixpoint.Types.Config  (Config)

src/Language/Fixpoint/Solver/PLE.hs

@@ -52,6 +52,7 @@ import Language.REST.ExploredTerms as ExploredTerms
 import Language.REST.RuntimeTerm as RT
 import Language.REST.SMT (withZ3, SolverHandle)
 
+import           Control.Monad (filterM, foldM, forM_, when)
 import           Control.Monad.State
 import           Control.Monad.Trans.Maybe
 import           Data.Bifunctor (second)

src/Language/Fixpoint/Solver/Rewrite.hs

@@ -21,7 +21,7 @@ module Language.Fixpoint.Solver.Rewrite
   , RESTOrdering(..)
   ) where
 
-import           Control.Monad.State (guard)
+import           Control.Monad (guard)
 import           Control.Monad.Trans.Maybe
 import           Data.Hashable
 import qualified Data.HashMap.Strict  as M

src/Language/Fixpoint/SortCheck.hs

@@ -70,7 +70,6 @@ module Language.Fixpoint.SortCheck  (
 --  import           Control.DeepSeq
 import           Control.Exception (Exception, catch, try, throwIO)
 import           Control.Monad
-import           Control.Monad.Except      -- (MonadError(..))
 import           Control.Monad.Reader
 
 import qualified Data.HashMap.Strict       as M

stack.yaml

@@ -1,19 +1,21 @@
 
-resolver: lts-21.20
-allow-newer: true
+resolver: nightly-2023-11-27
 
 flags:
   liquid-fixpoint:
     devel: true 
+#   Don't enable z3 linking by default
+#   Most of the time, devs don't care about it and it demands the
+#   z3 library to be at the linker's reach.
+#   link-z3-as-a-library: true
 
 packages:
 - '.'
 
 extra-deps:
-- rest-rewrite-0.4.1
-- smtlib-backends-0.3
-- smtlib-backends-z3-0.3
-- smtlib-backends-process-0.3
+- smtlib-backends-0.3@rev:1
+- smtlib-backends-process-0.3@rev:1
+- smtlib-backends-z3-0.3@rev:1
 
 nix:
   packages: [z3]

stack.yaml.lock

@@ -5,43 +5,29 @@
 
 packages:
 - completed:
-    hackage: hashable-1.4.2.0@sha256:585792335d5541dba78fa8dfcb291a89cd5812a281825ff7a44afa296ab5d58a,4520
+    hackage: smtlib-backends-0.3@sha256:69977f97a8db2c11e97bde92fff7e86e793c1fb23827b284bf89938ee463fbf0,1211
     pantry-tree:
-      sha256: 792a6cab3f15c5db29d759c8ca735d0be5f4c94f363329652f8b9780009d0829
-      size: 1248
-  original:
-    hackage: hashable-1.4.2.0
-- completed:
-    hackage: rest-rewrite-0.4.1@sha256:1254960c0a595cf4c9d5a3b986f42644407c63c74578d75b3568a6a12e5143f0,3886
-    pantry-tree:
-      sha256: 17b4e99420cc1929e2b7d29558a0f909d6fcabd263fbc590dbf2585f893f5a6e
-      size: 4018
-  original:
-    hackage: rest-rewrite-0.4.1
-- completed:
-    hackage: smtlib-backends-0.3@sha256:917d88540a9ede7beedbe2ed13b492acddbce394d30ccf5d0ef4f4fba9aa2c12,1157
-    pantry-tree:
-      sha256: 59b578ae7df155a6c73a513358370747e3cc6229ebb44adaba9e0935f811539c
+      sha256: d7c614eab0f3f256b22724ca2d7ac41651f22209242af1d24f052f41d7a7541f
       size: 275
   original:
-    hackage: smtlib-backends-0.3
+    hackage: smtlib-backends-0.3@rev:1
 - completed:
-    hackage: smtlib-backends-z3-0.3@sha256:cca514fa7349a34becb659ff747ec144b7d1902fec2826ff3a51f81388e1eafd,1822
+    hackage: smtlib-backends-process-0.3@sha256:3eee93e91f41c8a2fb2699e95b502a24d8053485ccf7749e2766683d1ebfe11d,1676
     pantry-tree:
-      sha256: e7aee82930b082ed4af91b32a80b8b65249441d458e392cbf2b4d47338e62404
-      size: 499
+      sha256: 579580c8067b4c6640261187fc5d2ac0a02923db4633e0027067de72f947083c
+      size: 461
   original:
-    hackage: smtlib-backends-z3-0.3
+    hackage: smtlib-backends-process-0.3@rev:1
 - completed:
-    hackage: smtlib-backends-process-0.3@sha256:d4d7d02859383e0a43db2d8ce7ef01deffe1bcd356b2ff8626925c3a1c8db922,1600
+    hackage: smtlib-backends-z3-0.3@sha256:b748fafd29eed0ea3f9e3924053c080196fad1eee5a73abc2f52e91f1dc19224,1907
     pantry-tree:
-      sha256: d7d8ec52d07f4a59614000fd93d77b109d085d58f2d96e2c4b972f541c4e8287
-      size: 461
+      sha256: e3365fd8b3d5a06e199f58ad5c53db25cc5d98aca369ee5c649b287a807f5d62
+      size: 499
   original:
-    hackage: smtlib-backends-process-0.3
+    hackage: smtlib-backends-z3-0.3@rev:1
 snapshots:
 - completed:
-    sha256: b73b2b116143aea728c70e65c3239188998bac5bc3be56465813dacd74215dc5
-    size: 648424
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/20/1.yaml
-  original: lts-20.1
+    sha256: c067098ea221c83ce03ccae4cfd5b104fb8a689b17ebb15dbe9d0793e9db4329
+    size: 699418
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2023/11/27.yaml
+  original: nightly-2023-11-27