Documentation

type ArcFormula l = (PropFormula l, [PropFormula l])

data ArcBZVec a

data Size

arcToBits :: ArcInt -> Int

bitsToArc :: Int -> ArcInt

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

bits :: Size -> Int

bound :: Size -> ArcInt

intbound :: Size -> Int

increment :: Size -> Size

padBots :: Int -> ArcFormula l -> ArcFormula l

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

mTruncTo :: (Ord l, Solver s l) => Int -> ArcFormula l -> NatMonad s 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

arcAtom :: (Eq l, PropAtom a) => Size -> a -> ArcFormula l

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

arcAtom' :: (Eq l, PropAtom a) => Int -> Int -> a -> [PropFormula l]

baseFromVec :: (Ord a, Show a, Typeable a) => ArcBZVec a -> a

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

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

boolsToInt' :: [Bool] -> Int