<commit_before>homepage: https://github.com/msakai/toysolver/
changelog-type: markdown
hash: ed17abfa74cd61ba3eff6a5dc76d937dfa329a03b95788d0fe180c0fe0be5030
test-bench-deps:
  bytestring: -any
  mwc-random: -any
  tasty-th: -any
  base: -any
  data-default-class: -any
  unordered-containers: -any
  text: -any
  vector-space: -any
  megaparsec: -any
  toysolver: -any
  criterion: ! '>=1.0 && <1.6'
  parsec: ! '>=3.1.2 && <4'
  array: -any
  pseudo-boolean: -any
  lattices: -any
  containers: -any
  OptDir: -any
  data-interval: -any
  intern: -any
  tasty-quickcheck: ! '>=0.8 && <0.11'
  mtl: -any
  hashable: -any
  tasty-hunit: ! '>=0.9 && <0.11'
  transformers: -any
  tasty: ! '>=0.10.1'
  deepseq: -any
  scientific: -any
  bytestring-builder: -any
  QuickCheck: ! '>=2.5 && <3'
  finite-field: ! '>=0.7.0 && <1.0.0'
  pretty: -any
  transformers-compat: -any
  vector: -any
maintainer: <EMAIL>
synopsis: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
changelog: "0.6.0\n-----\n* new solvers:\n  * `ToySolver.SAT.SLS.ProbSAT` and sample
  `probsat` program\n* new converters:\n  * `ToySolver.Converter.NAESAT`\n  * `ToySolver.Converter.SAT2MaxCut`\n
  \ * `ToySolver.Converter.SAT2MaxSAT`: SAT and 3-SAT to Max-2-SAT converter\n  *
  `ToySolver.Converter.QBF2IPC`\n  * `ToySolver.Converter.QUBO`: QUBO↔IsingModel converter\n*
  new file format API:\n  * merge `ToySolver.Text.MaxSAT`, `ToySolver.Text.GCNF`,
  `ToySolver.Text.QDimacs`, and `ToySolver.Text.CNF`\n    info `ToySolver.FileFormat`
  and `ToySolver.FileFormat.CNF`\n  * allow reading/writing `gzip`ped CNF/WCNF/GCNF/QDimacs/LP/MPS
  files\n* rename modules:\n  *\t`ToySolver.Arith.Simplex2` to `ToySolver.Arith.Simplex`\n
  \ * `ToySolver.Arith.MIPSolver2` to `ToySolver.Arith.MIP`\n  * `ToySolver.Data.Var`
  to `ToySolver.Data.IntVar`\n* `ToySolver.SAT`:\n  * add `cancel` function for interruption\n
  \ * introduce `PackedClause` type\n* `ToySolver.Arith.Simplex`\n  * introduce `Config`
  data type\n  * implement bound tightening\n* switch from `System.Console.GetOpt`
  to `optparse-applicative`\n* stop supporting GHC-7.8\n\n0.5.0\n-----\n* new solvers:\n
  \ * `ToySolver.BitVector`\n  * `ToySolver.Combinatorial.BipartiteMatching`\n  *
  `ToySolver.Combinatorial.HittingSet.DAA`\n  * `ToySolver.Combinatorial.HittingSet.MARCO`\n
  \ * `ToySolver.Arith.DifferenceLogic`\n  * `ToySolver.Graph.ShortestPath`\n  * `ToySolver.QBF`\n*
  `toysat`\n  * add `--init-sp` option to initialize variable state using survey propagation\n
  \ * allow using `UBCSAT` when solving PBO/WBO problems\n* `toysmt`\n  * suport bit-vector
  logic\n* `toyconvert`\n  * `pbconvert` and `lpconvert` were merged into a single
  command `toyconvert`\n  * add `--ksat=NUMBER` option to convert to k-SAT formula\n
  \ * add `--linearlize` and `--linearizer-pb` options\n  * add `--remove-usercuts`
  option\n* add new modules to `ToySolver.Converter`\n  * `ToySolver.Converter.GCNF2MaxSAT`\n
  \ * `ToySolver.Converter.MIP2PB`\n  * `ToySolver.Converter.PBLinearlization`\n  *
  `ToySolver.Converter.SAT2KSAT`\n* `ToySolver.SAT`\n  * introduce type classes for
  adding constraints\n  * `ToySolver.SAT.Encoder.Tseitin`: add XOR and Full-adder
  encoder\n  * `ToySolver.SAT.Encoder.PB`: add functionality to encode PB constraint
  using adder networks and sorting networks\n  * `ToySolver.SAT.MUS.Enum`: add `GurvichKhachiyan1999`
  and `MARCO` to the MUS enumeration methods\n  * implement learning rate based branching
  heuristics\n  * add `ToySolver.SAT.ExistentialQuantification`\n  * add `ToySolver.SAT.Store.CNF`
  and `ToySolver.SAT.Store.PB`\n  * implement survey propagation as `ToySolver.SAT.MessagePassing.SurveyPropagation`\n*
  `Data.MIP`\n  * parameterize Problem type with coefficient type and use `Scientific`
  as default\n  * introduce `Status` type\n  * add solution file parsers: `ToySolver.Data.MIP.Solution.{CBC,CPLEX,GLPK,Gurobi,SCIP}`\n
  \ * add solver wrapper modules: `ToySolver.MIP.Solver.{CBC,CPLEX,Glpsol,GurobiCl,LPSolve,SCIP}`\n*
  add a QDimacs parser as `ToySolver.Text.QDimacs`\n* add `ToySolver.Text.CNF`, `ToySolver.Text.QDimacs`\n*
  switch to use `megaparsec`\n* use `clock` package for measuring duration\n* add
  simple numberlink solver sample\n\n0.4.0\n-----\n* add experimental SMT (Satisfiablity
  Modulo Theories) solver 'toysmt', which supports theory of uninterpreted functions
  and linear real arithmetics.\n* fix toysat to output model in Max-SAT format instead
  of PB/WBO format when solving Max-SAT problems\n* add experimental getAssumptionsImplications
  functions to ToySolver.SAT module.\n* add getFixedLiterals to ToySolver.SAT module.\n*
  use 'mwc-random' package instead of 'random' package.\n* introduce 'Config' data
  type in ToySolver.SAT to simplify configulation management.\n* add subset-sum problem
  solver\n* implement backracking and explanation generation in simplex solver and
  congruence closure solver.\n\n0.3.0\n-----\n* split OPB/WBO file library into a
  serarate 'pseudo-boolean' library.\n\n"
