Name:		toysolver
Version:	0.4.0
x-revision: 2
License:	BSD3
License-File:	COPYING
Author:		Masahiro Sakai (masahiro.sakai@gmail.com)
Maintainer:	masahiro.sakai@gmail.com
Category:	Algorithms, Optimisation, Optimization, Theorem Provers, Constraints, Logic
Cabal-Version:	>= 1.10
Synopsis:	Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc
Description:	Toy-level implementation of some decision procedures
Bug-Reports:	https://github.com/msakai/toysolver/issues
Tested-With:
   GHC ==7.6.3
   GHC ==7.8.3
   GHC ==7.10.3
Extra-Source-Files:
   README.md
   CHANGELOG.markdown
   COPYING
   COPYING-GPL
   .ghci
   .travis.yml
   appveyor.yml
   build_bdist_linux.sh
   build_bdist_macos.sh
   build_bdist_win32.sh
   build_bdist_win64.sh
   build_bdist_maxsat_evaluation.sh
   build_bdist_pb_evaluation.sh
   misc/maxsat/toysat/README.md
   misc/maxsat/toysat/toysat
   misc/maxsat/toysat_ls/README.md
   misc/maxsat/toysat_ls/toysat_ls
   misc/pb/README.md
   src/TseitinEncode.hs
   src/ToySolver/Data/Polyhedron.hs
   samples/gcnf/*.cnf
   samples/gcnf/*.gcnf
   samples/gcnf/edn_20403_8.cnf_0.03000000.unsat.gcnf
   samples/lp/*.lp
   samples/lp/error/*.lp
   samples/maxsat/*.cnf
   samples/maxsat/t3pm3-5555.spn.cnf
   samples/maxsat/*.wcnf
   samples/maxsat/ram_k3_n10.ra1.wcnf
   samples/mps/*.mps
   samples/pbo/*.opb
   samples/pbs/*.opb
   samples/pbs/normalized-1096.cudf.paranoid.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
   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 BuildToyFMF
  Description: build toyfmf command
  Default: False
  Manual: True

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

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

Flag Exceptions06
  Description: use exceptions >=0.6
  Manual: False

Flag Time15
  Description: use time >=1.5.0
  Manual: False

Flag Transformers051
  Description: use transformers >=0.5.1
  Manual: False

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

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

Library
  Exposed: True
  Hs-source-dirs: src
  Build-Depends:
     base >=4.6 && <4.11,
     template-haskell,
     -- IntMap.mergeWithKey and IntMap.toDescList require containers >=0.5.0
     containers >=0.5.0,
     unordered-containers >=0.2.3 && <0.3.0,
     transformers >=0.2,
     transformers-compat >=0.3,
     mtl >=2.1.2,
     array >=0.4.0.0,
     stm >=2.3,
     parsec >=3.1.2 && <4,
     bytestring >=0.9.2.1 && <0.11,
     bytestring-builder,
     filepath,
     deepseq,
     time,
     primes,
     process >=1.1.0.2,
     parse-dimacs,
     queue,
     heaps,
     vector,
     vector-space >=0.8.6,
     multiset,
     prettyclass >=1.0.0,
     type-level-numbers >=0.1.1.0 && <0.2.0.0,
     hashable >=1.1.2.5 && <1.3.0.0,
     intern >=0.9.1.2 && <1.0.0.0,
     loop >=0.2.0 && < 1.0.0,
     data-default-class,
     -- createSystemRandom requires mwc-random >=0.13.1.0
     mwc-random >=0.13.1 && <0.14,
     semigroups >=0.17,
     OptDir,
     extended-reals >=0.1 && <1.0,
     data-interval >=1.0.1 && <1.3.0,
     finite-field >=0.7.0 && <0.9.0,
     sign >=0.2.0 && <1.0.0,
     pseudo-boolean >=0.1.3.0 && <0.2.0.0
  -- NOTE: temporary-1.2.0.2 does not work with exceptions-0.6
  if flag(Exceptions06)
     Build-Depends: temporary >1.2.0.2, exceptions >=0.6
  else
     Build-Depends: temporary >=1.2, exceptions ==0.5
  if impl(ghc <7.7)
    Build-Depends:
      -- vector-space depends on MemoTrie, but MemoTrie >=0.6.3 uses extensions that are not available on GHC 7.6.
      MemoTrie <=0.6.2
  if flag(Transformers051)
     Build-Depends: transformers >=0.5.1.0
  else
     Build-Depends: transformers <0.5.1.0
  if impl(ghc)
     Build-Depends: ghc-prim
  Default-Language: Haskell2010
  Other-Extensions:
     BangPatterns
     CPP
     DeriveDataTypeable
     FlexibleContexts
     FlexibleInstances
     FunctionalDependencies
     GeneralizedNewtypeDeriving
     MultiParamTypeClasses
     OverloadedStrings
     RecursiveDo
     Rank2Types
     ScopedTypeVariables
     TemplateHaskell
     TypeFamilies
     TypeSynonymInstances
  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.FourierMotzkin
     ToySolver.Arith.FourierMotzkin.Base
     ToySolver.Arith.FourierMotzkin.FOL
     ToySolver.Arith.FourierMotzkin.Optimization
     ToySolver.Arith.LPSolver
     ToySolver.Arith.LPSolverHL
     ToySolver.Arith.LPUtil
     ToySolver.Arith.MIPSolverHL
     ToySolver.Arith.MIPSolver2
     ToySolver.Arith.OmegaTest
     ToySolver.Arith.OmegaTest.Base
     ToySolver.Arith.Simplex
     ToySolver.Arith.Simplex2
     ToySolver.Arith.VirtualSubstitution
     ToySolver.EUF.CongruenceClosure
     ToySolver.EUF.EUFSolver
     ToySolver.EUF.FiniteModelFinder
     ToySolver.Combinatorial.HittingSet.Simple
     ToySolver.Combinatorial.HittingSet.HTCBDD
     ToySolver.Combinatorial.HittingSet.SHD
     ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
     ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999
     ToySolver.Combinatorial.Knapsack.BB
     ToySolver.Combinatorial.Knapsack.DPDense
     ToySolver.Combinatorial.Knapsack.DPSparse
     ToySolver.Combinatorial.SubsetSum
     ToySolver.Converter.ObjType
     ToySolver.Converter.MIP2SMT
     ToySolver.Converter.MaxSAT2IP
     ToySolver.Converter.MaxSAT2NLPB
     ToySolver.Converter.MaxSAT2WBO
     ToySolver.Converter.PB2IP
     ToySolver.Converter.PB2LSP
     ToySolver.Converter.PB2WBO
     ToySolver.Converter.PBSetObj
     ToySolver.Converter.PB2SMP
     ToySolver.Converter.SAT2PB
     ToySolver.Converter.SAT2IP
     ToySolver.Converter.WBO2PB
     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.LA
     ToySolver.Data.LA.FOL
     ToySolver.Data.LBool
     ToySolver.Data.MIP
     ToySolver.Data.MIP.Base
     ToySolver.Data.MIP.LPFile
     ToySolver.Data.MIP.MPSFile
     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.Lagrange
     ToySolver.Data.Var
     ToySolver.SAT
     ToySolver.SAT.Integer
     ToySolver.SAT.MUS
     ToySolver.SAT.MUS.CAMUS
     ToySolver.SAT.MUS.DAA
     ToySolver.SAT.MUS.Types
     ToySolver.SAT.MUS.QuickXplain
     ToySolver.SAT.PBNLC
     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.TheorySolver
     ToySolver.SAT.TseitinEncoder
     ToySolver.SAT.Types
     ToySolver.SAT.Printer
     ToySolver.SMT
     ToySolver.Text.GCNF
     ToySolver.Text.GurobiSol
     ToySolver.Text.MaxSAT
     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.Data.AlgebraicNumber.Graeffe
     ToySolver.Data.Polynomial.Base
     ToySolver.Version.TH
     Paths_toysolver
  -- GHC-Prof-Options: -auto-all

Executable toysolver
  Main-is: toysolver.hs
  HS-Source-Dirs: toysolver
  Build-Depends:
    base,
    containers,
    array,
    data-default-class,
    filepath,
    OptDir,
    parse-dimacs,
    pseudo-boolean,
    toysolver
  Default-Language: Haskell2010
  if impl(ghc)
    GHC-Options: -rtsopts -threaded
  if flag(LinuxStatic)
    GHC-Options: -static -optl-static -optl-pthread
  -- GHC-Prof-Options: -auto-all

Executable toysat
  Main-is: toysat.hs
  Other-Modules: UBCSAT
  HS-Source-Dirs: toysat
  Build-Depends:
    base,
    data-default-class,
    mwc-random,
    containers,
    array,
    process >=1.1.0.2,
    parsec,
    bytestring,
    filepath,
    parse-dimacs,
    unbounded-delays,
    vector,
    vector-space,
    pseudo-boolean,
    toysolver
  if flag(Time15)
    Build-Depends: time >=1.5.0
  else
    Build-Depends: time <1.5.0, old-locale
  Default-Language: Haskell2010
  Other-Extensions: ScopedTypeVariables, CPP
  if impl(ghc)
    GHC-Options: -rtsopts
  -- GHC-Prof-Options: -auto-all
  if flag(ForceChar8) && impl(ghc)
    Build-Depends: base >=4.5
    CPP-OPtions: "-DFORCE_CHAR8"
  if flag(LinuxStatic)
    GHC-Options: -static -optl-static -optl-pthread

Executable toysmt
  HS-Source-Dirs: 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:
    base,
    containers,
    data-default-class,
    mtl,
    parsec,
    transformers,
    transformers-compat,
    toysolver
  if flag(UseHaskeline)
    Build-Depends: haskeline >=0.7 && <0.8
    CPP-Options: "-DUSE_HASKELINE_PACKAGE"
  Default-Language: Haskell2010
  Other-Extensions: ScopedTypeVariables, CPP
  if impl(ghc >= 7)
    GHC-Options: -rtsopts
  -- GHC-Prof-Options: -auto-all
  if flag(ForceChar8) && impl(ghc)
    Build-Depends: base >=4.5
    CPP-OPtions: "-DFORCE_CHAR8"
  if flag(LinuxStatic)
    GHC-Options: -static -optl-static -optl-pthread

Executable toyfmf
  If !flag(BuildToyFMF)
    Buildable: False
  Main-is: toyfmf.hs
  HS-Source-Dirs: toyfmf
  If flag(BuildToyFMF)
    Build-Depends:
      base,
      containers,
      toysolver,
      logic-TPTP >=0.4.1
    -- logic-TPTP <=0.4.3 has build error on ghc <7.9 and transformers >=0.5.1.
    if impl(ghc <7.9) && flag(Transformers051)
      Build-Depends: logic-TPTP >=0.4.4.0
  Default-Language: Haskell2010
  if impl(ghc)
    GHC-Options: -rtsopts
  if flag(LinuxStatic)
    GHC-Options: -static -optl-static -optl-pthread
  -- GHC-Prof-Options: -auto-all

-- Converters

Executable lpconvert
  Main-is: lpconvert.hs
  HS-Source-Dirs: lpconvert
  Build-Depends:
    base,
    filepath,
    data-default-class,
    parse-dimacs,
    pseudo-boolean,
    toysolver
  Default-Language: Haskell2010
  if flag(LinuxStatic)
    GHC-Options: -static -optl-static -optl-pthread

Executable pbconvert
  Main-is: pbconvert.hs
  HS-Source-Dirs: pbconvert
  Build-Depends:
    base >=4 && <5,
    filepath,
    data-default-class,
    parse-dimacs,
    pseudo-boolean,
    toysolver
  Default-Language: Haskell2010
  if flag(LinuxStatic)
    GHC-Options: -static -optl-static -optl-pthread

-- Sample Programs

Executable sudoku
  If !flag(BuildSamplePrograms)
    Buildable: False
  Main-is: sudoku.hs
  HS-Source-Dirs: samples/programs/sudoku
  Build-Depends:
    base,
    array,
    toysolver
  Default-Language: Haskell2010
  if flag(LinuxStatic)
    GHC-Options: -static -optl-static -optl-pthread

Executable nonogram
  If !flag(BuildSamplePrograms)
    Buildable: False
  Main-is: nonogram.hs
  HS-Source-Dirs: samples/programs/nonogram
  Build-Depends:
    base,
    array,
    containers,
    toysolver
  Default-Language: Haskell2010
  if flag(LinuxStatic)
    GHC-Options: -static -optl-static -optl-pthread

Executable nqueens
  If !flag(BuildSamplePrograms)
    Buildable: False
  Main-is: nqueens.hs
  HS-Source-Dirs: samples/programs/nqueens
  Build-Depends:
    base,
    array,
    toysolver
  Default-Language: Haskell2010
  if flag(LinuxStatic)
    GHC-Options: -static -optl-static -optl-pthread

Executable knapsack
  If !flag(BuildSamplePrograms)
    Buildable: False
  Main-is: knapsack.hs
  HS-Source-Dirs: samples/programs/knapsack
  Build-Depends:
    base,
    toysolver
  Default-Language: Haskell2010
  if flag(LinuxStatic)
    GHC-Options: -static -optl-static -optl-pthread

Executable htc
  If !flag(BuildSamplePrograms)
    Buildable: False
  Main-is: htc.hs
  HS-Source-Dirs: samples/programs/htc
  Build-Depends:
    base,
    containers,
    toysolver
  Default-Language: Haskell2010
  if flag(LinuxStatic)
    GHC-Options: -static -optl-static -optl-pthread

Executable svm2lp
  If !flag(BuildSamplePrograms)
    Buildable: False
  Main-is: svm2lp.hs
  HS-Source-Dirs: samples/programs/svm2lp
  Build-Depends:
    base,
    containers,
    data-default-class,
    split,
    toysolver
  Default-Language: Haskell2010
  if flag(LinuxStatic)
    GHC-Options: -static -optl-static -optl-pthread

-- Misc Programs

Executable pigeonhole
  If !flag(BuildMiscPrograms)
    Buildable: False
  Main-is: pigeonhole.hs
  HS-Source-Dirs: pigeonhole
  Build-Depends:
    base,
    containers,
    pseudo-boolean,
    toysolver
  Default-Language: Haskell2010
  if flag(LinuxStatic)
    GHC-Options: -static -optl-static -optl-pthread

Executable maxsatverify
  If !flag(BuildMiscPrograms)
    Buildable: False
  Main-is: maxsatverify.hs
  HS-Source-Dirs: maxsatverify
  Build-Depends:
    base,
    array,
    toysolver
  Default-Language: Haskell2010
  if flag(LinuxStatic)
    GHC-Options: -static -optl-static -optl-pthread

Executable pbverify
  Main-is: pbverify.hs
  If !flag(BuildMiscPrograms)
    Buildable: False
  HS-Source-Dirs: pbverify
  Build-Depends:
    base,
    array,
    pseudo-boolean,
    toysolver
  Default-Language: Haskell2010
  if flag(LinuxStatic)
    GHC-Options: -static -optl-static -optl-pthread

-- Test suites and benchmarks

Test-suite TestPolynomial
  Type:              exitcode-stdio-1.0
  HS-Source-Dirs:    test
  Main-is:           TestPolynomial.hs
  Build-depends:
    base,
    containers,
    toysolver,
    tasty >=0.10.1,
    tasty-hunit ==0.9.*,
    tasty-quickcheck ==0.8.*,
    tasty-th,
    data-interval,
    finite-field >=0.7.0 && <1.0.0,
    prettyclass >=1.0.0
  Default-Language: Haskell2010
  Other-Extensions: TemplateHaskell

Test-suite TestSuite
  Type:              exitcode-stdio-1.0
  HS-Source-Dirs:    test Smtlib toysmt
  Main-is:           TestSuite.hs
  Other-Modules:
    Test.AReal
    Test.AReal2
    Test.Arith
    Test.BoolExpr
    Test.CongruenceClosure
    Test.ContiTraverso
    Test.Delta
    Test.FiniteModelFinder
    Test.HittingSets
    Test.Knapsack
    Test.LPFile
    Test.Misc
    Test.MIPSolver2
    Test.MPSFile
    Test.SAT
    Test.SDPFile
    Test.Simplex
    Test.Simplex2
    Test.SMT
    Test.SMTLIB2Solver
    Test.SubsetSum
    Smtlib.Parsers.CommonParsers,
    Smtlib.Parsers.ResponseParsers,
    Smtlib.Parsers.CommandsParsers,
    Smtlib.Syntax.Syntax,
    Smtlib.Syntax.ShowSL
  Build-depends:
    base,
    array,
    containers,
    data-default-class,
    deepseq,
    mtl,
    mwc-random,
    parsec,
    transformers,
    transformers-compat,
    vector,
    vector-space,
    toysolver,
    data-interval,
    OptDir,
    tasty >=0.10.1,
    tasty-hunit ==0.9.*,
    tasty-quickcheck ==0.8.*,
    tasty-th,
    QuickCheck >=2.5 && <3
  Default-Language: Haskell2010
  Other-Extensions: TemplateHaskell, ScopedTypeVariables

Benchmark BenchmarkSATLIB
  type:             exitcode-stdio-1.0
  hs-source-dirs:   benchmarks
  main-is:          BenchmarkSATLIB.hs
  build-depends:
    base >=4 && <5,
    array,
    data-default-class,
    parse-dimacs,
    toysolver,
    criterion >=1.0 && <1.2
  Default-Language: Haskell2010

Benchmark BenchmarkKnapsack
  type:             exitcode-stdio-1.0
  hs-source-dirs:   benchmarks
  main-is:          BenchmarkKnapsack.hs
  build-depends:
    base >=4 && <5,
    toysolver,
    criterion >=1.0 && <1.2
  Default-Language: Haskell2010

Benchmark BenchmarkSubsetSum
  type:             exitcode-stdio-1.0
  hs-source-dirs:   benchmarks
  main-is:          BenchmarkSubsetSum.hs
  build-depends:
    base >=4 && <5,
    vector,
    toysolver,
    criterion >=1.0 && <1.2
  Default-Language: Haskell2010