toysolver-0.6.0: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc

Copyright	(c) Masahiro Sakai 2011-2015
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

ToySolver.Converter.PB2IP

Description

Documentation

pb2ip :: Formula -> (Problem Integer, PB2IPInfo) Source #

data PB2IPInfo Source #

Instances

Eq PB2IPInfo Source #
Instance details Defined in ToySolver.Converter.PB2IP Methods (==) :: PB2IPInfo -> PB2IPInfo -> Bool # (/=) :: PB2IPInfo -> PB2IPInfo -> Bool #
Read PB2IPInfo Source #
Instance details Defined in ToySolver.Converter.PB2IP Methods readsPrec :: Int -> ReadS PB2IPInfo # readList :: ReadS [PB2IPInfo] # readPrec :: ReadPrec PB2IPInfo # readListPrec :: ReadPrec [PB2IPInfo] #
Show PB2IPInfo Source #
Instance details Defined in ToySolver.Converter.PB2IP Methods showsPrec :: Int -> PB2IPInfo -> ShowS # show :: PB2IPInfo -> String # showList :: [PB2IPInfo] -> ShowS #
BackwardTransformer PB2IPInfo Source #
Instance details Defined in ToySolver.Converter.PB2IP Methods transformBackward :: PB2IPInfo -> Target PB2IPInfo -> Source PB2IPInfo Source #
ForwardTransformer PB2IPInfo Source #
Instance details Defined in ToySolver.Converter.PB2IP Methods transformForward :: PB2IPInfo -> Source PB2IPInfo -> Target PB2IPInfo Source #
Transformer PB2IPInfo Source #
Instance details Defined in ToySolver.Converter.PB2IP Associated Types type Source PB2IPInfo :: Type Source # type Target PB2IPInfo :: Type Source #
type Source PB2IPInfo Source #
Instance details Defined in ToySolver.Converter.PB2IP type Source PB2IPInfo = Model
type Target PB2IPInfo Source #
Instance details Defined in ToySolver.Converter.PB2IP type Target PB2IPInfo = Map Var Rational

wbo2ip :: Bool -> SoftFormula -> (Problem Integer, WBO2IPInfo) Source #

data WBO2IPInfo Source #

Instances

Eq WBO2IPInfo Source #
Instance details Defined in ToySolver.Converter.PB2IP Methods (==) :: WBO2IPInfo -> WBO2IPInfo -> Bool # (/=) :: WBO2IPInfo -> WBO2IPInfo -> Bool #
Show WBO2IPInfo Source #
Instance details Defined in ToySolver.Converter.PB2IP Methods showsPrec :: Int -> WBO2IPInfo -> ShowS # show :: WBO2IPInfo -> String # showList :: [WBO2IPInfo] -> ShowS #
BackwardTransformer WBO2IPInfo Source #
Instance details Defined in ToySolver.Converter.PB2IP Methods transformBackward :: WBO2IPInfo -> Target WBO2IPInfo -> Source WBO2IPInfo Source #
ForwardTransformer WBO2IPInfo Source #
Instance details Defined in ToySolver.Converter.PB2IP Methods transformForward :: WBO2IPInfo -> Source WBO2IPInfo -> Target WBO2IPInfo Source #
Transformer WBO2IPInfo Source #
Instance details Defined in ToySolver.Converter.PB2IP Associated Types type Source WBO2IPInfo :: Type Source # type Target WBO2IPInfo :: Type Source #
type Source WBO2IPInfo Source #
Instance details Defined in ToySolver.Converter.PB2IP type Source WBO2IPInfo = Model
type Target WBO2IPInfo Source #
Instance details Defined in ToySolver.Converter.PB2IP type Target WBO2IPInfo = Map Var Rational

sat2ip :: CNF -> (Problem Integer, SAT2IPInfo) Source #

type SAT2IPInfo = ComposedTransformer SAT2PBInfo PB2IPInfo Source #

maxsat2ip :: Bool -> WCNF -> (Problem Integer, MaxSAT2IPInfo) Source #

type MaxSAT2IPInfo = ComposedTransformer MaxSAT2WBOInfo WBO2IPInfo Source #