liquid-fixpoint: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
This package is a Haskell wrapper to the SMTLIB-based Horn-Clause/Logical Implication constraint solver used for Liquid Types.
The package includes:
Types for Expressions, Predicates, Constraints, Solutions
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.
Modules
[Index]
- Language
- Fixpoint
- Language.Fixpoint.Defunctionalize
- Language.Fixpoint.Graph
- Language.Fixpoint.Minimize
- Language.Fixpoint.Misc
- Language.Fixpoint.Parse
- Smt
- Language.Fixpoint.Solver
- Language.Fixpoint.Solver.Eliminate
- Language.Fixpoint.Solver.GradualSolution
- Language.Fixpoint.Solver.Instantiate
- Language.Fixpoint.Solver.Monad
- Language.Fixpoint.Solver.Sanitize
- Language.Fixpoint.Solver.Solution
- Language.Fixpoint.Solver.Solve
- Language.Fixpoint.Solver.TrivialSort
- Language.Fixpoint.Solver.UniqifyBinds
- Language.Fixpoint.Solver.UniqifyKVars
- Language.Fixpoint.Solver.Worklist
- Language.Fixpoint.SortCheck
- Language.Fixpoint.Types
- Language.Fixpoint.Types.Config
- Language.Fixpoint.Types.Constraints
- Language.Fixpoint.Types.Environments
- Language.Fixpoint.Types.Errors
- Language.Fixpoint.Types.Graduals
- Language.Fixpoint.Types.Names
- Language.Fixpoint.Types.PrettyPrint
- Language.Fixpoint.Types.Refinements
- Language.Fixpoint.Types.Solutions
- Language.Fixpoint.Types.Sorts
- Language.Fixpoint.Types.Spans
- Language.Fixpoint.Types.Substitutions
- Language.Fixpoint.Types.Theories
- Language.Fixpoint.Types.Triggers
- Language.Fixpoint.Types.Utils
- Language.Fixpoint.Types.Visitor
- Utils
- Fixpoint
Flags
Manual Flags
| Name | Description | Default |
|---|---|---|
| devel | turn on stricter error reporting for development | Disabled |
Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info
Downloads
- liquid-fixpoint-0.7.0.5.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
| Versions [RSS] | 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, 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 (info) |
|---|---|
| Dependencies | ansi-terminal, array, ascii-progress (>=0.3), async, attoparsec, base (>=4.8.1.0 && <5), bifunctors, binary, boxes, bytestring, cereal, cmdargs, containers, deepseq, directory, dotgen, fgl, fgl-visualize, filemanip, filepath, ghc-prim, hashable, intern, liquid-fixpoint, located-base, mtl, parallel, parallel-io, parsec, pretty, process, syb, text, text-format, time, transformers, unordered-containers [details] |
| Tested with | ghc ==7.10.3, ghc ==8.0.1 |
| License | BSD-3-Clause |
| Copyright | 2010-17 Ranjit Jhala, University of California, San Diego. |
| 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 ranjitjhala at 2017-10-07T12:32:52Z |
| Distributions | |
| Reverse Dependencies | 5 direct, 17 indirect [details] |
| Executables | fixpoint |
| Downloads | 20126 total (68 in the last 30 days) |
| Rating | (no votes yet) [estimated by Bayesian average] |
| Your Rating | |
| Status | Docs available [build log] Last success reported on 2017-10-07 [all 1 reports] |