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

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

Requirements

In addition to the .cabal dependencies you require

Flags

Automatic Flags
NameDescriptionDefault
z3mem

Link to Z3

Disabled

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

Downloads

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, 8.10.7 (info)
Dependencies ansi-terminal, array, base (>=4 && <5), bifunctors, bytestring, cmdargs, containers, deepseq, directory, filemanip, filepath, ghc (==7.6.3), ghc-prim, hashable (<1.2), liquid-fixpoint, mtl, parsec, pretty, process, syb, text, unordered-containers [details]
License BSD-3-Clause
Author Ranjit Jhala
Maintainer jhala@cs.ucsd.edu
Category Language
Home page https://github.com/ucsd-progsys/liquid-fixpoint
Uploaded by EricSeidel at 2013-09-23T07:49:04Z
Distributions
Reverse Dependencies 5 direct, 17 indirect [details]
Executables fixpoint
Downloads 19232 total (123 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user [build log]
All reported builds failed [all 1 reports]