toysolver.cabal

cabal-version: 3.0
Name:		toysolver
Version:	0.9.0
License:	BSD-3-Clause
License-File:	COPYING
Author:		Masahiro Sakai (masahiro.sakai@gmail.com)
Maintainer:	masahiro.sakai@gmail.com
Category:	Algorithms, Optimisation, Optimization, Theorem Provers, Constraints, Logic, Formal Methods, SMT
Synopsis:	Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
Description:	Toy-level solver implementation of various problems including SAT, SMT, Max-SAT, PBS/PBO (Pseudo Boolean Satisfaction/Optimization), MILP (Mixed Integer Linear Programming) and non-linear real arithmetic.
Homepage:	https://github.com/msakai/toysolver/
Bug-Reports:	https://github.com/msakai/toysolver/issues
Tested-With:
   GHC ==9.2.8
   GHC ==9.4.8
   GHC ==9.6.6
   GHC ==9.8.4
   GHC ==9.10.1
Extra-Doc-Files:
   README.md
   INSTALL.md
   CHANGELOG.markdown
   COPYING
   COPYING-GPL
Extra-Source-Files:
   app/toysat-ipasir/ipasir.h
   app/toysat-ipasir/ipasir.map
   src/ToySolver/Data/Polyhedron.hs
   samples/gcnf/*.cnf
   samples/gcnf/*.gcnf
   samples/lp/*.lp
   samples/lp/*.sol
   samples/lp/*.txt
   samples/lp/error/*.lp
   samples/maxsat/*.cnf
   samples/maxsat/*.wcnf
   samples/mps/*.mps
   samples/pbo/*.opb
   samples/pbs/*.opb
   samples/sat/*.cnf
   samples/wbo/*.wbo
   samples/sdp/*.dat
   samples/sdp/*.dat-s
   samples/smt/*.smt2
   samples/smt/*.ys
   samples/qbf/*.qdimacs
   samples/programs/sudoku/*.sdk
   samples/programs/knapsack/README.md
   samples/programs/knapsack/*.txt
   samples/programs/htc/test1.dat
   samples/programs/htc/test2.dat
   samples/programs/svm2lp/a1a
   samples/programs/nonogram/*.cwd
   samples/programs/nonogram/README.md
   samples/programs/numberlink/README.md
   samples/programs/numberlink/ADC2013/*.txt
   samples/programs/numberlink/ADC2014_QA/A/*.txt
   samples/programs/numberlink/ADC2014_QA/Q/*.txt
   samples/programs/numberlink/ADC2016/sample/01/*.txt
   benchmarks/UF250.1065.100/*.cnf
   benchmarks/UUF250.1065.100/*.cnf
Build-Type: Simple

Flag ForceChar8
  Description: set default encoding to char8 (not to use iconv)
  Default: False
  Manual: True

Flag LinuxStatic
  Description: build statically linked binaries
  Default: False
  Manual: True

Flag WithZlib
  Description: Use zlib package to support gzipped files
  Default: True
  Manual: True

Flag BuildToyFMF
  Description: build toyfmf command
  Default: False
  Manual: True

Flag BuildForeignLibraries
  Description: build foreign libraries
  Default: True
  Manual: True  

Flag BuildSamplePrograms
  Description: build sample programs
  Default: False
  Manual: True

Flag BuildMiscPrograms
  Description: build misc programs
  Default: False
  Manual: True

Flag UseHaskeline
  Description: use haskeline package
  Manual: True
  Default: True

Flag OpenCL
  Description: use opencl package (deprecated)
  Manual: True
  Default: False

Flag ExtraBoundsChecking
  Description: enable extra bounds checking for debugging
  Manual: True
  Default: False

Flag optparse-applicative-018
  Description: use optparse-applicative >=0.18
  Manual: False
  Default: False

source-repository head
  type:     git
  location: git://github.com/msakai/toysolver.git

Common common-options
  Default-Language: Haskell2010
  GHC-Options: -rtsopts
  -- GHC-Prof-Options: -auto-all
  Build-Depends:
     -- GHC >=9.2 && <9.13
     base >=4.16 && <4.22

Common exe-options
  Import: common-options
  if flag(ForceChar8)
    CPP-OPtions: "-DFORCE_CHAR8"
  if flag(LinuxStatic)
    GHC-Options: -static -optl-static -optl-pthread
  Other-Extensions: CPP

Library
  Import: common-options
  Exposed: True
  Hs-source-dirs: src
  Build-Depends:
     aeson >=1.4.2.0 && <2.3,
     array >=0.5,
     bytestring >=0.9.2.1 && <0.13,
     bytestring-builder,
     bytestring-encoding >=0.1.1.0,
     case-insensitive,
     clock >=0.7.1,
     -- IntMap.restrictKeys and IntMap.withoutKeys require containers >=0.5.8
     containers >=0.5.8,
     data-default,
     data-default-class,
     data-interval >=2.0.1 && <2.2.0,
     deepseq,
     directory,
     extended-reals >=0.1 && <1.0,
     filepath,
     finite-field >=0.9.0 && <1.0.0,
     -- hashUsing is available on hashable >=1.2
     hashable >=1.2 && <1.6.0.0,
     hashtables,
     heaps,
     intern >=0.9.1.2 && <1.0.0.0,
     log-domain,
     -- numLoopState requires loop >=0.3.0
     loop >=0.3.0 && < 1.0.0,
     MIP >=0.2.0.0 && <0.3,
     mtl >=2.1.2,
     multiset,
     -- createSystemRandom requires mwc-random >=0.13.1.0
     mwc-random >=0.13.1 && <0.16,
     OptDir,
     lattices,
     megaparsec >=7 && <10,
     -- Text.PrettyPrint.HughesPJClass is available on pretty >=1.1.2.0
     pretty >=1.1.2.0 && <1.2,
     primes,
     primitive >=0.6,
     process >=1.1.0.2,
     pseudo-boolean >=0.1.3.0 && <0.2.0.0,
     queue,
     scientific,
     semigroups >=0.17,
     sign >=0.2.0 && <1.0.0,
     stm >=2.3,
     template-haskell,
     temporary >=1.2,
     text >=1.1.0.0,
     -- defaultTimeLocale is available on time >=1.5.0
     time >=1.5.0,
     transformers >=0.2,
     transformers-compat >=0.3,
     unordered-containers >=0.2.3 && <0.3.0,
     -- imapM and modify are available on vector >=0.11.0
     vector >=0.11,
     vector-space >=0.8.6,
     xml-conduit
  if flag(WithZlib)
     Build-Depends: zlib
     CPP-Options: "-DWITH_ZLIB"
  if flag(ExtraBoundsChecking)
     CPP-Options: "-DEXTRA_BOUNDS_CHECKING"
  if impl(ghc)
     Build-Depends: ghc-prim
  Other-Extensions:
     BangPatterns
     CPP
     ConstraintKinds
     DeriveDataTypeable
     DeriveGeneric
     ExistentialQuantification
     FlexibleContexts
     FlexibleInstances
     FunctionalDependencies
     GADTs
     GeneralizedNewtypeDeriving
     InstanceSigs
     KindSignatures
     MultiParamTypeClasses
     OverloadedStrings
     PatternSynonyms
     Rank2Types
     RecursiveDo
     ScopedTypeVariables
     TemplateHaskell
     TypeFamilies
     TypeOperators
     TypeSynonymInstances
     UndecidableInstances
     ViewPatterns
  if impl(ghc)
     Other-Extensions:
        MagicHash
        UnboxedTuples
  Exposed-Modules:
     ToySolver.Arith.BoundsInference
     ToySolver.Arith.CAD
     ToySolver.Arith.ContiTraverso
     ToySolver.Arith.Cooper
     ToySolver.Arith.Cooper.Base
     ToySolver.Arith.Cooper.FOL
     ToySolver.Arith.DifferenceLogic
     ToySolver.Arith.FourierMotzkin
     ToySolver.Arith.FourierMotzkin.Base
     ToySolver.Arith.FourierMotzkin.FOL
     ToySolver.Arith.FourierMotzkin.Optimization
     ToySolver.Arith.LPUtil
     ToySolver.Arith.MIP
     ToySolver.Arith.OmegaTest
     ToySolver.Arith.OmegaTest.Base
     ToySolver.Arith.Simplex
     ToySolver.Arith.Simplex.Simple
     ToySolver.Arith.Simplex.Textbook
     ToySolver.Arith.Simplex.Textbook.LPSolver
     ToySolver.Arith.Simplex.Textbook.LPSolver.Simple
     ToySolver.Arith.Simplex.Textbook.MIPSolver.Simple
     ToySolver.Arith.VirtualSubstitution
     ToySolver.BitVector
     ToySolver.BitVector.Base
     ToySolver.BitVector.Solver
     ToySolver.EUF.CongruenceClosure
     ToySolver.EUF.EUFSolver
     ToySolver.EUF.FiniteModelFinder
     ToySolver.Combinatorial.BipartiteMatching
     ToySolver.Combinatorial.HittingSet.DAA
     ToySolver.Combinatorial.HittingSet.MARCO
     ToySolver.Combinatorial.HittingSet.Simple
     ToySolver.Combinatorial.HittingSet.HTCBDD
     ToySolver.Combinatorial.HittingSet.InterestingSets
     ToySolver.Combinatorial.HittingSet.SHD
     ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
     ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999
     ToySolver.Combinatorial.HittingSet.Util
     ToySolver.Combinatorial.Knapsack.BB
     ToySolver.Combinatorial.Knapsack.DPDense
     ToySolver.Combinatorial.Knapsack.DPSparse
     ToySolver.Combinatorial.SubsetSum
     ToySolver.Converter
     ToySolver.Converter.Base
     ToySolver.Converter.GCNF2MaxSAT
     ToySolver.Converter.MIP2SMT
     ToySolver.Converter.NAESAT
     ToySolver.Converter.PB
     ToySolver.Converter.MIP
     ToySolver.Converter.QBF2IPC
     ToySolver.Converter.QUBO
     ToySolver.Converter.SAT2MIS
     ToySolver.Converter.SAT2KSAT
     ToySolver.Converter.SAT2MaxCut
     ToySolver.Converter.SAT2MaxSAT
     ToySolver.Converter.Tseitin
     ToySolver.Data.AlgebraicNumber.Complex
     ToySolver.Data.AlgebraicNumber.Real
     ToySolver.Data.AlgebraicNumber.Root
     ToySolver.Data.AlgebraicNumber.Sturm
     ToySolver.Data.Boolean
     ToySolver.Data.BoolExpr
     ToySolver.Data.Delta
     ToySolver.Data.DNF
     ToySolver.Data.FOL.Arith
     ToySolver.Data.FOL.Formula
     ToySolver.Data.IntVar
     ToySolver.Data.LA
     ToySolver.Data.LA.FOL
     ToySolver.Data.LBool
     ToySolver.Data.OrdRel
     ToySolver.Data.Polynomial
     ToySolver.Data.Polynomial.Factorization.FiniteField
     ToySolver.Data.Polynomial.Factorization.Hensel
     ToySolver.Data.Polynomial.Factorization.Hensel.Internal
     ToySolver.Data.Polynomial.Factorization.Integer
     ToySolver.Data.Polynomial.Factorization.Kronecker
     ToySolver.Data.Polynomial.Factorization.Rational
     ToySolver.Data.Polynomial.Factorization.SquareFree
     ToySolver.Data.Polynomial.Factorization.Zassenhaus
     ToySolver.Data.Polynomial.GroebnerBasis
     ToySolver.Data.Polynomial.Interpolation.Hermite
     ToySolver.Data.Polynomial.Interpolation.Lagrange
     ToySolver.FileFormat
     ToySolver.FileFormat.Base
     ToySolver.FileFormat.CNF
     ToySolver.Graph.Base
     ToySolver.Graph.ShortestPath
     ToySolver.Graph.MaxCut
     ToySolver.QBF
     ToySolver.QUBO
     ToySolver.SAT
     ToySolver.SAT.Encoder.Integer
     ToySolver.SAT.Encoder.PB
     ToySolver.SAT.Encoder.PB.Internal.Adder
     ToySolver.SAT.Encoder.PB.Internal.BCCNF
     ToySolver.SAT.Encoder.PB.Internal.BDD
     ToySolver.SAT.Encoder.PB.Internal.Sorter
     ToySolver.SAT.Encoder.PBNLC
     ToySolver.SAT.Encoder.Cardinality
     ToySolver.SAT.Encoder.Cardinality.Internal.Naive
     ToySolver.SAT.Encoder.Cardinality.Internal.ParallelCounter
     ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer
     ToySolver.SAT.Encoder.Tseitin
     ToySolver.SAT.ExistentialQuantification
     ToySolver.SAT.Formula
     ToySolver.SAT.MUS
     ToySolver.SAT.MUS.Enum
     ToySolver.SAT.MUS.Types
     ToySolver.SAT.PBO
     ToySolver.SAT.PBO.Context
     ToySolver.SAT.PBO.BC
     ToySolver.SAT.PBO.BCD
     ToySolver.SAT.PBO.BCD2
     ToySolver.SAT.PBO.MSU4
     ToySolver.SAT.PBO.UnsatBased
     ToySolver.SAT.Solver.CDCL
     ToySolver.SAT.Solver.CDCL.Config
     ToySolver.SAT.Solver.MessagePassing.SurveyPropagation
     ToySolver.SAT.Solver.SLS.ProbSAT
     ToySolver.SAT.Solver.SLS.UBCSAT
     ToySolver.SAT.Store.CNF
     ToySolver.SAT.Store.PB
     ToySolver.SAT.TheorySolver
     ToySolver.SAT.Types
     ToySolver.SAT.Printer
     ToySolver.SDP
     ToySolver.SMT
     ToySolver.Text.SDPFile
     ToySolver.Internal.Data.IndexedPriorityQueue
     ToySolver.Internal.Data.IOURef
     ToySolver.Internal.Data.PriorityQueue
     ToySolver.Internal.Data.SeqQueue
     ToySolver.Internal.Data.Vec
     ToySolver.Internal.ProcessUtil
     ToySolver.Internal.TextUtil
     ToySolver.Internal.Util
     ToySolver.Wang
     ToySolver.Version
  Other-Modules:
     ToySolver.Converter.PB.Internal.LargestIntersectionFinder
     ToySolver.Converter.PB.Internal.Product
     ToySolver.Data.AlgebraicNumber.Graeffe
     ToySolver.Data.Polynomial.Base
     ToySolver.Internal.JSON
     ToySolver.SAT.Internal.JSON
     ToySolver.SAT.MUS.Base
     ToySolver.SAT.MUS.Deletion
     ToySolver.SAT.MUS.Insertion
     ToySolver.SAT.MUS.QuickXplain
     ToySolver.SAT.MUS.Enum.Base
     ToySolver.SAT.MUS.Enum.CAMUS
     ToySolver.Version.TH
     Paths_toysolver
  autogen-modules:
     Paths_toysolver

Executable toysolver
  Import: exe-options
  Main-is: toysolver.hs
  HS-Source-Dirs: app
  Build-Depends:
    array,
    containers,
    data-default-class,
    filepath,
    MIP,
    OptDir,
    -- maybeReader is available on optparse-applicative >=0.13.0.0
    optparse-applicative >=0.13,
    pseudo-boolean,
    scientific,
    toysolver
  GHC-Options: -threaded

Executable toysat
  Import: exe-options
  Main-is: toysat.hs
  HS-Source-Dirs: app/toysat
  Build-Depends:
    array,
    bytestring,
    containers,
    clock,
    data-default-class,
    filepath,
    megaparsec,
    MIP,
    mwc-random,
    -- maybeReader is available on optparse-applicative >=0.13.0.0
    optparse-applicative >=0.13,
    pseudo-boolean,
    scientific,
    time,
    toysolver,
    unbounded-delays,
    vector
  Other-Extensions: ScopedTypeVariables
  GHC-Options: -threaded
  if flag(WithZlib)
    CPP-Options: "-DWITH_ZLIB"

Foreign-Library     toysat-ipasir
  import:           common-options
  type:             native-shared
  if !flag(BuildForeignLibraries)
    buildable: False
  if os(Windows)
    options: standalone
    mod-def-file: app/toysat-ipasir/ipasir.def
  if os(Linux)
    ld-options: -Wl,--version-script=app/toysat-ipasir/ipasir.map
  build-depends:
    containers,
    toysolver
  hs-source-dirs:   app/toysat-ipasir
  include-dirs:     app/toysat-ipasir
  c-sources:        app/toysat-ipasir/cbits.c
  cc-options:       -Wall
  cpp-options:      -DIPASIR_SHARED_LIB -DBUILDING_IPASIR_SHARED_LIB
  includes:         ipasir.h
  other-modules:    IPASIR
  default-language: Haskell2010

Executable toysmt
  Import: exe-options
  HS-Source-Dirs: app/toysmt, Smtlib
  Main-is: toysmt.hs
  Other-Modules:
     ToySolver.SMT.SMTLIB2Solver,
     -- Following modules are copied from SmtLib package.
     -- http://hackage.haskell.org/package/SmtLib
     -- https://github.com/MfesGA/Smtlib
     Smtlib.Parsers.CommonParsers,
     Smtlib.Parsers.ResponseParsers,
     Smtlib.Parsers.CommandsParsers,
     Smtlib.Syntax.Syntax,
     Smtlib.Syntax.ShowSL
  Build-Depends:
    containers,
    -- TODO: remove intern dependency
    intern,
    mtl,
    optparse-applicative,
    parsec >=3.1.2 && <4,
    toysolver,
    text,
    transformers,
    transformers-compat
  if flag(UseHaskeline)
    Build-Depends: haskeline >=0.7 && <0.9
    CPP-Options: "-DUSE_HASKELINE_PACKAGE"
  Other-Extensions: ScopedTypeVariables

Executable toyqbf
  Import: exe-options
  Main-is: toyqbf.hs
  HS-Source-Dirs: app
  Build-Depends:
    containers,
    data-default-class,
    optparse-applicative,
    toysolver
  Other-Extensions: ScopedTypeVariables

Executable toyfmf
  Import: exe-options
  If !flag(BuildToyFMF)
    Buildable: False
  Main-is: toyfmf.hs
  HS-Source-Dirs: app
  If flag(BuildToyFMF)
    Build-Depends:
        containers,
      intern,
      logic-TPTP >=0.4.6.0 && <0.7,
      optparse-applicative,
      text,
      toysolver

-- Converters

Executable toyconvert
  Import: exe-options
  Main-is: toyconvert.hs
  HS-Source-Dirs: app
  Build-Depends:
    aeson,
    bytestring,
    bytestring-builder,
    containers,
    data-default-class,
    filepath,
    MIP,
    pseudo-boolean,
    scientific,
    text,
    toysolver
  if flag(optparse-applicative-018)
    Build-Depends:
      optparse-applicative >=0.18,
      prettyprinter >=1
  else
    Build-Depends:
      optparse-applicative <0.18,
      ansi-wl-pprint
  GHC-Options: -rtsopts
  if flag(WithZlib)
    CPP-Options: "-DWITH_ZLIB"

-- Sample Programs

Executable sudoku
  Import: exe-options
  If !flag(BuildSamplePrograms)
    Buildable: False
  Main-is: sudoku.hs
  HS-Source-Dirs: samples/programs/sudoku
  Build-Depends:
    array,
    toysolver

Executable nonogram
  Import: exe-options
  If !flag(BuildSamplePrograms)
    Buildable: False
  Main-is: nonogram.hs
  HS-Source-Dirs: samples/programs/nonogram
  Build-Depends:
    array,
    containers,
    toysolver

Executable nqueens
  Import: exe-options
  If !flag(BuildSamplePrograms)
    Buildable: False
  Main-is: nqueens.hs
  HS-Source-Dirs: samples/programs/nqueens
  Build-Depends:
    array,
    toysolver

Executable numberlink
  Import: exe-options
  If !flag(BuildSamplePrograms)
    Buildable: False
  Main-is: numberlink.hs
  HS-Source-Dirs: samples/programs/numberlink
  Build-Depends:
    array,
    bytestring,
    containers,
    data-default-class,
    parsec,
    pseudo-boolean,
    toysolver

Executable knapsack
  Import: exe-options
  If !flag(BuildSamplePrograms)
    Buildable: False
  Main-is: knapsack.hs
  HS-Source-Dirs: samples/programs/knapsack
  Build-Depends:
    toysolver

Executable assign
  Import: exe-options
  If !flag(BuildSamplePrograms)
    Buildable: False
  Main-is: assign.hs
  HS-Source-Dirs: samples/programs/assign
  Build-Depends:
    attoparsec,
    bytestring,
    containers,
    toysolver,
    vector

Executable shortest-path
  Import: exe-options
  If !flag(BuildSamplePrograms)
    Buildable: False
  Main-is: shortest-path.hs
  HS-Source-Dirs: samples/programs/shortest-path
  Build-Depends:
    bytestring,
    containers,
    unordered-containers,
    toysolver

Executable htc
  Import: exe-options
  If !flag(BuildSamplePrograms)
    Buildable: False
  Main-is: htc.hs
  HS-Source-Dirs: samples/programs/htc
  Build-Depends:
    containers,
    toysolver

Executable svm2lp
  Import: exe-options
  If !flag(BuildSamplePrograms)
    Buildable: False
  Main-is: svm2lp.hs
  HS-Source-Dirs: samples/programs/svm2lp
  Build-Depends:
    containers,
    data-default-class,
    MIP,
    scientific,
    split,
    text,
    toysolver

Executable survey-propagation
  Import: exe-options
  if !flag(BuildSamplePrograms)
    Buildable: False    
  Main-is: survey-propagation.hs
  HS-Source-Dirs: samples/programs/survey-propagation
  Build-Depends:
    data-default-class,
    toysolver
  GHC-Options: -rtsopts

Executable probsat
  Import: exe-options
  if !flag(BuildSamplePrograms)
    Buildable: False    
  Main-is: probsat.hs
  HS-Source-Dirs: samples/programs/probsat
  Build-Depends:
    clock,
    data-default-class,
    mwc-random,
    optparse-applicative,
    vector,
    toysolver

-- Misc Programs

Executable pigeonhole
  Import: exe-options
  If !flag(BuildMiscPrograms)
    Buildable: False
  Main-is: pigeonhole.hs
  HS-Source-Dirs: app
  Build-Depends:
    bytestring,
    containers,
    pseudo-boolean,
    toysolver

Executable maxsatverify
  Import: exe-options
  If !flag(BuildMiscPrograms)
    Buildable: False
  Main-is: maxsatverify.hs
  HS-Source-Dirs: app
  Build-Depends:
    array,
    toysolver

Executable pbverify
  Import: exe-options
  Main-is: pbverify.hs
  If !flag(BuildMiscPrograms)
    Buildable: False
  HS-Source-Dirs: app
  Build-Depends:
    array,
    pseudo-boolean,
    toysolver

-- Test suites and benchmarks

Test-suite TestPolynomial
  Import:            common-options
  Type:              exitcode-stdio-1.0
  HS-Source-Dirs:    test
  Main-is:           TestPolynomial.hs
  Build-depends:
    containers,
    data-interval,
    finite-field >=0.7.0 && <1.0.0,
    pretty,
    tasty >=0.10.1,
    tasty-hunit >=0.9 && <0.11,
    tasty-quickcheck >=0.8 && <0.12,
    tasty-th,
    toysolver
  Other-Extensions:
    DataKinds
    TemplateHaskell

Test-suite TestSuite
  Import:            common-options
  Type:              exitcode-stdio-1.0
  HS-Source-Dirs:    test Smtlib app/toysmt
  Main-is:           TestSuite.hs
  Other-Modules:
    Test.AReal
    Test.AReal2
    Test.Arith
    Test.BitVector
    Test.BoolExpr
    Test.BipartiteMatching
    Test.CNF
    Test.CongruenceClosure
    Test.ContiTraverso
    Test.Converter
    Test.Delta
    Test.FiniteModelFinder
    Test.Graph
    Test.GraphShortestPath
    Test.HittingSets
    Test.Knapsack
    Test.Misc
    Test.MIPSolver
    Test.ProbSAT
    Test.QBF
    Test.QUBO
    Test.SAT
    Test.SAT.Encoder
    Test.SAT.ExistentialQuantification
    Test.SAT.MUS
    Test.SAT.TheorySolver
    Test.SAT.Types
    Test.SAT.Utils
    Test.SDPFile
    Test.Simplex
    Test.SimplexTextbook
    Test.SMT
    Test.SMTLIB2Solver
    Test.Smtlib
    Test.SubsetSum
    ToySolver.SMT.SMTLIB2Solver
    Smtlib.Parsers.CommonParsers
    Smtlib.Parsers.ResponseParsers
    Smtlib.Parsers.CommandsParsers
    Smtlib.Syntax.Syntax
    Smtlib.Syntax.ShowSL
  Build-depends:
    aeson,
    array,
    bytestring,
    bytestring-builder,
    containers,
    data-default-class,
    data-interval,
    deepseq,
    hashable,
    intern,
    lattices,
    megaparsec,
    MIP,
    mtl,
    mwc-random,
    OptDir,
    parsec >=3.1.2 && <4,
    pseudo-boolean,
    -- sublistOf is available on QuickCheck >=2.8
    QuickCheck >=2.8 && <3,
    scientific,
    tasty >=0.10.1,
    tasty-hunit >=0.9 && <0.11,
    tasty-quickcheck >=0.8 && <0.12,
    tasty-th,
    text,
    toysolver,
    transformers,
    transformers-compat,
    unordered-containers,
    vector,
    vector-space
  Other-Extensions:
    CPP
    DataKinds
    FlexibleContexts
    LambdaCase
    ScopedTypeVariables
    TemplateHaskell
    TupleSections

Benchmark BenchmarkSATLIB
  Import:           common-options
  type:             exitcode-stdio-1.0
  hs-source-dirs:   benchmarks
  main-is:          BenchmarkSATLIB.hs
  build-depends:
    array,
    criterion >=1.0 && <1.7,
    data-default-class,
    toysolver

Benchmark BenchmarkKnapsack
  Import:           common-options
  type:             exitcode-stdio-1.0
  hs-source-dirs:   benchmarks
  main-is:          BenchmarkKnapsack.hs
  build-depends:
    criterion >=1.0 && <1.7,
    toysolver

Benchmark BenchmarkSubsetSum
  Import:           common-options
  type:             exitcode-stdio-1.0
  hs-source-dirs:   benchmarks
  main-is:          BenchmarkSubsetSum.hs
  build-depends:
    criterion >=1.0 && <1.7,
    toysolver,
    vector