| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
ToySolver.SAT.Types
- type Var = Int
- type VarSet = IntSet
- type VarMap = IntMap
- validVar :: Var -> Bool
- class IModel a where
- type Model = UArray Var Bool
- type Lit = Int
- type LitSet = IntSet
- type LitMap = IntMap
- litUndef :: Lit
- validLit :: Lit -> Bool
- literal :: Var -> Bool -> Lit
- litNot :: Lit -> Lit
- litVar :: Lit -> Var
- litPolarity :: Lit -> Bool
- evalLit :: IModel m => m -> Lit -> Bool
- type Clause = [Lit]
- normalizeClause :: Clause -> Maybe Clause
- instantiateClause :: forall m. Monad m => (Lit -> m LBool) -> Clause -> m (Maybe Clause)
- clauseSubsume :: Clause -> Clause -> Bool
- evalClause :: IModel m => m -> Clause -> Bool
- clauseToPBLinAtLeast :: Clause -> PBLinAtLeast
- type AtLeast = ([Lit], Int)
- type Exactly = ([Lit], Int)
- normalizeAtLeast :: AtLeast -> AtLeast
- instantiateAtLeast :: forall m. Monad m => (Lit -> m LBool) -> AtLeast -> m AtLeast
- evalAtLeast :: IModel m => m -> AtLeast -> Bool
- evalExactly :: IModel m => m -> Exactly -> Bool
- type PBLinTerm = (Integer, Lit)
- type PBLinSum = [PBLinTerm]
- type PBLinAtLeast = (PBLinSum, Integer)
- type PBLinExactly = (PBLinSum, Integer)
- normalizePBLinSum :: (PBLinSum, Integer) -> (PBLinSum, Integer)
- normalizePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast
- normalizePBLinExactly :: PBLinExactly -> PBLinExactly
- instantiatePBLinAtLeast :: forall m. Monad m => (Lit -> m LBool) -> PBLinAtLeast -> m PBLinAtLeast
- instantiatePBLinExactly :: Monad m => (Lit -> m LBool) -> PBLinExactly -> m PBLinExactly
- cutResolve :: PBLinAtLeast -> PBLinAtLeast -> Var -> PBLinAtLeast
- cardinalityReduction :: PBLinAtLeast -> AtLeast
- negatePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast
- evalPBLinSum :: IModel m => m -> PBLinSum -> Integer
- evalPBLinAtLeast :: IModel m => m -> PBLinAtLeast -> Bool
- evalPBLinExactly :: IModel m => m -> PBLinAtLeast -> Bool
- pbLowerBound :: PBLinSum -> Integer
- pbUpperBound :: PBLinSum -> Integer
- pbSubsume :: PBLinAtLeast -> PBLinAtLeast -> Bool
- type XORClause = ([Lit], Bool)
- normalizeXORClause :: XORClause -> XORClause
- instantiateXORClause :: forall m. Monad m => (Lit -> m LBool) -> XORClause -> m XORClause
- evalXORClause :: IModel m => m -> XORClause -> Bool
Variable
Model
Minimal complete definition
type Model = UArray Var Bool Source #
A model is represented as a mapping from variables to its values.
Literal
Positive (resp. negative) literals are represented as positive (resp. negative) integers. (DIMACS format).
litPolarity :: Lit -> Bool Source #
Clause
normalizeClause :: Clause -> Maybe Clause Source #
Normalizing clause
Nothing if the clause is trivially true.
Cardinality Constraint
normalizeAtLeast :: AtLeast -> AtLeast Source #
Pseudo Boolean Constraint
type PBLinAtLeast = (PBLinSum, Integer) Source #
type PBLinExactly = (PBLinSum, Integer) Source #
normalizePBLinSum :: (PBLinSum, Integer) -> (PBLinSum, Integer) Source #
normalizing PB term of the form c1 x1 + c2 x2 ... cn xn + c into d1 x1 + d2 x2 ... dm xm + d where d1,...,dm ≥ 1.
normalizePBLinAtLeast :: PBLinAtLeast -> PBLinAtLeast Source #
normalizing PB constraint of the form c1 x1 + c2 cn ... cn xn >= b.
normalizePBLinExactly :: PBLinExactly -> PBLinExactly Source #
normalizing PB constraint of the form c1 x1 + c2 cn ... cn xn = b.
instantiatePBLinAtLeast :: forall m. Monad m => (Lit -> m LBool) -> PBLinAtLeast -> m PBLinAtLeast Source #
instantiatePBLinExactly :: Monad m => (Lit -> m LBool) -> PBLinExactly -> m PBLinExactly Source #
cutResolve :: PBLinAtLeast -> PBLinAtLeast -> Var -> PBLinAtLeast Source #
evalPBLinAtLeast :: IModel m => m -> PBLinAtLeast -> Bool Source #
evalPBLinExactly :: IModel m => m -> PBLinAtLeast -> Bool Source #
pbLowerBound :: PBLinSum -> Integer Source #
pbUpperBound :: PBLinSum -> Integer Source #
pbSubsume :: PBLinAtLeast -> PBLinAtLeast -> Bool Source #
XOR Clause
type XORClause = ([Lit], Bool) Source #
XOR clause
'([l1,l2..ln], b)' means l1 ⊕ l2 ⊕ ⋯ ⊕ ln = b.
Note that:
- True can be represented as ([], False)
- False can be represented as ([], True)
normalizeXORClause :: XORClause -> XORClause Source #
Normalize XOR clause