sbv 9.1 → 9.2
raw patch · 8 files changed
+67/−36 lines, 8 files
Files
- CHANGES.md +6/−1
- Data/SBV/Control/Utils.hs +27/−31
- Data/SBV/SMT/SMTLib2.hs +3/−1
- SBVTestSuite/GoldFiles/unint-axioms-query.gold +1/−0
- SBVTestSuite/GoldFiles/uninterpreted-4.gold +1/−0
- SBVTestSuite/GoldFiles/uninterpreted-4a.gold +1/−0
- SBVTestSuite/TestSuite/Uninterpreted/Axioms.hs +27/−2
- sbv.cabal +1/−1
CHANGES.md view
@@ -1,7 +1,12 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://leventerkok.github.io/sbv/> -* Latest Hackage released version: 9.1, 2023-01-09+* Latest Hackage released version: 9.2, 2023-01-16++### Version 9.2, 2023-1-16++ * Handle uninterpreted sorts better, avoiding kind-registration issue.+ See #634 for details. Thanks to Nick Lewchenko for the report. ### Version 9.1, Released, 2023-01-09
Data/SBV/Control/Utils.hs view
@@ -376,7 +376,7 @@ -- Given the function, figure out a default "return value" smtFunDefault _- | Just v <- defaultKindedValue (kindOf (Proxy @r)), Just (res, []) <- parseCVs [v]+ | let v = defaultKindedValue (kindOf (Proxy @r)), Just (res, []) <- parseCVs [v] = Just res | True = Nothing@@ -510,13 +510,7 @@ -- is safe here since we only use in smtFunSaturate calls, which looks at the -- kind stored inside only. mkArg :: forall a. Kind -> SBV a-mkArg k = case defaultKindedValue k of- Nothing -> error $ unlines [ ""- , "*** Data.SBV.smtFunSaturate: Impossible happened!"- , "*** Unable to create a valid parameter for kind: " ++ show k- , "*** Please report this as an SBV bug!"- ]- Just c -> SBV $ SVal k (Left c)+mkArg k = SBV $ SVal k (Left (defaultKindedValue k)) -- | Functions of arity 1 instance ( SymVal a, HasKind a@@ -725,31 +719,33 @@ = extractValue mbi (show s) (kindOf s) -- | "Make up" a CV for this type. Like zero, but smarter.-defaultKindedValue :: Kind -> Maybe CV-defaultKindedValue k = CV k <$> cvt k- where cvt :: Kind -> Maybe CVal- cvt KBool = Just $ CInteger 0- cvt KBounded{} = Just $ CInteger 0- cvt KUnbounded = Just $ CInteger 0- cvt KReal = Just $ CAlgReal 0- cvt (KUserSort _ ui) = uninterp ui- cvt KFloat = Just $ CFloat 0- cvt KDouble = Just $ CDouble 0- cvt KRational = Just $ CRational 0- cvt (KFP eb sb) = Just $ CFP (fpZero False eb sb)- cvt KChar = Just $ CChar '\NUL' -- why not?- cvt KString = Just $ CString ""- cvt (KList _) = Just $ CList []- cvt (KSet _) = Just $ CSet $ RegularSet Set.empty -- why not? Arguably, could be the universal set- cvt (KTuple ks) = CTuple <$> mapM cvt ks- cvt (KMaybe _) = Just $ CMaybe Nothing- cvt (KEither k1 _) = CEither . Left <$> cvt k1 -- why not?+defaultKindedValue :: Kind -> CV+defaultKindedValue k = CV k $ cvt k+ where cvt :: Kind -> CVal+ cvt KBool = CInteger 0+ cvt KBounded{} = CInteger 0+ cvt KUnbounded = CInteger 0+ cvt KReal = CAlgReal 0+ cvt (KUserSort s ui) = uninterp s ui+ cvt KFloat = CFloat 0+ cvt KDouble = CDouble 0+ cvt KRational = CRational 0+ cvt (KFP eb sb) = CFP (fpZero False eb sb)+ cvt KChar = CChar '\NUL' -- why not?+ cvt KString = CString ""+ cvt (KList _) = CList []+ cvt (KSet _) = CSet $ RegularSet Set.empty -- why not? Arguably, could be the universal set+ cvt (KTuple ks) = CTuple $ map cvt ks+ cvt (KMaybe _) = CMaybe Nothing+ cvt (KEither k1 _) = CEither . Left $ cvt k1 -- why not? -- Tricky case of uninterpreted- uninterp (Just (c:_)) = Just $ CUserSort (Just 1, c)- uninterp (Just []) = Nothing -- I don't think this can actually happen, but just in case- uninterp Nothing = Nothing -- Out of luck, truly uninterpreted; we don't even know if it's inhabited.+ uninterp _ (Just (c:_)) = CUserSort (Just 1, c)+ uninterp _ (Just []) = error "defaultKindedValue: enumerated kind with no constructors!" + -- A completely uninterpreted sort, i.e., no elements. Return the witness element for it.+ uninterp s Nothing = CUserSort (Nothing, s ++ "_witness")+ -- | Go from an SExpr directly to a value sexprToVal :: forall a. SymVal a => SExpr -> Maybe a sexprToVal e = fromCV <$> recoverKindedValue (kindOf (Proxy @a)) e@@ -1045,7 +1041,7 @@ Just (Right assocs) | Just res <- convert assocs -> return res | True -> tryPointWise bailOut - Just (Left nm') | nm == nm', Just res <- defaultKindedValue rt -> return ([], res)+ Just (Left nm') | nm == nm', let res = defaultKindedValue rt -> return ([], res) | True -> bad r Nothing Nothing -> tryPointWise bailOut
Data/SBV/SMT/SMTLib2.hs view
@@ -372,7 +372,9 @@ declSort (s, _) | s == "RoundingMode" -- built-in-sort; so don't declare. = []-declSort (s, Nothing) = ["(declare-sort " ++ s ++ " 0) ; N.B. Uninterpreted sort." ]+declSort (s, Nothing) = [ "(declare-sort " ++ s ++ " 0) ; N.B. Uninterpreted sort." + , "(declare-fun " ++ s ++ "_witness () " ++ s ++ ")"+ ] declSort (s, Just fs) = [ "(declare-datatypes ((" ++ s ++ " 0)) ((" ++ unwords (map (\c -> "(" ++ c ++ ")") fs) ++ ")))" , "(define-fun " ++ s ++ "_constrIndex ((x " ++ s ++ ")) Int" ] ++ [" " ++ body fs (0::Int)] ++ [")"]
SBVTestSuite/GoldFiles/unint-axioms-query.gold view
@@ -8,6 +8,7 @@ [GOOD] (set-logic ALL) ; has user-defined sorts, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] (declare-sort B 0) ; N.B. Uninterpreted sort.+[GOOD] (declare-fun B_witness () B) [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ---
SBVTestSuite/GoldFiles/uninterpreted-4.gold view
@@ -8,6 +8,7 @@ [GOOD] (set-logic ALL) ; has user-defined sorts, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] (declare-sort Q 0) ; N.B. Uninterpreted sort.+[GOOD] (declare-fun Q_witness () Q) [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ---
SBVTestSuite/GoldFiles/uninterpreted-4a.gold view
@@ -8,6 +8,7 @@ [GOOD] (set-logic ALL) ; has user-defined sorts, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] (declare-sort Q 0) ; N.B. Uninterpreted sort.+[GOOD] (declare-fun Q_witness () Q) [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants ---
SBVTestSuite/TestSuite/Uninterpreted/Axioms.hs view
@@ -23,15 +23,18 @@ import Data.SBV.Control data Bitstring-mkUninterpretedSort ''Bitstring- data B+data Thing++mkUninterpretedSort ''Bitstring mkUninterpretedSort ''B+mkUninterpretedSort ''Thing tests :: TestTree tests = testGroup "Uninterpreted.Axioms" [ testCase "unint-axioms" (assertIsThm p0)+ , testCase "unint-axioms-empty" (assertIsThm p1) , goldenCapturedIO "unint-axioms-query" testQuery ] @@ -54,6 +57,28 @@ constrain $ a p constrain $ a k return $ a (e k p)++axThings :: [String]+axThings = [ -- thingCompare is reflexive+ "(assert (forall ((k1 Thing))"+ , " (thingCompare k1 k1)))"+ -- thingMerge produces a new, distinct thing+ , "(assert (forall ((k1 Thing) (k2 Thing))"+ , " (distinct k1 (thingMerge k1 k2))))"+ ]++thingCompare :: SThing -> SThing -> SBV Bool+thingCompare = uninterpret "thingCompare"++thingMerge :: SThing -> SThing -> SThing+thingMerge = uninterpret "thingMerge"++p1 :: Symbolic SBool+p1 = do addAxiom "things" axThings+ registerUISMTFunction thingMerge+ k1 <- sbvForall_+ k2 <- sbvForall_+ return $ k1 .== k2 .=> thingCompare k1 k2 testQuery :: FilePath -> IO () testQuery rf = do r <- runSMTWith defaultSMTCfg{verbose=True, redirectVerbose=Just rf} t
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv-Version : 9.1+Version : 9.2 Category : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description : Express properties about Haskell programs and automatically prove them using SMT