SoPSat.Internal.Unify
data Unifier f c Source #
Constructors
Fields
Defined in SoPSat.Internal.Unify
Methods
showsPrec :: Int -> Unifier f c -> ShowS #
show :: Unifier f c -> String #
showList :: [Unifier f c] -> ShowS #
(==) :: Unifier f c -> Unifier f c -> Bool #
(/=) :: Unifier f c -> Unifier f c -> Bool #
substsSoP :: (Ord f, Ord c) => [Unifier f c] -> SoP f c -> SoP f c Source #
substSoP :: (Ord f, Ord c) => Atom f c -> SoP f c -> SoP f c -> SoP f c Source #
substProduct :: (Ord f, Ord c) => Atom f c -> SoP f c -> Product f c -> SoP f c Source #
substSymbol :: (Ord f, Ord c) => Atom f c -> SoP f c -> Symbol f c -> SoP f c Source #
substsSubst :: (Ord f, Ord c) => [Unifier f c] -> [Unifier f c] -> [Unifier f c] Source #
unifiers :: (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c] Source #
unifiers' :: (Ord f, Ord c) => SoP f c -> SoP f c -> [Unifier f c] Source #
splitSoP :: (Ord f, Ord c) => SoP f c -> SoP f c -> (SoP f c, SoP f c) Source #
collectBases :: Product f c -> Maybe ([SoP f c], [Product f c]) Source #
safeDiv :: Integer -> Integer -> Maybe Integer Source #
integerLogBase :: Integer -> Integer -> Maybe Integer Source #
integerLogBase' :: Integer -> Integer -> Integer Source #
integerRt :: Integer -> Integer -> Maybe Integer Source #