Horname.Internal.SMT

Documentation

newtype VarName

Constructors

VarName Text

Instances

Eq VarName

Methods

(==) :: VarName -> VarName -> Bool

(/=) :: VarName -> VarName -> Bool

Data VarName

Methods

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

Methods

compare :: VarName -> VarName -> Ordering

(<) :: VarName -> VarName -> Bool

(<=) :: VarName -> VarName -> Bool

(>) :: VarName -> VarName -> Bool

(>=) :: VarName -> VarName -> Bool

max :: VarName -> VarName -> VarName

min :: VarName -> VarName -> VarName

Show VarName

Methods

showsPrec :: Int -> VarName -> ShowS

show :: VarName -> String

showList :: [VarName] -> ShowS

newtype Sort

Constructors

Sort Text

Instances

Eq Sort

Methods

(==) :: Sort -> Sort -> Bool

(/=) :: Sort -> Sort -> Bool

Data Sort

Methods

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

toConstr :: Sort -> Constr

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

Methods

compare :: Sort -> Sort -> Ordering

(<) :: Sort -> Sort -> Bool

(<=) :: Sort -> Sort -> Bool

(>) :: Sort -> Sort -> Bool

(>=) :: Sort -> Sort -> Bool

max :: Sort -> Sort -> Sort

min :: Sort -> Sort -> Sort

Show Sort

Methods

showsPrec :: Int -> Sort -> ShowS

show :: Sort -> String

showList :: [Sort] -> ShowS

data Arg

Constructors

Arg

Fields

• argName :: !VarName
• argSort :: !Sort

Instances

Eq Arg

Methods

(==) :: Arg -> Arg -> Bool

(/=) :: Arg -> Arg -> Bool

Data Arg

Methods

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

toConstr :: Arg -> Constr

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

Methods

compare :: Arg -> Arg -> Ordering

(<) :: Arg -> Arg -> Bool

(<=) :: Arg -> Arg -> Bool

(>) :: Arg -> Arg -> Bool

(>=) :: Arg -> Arg -> Bool

max :: Arg -> Arg -> Arg

min :: Arg -> Arg -> Arg

Show Arg

Methods

showsPrec :: Int -> Arg -> ShowS

show :: Arg -> String

showList :: [Arg] -> ShowS

data DefineFun

Constructors

DefineFun

Fields

• funName :: !Text
• arguments :: ![Arg]
• returnSort :: !Sort
• body :: !SExpr

Instances

Eq DefineFun

Methods

(==) :: DefineFun -> DefineFun -> Bool

(/=) :: DefineFun -> DefineFun -> Bool

Data DefineFun

Methods

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

Methods

compare :: DefineFun -> DefineFun -> Ordering

(<) :: DefineFun -> DefineFun -> Bool

(<=) :: DefineFun -> DefineFun -> Bool

(>) :: DefineFun -> DefineFun -> Bool

(>=) :: DefineFun -> DefineFun -> Bool

max :: DefineFun -> DefineFun -> DefineFun

min :: DefineFun -> DefineFun -> DefineFun

Show DefineFun

Methods

showsPrec :: Int -> DefineFun -> ShowS

show :: DefineFun -> String

showList :: [DefineFun] -> ShowS

data SExpr

Constructors

IntLit !Integer

StringLit !Text

List ![SExpr]

Instances

Eq SExpr

Methods

(==) :: SExpr -> SExpr -> Bool

(/=) :: SExpr -> SExpr -> Bool

Data SExpr

Methods

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

toConstr :: SExpr -> Constr

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

Methods

compare :: SExpr -> SExpr -> Ordering

(<) :: SExpr -> SExpr -> Bool

(<=) :: SExpr -> SExpr -> Bool

(>) :: SExpr -> SExpr -> Bool

(>=) :: SExpr -> SExpr -> Bool

max :: SExpr -> SExpr -> SExpr

min :: SExpr -> SExpr -> SExpr

Show SExpr

Methods

showsPrec :: Int -> SExpr -> ShowS

show :: SExpr -> String

showList :: [SExpr] -> ShowS

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

This is not correct in the case of quantifiers but ignoring this simplifies the implementation and seems to be enough for z3 and eldarica

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]