Copyright	(c) Masahiro Sakai 2011-20142016-2018
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	experimental
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010
Extensions	MonoLocalBinds BangPatterns TypeFamilies OverloadedStrings KindSignatures ExplicitNamespaces

ToySolver.Converter.PB

Contents

Normalization of PB/WBO problems
Modify objective function
Linealization of PB/WBO problems
Quadratization of PB problems
Converting inequality constraints into equality constraints
Converting constraints into penalty terms in objective function
PB↔WBO conversion
SAT↔PB conversion
MaxSAT↔WBO conversion
PB→QUBO conversion
General data types
misc

Description

Synopsis

module ToySolver.Converter.Base
module ToySolver.Converter.Tseitin
normalizePB :: Formula -> Formula
normalizeWBO :: SoftFormula -> SoftFormula
data ObjType
- = ObjNone
- | ObjMaxOne
- | ObjMaxZero
setObj :: ObjType -> Formula -> Formula
linearizePB :: Formula -> Bool -> (Formula, PBLinearizeInfo)
linearizeWBO :: SoftFormula -> Bool -> (SoftFormula, PBLinearizeInfo)
type PBLinearizeInfo = PBTseitinInfo
quadratizePB :: Formula -> ((Formula, Integer), PBQuadratizeInfo)
quadratizePB' :: (Formula, Integer) -> ((Formula, Integer), PBQuadratizeInfo)
type PBQuadratizeInfo = PBTseitinInfo
inequalitiesToEqualitiesPB :: Formula -> (Formula, PBInequalitiesToEqualitiesInfo)
data PBInequalitiesToEqualitiesInfo = PBInequalitiesToEqualitiesInfo !Int !Int [(Sum, Integer, [Var])]
unconstrainPB :: Formula -> ((Formula, Integer), PBUnconstrainInfo)
newtype PBUnconstrainInfo = PBUnconstrainInfo PBInequalitiesToEqualitiesInfo
pb2wbo :: Formula -> (SoftFormula, PB2WBOInfo)
newtype PB2WBOInfo = PB2WBOInfo Integer
wbo2pb :: SoftFormula -> (Formula, WBO2PBInfo)
data WBO2PBInfo = WBO2PBInfo !Int !Int (VarMap Constraint)
addWBO :: (PrimMonad m, AddPBNL m enc) => enc -> SoftFormula -> m (PBSum, VarMap Constraint)
sat2pb :: CNF -> (Formula, SAT2PBInfo)
type SAT2PBInfo = IdentityTransformer Model
pb2sat :: Formula -> (CNF, PB2SATInfo)
pb2satWith :: Strategy -> Formula -> (CNF, PB2SATInfo)
type PB2SATInfo = TseitinInfo
maxsat2wbo :: WCNF -> (SoftFormula, MaxSAT2WBOInfo)
type MaxSAT2WBOInfo = PBIdentityInfo
wbo2maxsat :: SoftFormula -> (WCNF, WBO2MaxSATInfo)
wbo2maxsatWith :: Strategy -> SoftFormula -> (WCNF, WBO2MaxSATInfo)
type WBO2MaxSATInfo = PBTseitinInfo
pb2qubo' :: Formula -> ((Formula, Integer), PB2QUBOInfo')
type PB2QUBOInfo' = ComposedTransformer PBUnconstrainInfo PBQuadratizeInfo
data PBIdentityInfo = PBIdentityInfo
newtype PBTseitinInfo = PBTseitinInfo TseitinInfo
pb2lsp :: Formula -> Builder
wbo2lsp :: SoftFormula -> Builder
pb2smp :: Bool -> Formula -> Builder

Documentation

module ToySolver.Converter.Base

module ToySolver.Converter.Tseitin

Normalization of PB/WBO problems

normalizePB :: Formula -> Formula Source #

normalizeWBO :: SoftFormula -> SoftFormula Source #

Modify objective function

data ObjType Source #

Constructors

ObjNone
ObjMaxOne
ObjMaxZero

Instances

Instances details

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

setObj :: ObjType -> Formula -> Formula Source #

Linealization of PB/WBO problems

linearizePB :: Formula -> Bool -> (Formula, PBLinearizeInfo) Source #

linearizeWBO :: SoftFormula -> Bool -> (SoftFormula, PBLinearizeInfo) Source #

type PBLinearizeInfo = PBTseitinInfo Source #

Quadratization of PB problems

quadratizePB :: Formula -> ((Formula, Integer), PBQuadratizeInfo) Source #

Quandratize PBO/PBS problem without introducing additional constraints.

