Name: toysolver Version: 0.7.0 x-revision: 5 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: 2.0 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.0.2 GHC ==8.2.2 GHC ==8.4.4 GHC ==8.6.5 GHC ==8.8.4 GHC ==8.10.2 Extra-Source-Files: README.md CHANGELOG.markdown COPYING COPYING-GPL app/toysat-ipasir/ipasir.h app/toysat-ipasir/ipasir.map 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/Solver/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 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 UseHaskeline Description: use haskeline package Manual: True Default: True Flag OpenCL Description: use opencl package Manual: True Default: False Flag ExtraBoundsChecking Description: enable extra bounds checking for debugging 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.5, -- GHC >=8.0 base >=4.9 && <4.15, bytestring >=0.9.2.1 && <0.12, 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, 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.5.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.1.1.0 && <0.2, mtl >=2.1.2, multiset, -- createSystemRandom requires mwc-random >=0.13.1.0 mwc-random >=0.13.1 && <0.16, OptDir, lattices, megaparsec >=5 && <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(OpenCL) Build-Depends: OpenCL >=1.0.3.4 Exposed-Modules: ToySolver.SAT.Solver.MessagePassing.SurveyPropagation.OpenCL if flag(ExtraBoundsChecking) CPP-Options: "-DEXTRA_BOUNDS_CHECKING" if impl(ghc) Build-Depends: ghc-prim Default-Language: Haskell2010 Other-Extensions: BangPatterns CPP ConstraintKinds DeriveDataTypeable ExistentialQuantification FlexibleContexts FlexibleInstances FunctionalDependencies GADTs GeneralizedNewtypeDeriving InstanceSigs KindSignatures MultiParamTypeClasses OverloadedStrings Rank2Types RecursiveDo ScopedTypeVariables TemplateHaskell TypeFamilies TypeOperators TypeSynonymInstances UndecidableInstances 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.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.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.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.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 autogen-modules: 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, 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, 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 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, 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, 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, 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.6.0 && <0.5, 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: base, ansi-wl-pprint, bytestring, bytestring-builder, data-default-class, filepath, MIP, optparse-applicative <0.18, 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, 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, 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.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: 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, -- 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.11, tasty-th, text, toysolver, transformers, transformers-compat, unordered-containers, vector, vector-space Default-Language: Haskell2010 Other-Extensions: CPP DataKinds ScopedTypeVariables TemplateHaskell 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