Merge pull request #729 from ucsd-progsys/issue-728

Clean up support for CVC5

.circleci/config.yml

@@ -19,7 +19,15 @@ jobs:
             sudo cp z3-4.8.7-x64-ubuntu-16.04/include/* /usr/local/include
             rm -rf z3-4.8.7-x64-ubuntu-16.04
             z3 --version
-
+      - run:
+          name: Install cvc5
+          command: |
+            wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-Linux-x86_64-static.zip
+            unzip cvc5-Linux-x86_64-static.zip
+            rm -f cvc5-Linux-x86_64-static.zip
+            sudo cp cvc5-Linux-x86_64-static/bin/cvc5 /usr/local/bin
+            rm -rf cvc5-Linux-x86_64-static
+            cvc5 --version
       - checkout
       - restore_cache:
           keys:
@@ -38,7 +46,7 @@ jobs:
             - ./.stack-work
       - run:
           name: Compile
-          command : |
+          command: |
             stack --no-terminal build -j2 liquid-fixpoint --flag liquid-fixpoint:devel --test --no-run-tests
       - run:
           name: Test

.github/workflows/cabal.yml

@@ -36,6 +36,16 @@ jobs:
         # https://github.com/actions/runner-images/issues/7061
         run: sudo chown -R $USER /usr/local/.ghcup
 
+      - run:
+        name: Install cvc5
+        command: |
+          wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-Linux-x86_64-static.zip
+          unzip cvc5-Linux-x86_64-static.zip
+          rm -f cvc5-Linux-x86_64-static.zip
+          sudo cp cvc5-Linux-x86_64-static/bin/cvc5 /usr/local/bin
+          rm -rf cvc5-Linux-x86_64-static
+          cvc5 --version
+
       - name: Setup GHC and cabal-install
         uses: haskell-actions/setup@v2
         with:

.github/workflows/stack.yml

@@ -18,9 +18,9 @@ jobs:
       matrix:
         cabal: ["3.10.3.0"]
         vers:
-          - {ghc: "9.8.2", stackage: "nightly-2024-05-25"}
-          - {ghc: "9.6.5", stackage: "lts-22.23"}
-          - {ghc: "9.4.8", stackage: "lts-21.25"}
+          - { ghc: "9.8.2", stackage: "nightly-2024-05-25" }
+          - { ghc: "9.6.5", stackage: "lts-22.23" }
+          - { ghc: "9.4.8", stackage: "lts-21.25" }
         ghc-default:
           - "9.8.2"
         z3:
@@ -34,6 +34,16 @@ jobs:
         with:
           version: ${{ matrix.z3 }}
 
+      - run:
+          name: Install cvc5
+          command: |
+            wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-Linux-x86_64-static.zip
+            unzip cvc5-Linux-x86_64-static.zip
+            rm -f cvc5-Linux-x86_64-static.zip
+            sudo cp cvc5-Linux-x86_64-static/bin/cvc5 /usr/local/bin
+            rm -rf cvc5-Linux-x86_64-static
+            cvc5 --version
+
       - name: Workaround runner image issue
         # https://github.com/actions/runner-images/issues/7061
         run: sudo chown -R $USER /usr/local/.ghcup
@@ -45,7 +55,7 @@ jobs:
           ghc-version: ${{ matrix.vers.ghc }}
           cabal-version: ${{ matrix.cabal }}
           enable-stack: true
-          stack-version: '2.15.7'
+          stack-version: "2.15.7"
 
       - name: Configure stack
         run: |

TODO.md

@@ -1,9 +1 @@
 # TODO
-
-## HORN-SMTLIB
-
-Liquid-Fixpoint Copyright 2013-21 Regents of the University of California.
-All Rights Reserved.
-
-
-(if (<= n 0) 0 (+ n (sum (- n 1))))

src/Language/Fixpoint/Horn/Transformations.hs

@@ -125,7 +125,7 @@ solveEbs cfg query@(Query {}) = do
   whenLoud $ printPiSols piSols
 
   whenLoud $ putStrLn "solved pis:"
-  let solvedPiCstrs = solPis (S.fromList $ M.keys cons ++ M.keys dist) piSols
+  let solvedPiCstrs = solPis cfg (S.fromList $ M.keys cons ++ M.keys dist) piSols
   whenLoud $ putStrLn $ F.showpp solvedPiCstrs
 
   whenLoud $ putStrLn "solved horn:"
@@ -164,18 +164,18 @@ map3 :: (c -> d) -> (a, b, c) -> (a, b, d)
 map3 f (x, y, z) = (x, y, f z)
 
 -- | Solve out the given pivars
-solPis :: S.Set F.Symbol -> M.HashMap F.Symbol ((F.Symbol, [F.Symbol]), Cstr a) -> M.HashMap F.Symbol Pred
-solPis measures piSolsMap = go (M.toList piSolsMap) piSolsMap
+solPis :: F.Config -> S.Set F.Symbol -> M.HashMap F.Symbol ((F.Symbol, [F.Symbol]), Cstr a) -> M.HashMap F.Symbol Pred
+solPis cfg measures piSolsMap = go (M.toList piSolsMap) piSolsMap
   where
     go ((pi', ((n, xs), c)):pis) piSols = M.insert pi' solved $ go pis piSols
-      where solved = solPi measures pi' n (S.fromList xs) piSols c
+      where solved = solPi cfg measures pi' n (S.fromList xs) piSols c
     go [] _ = mempty
 
 -- TODO: rewrite to use CC
-solPi :: S.Set F.Symbol -> F.Symbol -> F.Symbol -> S.Set F.Symbol -> M.HashMap F.Symbol ((F.Symbol, [F.Symbol]), Cstr a) -> Cstr a -> Pred
-solPi measures basePi n args piSols cstr = trace ("\n\nsolPi: " <> F.showpp basePi <> "\n\n" <> F.showpp n <> "\n" <> F.showpp (S.toList args) <> "\n" <> F.showpp ((\(a, _, c) -> (a, c)) <$> edges) <> "\n" <> F.showpp (sols n) <> "\n" <> F.showpp rewritten <> "\n" <> F.showpp cstr <> "\n\n") $ PAnd rewritten
+solPi :: F.Config -> S.Set F.Symbol -> F.Symbol -> F.Symbol -> S.Set F.Symbol -> M.HashMap F.Symbol ((F.Symbol, [F.Symbol]), Cstr a) -> Cstr a -> Pred
+solPi cfg measures basePi n args piSols cstr = trace ("\n\nsolPi: " <> F.showpp basePi <> "\n\n" <> F.showpp n <> "\n" <> F.showpp (S.toList args) <> "\n" <> F.showpp ((\(a, _, c) -> (a, c)) <$> edges) <> "\n" <> F.showpp (sols n) <> "\n" <> F.showpp rewritten <> "\n" <> F.showpp cstr <> "\n\n") $ PAnd rewritten
   where
-    rewritten = rewriteWithEqualities measures n args equalities
+    rewritten = rewriteWithEqualities cfg measures n args equalities
     equalities = (nub . fst) $ go (S.singleton basePi) cstr
     edges = eqEdges args mempty equalities
     (eGraph, vf, lookupVertex) = DG.graphFromEdges edges
@@ -630,8 +630,8 @@ instance V.Visitable (Cstr a) where
 --     equalities = collectEqualities c
 --     ps = rewriteWithEqualities n args equalities
 
-rewriteWithEqualities :: S.Set F.Symbol -> F.Symbol -> S.Set F.Symbol -> [(F.Symbol, F.Expr)] -> [Pred]
-rewriteWithEqualities measures n args equalities = preds
+rewriteWithEqualities :: F.Config -> S.Set F.Symbol -> F.Symbol -> S.Set F.Symbol -> [(F.Symbol, F.Expr)] -> [Pred]
+rewriteWithEqualities cfg measures n args equalities = preds
   where
     (eGraph, vf, lookupVertex) = DG.graphFromEdges $ eqEdges args mempty equalities
 
@@ -647,7 +647,7 @@ rewriteWithEqualities measures n args equalities = preds
       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 []) `S.union`measures
+    argsAndPrims = args `S.union` S.fromList (map fst $ F.toListSEnv $ F.theorySymbols (F.solver cfg) []) `S.union`measures
 
     isWellFormed :: F.Expr -> Bool
     isWellFormed e = S.fromList (F.syms e) `S.isSubsetOf` argsAndPrims

src/Language/Fixpoint/Smt/Serialize.hs

@@ -42,8 +42,8 @@ smt2data env = smt2data' env . map padDataDecl
 
 smt2data' :: SymEnv -> [DataDecl] -> Builder
 smt2data' env ds = seqs [ parens $ smt2many (smt2dataname env <$> ds)
-                         , parens $ smt2many (smt2datactors env <$> ds)
-                         ]
+                        , parens $ smt2many (smt2datactors env <$> ds)
+                        ]
 
 
 smt2dataname :: SymEnv -> DataDecl -> Builder
@@ -54,18 +54,17 @@ smt2dataname env (DDecl tc as _) = parenSeqs [name, n]
 
 
 smt2datactors :: SymEnv -> DataDecl -> Builder
-smt2datactors env (DDecl _ as cs) = parenSeqs ["par", parens tvars, parens ds]
+smt2datactors env (DDecl _ as cs)
+  | as > 0       = parenSeqs ["par", parens tvars, parens ds]
+  | otherwise    =                                 parens ds
   where
     tvars        = smt2many (smt2TV <$> [0..(as-1)])
     smt2TV       = smt2 env . SVar
     ds           = smt2many (smt2ctor env as <$> cs)
 
 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)
+smt2ctor env as (DCtor c fs)  = parenSeqs (smt2 env c : (smt2field env as <$> fs))
 
 smt2field :: SymEnv -> Int -> DataField -> Builder
 smt2field env as d@(DField x t) = parenSeqs [smt2 env x, smt2SortPoly d env $ mkPoly as t]

src/Language/Fixpoint/Smt/Theories.hs

@@ -7,6 +7,7 @@
 {-# LANGUAGE ViewPatterns              #-}
 
 {-# OPTIONS_GHC -Wno-orphans           #-}
+{-# LANGUAGE TupleSections #-}
 
 module Language.Fixpoint.Smt.Theories
      (
@@ -64,6 +65,7 @@ import           Data.Maybe (catMaybes)
 -- import           Data.Text.Format
 import qualified Data.Text
 import           Data.String                 (IsString(..))
+import Text.Printf (printf)
 import Language.Fixpoint.Utils.Builder
 
 {- | [NOTE:Adding-Theories] To add new (SMTLIB supported) theories to
@@ -197,10 +199,10 @@ strLen    = "strLen"
 strSubstr = "subString"
 strConcat = "concatString"
 
-z3strlen, z3strsubstr, z3strconcat :: Raw
-z3strlen    = "str.len"
-z3strsubstr = "str.substr"
-z3strconcat = "str.++"
+smtlibStrLen, smtlibStrSubstr, smtlibStrConcat :: Raw
+smtlibStrLen    = "str.len"
+smtlibStrSubstr = "str.substr"
+smtlibStrConcat = "str.++"
 
 strLenSort, substrSort, concatstrSort :: Sort
 strLenSort    = FFunc strSort intSort
@@ -223,54 +225,65 @@ bFun' name ts out = key "declare-fun" (seqs [fromText name, args, out])
 bSort :: Raw -> Builder -> Builder
 bSort name def = key "define-sort" (fromText name <+> "()" <+> def)
 
-z3Preamble :: Config -> [Builder]
-z3Preamble u
-  = stringPreamble u ++
-    [ bFun boolToIntName
-        [("b", "Bool")]
-        "Int"
-        "(ite b 1 0)"
 
-    , uifDef u (symbolText mulFuncName) "*"
-    , uifDef u (symbolText divFuncName) "div"
-    ]
 
 -- 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 -> Data.Text.Text -> Data.Text.Text -> Builder
 uifDef cfg f op
-  | linear cfg || Z3 /= solver cfg
+  | onlyLinearArith cfg -- linear cfg || Z3 /= solver cfg
   = bFun' f ["Int", "Int"] "Int"
   | otherwise
   = bFun f [("x", "Int"), ("y", "Int")] "Int" (key2 (fromText op) "x" "y")
 
-cvc4Preamble :: Config -> [Builder]
-cvc4Preamble z
-  = "(set-logic ALL_SUPPORTED)" : commonPreamble z
+onlyLinearArith :: Config -> Bool
+onlyLinearArith cfg = linear cfg || solver cfg `notElem` [Z3, Cvc5]
 
-cvc5Preamble :: Config -> [Builder]
-cvc5Preamble z
-  = "(set-logic ALL)" : commonPreamble z
+preamble :: Config -> SMTSolver -> [Builder]
+preamble cfg s = snd <$> filter (matchesCondition s . fst) (solverPreamble cfg)
 
-commonPreamble :: Config -> [Builder]
-commonPreamble _ --TODO use uif flag u (see z3Preamble)
-  = [ bSort string "Int"
-    , bFun boolToIntName [("b", "Bool")] "Int" "(ite b 1 0)"
-    ]
 
-stringPreamble :: Config -> [Builder]
+matchesCondition :: SMTSolver -> PreambleCondition -> Bool
+matchesCondition _ SAll       = True
+matchesCondition s (SOnly ss) = s `elem` ss
+
+solverPreamble :: Config -> [Preamble]
+solverPreamble cfg
+  =  [(SOnly [Cvc4], "(set-logic ALL_SUPPORTED)")]
+  ++ [(SOnly [Cvc5], "(set-logic ALL)")]
+  ++ boolPreamble cfg
+  ++ arithPreamble cfg
+  ++ stringPreamble cfg
+
+type Preamble = (PreambleCondition, Builder)
+
+data PreambleCondition = SAll | SOnly [SMTSolver]
+  deriving (Eq, Show)
+
+
+boolPreamble :: Config -> [Preamble]
+boolPreamble _
+  = [ (SAll, bFun boolToIntName [("b", "Bool")] "Int" "(ite b 1 0)") ]
+
+arithPreamble :: Config -> [Preamble]
+arithPreamble cfg = (SAll,) <$>
+ [ uifDef cfg (symbolText mulFuncName) "*"
+ , uifDef cfg (symbolText divFuncName) "div"
+ ]
+
+stringPreamble :: Config -> [Preamble]
 stringPreamble cfg | stringTheory cfg
-  = [ bSort string "String"
-    , 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")
+  = [ (SAll, bSort string "String")
+    , (SAll, bFun strLen [("s", fromText string)] "Int" (key (fromText smtlibStrLen) "s"))
+    , (SAll, bFun strSubstr [("s", fromText string), ("i", "Int"), ("j", "Int")] (fromText string) (key (fromText smtlibStrSubstr) "s i j"))
+    , (SAll, bFun strConcat [("x", fromText string), ("y", fromText string)] (fromText string) (key (fromText smtlibStrConcat) "x y"))
     ]
 
 stringPreamble _
-  = [ bSort string "Int"
-    , bFun' strLen [fromText string] "Int"
-    , bFun' strSubstr [fromText string, "Int", "Int"] (fromText string)
-    , bFun' strConcat [fromText string, fromText string] (fromText string)
+  = [ (SAll, bSort string "Int")
+    , (SAll, bFun' strLen [fromText string] "Int")
+    , (SAll, bFun' strSubstr [fromText string, "Int", "Int"] (fromText string))
+    , (SAll, bFun' strConcat [fromText string, fromText string] (fromText string))
     ]
 
 --------------------------------------------------------------------------------
@@ -352,11 +365,7 @@ sortAppInfo t = case bkFFunc t of
   Just (_, ts) -> Just (length ts - 1)
   Nothing      -> Nothing
 
-preamble :: Config -> SMTSolver -> [Builder]
-preamble u Z3   = z3Preamble u
-preamble u Cvc4 = cvc4Preamble u
-preamble u Cvc5 = cvc5Preamble u
-preamble u _    = commonPreamble u
+
 
 --------------------------------------------------------------------------------
 -- | Theory Symbols : `uninterpSEnv` should be disjoint from see `interpSEnv`
@@ -366,16 +375,16 @@ preamble u _    = commonPreamble u
 
 -- | `theorySymbols` contains the list of ALL SMT symbols with interpretations,
 --   i.e. which are given via `define-fun` (as opposed to `declare-fun`)
-theorySymbols :: [DataDecl] -> SEnv TheorySymbol -- M.HashMap Symbol TheorySymbol
-theorySymbols ds = fromListSEnv $  -- SHIFTLAM uninterpSymbols
-                                  interpSymbols
+theorySymbols :: SMTSolver -> [DataDecl] -> SEnv TheorySymbol -- M.HashMap Symbol TheorySymbol
+theorySymbols cfg ds = fromListSEnv $  -- SHIFTLAM uninterpSymbols
+                                  interpSymbols cfg
                                ++ concatMap dataDeclSymbols ds
 
 
 --------------------------------------------------------------------------------
-interpSymbols :: [(Symbol, TheorySymbol)]
+interpSymbols :: SMTSolver -> [(Symbol, TheorySymbol)]
 --------------------------------------------------------------------------------
-interpSymbols =
+interpSymbols cfg =
   [
   -- TODO we'll probably need two versions of these - one for sets and one for maps
     interpSym arrConstS  "const"  (FAbs 0 $ FFunc boolSort setArrSort)
@@ -477,14 +486,15 @@ interpSymbols =
   , 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)
-
+  , interpSym intbv32Name   "(_ int2bv 32)" (FFunc intSort bv32)
+  , interpSym intbv64Name   "(_ int2bv 64)" (FFunc intSort bv64)
+  , interpSym bv32intName   (bv2i cfg 32) (FFunc bv32    intSort)
+  , interpSym bv64intName   (bv2i cfg 64) (FFunc bv64    intSort)
+  -- , interpSym bv32intName   "(_ bv2int 32)" (FFunc bv32    intSort)
+  -- , interpSym bv64intName   "(_ bv2int 64)" (FFunc bv64    intSort)
   ]
   where
+
     mapArrSort = arraySort (FVar 0) (FVar 1)
     setArrSort = arraySort (FVar 0) boolSort
     bagArrSort = arraySort (FVar 0) intSort
@@ -515,6 +525,12 @@ interpSymbols =
                                  $ FFunc (bagSort $ FVar 0)
                                          (bagSort $ FVar 0)
     bagSubSort = FAbs 0 $ FFunc (bagSort $ FVar 0) $ FFunc (bagSort $ FVar 0) boolSort
+
+bv2i :: SMTSolver -> Int -> Raw
+bv2i Cvc4 _ = "bv2nat"
+bv2i Cvc5 _ = "bv2nat"
+bv2i _    n = Data.Text.pack $ printf "(_ bv2nat %d)" n
+
 interpBvUop :: Symbol -> (Symbol, TheorySymbol)
 interpBvUop name = interpSym' name bvUopSort
 interpBvBop :: Symbol -> (Symbol, TheorySymbol)