basic-deps:
  heaps: -any
  bytestring: ! '>=0.9.2.1 && <0.11'
  mwc-random: ! '>=0.13.1 && <0.15'
  ansi-wl-pprint: -any
  case-insensitive: -any
  haskeline: ! '>=0.7 && <0.8'
  split: -any
  stm: ! '>=2.3'
  xml-conduit: -any
  base: ! '>=4.8 && <5'
  data-default-class: -any
  time: ! '>=1.5.0'
  unordered-containers: ! '>=0.2.3 && <0.3.0'
  text: ! '>=1.1.0.0'
  vector-space: ! '>=0.8.6'
  primes: -any
  clock: ! '>=0.7.1'
  megaparsec: ! '>=4 && <8'
  unbounded-delays: -any
  toysolver: -any
  filepath: -any
  process: ! '>=1.1.0.2'
  parsec: ! '>=3.1.2 && <4'
  data-default: -any
  semigroups: ! '>=0.17'
  array: ! '>=0.4.0.0'
  pseudo-boolean: ! '>=0.1.3.0 && <0.2.0.0'
  queue: -any
  log-domain: -any
  bytestring-encoding: -any
  lattices: -any
  containers: ! '>=0.5.0'
  OptDir: -any
  loop: ! '>=0.3.0 && <1.0.0'
  hashtables: -any
  ghc-prim: -any
  data-interval: ! '>=1.0.1 && <1.4.0'
  intern: ! '>=0.9.1.2 && <1.0.0.0'
  zlib: -any
  mtl: ! '>=2.1.2'
  hashable: ! '>=1.1.2.5 && <1.3.0.0'
  attoparsec: -any
  transformers: ! '>=0.2'
  temporary: ! '>=1.2'
  optparse-applicative: -any
  sign: ! '>=0.2.0 && <1.0.0'
  deepseq: -any
  extended-reals: ! '>=0.1 && <1.0'
  scientific: -any
  bytestring-builder: -any
  multiset: -any
  finite-field: ! '>=0.9.0 && <1.0.0'
  pretty: ! '>=1.1.2.0 && <1.2'
  template-haskell: -any
  primitive: ! '>=0.6'
  transformers-compat: ! '>=0.3'
  vector: -any
  directory: -any
