Qlogic.IntSat

Synopsis

• data Size
  • = Bits Int
  • | Bound Int Int
• intToBits :: Int -> Int
• signedBitsToNat :: Int -> Int
• bits :: Size -> Int
• bound :: Size -> (Int, Int)
• lowerbound :: Size -> Int
• upperbound :: Size -> Int
• increment :: Size -> Size
• twoComplement :: Eq l => Int -> NatFormula l
• truncFront :: Eq l => NatFormula l -> NatFormula l
• truncTo :: Int -> NatFormula l -> NatFormula l
• padFrontM :: (Eq l, Solver s l) => Int -> NatFormula l -> NatMonad s l (NatFormula l)
• mNegate :: (Ord l, Solver s l) => NatFormula l -> NatMonad s l (NatFormula l)
• mAdd :: (Ord l, Solver s l) => NatFormula l -> NatFormula l -> NatMonad s l (NatFormula l)
• mTimes :: (Ord l, Solver s l) => NatFormula l -> NatFormula l -> NatMonad s l (NatFormula l)
• unsignedMTimes :: (Ord l, Solver s l) => NatFormula l -> NatFormula l -> NatMonad s l (NatFormula l)
• mGrt :: (Solver s l, Eq l) => NatFormula l -> NatFormula l -> NatMonad s l (PropFormula l)
• mGeq :: (Solver s l, Eq l) => NatFormula l -> NatFormula l -> NatMonad s l (PropFormula l)
• mEqu :: (Solver s l, Eq l) => NatFormula l -> NatFormula l -> NatMonad s l (PropFormula l)
• natAtomM :: (PropAtom a, Eq l, Solver s l) => Size -> a -> NatMonad s l (NatFormula l)
• intAssignment :: (Ord a, Typeable a) => Size -> Assign () -> NatAssign a
• eval :: Ord l => NatFormula l -> Assign l -> Int
• boolsToInt :: [Bool] -> Int

Documentation