Cabal revisions of toysolver-0.6.0
Hackage metadata revisions edit the .cabal file after upload; each diff below is one revision.
revision 1
-Name: toysolver-Version: 0.6.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, Formal Methods, SMT-Cabal-Version: 1.18-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 ==7.10.3- GHC ==8.0.2- GHC ==8.2.2- GHC ==8.4.4- GHC ==8.6.4-Extra-Source-Files:- README.md- CHANGELOG.markdown- COPYING- COPYING-GPL- misc/build_bdist_linux.sh- misc/build_bdist_macos.sh- misc/build_bdist_win32.sh- misc/build_bdist_win64.sh- misc/build_bdist_maxsat_evaluation.sh- misc/build_bdist_pb_evaluation.sh- misc/build_bdist_qbf_evaluation.sh- misc/build_bdist_smtcomp.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- misc/qbf/README.md- misc/smtcomp/bin/starexec_run_default- misc/smtcomp/starexec_description.txt- src/ToySolver/Data/Polyhedron.hs- src/ToySolver/SAT/MessagePassing/SurveyPropagation/sp.cl- samples/gcnf/*.cnf- samples/gcnf/*.gcnf- samples/gcnf/edn_20403_8.cnf_0.03000000.unsat.gcnf- samples/lp/*.lp- samples/lp/*.sol- samples/lp/*.txt- 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- 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- doc-images/MIP-Status-diagram.tex-Extra-Doc-Files:- doc-images/MIP-Status-diagram.png-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 BuildSamplePrograms- Description: build sample programs- Default: False- Manual: True--Flag BuildMiscPrograms- Description: build misc programs- Default: False- Manual: True--Flag LogicTPTP045- Description: use logic-TPTP >=0.4.5.0- Manual: False- Default: True--Flag UseHaskeline- Description: use haskeline package- Manual: True- Default: True--Flag OpenCL- Description: use opencl package- Manual: True- Default: False--Flag TestCBC- Description: run test cases that depends on cbc command- Manual: True- Default: False--Flag TestCPLEX- Description: run test cases that depends on cplex command- Manual: True- Default: False--Flag TestGlpsol- Description: run test cases that depends on glpsol command- Manual: True- Default: False--Flag TestGurobiCl- Description: run test cases that depends on gurobi_cl command- Manual: True- Default: False--Flag TestLPSolve- Description: run test cases that depends on lp_solve command- Manual: True- Default: False--Flag TestSCIP- Description: run test cases that depends on scip command- Manual: True- Default: False--source-repository head- type: git- location: git://github.com/msakai/toysolver.git--Library- Exposed: True- Hs-source-dirs: src- Build-Depends:- array >=0.4.0.0,- -- GHC >=7.10- base >=4.8 && <5,- bytestring >=0.9.2.1 && <0.11,- bytestring-builder,- bytestring-encoding,- case-insensitive,- clock >=0.7.1,- -- IntMap.mergeWithKey and IntMap.toDescList require containers >=0.5.0- containers >=0.5.0,- data-default-class,- data-interval >=1.0.1 && <1.4.0,- deepseq,- extended-reals >=0.1 && <1.0,- filepath,- finite-field >=0.9.0 && <1.0.0,- hashable >=1.1.2.5 && <1.3.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,- mtl >=2.1.2,- multiset,- -- createSystemRandom requires mwc-random >=0.13.1.0- mwc-random >=0.13.1 && <0.15,- OptDir,- lattices,- megaparsec >=4 && <8,- -- 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,- time >=1.5.0,- transformers >=0.2,- transformers-compat >=0.3,- unordered-containers >=0.2.3 && <0.3.0,- vector,- vector-space >=0.8.6,- xml-conduit- if flag(WithZlib)- Build-Depends: zlib- CPP-Options: "-DWITH_ZLIB"- if flag(OpenCL)- Build-Depends: OpenCL >=1.0.3.4- Exposed-Modules: ToySolver.SAT.MessagePassing.SurveyPropagation.OpenCL- if impl(ghc)- Build-Depends: ghc-prim- Default-Language: Haskell2010- Other-Extensions:- BangPatterns- CPP- DeriveDataTypeable- ExistentialQuantification- FlexibleContexts- FlexibleInstances- FunctionalDependencies- GeneralizedNewtypeDeriving- MultiParamTypeClasses- OverloadedStrings- RecursiveDo- Rank2Types- ScopedTypeVariables- TemplateHaskell- TypeFamilies- TypeOperators- TypeSynonymInstances- -- commented out because cabal-1.16 does not understand InstanceSigs extension- -- InstanceSigs- 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.ObjType- ToySolver.Converter.MIP2PB- ToySolver.Converter.MIP2SMT- ToySolver.Converter.NAESAT- ToySolver.Converter.PB- ToySolver.Converter.PB2IP- ToySolver.Converter.PB2LSP- ToySolver.Converter.PBSetObj- ToySolver.Converter.PB2SMP- ToySolver.Converter.QBF2IPC- ToySolver.Converter.QUBO- 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.MIP- ToySolver.Data.MIP.Base- ToySolver.Data.MIP.FileUtils- ToySolver.Data.MIP.LPFile- ToySolver.Data.MIP.MPSFile- ToySolver.Data.MIP.Solution.CBC- ToySolver.Data.MIP.Solution.CPLEX- ToySolver.Data.MIP.Solution.GLPK- ToySolver.Data.MIP.Solution.Gurobi- ToySolver.Data.MIP.Solution.SCIP- ToySolver.Data.MIP.Solver- ToySolver.Data.MIP.Solver.Base- ToySolver.Data.MIP.Solver.CBC- ToySolver.Data.MIP.Solver.CPLEX- ToySolver.Data.MIP.Solver.Glpsol- ToySolver.Data.MIP.Solver.GurobiCl- ToySolver.Data.MIP.Solver.LPSolve- ToySolver.Data.MIP.Solver.SCIP- 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.FileFormat- ToySolver.FileFormat.Base- ToySolver.FileFormat.CNF- ToySolver.Graph.ShortestPath- ToySolver.MaxCut- ToySolver.QBF- ToySolver.QUBO- ToySolver.SAT- ToySolver.SAT.Config- ToySolver.SAT.Encoder.Integer- ToySolver.SAT.Encoder.PB- ToySolver.SAT.Encoder.PB.Internal.Adder- 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.Tseitin- ToySolver.SAT.ExistentialQuantification- ToySolver.SAT.MessagePassing.SurveyPropagation- 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.SLS.ProbSAT- ToySolver.SAT.Store.CNF- ToySolver.SAT.Store.PB- ToySolver.SAT.TheorySolver- ToySolver.SAT.Types- ToySolver.SAT.Printer- ToySolver.SDP- ToySolver.SMT- ToySolver.Text.CNF- ToySolver.Text.GCNF- ToySolver.Text.QDimacs- ToySolver.Text.SDPFile- ToySolver.Text.WCNF- 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.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- -- GHC-Prof-Options: -auto-all--Executable toysolver- Main-is: toysolver.hs- HS-Source-Dirs: app- Build-Depends:- array,- base,- containers,- data-default-class,- filepath,- OptDir,- optparse-applicative,- pseudo-boolean,- scientific,- toysolver- Default-Language: Haskell2010- Other-Extensions: CPP- GHC-Options: -rtsopts -threaded- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- 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: app/toysat- Build-Depends:- array,- base,- bytestring,- containers,- clock,- data-default,- data-default-class,- directory,- filepath,- megaparsec,- mwc-random,- optparse-applicative,- process >=1.1.0.2,- pseudo-boolean,- scientific,- temporary,- time,- toysolver,- unbounded-delays,- vector- Default-Language: Haskell2010- Other-Extensions: ScopedTypeVariables, CPP- GHC-Options: -rtsopts -threaded- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- if flag(WithZlib)- CPP-Options: "-DWITH_ZLIB"- if flag(LinuxStatic)- GHC-Options: -static -optl-static -optl-pthread--Executable toysmt- 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:- base,- 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.8- CPP-Options: "-DUSE_HASKELINE_PACKAGE"- Default-Language: Haskell2010- Other-Extensions: ScopedTypeVariables, CPP- GHC-Options: -rtsopts- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- if flag(LinuxStatic)- GHC-Options: -static -optl-static -optl-pthread--Executable toyqbf- Main-is: toyqbf.hs- HS-Source-Dirs: app- Build-Depends:- base,- containers,- data-default-class,- optparse-applicative,- toysolver- Default-Language: Haskell2010- Other-Extensions: ScopedTypeVariables, CPP- GHC-Options: -rtsopts- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- 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: app- If flag(BuildToyFMF)- Build-Depends:- base,- containers,- intern,- -- logic-TPTP <=0.4.3 has build error on ghc <7.9 and transformers >=0.5.1.- -- https://github.com/DanielSchuessler/logic-TPTP/pull/4- logic-TPTP >=0.4.4.0,- optparse-applicative,- text,- toysolver- -- logic-TPTP <=0.4.4.0 is not compatible with transformers-compat >=0.5- if impl(ghc <7.9)- if flag(LogicTPTP045)- Build-Depends:- logic-TPTP >=0.4.5.0- else- Build-Depends:- transformers-compat <0.5- -- for Semigroup (as superclass of) Monoid Proposal- if impl(ghc >=8.4)- Build-Depends: logic-TPTP >=0.4.6.0- Default-Language: Haskell2010- Other-Extensions: CPP- GHC-Options: -rtsopts- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- if flag(LinuxStatic)- GHC-Options: -static -optl-static -optl-pthread- -- GHC-Prof-Options: -auto-all---- Converters--Executable toyconvert- Main-is: toyconvert.hs- HS-Source-Dirs: app- Build-Depends:- base,- ansi-wl-pprint,- bytestring,- bytestring-builder,- data-default-class,- filepath,- optparse-applicative,- pseudo-boolean,- scientific,- text,- toysolver- Default-Language: Haskell2010- Other-Extensions: CPP- GHC-Options: -rtsopts- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- if flag(WithZlib)- CPP-Options: "-DWITH_ZLIB"- 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:- array,- base,- toysolver- Default-Language: Haskell2010- Other-Extensions: CPP- GHC-Options: -rtsopts- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- 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:- array,- base,- containers,- toysolver- Default-Language: Haskell2010- Other-Extensions: CPP- GHC-Options: -rtsopts- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- 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:- array,- base,- toysolver- Default-Language: Haskell2010- Other-Extensions: CPP- GHC-Options: -rtsopts- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- if flag(LinuxStatic)- GHC-Options: -static -optl-static -optl-pthread--Executable numberlink- If !flag(BuildSamplePrograms)- Buildable: False- Main-is: numberlink.hs- HS-Source-Dirs: samples/programs/numberlink- Build-Depends:- array,- base,- bytestring,- containers,- data-default-class,- parsec,- pseudo-boolean,- toysolver- Default-Language: Haskell2010- Other-Extensions: CPP- GHC-Options: -rtsopts- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- 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- Other-Extensions: CPP- GHC-Options: -rtsopts- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- if flag(LinuxStatic)- GHC-Options: -static -optl-static -optl-pthread--Executable assign- If !flag(BuildSamplePrograms)- Buildable: False- Main-is: assign.hs- HS-Source-Dirs: samples/programs/assign- Build-Depends:- attoparsec,- base,- bytestring,- containers,- toysolver,- vector- Default-Language: Haskell2010- Other-Extensions: CPP- GHC-Options: -rtsopts- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- if flag(LinuxStatic)- GHC-Options: -static -optl-static -optl-pthread--Executable shortest-path- If !flag(BuildSamplePrograms)- Buildable: False- Main-is: shortest-path.hs- HS-Source-Dirs: samples/programs/shortest-path- Build-Depends:- base,- bytestring,- containers,- unordered-containers,- toysolver- Default-Language: Haskell2010- Other-Extensions: CPP- GHC-Options: -rtsopts- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- 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- Other-Extensions: CPP- GHC-Options: -rtsopts- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- 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,- scientific,- split,- text,- toysolver- Default-Language: Haskell2010- Other-Extensions: CPP- GHC-Options: -rtsopts- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- if flag(LinuxStatic)- GHC-Options: -static -optl-static -optl-pthread--Executable survey-propagation- if !flag(BuildSamplePrograms)- Buildable: False - Main-is: survey-propagation.hs- HS-Source-Dirs: samples/programs/survey-propagation- Build-Depends:- base,- data-default-class,- toysolver- if flag(OpenCL)- Build-Depends: OpenCL- CPP-Options: "-DENABLE_OPENCL"- Default-Language: Haskell2010- Other-Extensions: CPP- -- We use threaded RTS to avoid the error "schedule: re-entered unsafely.- -- Perhaps a 'foreign import unsafe' should be 'safe'?" on NVIDIA CUDA.- GHC-Options: -rtsopts -threaded- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- CPP-Options: "-DFORCE_CHAR8"- if flag(LinuxStatic)- GHC-Options: -static -optl-static -optl-pthread--Executable probsat- if !flag(BuildSamplePrograms)- Buildable: False - Main-is: probsat.hs- HS-Source-Dirs: samples/programs/probsat- Build-Depends:- base,- clock,- data-default-class,- mwc-random,- optparse-applicative,- vector,- toysolver- Default-Language: Haskell2010- Other-Extensions: CPP- GHC-Options: -rtsopts- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- CPP-Options: "-DFORCE_CHAR8"- 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: app- Build-Depends:- base,- bytestring,- containers,- pseudo-boolean,- toysolver- Default-Language: Haskell2010- Other-Extensions: CPP- GHC-Options: -rtsopts- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- if flag(LinuxStatic)- GHC-Options: -static -optl-static -optl-pthread--Executable maxsatverify- If !flag(BuildMiscPrograms)- Buildable: False- Main-is: maxsatverify.hs- HS-Source-Dirs: app- Build-Depends:- array,- base,- toysolver- Default-Language: Haskell2010- Other-Extensions: CPP- GHC-Options: -rtsopts- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- if flag(LinuxStatic)- GHC-Options: -static -optl-static -optl-pthread--Executable pbverify- Main-is: pbverify.hs- If !flag(BuildMiscPrograms)- Buildable: False- HS-Source-Dirs: app- Build-Depends:- array,- base,- pseudo-boolean,- toysolver- Default-Language: Haskell2010- Other-Extensions: CPP- GHC-Options: -rtsopts- -- GHC-Prof-Options: -auto-all- if flag(ForceChar8)- CPP-OPtions: "-DFORCE_CHAR8"- 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,- 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.11,- tasty-th,- toysolver- Default-Language: Haskell2010- Other-Extensions: TemplateHaskell--Test-suite TestSuite- 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.GraphShortestPath- Test.HittingSets- Test.Knapsack- Test.LPFile- Test.Misc- Test.MIP- Test.MIPSolver- Test.MIPSolver2- Test.MPSFile- 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:- array,- base,- bytestring,- bytestring-builder,- containers,- data-default-class,- data-interval,- deepseq,- hashable,- intern,- lattices,- megaparsec,- mtl,- mwc-random,- OptDir,- parsec >=3.1.2 && <4,- pseudo-boolean,- QuickCheck >=2.5 && <3,- scientific,- tasty >=0.10.1,- tasty-hunit >=0.9 && <0.11,- tasty-quickcheck >=0.8 && <0.11,- tasty-th,- text,- toysolver,- transformers,- transformers-compat,- unordered-containers,- vector,- vector-space- Default-Language: Haskell2010- Other-Extensions: TemplateHaskell, ScopedTypeVariables- if flag(TestCBC)- CPP-Options: "-DTEST_CBC"- if flag(TestCPLEX)- CPP-Options: "-DTEST_CPLEX"- if flag(TestGlpsol)- CPP-Options: "-DTEST_GLPSOL"- if flag(TestGurobiCl)- CPP-Options: "-DTEST_GUROBI_CL"- if flag(TestLPSolve)- CPP-Options: "-DTEST_LP_SOLVE"- if flag(TestSCIP)- CPP-Options: "-DTEST_SCIP"--Benchmark BenchmarkSATLIB- type: exitcode-stdio-1.0- hs-source-dirs: benchmarks- main-is: BenchmarkSATLIB.hs- build-depends:- array,- base,- criterion >=1.0 && <1.6,- data-default-class,- toysolver- Default-Language: Haskell2010--Benchmark BenchmarkKnapsack- type: exitcode-stdio-1.0- hs-source-dirs: benchmarks- main-is: BenchmarkKnapsack.hs- build-depends:- base,- criterion >=1.0 && <1.6,- toysolver- Default-Language: Haskell2010--Benchmark BenchmarkSubsetSum- type: exitcode-stdio-1.0- hs-source-dirs: benchmarks- main-is: BenchmarkSubsetSum.hs- build-depends:- base,- criterion >=1.0 && <1.6,- toysolver,- vector- Default-Language: Haskell2010+Name: toysolver +Version: 0.6.0 +x-revision: 1 +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, Formal Methods, SMT +Cabal-Version: 1.18 +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 ==7.10.3 + GHC ==8.0.2 + GHC ==8.2.2 + GHC ==8.4.4 + GHC ==8.6.4 +Extra-Source-Files: + README.md + CHANGELOG.markdown + COPYING + COPYING-GPL + misc/build_bdist_linux.sh + misc/build_bdist_macos.sh + misc/build_bdist_win32.sh + misc/build_bdist_win64.sh + misc/build_bdist_maxsat_evaluation.sh + misc/build_bdist_pb_evaluation.sh + misc/build_bdist_qbf_evaluation.sh + misc/build_bdist_smtcomp.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 + misc/qbf/README.md + misc/smtcomp/bin/starexec_run_default + misc/smtcomp/starexec_description.txt + src/ToySolver/Data/Polyhedron.hs + src/ToySolver/SAT/MessagePassing/SurveyPropagation/sp.cl + samples/gcnf/*.cnf + samples/gcnf/*.gcnf + samples/gcnf/edn_20403_8.cnf_0.03000000.unsat.gcnf + samples/lp/*.lp + samples/lp/*.sol + samples/lp/*.txt + 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 + 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 + doc-images/MIP-Status-diagram.tex +Extra-Doc-Files: + doc-images/MIP-Status-diagram.png +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 BuildSamplePrograms + Description: build sample programs + Default: False + Manual: True + +Flag BuildMiscPrograms + Description: build misc programs + Default: False + Manual: True + +Flag LogicTPTP045 + Description: use logic-TPTP >=0.4.5.0 + Manual: False + Default: True + +Flag UseHaskeline + Description: use haskeline package + Manual: True + Default: True + +Flag OpenCL + Description: use opencl package + Manual: True + Default: False + +Flag TestCBC + Description: run test cases that depends on cbc command + Manual: True + Default: False + +Flag TestCPLEX + Description: run test cases that depends on cplex command + Manual: True + Default: False + +Flag TestGlpsol + Description: run test cases that depends on glpsol command + Manual: True + Default: False + +Flag TestGurobiCl + Description: run test cases that depends on gurobi_cl command + Manual: True + Default: False + +Flag TestLPSolve + Description: run test cases that depends on lp_solve command + Manual: True + Default: False + +Flag TestSCIP + Description: run test cases that depends on scip command + Manual: True + Default: False + +source-repository head + type: git + location: git://github.com/msakai/toysolver.git + +Library + Exposed: True + Hs-source-dirs: src + Build-Depends: + array >=0.4.0.0, + -- GHC >=7.10 + base >=4.8 && <5, + bytestring >=0.9.2.1 && <0.11, + bytestring-builder, + bytestring-encoding, + case-insensitive, + clock >=0.7.1, + -- IntMap.mergeWithKey and IntMap.toDescList require containers >=0.5.0 + containers >=0.5.0, + data-default-class, + data-interval >=1.0.1 && <1.4.0, + deepseq, + extended-reals >=0.1 && <1.0, + filepath, + finite-field >=0.9.0 && <1.0.0, + hashable >=1.1.2.5 && <1.4.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, + mtl >=2.1.2, + multiset, + -- createSystemRandom requires mwc-random >=0.13.1.0 + mwc-random >=0.13.1 && <0.15, + OptDir, + lattices, + megaparsec >=4 && <8, + -- 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, + time >=1.5.0, + transformers >=0.2, + transformers-compat >=0.3, + unordered-containers >=0.2.3 && <0.3.0, + vector, + vector-space >=0.8.6, + xml-conduit + if flag(WithZlib) + Build-Depends: zlib + CPP-Options: "-DWITH_ZLIB" + if flag(OpenCL) + Build-Depends: OpenCL >=1.0.3.4 + Exposed-Modules: ToySolver.SAT.MessagePassing.SurveyPropagation.OpenCL + if impl(ghc) + Build-Depends: ghc-prim + Default-Language: Haskell2010 + Other-Extensions: + BangPatterns + CPP + DeriveDataTypeable + ExistentialQuantification + FlexibleContexts + FlexibleInstances + FunctionalDependencies + GeneralizedNewtypeDeriving + MultiParamTypeClasses + OverloadedStrings + RecursiveDo + Rank2Types + ScopedTypeVariables + TemplateHaskell + TypeFamilies + TypeOperators + TypeSynonymInstances + -- commented out because cabal-1.16 does not understand InstanceSigs extension + -- InstanceSigs + 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.ObjType + ToySolver.Converter.MIP2PB + ToySolver.Converter.MIP2SMT + ToySolver.Converter.NAESAT + ToySolver.Converter.PB + ToySolver.Converter.PB2IP + ToySolver.Converter.PB2LSP + ToySolver.Converter.PBSetObj + ToySolver.Converter.PB2SMP + ToySolver.Converter.QBF2IPC + ToySolver.Converter.QUBO + 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.MIP + ToySolver.Data.MIP.Base + ToySolver.Data.MIP.FileUtils + ToySolver.Data.MIP.LPFile + ToySolver.Data.MIP.MPSFile + ToySolver.Data.MIP.Solution.CBC + ToySolver.Data.MIP.Solution.CPLEX + ToySolver.Data.MIP.Solution.GLPK + ToySolver.Data.MIP.Solution.Gurobi + ToySolver.Data.MIP.Solution.SCIP + ToySolver.Data.MIP.Solver + ToySolver.Data.MIP.Solver.Base + ToySolver.Data.MIP.Solver.CBC + ToySolver.Data.MIP.Solver.CPLEX + ToySolver.Data.MIP.Solver.Glpsol + ToySolver.Data.MIP.Solver.GurobiCl + ToySolver.Data.MIP.Solver.LPSolve + ToySolver.Data.MIP.Solver.SCIP + 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.FileFormat + ToySolver.FileFormat.Base + ToySolver.FileFormat.CNF + ToySolver.Graph.ShortestPath + ToySolver.MaxCut + ToySolver.QBF + ToySolver.QUBO + ToySolver.SAT + ToySolver.SAT.Config + ToySolver.SAT.Encoder.Integer + ToySolver.SAT.Encoder.PB + ToySolver.SAT.Encoder.PB.Internal.Adder + 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.Tseitin + ToySolver.SAT.ExistentialQuantification + ToySolver.SAT.MessagePassing.SurveyPropagation + 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.SLS.ProbSAT + ToySolver.SAT.Store.CNF + ToySolver.SAT.Store.PB + ToySolver.SAT.TheorySolver + ToySolver.SAT.Types + ToySolver.SAT.Printer + ToySolver.SDP + ToySolver.SMT + ToySolver.Text.CNF + ToySolver.Text.GCNF + ToySolver.Text.QDimacs + ToySolver.Text.SDPFile + ToySolver.Text.WCNF + 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.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 + -- GHC-Prof-Options: -auto-all + +Executable toysolver + Main-is: toysolver.hs + HS-Source-Dirs: app + Build-Depends: + array, + base, + containers, + data-default-class, + filepath, + OptDir, + optparse-applicative, + pseudo-boolean, + scientific, + toysolver + Default-Language: Haskell2010 + Other-Extensions: CPP + GHC-Options: -rtsopts -threaded + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + 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: app/toysat + Build-Depends: + array, + base, + bytestring, + containers, + clock, + data-default, + data-default-class, + directory, + filepath, + megaparsec, + mwc-random, + optparse-applicative, + process >=1.1.0.2, + pseudo-boolean, + scientific, + temporary, + time, + toysolver, + unbounded-delays, + vector + Default-Language: Haskell2010 + Other-Extensions: ScopedTypeVariables, CPP + GHC-Options: -rtsopts -threaded + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + if flag(WithZlib) + CPP-Options: "-DWITH_ZLIB" + if flag(LinuxStatic) + GHC-Options: -static -optl-static -optl-pthread + +Executable toysmt + 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: + base, + 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.8 + CPP-Options: "-DUSE_HASKELINE_PACKAGE" + Default-Language: Haskell2010 + Other-Extensions: ScopedTypeVariables, CPP + GHC-Options: -rtsopts + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + if flag(LinuxStatic) + GHC-Options: -static -optl-static -optl-pthread + +Executable toyqbf + Main-is: toyqbf.hs + HS-Source-Dirs: app + Build-Depends: + base, + containers, + data-default-class, + optparse-applicative, + toysolver + Default-Language: Haskell2010 + Other-Extensions: ScopedTypeVariables, CPP + GHC-Options: -rtsopts + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + 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: app + If flag(BuildToyFMF) + Build-Depends: + base, + containers, + intern, + -- logic-TPTP <=0.4.3 has build error on ghc <7.9 and transformers >=0.5.1. + -- https://github.com/DanielSchuessler/logic-TPTP/pull/4 + logic-TPTP >=0.4.4.0, + optparse-applicative, + text, + toysolver + -- logic-TPTP <=0.4.4.0 is not compatible with transformers-compat >=0.5 + if impl(ghc <7.9) + if flag(LogicTPTP045) + Build-Depends: + logic-TPTP >=0.4.5.0 + else + Build-Depends: + transformers-compat <0.5 + -- for Semigroup (as superclass of) Monoid Proposal + if impl(ghc >=8.4) + Build-Depends: logic-TPTP >=0.4.6.0 + Default-Language: Haskell2010 + Other-Extensions: CPP + GHC-Options: -rtsopts + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + if flag(LinuxStatic) + GHC-Options: -static -optl-static -optl-pthread + -- GHC-Prof-Options: -auto-all + +-- Converters + +Executable toyconvert + Main-is: toyconvert.hs + HS-Source-Dirs: app + Build-Depends: + base, + ansi-wl-pprint, + bytestring, + bytestring-builder, + data-default-class, + filepath, + optparse-applicative, + pseudo-boolean, + scientific, + text, + toysolver + Default-Language: Haskell2010 + Other-Extensions: CPP + GHC-Options: -rtsopts + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + if flag(WithZlib) + CPP-Options: "-DWITH_ZLIB" + 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: + array, + base, + toysolver + Default-Language: Haskell2010 + Other-Extensions: CPP + GHC-Options: -rtsopts + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + 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: + array, + base, + containers, + toysolver + Default-Language: Haskell2010 + Other-Extensions: CPP + GHC-Options: -rtsopts + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + 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: + array, + base, + toysolver + Default-Language: Haskell2010 + Other-Extensions: CPP + GHC-Options: -rtsopts + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + if flag(LinuxStatic) + GHC-Options: -static -optl-static -optl-pthread + +Executable numberlink + If !flag(BuildSamplePrograms) + Buildable: False + Main-is: numberlink.hs + HS-Source-Dirs: samples/programs/numberlink + Build-Depends: + array, + base, + bytestring, + containers, + data-default-class, + parsec, + pseudo-boolean, + toysolver + Default-Language: Haskell2010 + Other-Extensions: CPP + GHC-Options: -rtsopts + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + 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 + Other-Extensions: CPP + GHC-Options: -rtsopts + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + if flag(LinuxStatic) + GHC-Options: -static -optl-static -optl-pthread + +Executable assign + If !flag(BuildSamplePrograms) + Buildable: False + Main-is: assign.hs + HS-Source-Dirs: samples/programs/assign + Build-Depends: + attoparsec, + base, + bytestring, + containers, + toysolver, + vector + Default-Language: Haskell2010 + Other-Extensions: CPP + GHC-Options: -rtsopts + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + if flag(LinuxStatic) + GHC-Options: -static -optl-static -optl-pthread + +Executable shortest-path + If !flag(BuildSamplePrograms) + Buildable: False + Main-is: shortest-path.hs + HS-Source-Dirs: samples/programs/shortest-path + Build-Depends: + base, + bytestring, + containers, + unordered-containers, + toysolver + Default-Language: Haskell2010 + Other-Extensions: CPP + GHC-Options: -rtsopts + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + 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 + Other-Extensions: CPP + GHC-Options: -rtsopts + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + 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, + scientific, + split, + text, + toysolver + Default-Language: Haskell2010 + Other-Extensions: CPP + GHC-Options: -rtsopts + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + if flag(LinuxStatic) + GHC-Options: -static -optl-static -optl-pthread + +Executable survey-propagation + if !flag(BuildSamplePrograms) + Buildable: False + Main-is: survey-propagation.hs + HS-Source-Dirs: samples/programs/survey-propagation + Build-Depends: + base, + data-default-class, + toysolver + if flag(OpenCL) + Build-Depends: OpenCL + CPP-Options: "-DENABLE_OPENCL" + Default-Language: Haskell2010 + Other-Extensions: CPP + -- We use threaded RTS to avoid the error "schedule: re-entered unsafely. + -- Perhaps a 'foreign import unsafe' should be 'safe'?" on NVIDIA CUDA. + GHC-Options: -rtsopts -threaded + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + CPP-Options: "-DFORCE_CHAR8" + if flag(LinuxStatic) + GHC-Options: -static -optl-static -optl-pthread + +Executable probsat + if !flag(BuildSamplePrograms) + Buildable: False + Main-is: probsat.hs + HS-Source-Dirs: samples/programs/probsat + Build-Depends: + base, + clock, + data-default-class, + mwc-random, + optparse-applicative, + vector, + toysolver + Default-Language: Haskell2010 + Other-Extensions: CPP + GHC-Options: -rtsopts + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + CPP-Options: "-DFORCE_CHAR8" + 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: app + Build-Depends: + base, + bytestring, + containers, + pseudo-boolean, + toysolver + Default-Language: Haskell2010 + Other-Extensions: CPP + GHC-Options: -rtsopts + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + if flag(LinuxStatic) + GHC-Options: -static -optl-static -optl-pthread + +Executable maxsatverify + If !flag(BuildMiscPrograms) + Buildable: False + Main-is: maxsatverify.hs + HS-Source-Dirs: app + Build-Depends: + array, + base, + toysolver + Default-Language: Haskell2010 + Other-Extensions: CPP + GHC-Options: -rtsopts + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + if flag(LinuxStatic) + GHC-Options: -static -optl-static -optl-pthread + +Executable pbverify + Main-is: pbverify.hs + If !flag(BuildMiscPrograms) + Buildable: False + HS-Source-Dirs: app + Build-Depends: + array, + base, + pseudo-boolean, + toysolver + Default-Language: Haskell2010 + Other-Extensions: CPP + GHC-Options: -rtsopts + -- GHC-Prof-Options: -auto-all + if flag(ForceChar8) + CPP-OPtions: "-DFORCE_CHAR8" + 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, + 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.11, + tasty-th, + toysolver + Default-Language: Haskell2010 + Other-Extensions: TemplateHaskell + +Test-suite TestSuite + 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.GraphShortestPath + Test.HittingSets + Test.Knapsack + Test.LPFile + Test.Misc + Test.MIP + Test.MIPSolver + Test.MIPSolver2 + Test.MPSFile + 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: + array, + base, + bytestring, + bytestring-builder, + containers, + data-default-class, + data-interval, + deepseq, + hashable, + intern, + lattices, + megaparsec, + mtl, + mwc-random, + OptDir, + parsec >=3.1.2 && <4, + pseudo-boolean, + QuickCheck >=2.5 && <3, + scientific, + tasty >=0.10.1, + tasty-hunit >=0.9 && <0.11, + tasty-quickcheck >=0.8 && <0.11, + tasty-th, + text, + toysolver, + transformers, + transformers-compat, + unordered-containers, + vector, + vector-space + Default-Language: Haskell2010 + Other-Extensions: TemplateHaskell, ScopedTypeVariables + if flag(TestCBC) + CPP-Options: "-DTEST_CBC" + if flag(TestCPLEX) + CPP-Options: "-DTEST_CPLEX" + if flag(TestGlpsol) + CPP-Options: "-DTEST_GLPSOL" + if flag(TestGurobiCl) + CPP-Options: "-DTEST_GUROBI_CL" + if flag(TestLPSolve) + CPP-Options: "-DTEST_LP_SOLVE" + if flag(TestSCIP) + CPP-Options: "-DTEST_SCIP" + +Benchmark BenchmarkSATLIB + type: exitcode-stdio-1.0 + hs-source-dirs: benchmarks + main-is: BenchmarkSATLIB.hs + build-depends: + array, + base, + criterion >=1.0 && <1.6, + data-default-class, + toysolver + Default-Language: Haskell2010 + +Benchmark BenchmarkKnapsack + type: exitcode-stdio-1.0 + hs-source-dirs: benchmarks + main-is: BenchmarkKnapsack.hs + build-depends: + base, + criterion >=1.0 && <1.6, + toysolver + Default-Language: Haskell2010 + +Benchmark BenchmarkSubsetSum + type: exitcode-stdio-1.0 + hs-source-dirs: benchmarks + main-is: BenchmarkSubsetSum.hs + build-depends: + base, + criterion >=1.0 && <1.6, + toysolver, + vector + Default-Language: Haskell2010
revision 2
Name: toysolver Version: 0.6.0 -x-revision: 1 +x-revision: 2 License: BSD3 License-File: COPYING Author: Masahiro Sakai (masahiro.sakai@gmail.com) hashtables, heaps, intern >=0.9.1.2 && <1.0.0.0, - log-domain, + log-domain <0.13, -- numLoopState requires loop >=0.3.0 loop >=0.3.0 && < 1.0.0, mtl >=2.1.2,
revision 3
Name: toysolver Version: 0.6.0 -x-revision: 2 +x-revision: 3 License: BSD3 License-File: COPYING Author: Masahiro Sakai (masahiro.sakai@gmail.com) mwc-random >=0.13.1 && <0.15, OptDir, lattices, - megaparsec >=4 && <8, + megaparsec >=4 && <10, -- Text.PrettyPrint.HughesPJClass is available on pretty >=1.1.2.0 pretty >=1.1.2.0 && <1.2, primes, transformers, transformers-compat if flag(UseHaskeline) - Build-Depends: haskeline >=0.7 && <0.8 + Build-Depends: haskeline >=0.7 && <0.9 CPP-Options: "-DUSE_HASKELINE_PACKAGE" Default-Language: Haskell2010 Other-Extensions: ScopedTypeVariables, CPP
revision 4
Name: toysolver Version: 0.6.0 -x-revision: 3 +x-revision: 4 License: BSD3 License-File: COPYING Author: Masahiro Sakai (masahiro.sakai@gmail.com) mwc-random >=0.13.1 && <0.15, OptDir, lattices, - megaparsec >=4 && <10, + megaparsec >=4.4.0 && <10, -- Text.PrettyPrint.HughesPJClass is available on pretty >=1.1.2.0 pretty >=1.1.2.0 && <1.2, primes,
revision 5
Name: toysolver Version: 0.6.0 -x-revision: 4 +x-revision: 5 License: BSD3 License-File: COPYING Author: Masahiro Sakai (masahiro.sakai@gmail.com) bytestring-builder, data-default-class, filepath, - optparse-applicative, + optparse-applicative <0.18, pseudo-boolean, scientific, text,