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.


In addition to the .cabal dependencies you require


[Last Documentation]

  • 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


Automatic Flags

Link to Z3


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


Versions [RSS],,,,,,,,,,,,,,,,,,,,,,,,,,,, 8.10.7 (info)
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
Category Language
Home page
Source repo head: git clone
Uploaded by EricSeidel at 2014-09-03T04:29:34Z
Reverse Dependencies 5 direct, 17 indirect [details]
Executables fixpoint, fixpoint.native
Downloads 19487 total (142 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2016-12-13 [all 5 reports]