<commit_before>homepage: https://github.com/ucsd-progsys/liquid-fixpoint
changelog-type: ''
hash: 96f4f1f5fdaefbedc31a32fea08cd357821d0e5846ccadb46a7282276b234961
test-bench-deps:
  base: -any
  text: -any
  filepath: -any
  process: -any
  tasty-hunit: -any
  tasty-rerun: ! '>=1.1'
  tasty: ! '>=0.10'
  directory: -any
maintainer: <EMAIL>
synopsis: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
changelog: ''
basic-deps:
  cereal: -any
  bytestring: -any
  filemanip: -any
  base: ! '>=4.7 && <5'
  unordered-containers: -any
  text: -any
  syb: -any
  dotgen: -any
  filepath: -any
  process: -any
  async: -any
  parsec: -any
  array: -any
  containers: -any
  ansi-terminal: -any
  bifunctors: -any
  binary: -any
  ghc-prim: -any
  fgl-visualize: -any
  intern: -any
  liquid-fixpoint: -any
  fgl: -any
  mtl: -any
  cmdargs: -any
  hashable: -any
  attoparsec: -any
  transformers: -any
  parallel: -any
  text-format: -any
  deepseq: -any
  boxes: -any
  pretty: -any
  ascii-progress: ! '>=0.3'
  directory: -any
