toysolver-0.9.0: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
Copyright(c) Masahiro Sakai 2011-2016
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010
Extensions
  • Cpp
  • MonoLocalBinds
  • ScopedTypeVariables
  • TypeFamilies
  • OverloadedStrings
  • ConstrainedClassMethods
  • MultiParamTypeClasses
  • KindSignatures
  • ExplicitNamespaces
  • ExplicitForAll

ToySolver.Converter.MIP

Description

 
Synopsis

PB/WBO to IP

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

data PB2IPInfo Source #

Instances

Instances details
FromJSON PB2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

parseJSON :: Value -> Parser PB2IPInfo #

parseJSONList :: Value -> Parser [PB2IPInfo] #

omittedField :: Maybe PB2IPInfo #

ToJSON PB2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

toJSON :: PB2IPInfo -> Value #

toEncoding :: PB2IPInfo -> Encoding #

toJSONList :: [PB2IPInfo] -> Value #

toEncodingList :: [PB2IPInfo] -> Encoding #

omitField :: PB2IPInfo -> Bool #

Read PB2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

readsPrec :: Int -> ReadS PB2IPInfo #

readList :: ReadS [PB2IPInfo] #

readPrec :: ReadPrec PB2IPInfo #

readListPrec :: ReadPrec [PB2IPInfo] #

Show PB2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

showsPrec :: Int -> PB2IPInfo -> ShowS #

show :: PB2IPInfo -> String #

showList :: [PB2IPInfo] -> ShowS #

Eq PB2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

(==) :: PB2IPInfo -> PB2IPInfo -> Bool #

(/=) :: PB2IPInfo -> PB2IPInfo -> Bool #

BackwardTransformer PB2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

transformBackward :: PB2IPInfo -> Target PB2IPInfo -> Source PB2IPInfo Source #

ForwardTransformer PB2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

transformForward :: PB2IPInfo -> Source PB2IPInfo -> Target PB2IPInfo Source #

ObjValueBackwardTransformer PB2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

transformObjValueBackward :: PB2IPInfo -> TargetObjValue PB2IPInfo -> SourceObjValue PB2IPInfo Source #

ObjValueForwardTransformer PB2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

transformObjValueForward :: PB2IPInfo -> SourceObjValue PB2IPInfo -> TargetObjValue PB2IPInfo Source #

ObjValueTransformer PB2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Associated Types

type SourceObjValue PB2IPInfo Source #

type TargetObjValue PB2IPInfo Source #

Transformer PB2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Associated Types

type Source PB2IPInfo Source #

type Target PB2IPInfo Source #

type Source PB2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

type Source PB2IPInfo = Model
type SourceObjValue PB2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

type SourceObjValue PB2IPInfo = Integer
type Target PB2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

type Target PB2IPInfo = Map Var Rational
type TargetObjValue PB2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

type TargetObjValue PB2IPInfo = Rational

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

data WBO2IPInfo Source #

Instances

Instances details
FromJSON WBO2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

parseJSON :: Value -> Parser WBO2IPInfo #

parseJSONList :: Value -> Parser [WBO2IPInfo] #

omittedField :: Maybe WBO2IPInfo #

ToJSON WBO2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

toJSON :: WBO2IPInfo -> Value #

toEncoding :: WBO2IPInfo -> Encoding #

toJSONList :: [WBO2IPInfo] -> Value #

toEncodingList :: [WBO2IPInfo] -> Encoding #

omitField :: WBO2IPInfo -> Bool #

Show WBO2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

showsPrec :: Int -> WBO2IPInfo -> ShowS #

show :: WBO2IPInfo -> String #

showList :: [WBO2IPInfo] -> ShowS #

Eq WBO2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

(==) :: WBO2IPInfo -> WBO2IPInfo -> Bool #

(/=) :: WBO2IPInfo -> WBO2IPInfo -> Bool #

BackwardTransformer WBO2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

transformBackward :: WBO2IPInfo -> Target WBO2IPInfo -> Source WBO2IPInfo Source #