quadratizePB' :: (Formula, Integer) -> ((Formula, Integer), PBQuadratizeInfo) Source #

Quandratize PBO/PBS problem without introducing additional constraints.

type PBQuadratizeInfo = PBTseitinInfo Source #

Converting inequality constraints into equality constraints

inequalitiesToEqualitiesPB :: Formula -> (Formula, PBInequalitiesToEqualitiesInfo) Source #

Convert inequality constraints into equality constraints by introducing surpass variables.

data PBInequalitiesToEqualitiesInfo Source #

Constructors

PBInequalitiesToEqualitiesInfo !Int !Int [(Sum, Integer, [Var])]

Instances

Instances details

FromJSON PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods parseJSON :: Value -> Parser PBInequalitiesToEqualitiesInfo # parseJSONList :: Value -> Parser [PBInequalitiesToEqualitiesInfo] # omittedField :: Maybe PBInequalitiesToEqualitiesInfo #
ToJSON PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods toJSON :: PBInequalitiesToEqualitiesInfo -> Value # toEncoding :: PBInequalitiesToEqualitiesInfo -> Encoding # toJSONList :: [PBInequalitiesToEqualitiesInfo] -> Value # toEncodingList :: [PBInequalitiesToEqualitiesInfo] -> Encoding # omitField :: PBInequalitiesToEqualitiesInfo -> Bool #
Show PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods showsPrec :: Int -> PBInequalitiesToEqualitiesInfo -> ShowS # show :: PBInequalitiesToEqualitiesInfo -> String # showList :: [PBInequalitiesToEqualitiesInfo] -> ShowS #
Eq PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods (==) :: PBInequalitiesToEqualitiesInfo -> PBInequalitiesToEqualitiesInfo -> Bool # (/=) :: PBInequalitiesToEqualitiesInfo -> PBInequalitiesToEqualitiesInfo -> Bool #
BackwardTransformer PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformBackward :: PBInequalitiesToEqualitiesInfo -> Target PBInequalitiesToEqualitiesInfo -> Source PBInequalitiesToEqualitiesInfo Source #
ForwardTransformer PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformForward :: PBInequalitiesToEqualitiesInfo -> Source PBInequalitiesToEqualitiesInfo -> Target PBInequalitiesToEqualitiesInfo Source #
ObjValueBackwardTransformer PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueBackward :: PBInequalitiesToEqualitiesInfo -> TargetObjValue PBInequalitiesToEqualitiesInfo -> SourceObjValue PBInequalitiesToEqualitiesInfo Source #
ObjValueForwardTransformer PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueForward :: PBInequalitiesToEqualitiesInfo -> SourceObjValue PBInequalitiesToEqualitiesInfo -> TargetObjValue PBInequalitiesToEqualitiesInfo Source #
ObjValueTransformer PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type SourceObjValue PBInequalitiesToEqualitiesInfo Source # type TargetObjValue PBInequalitiesToEqualitiesInfo Source #
Transformer PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type Source PBInequalitiesToEqualitiesInfo Source # type Target PBInequalitiesToEqualitiesInfo Source #
type Source PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB type Source PBInequalitiesToEqualitiesInfo = Model
type SourceObjValue PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB type SourceObjValue PBInequalitiesToEqualitiesInfo = Integer
type Target PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB type Target PBInequalitiesToEqualitiesInfo = Model
type TargetObjValue PBInequalitiesToEqualitiesInfo Source #
Instance details Defined in ToySolver.Converter.PB type TargetObjValue PBInequalitiesToEqualitiesInfo = Integer

Converting constraints into penalty terms in objective function

unconstrainPB :: Formula -> ((Formula, Integer), PBUnconstrainInfo) Source #

newtype PBUnconstrainInfo Source #

Constructors

PBUnconstrainInfo PBInequalitiesToEqualitiesInfo

Instances

Instances details

