Documentation.SBV.Examples.Uninterpreted.UISortAllSat

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

Documentation

data L

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

Instances

Data L

Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> L -> c L

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c L

toConstr :: L -> Constr

dataTypeOf :: L -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c L)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c L)

gmapT :: (forall b. Data b => b -> b) -> L -> L

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> L -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> L -> r

gmapQ :: (forall d. Data d => d -> u) -> L -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> L -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> L -> m L

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> L -> m L

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> L -> m L

Read L

Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat

Methods

readsPrec :: Int -> ReadS L

readList :: ReadS [L]

readPrec :: ReadPrec L

readListPrec :: ReadPrec [L]

Show L

Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat

Methods

showsPrec :: Int -> L -> ShowS

show :: L -> String

showList :: [L] -> ShowS

SymVal L

Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV L)

literal :: L -> SBV L

fromCV :: CV -> L

isConcretely :: SBV L -> (L -> Bool) -> Bool

free :: MonadSymbolic m => String -> m (SBV L)

free_ :: MonadSymbolic m => m (SBV L)

mkFreeVars :: MonadSymbolic m => Int -> m [SBV L]

symbolic :: MonadSymbolic m => String -> m (SBV L)

symbolics :: MonadSymbolic m => [String] -> m [SBV L]

unliteral :: SBV L -> Maybe L

isConcrete :: SBV L -> Bool

isSymbolic :: SBV L -> Bool

HasKind L

Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat

Methods

kindOf :: L -> Kind

hasSign :: L -> Bool

intSizeOf :: L -> Int

isBoolean :: L -> Bool

isBounded :: L -> Bool

isReal :: L -> Bool

isFloat :: L -> Bool

isDouble :: L -> Bool

isRational :: L -> Bool

isFP :: L -> Bool

isUnbounded :: L -> Bool

isUserSort :: L -> Bool

isChar :: L -> Bool

isString :: L -> Bool

isList :: L -> Bool

isSet :: L -> Bool

isTuple :: L -> Bool

isMaybe :: L -> Bool

isEither :: L -> Bool

isArray :: L -> Bool

showType :: L -> String

SatModel L

Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat

Methods

parseCVs :: [CV] -> Maybe (L, [CV])

cvtModel :: (L -> Maybe b) -> Maybe (L, [CV]) -> Maybe (b, [CV])

type SL = SBV L

Symbolic version of the type L.

classify :: SL -> SInteger

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

genLs :: Predicate

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.