Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Synopsis
- newtype VarName = VarName Text
- newtype Sort = Sort Text
- data Arg = Arg {}
- data DefineFun = DefineFun {}
- data SExpr
- renameDefineFun :: [Text] -> DefineFun -> DefineFun
- insertBindings :: Map Text SExpr -> [SExpr] -> Map Text SExpr
- insertBinding :: Map Text SExpr -> Map Text SExpr -> SExpr -> Map Text SExpr
- inlineLets :: SExpr -> SExpr
- inlineLets' :: Map Text SExpr -> SExpr -> SExpr
- comparisonOps :: [Text]
- partitionPosNeg :: SExpr -> ([SExpr], [SExpr])
- partition :: (a -> Either b c) -> [a] -> ([b], [c])
- select :: (a -> Either b c) -> a -> ([b], [c]) -> ([b], [c])
- nonZero :: SExpr -> Bool
- sumExprs :: [SExpr] -> SExpr
- pattern And :: [SExpr] -> SExpr
- pattern Neg :: SExpr -> SExpr
- pattern Or :: [SExpr] -> SExpr
- pattern BinOp :: Text -> SExpr -> SExpr -> SExpr
- simplify :: SExpr -> SExpr
- antiSymmetricOp :: Text -> Bool
- simplify' :: SExpr -> SExpr
- negateExpr :: SExpr -> SExpr
- extractDefinitions :: Map Text [Text] -> [DefineFun] -> [DefineFun]
Documentation
Instances
Eq VarName Source # | |
Data VarName Source # | |
Defined in Horname.Internal.SMT gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VarName -> c VarName # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VarName # toConstr :: VarName -> Constr # dataTypeOf :: VarName -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c VarName) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarName) # gmapT :: (forall b. Data b => b -> b) -> VarName -> VarName # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VarName -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VarName -> r # gmapQ :: (forall d. Data d => d -> u) -> VarName -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> VarName -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> VarName -> m VarName # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VarName -> m VarName # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VarName -> m VarName # | |
Ord VarName Source # | |
Show VarName Source # | |
Instances
Eq Sort Source # | |
Data Sort Source # | |
Defined in Horname.Internal.SMT gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sort -> c Sort # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sort # dataTypeOf :: Sort -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Sort) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sort) # gmapT :: (forall b. Data b => b -> b) -> Sort -> Sort # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r # gmapQ :: (forall d. Data d => d -> u) -> Sort -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Sort -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sort -> m Sort # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sort -> m Sort # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sort -> m Sort # | |
Ord Sort Source # | |
Show Sort Source # | |
Instances
Eq Arg Source # | |
Data Arg Source # | |
Defined in Horname.Internal.SMT gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Arg -> c Arg # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Arg # dataTypeOf :: Arg -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Arg) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Arg) # gmapT :: (forall b. Data b => b -> b) -> Arg -> Arg # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Arg -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Arg -> r # gmapQ :: (forall d. Data d => d -> u) -> Arg -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Arg -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Arg -> m Arg # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Arg -> m Arg # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Arg -> m Arg # | |
Ord Arg Source # | |
Show Arg Source # | |
Instances
Eq DefineFun Source # | |
Data DefineFun Source # | |
Defined in Horname.Internal.SMT gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefineFun -> c DefineFun # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c DefineFun # toConstr :: DefineFun -> Constr # dataTypeOf :: DefineFun -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c DefineFun) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c DefineFun) # gmapT :: (forall b. Data b => b -> b) -> DefineFun -> DefineFun # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefineFun -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefineFun -> r # gmapQ :: (forall d. Data d => d -> u) -> DefineFun -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DefineFun -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DefineFun -> m DefineFun # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DefineFun -> m DefineFun # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DefineFun -> m DefineFun # | |
Ord DefineFun Source # | |
Defined in Horname.Internal.SMT | |
Show DefineFun Source # | |
Instances
Eq SExpr Source # | |
Data SExpr Source # | |
Defined in Horname.Internal.SMT gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SExpr -> c SExpr # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SExpr # dataTypeOf :: SExpr -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SExpr) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SExpr) # gmapT :: (forall b. Data b => b -> b) -> SExpr -> SExpr # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SExpr -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SExpr -> r # gmapQ :: (forall d. Data d => d -> u) -> SExpr -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SExpr -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SExpr -> m SExpr # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SExpr -> m SExpr # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SExpr -> m SExpr # | |
Ord SExpr Source # | |
Show SExpr Source # | |
inlineLets :: SExpr -> SExpr Source #
This is not correct in the case of quantifiers but ignoring this simplifies the implementation and seems to be enough for z3 and eldarica
comparisonOps :: [Text] Source #
antiSymmetricOp :: Text -> Bool Source #
negateExpr :: SExpr -> SExpr Source #