toysolver-0.7.0: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
Copyright(c) Masahiro Sakai 2016
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010
Extensions
  • MonoLocalBinds
  • TypeFamilies
  • FlexibleContexts
  • ConstrainedClassMethods
  • MultiParamTypeClasses
  • KindSignatures
  • ExplicitNamespaces

ToySolver.Converter.SAT2KSAT

Description

 

Documentation

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

data SAT2KSATInfo Source #

Constructors

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

Instances

Instances details
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 Source #

type Target SAT2KSATInfo 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