Safe Haskell	None

Qlogic.NatSat

Synopsis

Documentation

type NatFormula l = [PropFormula l]

data Size

Constructors

Bits Int
Bound Int

Instances

Eq Size
Ord Size
Show Size
Typeable Size

natToBits :: Int -> Int

calculates the necessary length of a list of Top/Bot values for representing the given natural number

bitsToNat :: Int -> Int

bits :: Size -> Int

bound :: Size -> Int

increment :: Size -> Size

data PLVec a

Constructors

PLVec a Int

Instances

Typeable1 PLVec
Eq a => Eq (PLVec a)
Ord a => Ord (PLVec a)
Show a => Show (PLVec a)
(Eq a, Ord a, Show a, Typeable a) => PropAtom (PLVec a)

type NatAssign a = Map a Int

emptyAssignment :: NatAssign a

natToFormula :: Int -> NatFormula l

transforms a natural number into a list of Top/Bot values

newtype NatMonad s l r

Constructors

NatMonad
Fields runNat :: StateT [PropFormula l] (SatSolver s l) r

Instances

Monad s => MonadState [PropFormula l] (NatMonad s l)
Monad s => Monad (NatMonad s l)
(Solver s l, Boolean r) => Boolean (NatMonad s l r)

liftN :: Solver s l => SatSolver s l r -> NatMonad s l r

runNatMonad :: NatMonad s l r -> SatSolver s l (r, [PropFormula l])

toFormula :: (Eq l, Monad s) => NatMonad s l (PropFormula l) -> SatSolver s l (PropFormula l)

freshVar :: Solver s l => NatMonad s l (PropFormula l)

enforce :: Solver s l => [PropFormula l] -> NatMonad s l ()

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

truncBots :: NatFormula l -> NatFormula l

removes leading Bottoms from a list of propositional formulas however, the last Bot in a list consisting only of Bots is never removed

truncTo :: Int -> NatFormula l -> NatFormula l

If the given list of propositional formulas is longer than n, its length is reduced to n by chopping off the first elements

mTruncTo :: (Ord l, Solver s l) => Int -> NatFormula l -> NatMonad s l (NatFormula l)

padBots :: Int -> NatFormula l -> NatFormula l

mAdd :: (Ord l, Solver s l) => NatFormula l -> NatFormula l -> NatMonad s l (NatFormula l)

mAddNO :: (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)

mTimesNO :: (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)

performs equality comparisons of integers in the representation as a list of propositional formulas

natAtom :: (PropAtom a, Eq l) => Size -> a -> NatFormula l

creates a natural number variable encoded by a list of propositional variables. The length of the list is chosen to be exactly enough in order to represent n

natAtomM :: (PropAtom a, Eq l, Solver s l) => Size -> a -> NatMonad s l (NatFormula l)

nBitVar :: (PropAtom a, Eq l) => Int -> a -> NatFormula l

nBitVar' :: (PropAtom a, Eq l) => Int -> Int -> a -> NatFormula l

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

natAssignment :: (Ord a, Typeable a) => Size -> Assign () -> NatAssign a

eval :: Ord l => NatFormula l -> Assign l -> Int

boolsToNat :: [Bool] -> Int