FromJSON PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods parseJSON :: Value -> Parser PBUnconstrainInfo # parseJSONList :: Value -> Parser [PBUnconstrainInfo] # omittedField :: Maybe PBUnconstrainInfo #
ToJSON PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods toJSON :: PBUnconstrainInfo -> Value # toEncoding :: PBUnconstrainInfo -> Encoding # toJSONList :: [PBUnconstrainInfo] -> Value # toEncodingList :: [PBUnconstrainInfo] -> Encoding # omitField :: PBUnconstrainInfo -> Bool #
Show PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods showsPrec :: Int -> PBUnconstrainInfo -> ShowS # show :: PBUnconstrainInfo -> String # showList :: [PBUnconstrainInfo] -> ShowS #
Eq PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods (==) :: PBUnconstrainInfo -> PBUnconstrainInfo -> Bool # (/=) :: PBUnconstrainInfo -> PBUnconstrainInfo -> Bool #
BackwardTransformer PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformBackward :: PBUnconstrainInfo -> Target PBUnconstrainInfo -> Source PBUnconstrainInfo Source #
ForwardTransformer PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformForward :: PBUnconstrainInfo -> Source PBUnconstrainInfo -> Target PBUnconstrainInfo Source #
ObjValueBackwardTransformer PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueBackward :: PBUnconstrainInfo -> TargetObjValue PBUnconstrainInfo -> SourceObjValue PBUnconstrainInfo Source #
ObjValueForwardTransformer PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueForward :: PBUnconstrainInfo -> SourceObjValue PBUnconstrainInfo -> TargetObjValue PBUnconstrainInfo Source #
ObjValueTransformer PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type SourceObjValue PBUnconstrainInfo Source # type TargetObjValue PBUnconstrainInfo Source #
Transformer PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type Source PBUnconstrainInfo Source # type Target PBUnconstrainInfo Source #
type Source PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB type Source PBUnconstrainInfo = Model
type SourceObjValue PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB type SourceObjValue PBUnconstrainInfo = Integer
type Target PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB type Target PBUnconstrainInfo = Model
type TargetObjValue PBUnconstrainInfo Source #
Instance details Defined in ToySolver.Converter.PB type TargetObjValue PBUnconstrainInfo = Integer

PB↔WBO conversion

pb2wbo :: Formula -> (SoftFormula, PB2WBOInfo) Source #

newtype PB2WBOInfo Source #

Constructors

PB2WBOInfo Integer

Instances

Instances details

FromJSON PB2WBOInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods parseJSON :: Value -> Parser PB2WBOInfo # parseJSONList :: Value -> Parser [PB2WBOInfo] # omittedField :: Maybe PB2WBOInfo #
ToJSON PB2WBOInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods toJSON :: PB2WBOInfo -> Value # toEncoding :: PB2WBOInfo -> Encoding # toJSONList :: [PB2WBOInfo] -> Value # toEncodingList :: [PB2WBOInfo] -> Encoding # omitField :: PB2WBOInfo -> Bool #
Show PB2WBOInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods showsPrec :: Int -> PB2WBOInfo -> ShowS # show :: PB2WBOInfo -> String # showList :: [PB2WBOInfo] -> ShowS #
Eq PB2WBOInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods (==) :: PB2WBOInfo -> PB2WBOInfo -> Bool # (/=) :: PB2WBOInfo -> PB2WBOInfo -> Bool #
BackwardTransformer PB2WBOInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformBackward :: PB2WBOInfo -> Target PB2WBOInfo -> Source PB2WBOInfo Source #
ForwardTransformer PB2WBOInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformForward :: PB2WBOInfo -> Source PB2WBOInfo -> Target PB2WBOInfo Source #
ObjValueBackwardTransformer PB2WBOInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueBackward :: PB2WBOInfo -> TargetObjValue PB2WBOInfo -> SourceObjValue PB2WBOInfo Source #
ObjValueForwardTransformer PB2WBOInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueForward :: PB2WBOInfo -> SourceObjValue PB2WBOInfo -> TargetObjValue PB2WBOInfo Source #
ObjValueTransformer PB2WBOInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type SourceObjValue PB2WBOInfo Source # type TargetObjValue PB2WBOInfo Source #
Transformer PB2WBOInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type Source PB2WBOInfo Source # type Target PB2WBOInfo Source #
type Source PB2WBOInfo Source #
Instance details Defined in ToySolver.Converter.PB type Source PB2WBOInfo = Model
type SourceObjValue PB2WBOInfo Source #
Instance details Defined in ToySolver.Converter.PB type SourceObjValue PB2WBOInfo = Integer
type Target PB2WBOInfo Source #
Instance details Defined in ToySolver.Converter.PB type Target PB2WBOInfo = Model
type TargetObjValue PB2WBOInfo Source #
Instance details Defined in ToySolver.Converter.PB type TargetObjValue PB2WBOInfo = Integer

wbo2pb :: SoftFormula -> (Formula, WBO2PBInfo) Source #

data WBO2PBInfo Source #

Constructors

WBO2PBInfo !Int !Int (VarMap Constraint)

Instances

Instances details

