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

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

ToySolver.Converter.MIP2SMT

Description

Synopsis

Documentation

convert :: Options -> Problem Rational -> Builder Source #

data Options Source #

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 Source #
Methods (==) :: Options -> Options -> Bool # (/=) :: Options -> Options -> Bool #
Ord Options Source #
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 Source #
Methods showsPrec :: Int -> Options -> ShowS # show :: Options -> String # showList :: [Options] -> ShowS #
Default Options Source #
Methods def :: Options #

data Language Source #

Constructors

SMTLIB2
YICES YicesVersion

Instances

Eq Language Source #
Methods (==) :: Language -> Language -> Bool # (/=) :: Language -> Language -> Bool #
Ord Language Source #
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 Source #
Methods showsPrec :: Int -> Language -> ShowS # show :: Language -> String # showList :: [Language] -> ShowS #

data YicesVersion Source #

Constructors

Yices1
Yices2

Instances

Bounded YicesVersion Source #
Methods minBound :: YicesVersion # maxBound :: YicesVersion #
Enum YicesVersion Source #
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 Source #
Methods (==) :: YicesVersion -> YicesVersion -> Bool # (/=) :: YicesVersion -> YicesVersion -> Bool #
Ord YicesVersion Source #
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 Source #
Methods showsPrec :: Int -> YicesVersion -> ShowS # show :: YicesVersion -> String # showList :: [YicesVersion] -> ShowS #