Grisette.Internal.SymPrim.Quantifier

Documentation

forallSet :: ConstantSymbolSet -> SymBool -> SymBool

Forall quantifier over a set of constant symbols. Quantifier over functions is not supported.

>>> let xsym = "x" :: TypedConstantSymbol Integer
>>> let ysym = "y" :: TypedConstantSymbol Integer
>>> let x = "x" :: SymInteger
>>> let y = "y" :: SymInteger
>>> forallSet (buildSymbolSet [xsym, ysym]) (x .== y)
(forall x :: Integer (forall y :: Integer (= x y)))

Only available with SBV 10.1.0 or later.

forallSym :: (HasCallStack, ExtractSym a) => a -> SymBool -> SymBool

Forall quantifier over all symbolic constants in a value. Quantifier over functions is not supported.

>>> let a = ["x", "y"] :: [SymInteger]
>>> forallSym a $ sum a .== 0
(forall x :: Integer (forall y :: Integer (= (+ x y) 0)))

Only available with sbv 10.1.0 or later.

existsSet :: ConstantSymbolSet -> SymBool -> SymBool

Exists quantifier over a set of constant symbols. Quantifier over functions is not supported.

>>> let xsym = "x" :: TypedConstantSymbol Integer
>>> let ysym = "y" :: TypedConstantSymbol Integer
>>> let x = "x" :: SymInteger
>>> let y = "y" :: SymInteger
>>> existsSet (buildSymbolSet [xsym, ysym]) (x .== y)
(exists x :: Integer (exists y :: Integer (= x y)))

Only available with SBV 10.1.0 or later.

existsSym :: (HasCallStack, ExtractSym a) => a -> SymBool -> SymBool

Exists quantifier over all symbolic constants in a value. Quantifier over functions is not supported.

>>> let a = ["x", "y"] :: [SymInteger]
>>> existsSym a $ sum a .== 0
(exists x :: Integer (exists y :: Integer (= (+ x y) 0)))

Only available with sbv 10.1.0 or later.

forallFresh :: (HasCallStack, ExtractSym v, MonadFresh m, GenSym spec v, TryMerge m) => spec -> (v -> FreshT Union SymBool) -> m SymBool

Forall quantifier over symbolic constants in a freshly generated value. Quantifier over functions is not supported.

>>> :{
x :: Fresh SymBool
x = forallFresh () $ \(a :: SymBool) ->
      existsFresh () $ \(b :: SymBool) ->
        mrgReturn $ a .== b
:}

>>> runFresh x "x"
(forall x@0 :: Bool (exists x@1 :: Bool (= x@0 x@1)))

Only available with sbv 10.1.0 or later.

existsFresh :: (HasCallStack, ExtractSym v, MonadFresh m, GenSym spec v, TryMerge m) => spec -> (v -> FreshT Union SymBool) -> m SymBool

Exists quantifier over symbolic constants in a freshly generated value. Quantifier over functions is not supported.

>>> :{
x :: Fresh SymBool
x = forallFresh () $ \(a :: SymBool) ->
      existsFresh () $ \(b :: SymBool) ->
        mrgReturn $ a .== b
:}

>>> runFresh x "x"
(forall x@0 :: Bool (exists x@1 :: Bool (= x@0 x@1)))

Only available with sbv 10.1.0 or later.