Documentation

data Size

arcToBits :: ArcInt -> Int

signedBitsToArc :: Int -> ArcInt

bits :: Size -> Int

bound :: Size -> (ArcInt, ArcInt)

lowerbound :: Size -> ArcInt

upperbound :: Size -> ArcInt

increment :: Size -> Size

arcToFormula :: Eq l => ArcInt -> ArcFormula l

padFrontM :: (Eq l, Solver s l) => Int -> ArcFormula l -> NatMonad s l (ArcFormula l)

truncFront :: Eq l => ArcFormula l -> ArcFormula l

truncTo :: Int -> ArcFormula l -> ArcFormula l

mAdd :: (Eq l, Solver s l) => ArcFormula l -> ArcFormula l -> NatMonad s l (ArcFormula l)

mTimes :: (Ord l, Solver s l) => ArcFormula l -> ArcFormula l -> NatMonad s l (ArcFormula l)

mGrt :: (Eq l, Solver s l) => ArcFormula l -> ArcFormula l -> NatMonad s l (PropFormula l)

mGeq :: (Eq l, Solver s l) => ArcFormula l -> ArcFormula l -> NatMonad s l (PropFormula l)

mEqu :: (Eq l, Solver s l) => ArcFormula l -> ArcFormula l -> NatMonad s l (PropFormula l)

soundInf :: (Eq l, PropAtom a) => Size -> a -> PropFormula l

soundInf' :: (Eq l, PropAtom a) => Int -> a -> PropFormula l

arcAtomM :: (Eq l, Solver s l, PropAtom a) => Size -> a -> NatMonad s l (ArcFormula l)

eval :: Ord l => ArcFormula l -> Assign l -> ArcInt

boolsToInt :: (Bool, [Bool]) -> ArcInt

boolsToInt' :: [Bool] -> Int