Qlogic.Diophantine

Contents

• Types
• Operations

Synopsis

• type DioFormula l a b = Formula l (DioAtom a b)
• data DioAtom a b
  • = Grt (DioPoly a b) (DioPoly a b)
  • | Geq (DioPoly a b) (DioPoly a b)
  • | Equ (DioPoly a b) (DioPoly a b)
  • | PAtom PA
• type DioPoly a b = [DioMono a b]
• data DioMono a b = DioMono b [VPower a]
• data VPower a
  • = VPower a Int
  • | RestrictVar a Int
• data DioVar = forall a . DioVarClass a => DioVar a
• class PropAtom a => DioVarClass a where
  • toDioVar :: a -> DioVar
  • fromDioVar :: DioVar -> Maybe a
• class (Solver s l, SizeSemiring b) => MSemiring s l f a b | f -> a, f -> b, f -> s, f -> l, b -> f where
  • plus :: f -> f -> NatMonad s l f
  • prod :: f -> f -> NatMonad s l f
  • zero :: f
  • one :: f
  • geq :: f -> f -> NatMonad s l (PropFormula l)
  • grt :: f -> f -> NatMonad s l (PropFormula l)
  • equ :: f -> f -> NatMonad s l (PropFormula l)
  • constToFormula :: b -> f
  • formAtom :: b -> a -> NatMonad s l f
  • padFormTo :: Int -> f -> f
  • truncFormTo :: Int -> f -> NatMonad s l f
  • bigPlus :: [f] -> NatMonad s l f
  • bigProd :: [f] -> NatMonad s l f
• class Semiring b => SizeSemiring b where
  • sizeToBits :: b -> Int
  • bitsToSize :: Int -> b
• toFormula :: (Ord l, Ord b, DioVarClass a, MSemiring s l f a b) => Maybe b -> b -> DioFormula l a b -> SatSolver s l (PropFormula l)
• constToPoly :: b -> DioPoly a b
• varToPoly :: Semiring b => a -> DioPoly a b
• restrictVarToPoly :: Semiring b => a -> DioPoly a b
• add :: (Eq a, Eq b, Semiring b) => DioPoly a b -> DioPoly a b -> DioPoly a b
• bigAdd :: (Eq a, Eq b, Semiring b) => [DioPoly a b] -> DioPoly a b
• mult :: (Eq a, Eq b, Semiring b) => DioPoly a b -> DioPoly a b -> DioPoly a b
• bigMult :: (Eq a, Eq b, Semiring b) => [DioPoly a b] -> DioPoly a b
• simplify :: (Eq a, Eq b, Semiring b) => DioPoly a b -> DioPoly a b

Types

Operations