Name: toysolver Version: 0.3.0 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.1 Extra-Source-Files: README.md COPYING .ghci .travis.yml build_bdist_linux-i386.sh build_bdist_linux-x86_64.sh build_bdist_macos.sh build_bdist_win32.sh build_bdist_win64.sh 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 test/TestAReal2.hs 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 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 Random1013 Description: use random >=1.0.1.3 Manual: False Flag Time15 Description: use time >=1.5.0 Manual: False source-repository head type: git location: git://github.com/msakai/toysolver.git Library Exposed: True Hs-source-dirs: src Build-Depends: base >=4 && <5, -- mergeWithKey requires containers >=0.5.0 containers >=0.5.0, unordered-containers >=0.2.3 && <0.3.0, 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, unbounded-delays, 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, OptDir, extended-reals >=0.1 && <1.0, data-interval >=1.0.1 && <1.3.0, finite-field >=0.7.0 && <1.0.0, sign >=0.2.0 && <1.0.0, pseudo-boolean >=0.1.0.0 && <0.1.1.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 -- NOTE: random-1.0.1.3 uses atomicModifyIORef' which is provided by base >=4.6.0.0. if flag(Random1013) Build-Depends: base >=4.6.0.0, random >=1.0.1.3 else Build-Depends: random <1.0.1.3 if impl(ghc) Build-Depends: ghc-prim Default-Language: Haskell2010 Other-Extensions: BangPatterns CPP DeriveDataTypeable DeriveGeneric DoRec FlexibleContexts FlexibleInstances FunctionalDependencies GeneralizedNewtypeDeriving MultiParamTypeClasses Rank2Types ScopedTypeVariables TypeFamilies TypeSynonymInstances OverloadedStrings 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.CongruenceClosure ToySolver.FOLModelFinder 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.DP 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.ArithRel 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.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.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 Paths_toysolver -- GHC-Prof-Options: -auto-all Executable toysolver Main-is: toysolver.hs HS-Source-Dirs: toysolver Build-Depends: base >=4.4 && <5, containers, array, data-default-class, filepath, parsec, OptDir, parse-dimacs, pseudo-boolean, toysolver Default-Language: Haskell2010 if impl(ghc) GHC-Options: -threaded if impl(ghc >= 7) GHC-Options: -rtsopts -- GHC-Prof-Options: -auto-all Executable toysat Main-is: toysat.hs Other-Modules: UBCSAT HS-Source-Dirs: toysat Build-Depends: base >=4 && <5, data-default-class, random, containers >= 0.4.2, array, process >=1.1.0.2, parsec, bytestring, filepath, parse-dimacs, unbounded-delays, vector-space >=0.8.6, 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 >= 7) GHC-Options: -rtsopts -- GHC-Prof-Options: -auto-all if flag(ForceChar8) && impl(ghc) Build-Depends: base >=4.5 CPP-OPtions: "-DFORCE_CHAR8" Executable toyfmf If !flag(BuildToyFMF) Buildable: False Main-is: toyfmf.hs HS-Source-Dirs: toyfmf If flag(BuildToyFMF) Build-Depends: base >=4 && <5, containers >= 0.4.2, toysolver, logic-TPTP >=0.4.1 Default-Language: Haskell2010 if impl(ghc >= 7) GHC-Options: -rtsopts -- GHC-Prof-Options: -auto-all -- Converters Executable lpconvert Main-is: lpconvert.hs HS-Source-Dirs: lpconvert Build-Depends: base >=4 && <5, containers, filepath, parse-dimacs, pseudo-boolean, toysolver Default-Language: Haskell2010 Executable pbconvert Main-is: pbconvert.hs HS-Source-Dirs: pbconvert Build-Depends: base >=4 && <5, containers, filepath, parse-dimacs, pseudo-boolean, toysolver Default-Language: Haskell2010 -- 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 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 Executable knapsack If !flag(BuildSamplePrograms) Buildable: False Main-is: knapsack.hs HS-Source-Dirs: samples/programs/knapsack Build-Depends: base, array, toysolver Default-Language: Haskell2010 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 -- Misc Programs Executable pigeonhole If !flag(BuildMiscPrograms) Buildable: False Main-is: pigeonhole.hs HS-Source-Dirs: pigeonhole Build-Depends: base >=4 && <5, containers, filepath, pseudo-boolean, toysolver Default-Language: Haskell2010 Executable maxsatverify If !flag(BuildMiscPrograms) Buildable: False Main-is: maxsatverify.hs HS-Source-Dirs: maxsatverify Build-Depends: base >=4 && <5, array, containers, filepath, toysolver Default-Language: Haskell2010 Executable pbverify Main-is: pbverify.hs If !flag(BuildMiscPrograms) Buildable: False HS-Source-Dirs: pbverify Build-Depends: base >=4 && <5, array, containers, filepath, pseudo-boolean, toysolver Default-Language: Haskell2010 -- Test suites and benchmarks Test-suite TestSAT Type: exitcode-stdio-1.0 HS-Source-Dirs: test Main-is: TestSAT.hs Build-depends: base >=4 && <5, array, containers, random, toysolver, tasty >=0.10.1, tasty-hunit ==0.9.*, tasty-quickcheck ==0.8.*, tasty-th, HUnit, QuickCheck >=2.5 && <3 Default-Language: Haskell2010 Other-Extensions: TemplateHaskell Test-suite TestSimplex Type: exitcode-stdio-1.0 HS-Source-Dirs: test Main-is: TestSimplex.hs Build-depends: base >=4 && <5, containers, mtl, toysolver, tasty >=0.10.1, tasty-hunit ==0.9.*, tasty-th, HUnit Default-Language: Haskell2010 Other-Extensions: TemplateHaskell Test-suite TestSimplex2 Type: exitcode-stdio-1.0 HS-Source-Dirs: test Main-is: TestSimplex2.hs Build-depends: base >=4 && <5, containers, vector-space >=0.8.6, toysolver, tasty >=0.10.1, tasty-hunit ==0.9.*, tasty-th, HUnit Default-Language: Haskell2010 Other-Extensions: TemplateHaskell Test-suite TestMIPSolver2 Type: exitcode-stdio-1.0 HS-Source-Dirs: test Main-is: TestMIPSolver2.hs Build-depends: base >=4 && <5, containers, vector-space >=0.8.6, toysolver, tasty >=0.10.1, tasty-hunit ==0.9.*, tasty-th, HUnit, OptDir, stm Default-Language: Haskell2010 Other-Extensions: TemplateHaskell Test-suite TestPolynomial Type: exitcode-stdio-1.0 HS-Source-Dirs: test Main-is: TestPolynomial.hs Build-depends: base >=4 && <5, containers, toysolver, tasty >=0.10.1, tasty-hunit ==0.9.*, tasty-quickcheck ==0.8.*, tasty-th, HUnit, QuickCheck >=2.5 && <3, data-interval, finite-field >=0.7.0 && <1.0.0, prettyclass >=1.0.0 Default-Language: Haskell2010 Other-Extensions: TemplateHaskell Test-suite TestAReal Type: exitcode-stdio-1.0 HS-Source-Dirs: test Main-is: TestAReal.hs Build-depends: base >=4 && <5, containers, toysolver, tasty >=0.10.1, tasty-hunit ==0.9.*, tasty-quickcheck ==0.8.*, tasty-th, HUnit, QuickCheck >=2.5 && <3, data-interval Default-Language: Haskell2010 Other-Extensions: TemplateHaskell, ScopedTypeVariables Test-suite TestArith Type: exitcode-stdio-1.0 HS-Source-Dirs: test Main-is: TestArith.hs Build-depends: base >=4 && <5, containers, vector-space >=0.8.6, toysolver, data-interval, OptDir, tasty >=0.10.1, tasty-hunit ==0.9.*, tasty-quickcheck ==0.8.*, tasty-th, HUnit, QuickCheck >=2.5 && <3 Default-Language: Haskell2010 Other-Extensions: TemplateHaskell Test-suite TestContiTraverso Type: exitcode-stdio-1.0 HS-Source-Dirs: test Main-is: TestContiTraverso.hs Build-depends: base >=4 && <5, containers, vector-space >=0.8.6, toysolver, OptDir, tasty >=0.10.1, tasty-hunit ==0.9.*, tasty-quickcheck ==0.8.*, tasty-th, HUnit, QuickCheck >=2.5 && <3 Default-Language: Haskell2010 Other-Extensions: TemplateHaskell Test-suite TestCongruenceClosure Type: exitcode-stdio-1.0 HS-Source-Dirs: test Main-is: TestCongruenceClosure.hs Build-depends: base >=4 && <5, containers, toysolver, tasty >=0.10.1, tasty-hunit ==0.9.*, tasty-quickcheck ==0.8.*, tasty-th, HUnit, QuickCheck >=2.5 && <3 Default-Language: Haskell2010 Other-Extensions: TemplateHaskell Test-suite TestLPFile Type: exitcode-stdio-1.0 HS-Source-Dirs: test Main-is: TestLPFile.hs Build-depends: base >=4 && <5, containers, toysolver, tasty >=0.10.1, tasty-hunit ==0.9.*, tasty-quickcheck ==0.8.*, tasty-th, HUnit, QuickCheck >=2.5 && <3 Default-Language: Haskell2010 Other-Extensions: TemplateHaskell Test-suite TestMPSFile Type: exitcode-stdio-1.0 HS-Source-Dirs: test Main-is: TestMPSFile.hs Build-depends: base >=4 && <5, containers, toysolver, tasty >=0.10.1, tasty-hunit ==0.9.*, tasty-quickcheck ==0.8.*, tasty-th, HUnit, QuickCheck >=2.5 && <3 Default-Language: Haskell2010 Other-Extensions: TemplateHaskell Test-suite TestSDPFile Type: exitcode-stdio-1.0 HS-Source-Dirs: test Main-is: TestSDPFile.hs Build-depends: base >=4 && <5, toysolver, tasty >=0.10.1, tasty-hunit ==0.9.*, tasty-quickcheck ==0.8.*, tasty-th, HUnit, QuickCheck >=2.5 && <3 Default-Language: Haskell2010 Other-Extensions: TemplateHaskell Test-suite TestUtil Type: exitcode-stdio-1.0 HS-Source-Dirs: test Main-is: TestUtil.hs Build-depends: base >=4 && <5, containers, toysolver, tasty >=0.10.1, tasty-hunit ==0.9.*, tasty-quickcheck ==0.8.*, tasty-th, HUnit, 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, containers, random, parse-dimacs, toysolver, criterion >=1.0 && <1.1 Default-Language: Haskell2010