all-versions:
- 0.0.2
- 0.0.3
- 0.0.4
- 0.0.4.1
- 0.0.5
- 0.0.6
- 0.1.0
- 0.2.0
- 0.3.0
- 0.4.0
- 0.5.0
- 0.6.0
author: <NAME> (<EMAIL>)
latest: 0.6.0
description-type: markdown
description: "toysolver\n=========\n\n[![Join the chat at https://gitter.im/msakai/toysolver](https://badges.gitter.im/Join%20Chat.svg)](https://gitter.im/msakai/toysolver)\n\n[![Build
  Status (Travis CI)](https://secure.travis-ci.org/msakai/toysolver.svg?branch=master)](http://travis-ci.org/msakai/toysolver)\n[![Build
  Status (AppVeyor)](https://ci.appveyor.com/api/projects/status/w7g615sp8ysiqk7w/branch/master?svg=true)](https://ci.appveyor.com/project/msakai/toysolver/branch/master)\n[![Coverage
  Status](https://coveralls.io/repos/msakai/toysolver/badge.svg)](https://coveralls.io/r/msakai/toysolver)\n[![Hackage](https://img.shields.io/hackage/v/toysolver.svg)](https://hackage.haskell.org/package/toysolver)\n[![License](https://img.shields.io/badge/License-BSD%203--Clause-blue.svg)](https://opensource.org/licenses/BSD-3-Clause)\n\nIt
  provides solver implementations of various problems including SAT, SMT, Max-SAT,
  PBS (Pseudo Boolean Satisfaction), PBO (Pseudo Boolean Optimization), MILP (Mixed
  Integer Linear Programming) and non-linear real arithmetic.\n\nIn particular it
  contains moderately-fast pure-Haskell SAT solver 'toysat'.\n\nInstallation\n------------\n\n*
  unpack\n* cd toysolver\n* cabal install\n\nUsage\n-----\n\nThis package includes
  several commands.\n\n### toysolver\n\nArithmetic solver for the following problems:\n\n*
  Mixed Integer Liner Programming (MILP or MIP)\n* Boolean SATisfiability problem
  (SAT)\n* PB\n    * Pseudo Boolean Satisfaction (PBS)\n    * Pseudo Boolean Optimization
  (PBO)\n    * Weighted Boolean Optimization (WBO)\n* Max-SAT families\n    * Max-SAT\n
  \   * Partial Max-SAT\n    * Weighted Max-SAT\n    * Weighted Partial Max-SAT\n*
  Real Closed Field\n\nUsage:\n\n    toysolver [OPTION...] [file.lp|file.mps]\n    toysolver
  --lp [OPTION...] [file.lp|file.mps]\n    toysolver --sat [OPTION...] [file.cnf]\n
  \   toysolver --pb [OPTION...] [file.opb]\n    toysolver --wbo [OPTION...] [file.wbo]\n
  \   toysolver --maxsat [OPTION...] [file.cnf|file.wcnf]\n\n    -h  --help           show
  help\n    -v  --version        show version number\n        --solver=SOLVER  mip
  (default), omega-test, cooper, cad, old-mip, ct\n\n### toysat\n\nSAT-based solver
  for the following problems:\n\n* SAT\n    * Boolean SATisfiability problem (SAT)\n
  \   * Minimally Unsatisfiable Subset (MUS)\n    * Group-Oriented MUS (GMUS)\n* PB\n
  \   * Pseudo Boolean Satisfaction (PBS)\n    * Pseudo Boolean Optimization (PBO)\n
  \   * Weighted Boolean Optimization (WBO)\n* Max-SAT families\n    * Max-SAT\n    *
  Partial Max-SAT\n    * Weighted Max-SAT\n    * Weighted Partial Max-SAT\n* Integer
  Programming (all variables must be bounded)\n\nUsage:\n\n    toysat [file.cnf|-]\n
  \   toysat --sat [file.cnf|-]\n    toysat --mus [file.gcnf|file.cnf|-]\n    toysat
  --pb [file.opb|-]\n    toysat --wbo [file.wbo|-]\n    toysat --maxsat [file.cnf|file.wcnf|-]\n
  \   toysat --lp [file.lp|file.mps|-]\n\nPB'12 competition result: \n\n* toysat placed
  2nd in PARTIAL-BIGINT-LIN and SOFT-BIGINT-LIN categories\n* toysat placed 4th in
  PARTIAL-SMALLINT-LIN and SOFT-SMALLINT-LIN categories\n* toysat placed 8th in OPT-BIGINT-LIN
  category\n\n### toysmt\n\nSMT solver based on toysat.\n\nUsage:\n\n    toysmt [file.smt2]\n\nCurrently
  only QF_UF, QF_RDL, QF_LRA, QF_UFRDL and QF_UFLRA logic are supported.\n\n### toyfmf\n\nSAT-based
  finite model finder for first order logic (FOL).\n\nUsage:\n\n    toyfmf [file.tptp]
  [size]\n\n### toyconvert\n\nConverter between various problem files.\n\nUsage:\n\n
  \   toyconvert -o [outputfile] [inputfile]\n\nSupported formats:\n\n* Input formats:
  .cnf .wcnf .opb .wbo .gcnf .lp .mps\n* Output formats: .cnf .wcnf .opb .wbo .lsp
  .lp .mps .smp .smt2 .ys\n\nBindings\n--------\n\n* [ersatz-toysat](http://hackage.haskell.org/package/ersatz-toysat)
  -  toysat backend driver for [ersatz](http://hackage.haskell.org/package/ersatz)\n*
  [satchmo-toysat](http://hackage.haskell.org/package/satchmo-toysat) - toysat backend
  driver for [satchmo](http://hackage.haskell.org/package/satchmo)\n"
license-name: BSD-3-Clause
<commit_msg>Update from Hackage at 2019-10-13T05:37:37Z<commit_after>homepage: https://github.com/msakai/toysolver/
changelog-type: markdown
hash: 06d8bbda8c98ebde2d7d4cf1d22c04130694bea5bbd015a1f0578e8c91d1383f
test-bench-deps:
  bytestring: -any
  mwc-random: -any
  tasty-th: -any
  base: -any
  data-default-class: -any
  unordered-containers: -any
  text: -any
  vector-space: -any
  megaparsec: -any
  toysolver: -any
  criterion: ! '>=1.0 && <1.6'
  parsec: ! '>=3.1.2 && <4'
  array: -any
  pseudo-boolean: -any
  lattices: -any
  containers: -any
  OptDir: -any
  data-interval: -any
  intern: -any
  tasty-quickcheck: ! '>=0.8 && <0.11'
  mtl: -any
  hashable: -any
  tasty-hunit: ! '>=0.9 && <0.11'
  transformers: -any
  tasty: ! '>=0.10.1'
  deepseq: -any
  scientific: -any
  bytestring-builder: -any
  QuickCheck: ! '>=2.5 && <3'
  finite-field: ! '>=0.7.0 && <1.0.0'
  pretty: -any
  transformers-compat: -any
  vector: -any
maintainer: <EMAIL>
synopsis: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
changelog: "0.6.0\n-----\n* new solvers:\n  * `ToySolver.SAT.SLS.ProbSAT` and sample
  `probsat` program\n* new converters:\n  * `ToySolver.Converter.NAESAT`\n  * `ToySolver.Converter.SAT2MaxCut`\n
  \ * `ToySolver.Converter.SAT2MaxSAT`: SAT and 3-SAT to Max-2-SAT converter\n  *
  `ToySolver.Converter.QBF2IPC`\n  * `ToySolver.Converter.QUBO`: QUBO↔IsingModel converter\n*
  new file format API:\n  * merge `ToySolver.Text.MaxSAT`, `ToySolver.Text.GCNF`,
  `ToySolver.Text.QDimacs`, and `ToySolver.Text.CNF`\n    info `ToySolver.FileFormat`
  and `ToySolver.FileFormat.CNF`\n  * allow reading/writing `gzip`ped CNF/WCNF/GCNF/QDimacs/LP/MPS
  files\n* rename modules:\n  *\t`ToySolver.Arith.Simplex2` to `ToySolver.Arith.Simplex`\n
  \ * `ToySolver.Arith.MIPSolver2` to `ToySolver.Arith.MIP`\n  * `ToySolver.Data.Var`
  to `ToySolver.Data.IntVar`\n* `ToySolver.SAT`:\n  * add `cancel` function for interruption\n
  \ * introduce `PackedClause` type\n* `ToySolver.Arith.Simplex`\n  * introduce `Config`
  data type\n  * implement bound tightening\n* switch from `System.Console.GetOpt`
  to `optparse-applicative`\n* stop supporting GHC-7.8\n\n0.5.0\n-----\n* new solvers:\n
  \ * `ToySolver.BitVector`\n  * `ToySolver.Combinatorial.BipartiteMatching`\n  *
  `ToySolver.Combinatorial.HittingSet.DAA`\n  * `ToySolver.Combinatorial.HittingSet.MARCO`\n
  \ * `ToySolver.Arith.DifferenceLogic`\n  * `ToySolver.Graph.ShortestPath`\n  * `ToySolver.QBF`\n*
  `toysat`\n  * add `--init-sp` option to initialize variable state using survey propagation\n
  \ * allow using `UBCSAT` when solving PBO/WBO problems\n* `toysmt`\n  * suport bit-vector
  logic\n* `toyconvert`\n  * `pbconvert` and `lpconvert` were merged into a single
  command `toyconvert`\n  * add `--ksat=NUMBER` option to convert to k-SAT formula\n
  \ * add `--linearlize` and `--linearizer-pb` options\n  * add `--remove-usercuts`
  option\n* add new modules to `ToySolver.Converter`\n  * `ToySolver.Converter.GCNF2MaxSAT`\n
  \ * `ToySolver.Converter.MIP2PB`\n  * `ToySolver.Converter.PBLinearlization`\n  *
  `ToySolver.Converter.SAT2KSAT`\n* `ToySolver.SAT`\n  * introduce type classes for
  adding constraints\n  * `ToySolver.SAT.Encoder.Tseitin`: add XOR and Full-adder
  encoder\n  * `ToySolver.SAT.Encoder.PB`: add functionality to encode PB constraint
  using adder networks and sorting networks\n  * `ToySolver.SAT.MUS.Enum`: add `GurvichKhachiyan1999`
  and `MARCO` to the MUS enumeration methods\n  * implement learning rate based branching
  heuristics\n  * add `ToySolver.SAT.ExistentialQuantification`\n  * add `ToySolver.SAT.Store.CNF`
  and `ToySolver.SAT.Store.PB`\n  * implement survey propagation as `ToySolver.SAT.MessagePassing.SurveyPropagation`\n*
  `Data.MIP`\n  * parameterize Problem type with coefficient type and use `Scientific`
  as default\n  * introduce `Status` type\n  * add solution file parsers: `ToySolver.Data.MIP.Solution.{CBC,CPLEX,GLPK,Gurobi,SCIP}`\n
  \ * add solver wrapper modules: `ToySolver.MIP.Solver.{CBC,CPLEX,Glpsol,GurobiCl,LPSolve,SCIP}`\n*
  add a QDimacs parser as `ToySolver.Text.QDimacs`\n* add `ToySolver.Text.CNF`, `ToySolver.Text.QDimacs`\n*
  switch to use `megaparsec`\n* use `clock` package for measuring duration\n* add
  simple numberlink solver sample\n\n0.4.0\n-----\n* add experimental SMT (Satisfiablity
  Modulo Theories) solver 'toysmt', which supports theory of uninterpreted functions
  and linear real arithmetics.\n* fix toysat to output model in Max-SAT format instead
  of PB/WBO format when solving Max-SAT problems\n* add experimental getAssumptionsImplications
  functions to ToySolver.SAT module.\n* add getFixedLiterals to ToySolver.SAT module.\n*
  use 'mwc-random' package instead of 'random' package.\n* introduce 'Config' data
  type in ToySolver.SAT to simplify configulation management.\n* add subset-sum problem
  solver\n* implement backracking and explanation generation in simplex solver and
  congruence closure solver.\n\n0.3.0\n-----\n* split OPB/WBO file library into a
  serarate 'pseudo-boolean' library.\n\n"
basic-deps:
  heaps: -any
  bytestring: ! '>=0.9.2.1 && <0.11'
  mwc-random: ! '>=0.13.1 && <0.15'
  ansi-wl-pprint: -any
  case-insensitive: -any
  haskeline: ! '>=0.7 && <0.8'
  split: -any
  stm: ! '>=2.3'
  xml-conduit: -any
  base: ! '>=4.8 && <5'
  data-default-class: -any
  time: ! '>=1.5.0'
  unordered-containers: ! '>=0.2.3 && <0.3.0'
  text: ! '>=1.1.0.0'
  vector-space: ! '>=0.8.6'
  primes: -any
  clock: ! '>=0.7.1'
  megaparsec: ! '>=4 && <8'
  unbounded-delays: -any
  toysolver: -any
  filepath: -any
  process: ! '>=1.1.0.2'
  parsec: ! '>=3.1.2 && <4'
  data-default: -any
  semigroups: ! '>=0.17'
  array: ! '>=0.4.0.0'
  pseudo-boolean: ! '>=0.1.3.0 && <0.2.0.0'
  queue: -any
  log-domain: -any
  bytestring-encoding: -any
  lattices: -any
  containers: ! '>=0.5.0'
  OptDir: -any
  loop: ! '>=0.3.0 && <1.0.0'
  hashtables: -any
  ghc-prim: -any
  data-interval: ! '>=1.0.1 && <1.4.0'
  intern: ! '>=0.9.1.2 && <1.0.0.0'
  zlib: -any
  mtl: ! '>=2.1.2'
  hashable: ! '>=1.1.2.5 && <1.4.0.0'
  attoparsec: -any
  transformers: ! '>=0.2'
  temporary: ! '>=1.2'
  optparse-applicative: -any
  sign: ! '>=0.2.0 && <1.0.0'
  deepseq: -any
  extended-reals: ! '>=0.1 && <1.0'
  scientific: -any
  bytestring-builder: -any
  multiset: -any
  finite-field: ! '>=0.9.0 && <1.0.0'
  pretty: ! '>=1.1.2.0 && <1.2'
  template-haskell: -any
  primitive: ! '>=0.6'
  transformers-compat: ! '>=0.3'
  vector: -any
  directory: -any
all-versions:
- 0.0.2
- 0.0.3
- 0.0.4
- 0.0.4.1
- 0.0.5
- 0.0.6
- 0.1.0
- 0.2.0
- 0.3.0
- 0.4.0
- 0.5.0
- 0.6.0
author: <NAME> (<EMAIL>)
latest: 0.6.0
description-type: markdown
description: "toysolver\n=========\n\n[![Join the chat at https://gitter.im/msakai/toysolver](https://badges.gitter.im/Join%20Chat.svg)](https://gitter.im/msakai/toysolver)\n\n[![Build
  Status (Travis CI)](https://secure.travis-ci.org/msakai/toysolver.svg?branch=master)](http://travis-ci.org/msakai/toysolver)\n[![Build
  Status (AppVeyor)](https://ci.appveyor.com/api/projects/status/w7g615sp8ysiqk7w/branch/master?svg=true)](https://ci.appveyor.com/project/msakai/toysolver/branch/master)\n[![Coverage
  Status](https://coveralls.io/repos/msakai/toysolver/badge.svg)](https://coveralls.io/r/msakai/toysolver)\n[![Hackage](https://img.shields.io/hackage/v/toysolver.svg)](https://hackage.haskell.org/package/toysolver)\n[![License](https://img.shields.io/badge/License-BSD%203--Clause-blue.svg)](https://opensource.org/licenses/BSD-3-Clause)\n\nIt
  provides solver implementations of various problems including SAT, SMT, Max-SAT,
  PBS (Pseudo Boolean Satisfaction), PBO (Pseudo Boolean Optimization), MILP (Mixed
  Integer Linear Programming) and non-linear real arithmetic.\n\nIn particular it
  contains moderately-fast pure-Haskell SAT solver 'toysat'.\n\nInstallation\n------------\n\n*
  unpack\n* cd toysolver\n* cabal install\n\nUsage\n-----\n\nThis package includes
  several commands.\n\n### toysolver\n\nArithmetic solver for the following problems:\n\n*
  Mixed Integer Liner Programming (MILP or MIP)\n* Boolean SATisfiability problem
  (SAT)\n* PB\n    * Pseudo Boolean Satisfaction (PBS)\n    * Pseudo Boolean Optimization
  (PBO)\n    * Weighted Boolean Optimization (WBO)\n* Max-SAT families\n    * Max-SAT\n
  \   * Partial Max-SAT\n    * Weighted Max-SAT\n    * Weighted Partial Max-SAT\n*
  Real Closed Field\n\nUsage:\n\n    toysolver [OPTION...] [file.lp|file.mps]\n    toysolver
  --lp [OPTION...] [file.lp|file.mps]\n    toysolver --sat [OPTION...] [file.cnf]\n
  \   toysolver --pb [OPTION...] [file.opb]\n    toysolver --wbo [OPTION...] [file.wbo]\n
  \   toysolver --maxsat [OPTION...] [file.cnf|file.wcnf]\n\n    -h  --help           show
  help\n    -v  --version        show version number\n        --solver=SOLVER  mip
  (default), omega-test, cooper, cad, old-mip, ct\n\n### toysat\n\nSAT-based solver
  for the following problems:\n\n* SAT\n    * Boolean SATisfiability problem (SAT)\n
  \   * Minimally Unsatisfiable Subset (MUS)\n    * Group-Oriented MUS (GMUS)\n* PB\n
  \   * Pseudo Boolean Satisfaction (PBS)\n    * Pseudo Boolean Optimization (PBO)\n
  \   * Weighted Boolean Optimization (WBO)\n* Max-SAT families\n    * Max-SAT\n    *
  Partial Max-SAT\n    * Weighted Max-SAT\n    * Weighted Partial Max-SAT\n* Integer
  Programming (all variables must be bounded)\n\nUsage:\n\n    toysat [file.cnf|-]\n
  \   toysat --sat [file.cnf|-]\n    toysat --mus [file.gcnf|file.cnf|-]\n    toysat
  --pb [file.opb|-]\n    toysat --wbo [file.wbo|-]\n    toysat --maxsat [file.cnf|file.wcnf|-]\n
  \   toysat --lp [file.lp|file.mps|-]\n\nPB'12 competition result: \n\n* toysat placed
  2nd in PARTIAL-BIGINT-LIN and SOFT-BIGINT-LIN categories\n* toysat placed 4th in
  PARTIAL-SMALLINT-LIN and SOFT-SMALLINT-LIN categories\n* toysat placed 8th in OPT-BIGINT-LIN
  category\n\n### toysmt\n\nSMT solver based on toysat.\n\nUsage:\n\n    toysmt [file.smt2]\n\nCurrently
  only QF_UF, QF_RDL, QF_LRA, QF_UFRDL and QF_UFLRA logic are supported.\n\n### toyfmf\n\nSAT-based
  finite model finder for first order logic (FOL).\n\nUsage:\n\n    toyfmf [file.tptp]
  [size]\n\n### toyconvert\n\nConverter between various problem files.\n\nUsage:\n\n
  \   toyconvert -o [outputfile] [inputfile]\n\nSupported formats:\n\n* Input formats:
  .cnf .wcnf .opb .wbo .gcnf .lp .mps\n* Output formats: .cnf .wcnf .opb .wbo .lsp
  .lp .mps .smp .smt2 .ys\n\nBindings\n--------\n\n* [ersatz-toysat](http://hackage.haskell.org/package/ersatz-toysat)
  -  toysat backend driver for [ersatz](http://hackage.haskell.org/package/ersatz)\n*
  [satchmo-toysat](http://hackage.haskell.org/package/satchmo-toysat) - toysat backend
  driver for [satchmo](http://hackage.haskell.org/package/satchmo)\n"
license-name: BSD-3-Clause

{'fraction_non_alphanumeric': 0.17057628370890285, 'fraction_numerical': 0.026967122275581824, 'mean_word_length': 3.3619335347432022, 'pattern_counts': {'":': 0, '<': 53, '<?xml version=': 0, '>': 83, 'https://': 26, 'lorem ipsum': 0, 'www.': 0, 'xml': 2}, 'pii_count': 24, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2614015', 'n_tokens_mistral': 9277, 'n_tokens_neox': 8978, 'n_words': 1778}