diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,12 @@ * Hackage: * GitHub: -* 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 diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs --- a/Data/SBV/Control/Utils.hs +++ b/Data/SBV/Control/Utils.hs @@ -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 diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -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)] ++ [")"] diff --git a/SBVTestSuite/GoldFiles/unint-axioms-query.gold b/SBVTestSuite/GoldFiles/unint-axioms-query.gold --- a/SBVTestSuite/GoldFiles/unint-axioms-query.gold +++ b/SBVTestSuite/GoldFiles/unint-axioms-query.gold @@ -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 --- diff --git a/SBVTestSuite/GoldFiles/uninterpreted-4.gold b/SBVTestSuite/GoldFiles/uninterpreted-4.gold --- a/SBVTestSuite/GoldFiles/uninterpreted-4.gold +++ b/SBVTestSuite/GoldFiles/uninterpreted-4.gold @@ -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 --- diff --git a/SBVTestSuite/GoldFiles/uninterpreted-4a.gold b/SBVTestSuite/GoldFiles/uninterpreted-4a.gold --- a/SBVTestSuite/GoldFiles/uninterpreted-4a.gold +++ b/SBVTestSuite/GoldFiles/uninterpreted-4a.gold @@ -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 --- diff --git a/SBVTestSuite/TestSuite/Uninterpreted/Axioms.hs b/SBVTestSuite/TestSuite/Uninterpreted/Axioms.hs --- a/SBVTestSuite/TestSuite/Uninterpreted/Axioms.hs +++ b/SBVTestSuite/TestSuite/Uninterpreted/Axioms.hs @@ -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 diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -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