ForwardTransformer WBO2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

transformForward :: WBO2IPInfo -> Source WBO2IPInfo -> Target WBO2IPInfo Source #

ObjValueBackwardTransformer WBO2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

transformObjValueBackward :: WBO2IPInfo -> TargetObjValue WBO2IPInfo -> SourceObjValue WBO2IPInfo Source #

ObjValueForwardTransformer WBO2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

transformObjValueForward :: WBO2IPInfo -> SourceObjValue WBO2IPInfo -> TargetObjValue WBO2IPInfo Source #

ObjValueTransformer WBO2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Associated Types

type SourceObjValue WBO2IPInfo Source #

type TargetObjValue WBO2IPInfo Source #

Transformer WBO2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Associated Types

type Source WBO2IPInfo Source #

type Target WBO2IPInfo Source #

type Source WBO2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

type Source WBO2IPInfo = Model
type SourceObjValue WBO2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

type SourceObjValue WBO2IPInfo = Integer
type Target WBO2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

type Target WBO2IPInfo = Map Var Rational
type TargetObjValue WBO2IPInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

type TargetObjValue WBO2IPInfo = Rational

SAT/Max-SAT to IP

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 #

IP to PB

ip2pb :: Problem Rational -> Either String (Formula, IP2PBInfo) Source #

data IP2PBInfo Source #

Constructors

IP2PBInfo (Map Var Expr) (Map Var Lit) !Integer 

Instances

Instances details
FromJSON IP2PBInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

parseJSON :: Value -> Parser IP2PBInfo #

parseJSONList :: Value -> Parser [IP2PBInfo] #

omittedField :: Maybe IP2PBInfo #

ToJSON IP2PBInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

toJSON :: IP2PBInfo -> Value #

toEncoding :: IP2PBInfo -> Encoding #

toJSONList :: [IP2PBInfo] -> Value #

toEncodingList :: [IP2PBInfo] -> Encoding #

omitField :: IP2PBInfo -> Bool #

Show IP2PBInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

showsPrec :: Int -> IP2PBInfo -> ShowS #

show :: IP2PBInfo -> String #

showList :: [IP2PBInfo] -> ShowS #

Eq IP2PBInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

(==) :: IP2PBInfo -> IP2PBInfo -> Bool #

(/=) :: IP2PBInfo -> IP2PBInfo -> Bool #

BackwardTransformer IP2PBInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

transformBackward :: IP2PBInfo -> Target IP2PBInfo -> Source IP2PBInfo Source #

ForwardTransformer IP2PBInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

transformForward :: IP2PBInfo -> Source IP2PBInfo -> Target IP2PBInfo Source #

ObjValueBackwardTransformer IP2PBInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

transformObjValueBackward :: IP2PBInfo -> TargetObjValue IP2PBInfo -> SourceObjValue IP2PBInfo Source #

ObjValueForwardTransformer IP2PBInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Methods

transformObjValueForward :: IP2PBInfo -> SourceObjValue IP2PBInfo -> TargetObjValue IP2PBInfo Source #

ObjValueTransformer IP2PBInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Associated Types

type SourceObjValue IP2PBInfo Source #

type TargetObjValue IP2PBInfo Source #

Transformer IP2PBInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

Associated Types

type Source IP2PBInfo Source #

type Target IP2PBInfo Source #

type Source IP2PBInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

type Source IP2PBInfo = Map Var Rational
type SourceObjValue IP2PBInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

type SourceObjValue IP2PBInfo = Rational
type Target IP2PBInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

type Target IP2PBInfo = Model
type TargetObjValue IP2PBInfo Source # 
Instance details

Defined in ToySolver.Converter.MIP

type TargetObjValue IP2PBInfo = Integer

addMIP :: (AddPBNL m enc, PrimMonad m) => enc -> Problem Rational -> m (Either String (Expr, IP2PBInfo)) Source #