Name: toysolver Version: 0.1.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 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.4.2 GHC ==7.6.3 GHC ==7.8.2 Extra-Source-Files: README.md COPYING .ghci .travis.yml src/TseitinEncode.hs src/ToySolver/Data/Polyhedron.hs src/ToySolver/Wang.hs samples/gcnf/*.cnf samples/gcnf/*.gcnf samples/lp/*.lp 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 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 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 source-repository head type: git location: git://github.com/msakai/toysolver.git Library Exposed: True Hs-source-dirs: src Build-Depends: base >=4 && <5, containers >= 0.4.2, unordered-containers >=0.2.3 && <0.3.0, mtl >=2.1.2, array, stm >=2.3, parsec, bytestring, filepath, deepseq, time, old-locale, 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, OptDir, data-interval >=0.6.0 && <1.0.0, finite-field >=0.7.0 && <1.0.0, sign >=0.2.0 && <1.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 if !flag(Exceptions06) Build-Depends: temporary >=1.2, exceptions ==0.5 if flag(Random1013) -- NOTE: random-1.0.1.3 uses atomicModifyIORef' which is provided by base >=4.6.0.0. 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 DoRec FlexibleInstances FunctionalDependencies GeneralizedNewtypeDeriving MultiParamTypeClasses Rank2Types ScopedTypeVariables TypeFamilies TypeSynonymInstances OverloadedStrings Exposed-Modules: ToySolver.BoundsInference ToySolver.CAD ToySolver.CongruenceClosure ToySolver.ContiTraverso ToySolver.Cooper ToySolver.Cooper.Core ToySolver.Cooper.FOL ToySolver.FOLModelFinder ToySolver.FourierMotzkin ToySolver.FourierMotzkin.Core ToySolver.FourierMotzkin.FOL ToySolver.HittingSet ToySolver.HittingSet.HTCBDD ToySolver.HittingSet.SHD ToySolver.Knapsack ToySolver.LPSolver ToySolver.LPSolverHL ToySolver.LPUtil ToySolver.MIPSolverHL ToySolver.MIPSolver2 ToySolver.OmegaTest ToySolver.OmegaTest.Misc ToySolver.Simplex ToySolver.Simplex2 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.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.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.Vec ToySolver.Data.Var ToySolver.SAT ToySolver.SAT.Integer ToySolver.SAT.MUS ToySolver.SAT.CAMUS 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.LPFile ToySolver.Text.MPSFile ToySolver.Text.MaxSAT ToySolver.Text.PBFile ToySolver.Text.SDPFile ToySolver.Internal.Data.IndexedPriorityQueue ToySolver.Internal.Data.PriorityQueue ToySolver.Internal.Data.SeqQueue ToySolver.Internal.ProcessUtil ToySolver.Internal.TextUtil ToySolver.Internal.Util 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, filepath, parsec, OptDir, parse-dimacs, 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, random, containers >= 0.4.2, array, process >=1.1.0.2, parsec, bytestring, filepath, parse-dimacs, time, old-locale, unbounded-delays, vector-space >=0.8.6, toysolver 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 Executable lpconvert Main-is: lpconvert.hs HS-Source-Dirs: lpconvert Build-Depends: base >=4 && <5, containers, filepath, parse-dimacs, toysolver Default-Language: Haskell2010 Executable pbconvert Main-is: pbconvert.hs HS-Source-Dirs: pbconvert Build-Depends: base >=4 && <5, containers, filepath, parse-dimacs, toysolver Default-Language: Haskell2010 Executable pigeonhole If !flag(BuildMiscPrograms) Buildable: False Main-is: pigeonhole.hs HS-Source-Dirs: pigeonhole Build-Depends: base >=4 && <5, containers, filepath, 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 HS-Source-Dirs: pbverify Build-Depends: base >=4 && <5, array, containers, filepath, toysolver Default-Language: Haskell2010 Test-suite TestSAT Type: exitcode-stdio-1.0 HS-Source-Dirs: test Main-is: TestSAT.hs Build-depends: base >=4 && <5, array, containers, toysolver, test-framework,test-framework-th,test-framework-hunit,test-framework-quickcheck2 >=0.2.12.3 && <0.4.0,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, test-framework,test-framework-th,test-framework-hunit,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, test-framework,test-framework-th,test-framework-hunit,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, test-framework, test-framework-th, test-framework-hunit, 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, test-framework,test-framework-th,test-framework-hunit,test-framework-quickcheck2 >=0.2.12.3 && <0.4.0,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, test-framework,test-framework-th,test-framework-hunit,test-framework-quickcheck2 >=0.2.12.3 && <0.4.0,HUnit,QuickCheck >=2.5 && <3, data-interval Default-Language: Haskell2010 Other-Extensions: TemplateHaskell, ScopedTypeVariables Test-suite TestQE Type: exitcode-stdio-1.0 HS-Source-Dirs: test Main-is: TestQE.hs Build-depends: base >=4 && <5, containers, vector-space >=0.8.6, toysolver, OptDir, test-framework,test-framework-th,test-framework-hunit,test-framework-quickcheck2 >=0.2.12.3 && <0.4.0,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, test-framework,test-framework-th,test-framework-hunit,test-framework-quickcheck2 >=0.2.12.3 && <0.4.0,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, test-framework,test-framework-th,test-framework-hunit,test-framework-quickcheck2 >=0.2.12.3 && <0.4.0,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, test-framework,test-framework-th,test-framework-hunit,test-framework-quickcheck2 >=0.2.12.3 && <0.4.0,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, test-framework,test-framework-th,test-framework-hunit,test-framework-quickcheck2 >=0.2.12.3 && <0.4.0,HUnit,QuickCheck >=2.5 && <3 Default-Language: Haskell2010 Other-Extensions: TemplateHaskell Test-suite TestPBFile Type: exitcode-stdio-1.0 HS-Source-Dirs: test Main-is: TestPBFile.hs Build-depends: base >=4 && <5, toysolver, test-framework,test-framework-th,test-framework-hunit,test-framework-quickcheck2 >=0.2.12.3 && <0.4.0,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, test-framework,test-framework-th,test-framework-hunit,test-framework-quickcheck2 >=0.2.12.3 && <0.4.0,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, toysolver, test-framework,test-framework-th,test-framework-hunit,test-framework-quickcheck2 >=0.2.12.3 && <0.4.0,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 Default-Language: Haskell2010