Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.Uninterpreted.UISortAllSat

Description

Demonstrates uninterpreted sorts and how all-sat behaves for them. Thanks to Eric Seidel for the idea.

Synopsis

data L
cv2L :: String -> [CV] -> L
_undefiner_L :: a
type SL = SBV L
classify :: SL -> SInteger
genLs :: Predicate

Documentation

data L Source #

A "list-like" data type, but one we plan to uninterpret at the SMT level. The actual shape is really immaterial for us.

Instances

Instances details

Arbitrary L Source #
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat Methods arbitrary :: Gen L # shrink :: L -> [L] #
SymVal L Source #
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV L) Source # mkSymValInit :: State -> SBV L -> IO () Source # literal :: L -> SBV L Source # fromCV :: CV -> L Source # isConcretely :: SBV L -> (L -> Bool) -> Bool Source # minMaxBound :: Maybe (L, L) Source # free :: MonadSymbolic m => String -> m (SBV L) Source # free_ :: MonadSymbolic m => m (SBV L) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV L] Source # symbolic :: MonadSymbolic m => String -> m (SBV L) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV L] Source # unliteral :: SBV L -> Maybe L Source # unlitCV :: SBV L -> Maybe (Kind, CVal) Source # isConcrete :: SBV L -> Bool Source # isSymbolic :: SBV L -> Bool Source #
HasKind L Source #
Instance details Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat Methods kindOf :: L -> Kind Source # hasSign :: L -> Bool Source # intSizeOf :: L -> Int Source # isBoolean :: L -> Bool Source # isBounded :: L -> Bool Source # isReal :: L -> Bool Source # isFloat :: L -> Bool Source # isDouble :: L -> Bool Source # isRational :: L -> Bool Source # isFP :: L -> Bool Source # isUnbounded :: L -> Bool Source # isADT :: L -> Bool Source # isChar :: L -> Bool Source # isString :: L -> Bool Source # isList :: L -> Bool Source # isSet :: L -> Bool Source # isTuple :: L -> Bool Source # isArray :: L -> Bool Source # isRoundingMode :: L -> Bool Source # isUninterpreted :: L -> Bool Source # showType :: L -> String Source #

cv2L :: String -> [CV] -> L Source #

Conversion from SMT values to L values.

_undefiner_L :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SL = SBV L Source #

Symbolic version of the type L.

classify :: SL -> SInteger Source #

An uninterpreted "classify" function. Really, we only care about the fact that such a function exists, not what it does.

genLs :: Predicate Source #

Formulate a query that essentially asserts a cardinality constraint on the uninterpreted sort L. The goal is to say there are precisely 3 such things, as it might be the case. We manage this by declaring four elements, and asserting that for a free variable of this sort, the shape of the data matches one of these three instances. That is, we assert that all the instances of the data L can be classified into 3 equivalence classes. Then, allSat returns all the possible instances, which of course are all uninterpreted.

As expected, we have:

>>> allSat genLs
Solution #1:
  l  = L_2 :: L
  l0 = L_0 :: L
  l1 = L_1 :: L
  l2 = L_2 :: L

  classify :: L -> Integer
  classify L_2 = 2
  classify L_1 = 1
  classify _   = 0
Solution #2:
  l  = L_1 :: L
  l0 = L_0 :: L
  l1 = L_1 :: L
  l2 = L_2 :: L

  classify :: L -> Integer
  classify L_2 = 2
  classify L_1 = 1
  classify _   = 0
Solution #3:
  l  = L_0 :: L
  l0 = L_0 :: L
  l1 = L_1 :: L
  l2 = L_2 :: L

  classify :: L -> Integer
  classify L_2 = 2
  classify L_1 = 1
  classify _   = 0
Found 3 different solutions.