Copyright | (c) Levent Erkok |
---|---|

License | BSD3 |

Maintainer | erkokl@gmail.com |

Stability | experimental |

Safe Haskell | None |

Language | Haskell2010 |

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

# Documentation

A "list-like" data type, but one we plan to uninterpret at the SMT level. The actual shape is really immaterial for us, but could be used as a proxy to generate test cases or explore data-space in some other part of a program. Note that we neither rely on the shape of this data, nor need the actual constructors.

## Instances

Eq L Source # | |

Data L Source # | |

Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat 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 # 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 :: (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 # | |

Ord L Source # | |

Read L Source # | |

Show L Source # | |

HasKind L Source # | Similarly, |

Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat | |

SymVal L Source # | Declare instances to make |

Defined in Documentation.SBV.Examples.Uninterpreted.UISortAllSat mkSymVal :: MonadSymbolic m => Maybe Quantifier -> Maybe String -> m (SBV L) Source # literal :: L -> SBV L Source # isConcretely :: SBV L -> (L -> Bool) -> Bool Source # forall :: MonadSymbolic m => String -> m (SBV L) Source # forall_ :: MonadSymbolic m => m (SBV L) Source # mkForallVars :: MonadSymbolic m => Int -> m [SBV L] Source # exists :: MonadSymbolic m => String -> m (SBV L) Source # exists_ :: MonadSymbolic m => m (SBV L) Source # mkExistVars :: MonadSymbolic m => Int -> m [SBV 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 # |

classify :: SBV L -> SInteger Source #

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

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:

`>>>`

Solution #1: l = L!val!0 :: L l0 = L!val!0 :: L l1 = L!val!1 :: L l2 = L!val!2 :: L classify :: L -> Integer classify L!val!2 = 2 classify L!val!1 = 1 classify _ = 0 Solution #2: l = L!val!1 :: L l0 = L!val!0 :: L l1 = L!val!1 :: L l2 = L!val!2 :: L classify :: L -> Integer classify L!val!2 = 2 classify L!val!1 = 1 classify _ = 0 Solution #3: l = L!val!2 :: L l0 = L!val!0 :: L l1 = L!val!1 :: L l2 = L!val!2 :: L classify :: L -> Integer classify L!val!2 = 2 classify L!val!1 = 1 classify _ = 0 Found 3 different solutions.`allSat genLs`