all-versions:
- '0.1.0.0'
- '0.2.0.0'
- '0.2.1.0'
- '0.2.1.1'
- '0.2.2.0'
- '0.2.3.0'
- '0.2.3.1'
- '0.2.3.2'
- '0.3.0.0'
- '0.3.0.1'
- '0.4.0.0'
- '0.5.0.0'
- '0.5.0.1'
author: <NAME>, <NAME>, <NAME>
latest: '0.5.0.1'
description-type: haddock
description: ! 'This package is a Haskell wrapper to the SMTLIB-based

  Horn-Clause/Logical Implication constraint solver used

  for Liquid Types.


  The package includes:


  1. Types for Expressions, Predicates, Constraints, Solutions


  2. Code for solving constraints


  Requirements


  In addition to the .cabal dependencies you require


  - A Z3 (<http://z3.codeplex.com>) or CVC4 (<http://cvc4.cs.nyu.edu>) binary.'
license-name: BSD3<commit_msg>Update from Hackage at 2017-05-02T18:25:20Z<commit_after>homepage: https://github.com/ucsd-progsys/liquid-fixpoint
changelog-type: markdown
hash: 5f50c91b21d17c0f44efdc3aaef3516071ce2cd6375b6a0a68ece4c849c9f33c
test-bench-deps:
  base: -any
  text: -any
  filepath: -any
  process: -any
  liquid-fixpoint: -any
  tasty-hunit: -any
  tasty-rerun: ! '>=1.1'
  tasty: ! '>=0.10'
  directory: -any
maintainer: <EMAIL>
synopsis: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
changelog: ! "# CHANGES\n\n## NEXT\n\n## 0.3.0.0\n\n- Make interpreted mul and div
  the default, when `solver = z3`\n- Use `higherorder` flag to allow higher order
  binders into the environment \n\n## 0.2.2.0\n\n- Added support for theory of Arrays
  `Map_t`, `Map_select`, `Map_store`\n\n- Added support for theory of Bitvectors --
  see `Language.Fixpoint.Smt.Bitvector`\n\n- Added support for string literals\n\n##
  0.2.1.0\n\n- Pre-compiled binaries of the underlying ocaml solver are now\n  provided
  for Linux, Mac OSX, and Windows.\n\n  No more need to install Ocaml!\n\n## 0.2.0.0\n\n-
  Parsing has been improved to require *much* fewer parentheses.\n\n- Experimental
  support for Z3's theory of real numbers with the `--real` flag.\n"
basic-deps:
  cereal: -any
  bytestring: -any
  filemanip: -any
  base: ! '>=4.8 && <5'
  time: -any
  unordered-containers: -any
  text: -any
  syb: -any
  dotgen: -any
  filepath: -any
  process: -any
  async: -any
  parsec: -any
  array: -any
  containers: -any
  ansi-terminal: -any
  bifunctors: -any
  binary: -any
  ghc-prim: -any
  fgl-visualize: -any
  intern: -any
  liquid-fixpoint: -any
  fgl: -any
  mtl: -any
  cmdargs: -any
  hashable: -any
  attoparsec: -any
  transformers: -any
  parallel: -any
  text-format: -any
  deepseq: -any
  boxes: -any
  pretty: -any
  ascii-progress: ! '>=0.3'
  directory: -any
all-versions:
- '0.1.0.0'
- '0.2.0.0'
- '0.2.1.0'
- '0.2.1.1'
- '0.2.2.0'
- '0.2.3.0'
- '0.2.3.1'
- '0.2.3.2'
- '0.3.0.0'
- '0.3.0.1'
- '0.4.0.0'
- '0.5.0.0'
- '0.5.0.1'
- '0.6.0.1'
author: <NAME>, <NAME>, <NAME>
latest: '0.6.0.1'
description-type: markdown
description: ! "Liquid Fixpoint [![Hackage](https://img.shields.io/hackage/v/liquid-fixpoint.svg)](https://hackage.haskell.org/package/liquid-fixpoint)
  [![Hackage-Deps](https://img.shields.io/hackage-deps/v/liquid-fixpoint.svg)](http://packdeps.haskellers.com/feed?needle=liquid-fixpoint)
  [![Build Status](https://img.shields.io/travis/ucsd-progsys/liquid-fixpoint/master.svg)](https://travis-ci.org/ucsd-progsys/liquid-fixpoint)\n===============\n\n\nThis
  package implements a Horn-Clause/Logical Implication constraint solver used\nfor
  various Liquid Types. The solver uses SMTLIB2 to implement an algorithm similar
  to:\n\n+ [Houdini](https://users.soe.ucsc.edu/~cormac/papers/fme01.pdf)\n+ [cartesian
  predicate abstraction](http://swt.informatik.uni-freiburg.de/berit/papers/boolean-and-cartesian-....pdf)\n\n\nRequirements\n------------\n\nIn
  addition to the .cabal dependencies you require an SMTLIB2 compatible solver binary:\n\n-
  [Z3](http://z3.codeplex.com)\n- [CVC4](http://cvc4.cs.nyu.edu)\n- [MathSat](http://mathsat.fbk.eu/download.html)\n\nIf
  on Windows, please make sure to place the binary and any associated DLLs somewhere\nin
  your path.\n\nHow To Build and Install\n------------------------\n\nSimply do:\n\n
  \   git clone https://github.com/ucsd-progsys/liquid-fixpoint.git\n    cd liquid-fixpoint\n
  \   stack install\n\nor (`cabal` instead of `stack` if you prefer.)\n\n\nUsing SMTLIB-based
  SMT Solvers\n------------------------------\n\nYou can use one of several SMTLIB2
  compliant solvers, by:\n\n    fixpoint --smtsolver=z3 path/to/file.hs\n\nCurrently,
  we support\n\n    * Z3\n    * CVC4\n    * MathSat\n\n\n\nConfiguration Management\n------------------------\n\nIt
  is very important that the version of Liquid Fixpoint be maintained properly.\n\nSuppose
  that the current version of Liquid Haskell is `A.B.C.D`:\n\n+ After a release to
  hackage is made, if any of the components `B`, `C`, or `D` are missing, they shall
  be added and set to `0`. Then the `D` component of Liquid Fixpoint shall be incremented
  by `1`. The version of Liquid Fixpoint is now `A.B.C.(D + 1)`\n\n+ The first time
  a new function or type is exported from Liquid Fixpoint, if any of the components
  `B`, or `C` are missing, they shall be added and set to `0`. Then the `C` component
  shall be incremented by `1`, and the `D` component shall stripped. The version of
  Liquid Fixpoint is now `A.B.(C + 1)`\n\n+ The first time the signature of an exported
  function or type is changed, or an exported function or type is removed (this includes
  functions or types that Liquid Fixpoint re-exports from its own dependencies), if
  the `B` component is missing, it shall be added and set to `0`. Then the `B` component
  shall be incremented by `1`, and the `C` and `D` components shall be stripped. The
  version of Liquid Fixpoint is now `A.(B + 1)`\n\n+ The `A` component shall be updated
  at the sole discretion of the project owners.\n\nIt is recommended to use the [Bumper](https://hackage.haskell.org/package/bumper)
  utility to manage the versioning of Liquid Fixpoint. Bumper will automatically do
  the correct update to the cabal file. Additionally, it will update any packages
  that you have the source for that depend on Liquid Fixpoint.\n\nTo update Liquid
  Fixpoint and Liquid Haskell, first clone Liquid Haskell and Liquid Fixpoint to a
  common location:\n\n```\ngit clone https://github.com/ucsd-progsys/liquidhaskell.git\ngit
  clone https://github.com/ucsd-progsys/liquid-fixpoint.git\n```\n\nTo increment the
  `D` component of Liquid Fixpoint:\n\n```\n./path/to/bumper -3 liquid-fixpoint\n```\n\nThis
  will update the `D` component of Liquid Fixpoint. If necessary, this will update
  the `Build-Depends` of Liquid Haskell. If the `Build-Depends` was updated, Liquid
  Haskell's `D` component will be incremented.\n\nTo increment the `C` component of
  Liquid Fixpoint, and strip the `D` component:\n\n```\n./path/to/bumper --minor liquid-fixpoint\n```\n\nAs
  before, this will update Liquid Fixpoint and, if necessary, Liquid Haskell.\n\nTo
  increment the `B` component of Liquid Fixpoint, and strip the `D` and `C` components:\n\n```\n./path/to/bumper
  --major liquid-fixpoint\n```\n\nAs before, this will update Liquid Fixpoint and,
  if necessary, Liquid Haskell\n\nSMTLIB2 Interface\n-----------------\n\nThere is
  a new SMTLIB2 interface directly from Haskell:\n\n+ Language.Fixpoint.SmtLib2\n\nSee
  `tests/smt2/{Smt.hs, foo.smt2}` for an example of how to use it.\n\nOptions\n-------\n\n`--higherorder`
  allows higher order binders into the environment\n\n`--extsolver` runs the **deprecated**
  external solver.\n\n`--parts` Partitions an `FInfo` into a `[FInfo]` and emits a
  bunch of files. So:\n\n    $ fixpoint -n -p path/to/foo.fq\n\nwill now emit files:\n\n
  \   path/to/.liquid/foo.1.fq\n    path/to/.liquid/foo.2.fq\n    . . .\n    path/to/.liquid/foo.k.fq\n\nand
  also a dot file with the constraint dependency graph:\n\n    path/to/.liquid/foo.fq.dot\n\n\n##
  FInfo Invariants\n\n### Binders\n\nThis is the field\n\n```\n     , bs       ::
  !BindEnv         -- ^ Bind  |-> (Symbol, SortedReft)\n```\n\nor in the .fq files
  as\n\n```\nbind 1 x : ...\nbind 2 y : ...\n```\n\n* Each `BindId` must be a distinct
  `Int`,\n* Each `BindId` that appears in a constraint\n  environment i.e. inside
  _any_ `IBindEnv`\n  must appear inside the `bs`\n\n### Environments\n\n* Each constraint's
  environment is a set of `BindId`\n  which must be defined in the `bindInfo`. Furthermore\n\n*
  Each constraint should not have _duplicate_ names in its\n  environment, that is
  if you have two binders\n\n```\n  bind 1 x : ...\n  bind 12 x : ...\n```\n\n  Then
  a single `IBindEnv` should only mention _at most_\n  one of `1` or `12`.\n\n* There
  is also a \"tree-shape\" property that its a bit hard\n  to describe ... TODO     \n\n###
  LHS\n\nEach `slhs` of a constraint is a `SortedReft`.\n\n- Each `SortredReft` is
  basically a `Reft` -- a logical predicate.\n  The important bit is that a `KVar`
  i.e. terms of the formalized\n\n```\n     $k1[x1:=y1][x2:=y2]...[xn:=yn]\n```\n\n
  \ That is represented in the `Expr` type as\n\n```\n  | PKVar  !KVar !Subst\n```\n\n
  \ must appear _only_ at the **top-level** that is not under _any_\n  other operators,
  i.e. not as a sub-`Expr` of other expressions.\n\n\n- This is basically a predicate
  that needs to be \"well sorted\"\n  with respect to the `BindId`, intuitively\n\n```\n
  \   x:int, y:int |- x + y : int\n```\n\n  is well sorted. but\n\n```\n    x:int
  \ |- x + y : int\n```\n\n  is not, and\n\n```\n    x:int, y: list |- x + y : int\n```\n\n
  \ is not. The exact definition is formalized in `Language.Fixpoint.SortCheck`\n\n\n###
  RHS\n\nSimilarly each `rhs` of a `SubC` must either be a single `$k[...]` or an
  plain `$k`-free `Expr`.\n\n### Global vs. Distinct Literals\n\n```\n     , gLits
  \   :: !(SEnv Sort)               -- ^ Global Constant symbols\n     , dLits    ::
  !(SEnv Sort)       \n```\n\nThe _global_ literals `gLits` are symbols that\nare
  in scope _everywhere_ i.e. need not be separately\ndefined in individual environments.
  These include things like\n\n- uninterpreted _measure_ functions `len`, `height`,\n-
  uninterpreted _data constructor_ literals `True`, `False`\n\nSuppose you have an
  enumerated type like:\n\n```\ndata Day = Sun | Mon | Tue | Wed | ... | Sat\n```\n\nYou
  can model the above values in fixpoint as:\n\n```\nconstant lit#Sun : Day\nconstant
  lit#Mon : Day\nconstant lit#Tue : Day\nconstant lit#Wed : Day\n```\n\nThe _distinct_
  literals are a subset of the above where we\nwant to tell the SMT solver that the
  values are *distinct*\ni.e. **not equal** to each other, for example, you can\n**additionally**
  specify this as:\n\n```\ndistinct lit#Sun : Day\ndistinct lit#Mon : Day\ndistinct
  lit#Tue : Day\ndistinct lit#Wed : Day\n```\n\nThe above two are represented programmatically
  by generating   \nsuitable `Symbol` values (for the literals  see `litSymbol`)\nand
  `Sort` values as `FTC FTycon` and then making an `SEnv`\nfrom the `[(Symbol, Sort)]`.\n\n###
  Sorts\n\n> What's the difference between an FTC and an FObj?\n\nIn early versions
  of fixpoint, there was support for \nthree sorts for expressions (`Expr`) that were
  sent \nto the SMT solver:\n\n1. `int`\n2. `bool`\n3. \"other\"\n\nThe `FObj` sort
  was introduced to represent essentially _all_ \nnon-int and non-bool values (e.g.
  tuples, lists, trees, pointers...)\n\nHowever, we later realized that it is valuable
  to keep _more_\nprecise information for `Expr`s and so we introduced the `FTC`\n(fixpoint
  type constructor), which lets us represent the above\nrespectively as:\n\n- `FTC
  \"String\" []`                   -- in Haskell `String`\n- `FTC \"Tuple\"  [FInt,
  Bool]`         -- in Haskell `(Int, Bool)`\n- `FTC \"List\" [FTC \"List\" [FInt]]`
  \   -- in Haskell `[[Int]]`\n\n> There is a comment that says FObj's are uninterpretted
  types;\n> so probably a type the SMT solver doesn't know about?\n> Does that then
  make FTC types that the SMT solver does\n> know about (bools, ints, lists, sets,
  etc.)?\n\nThe SMT solver knows about `bool`, `int` and `set` (also `bitvector` \nand
  `map`) but _all_ other types are _currently_ represented as plain \n`Int` inside
  the SMT solver. However, we _will be_ changing this \nto make use of SMT support
  for ADTs ...\n\nTo sum up: the `FObj` is there for historical reasons; it has been
  \nsubsumed by `FTC` which is what I recomend you use. However `FObj` \nis there
  if you want a simple \"unitype\" / \"any\" type for terms \nthat are not \"interpreted\".\n\n"
license-name: BSD3
{'fraction_non_alphanumeric': 0.15289711390174046, 'fraction_numerical': 0.021590658735404274, 'mean_word_length': 3.077245508982036, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 27, 'https://': 12, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 33, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 1, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5276772', 'n_tokens_mistral': 5357, 'n_tokens_neox': 5063, 'n_words': 1540}