FromJSON WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods parseJSON :: Value -> Parser WBO2PBInfo # parseJSONList :: Value -> Parser [WBO2PBInfo] # omittedField :: Maybe WBO2PBInfo #
ToJSON WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods toJSON :: WBO2PBInfo -> Value # toEncoding :: WBO2PBInfo -> Encoding # toJSONList :: [WBO2PBInfo] -> Value # toEncodingList :: [WBO2PBInfo] -> Encoding # omitField :: WBO2PBInfo -> Bool #
Show WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods showsPrec :: Int -> WBO2PBInfo -> ShowS # show :: WBO2PBInfo -> String # showList :: [WBO2PBInfo] -> ShowS #
Eq WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods (==) :: WBO2PBInfo -> WBO2PBInfo -> Bool # (/=) :: WBO2PBInfo -> WBO2PBInfo -> Bool #
BackwardTransformer WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformBackward :: WBO2PBInfo -> Target WBO2PBInfo -> Source WBO2PBInfo Source #
ForwardTransformer WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformForward :: WBO2PBInfo -> Source WBO2PBInfo -> Target WBO2PBInfo Source #
ObjValueBackwardTransformer WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueBackward :: WBO2PBInfo -> TargetObjValue WBO2PBInfo -> SourceObjValue WBO2PBInfo Source #
ObjValueForwardTransformer WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueForward :: WBO2PBInfo -> SourceObjValue WBO2PBInfo -> TargetObjValue WBO2PBInfo Source #
ObjValueTransformer WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type SourceObjValue WBO2PBInfo Source # type TargetObjValue WBO2PBInfo Source #
Transformer WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type Source WBO2PBInfo Source # type Target WBO2PBInfo Source #
type Source WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB type Source WBO2PBInfo = Model
type SourceObjValue WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB type SourceObjValue WBO2PBInfo = Integer
type Target WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB type Target WBO2PBInfo = Model
type TargetObjValue WBO2PBInfo Source #
Instance details Defined in ToySolver.Converter.PB type TargetObjValue WBO2PBInfo = Integer

addWBO :: (PrimMonad m, AddPBNL m enc) => enc -> SoftFormula -> m (PBSum, VarMap Constraint) Source #

SAT↔PB conversion

sat2pb :: CNF -> (Formula, SAT2PBInfo) Source #

type SAT2PBInfo = IdentityTransformer Model Source #

pb2sat :: Formula -> (CNF, PB2SATInfo) Source #

Convert a pseudo boolean formula φ to a equisatisfiable CNF formula ψ together with two functions f and g such that:

if M ⊨ φ then f(M) ⊨ ψ
if M ⊨ ψ then g(M) ⊨ φ

pb2satWith :: Strategy -> Formula -> (CNF, PB2SATInfo) Source #

type PB2SATInfo = TseitinInfo Source #

MaxSAT↔WBO conversion

maxsat2wbo :: WCNF -> (SoftFormula, MaxSAT2WBOInfo) Source #

type MaxSAT2WBOInfo = PBIdentityInfo Source #

wbo2maxsat :: SoftFormula -> (WCNF, WBO2MaxSATInfo) Source #

wbo2maxsatWith :: Strategy -> SoftFormula -> (WCNF, WBO2MaxSATInfo) Source #

type WBO2MaxSATInfo = PBTseitinInfo Source #

PB→QUBO conversion

pb2qubo' :: Formula -> ((Formula, Integer), PB2QUBOInfo') Source #

type PB2QUBOInfo' = ComposedTransformer PBUnconstrainInfo PBQuadratizeInfo Source #

General data types

data PBIdentityInfo Source #

Constructors

PBIdentityInfo

Instances

Instances details

