liquid-fixpoint: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.
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:
Types for Expressions, Predicates, Constraints, Solutions
Code for serializing the above
Code for parsing the results from the fixpoint.native binary
The Ocaml fixpoint code
(Deprecated) Z3 binaries if you want to link against the API.
Requirements
In addition to the .cabal dependencies you require
A Recent Ocaml compiler
A Z3 Binary (http://z3.codeplex.com)
Properties
| Versions | 0.1.0.0, 0.2.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, 0.8.0.2, 0.8.10.1, 0.8.10.2, 0.8.10.7, 0.9.0.2.1, 0.9.2.5, 0.9.4.7, 0.9.6.3, 0.9.6.3.1, 8.10.7 |
|---|---|
| Change log | None available |
| Dependencies | ansi-terminal, array, attoparsec, base (>=4 && <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 |
| Author | Ranjit Jhala, Niki Vazou, Eric Seidel |
| Maintainer | jhala@cs.ucsd.edu |
| 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 2014-09-03T04:28:36Z |
Modules
- Language
- Fixpoint
- Language.Fixpoint.Config
- Language.Fixpoint.Errors
- Language.Fixpoint.Files
- Language.Fixpoint.Interface
- Language.Fixpoint.Misc
- Language.Fixpoint.Names
- Language.Fixpoint.Parse
- Language.Fixpoint.PrettyPrint
- Language.Fixpoint.SmtLib2
- Language.Fixpoint.Sort
- Language.Fixpoint.Types
- Fixpoint
Flags
Automatic Flags
| Name | Description | Default |
|---|---|---|
| z3mem | Link to Z3 | Disabled |
Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info
Downloads
- liquid-fixpoint-0.2.0.0.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
Package maintainers
For package maintainers and hackage trustees