liquid-fixpoint: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

[ bsd3, language, library, program ] [ Propose Tags ]

This package is a Haskell wrapper to the SMTLIB-based Horn-Clause/Logical Implication constraint solver used for Liquid Types.

The solver itself is written in Ocaml.

The package includes:

  1. Types for Expressions, Predicates, Constraints, Solutions

  2. Code for serializing the above

  3. Code for parsing the results from the fixpoint.native binary

  4. The Ocaml fixpoint code and pre-compiled binaries

  5. (Deprecated) Z3 binaries if you want to link against the API.

Requirements

In addition to the .cabal dependencies you require

Versions [faq] 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, 0.7.0.1, 0.7.0.2, 0.7.0.3, 0.7.0.5, 0.7.0.6, 0.7.0.7
Dependencies ansi-terminal, array, attoparsec, base (>=4.7 && <5), bifunctors, bytestring, cmdargs, containers, deepseq, directory, filemanip, filepath, ghc-prim, hashable, intern, liquid-fixpoint, mtl, parsec, pretty, process, syb, text, text-format, transformers, unordered-containers [details]
License BSD-3-Clause
Copyright 2010-15 Ranjit Jhala, University of California, San Diego.
Author Ranjit Jhala, Niki Vazou, Eric Seidel
Maintainer jhala@cs.ucsd.edu
Revised Revision 2 made by EricSeidel at Wed Aug 12 21:05:48 UTC 2015
Category Language
Home page https://github.com/ucsd-progsys/liquid-fixpoint
Source repo head: git clone https://github.com/ucsd-progsys/liquid-fixpoint/
Uploaded by EricSeidel at Wed Aug 12 20:21:26 UTC 2015
Distributions
Executables fixpoint, fixpoint.native
Downloads 7453 total (175 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs available [build log]
Last success reported on 2015-08-12 [all 1 reports]

Modules

[Index]

Flags

NameDescriptionDefaultType
z3mem

Link to Z3

DisabledAutomatic
build-external

Build fixpoint.native binary from source (requires ocaml)

DisabledAutomatic

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

Maintainer's Corner

For package maintainers and hackage trustees