ToySolver.Converter.MIP2SMT

Documentation

mip2smt :: Options -> Problem Rational -> Builder

data Options

Translation options.

The default option can be obtained by def.

Constructors

Options

Fields

• optLanguage :: Language
• optSetLogic :: Maybe String
• optCheckSAT :: Bool
• optProduceModel :: Bool
• optOptimize :: Bool

Instances

Eq Options

Defined in ToySolver.Converter.MIP2SMT

Methods

(==) :: Options -> Options -> Bool

(/=) :: Options -> Options -> Bool

Ord Options

Defined in ToySolver.Converter.MIP2SMT

Methods

compare :: Options -> Options -> Ordering

(<) :: Options -> Options -> Bool

(<=) :: Options -> Options -> Bool

(>) :: Options -> Options -> Bool

(>=) :: Options -> Options -> Bool

max :: Options -> Options -> Options

min :: Options -> Options -> Options

Show Options

Defined in ToySolver.Converter.MIP2SMT

Methods

showsPrec :: Int -> Options -> ShowS

show :: Options -> String

showList :: [Options] -> ShowS

Default Options

Defined in ToySolver.Converter.MIP2SMT

Methods

def :: Options

data Language

Constructors

SMTLIB2

YICES YicesVersion

Instances

Eq Language

Defined in ToySolver.Converter.MIP2SMT

Methods

(==) :: Language -> Language -> Bool

(/=) :: Language -> Language -> Bool

Ord Language

Defined in ToySolver.Converter.MIP2SMT

Methods

compare :: Language -> Language -> Ordering

(<) :: Language -> Language -> Bool

(<=) :: Language -> Language -> Bool

(>) :: Language -> Language -> Bool

(>=) :: Language -> Language -> Bool

max :: Language -> Language -> Language

min :: Language -> Language -> Language

Show Language

Defined in ToySolver.Converter.MIP2SMT

Methods

showsPrec :: Int -> Language -> ShowS

show :: Language -> String

showList :: [Language] -> ShowS

data YicesVersion

Constructors

Yices1

Yices2

Instances

Bounded YicesVersion

Defined in ToySolver.Converter.MIP2SMT

Methods

minBound :: YicesVersion

maxBound :: YicesVersion

Enum YicesVersion

Defined in ToySolver.Converter.MIP2SMT

Methods

succ :: YicesVersion -> YicesVersion

pred :: YicesVersion -> YicesVersion

toEnum :: Int -> YicesVersion

fromEnum :: YicesVersion -> Int

enumFrom :: YicesVersion -> [YicesVersion]

enumFromThen :: YicesVersion -> YicesVersion -> [YicesVersion]

enumFromTo :: YicesVersion -> YicesVersion -> [YicesVersion]

enumFromThenTo :: YicesVersion -> YicesVersion -> YicesVersion -> [YicesVersion]

Eq YicesVersion

Defined in ToySolver.Converter.MIP2SMT

Methods

(==) :: YicesVersion -> YicesVersion -> Bool

(/=) :: YicesVersion -> YicesVersion -> Bool

Ord YicesVersion

Defined in ToySolver.Converter.MIP2SMT

Methods

compare :: YicesVersion -> YicesVersion -> Ordering

(<) :: YicesVersion -> YicesVersion -> Bool

(<=) :: YicesVersion -> YicesVersion -> Bool

(>) :: YicesVersion -> YicesVersion -> Bool

(>=) :: YicesVersion -> YicesVersion -> Bool

max :: YicesVersion -> YicesVersion -> YicesVersion

min :: YicesVersion -> YicesVersion -> YicesVersion

Show YicesVersion

Defined in ToySolver.Converter.MIP2SMT

Methods

showsPrec :: Int -> YicesVersion -> ShowS

show :: YicesVersion -> String

showList :: [YicesVersion] -> ShowS