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

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

ToySolver.Converter.SAT2KSAT

Description

Documentation

sat2ksat :: Int -> CNF -> (CNF, SAT2KSATInfo) Source #

data SAT2KSATInfo Source #

Constructors

SAT2KSATInfo !Int !Int (Seq (Var, [Lit]))

Instances

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