Copyright	(c) Masahiro Sakai 2016
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010
Extensions	ScopedTypeVariables BangPatterns TypeSynonymInstances FlexibleInstances ConstrainedClassMethods MultiParamTypeClasses ExplicitForAll

ToySolver.SAT.Encoder.PB

Contents

Description

[ES06] N. Eén and N. Sörensson. Translating Pseudo-Boolean Constraints into SAT. JSAT 2:1–26, 2006.

Synopsis

Documentation

Constructors

Instances details

PrimMonad m => AddCardinality m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PB Methods addAtLeast :: Encoder m -> [Lit] -> Int -> m () Source # addAtMost :: Encoder m -> [Lit] -> Int -> m () Source # addExactly :: Encoder m -> [Lit] -> Int -> m () Source #
Monad m => AddClause m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PB Methods addClause :: Encoder m -> Clause -> m () Source #
PrimMonad m => AddPBLin m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PB Methods addPBAtLeast :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBAtMost :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBExactly :: Encoder m -> PBLinSum -> Integer -> m () Source # addPBAtLeastSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source # addPBAtMostSoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source # addPBExactlySoft :: Encoder m -> Lit -> PBLinSum -> Integer -> m () Source #
Monad m => NewVar m (Encoder m) Source #
Instance details Defined in ToySolver.SAT.Encoder.PB Methods newVar :: Encoder m -> m Var Source # newVars :: Encoder m -> Int -> m [Var] Source # newVars_ :: Encoder m -> Int -> m () Source #

Configulation

Constructors

Instances details

Bounded Strategy Source #
Instance details Defined in ToySolver.SAT.Encoder.PB Methods minBound :: Strategy # maxBound :: Strategy #
Enum Strategy Source #
Instance details Defined in ToySolver.SAT.Encoder.PB Methods succ :: Strategy -> Strategy # pred :: Strategy -> Strategy # toEnum :: Int -> Strategy # fromEnum :: Strategy -> Int # enumFrom :: Strategy -> [Strategy] # enumFromThen :: Strategy -> Strategy -> [Strategy] # enumFromTo :: Strategy -> Strategy -> [Strategy] # enumFromThenTo :: Strategy -> Strategy -> Strategy -> [Strategy] #
Show Strategy Source #
Instance details Defined in ToySolver.SAT.Encoder.PB Methods showsPrec :: Int -> Strategy -> ShowS # show :: Strategy -> String # showList :: [Strategy] -> ShowS #
Default Strategy Source #
Instance details Defined in ToySolver.SAT.Encoder.PB Methods def :: Strategy #
Eq Strategy Source #
Instance details Defined in ToySolver.SAT.Encoder.PB Methods (==) :: Strategy -> Strategy -> Bool # (/=) :: Strategy -> Strategy -> Bool #
Ord Strategy Source #
Instance details Defined in ToySolver.SAT.Encoder.PB Methods compare :: Strategy -> Strategy -> Ordering # (<) :: Strategy -> Strategy -> Bool # (<=) :: Strategy -> Strategy -> Bool # (>) :: Strategy -> Strategy -> Bool # (>=) :: Strategy -> Strategy -> Bool # max :: Strategy -> Strategy -> Strategy # min :: Strategy -> Strategy -> Strategy #

Constructors

Polarity
Fields polarityPosOccurs :: Bool polarityNegOccurs :: Bool

Instances details

Show Polarity Source #
Instance details Defined in ToySolver.SAT.Encoder.Tseitin Methods showsPrec :: Int -> Polarity -> ShowS # show :: Polarity -> String # showList :: [Polarity] -> ShowS #
Eq Polarity Source #
Instance details Defined in ToySolver.SAT.Encoder.Tseitin Methods (==) :: Polarity -> Polarity -> Bool # (/=) :: Polarity -> Polarity -> Bool #