FromJSON PBIdentityInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods parseJSON :: Value -> Parser PBIdentityInfo # parseJSONList :: Value -> Parser [PBIdentityInfo] # omittedField :: Maybe PBIdentityInfo #
ToJSON PBIdentityInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods toJSON :: PBIdentityInfo -> Value # toEncoding :: PBIdentityInfo -> Encoding # toJSONList :: [PBIdentityInfo] -> Value # toEncodingList :: [PBIdentityInfo] -> Encoding # omitField :: PBIdentityInfo -> Bool #
Show PBIdentityInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods showsPrec :: Int -> PBIdentityInfo -> ShowS # show :: PBIdentityInfo -> String # showList :: [PBIdentityInfo] -> ShowS #
Eq PBIdentityInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods (==) :: PBIdentityInfo -> PBIdentityInfo -> Bool # (/=) :: PBIdentityInfo -> PBIdentityInfo -> Bool #
BackwardTransformer PBIdentityInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformBackward :: PBIdentityInfo -> Target PBIdentityInfo -> Source PBIdentityInfo Source #
ForwardTransformer PBIdentityInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformForward :: PBIdentityInfo -> Source PBIdentityInfo -> Target PBIdentityInfo Source #
ObjValueBackwardTransformer PBIdentityInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueBackward :: PBIdentityInfo -> TargetObjValue PBIdentityInfo -> SourceObjValue PBIdentityInfo Source #
ObjValueForwardTransformer PBIdentityInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueForward :: PBIdentityInfo -> SourceObjValue PBIdentityInfo -> TargetObjValue PBIdentityInfo Source #
ObjValueTransformer PBIdentityInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type SourceObjValue PBIdentityInfo Source # type TargetObjValue PBIdentityInfo Source #
Transformer PBIdentityInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type Source PBIdentityInfo Source # type Target PBIdentityInfo Source #
type Source PBIdentityInfo Source #
Instance details Defined in ToySolver.Converter.PB type Source PBIdentityInfo = Model
type SourceObjValue PBIdentityInfo Source #
Instance details Defined in ToySolver.Converter.PB type SourceObjValue PBIdentityInfo = Integer
type Target PBIdentityInfo Source #
Instance details Defined in ToySolver.Converter.PB type Target PBIdentityInfo = Model
type TargetObjValue PBIdentityInfo Source #
Instance details Defined in ToySolver.Converter.PB type TargetObjValue PBIdentityInfo = Integer

newtype PBTseitinInfo Source #

Constructors

PBTseitinInfo TseitinInfo

Instances

Instances details

FromJSON PBTseitinInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods parseJSON :: Value -> Parser PBTseitinInfo # parseJSONList :: Value -> Parser [PBTseitinInfo] # omittedField :: Maybe PBTseitinInfo #
ToJSON PBTseitinInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods toJSON :: PBTseitinInfo -> Value # toEncoding :: PBTseitinInfo -> Encoding # toJSONList :: [PBTseitinInfo] -> Value # toEncodingList :: [PBTseitinInfo] -> Encoding # omitField :: PBTseitinInfo -> Bool #
Show PBTseitinInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods showsPrec :: Int -> PBTseitinInfo -> ShowS # show :: PBTseitinInfo -> String # showList :: [PBTseitinInfo] -> ShowS #
Eq PBTseitinInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods (==) :: PBTseitinInfo -> PBTseitinInfo -> Bool # (/=) :: PBTseitinInfo -> PBTseitinInfo -> Bool #
BackwardTransformer PBTseitinInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformBackward :: PBTseitinInfo -> Target PBTseitinInfo -> Source PBTseitinInfo Source #
ForwardTransformer PBTseitinInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformForward :: PBTseitinInfo -> Source PBTseitinInfo -> Target PBTseitinInfo Source #
ObjValueBackwardTransformer PBTseitinInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueBackward :: PBTseitinInfo -> TargetObjValue PBTseitinInfo -> SourceObjValue PBTseitinInfo Source #
ObjValueForwardTransformer PBTseitinInfo Source #
Instance details Defined in ToySolver.Converter.PB Methods transformObjValueForward :: PBTseitinInfo -> SourceObjValue PBTseitinInfo -> TargetObjValue PBTseitinInfo Source #
ObjValueTransformer PBTseitinInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type SourceObjValue PBTseitinInfo Source # type TargetObjValue PBTseitinInfo Source #
Transformer PBTseitinInfo Source #
Instance details Defined in ToySolver.Converter.PB Associated Types type Source PBTseitinInfo Source # type Target PBTseitinInfo Source #
type Source PBTseitinInfo Source #
Instance details Defined in ToySolver.Converter.PB type Source PBTseitinInfo = Model
type SourceObjValue PBTseitinInfo Source #
Instance details Defined in ToySolver.Converter.PB type SourceObjValue PBTseitinInfo = Integer
type Target PBTseitinInfo Source #
Instance details Defined in ToySolver.Converter.PB type Target PBTseitinInfo = Model
type TargetObjValue PBTseitinInfo Source #
Instance details Defined in ToySolver.Converter.PB type TargetObjValue PBTseitinInfo = Integer

misc

pb2lsp :: Formula -> Builder Source #

wbo2lsp :: SoftFormula -> Builder Source #

pb2smp :: Bool -> Formula -> Builder Source #