Cabal revisions of toysolver-0.9.0
Hackage metadata revisions edit the .cabal file after upload; each diff below is one revision.
revision 1
-cabal-version: 2.4-Name: toysolver-Version: 0.9.0-License: BSD-3-Clause-License-File: COPYING-Author: Masahiro Sakai (masahiro.sakai@gmail.com)-Maintainer: masahiro.sakai@gmail.com-Category: Algorithms, Optimisation, Optimization, Theorem Provers, Constraints, Logic, Formal Methods, SMT-Synopsis: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc-Description: Toy-level solver implementation of various problems including SAT, SMT, Max-SAT, PBS/PBO (Pseudo Boolean Satisfaction/Optimization), MILP (Mixed Integer Linear Programming) and non-linear real arithmetic.-Homepage: https://github.com/msakai/toysolver/-Bug-Reports: https://github.com/msakai/toysolver/issues-Tested-With:- GHC ==8.6.3- GHC ==8.8.4- GHC ==8.10.7- GHC ==9.0.2- GHC ==9.2.8- GHC ==9.4.8- GHC ==9.6.6- GHC ==9.8.2-Extra-Doc-Files:- README.md- INSTALL.md- CHANGELOG.markdown- COPYING- COPYING-GPL-Extra-Source-Files:- app/toysat-ipasir/ipasir.h- app/toysat-ipasir/ipasir.map- src/ToySolver/Data/Polyhedron.hs- samples/gcnf/*.cnf- samples/gcnf/*.gcnf- samples/lp/*.lp- samples/lp/*.sol- samples/lp/*.txt- samples/lp/error/*.lp- samples/maxsat/*.cnf- samples/maxsat/*.wcnf- samples/mps/*.mps- samples/pbo/*.opb- samples/pbs/*.opb- samples/sat/*.cnf- samples/wbo/*.wbo- samples/sdp/*.dat- samples/sdp/*.dat-s- samples/smt/*.smt2- samples/smt/*.ys- samples/qbf/*.qdimacs- samples/programs/sudoku/*.sdk- samples/programs/knapsack/README.md- samples/programs/knapsack/*.txt- samples/programs/htc/test1.dat- samples/programs/htc/test2.dat- samples/programs/svm2lp/a1a- samples/programs/nonogram/*.cwd- samples/programs/nonogram/README.md- samples/programs/numberlink/README.md- samples/programs/numberlink/ADC2013/*.txt- samples/programs/numberlink/ADC2014_QA/A/*.txt- samples/programs/numberlink/ADC2014_QA/Q/*.txt- samples/programs/numberlink/ADC2016/sample/01/*.txt- benchmarks/UF250.1065.100/*.cnf- benchmarks/UUF250.1065.100/*.cnf-Build-Type: Simple--Flag ForceChar8- Description: set default encoding to char8 (not to use iconv)- Default: False- Manual: True--Flag LinuxStatic- Description: build statically linked binaries- Default: False- Manual: True--Flag WithZlib- Description: Use zlib package to support gzipped files- Default: True- Manual: True--Flag BuildToyFMF- Description: build toyfmf command- Default: False- Manual: True--Flag BuildForeignLibraries- Description: build foreign libraries- Default: True- Manual: True --Flag BuildSamplePrograms- Description: build sample programs- Default: False- Manual: True--Flag BuildMiscPrograms- Description: build misc programs- Default: False- Manual: True--Flag UseHaskeline- Description: use haskeline package- Manual: True- Default: True--Flag OpenCL- Description: use opencl package (deprecated)- Manual: True- Default: False--Flag ExtraBoundsChecking- Description: enable extra bounds checking for debugging- Manual: True- Default: False--Flag optparse-applicative-018- Description: use optparse-applicative >=0.18- Manual: False- Default: False--source-repository head- type: git- location: git://github.com/msakai/toysolver.git--Library- Exposed: True- Hs-source-dirs: src- Build-Depends:- aeson >=1.4.2.0 && <2.3,- array >=0.5,- -- GHC >=8.6 && <9.11- base >=4.12 && <4.21,- bytestring >=0.9.2.1 && <0.13,- bytestring-builder,- bytestring-encoding >=0.1.1.0,- case-insensitive,- clock >=0.7.1,- -- IntMap.restrictKeys and IntMap.withoutKeys require containers >=0.5.8- containers >=0.5.8,- data-default,- data-default-class,- data-interval >=2.0.1 && <2.2.0,- deepseq,- directory,- extended-reals >=0.1 && <1.0,- filepath,- finite-field >=0.9.0 && <1.0.0,- -- hashUsing is available on hashable >=1.2- hashable >=1.2 && <1.6.0.0,- hashtables,- heaps,- intern >=0.9.1.2 && <1.0.0.0,- log-domain,- -- numLoopState requires loop >=0.3.0- loop >=0.3.0 && < 1.0.0,- MIP >=0.2.0.0 && <0.3,- mtl >=2.1.2,- multiset,- -- createSystemRandom requires mwc-random >=0.13.1.0- mwc-random >=0.13.1 && <0.16,- OptDir,- lattices,- megaparsec >=7 && <10,- -- Text.PrettyPrint.HughesPJClass is available on pretty >=1.1.2.0- pretty >=1.1.2.0 && <1.2,- primes,- primitive >=0.6,- process >=1.1.0.2,- pseudo-boolean >=0.1.3.0 && <0.2.0.0,- queue,- scientific,- semigroups >=0.17,- sign >=0.2.0 && <1.0.0,- stm >=2.3,- template-haskell,- temporary >=1.2,- text >=1.1.0.0,- -- defaultTimeLocale is available on time >=1.5.0- time >=1.5.0,- transformers >=0.2,- transformers-compat >=0.3,- unordered-containers >=0.2.3 && <0.3.0,- -- imapM and modify are available on vector >=0.11.0- vector >=0.11,- vector-space >=0.8.6,- xml-conduit- if flag(WithZlib)- Build-Depends: zlib- CPP-Options: "-DWITH_ZLIB"- if flag(ExtraBoundsChecking)- CPP-Options: "-DEXTRA_BOUNDS_CHECKING"- if impl(ghc)- Build-Depends: ghc-prim- Default-Language: Haskell2010- Other-Extensions:- BangPatterns- CPP- ConstraintKinds- DeriveDataTypeable- DeriveGeneric- ExistentialQuantification- FlexibleContexts- FlexibleInstances- FunctionalDependencies- GADTs- GeneralizedNewtypeDeriving- InstanceSigs- KindSignatures- MultiParamTypeClasses- OverloadedStrings- PatternSynonyms- Rank2Types- RecursiveDo- ScopedTypeVariables- TemplateHaskell- TypeFamilies- TypeOperators- TypeSynonymInstances- UndecidableInstances- ViewPatterns- if impl(ghc)- Other-Extensions:- MagicHash- UnboxedTuples- Exposed-Modules:- ToySolver.Arith.BoundsInference- ToySolver.Arith.CAD- ToySolver.Arith.ContiTraverso- ToySolver.Arith.Cooper- ToySolver.Arith.Cooper.Base- ToySolver.Arith.Cooper.FOL- ToySolver.Arith.DifferenceLogic- ToySolver.Arith.FourierMotzkin- ToySolver.Arith.FourierMotzkin.Base- ToySolver.Arith.FourierMotzkin.FOL- ToySolver.Arith.FourierMotzkin.Optimization- ToySolver.Arith.LPUtil- ToySolver.Arith.MIP- ToySolver.Arith.OmegaTest- ToySolver.Arith.OmegaTest.Base- ToySolver.Arith.Simplex- ToySolver.Arith.Simplex.Simple- ToySolver.Arith.Simplex.Textbook- ToySolver.Arith.Simplex.Textbook.LPSolver- ToySolver.Arith.Simplex.Textbook.LPSolver.Simple- ToySolver.Arith.Simplex.Textbook.MIPSolver.Simple- ToySolver.Arith.VirtualSubstitution- ToySolver.BitVector- ToySolver.BitVector.Base- ToySolver.BitVector.Solver- ToySolver.EUF.CongruenceClosure- ToySolver.EUF.EUFSolver- ToySolver.EUF.FiniteModelFinder- ToySolver.Combinatorial.BipartiteMatching- ToySolver.Combinatorial.HittingSet.DAA- ToySolver.Combinatorial.HittingSet.MARCO- ToySolver.Combinatorial.HittingSet.Simple- ToySolver.Combinatorial.HittingSet.HTCBDD- ToySolver.Combinatorial.HittingSet.InterestingSets- ToySolver.Combinatorial.HittingSet.SHD- ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996- ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999- ToySolver.Combinatorial.HittingSet.Util- ToySolver.Combinatorial.Knapsack.BB- ToySolver.Combinatorial.Knapsack.DPDense- ToySolver.Combinatorial.Knapsack.DPSparse- ToySolver.Combinatorial.SubsetSum- ToySolver.Converter- ToySolver.Converter.Base- ToySolver.Converter.GCNF2MaxSAT- ToySolver.Converter.MIP2SMT- ToySolver.Converter.NAESAT- ToySolver.Converter.PB- ToySolver.Converter.MIP- ToySolver.Converter.QBF2IPC- ToySolver.Converter.QUBO- ToySolver.Converter.SAT2MIS- ToySolver.Converter.SAT2KSAT- ToySolver.Converter.SAT2MaxCut- ToySolver.Converter.SAT2MaxSAT- ToySolver.Converter.Tseitin- ToySolver.Data.AlgebraicNumber.Complex- ToySolver.Data.AlgebraicNumber.Real- ToySolver.Data.AlgebraicNumber.Root- ToySolver.Data.AlgebraicNumber.Sturm- ToySolver.Data.Boolean- ToySolver.Data.BoolExpr- ToySolver.Data.Delta- ToySolver.Data.DNF- ToySolver.Data.FOL.Arith- ToySolver.Data.FOL.Formula- ToySolver.Data.IntVar- ToySolver.Data.LA- ToySolver.Data.LA.FOL- ToySolver.Data.LBool- ToySolver.Data.OrdRel- ToySolver.Data.Polynomial- ToySolver.Data.Polynomial.Factorization.FiniteField- ToySolver.Data.Polynomial.Factorization.Hensel- ToySolver.Data.Polynomial.Factorization.Hensel.Internal- ToySolver.Data.Polynomial.Factorization.Integer- ToySolver.Data.Polynomial.Factorization.Kronecker- ToySolver.Data.Polynomial.Factorization.Rational- ToySolver.Data.Polynomial.Factorization.SquareFree- ToySolver.Data.Polynomial.Factorization.Zassenhaus- ToySolver.Data.Polynomial.GroebnerBasis- ToySolver.Data.Polynomial.Interpolation.Hermite- ToySolver.Data.Polynomial.Interpolation.Lagrange- ToySolver.FileFormat- ToySolver.FileFormat.Base- ToySolver.FileFormat.CNF- ToySolver.Graph.Base- ToySolver.Graph.ShortestPath- ToySolver.Graph.MaxCut- ToySolver.QBF- ToySolver.QUBO- ToySolver.SAT- ToySolver.SAT.Encoder.Integer- ToySolver.SAT.Encoder.PB- ToySolver.SAT.Encoder.PB.Internal.Adder- ToySolver.SAT.Encoder.PB.Internal.BCCNF- ToySolver.SAT.Encoder.PB.Internal.BDD- ToySolver.SAT.Encoder.PB.Internal.Sorter- ToySolver.SAT.Encoder.PBNLC- ToySolver.SAT.Encoder.Cardinality- ToySolver.SAT.Encoder.Cardinality.Internal.Naive- ToySolver.SAT.Encoder.Cardinality.Internal.ParallelCounter- ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer- ToySolver.SAT.Encoder.Tseitin- ToySolver.SAT.ExistentialQuantification- ToySolver.SAT.Formula- ToySolver.SAT.MUS- ToySolver.SAT.MUS.Enum- ToySolver.SAT.MUS.Types- ToySolver.SAT.PBO- ToySolver.SAT.PBO.Context- ToySolver.SAT.PBO.BC- ToySolver.SAT.PBO.BCD- ToySolver.SAT.PBO.BCD2- ToySolver.SAT.PBO.MSU4- ToySolver.SAT.PBO.UnsatBased- ToySolver.SAT.Solver.CDCL- ToySolver.SAT.Solver.CDCL.Config- ToySolver.SAT.Solver.MessagePassing.SurveyPropagation- ToySolver.SAT.Solver.SLS.ProbSAT- ToySolver.SAT.Solver.SLS.UBCSAT- ToySolver.SAT.Store.CNF- ToySolver.SAT.Store.PB- ToySolver.SAT.TheorySolver- ToySolver.SAT.Types- ToySolver.SAT.Printer- ToySolver.SDP- ToySolver.SMT- ToySolver.Text.SDPFile- ToySolver.Internal.Data.IndexedPriorityQueue- ToySolver.Internal.Data.IOURef- ToySolver.Internal.Data.PriorityQueue- ToySolver.Internal.Data.SeqQueue- ToySolver.Internal.Data.Vec- ToySolver.Internal.ProcessUtil- ToySolver.Internal.TextUtil- ToySolver.Internal.Util- ToySolver.Wang- ToySolver.Version- Other-Modules:- ToySolver.Converter.PB.Internal.LargestIntersectionFinder- ToySolver.Converter.PB.Internal.Product- ToySolver.Data.AlgebraicNumber.Graeffe- ToySolver.Data.Polynomial.Base- ToySolver.Internal.JSON- ToySolver.SAT.Internal.JSON- ToySolver.SAT.MUS.Base- ToySolver.SAT.MUS.Deletion- ToySolver.SAT.MUS.Insertion- ToySolver.SAT.MUS.QuickXplain- ToySolver.SAT.MUS.Enum.Base- ToySolver.SAT.MUS.Enum.CAMUS- ToySolver.Version.TH- Paths_toysolver- autogen-modules:- Paths_toysolver- -- GHC-Prof-Options: -auto-all--Executable toysolver- Main-is: toysolver.hs- HS-Source-Dirs: app- Build-Depends:- array,- base >=4.12 && <4.21,- containers,- data-default-class,- filepath,- MIP,- OptDir,- -- maybeReader is available on optparse-applicative >=0.13.0.0- optparse-applicative >=0.13,- pseudo-boolean,- scientific,- toysolver- 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- HS-Source-Dirs: app/toysat- Build-Depends:- array,- base >=4.12 && <4.21,- bytestring,- containers,- clock,- data-default-class,- filepath,- megaparsec,- MIP,- mwc-random,- -- maybeReader is available on optparse-applicative >=0.13.0.0- optparse-applicative >=0.13,- pseudo-boolean,- scientific,- time,- toysolver,- unbounded-delays,- vector- 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--Foreign-Library toysat-ipasir- type: native-shared- if !flag(BuildForeignLibraries)- buildable: False- if os(Windows)- options: standalone- mod-def-file: app/toysat-ipasir/ipasir.def- if os(Linux)- ld-options: -Wl,--version-script=app/toysat-ipasir/ipasir.map- build-depends:- base >=4.12 && <4.21,- containers,- toysolver- hs-source-dirs: app/toysat-ipasir- include-dirs: app/toysat-ipasir- c-sources: app/toysat-ipasir/cbits.c- cc-options: -Wall- cpp-options: -DIPASIR_SHARED_LIB -DBUILDING_IPASIR_SHARED_LIB- includes: ipasir.h- other-modules: IPASIR- default-language: Haskell2010--Executable toysmt- 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 >=4.12 && <4.21,- containers,- -- TODO: remove intern dependency- intern,- mtl,- optparse-applicative,- parsec >=3.1.2 && <4,- toysolver,- text,- transformers,- transformers-compat- if flag(UseHaskeline)- Build-Depends: haskeline >=0.7 && <0.9- CPP-Options: "-DUSE_HASKELINE_PACKAGE"- 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 >=4.12 && <4.21,- 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 >=4.12 && <4.21,- containers,- intern,- logic-TPTP >=0.4.6.0 && <0.7,- optparse-applicative,- text,- 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- -- GHC-Prof-Options: -auto-all---- Converters--Executable toyconvert- Main-is: toyconvert.hs- HS-Source-Dirs: app- Build-Depends:- aeson,- base >=4.12 && <4.21,- bytestring,- bytestring-builder,- containers,- data-default-class,- filepath,- MIP,- pseudo-boolean,- scientific,- text,- toysolver- if flag(optparse-applicative-018)- Build-Depends:- optparse-applicative >=0.18,- prettyprinter >=1- else- Build-Depends:- optparse-applicative <0.18,- ansi-wl-pprint- 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 >=4.12 && <4.21,- 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 >=4.12 && <4.21,- 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 >=4.12 && <4.21,- 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 >=4.12 && <4.21,- 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 >=4.12 && <4.21,- 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 >=4.12 && <4.21,- 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 >=4.12 && <4.21,- 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 >=4.12 && <4.21,- 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 >=4.12 && <4.21,- containers,- data-default-class,- MIP,- 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 >=4.12 && <4.21,- data-default-class,- 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 probsat- if !flag(BuildSamplePrograms)- Buildable: False - Main-is: probsat.hs- HS-Source-Dirs: samples/programs/probsat- Build-Depends:- base >=4.12 && <4.21,- 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 >=4.12 && <4.21,- 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 >=4.12 && <4.21,- 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 >=4.12 && <4.21,- 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 >=4.12 && <4.21,- containers,- data-interval,- finite-field >=0.7.0 && <1.0.0,- pretty,- tasty >=0.10.1,- tasty-hunit >=0.9 && <0.11,- tasty-quickcheck >=0.8 && <0.12,- tasty-th,- toysolver- Default-Language: Haskell2010- Other-Extensions:- DataKinds- 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.Graph- Test.GraphShortestPath- Test.HittingSets- Test.Knapsack- Test.Misc- Test.MIPSolver- Test.ProbSAT- Test.QBF- Test.QUBO- Test.SAT- Test.SAT.Encoder- Test.SAT.ExistentialQuantification- Test.SAT.MUS- Test.SAT.TheorySolver- Test.SAT.Types- Test.SAT.Utils- Test.SDPFile- Test.Simplex- Test.SimplexTextbook- Test.SMT- Test.SMTLIB2Solver- Test.Smtlib- Test.SubsetSum- ToySolver.SMT.SMTLIB2Solver- Smtlib.Parsers.CommonParsers- Smtlib.Parsers.ResponseParsers- Smtlib.Parsers.CommandsParsers- Smtlib.Syntax.Syntax- Smtlib.Syntax.ShowSL- Build-depends:- aeson,- array,- base >=4.12 && <4.21,- bytestring,- bytestring-builder,- containers,- data-default-class,- data-interval,- deepseq,- hashable,- intern,- lattices,- megaparsec,- MIP,- mtl,- mwc-random,- OptDir,- parsec >=3.1.2 && <4,- pseudo-boolean,- -- sublistOf is available on QuickCheck >=2.8- QuickCheck >=2.8 && <3,- scientific,- tasty >=0.10.1,- tasty-hunit >=0.9 && <0.11,- tasty-quickcheck >=0.8 && <0.12,- tasty-th,- text,- toysolver,- transformers,- transformers-compat,- unordered-containers,- vector,- vector-space- Default-Language: Haskell2010- Other-Extensions:- CPP- DataKinds- FlexibleContexts- LambdaCase- ScopedTypeVariables- TemplateHaskell- TupleSections--Benchmark BenchmarkSATLIB- type: exitcode-stdio-1.0- hs-source-dirs: benchmarks- main-is: BenchmarkSATLIB.hs- build-depends:- array,- base >=4.12 && <4.21,- criterion >=1.0 && <1.7,- 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 >=4.12 && <4.21,- criterion >=1.0 && <1.7,- toysolver- Default-Language: Haskell2010--Benchmark BenchmarkSubsetSum- type: exitcode-stdio-1.0- hs-source-dirs: benchmarks- main-is: BenchmarkSubsetSum.hs- build-depends:- base >=4.12 && <4.21,- criterion >=1.0 && <1.7,- toysolver,- vector- Default-Language: Haskell2010+cabal-version: 2.4 +Name: toysolver +Version: 0.9.0 +x-revision: 1 +License: BSD-3-Clause +License-File: COPYING +Author: Masahiro Sakai (masahiro.sakai@gmail.com) +Maintainer: masahiro.sakai@gmail.com +Category: Algorithms, Optimisation, Optimization, Theorem Provers, Constraints, Logic, Formal Methods, SMT +Synopsis: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc +Description: Toy-level solver implementation of various problems including SAT, SMT, Max-SAT, PBS/PBO (Pseudo Boolean Satisfaction/Optimization), MILP (Mixed Integer Linear Programming) and non-linear real arithmetic. +Homepage: https://github.com/msakai/toysolver/ +Bug-Reports: https://github.com/msakai/toysolver/issues +Tested-With: + GHC ==8.6.3 + GHC ==8.8.4 + GHC ==8.10.7 + GHC ==9.0.2 + GHC ==9.2.8 + GHC ==9.4.8 + GHC ==9.6.6 + GHC ==9.8.2 +Extra-Doc-Files: + README.md + INSTALL.md + CHANGELOG.markdown + COPYING + COPYING-GPL +Extra-Source-Files: + app/toysat-ipasir/ipasir.h + app/toysat-ipasir/ipasir.map + src/ToySolver/Data/Polyhedron.hs + samples/gcnf/*.cnf + samples/gcnf/*.gcnf + samples/lp/*.lp + samples/lp/*.sol + samples/lp/*.txt + samples/lp/error/*.lp + samples/maxsat/*.cnf + samples/maxsat/*.wcnf + samples/mps/*.mps + samples/pbo/*.opb + samples/pbs/*.opb + samples/sat/*.cnf + samples/wbo/*.wbo + samples/sdp/*.dat + samples/sdp/*.dat-s + samples/smt/*.smt2 + samples/smt/*.ys + samples/qbf/*.qdimacs + samples/programs/sudoku/*.sdk + samples/programs/knapsack/README.md + samples/programs/knapsack/*.txt + samples/programs/htc/test1.dat + samples/programs/htc/test2.dat + samples/programs/svm2lp/a1a + samples/programs/nonogram/*.cwd + samples/programs/nonogram/README.md + samples/programs/numberlink/README.md + samples/programs/numberlink/ADC2013/*.txt + samples/programs/numberlink/ADC2014_QA/A/*.txt + samples/programs/numberlink/ADC2014_QA/Q/*.txt + samples/programs/numberlink/ADC2016/sample/01/*.txt + benchmarks/UF250.1065.100/*.cnf + benchmarks/UUF250.1065.100/*.cnf +Build-Type: Simple + +Flag ForceChar8 + Description: set default encoding to char8 (not to use iconv) + Default: False + Manual: True + +Flag LinuxStatic + Description: build statically linked binaries + Default: False + Manual: True + +Flag WithZlib + Description: Use zlib package to support gzipped files + Default: True + Manual: True + +Flag BuildToyFMF + Description: build toyfmf command + Default: False + Manual: True + +Flag BuildForeignLibraries + Description: build foreign libraries + Default: True + Manual: True + +Flag BuildSamplePrograms + Description: build sample programs + Default: False + Manual: True + +Flag BuildMiscPrograms + Description: build misc programs + Default: False + Manual: True + +Flag UseHaskeline + Description: use haskeline package + Manual: True + Default: True + +Flag OpenCL + Description: use opencl package (deprecated) + Manual: True + Default: False + +Flag ExtraBoundsChecking + Description: enable extra bounds checking for debugging + Manual: True + Default: False + +Flag optparse-applicative-018 + Description: use optparse-applicative >=0.18 + Manual: False + Default: False + +source-repository head + type: git + location: git://github.com/msakai/toysolver.git + +Library + Exposed: True + Hs-source-dirs: src + Build-Depends: + aeson >=1.4.2.0 && <2.3, + array >=0.5, + -- GHC >=8.6 && <9.13 + base >=4.12 && <4.22, + bytestring >=0.9.2.1 && <0.13, + bytestring-builder, + bytestring-encoding >=0.1.1.0, + case-insensitive, + clock >=0.7.1, + -- IntMap.restrictKeys and IntMap.withoutKeys require containers >=0.5.8 + containers >=0.5.8, + data-default, + data-default-class, + data-interval >=2.0.1 && <2.2.0, + deepseq, + directory, + extended-reals >=0.1 && <1.0, + filepath, + finite-field >=0.9.0 && <1.0.0, + -- hashUsing is available on hashable >=1.2 + hashable >=1.2 && <1.6.0.0, + hashtables, + heaps, + intern >=0.9.1.2 && <1.0.0.0, + log-domain, + -- numLoopState requires loop >=0.3.0 + loop >=0.3.0 && < 1.0.0, + MIP >=0.2.0.0 && <0.3, + mtl >=2.1.2, + multiset, + -- createSystemRandom requires mwc-random >=0.13.1.0 + mwc-random >=0.13.1 && <0.16, + OptDir, + lattices, + megaparsec >=7 && <10, + -- Text.PrettyPrint.HughesPJClass is available on pretty >=1.1.2.0 + pretty >=1.1.2.0 && <1.2, + primes, + primitive >=0.6, + process >=1.1.0.2, + pseudo-boolean >=0.1.3.0 && <0.2.0.0, + queue, + scientific, + semigroups >=0.17, + sign >=0.2.0 && <1.0.0, + stm >=2.3, + template-haskell, + temporary >=1.2, + text >=1.1.0.0, + -- defaultTimeLocale is available on time >=1.5.0 + time >=1.5.0, + transformers >=0.2, + transformers-compat >=0.3, + unordered-containers >=0.2.3 && <0.3.0, + -- imapM and modify are available on vector >=0.11.0 + vector >=0.11, + vector-space >=0.8.6, + xml-conduit + if flag(WithZlib) + Build-Depends: zlib + CPP-Options: "-DWITH_ZLIB" + if flag(ExtraBoundsChecking) + CPP-Options: "-DEXTRA_BOUNDS_CHECKING" + if impl(ghc) + Build-Depends: ghc-prim + Default-Language: Haskell2010 + Other-Extensions: + BangPatterns + CPP + ConstraintKinds + DeriveDataTypeable + DeriveGeneric + ExistentialQuantification + FlexibleContexts + FlexibleInstances + FunctionalDependencies + GADTs + GeneralizedNewtypeDeriving + InstanceSigs + KindSignatures + MultiParamTypeClasses + OverloadedStrings + PatternSynonyms + Rank2Types + RecursiveDo + ScopedTypeVariables + TemplateHaskell + TypeFamilies + TypeOperators + TypeSynonymInstances + UndecidableInstances + ViewPatterns + if impl(ghc) + Other-Extensions: + MagicHash + UnboxedTuples + Exposed-Modules: + ToySolver.Arith.BoundsInference + ToySolver.Arith.CAD + ToySolver.Arith.ContiTraverso + ToySolver.Arith.Cooper + ToySolver.Arith.Cooper.Base + ToySolver.Arith.Cooper.FOL + ToySolver.Arith.DifferenceLogic + ToySolver.Arith.FourierMotzkin + ToySolver.Arith.FourierMotzkin.Base + ToySolver.Arith.FourierMotzkin.FOL + ToySolver.Arith.FourierMotzkin.Optimization + ToySolver.Arith.LPUtil + ToySolver.Arith.MIP + ToySolver.Arith.OmegaTest + ToySolver.Arith.OmegaTest.Base + ToySolver.Arith.Simplex + ToySolver.Arith.Simplex.Simple + ToySolver.Arith.Simplex.Textbook + ToySolver.Arith.Simplex.Textbook.LPSolver + ToySolver.Arith.Simplex.Textbook.LPSolver.Simple + ToySolver.Arith.Simplex.Textbook.MIPSolver.Simple + ToySolver.Arith.VirtualSubstitution + ToySolver.BitVector + ToySolver.BitVector.Base + ToySolver.BitVector.Solver + ToySolver.EUF.CongruenceClosure + ToySolver.EUF.EUFSolver + ToySolver.EUF.FiniteModelFinder + ToySolver.Combinatorial.BipartiteMatching + ToySolver.Combinatorial.HittingSet.DAA + ToySolver.Combinatorial.HittingSet.MARCO + ToySolver.Combinatorial.HittingSet.Simple + ToySolver.Combinatorial.HittingSet.HTCBDD + ToySolver.Combinatorial.HittingSet.InterestingSets + ToySolver.Combinatorial.HittingSet.SHD + ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996 + ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999 + ToySolver.Combinatorial.HittingSet.Util + ToySolver.Combinatorial.Knapsack.BB + ToySolver.Combinatorial.Knapsack.DPDense + ToySolver.Combinatorial.Knapsack.DPSparse + ToySolver.Combinatorial.SubsetSum + ToySolver.Converter + ToySolver.Converter.Base + ToySolver.Converter.GCNF2MaxSAT + ToySolver.Converter.MIP2SMT + ToySolver.Converter.NAESAT + ToySolver.Converter.PB + ToySolver.Converter.MIP + ToySolver.Converter.QBF2IPC + ToySolver.Converter.QUBO + ToySolver.Converter.SAT2MIS + ToySolver.Converter.SAT2KSAT + ToySolver.Converter.SAT2MaxCut + ToySolver.Converter.SAT2MaxSAT + ToySolver.Converter.Tseitin + ToySolver.Data.AlgebraicNumber.Complex + ToySolver.Data.AlgebraicNumber.Real + ToySolver.Data.AlgebraicNumber.Root + ToySolver.Data.AlgebraicNumber.Sturm + ToySolver.Data.Boolean + ToySolver.Data.BoolExpr + ToySolver.Data.Delta + ToySolver.Data.DNF + ToySolver.Data.FOL.Arith + ToySolver.Data.FOL.Formula + ToySolver.Data.IntVar + ToySolver.Data.LA + ToySolver.Data.LA.FOL + ToySolver.Data.LBool + ToySolver.Data.OrdRel + ToySolver.Data.Polynomial + ToySolver.Data.Polynomial.Factorization.FiniteField + ToySolver.Data.Polynomial.Factorization.Hensel + ToySolver.Data.Polynomial.Factorization.Hensel.Internal + ToySolver.Data.Polynomial.Factorization.Integer + ToySolver.Data.Polynomial.Factorization.Kronecker + ToySolver.Data.Polynomial.Factorization.Rational + ToySolver.Data.Polynomial.Factorization.SquareFree + ToySolver.Data.Polynomial.Factorization.Zassenhaus + ToySolver.Data.Polynomial.GroebnerBasis + ToySolver.Data.Polynomial.Interpolation.Hermite + ToySolver.Data.Polynomial.Interpolation.Lagrange + ToySolver.FileFormat + ToySolver.FileFormat.Base + ToySolver.FileFormat.CNF + ToySolver.Graph.Base + ToySolver.Graph.ShortestPath + ToySolver.Graph.MaxCut + ToySolver.QBF + ToySolver.QUBO + ToySolver.SAT + ToySolver.SAT.Encoder.Integer + ToySolver.SAT.Encoder.PB + ToySolver.SAT.Encoder.PB.Internal.Adder + ToySolver.SAT.Encoder.PB.Internal.BCCNF + ToySolver.SAT.Encoder.PB.Internal.BDD + ToySolver.SAT.Encoder.PB.Internal.Sorter + ToySolver.SAT.Encoder.PBNLC + ToySolver.SAT.Encoder.Cardinality + ToySolver.SAT.Encoder.Cardinality.Internal.Naive + ToySolver.SAT.Encoder.Cardinality.Internal.ParallelCounter + ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer + ToySolver.SAT.Encoder.Tseitin + ToySolver.SAT.ExistentialQuantification + ToySolver.SAT.Formula + ToySolver.SAT.MUS + ToySolver.SAT.MUS.Enum + ToySolver.SAT.MUS.Types + ToySolver.SAT.PBO + ToySolver.SAT.PBO.Context + ToySolver.SAT.PBO.BC + ToySolver.SAT.PBO.BCD + ToySolver.SAT.PBO.BCD2 + ToySolver.SAT.PBO.MSU4 + ToySolver.SAT.PBO.UnsatBased + ToySolver.SAT.Solver.CDCL + ToySolver.SAT.Solver.CDCL.Config + ToySolver.SAT.Solver.MessagePassing.SurveyPropagation + ToySolver.SAT.Solver.SLS.ProbSAT + ToySolver.SAT.Solver.SLS.UBCSAT + ToySolver.SAT.Store.CNF + ToySolver.SAT.Store.PB + ToySolver.SAT.TheorySolver + ToySolver.SAT.Types + ToySolver.SAT.Printer + ToySolver.SDP + ToySolver.SMT + ToySolver.Text.SDPFile + ToySolver.Internal.Data.IndexedPriorityQueue + ToySolver.Internal.Data.IOURef + ToySolver.Internal.Data.PriorityQueue + ToySolver.Internal.Data.SeqQueue + ToySolver.Internal.Data.Vec + ToySolver.Internal.ProcessUtil + ToySolver.Internal.TextUtil + ToySolver.Internal.Util + ToySolver.Wang + ToySolver.Version + Other-Modules: + ToySolver.Converter.PB.Internal.LargestIntersectionFinder + ToySolver.Converter.PB.Internal.Product + ToySolver.Data.AlgebraicNumber.Graeffe + ToySolver.Data.Polynomial.Base + ToySolver.Internal.JSON + ToySolver.SAT.Internal.JSON + ToySolver.SAT.MUS.Base + ToySolver.SAT.MUS.Deletion + ToySolver.SAT.MUS.Insertion + ToySolver.SAT.MUS.QuickXplain + ToySolver.SAT.MUS.Enum.Base + ToySolver.SAT.MUS.Enum.CAMUS + ToySolver.Version.TH + Paths_toysolver + autogen-modules: + Paths_toysolver + -- GHC-Prof-Options: -auto-all + +Executable toysolver + Main-is: toysolver.hs + HS-Source-Dirs: app + Build-Depends: + array, + base >=4.12 && <4.21, + containers, + data-default-class, + filepath, + MIP, + OptDir, + -- maybeReader is available on optparse-applicative >=0.13.0.0 + optparse-applicative >=0.13, + pseudo-boolean, + scientific, + toysolver + 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 + HS-Source-Dirs: app/toysat + Build-Depends: + array, + base >=4.12 && <4.21, + bytestring, + containers, + clock, + data-default-class, + filepath, + megaparsec, + MIP, + mwc-random, + -- maybeReader is available on optparse-applicative >=0.13.0.0 + optparse-applicative >=0.13, + pseudo-boolean, + scientific, + time, + toysolver, + unbounded-delays, + vector + 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 + +Foreign-Library toysat-ipasir + type: native-shared + if !flag(BuildForeignLibraries) + buildable: False + if os(Windows) + options: standalone + mod-def-file: app/toysat-ipasir/ipasir.def + if os(Linux) + ld-options: -Wl,--version-script=app/toysat-ipasir/ipasir.map + build-depends: + base >=4.12 && <4.21, + containers, + toysolver + hs-source-dirs: app/toysat-ipasir + include-dirs: app/toysat-ipasir + c-sources: app/toysat-ipasir/cbits.c + cc-options: -Wall + cpp-options: -DIPASIR_SHARED_LIB -DBUILDING_IPASIR_SHARED_LIB + includes: ipasir.h + other-modules: IPASIR + default-language: Haskell2010 + +Executable toysmt + 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 >=4.12 && <4.21, + containers, + -- TODO: remove intern dependency + intern, + mtl, + optparse-applicative, + parsec >=3.1.2 && <4, + toysolver, + text, + transformers, + transformers-compat + if flag(UseHaskeline) + Build-Depends: haskeline >=0.7 && <0.9 + CPP-Options: "-DUSE_HASKELINE_PACKAGE" + 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 >=4.12 && <4.21, + 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 >=4.12 && <4.21, + containers, + intern, + logic-TPTP >=0.4.6.0 && <0.7, + optparse-applicative, + text, + 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 + -- GHC-Prof-Options: -auto-all + +-- Converters + +Executable toyconvert + Main-is: toyconvert.hs + HS-Source-Dirs: app + Build-Depends: + aeson, + base >=4.12 && <4.21, + bytestring, + bytestring-builder, + containers, + data-default-class, + filepath, + MIP, + pseudo-boolean, + scientific, + text, + toysolver + if flag(optparse-applicative-018) + Build-Depends: + optparse-applicative >=0.18, + prettyprinter >=1 + else + Build-Depends: + optparse-applicative <0.18, + ansi-wl-pprint + 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 >=4.12 && <4.21, + 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 >=4.12 && <4.21, + 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 >=4.12 && <4.21, + 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 >=4.12 && <4.21, + 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 >=4.12 && <4.21, + 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 >=4.12 && <4.21, + 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 >=4.12 && <4.21, + 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 >=4.12 && <4.21, + 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 >=4.12 && <4.21, + containers, + data-default-class, + MIP, + 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 >=4.12 && <4.21, + data-default-class, + 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 probsat + if !flag(BuildSamplePrograms) + Buildable: False + Main-is: probsat.hs + HS-Source-Dirs: samples/programs/probsat + Build-Depends: + base >=4.12 && <4.21, + 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 >=4.12 && <4.21, + 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 >=4.12 && <4.21, + 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 >=4.12 && <4.21, + 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 >=4.12 && <4.21, + containers, + data-interval, + finite-field >=0.7.0 && <1.0.0, + pretty, + tasty >=0.10.1, + tasty-hunit >=0.9 && <0.11, + tasty-quickcheck >=0.8 && <0.12, + tasty-th, + toysolver + Default-Language: Haskell2010 + Other-Extensions: + DataKinds + 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.Graph + Test.GraphShortestPath + Test.HittingSets + Test.Knapsack + Test.Misc + Test.MIPSolver + Test.ProbSAT + Test.QBF + Test.QUBO + Test.SAT + Test.SAT.Encoder + Test.SAT.ExistentialQuantification + Test.SAT.MUS + Test.SAT.TheorySolver + Test.SAT.Types + Test.SAT.Utils + Test.SDPFile + Test.Simplex + Test.SimplexTextbook + Test.SMT + Test.SMTLIB2Solver + Test.Smtlib + Test.SubsetSum + ToySolver.SMT.SMTLIB2Solver + Smtlib.Parsers.CommonParsers + Smtlib.Parsers.ResponseParsers + Smtlib.Parsers.CommandsParsers + Smtlib.Syntax.Syntax + Smtlib.Syntax.ShowSL + Build-depends: + aeson, + array, + base >=4.12 && <4.21, + bytestring, + bytestring-builder, + containers, + data-default-class, + data-interval, + deepseq, + hashable, + intern, + lattices, + megaparsec, + MIP, + mtl, + mwc-random, + OptDir, + parsec >=3.1.2 && <4, + pseudo-boolean, + -- sublistOf is available on QuickCheck >=2.8 + QuickCheck >=2.8 && <3, + scientific, + tasty >=0.10.1, + tasty-hunit >=0.9 && <0.11, + tasty-quickcheck >=0.8 && <0.12, + tasty-th, + text, + toysolver, + transformers, + transformers-compat, + unordered-containers, + vector, + vector-space + Default-Language: Haskell2010 + Other-Extensions: + CPP + DataKinds + FlexibleContexts + LambdaCase + ScopedTypeVariables + TemplateHaskell + TupleSections + +Benchmark BenchmarkSATLIB + type: exitcode-stdio-1.0 + hs-source-dirs: benchmarks + main-is: BenchmarkSATLIB.hs + build-depends: + array, + base >=4.12 && <4.21, + criterion >=1.0 && <1.7, + 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 >=4.12 && <4.21, + criterion >=1.0 && <1.7, + toysolver + Default-Language: Haskell2010 + +Benchmark BenchmarkSubsetSum + type: exitcode-stdio-1.0 + hs-source-dirs: benchmarks + main-is: BenchmarkSubsetSum.hs + build-depends: + base >=4.12 && <4.21, + criterion >=1.0 && <1.7, + toysolver, + vector + Default-Language: Haskell2010
revision 2
cabal-version: 2.4 Name: toysolver Version: 0.9.0 -x-revision: 1 +x-revision: 2 License: BSD-3-Clause License-File: COPYING Author: Masahiro Sakai (masahiro.sakai@gmail.com) HS-Source-Dirs: app Build-Depends: array, - base >=4.12 && <4.21, + base >=4.12 && <4.22, containers, data-default-class, filepath, HS-Source-Dirs: app/toysat Build-Depends: array, - base >=4.12 && <4.21, + base >=4.12 && <4.22, bytestring, containers, clock, if os(Linux) ld-options: -Wl,--version-script=app/toysat-ipasir/ipasir.map build-depends: - base >=4.12 && <4.21, + base >=4.12 && <4.22, containers, toysolver hs-source-dirs: app/toysat-ipasir Smtlib.Syntax.Syntax, Smtlib.Syntax.ShowSL Build-Depends: - base >=4.12 && <4.21, + base >=4.12 && <4.22, containers, -- TODO: remove intern dependency intern, Main-is: toyqbf.hs HS-Source-Dirs: app Build-Depends: - base >=4.12 && <4.21, + base >=4.12 && <4.22, containers, data-default-class, optparse-applicative, HS-Source-Dirs: app If flag(BuildToyFMF) Build-Depends: - base >=4.12 && <4.21, + base >=4.12 && <4.22, containers, intern, logic-TPTP >=0.4.6.0 && <0.7, HS-Source-Dirs: app Build-Depends: aeson, - base >=4.12 && <4.21, + base >=4.12 && <4.22, bytestring, bytestring-builder, containers, HS-Source-Dirs: samples/programs/sudoku Build-Depends: array, - base >=4.12 && <4.21, + base >=4.12 && <4.22, toysolver Default-Language: Haskell2010 Other-Extensions: CPP HS-Source-Dirs: samples/programs/nonogram Build-Depends: array, - base >=4.12 && <4.21, + base >=4.12 && <4.22, containers, toysolver Default-Language: Haskell2010 HS-Source-Dirs: samples/programs/nqueens Build-Depends: array, - base >=4.12 && <4.21, + base >=4.12 && <4.22, toysolver Default-Language: Haskell2010 Other-Extensions: CPP HS-Source-Dirs: samples/programs/numberlink Build-Depends: array, - base >=4.12 && <4.21, + base >=4.12 && <4.22, bytestring, containers, data-default-class, Main-is: knapsack.hs HS-Source-Dirs: samples/programs/knapsack Build-Depends: - base >=4.12 && <4.21, + base >=4.12 && <4.22, toysolver Default-Language: Haskell2010 Other-Extensions: CPP HS-Source-Dirs: samples/programs/assign Build-Depends: attoparsec, - base >=4.12 && <4.21, + base >=4.12 && <4.22, bytestring, containers, toysolver, Main-is: shortest-path.hs HS-Source-Dirs: samples/programs/shortest-path Build-Depends: - base >=4.12 && <4.21, + base >=4.12 && <4.22, bytestring, containers, unordered-containers, Main-is: htc.hs HS-Source-Dirs: samples/programs/htc Build-Depends: - base >=4.12 && <4.21, + base >=4.12 && <4.22, containers, toysolver Default-Language: Haskell2010 Main-is: svm2lp.hs HS-Source-Dirs: samples/programs/svm2lp Build-Depends: - base >=4.12 && <4.21, + base >=4.12 && <4.22, containers, data-default-class, MIP, Main-is: survey-propagation.hs HS-Source-Dirs: samples/programs/survey-propagation Build-Depends: - base >=4.12 && <4.21, + base >=4.12 && <4.22, data-default-class, toysolver Default-Language: Haskell2010 Main-is: probsat.hs HS-Source-Dirs: samples/programs/probsat Build-Depends: - base >=4.12 && <4.21, + base >=4.12 && <4.22, clock, data-default-class, mwc-random, Main-is: pigeonhole.hs HS-Source-Dirs: app Build-Depends: - base >=4.12 && <4.21, + base >=4.12 && <4.22, bytestring, containers, pseudo-boolean, HS-Source-Dirs: app Build-Depends: array, - base >=4.12 && <4.21, + base >=4.12 && <4.22, toysolver Default-Language: Haskell2010 Other-Extensions: CPP HS-Source-Dirs: app Build-Depends: array, - base >=4.12 && <4.21, + base >=4.12 && <4.22, pseudo-boolean, toysolver Default-Language: Haskell2010 HS-Source-Dirs: test Main-is: TestPolynomial.hs Build-depends: - base >=4.12 && <4.21, + base >=4.12 && <4.22, containers, data-interval, finite-field >=0.7.0 && <1.0.0, Build-depends: aeson, array, - base >=4.12 && <4.21, + base >=4.12 && <4.22, bytestring, bytestring-builder, containers, main-is: BenchmarkSATLIB.hs build-depends: array, - base >=4.12 && <4.21, + base >=4.12 && <4.22, criterion >=1.0 && <1.7, data-default-class, toysolver hs-source-dirs: benchmarks main-is: BenchmarkKnapsack.hs build-depends: - base >=4.12 && <4.21, + base >=4.12 && <4.22, criterion >=1.0 && <1.7, toysolver Default-Language: Haskell2010 hs-source-dirs: benchmarks main-is: BenchmarkSubsetSum.hs build-depends: - base >=4.12 && <4.21, + base >=4.12 && <4.22, criterion >=1.0 && <1.7, toysolver, vector