From 62753894640b78e9bde18d2a39c8583f02f4d694 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Thu, 14 Nov 2024 08:48:41 -0800 Subject: [PATCH] Explicitly detect support for lambda expression support --- Data/SBV/Core/Symbolic.hs | 14 ++++++- Data/SBV/List.hs | 17 +++++++-- Data/SBV/Provers/ABC.hs | 1 + Data/SBV/Provers/Bitwuzla.hs | 1 + Data/SBV/Provers/Boolector.hs | 1 + Data/SBV/Provers/CVC4.hs | 1 + Data/SBV/Provers/CVC5.hs | 1 + Data/SBV/Provers/DReal.hs | 1 + Data/SBV/Provers/MathSAT.hs | 1 + Data/SBV/Provers/OpenSMT.hs | 1 + Data/SBV/Provers/Yices.hs | 1 + Data/SBV/Provers/Z3.hs | 1 + Data/SBV/SMT/SMTLib2.hs | 71 +++++++++++++++++++++-------------- 13 files changed, 78 insertions(+), 34 deletions(-) diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs index 5197e7a85..b3e935caa 100644 --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -54,7 +54,7 @@ module Data.SBV.Core.Symbolic , getTableIndex, sObserve , SBVPgm(..), MonadSymbolic(..), SymbolicT, Symbolic, runSymbolic, mkNewState, runSymbolicInState, State(..), SMTDef(..), smtDefGivenName, withNewIncState, IncState(..), incrementInternalCounter , inSMTMode, SBVRunMode(..), IStage(..), Result(..), ResultInp(..), UICodeKind(..) - , registerKind, registerLabel, recordObservable + , registerKind, registerLabel, registerSpecialFunction, recordObservable , addAssertion, addNewSMTOption, imposeConstraint, internalConstraint, internalVariable, lambdaVar, quantVar , SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension , SolverCapabilities(..) @@ -872,11 +872,12 @@ instance NFData ResultInp where data ProgInfo = ProgInfo { hasQuants :: Bool , progSpecialRels :: [SpecialRelOp] , progTransClosures :: [(String, String)] + , progSpecialFuncs :: [Op] -- functions that need to be generated, like list reverse/all/any/filter } deriving G.Data instance NFData ProgInfo where - rnf (ProgInfo a b c) = rnf a `seq` rnf b `seq` rnf c + rnf (ProgInfo a b c d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d deriving instance G.Data CallStack deriving instance G.Data SrcLoc @@ -1528,6 +1529,13 @@ registerLabel whence st nm where err w = error $ "SBV (" ++ whence ++ "): " ++ show nm ++ " " ++ w +-- We need to auto-generate certain functions, so keep track of them here +registerSpecialFunction :: State -> Op -> IO () +registerSpecialFunction st o = + do progInfo <- readIORef (rProgInfo st) + let upd p@ProgInfo{progSpecialFuncs} = p{progSpecialFuncs = o : progSpecialFuncs} + when (o `notElem` progSpecialFuncs progInfo) $ modifyState st rProgInfo upd (pure ()) + -- | Create a new constant; hash-cons as necessary newConst :: State -> CV -> IO SV newConst st c = do @@ -1827,6 +1835,7 @@ mkNewState cfg currentRunMode = liftIO $ do progInfo <- newIORef ProgInfo { hasQuants = False , progSpecialRels = [] , progTransClosures = [] + , progSpecialFuncs = [] } rm <- newIORef currentRunMode ctr <- newIORef (-2) -- start from -2; False and True will always occupy the first two elements @@ -2213,6 +2222,7 @@ data SolverCapabilities = SolverCapabilities { , supportsGlobalDecls :: Bool -- ^ Supports global declarations? (Needed for push-pop.) , supportsDataTypes :: Bool -- ^ Supports datatypes? , supportsFoldAndMap :: Bool -- ^ Does it support fold and map? + , supportsLambdas :: Bool -- ^ Does it support lambdas? , supportsSpecialRels :: Bool -- ^ Does it support special relations (orders, transitive closure etc.) , supportsDirectAccessors :: Bool -- ^ Supports data-type accessors without full ascription? , supportsFlattenedModels :: Maybe [String] -- ^ Supports flattened model output? (With given config lines.) diff --git a/Data/SBV/List.hs b/Data/SBV/List.hs index 8078ed36e..b015d7b86 100644 --- a/Data/SBV/List.hs +++ b/Data/SBV/List.hs @@ -51,6 +51,7 @@ import qualified Prelude as P import Data.SBV.Core.Kind import Data.SBV.Core.Data hiding (StrOp(..)) import Data.SBV.Core.Model +import Data.SBV.Core.Symbolic (registerSpecialFunction) import Data.SBV.Lambda import Data.SBV.Tuple @@ -378,7 +379,9 @@ reverse l = SBV $ SVal k $ Right $ cache r where k = kindOf l r st = do sva <- sbvToSV st l - newExpr st k (SBVApp (SeqOp (SBVReverse k)) [sva]) + let op = SeqOp (SBVReverse k) + registerSpecialFunction st op + newExpr st k (SBVApp op [sva]) -- | @`map` op s@ maps the operation on to sequence. -- @@ -569,7 +572,9 @@ all f l = SBV $ SVal KBool $ Right $ cache r where r st = do sva <- sbvToSV st l lam <- lambdaStr st KBool f - newExpr st KBool (SBVApp (SeqOp (SBVSeqAll (kindOf (Proxy @a)) lam)) [sva]) + let op = SeqOp (SBVSeqAll (kindOf (Proxy @a)) lam) + registerSpecialFunction st op + newExpr st KBool (SBVApp op [sva]) -- | Check some element satisfies the predicate. -- -- @@ -586,7 +591,9 @@ any f l = SBV $ SVal KBool $ Right $ cache r where r st = do sva <- sbvToSV st l lam <- lambdaStr st KBool f - newExpr st KBool (SBVApp (SeqOp (SBVSeqAny (kindOf (Proxy @a)) lam)) [sva]) + let op = SeqOp (SBVSeqAny (kindOf (Proxy @a)) lam) + registerSpecialFunction st op + newExpr st KBool (SBVApp op [sva]) -- | @filter f xs@ filters the list with the given predicate. -- @@ -607,7 +614,9 @@ filter f l k = kindOf (Proxy @(SList a)) r st = do sva <- sbvToSV st l lam <- lambdaStr st KBool f - newExpr st k (SBVApp (SeqOp (SBVSeqFilter (kindOf (Proxy @a)) lam)) [sva]) + let op = SeqOp (SBVSeqFilter (kindOf (Proxy @a)) lam) + registerSpecialFunction st op + newExpr st k (SBVApp op [sva]) -- | Lift a unary operator over lists. lift1 :: forall a b. (SymVal a, SymVal b) => Bool -> SeqOp -> Maybe (a -> b) -> SBV a -> SBV b diff --git a/Data/SBV/Provers/ABC.hs b/Data/SBV/Provers/ABC.hs index 202c23c52..a7fbed15c 100644 --- a/Data/SBV/Provers/ABC.hs +++ b/Data/SBV/Provers/ABC.hs @@ -47,6 +47,7 @@ abc = SMTSolver { , supportsGlobalDecls = False , supportsDataTypes = False , supportsFoldAndMap = False + , supportsLambdas = False , supportsSpecialRels = False , supportsDirectAccessors = False , supportsFlattenedModels = Nothing diff --git a/Data/SBV/Provers/Bitwuzla.hs b/Data/SBV/Provers/Bitwuzla.hs index 8b5103108..7e13a9f5a 100644 --- a/Data/SBV/Provers/Bitwuzla.hs +++ b/Data/SBV/Provers/Bitwuzla.hs @@ -45,6 +45,7 @@ bitwuzla = SMTSolver { , supportsGlobalDecls = True , supportsDataTypes = False , supportsFoldAndMap = False + , supportsLambdas = False , supportsSpecialRels = False , supportsDirectAccessors = False , supportsFlattenedModels = Nothing diff --git a/Data/SBV/Provers/Boolector.hs b/Data/SBV/Provers/Boolector.hs index 1b8c1c254..499c9ee42 100644 --- a/Data/SBV/Provers/Boolector.hs +++ b/Data/SBV/Provers/Boolector.hs @@ -45,6 +45,7 @@ boolector = SMTSolver { , supportsGlobalDecls = True , supportsDataTypes = False , supportsFoldAndMap = False + , supportsLambdas = False , supportsSpecialRels = False , supportsDirectAccessors = False , supportsFlattenedModels = Nothing diff --git a/Data/SBV/Provers/CVC4.hs b/Data/SBV/Provers/CVC4.hs index bb96da54e..34cf3acdd 100644 --- a/Data/SBV/Provers/CVC4.hs +++ b/Data/SBV/Provers/CVC4.hs @@ -49,6 +49,7 @@ cvc4 = SMTSolver { , supportsGlobalDecls = True , supportsDataTypes = True , supportsFoldAndMap = False + , supportsLambdas = False , supportsSpecialRels = False , supportsDirectAccessors = True , supportsFlattenedModels = Nothing diff --git a/Data/SBV/Provers/CVC5.hs b/Data/SBV/Provers/CVC5.hs index 14e668d05..a5ca95234 100644 --- a/Data/SBV/Provers/CVC5.hs +++ b/Data/SBV/Provers/CVC5.hs @@ -49,6 +49,7 @@ cvc5 = SMTSolver { , supportsGlobalDecls = True , supportsDataTypes = True , supportsFoldAndMap = False + , supportsLambdas = True , supportsSpecialRels = False , supportsDirectAccessors = True , supportsFlattenedModels = Nothing diff --git a/Data/SBV/Provers/DReal.hs b/Data/SBV/Provers/DReal.hs index 5b9c8cb1c..292dc99ba 100644 --- a/Data/SBV/Provers/DReal.hs +++ b/Data/SBV/Provers/DReal.hs @@ -49,6 +49,7 @@ dReal = SMTSolver { , supportsGlobalDecls = False , supportsDataTypes = False , supportsFoldAndMap = False + , supportsLambdas = False , supportsSpecialRels = False , supportsDirectAccessors = False , supportsFlattenedModels = Nothing diff --git a/Data/SBV/Provers/MathSAT.hs b/Data/SBV/Provers/MathSAT.hs index 612c8269e..1ca442c46 100644 --- a/Data/SBV/Provers/MathSAT.hs +++ b/Data/SBV/Provers/MathSAT.hs @@ -49,6 +49,7 @@ mathSAT = SMTSolver { , supportsGlobalDecls = True , supportsDataTypes = True , supportsFoldAndMap = False + , supportsLambdas = False , supportsSpecialRels = False , supportsDirectAccessors = True , supportsFlattenedModels = Nothing diff --git a/Data/SBV/Provers/OpenSMT.hs b/Data/SBV/Provers/OpenSMT.hs index de9e518da..dd98f7adb 100644 --- a/Data/SBV/Provers/OpenSMT.hs +++ b/Data/SBV/Provers/OpenSMT.hs @@ -45,6 +45,7 @@ openSMT = SMTSolver { , supportsGlobalDecls = True , supportsDataTypes = False , supportsFoldAndMap = False + , supportsLambdas = False , supportsSpecialRels = False , supportsDirectAccessors = False , supportsFlattenedModels = Nothing diff --git a/Data/SBV/Provers/Yices.hs b/Data/SBV/Provers/Yices.hs index aa2e1fded..077698052 100644 --- a/Data/SBV/Provers/Yices.hs +++ b/Data/SBV/Provers/Yices.hs @@ -47,6 +47,7 @@ yices = SMTSolver { , supportsGlobalDecls = True , supportsDataTypes = False , supportsFoldAndMap = False + , supportsLambdas = False , supportsSpecialRels = False , supportsDirectAccessors = False , supportsFlattenedModels = Nothing diff --git a/Data/SBV/Provers/Z3.hs b/Data/SBV/Provers/Z3.hs index c5681f2da..7b0b9cb54 100644 --- a/Data/SBV/Provers/Z3.hs +++ b/Data/SBV/Provers/Z3.hs @@ -47,6 +47,7 @@ z3 = SMTSolver { , supportsGlobalDecls = True , supportsDataTypes = True , supportsFoldAndMap = True + , supportsLambdas = True , supportsSpecialRels = True , supportsDirectAccessors = False -- Needs ascriptions. (See the CVC4 version of this) , supportsFlattenedModels = Just [ "(set-option :pp.max_depth 4294967295)" diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs index 79fe07a42..b69adc36f 100644 --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -11,6 +11,7 @@ {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE PatternGuards #-} +{-# LANGUAGE ParallelListComp #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE ViewPatterns #-} @@ -79,15 +80,21 @@ cvt ctx curProgInfo kindInfo isSat comments allInputs (_, consts) tbls uis defs isFoldMap SeqFoldLeftI{} = True isFoldMap _ = False in (not . null) [ () | o :: SeqOp <- G.universeBi asgnsSeq, isFoldMap o] + hasLambdas = let needsLambda SBVSeqFilter{} = True + needsLambda SBVSeqAll{} = True + needsLambda SBVSeqAny{} = True + needsLambda _ = False + in (not . null) [ () | o :: SeqOp <- G.universeBi asgnsSeq, needsLambda o] - (needsQuantifiers, needsSpecialRels) = case curProgInfo of - ProgInfo hasQ srs tcs -> (hasQ, not (null srs && null tcs)) + (needsQuantifiers, needsSpecialRels, specialFuncs) = case curProgInfo of + ProgInfo hasQ srs tcs sf -> (hasQ, not (null srs && null tcs), sf) -- Is there a reason why we can't handle this problem? -- NB. There's probably a lot more checking we can do here, but this is a start: doesntHandle = listToMaybe [nope w | (w, have, need) <- checks, need && not (have solverCaps)] where checks = [ ("data types", supportsDataTypes, hasTuples || hasEither || hasMaybe) , ("folds and maps", supportsFoldAndMap, hasFoldMap) + , ("needs lambds", supportsLambdas, hasLambdas) , ("set operations", supportsSets, hasSets) , ("bit vectors", supportsBitVectors, hasBVs) , ("special relations", supportsSpecialRels, needsSpecialRels) @@ -102,8 +109,14 @@ cvt ctx curProgInfo kindInfo isSat comments allInputs (_, consts) tbls uis defs , "*** But the chosen solver (" ++ show (name (solver cfg)) ++ ") doesn't support this feature." ] - -- Some cases require all, some require none. Sigh.. - setAll reason = ["(set-logic ALL) ; " ++ reason ++ ", using catch-all."] + -- Some cases require all, some require none. Sigh.. Also, if there're lambdas CVC5 needs HO_ALL + setAll reason = ["(set-logic " ++ allName ++ ") ; " ++ reason ++ ", using catch-all."] + where allName | hasLambdas && isCVC5 = "HO_ALL" + | True = "ALL" + + isCVC5 = case name (solver cfg) of + CVC5 -> True + _ -> False -- Determining the logic is surprisingly tricky! logic @@ -138,6 +151,7 @@ cvt ctx curProgInfo kindInfo isSat comments allInputs (_, consts) tbls uis defs | needsSpecialRels = ["; has special relations, no logic set."] -- Things that require ALL + | hasLambdas = setAll "has lambda expressions" | hasInteger = setAll "has unbounded values" | hasRational = setAll "has rational values" | hasReal = setAll "has algebraic reals" @@ -232,7 +246,7 @@ cvt ctx curProgInfo kindInfo isSat comments allInputs (_, consts) tbls uis defs ++ [ "; --- uninterpreted constants ---" ] ++ concatMap (declUI curProgInfo) uis ++ [ "; --- SBV Function definitions" | not (null funcMap) ] - ++ concat [declSBVFunc op nm | (op, nm) <- M.toAscList funcMap] + ++ concat [declSBVFunc cfg op nm | (op, nm) <- M.toAscList funcMap] ++ [ "; --- user defined functions ---"] ++ userDefs ++ [ "; --- assignments ---" ] @@ -290,19 +304,11 @@ cvt ctx curProgInfo kindInfo isSat comments allInputs (_, consts) tbls uis defs | True = Just $ Left s -- SBV only functions. - funcMap = M.fromList $ [(op, "|sbv.reverse_" ++ show k ++ "|") | (op@(SeqOp (SBVReverse k )), _) <- specials] - ++ [(op, "|sbv.seqFilter_" ++ show k ++ idx i ++ "|") | (op@(SeqOp (SBVSeqFilter k _)), i) <- specials] - ++ [(op, "|sbv.seqAll_" ++ show k ++ idx i ++ "|") | (op@(SeqOp (SBVSeqAll k _)), i) <- specials] - ++ [(op, "|sbv.seqAny_" ++ show k ++ idx i ++ "|") | (op@(SeqOp (SBVSeqAny k _)), i) <- specials] - where specials = zip (nub [op | op@(SeqOp so) <- G.universeBi asgnsSeq, isSpecial so]) [0..] - - isSpecial SBVReverse{} = True - isSpecial SBVSeqFilter{} = True - isSpecial SBVSeqAll{} = True - isSpecial SBVSeqAny{} = True - isSpecial _ = False - - -- if index 0, then ignore it; other wise add it. This distinguishes different functions passed to all/any + funcMap = M.fromList $ [(op, "|sbv.reverse_" ++ show k ++ "|") | op@(SeqOp (SBVReverse k )) <- specialFuncs] + ++ [(op, "|sbv.seqFilter_" ++ show k ++ idx i ++ "|") | op@(SeqOp (SBVSeqFilter k _)) <- specialFuncs | i <- [0..]] + ++ [(op, "|sbv.seqAll_" ++ show k ++ idx i ++ "|") | op@(SeqOp (SBVSeqAll k _)) <- specialFuncs | i <- [0..]] + ++ [(op, "|sbv.seqAny_" ++ show k ++ idx i ++ "|") | op@(SeqOp (SBVSeqAny k _)) <- specialFuncs | i <- [0..]] + where -- if index 0, then ignore it; other wise add it. This distinguishes different functions passed to all/any idx :: Int -> String idx 0 = "" idx i = show i @@ -315,14 +321,14 @@ cvt ctx curProgInfo kindInfo isSat comments allInputs (_, consts) tbls uis defs _ -> Nothing -- Declare "known" SBV functions here -declSBVFunc :: Op -> String -> [String] -declSBVFunc op nm = case op of - SeqOp (SBVReverse KString) -> mkStringRev - SeqOp (SBVReverse (KList k)) -> mkSeqRev (KList k) - SeqOp (SBVSeqFilter ek f) -> mkFilter ek f - SeqOp (SBVSeqAll ek f) -> mkAnyAll True ek f - SeqOp (SBVSeqAny ek f) -> mkAnyAll False ek f - _ -> error $ "Data.SBV.declSBVFunc: Unexpected internal function: " ++ show (op, nm) +declSBVFunc :: SMTConfig -> Op -> String -> [String] +declSBVFunc cfg op nm = case op of + SeqOp (SBVReverse KString) -> mkStringRev + SeqOp (SBVReverse (KList k)) -> mkSeqRev (KList k) + SeqOp (SBVSeqFilter ek f) -> mkFilter ek f + SeqOp (SBVSeqAll ek f) -> mkAnyAll True ek f + SeqOp (SBVSeqAny ek f) -> mkAnyAll False ek f + _ -> error $ "Data.SBV.declSBVFunc: Unexpected internal function: " ++ show (op, nm) where mkStringRev = [ "(define-fun-rec " ++ nm ++ " ((str String)) String" , " (ite (= str \"\")" , " \"\"" @@ -338,10 +344,19 @@ declSBVFunc op nm = case op of ] where t = smtType k + -- in Z3, lambdas are applied with select. In CVC5, it's @. This might change with higher-order features being added to SMTLib in v3 + hoApply + | isCVC5 = "@" + | True = "select" + + isCVC5 = case name (solver cfg) of + CVC5 -> True + _ -> False + mkAnyAll isAll ek f = [ "(define-fun-rec " ++ nm ++ " ((lst " ++ t ++ ")) Bool" , " (ite (= lst (as seq.empty " ++ t ++ "))" , " " ++ base - , " (" ++ conn ++ " (select " ++ f ++ " (seq.nth lst 0)) (" ++ nm ++ " (seq.extract lst 1 (- (seq.len lst) 1))))))" + , " (" ++ conn ++ " (" ++ hoApply ++ " " ++ f ++ " (seq.nth lst 0)) (" ++ nm ++ " (seq.extract lst 1 (- (seq.len lst) 1))))))" ] where t = smtType (KList ek) (base, conn) | isAll = ("true", "and") @@ -350,7 +365,7 @@ declSBVFunc op nm = case op of mkFilter k f = [ "(define-fun-rec " ++ nm ++ " ((lst " ++ t ++ ")) " ++ t , " (ite (= lst (as seq.empty " ++ t ++ "))" , " (as seq.empty " ++ t ++ ")" - , " (ite (select " ++ f ++ " (seq.nth lst 0))" + , " (ite (" ++ hoApply ++ " " ++ f ++ " (seq.nth lst 0))" , " (seq.++ (seq.unit (seq.nth lst 0)) (" ++ nm ++ " (seq.extract lst 1 (- (seq.len lst) 1))))" , " (" ++ nm ++ " (seq.extract lst 1 (- (seq.len lst) 1))))))" ]